diff options
34 files changed, 151 insertions, 112 deletions
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 1852cacc0..7ea1138e3 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -1771,7 +1771,7 @@ struct AbcPass : public Pass { extra_args(args, argidx, design); 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()) log_cmd_error("Got -constr but no -liberty!\n"); diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc index 47da98b06..531ac2b99 100644 --- a/passes/techmap/iopadmap.cc +++ b/passes/techmap/iopadmap.cc @@ -234,6 +234,9 @@ struct IopadmapPass : public Pass { SigBit wire_bit(wire, i); Cell *tbuf_cell = nullptr; + if (skip_wire_bits.count(wire_bit)) + continue; + if (tbuf_bits.count(wire_bit)) tbuf_cell = tbuf_bits.at(wire_bit); diff --git a/techlibs/anlogic/cells_map.v b/techlibs/anlogic/cells_map.v index cfc743a4b..8ac087d9d 100644 --- a/techlibs/anlogic/cells_map.v +++ b/techlibs/anlogic/cells_map.v @@ -6,14 +6,14 @@ module \$_DFFE_NP_ (input D, C, E, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REG module \$_DFFE_PN_ (input D, C, E, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'bx), .SRMUX("SR"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(E), .sr(1'b0)); endmodule module \$_DFFE_PP_ (input D, C, E, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'bx), .SRMUX("SR"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(E), .sr(1'b0)); endmodule -module \$_DFF_NN0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("INV"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_NN1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("INV"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_NP0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("SR"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_NP1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("SR"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_PN0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("INV"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C) , .ce(1'b1), .sr(R)); endmodule -module \$_DFF_PN1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("INV"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_PP0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("SR"), .SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule -module \$_DFF_PP1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("SR"), . SRMODE("SYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_NN0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("INV"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_NN1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("INV"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_NP0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("SR"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_NP1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("SR"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(~C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_PN0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("INV"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C) , .ce(1'b1), .sr(R)); endmodule +module \$_DFF_PN1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("INV"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_PP0_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b0), .SRMUX("SR"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule +module \$_DFF_PP1_ (input D, C, R, output Q); AL_MAP_SEQ #(.DFFMODE("FF"), .REGSET(1'b1), .SRMUX("SR"), . SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.d(D), .q(Q), .clk(C), .ce(1'b1), .sr(R)); endmodule module \$_DLATCH_N_ (E, D, Q); wire [1023:0] _TECHMAP_DO_ = "simplemap; opt"; diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v index 3bcbfc9aa..c27b0f02b 100644 --- a/techlibs/xilinx/cells_sim.v +++ b/techlibs/xilinx/cells_sim.v @@ -1112,8 +1112,8 @@ module RAM16X1D_1 ( endmodule module RAM32X1D ( - // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 - (* abc9_arrival=1153 *) + // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857 + (* abc9_arrival=1188 *) output DPO, SPO, input D, (* clkbuf_sink *) @@ -1135,8 +1135,8 @@ module RAM32X1D ( endmodule module RAM32X1D_1 ( - // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 - (* abc9_arrival=1153 *) + // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857 + (* abc9_arrival=1188 *) output DPO, SPO, input D, (* clkbuf_sink *) @@ -1158,7 +1158,7 @@ module RAM32X1D_1 ( endmodule 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 *) output DPO, SPO, input D, @@ -1181,7 +1181,7 @@ module RAM64X1D ( endmodule 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 *) output DPO, SPO, input D, @@ -1204,8 +1204,9 @@ module RAM64X1D_1 ( endmodule module RAM128X1D ( - // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 - (* abc9_arrival=1153 *) + // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L889 + // plus 204ps to cross MUXF7 + (* abc9_arrival=1357 *) output DPO, SPO, input D, (* clkbuf_sink *) @@ -1244,9 +1245,18 @@ endmodule // Multi port. module RAM32M ( - // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L957 - (* abc9_arrival=1153 *) - output [1:0] DOA, DOB, DOC, DOD, + // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L857 + (* abc9_arrival=1188 *) + 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 [1:0] DIA, DIB, DIC, DID, (* clkbuf_sink *) @@ -1347,9 +1357,18 @@ module RAM32M16 ( endmodule 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 *) - 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 DIA, DIB, DIC, DID, (* clkbuf_sink *) @@ -1508,7 +1527,7 @@ module SRL16 ( endmodule 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 *) output Q, input A0, A1, A2, A3, CE, @@ -1572,9 +1591,10 @@ module SRLC16E ( endmodule 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 *) output Q, + // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLM_R.sdf#L904 (* abc9_arrival=1114 *) output Q31, input [4:0] A, @@ -2216,7 +2236,7 @@ module DSP48E1 ( parameter [6:0] IS_OPMODE_INVERTED = 7'b0; initial begin -`ifdef __ICARUS__ +`ifndef YOSYS if (AUTORESET_PATDET != "NO_RESET") $fatal(1, "Unsupported AUTORESET_PATDET value"); if (SEL_MASK != "MASK") $fatal(1, "Unsupported SEL_MASK value"); if (SEL_PATTERN != "PATTERN") $fatal(1, "Unsupported SEL_PATTERN value"); @@ -2379,12 +2399,12 @@ module DSP48E1 ( case (OPMODEr[1:0]) 2'b00: X = 48'b0; 2'b01: begin X = $signed(Mrx); -`ifdef __ICARUS__ +`ifndef YOSYS if (OPMODEr[3:2] != 2'b01) $fatal(1, "OPMODEr[3:2] must be 2'b01 when OPMODEr[1:0] is 2'b01"); `endif end 2'b10: begin X = P; -`ifdef __ICARUS__ +`ifndef YOSYS if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[1:0] is 2'b10"); `endif end @@ -2396,7 +2416,7 @@ module DSP48E1 ( case (OPMODEr[3:2]) 2'b00: Y = 48'b0; 2'b01: begin Y = 48'b0; // FIXME: more accurate partial product modelling? -`ifdef __ICARUS__ +`ifndef YOSYS if (OPMODEr[1:0] != 2'b01) $fatal(1, "OPMODEr[1:0] must be 2'b01 when OPMODEr[3:2] is 2'b01"); `endif end @@ -2410,13 +2430,13 @@ module DSP48E1 ( 3'b000: Z = 48'b0; 3'b001: Z = PCIN; 3'b010: begin Z = P; -`ifdef __ICARUS__ +`ifndef YOSYS if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] i0s 3'b010"); `endif end 3'b011: Z = Cr; 3'b100: begin Z = P; -`ifdef __ICARUS__ +`ifndef YOSYS if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b100"); if (OPMODEr[3:0] != 4'b1000) $fatal(1, "OPMODEr[3:0] must be 4'b1000 when OPMODEr[6:4] i0s 3'b100"); `endif diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc index 215a48f95..b0c4795ee 100644 --- a/techlibs/xilinx/synth_xilinx.cc +++ b/techlibs/xilinx/synth_xilinx.cc @@ -64,7 +64,7 @@ struct SynthXilinxPass : public ScriptPass log(" (this feature is experimental and incomplete)\n"); log("\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(" -nobram\n"); log(" do not use block RAM cells in output netlist\n"); @@ -84,11 +84,9 @@ struct SynthXilinxPass : public ScriptPass log(" -nodsp\n"); log(" do not use DSP48E1s to implement multipliers and associated logic\n"); log("\n"); - log(" -iopad\n"); - log(" enable I/O buffer insertion (selected automatically by -ise)\n"); - log("\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(" -noclkbuf\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; - 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; int widemux; @@ -136,7 +134,6 @@ struct SynthXilinxPass : public ScriptPass retime = false; vpr = false; ise = false; - iopad = false; noiopad = false; noclkbuf = false; nocarry = false; @@ -213,7 +210,6 @@ struct SynthXilinxPass : public ScriptPass continue; } if (args[argidx] == "-iopad") { - iopad = true; continue; } if (args[argidx] == "-noiopad") { @@ -282,7 +278,6 @@ struct SynthXilinxPass : public ScriptPass void script() YS_OVERRIDE { - bool do_iopad = iopad || (ise && !noiopad); std::string ff_map_file; if (help_mode) ff_map_file = "+/xilinx/{family}_ff_map.v"; @@ -517,8 +512,8 @@ struct SynthXilinxPass : public ScriptPass if (check_label("map_cells")) { // Needs to be done before logic optimization, so that inverters (OE vs T) are handled. - if (help_mode || do_iopad) - 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')"); + 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 not '-noiopad')"); std::string techmap_args = "-map +/techmap.v -map +/xilinx/cells_map.v"; if (widemux > 0) techmap_args += stringf(" -D MIN_MUX_INPUTS=%d", widemux); diff --git a/tests/arch/anlogic/counter.ys b/tests/arch/anlogic/counter.ys index d363ec24e..a6eab248c 100644 --- a/tests/arch/anlogic/counter.ys +++ b/tests/arch/anlogic/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic # equivalency check 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 diff --git a/tests/arch/ecp5/counter.ys b/tests/arch/ecp5/counter.ys index f9f60fbff..e46001ffe 100644 --- a/tests/arch/ecp5/counter.ys +++ b/tests/arch/ecp5/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +equiv_opt -assert -multiclock -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) cd top # Constrain all select calls below inside the top module select -assert-count 4 t:CCU2C diff --git a/tests/arch/ecp5/macc.ys b/tests/arch/ecp5/macc.ys index 1863ea4d2..8da8d2f8e 100644 --- a/tests/arch/ecp5/macc.ys +++ b/tests/arch/ecp5/macc.ys @@ -3,8 +3,8 @@ hierarchy -top top proc # Blocked by issue #1358 (Missing ECP5 simulation models) #equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check -equiv_opt -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) +synth_ecp5 +#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 select -assert-count 1 t:MULT18X18D select -assert-count 4 t:CCU2C diff --git a/tests/arch/ecp5/mul.ys b/tests/arch/ecp5/mul.ys index 2105be52c..f887e9585 100644 --- a/tests/arch/ecp5/mul.ys +++ b/tests/arch/ecp5/mul.ys @@ -3,9 +3,9 @@ hierarchy -top top proc # Blocked by issue #1358 (Missing ECP5 simulation models) #equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check -equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +synth_ecp5 -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 select -assert-count 1 t:MULT18X18D select -assert-none t:MULT18X18D %% t:* %D diff --git a/tests/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys index d20b8ae27..f8fb29a87 100644 --- a/tests/arch/efinix/counter.ys +++ b/tests/arch/efinix/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check +equiv_opt -assert -multiclock -map +/efinix/cells_sim.v synth_efinix # equivalency check 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 diff --git a/tests/arch/gowin/counter.ys b/tests/arch/gowin/counter.ys index 920479d44..bdbc7ee24 100644 --- a/tests/arch/gowin/counter.ys +++ b/tests/arch/gowin/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/gowin/cells_sim.v synth_gowin # equivalency check +equiv_opt -assert -multiclock -map +/gowin/cells_sim.v synth_gowin # equivalency check 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 diff --git a/tests/arch/ice40/counter.ys b/tests/arch/ice40/counter.ys index f112eb97d..7bbc4f2c3 100644 --- a/tests/arch/ice40/counter.ys +++ b/tests/arch/ice40/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 # equivalency check 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 select -assert-count 6 t:SB_CARRY diff --git a/tests/arch/ice40/mul.ys b/tests/arch/ice40/mul.ys index 9891b77d6..b8c3eb941 100644 --- a/tests/arch/ice40/mul.ys +++ b/tests/arch/ice40/mul.ys @@ -1,6 +1,6 @@ read_verilog ../common/mul.v hierarchy -top top -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check 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 select -assert-count 1 t:SB_MAC16 diff --git a/tests/arch/ice40/rom.v b/tests/arch/ice40/rom.v index 0a0f41f37..71459fe38 100644 --- a/tests/arch/ice40/rom.v +++ b/tests/arch/ice40/rom.v @@ -2,7 +2,8 @@ Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74]. */ module top(data, addr); -output [3:0] data; +output [3:0] data; // Note: this prompts a Yosys warning, but + // vendor doc does not contain 'reg' input [4:0] addr; always @(addr) begin case (addr) diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys index 9dbddce47..313948cc5 100644 --- a/tests/arch/xilinx/add_sub.ys +++ b/tests/arch/xilinx/add_sub.ys @@ -1,7 +1,7 @@ read_verilog ../common/add_sub.v hierarchy -top top 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) cd top # Constrain all select calls below inside the top module select -assert-count 14 t:LUT2 diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys index c0ff6a2e2..3328f9edc 100644 --- a/tests/arch/xilinx/adffs.ys +++ b/tests/arch/xilinx/adffs.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top adff 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) cd adff # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDCE %% t:* %D design -load read hierarchy -top adffn 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) cd adffn # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -28,7 +28,7 @@ select -assert-none t:BUFG t:FDCE t:INV %% t:* %D design -load read hierarchy -top dffs 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) cd dffs # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -40,7 +40,7 @@ select -assert-none t:BUFG t:FDSE %% t:* %D design -load read hierarchy -top ndffnr 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) cd ndffnr # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys index 4c881b280..7bdd94a63 100644 --- a/tests/arch/xilinx/attributes_test.ys +++ b/tests/arch/xilinx/attributes_test.ys @@ -1,7 +1,7 @@ # Check that blockram memory without parameters is not modified read_verilog ../common/memory_attributes/attributes_test.v 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 select -assert-count 1 t:RAMB18E1 @@ -9,7 +9,7 @@ select -assert-count 1 t:RAMB18E1 design -reset read_verilog ../common/memory_attributes/attributes_test.v 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 select -assert-count 8 t:RAM32X1D @@ -18,7 +18,7 @@ design -reset read_verilog ../common/memory_attributes/attributes_test.v prep 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 select -assert-count 32 t:RAM128X1D @@ -27,7 +27,7 @@ design -reset read_verilog ../common/memory_attributes/attributes_test.v prep 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 select -assert-count 0 t:RAMB18E1 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 design -reset 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 select -assert-count 1 t:RAMB18E1 # Set synthesis, ram_block block to a distributed memory; will be implemented as blockram design -reset 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 select -assert-count 1 t:RAMB18E1 diff --git a/tests/arch/xilinx/blockram.ys b/tests/arch/xilinx/blockram.ys index bb908cbbf..ed743cf44 100644 --- a/tests/arch/xilinx/blockram.ys +++ b/tests/arch/xilinx/blockram.ys @@ -3,28 +3,28 @@ # Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1 read_verilog ../common/blockram.v 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 select -assert-count 1 t:RAMB18E1 design -reset read_verilog ../common/blockram.v 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 select -assert-count 1 t:RAMB18E1 design -reset read_verilog ../common/blockram.v 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 select -assert-count 1 t:RAMB18E1 design -reset read_verilog ../common/blockram.v 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 select -assert-count 1 t:RAMB18E1 @@ -32,7 +32,7 @@ select -assert-count 1 t:RAMB18E1 design -reset read_verilog ../common/blockram.v 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 select -assert-count 0 t:RAMB18E1 select -assert-count 4 t:RAM128X1D @@ -41,7 +41,7 @@ select -assert-count 4 t:RAM128X1D design -reset read_verilog ../common/blockram.v 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 select -assert-count 1 t:RAMB36E1 @@ -52,7 +52,7 @@ design -reset read_verilog ../common/blockram.v hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 setattr -set ram_style "block" m:memory -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 1 t:RAMB18E1 @@ -60,7 +60,7 @@ design -reset read_verilog ../common/blockram.v hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 setattr -set ram_block 1 m:memory -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 1 t:RAMB18E1 @@ -68,7 +68,7 @@ design -reset read_verilog ../common/blockram.v 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 -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 0 t:RAMB18E1 @@ -76,7 +76,7 @@ design -reset read_verilog ../common/blockram.v hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 setattr -set logic_block 1 m:memory -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 0 t:RAMB18E1 @@ -84,7 +84,7 @@ design -reset read_verilog ../common/blockram.v hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 setattr -set ram_style "block" m:memory -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 1 t:RAMB18E1 @@ -92,6 +92,6 @@ design -reset read_verilog ../common/blockram.v hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 setattr -set ram_block 1 m:memory -synth_xilinx -top sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad cd sync_ram_sdp select -assert-count 1 t:RAMB18E1 diff --git a/tests/arch/xilinx/bug1460.ys b/tests/arch/xilinx/bug1460.ys index 2018071cc..09935ccd8 100644 --- a/tests/arch/xilinx/bug1460.ys +++ b/tests/arch/xilinx/bug1460.ys @@ -28,7 +28,7 @@ module register_file( endmodule EOT -synth_xilinx +synth_xilinx -noiopad cd register_file select -assert-count 32 t:RAM32M select -assert-none t:* t:BUFG %d t:RAM32M %d diff --git a/tests/arch/xilinx/bug1605.ys b/tests/arch/xilinx/bug1605.ys new file mode 100644 index 000000000..4be659860 --- /dev/null +++ b/tests/arch/xilinx/bug1605.ys @@ -0,0 +1,19 @@ +read_verilog <<EOT +module top(inout io); + wire in; + wire t; + wire o; + + IOBUF IOBUF( + .I(in), + .T(t), + .IO(io), + .O(o) + ); +endmodule +EOT + +synth_xilinx +cd top +select -assert-count 1 t:IOBUF +select -assert-none t:* t:IOBUF %d diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys index 604acdbfc..11c29922e 100644 --- a/tests/arch/xilinx/counter.ys +++ b/tests/arch/xilinx/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc 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) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys index 0bba4858f..dc764b033 100644 --- a/tests/arch/xilinx/dffs.ys +++ b/tests/arch/xilinx/dffs.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top dff 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) cd dff # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D design -load read hierarchy -top dffe 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) cd dffe # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG diff --git a/tests/arch/xilinx/dsp_cascade.ys b/tests/arch/xilinx/dsp_cascade.ys index f9185551b..ca6b619b9 100644 --- a/tests/arch/xilinx/dsp_cascade.ys +++ b/tests/arch/xilinx/dsp_cascade.ys @@ -19,7 +19,7 @@ EOT proc 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 cd cascade 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 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 cd cascade select -assert-count 3 t:DSP48A1 @@ -65,7 +65,7 @@ EOT proc 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 cd cascade 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 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 cd cascade select -assert-count 2 t:DSP48A1 diff --git a/tests/arch/xilinx/dsp_fastfir.ys b/tests/arch/xilinx/dsp_fastfir.ys index 0067a822b..57fe49bde 100644 --- a/tests/arch/xilinx/dsp_fastfir.ys +++ b/tests/arch/xilinx/dsp_fastfir.ys @@ -63,7 +63,7 @@ module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_re endmodule EOT -synth_xilinx +synth_xilinx -noiopad cd fastfir_dynamictaps select -assert-count 2 t:DSP48E1 select -assert-none t:* t:DSP48E1 %d t:BUFG %d diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys index f03400fe7..3235d5af3 100644 --- a/tests/arch/xilinx/fsm.ys +++ b/tests/arch/xilinx/fsm.ys @@ -3,7 +3,7 @@ hierarchy -top fsm proc 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 sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys index c87a8e38b..e226c2ec8 100644 --- a/tests/arch/xilinx/latches.ys +++ b/tests/arch/xilinx/latches.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top latchp 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) cd latchp # Constrain all select calls below inside the top module select -assert-count 1 t:LDCE @@ -14,7 +14,7 @@ select -assert-none t:LDCE %% t:* %D design -load read hierarchy -top latchn 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) cd latchn # Constrain all select calls below inside the top module select -assert-count 1 t:LDCE @@ -26,7 +26,7 @@ select -assert-none t:LDCE t:INV %% t:* %D design -load read hierarchy -top latchsr 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) cd latchsr # Constrain all select calls below inside the top module select -assert-count 1 t:LDCE diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys index d5b5c1a37..61a9314cc 100644 --- a/tests/arch/xilinx/logic.ys +++ b/tests/arch/xilinx/logic.ys @@ -1,7 +1,7 @@ read_verilog ../common/logic.v hierarchy -top top 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) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys index 6c9d1eae1..3f127a77e 100644 --- a/tests/arch/xilinx/lutram.ys +++ b/tests/arch/xilinx/lutram.ys @@ -2,7 +2,7 @@ #hierarchy -top lutram_1w1r -chparam A_WIDTH 4 #proc #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 #opt -full # @@ -22,7 +22,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r -chparam A_WIDTH 5 proc 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 opt -full @@ -42,7 +42,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r proc 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 opt -full @@ -62,7 +62,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w3r proc 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 opt -full @@ -82,7 +82,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w3r -chparam A_WIDTH 6 proc 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 opt -full @@ -102,7 +102,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6 proc 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 opt -full @@ -122,7 +122,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6 proc 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 opt -full diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys index 11e959976..bf2b36320 100644 --- a/tests/arch/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys @@ -3,8 +3,8 @@ design -save read hierarchy -top macc proc -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad miter -equiv -flatten -make_assert -make_outputs gold gate 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) @@ -17,8 +17,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D design -load read hierarchy -top macc2 proc -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad miter -equiv -flatten -make_assert -make_outputs gold gate 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) diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys index 6cf994fbf..490846ff1 100644 --- a/tests/arch/xilinx/mul.ys +++ b/tests/arch/xilinx/mul.ys @@ -1,7 +1,7 @@ read_verilog ../common/mul.v hierarchy -top top 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) cd top # Constrain all select calls below inside the top module @@ -13,7 +13,7 @@ design -reset read_verilog ../common/mul.v hierarchy -top top 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) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys index c714680af..980263cbd 100644 --- a/tests/arch/xilinx/mul_unsigned.ys +++ b/tests/arch/xilinx/mul_unsigned.ys @@ -2,7 +2,7 @@ read_verilog mul_unsigned.v hierarchy -top mul_unsigned 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) cd mul_unsigned # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -16,7 +16,7 @@ read_verilog mul_unsigned.v hierarchy -top mul_unsigned 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) cd mul_unsigned # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys index 388272449..99817738d 100644 --- a/tests/arch/xilinx/mux.ys +++ b/tests/arch/xilinx/mux.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top mux2 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) cd mux2 # Constrain all select calls below inside the top module select -assert-count 1 t:LUT3 @@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D design -load read hierarchy -top mux4 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) cd mux4 # Constrain all select calls below inside the top module select -assert-count 1 t:LUT6 @@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D design -load read hierarchy -top mux8 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) cd mux8 # Constrain all select calls below inside the top module select -assert-count 1 t:LUT3 @@ -37,7 +37,7 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D design -load read hierarchy -top mux16 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) cd mux16 # Constrain all select calls below inside the top module select -assert-min 5 t:LUT6 diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys index 455437f18..3652319a0 100644 --- a/tests/arch/xilinx/shifter.ys +++ b/tests/arch/xilinx/shifter.ys @@ -2,7 +2,7 @@ read_verilog ../common/shifter.v hierarchy -top top proc 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) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys index 4697703ca..eaccab126 100644 --- a/tests/arch/xilinx/tribuf.ys +++ b/tests/arch/xilinx/tribuf.ys @@ -7,6 +7,7 @@ synth 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) 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 1 t:$_TBUF_ -select -assert-none t:$_TBUF_ %% t:* %D +select -assert-count 2 t:IBUF +select -assert-count 1 t:INV +select -assert-count 1 t:OBUFT +select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D |