mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor

Browse source
This commit is contained in:
Eddie Hung 2019-12-30 16:01:38 -08:00
parent f348ffa44d 22fe931c86
commit 658f424d7d
29 changed files with 196 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
backends/aiger/xaiger.cc
View file

@ -599,25 +599,46 @@ struct XAigerWriter
RTLIL::Module *holes_module = module->design->addModule("$__holes__"); RTLIL::Module *holes_module = module->design->addModule("$__holes__");
log_assert(holes_module); log_assert(holes_module);
dict<IdString, Cell*> cell_cache;
int port_id = 1; int port_id = 1;
int box_count = 0; int box_count = 0;
for (auto cell : box_list) { for (auto cell : box_list) {
RTLIL::Module* box_module = module->design->module(cell->type); RTLIL::Module* orig_box_module = module->design->module(cell->type);
log_assert(orig_box_module);
IdString derived_name = orig_box_module->derive(module->design, cell->parameters);
RTLIL::Module* box_module = module->design->module(derived_name);
if (box_module->has_processes())
log_error("ABC9 box '%s' contains processes!\n", box_module->name.c_str());
int box_inputs = 0, box_outputs = 0; int box_inputs = 0, box_outputs = 0;
Cell *holes_cell = nullptr; auto r = cell_cache.insert(std::make_pair(derived_name, nullptr));
if (box_module->get_bool_attribute("\\whitebox")) { Cell *holes_cell = r.first->second;
if (r.second && box_module->get_bool_attribute("\\whitebox")) {
holes_cell = holes_module->addCell(cell->name, cell->type); holes_cell = holes_module->addCell(cell->name, cell->type);
holes_cell->parameters = cell->parameters; holes_cell->parameters = cell->parameters;
r.first->second = holes_cell;
// Since Module::derive() will create a new module, there
// is a chance that the ports will be alphabetically ordered
// again, which is a problem when carry-chains are involved.
// Inherit the port ordering from the original module here...
// (and set the port_id below, when iterating through those)
log_assert(GetSize(box_module->ports) == GetSize(orig_box_module->ports));
box_module->ports = orig_box_module->ports;
} }
// NB: Assume box_module->ports are sorted alphabetically // NB: Assume box_module->ports are sorted alphabetically
// (as RTLIL::Module::fixup_ports() would do) // (as RTLIL::Module::fixup_ports() would do)
int box_port_id = 1;
for (const auto &port_name : box_module->ports) { for (const auto &port_name : box_module->ports) {
RTLIL::Wire *w = box_module->wire(port_name); RTLIL::Wire *w = box_module->wire(port_name);
log_assert(w); log_assert(w);
if (r.second)
w->port_id = box_port_id++;
RTLIL::Wire *holes_wire; RTLIL::Wire *holes_wire;
RTLIL::SigSpec port_wire; RTLIL::SigSpec port_sig;
if (w->port_input) { if (w->port_input)
for (int i = 0; i < GetSize(w); i++) { for (int i = 0; i < GetSize(w); i++) {
box_inputs++; box_inputs++;
holes_wire = holes_module->wire(stringf("\\i%d", box_inputs)); holes_wire = holes_module->wire(stringf("\\i%d", box_inputs));
@ -628,28 +649,29 @@ struct XAigerWriter
holes_module->ports.push_back(holes_wire->name); holes_module->ports.push_back(holes_wire->name);
} }
if (holes_cell) if (holes_cell)
port_wire.append(holes_wire); port_sig.append(holes_wire);
} }
if (!port_wire.empty())
holes_cell->setPort(w->name, port_wire);
}
if (w->port_output) { if (w->port_output) {
box_outputs += GetSize(w); box_outputs += GetSize(w);
for (int i = 0; i < GetSize(w); i++) { for (int i = 0; i < GetSize(w); i++) {
if (GetSize(w) == 1) if (GetSize(w) == 1)
holes_wire = holes_module->addWire(stringf("%s.%s", cell->name.c_str(), w->name.c_str())); holes_wire = holes_module->addWire(stringf("%s.%s", cell->name.c_str(), log_id(w->name)));
else else
holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), w->name.c_str(), i)); holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), log_id(w->name), i));
holes_wire->port_output = true; holes_wire->port_output = true;
holes_wire->port_id = port_id++; holes_wire->port_id = port_id++;
holes_module->ports.push_back(holes_wire->name); holes_module->ports.push_back(holes_wire->name);
if (holes_cell) if (holes_cell)
port_wire.append(holes_wire); port_sig.append(holes_wire);
else else
holes_module->connect(holes_wire, State::S0); holes_module->connect(holes_wire, State::S0);
} }
if (!port_wire.empty()) }
holes_cell->setPort(w->name, port_wire); if (!port_sig.empty()) {
if (r.second)
holes_cell->setPort(w->name, port_sig);
else
holes_module->connect(holes_cell->getPort(w->name), port_sig);
} }
} }
@ -679,14 +701,11 @@ struct XAigerWriter
RTLIL::Selection& sel = holes_module->design->selection_stack.back(); RTLIL::Selection& sel = holes_module->design->selection_stack.back();
sel.select(holes_module); sel.select(holes_module);
// TODO: Should not need to opt_merge if we only instantiate
// each box type once...
Pass::call(holes_module->design, "opt_merge -share_all");
Pass::call(holes_module->design, "flatten -wb"); Pass::call(holes_module->design, "flatten -wb");
// TODO: Should techmap/aigmap/check all lib_whitebox-es just once, // Cannot techmap/aigmap/check all lib_whitebox-es outside of write_xaiger
// instead of per write_xaiger call // since boxes may contain parameters in which case `flatten` would have
// created a new $paramod ...
Pass::call(holes_module->design, "techmap"); Pass::call(holes_module->design, "techmap");
Pass::call(holes_module->design, "aigmap"); Pass::call(holes_module->design, "aigmap");
for (auto cell : holes_module->cells()) for (auto cell : holes_module->cells())

2
passes/techmap/abc.cc
View file

@ -1767,7 +1767,7 @@ struct AbcPass : public Pass {
extra_args(args, argidx, design); extra_args(args, argidx, design);
if (!lut_costs.empty() && !liberty_file.empty()) if (!lut_costs.empty() && !liberty_file.empty())
log_cmd_error("Got -lut and -liberty! This two options are exclusive.\n"); log_cmd_error("Got -lut and -liberty! These two options are exclusive.\n");
if (!constr_file.empty() && liberty_file.empty()) if (!constr_file.empty() && liberty_file.empty())
log_cmd_error("Got -constr but no -liberty!\n"); log_cmd_error("Got -constr but no -liberty!\n");

12
techlibs/ecp5/cells_sim.v
View file

@ -1,5 +1,6 @@
// --------------------------------------- // ---------------------------------------
(* lib_whitebox *)
module LUT4(input A, B, C, D, output Z); module LUT4(input A, B, C, D, output Z);
parameter [15:0] INIT = 16'h0000; parameter [15:0] INIT = 16'h0000;
wire [7:0] s3 = D ? INIT[15:8] : INIT[7:0]; wire [7:0] s3 = D ? INIT[15:8] : INIT[7:0];
@ -31,13 +32,8 @@ module CCU2C(
// First half // First half
wire LUT4_0, LUT2_0; wire LUT4_0, LUT2_0;
`ifdef _ABC
assign LUT4_0 = INIT0[{D0, C0, B0, A0}];
assign LUT2_0 = INIT0[{2'b00, B0, A0}];
`else
LUT4 #(.INIT(INIT0)) lut4_0(.A(A0), .B(B0), .C(C0), .D(D0), .Z(LUT4_0)); LUT4 #(.INIT(INIT0)) lut4_0(.A(A0), .B(B0), .C(C0), .D(D0), .Z(LUT4_0));
LUT2 #(.INIT(INIT0[3:0])) lut2_0(.A(A0), .B(B0), .Z(LUT2_0)); LUT2 #(.INIT(INIT0[3:0])) lut2_0(.A(A0), .B(B0), .Z(LUT2_0));
`endif
wire gated_cin_0 = (INJECT1_0 == "YES") ? 1'b0 : CIN; wire gated_cin_0 = (INJECT1_0 == "YES") ? 1'b0 : CIN;
assign S0 = LUT4_0 ^ gated_cin_0; assign S0 = LUT4_0 ^ gated_cin_0;
@ -46,13 +42,8 @@ module CCU2C(
// Second half // Second half
wire LUT4_1, LUT2_1; wire LUT4_1, LUT2_1;
`ifdef _ABC
assign LUT4_1 = INIT1[{D1, C1, B1, A1}];
assign LUT2_1 = INIT1[{2'b00, B1, A1}];
`else
LUT4 #(.INIT(INIT1)) lut4_1(.A(A1), .B(B1), .C(C1), .D(D1), .Z(LUT4_1)); LUT4 #(.INIT(INIT1)) lut4_1(.A(A1), .B(B1), .C(C1), .D(D1), .Z(LUT4_1));
LUT2 #(.INIT(INIT1[3:0])) lut2_1(.A(A1), .B(B1), .Z(LUT2_1)); LUT2 #(.INIT(INIT1[3:0])) lut2_1(.A(A1), .B(B1), .Z(LUT2_1));
`endif
wire gated_cin_1 = (INJECT1_1 == "YES") ? 1'b0 : cout_0; wire gated_cin_1 = (INJECT1_1 == "YES") ? 1'b0 : cout_0;
assign S1 = LUT4_1 ^ gated_cin_1; assign S1 = LUT4_1 ^ gated_cin_1;
@ -209,6 +200,7 @@ endmodule
// --------------------------------------- // ---------------------------------------
(* lib_whitebox *)
module LUT2(input A, B, output Z); module LUT2(input A, B, output Z);
parameter [3:0] INIT = 4'h0; parameter [3:0] INIT = 4'h0;
wire [1:0] s1 = B ? INIT[ 3:2] : INIT[1:0]; wire [1:0] s1 = B ? INIT[ 3:2] : INIT[1:0];

2
techlibs/ecp5/synth_ecp5.cc
View file

@ -230,7 +230,7 @@ struct SynthEcp5Pass : public ScriptPass
{ {
if (check_label("begin")) if (check_label("begin"))
{ {
run("read_verilog -D_ABC -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v"); run("read_verilog -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v");
run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str())); run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
} }

50
techlibs/xilinx/cells_sim.v
View file

@ -1112,8 +1112,8 @@ module RAM16X1D_1 (
endmodule endmodule
module RAM32X1D ( module RAM32X1D (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857
(* abc9_arrival=1153 *) (* abc9_arrival=1188 *)
output DPO, SPO, output DPO, SPO,
input D, input D,
(* clkbuf_sink *) (* clkbuf_sink *)
@ -1135,8 +1135,8 @@ module RAM32X1D (
endmodule endmodule
module RAM32X1D_1 ( module RAM32X1D_1 (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857
(* abc9_arrival=1153 *) (* abc9_arrival=1188 *)
output DPO, SPO, output DPO, SPO,
input D, input D,
(* clkbuf_sink *) (* clkbuf_sink *)
@ -1158,7 +1158,7 @@ module RAM32X1D_1 (
endmodule endmodule
module RAM64X1D ( module RAM64X1D (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L889
(* abc9_arrival=1153 *) (* abc9_arrival=1153 *)
output DPO, SPO, output DPO, SPO,
input D, input D,
@ -1181,7 +1181,7 @@ module RAM64X1D (
endmodule endmodule
module RAM64X1D_1 ( module RAM64X1D_1 (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L889
(* abc9_arrival=1153 *) (* abc9_arrival=1153 *)
output DPO, SPO, output DPO, SPO,
input D, input D,
@ -1204,8 +1204,9 @@ module RAM64X1D_1 (
endmodule endmodule
module RAM128X1D ( module RAM128X1D (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L889
(* abc9_arrival=1153 *) // plus 204ps to cross MUXF7
(* abc9_arrival=1357 *)
output DPO, SPO, output DPO, SPO,
input D, input D,
(* clkbuf_sink *) (* clkbuf_sink *)
@ -1244,9 +1245,18 @@ endmodule
// Multi port. // Multi port.
module RAM32M ( module RAM32M (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857
(* abc9_arrival=1153 *) (* abc9_arrival=1188 *)
output [1:0] DOA, DOB, DOC, DOD, output [1:0] DOA,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L925
(* abc9_arrival=1187 *)
output [1:0] DOB,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L993
(* abc9_arrival=1180 *)
output [1:0] DOC,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L1061
(* abc9_arrival=1190 *)
output [1:0] DOD,
input [4:0] ADDRA, ADDRB, ADDRC, ADDRD, input [4:0] ADDRA, ADDRB, ADDRC, ADDRD,
input [1:0] DIA, DIB, DIC, DID, input [1:0] DIA, DIB, DIC, DID,
(* clkbuf_sink *) (* clkbuf_sink *)
@ -1347,9 +1357,18 @@ module RAM32M16 (
endmodule endmodule
module RAM64M ( module RAM64M (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L889
(* abc9_arrival=1153 *) (* abc9_arrival=1153 *)
output DOA, DOB, DOC, DOD, output DOA,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957
(* abc9_arrival=1161 *)
output DOB,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L1025
(* abc9_arrival=1158 *)
output DOC,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L1093
(* abc9_arrival=1163 *)
output DOD,
input [5:0] ADDRA, ADDRB, ADDRC, ADDRD, input [5:0] ADDRA, ADDRB, ADDRC, ADDRD,
input DIA, DIB, DIC, DID, input DIA, DIB, DIC, DID,
(* clkbuf_sink *) (* clkbuf_sink *)
@ -1508,7 +1527,7 @@ module SRL16 (
endmodule endmodule
module SRL16E ( module SRL16E (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L904-L905 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L905
(* abc9_arrival=1472 *) (* abc9_arrival=1472 *)
output Q, output Q,
input A0, A1, A2, A3, CE, input A0, A1, A2, A3, CE,
@ -1572,9 +1591,10 @@ module SRLC16E (
endmodule endmodule
module SRLC32E ( module SRLC32E (
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L904-L905 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L905
(* abc9_arrival=1472 *) (* abc9_arrival=1472 *)
output Q, output Q,
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L904
(* abc9_arrival=1114 *) (* abc9_arrival=1114 *)
output Q31, output Q31,
input [4:0] A, input [4:0] A,

17
techlibs/xilinx/synth_xilinx.cc
View file

@ -64,7 +64,7 @@ struct SynthXilinxPass : public ScriptPass
log(" (this feature is experimental and incomplete)\n"); log(" (this feature is experimental and incomplete)\n");
log("\n"); log("\n");
log(" -ise\n"); log(" -ise\n");
log(" generate an output netlist suitable for ISE (enables -iopad)\n"); log(" generate an output netlist suitable for ISE\n");
log("\n"); log("\n");
log(" -nobram\n"); log(" -nobram\n");
log(" do not use block RAM cells in output netlist\n"); log(" do not use block RAM cells in output netlist\n");
@ -84,11 +84,9 @@ struct SynthXilinxPass : public ScriptPass
log(" -nodsp\n"); log(" -nodsp\n");
log(" do not use DSP48E1s to implement multipliers and associated logic\n"); log(" do not use DSP48E1s to implement multipliers and associated logic\n");
log("\n"); log("\n");
log(" -iopad\n");
log(" enable I/O buffer insertion (selected automatically by -ise)\n");
log("\n");
log(" -noiopad\n"); log(" -noiopad\n");
log(" disable I/O buffer insertion (only useful with -ise)\n"); log(" disable I/O buffer insertion (useful for hierarchical or \n");
log(" out-of-context flows)\n");
log("\n"); log("\n");
log(" -noclkbuf\n"); log(" -noclkbuf\n");
log(" disable automatic clock buffer insertion\n"); log(" disable automatic clock buffer insertion\n");
@ -122,7 +120,7 @@ struct SynthXilinxPass : public ScriptPass
} }
std::string top_opt, edif_file, blif_file, family; std::string top_opt, edif_file, blif_file, family;
bool flatten, retime, vpr, ise, iopad, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram, abc9; bool flatten, retime, vpr, ise, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram, abc9;
bool flatten_before_abc; bool flatten_before_abc;
int widemux; int widemux;
@ -136,7 +134,6 @@ struct SynthXilinxPass : public ScriptPass
retime = false; retime = false;
vpr = false; vpr = false;
ise = false; ise = false;
iopad = false;
noiopad = false; noiopad = false;
noclkbuf = false; noclkbuf = false;
nocarry = false; nocarry = false;
@ -213,7 +210,6 @@ struct SynthXilinxPass : public ScriptPass
continue; continue;
} }
if (args[argidx] == "-iopad") { if (args[argidx] == "-iopad") {
iopad = true;
continue; continue;
} }
if (args[argidx] == "-noiopad") { if (args[argidx] == "-noiopad") {
@ -282,7 +278,6 @@ struct SynthXilinxPass : public ScriptPass
void script() YS_OVERRIDE void script() YS_OVERRIDE
{ {
bool do_iopad = iopad || (ise && !noiopad);
std::string ff_map_file; std::string ff_map_file;
if (help_mode) if (help_mode)
ff_map_file = "+/xilinx/{family}_ff_map.v"; ff_map_file = "+/xilinx/{family}_ff_map.v";
@ -517,8 +512,8 @@ struct SynthXilinxPass : public ScriptPass
if (check_label("map_cells")) { if (check_label("map_cells")) {
// Needs to be done before logic optimization, so that inverters (OE vs T) are handled. // Needs to be done before logic optimization, so that inverters (OE vs T) are handled.
if (help_mode || do_iopad) if (help_mode || !noiopad)
run("iopadmap -bits -outpad OBUF I:O -inpad IBUF O:I -toutpad $__XILINX_TOUTPAD OE:I:O -tinoutpad $__XILINX_TINOUTPAD OE:O:I:IO A:top", "(only if '-iopad' or '-ise' and not '-noiopad')"); run("iopadmap -bits -outpad OBUF I:O -inpad IBUF O:I -toutpad $__XILINX_TOUTPAD OE:I:O -tinoutpad $__XILINX_TINOUTPAD OE:O:I:IO A:top", "(only if not '-noiopad')");
std::string techmap_args = "-map +/techmap.v -map +/xilinx/cells_map.v"; std::string techmap_args = "-map +/techmap.v -map +/xilinx/cells_map.v";
if (widemux > 0) if (widemux > 0)
techmap_args += stringf(" -D MIN_MUX_INPUTS=%d", widemux); techmap_args += stringf(" -D MIN_MUX_INPUTS=%d", widemux);

16
tests/arch/ecp5/bug1598.ys Normal file
View file

@ -0,0 +1,16 @@
read_verilog <<EOT
module led_blink (
input clk,
output ledc
);
reg [6:0] led_counter = 0;
always @( posedge clk ) begin
led_counter <= led_counter + 1;
end
assign ledc = !led_counter[ 6:3 ];
endmodule
EOT
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -abc9

6
tests/arch/ecp5/mux.ys
View file

@ -39,8 +39,8 @@ proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module cd mux16 # Constrain all select calls below inside the top module
select -assert-count 8 t:L6MUX21 select -assert-count 12 t:L6MUX21
select -assert-count 26 t:LUT4 select -assert-count 34 t:LUT4
select -assert-count 12 t:PFUMX select -assert-count 17 t:PFUMX
select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D

16
tests/arch/ice40/bug1598.ys Normal file
View file

@ -0,0 +1,16 @@
read_verilog <<EOT
module led_blink (
input clk,
output ledc
);
reg [6:0] led_counter = 0;
always @( posedge clk ) begin
led_counter <= led_counter + 1;
end
assign ledc = !led_counter[ 6:3 ];
endmodule
EOT
proc
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -abc9

2
tests/arch/xilinx/add_sub.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/add_sub.v read_verilog ../common/add_sub.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
select -assert-count 14 t:LUT2 select -assert-count 14 t:LUT2

8
tests/arch/xilinx/adffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top adff hierarchy -top adff
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adff # Constrain all select calls below inside the top module cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDCE %% t:* %D
design -load read design -load read
hierarchy -top adffn hierarchy -top adffn
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adffn # Constrain all select calls below inside the top module cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -28,7 +28,7 @@ select -assert-none t:BUFG t:FDCE t:INV %% t:* %D
design -load read design -load read
hierarchy -top dffs hierarchy -top dffs
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffs # Constrain all select calls below inside the top module cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -40,7 +40,7 @@ select -assert-none t:BUFG t:FDSE %% t:* %D
design -load read design -load read
hierarchy -top ndffnr hierarchy -top ndffnr
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

12
tests/arch/xilinx/attributes_test.ys
View file

@ -1,7 +1,7 @@
# Check that blockram memory without parameters is not modified # Check that blockram memory without parameters is not modified
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top block_ram hierarchy -top block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -9,7 +9,7 @@ select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top distributed_ram hierarchy -top distributed_ram
synth_xilinx -top distributed_ram synth_xilinx -top distributed_ram -noiopad
cd distributed_ram # Constrain all select calls below inside the top module cd distributed_ram # Constrain all select calls below inside the top module
select -assert-count 8 t:RAM32X1D select -assert-count 8 t:RAM32X1D
@ -18,7 +18,7 @@ design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
prep prep
setattr -mod -set ram_style "distributed" block_ram setattr -mod -set ram_style "distributed" block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 32 t:RAM128X1D select -assert-count 32 t:RAM128X1D
@ -27,7 +27,7 @@ design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
prep prep
setattr -mod -set logic_block 1 block_ram setattr -mod -set logic_block 1 block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
select -assert-count 32 t:RAM128X1D select -assert-count 32 t:RAM128X1D
@ -35,13 +35,13 @@ select -assert-count 32 t:RAM128X1D
# Set ram_style block to a distributed memory; will be implemented as blockram # Set ram_style block to a distributed memory; will be implemented as blockram
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
synth_xilinx -top distributed_ram_manual synth_xilinx -top distributed_ram_manual -noiopad
cd distributed_ram_manual # Constrain all select calls below inside the top module cd distributed_ram_manual # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
# Set synthesis, ram_block block to a distributed memory; will be implemented as blockram # Set synthesis, ram_block block to a distributed memory; will be implemented as blockram
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
synth_xilinx -top distributed_ram_manual_syn synth_xilinx -top distributed_ram_manual_syn -noiopad
cd distributed_ram_manual_syn # Constrain all select calls below inside the top module cd distributed_ram_manual_syn # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1

24
tests/arch/xilinx/blockram.ys
View file

@ -3,28 +3,28 @@
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1 # Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -32,7 +32,7 @@ select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
select -assert-count 4 t:RAM128X1D select -assert-count 4 t:RAM128X1D
@ -41,7 +41,7 @@ select -assert-count 4 t:RAM128X1D
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB36E1 select -assert-count 1 t:RAMB36E1
@ -52,7 +52,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory setattr -set ram_style "block" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -60,7 +60,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_block 1 m:memory setattr -set ram_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -68,7 +68,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
@ -76,7 +76,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set logic_block 1 m:memory setattr -set logic_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
@ -84,7 +84,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory setattr -set ram_style "block" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -92,6 +92,6 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_block 1 m:memory setattr -set ram_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1

2
tests/arch/xilinx/bug1460.ys
View file

@ -28,7 +28,7 @@ module register_file(
endmodule endmodule
EOT EOT
synth_xilinx synth_xilinx -noiopad
cd register_file cd register_file
select -assert-count 32 t:RAM32M select -assert-count 32 t:RAM32M
select -assert-none t:* t:BUFG %d t:RAM32M %d select -assert-none t:* t:BUFG %d t:RAM32M %d

16
tests/arch/xilinx/bug1598.ys Normal file
View file

@ -0,0 +1,16 @@
read_verilog <<EOT
module led_blink (
input clk,
output ledc
);
reg [6:0] led_counter = 0;
always @( posedge clk ) begin
led_counter <= led_counter + 1;
end
assign ledc = !led_counter[ 6:3 ];
endmodule
EOT
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9

2
tests/arch/xilinx/counter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module

4
tests/arch/xilinx/dffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top dff hierarchy -top dff
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

8
tests/arch/xilinx/dsp_cascade.ys
View file

@ -19,7 +19,7 @@ EOT
proc proc
design -save read design -save read
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
design -load postopt design -load postopt
cd cascade cd cascade
select -assert-count 3 t:DSP48E1 select -assert-count 3 t:DSP48E1
@ -35,7 +35,7 @@ select -assert-none t:DSP48E1 t:BUFG %% t:* %D
select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
design -load read design -load read
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
design -load postopt design -load postopt
cd cascade cd cascade
select -assert-count 3 t:DSP48A1 select -assert-count 3 t:DSP48A1
@ -65,7 +65,7 @@ EOT
proc proc
design -save read design -save read
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
design -load postopt design -load postopt
cd cascade cd cascade
select -assert-count 2 t:DSP48E1 select -assert-count 2 t:DSP48E1
@ -75,7 +75,7 @@ select -assert-none t:DSP48E1 t:BUFG %% t:* %D
select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
design -load read design -load read
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
design -load postopt design -load postopt
cd cascade cd cascade
select -assert-count 2 t:DSP48A1 select -assert-count 2 t:DSP48A1

2
tests/arch/xilinx/dsp_fastfir.ys
View file

@ -63,7 +63,7 @@ module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_re
endmodule endmodule
EOT EOT
synth_xilinx synth_xilinx -noiopad
cd fastfir_dynamictaps cd fastfir_dynamictaps
select -assert-count 2 t:DSP48E1 select -assert-count 2 t:DSP48E1
select -assert-none t:* t:DSP48E1 %d t:BUFG %d select -assert-none t:* t:DSP48E1 %d t:BUFG %d

2
tests/arch/xilinx/fsm.ys
View file

@ -3,7 +3,7 @@ hierarchy -top fsm
proc proc
flatten flatten
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -make_assert -flatten gold gate miter miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter

6
tests/arch/xilinx/latches.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top latchp hierarchy -top latchp
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchp # Constrain all select calls below inside the top module cd latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE
@ -14,7 +14,7 @@ select -assert-none t:LDCE %% t:* %D
design -load read design -load read
hierarchy -top latchn hierarchy -top latchn
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchn # Constrain all select calls below inside the top module cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE
@ -26,7 +26,7 @@ select -assert-none t:LDCE t:INV %% t:* %D
design -load read design -load read
hierarchy -top latchsr hierarchy -top latchsr
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchsr # Constrain all select calls below inside the top module cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE

2
tests/arch/xilinx/logic.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/logic.v read_verilog ../common/logic.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module

14
tests/arch/xilinx/lutram.ys
View file

@ -2,7 +2,7 @@
#hierarchy -top lutram_1w1r -chparam A_WIDTH 4 #hierarchy -top lutram_1w1r -chparam A_WIDTH 4
#proc #proc
#memory -nomap #memory -nomap
#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx #equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
#memory #memory
#opt -full #opt -full
# #
@ -22,7 +22,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 hierarchy -top lutram_1w1r -chparam A_WIDTH 5
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -42,7 +42,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r hierarchy -top lutram_1w1r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -62,7 +62,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r hierarchy -top lutram_1w3r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -82,7 +82,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r -chparam A_WIDTH 6 hierarchy -top lutram_1w3r -chparam A_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -102,7 +102,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6 hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -122,7 +122,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6 hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full

8
tests/arch/xilinx/macc.ys
View file

@ -3,8 +3,8 @@ design -save read
hierarchy -top macc hierarchy -top macc
proc proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
@ -17,8 +17,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
design -load read design -load read
hierarchy -top macc2 hierarchy -top macc2
proc proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)

4
tests/arch/xilinx/mul.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/mul.v read_verilog ../common/mul.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
@ -13,7 +13,7 @@ design -reset
read_verilog ../common/mul.v read_verilog ../common/mul.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module

4
tests/arch/xilinx/mul_unsigned.ys
View file

@ -2,7 +2,7 @@ read_verilog mul_unsigned.v
hierarchy -top mul_unsigned hierarchy -top mul_unsigned
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned # Constrain all select calls below inside the top module cd mul_unsigned # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -16,7 +16,7 @@ read_verilog mul_unsigned.v
hierarchy -top mul_unsigned hierarchy -top mul_unsigned
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned # Constrain all select calls below inside the top module cd mul_unsigned # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

8
tests/arch/xilinx/mux.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top mux2 hierarchy -top mux2
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux2 # Constrain all select calls below inside the top module cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3 select -assert-count 1 t:LUT3
@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D
design -load read design -load read
hierarchy -top mux4 hierarchy -top mux4
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux4 # Constrain all select calls below inside the top module cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT6 select -assert-count 1 t:LUT6
@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux8 hierarchy -top mux8
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3 select -assert-count 1 t:LUT3
@ -37,7 +37,7 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux16 hierarchy -top mux16
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module cd mux16 # Constrain all select calls below inside the top module
select -assert-min 5 t:LUT6 select -assert-min 5 t:LUT6

2
tests/arch/xilinx/shifter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module

7
tests/arch/xilinx/tribuf.ys
View file

@ -7,6 +7,7 @@ synth
equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd tristate # Constrain all select calls below inside the top module cd tristate # Constrain all select calls below inside the top module
# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225 select -assert-count 2 t:IBUF
select -assert-count 1 t:$_TBUF_ select -assert-count 1 t:INV
select -assert-none t:$_TBUF_ %% t:* %D select -assert-count 1 t:OBUFT
select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D