diff options
28 files changed, 207 insertions, 267 deletions
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 7ef2827bf..27cec7549 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -40,16 +40,6 @@ struct EquivMakeWorker pool<SigBit> undriven_bits; SigMap assign_map; - dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells - - CellTypes comb_ct; - - EquivMakeWorker() - { - comb_ct.setup_internals(); - comb_ct.setup_stdcells(); - } - void read_blacklists() { for (auto fn : blacklists) @@ -147,6 +137,7 @@ struct EquivMakeWorker { SigMap assign_map(equiv_mod); SigMap rd_signal_map; + SigPool primary_inputs; // list of cells without added $equiv cells auto cells_list = equiv_mod->cells().to_vector(); @@ -262,6 +253,9 @@ struct EquivMakeWorker gate_wire->port_input = false; equiv_mod->connect(gold_wire, wire); equiv_mod->connect(gate_wire, wire); + primary_inputs.add(assign_map(gold_wire)); + primary_inputs.add(assign_map(gate_wire)); + primary_inputs.add(wire); } else { @@ -288,31 +282,19 @@ struct EquivMakeWorker } } - init_bit2driven(); - - pool<Cell*> visited_cells; for (auto c : cells_list) for (auto &conn : c->connections()) if (!ct.cell_output(c->type, conn.first)) { SigSpec old_sig = assign_map(conn.second); SigSpec new_sig = rd_signal_map(old_sig); - - if(old_sig != new_sig) { - SigSpec tmp_sig = old_sig; - for (int i = 0; i < GetSize(old_sig); i++) { - SigBit old_bit = old_sig[i], new_bit = new_sig[i]; - - visited_cells.clear(); - if (check_signal_in_fanout(visited_cells, old_bit, new_bit)) - continue; - - log("Changing input %s of cell %s (%s): %s -> %s\n", - log_id(conn.first), log_id(c), log_id(c->type), - log_signal(old_bit), log_signal(new_bit)); - - tmp_sig[i] = new_bit; - } - c->setPort(conn.first, tmp_sig); + for (int i = 0; i < GetSize(old_sig); i++) + if (primary_inputs.check(old_sig[i])) + new_sig[i] = old_sig[i]; + if (old_sig != new_sig) { + log("Changing input %s of cell %s (%s): %s -> %s\n", + log_id(conn.first), log_id(c), log_id(c->type), + log_signal(old_sig), log_signal(new_sig)); + c->setPort(conn.first, new_sig); } } @@ -403,57 +385,6 @@ struct EquivMakeWorker } } - void init_bit2driven() - { - for (auto cell : equiv_mod->cells()) { - if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_))) - continue; - for (auto &conn : cell->connections()) - { - if (yosys_celltypes.cell_input(cell->type, conn.first)) - for (auto bit : assign_map(conn.second)) - { - bit2driven[bit].insert(cell); - } - } - } - } - - bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit) - { - if (source_bit == target_bit) - return true; - - if (bit2driven.count(source_bit) == 0) - return false; - - auto driven_cells = bit2driven.at(source_bit); - for (auto driven_cell: driven_cells) - { - bool is_comb = comb_ct.cell_known(driven_cell->type); - if (!is_comb) - continue; - - if (visited_cells.count(driven_cell) > 0) - continue; - visited_cells.insert(driven_cell); - - for (auto &conn: driven_cell->connections()) - { - if (yosys_celltypes.cell_input(driven_cell->type, conn.first)) - continue; - - for (auto bit: conn.second) { - bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit); - if (is_in_fanout == true) - return true; - } - } - } - - return false; - } - void run() { copy_to_equiv(); diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index 4d0400448..f5eb75730 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -60,13 +60,16 @@ struct EquivOptPass:public ScriptPass log(" -undef\n"); log(" enable modelling of undef states during equiv_induct.\n"); log("\n"); + log(" -nocheck\n"); + log(" disable running check before and after the command under test.\n"); + log("\n"); log("The following commands are executed by this verification command:\n"); help_script(); log("\n"); } std::string command, techmap_opts, make_opts; - bool assert, undef, multiclock, async2sync; + bool assert, undef, multiclock, async2sync, nocheck; void clear_flags() override { @@ -77,6 +80,7 @@ struct EquivOptPass:public ScriptPass undef = false; multiclock = false; async2sync = false; + nocheck = false; } void execute(std::vector < std::string > args, RTLIL::Design * design) override @@ -110,6 +114,10 @@ struct EquivOptPass:public ScriptPass undef = true; continue; } + if (args[argidx] == "-nocheck") { + nocheck = true; + continue; + } if (args[argidx] == "-multiclock") { multiclock = true; continue; @@ -153,10 +161,14 @@ struct EquivOptPass:public ScriptPass if (check_label("run_pass")) { run("hierarchy -auto-top"); run("design -save preopt"); + if (!nocheck) + run("check -assert", "(unless -nocheck)"); if (help_mode) run("[command]"); else run(command); + if (!nocheck) + run("check -assert", "(unless -nocheck)"); run("design -stash postopt"); } diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 2384ffced..bba2cbbec 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -26,6 +26,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct SampledSig { + SigSpec sampled, current; + SigSpec &operator[](bool get_current) { return get_current ? current : sampled; } +}; + struct Clk2fflogicPass : public Pass { Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } void help() override @@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass { log("implicit global clock. This is useful for formal verification of designs with\n"); log("multiple clocks.\n"); log("\n"); + log("This pass assumes negative hold time for the async FF inputs. For example when\n"); + log("a reset deasserts with the clock edge, then the FF output will still drive the\n"); + log("reset value in the next cycle regardless of the data-in value at the time of\n"); + log("the clock edge.\n"); + log("\n"); } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) { - if (!is_fine) - return wrap_async_control(module, sig, polarity, past_sig_id); - return wrap_async_control_gate(module, sig, polarity, past_sig_id); + // Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted. + SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) { + if (!polarity) { + if (is_fine) + sig = module->NotGate(NEW_ID, sig); + else + sig = module->Not(NEW_ID, sig); + } + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); + else + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id, GetSize(sig)); - past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig)); - module->addFf(NEW_ID, sig, past_sig); - if (polarity) - sig = module->Or(NEW_ID, sig, past_sig); + // Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge. + SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - sig = module->And(NEW_ID, sig, past_sig); - if (polarity) - return sig; + module->addFf(NEW_ID, sig, sampled_sig); + return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0}); + } + // Sampled and current value of a data signal. + SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = init; + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - return module->Not(NEW_ID, sig); + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id); - past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1; - module->addFfGate(NEW_ID, sig, past_sig); - if (polarity) - sig = module->OrGate(NEW_ID, sig, past_sig); + SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) { + if (is_fine) + return module->MuxGate(NEW_ID, a, b, s); else - sig = module->AndGate(NEW_ID, sig, past_sig); - if (polarity) - return sig; + return module->Mux(NEW_ID, a, b, s); + } + SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) { + if (is_fine) + return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)); else - return module->NotGate(NEW_ID, sig); + return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r)); } void execute(std::vector<std::string> args, RTLIL::Design *design) override { @@ -177,96 +210,47 @@ struct Clk2fflogicPass : public Pass { ff.remove(); - // Strip spaces from signal name, since Yosys IDs can't contain spaces - // Spaces only occur when we have a signal that's a slice of a larger bus, - // e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness - std::string sig_q_str = log_signal(ff.sig_q); - sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end()); - - Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width); - - if (!ff.is_fine) { - module->addFf(NEW_ID, ff.sig_q, past_q); - } else { - module->addFfGate(NEW_ID, ff.sig_q, past_q); - } - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_q, ff.val_init); - - if (ff.has_clk) { + if (ff.has_clk) ff.unmap_ce_srst(); - Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk)))); - initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0); - - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_clk, past_clk); - else - module->addFfGate(NEW_ID, ff.sig_clk, past_clk); + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled; - SigSpec clock_edge_pattern; - - if (ff.pol_clk) { - clock_edge_pattern.append(State::S0); - clock_edge_pattern.append(State::S1); - } else { - clock_edge_pattern.append(State::S1); - clock_edge_pattern.append(State::S0); - } - - SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern); - - Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width); - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_d, past_d); - else - module->addFfGate(NEW_ID, ff.sig_d, past_d); - - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_d, ff.val_init); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); - else - qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); - } else { - qval = past_q; + if (ff.has_clk) { + // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs + auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine); + auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine); + next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine); } + SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst; // The check for a constant sig_aload is also done by opt_dff, but when using verific and running // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids // generating a lot of extra logic. - if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) { - SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload); - else - qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload); + bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1); + if (has_nonconst_aload) { + sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine); + // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs + sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine); } - if (ff.has_sr) { - SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID); - SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID); - if (!ff.is_fine) { - clrval = module->Not(NEW_ID, clrval); - qval = module->Or(NEW_ID, qval, setval); - module->addAnd(NEW_ID, qval, clrval, ff.sig_q); - } else { - clrval = module->NotGate(NEW_ID, clrval); - qval = module->OrGate(NEW_ID, qval, setval); - module->addAndGate(NEW_ID, qval, clrval, ff.sig_q); - } - } else if (ff.has_arst) { - IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst))); - SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id); - if (!ff.is_fine) - module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q); - else - module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q); - } else { - module->connect(ff.sig_q, qval); + sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine); + sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine); + } + if (ff.has_arst) + sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine); + + // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous + // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously. + for (int current = 0; current < 2; current++) { + if (has_nonconst_aload) + next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine); + if (ff.has_sr) + next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine); + if (ff.has_arst) + next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine); } + + module->connect(ff.sig_q, next_q); } } } diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys index b7983cfa4..c1509cabc 100644 --- a/tests/arch/ice40/bug1597.ys +++ b/tests/arch/ice40/bug1597.ys @@ -3,7 +3,7 @@ module top ( input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5, PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25, output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18, - PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24, + PIN_19, ); assign USBPU = 0; @@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]); endmodule EOT +read_verilog -lib +/ice40/cells_sim.v hierarchy -top top flatten -equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index 71b68431e..e779ab207 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O); endmodule EOT +read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt design -load postopt select -assert-count 1 t:* diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 56c9cabb3..0a5b9356a 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 @@ -17,7 +17,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys index 0ba3901f7..79e5a322c 100644 --- a/tests/arch/xilinx/abc9_dff.ys +++ b/tests/arch/xilinx/abc9_dff.ys @@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 6 t:FD* @@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 4 t:FD* @@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 8 t:FD* @@ -75,6 +78,7 @@ always @(posedge clk or posedge pre) endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDCE @@ -94,6 +98,7 @@ assign q = ~r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co w:r %i @@ -111,6 +116,7 @@ assign q2 = r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co %a w:r %i @@ -128,6 +134,7 @@ assign o = r1 | r2; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys index a01d02179..2328919a3 100644 --- a/tests/arch/xilinx/opt_lut_ins.ys +++ b/tests/arch/xilinx/opt_lut_ins.ys @@ -18,6 +18,7 @@ end EOF +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx design -load postopt diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index c09699411..9f0b27ced 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -5,7 +5,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -52,7 +52,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -100,7 +100,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -137,7 +137,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -183,7 +183,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -232,7 +232,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; diff --git a/tests/opt/opt_dff_en.ys b/tests/opt/opt_dff_en.ys index 06ee6c63d..9538afcc2 100644 --- a/tests/opt/opt_dff_en.ys +++ b/tests/opt/opt_dff_en.ys @@ -6,7 +6,7 @@ module top(...); input CLK; input [1:0] D; -output [15:0] Q; +output [11:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_mux.ys b/tests/opt/opt_dff_mux.ys index ed01bed59..f21f9e9b8 100644 --- a/tests/opt/opt_dff_mux.ys +++ b/tests/opt/opt_dff_mux.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input NE, NS; input EN; -output [23:0] Q; +output [17:0] Q; input [23:0] D; input SRST; input ARST; diff --git a/tests/opt/opt_dff_qd.ys b/tests/opt/opt_dff_qd.ys index afc96c42f..7b0b4c224 100644 --- a/tests/opt/opt_dff_qd.ys +++ b/tests/opt/opt_dff_qd.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input EN; (* init = 24'h555555 *) -output [23:0] Q; +output [19:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_sr.ys b/tests/opt/opt_dff_sr.ys index 0961cb11e..1d3fd300e 100644 --- a/tests/opt/opt_dff_sr.ys +++ b/tests/opt/opt_dff_sr.ys @@ -22,10 +22,9 @@ EOT design -save orig -# Equivalence check will fail for unmapped adlatch and dlatchsr due to negative hold hack. -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=2 %i select -assert-count 1 t:$dffsre @@ -36,9 +35,9 @@ select -assert-none t:$sr design -load orig -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=4 %i select -assert-count 1 t:$dffsre @@ -51,9 +50,9 @@ select -assert-count 1 t:$sr r:WIDTH=4 %i design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 1 t:$_DFFE_PN0P_ @@ -65,9 +64,9 @@ select -assert-none t:$_DFF_PP0_ t:$_DFF_PP1_ t:$_DFFE_PN0P_ t:$_DFFE_PN1P_ t:$_ design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 2 t:$_DFFSR_PPP_ diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys index a879f3ec9..8874f2775 100644 --- a/tests/opt/opt_expr_xor.ys +++ b/tests/opt/opt_expr_xor.ys @@ -10,7 +10,7 @@ design -save read select -assert-count 2 t:$xor select -assert-count 2 t:$xnor -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$xor select -assert-none t:$xnor @@ -19,7 +19,7 @@ select -assert-count 2 t:$not design -load read simplemap -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XOR_ select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ @@ -34,7 +34,7 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1])); endmodule EOT select -assert-count 2 t:$_XNOR_ -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ select -assert-count 1 t:$_NOT_ @@ -49,7 +49,7 @@ assign y = a~^1'b0; assign z = a~^1'b1; endmodule EOT -equiv_opt opt_expr +equiv_opt -assert opt_expr # Single-bit $xor diff --git a/tests/techmap/adff2dff.ys b/tests/techmap/adff2dff.ys index 53f7d2f08..6d03d1963 100644 --- a/tests/techmap/adff2dff.ys +++ b/tests/techmap/adff2dff.ys @@ -16,4 +16,4 @@ EOT proc -equiv_opt -async2sync techmap -map +/adff2dff.v +#equiv_opt -assert -async2sync techmap -map +/adff2dff.v diff --git a/tests/techmap/dff2ff.ys b/tests/techmap/dff2ff.ys index 5adf14b07..6e7e6082b 100644 --- a/tests/techmap/dff2ff.ys +++ b/tests/techmap/dff2ff.ys @@ -13,4 +13,4 @@ EOT proc -equiv_opt techmap -map +/dff2ff.v +equiv_opt -assert techmap -map +/dff2ff.v diff --git a/tests/techmap/dfflegalize_adlatch.ys b/tests/techmap/dfflegalize_adlatch.ys index b242cc809..559363301 100644 --- a/tests/techmap/dfflegalize_adlatch.ys +++ b/tests/techmap/dfflegalize_adlatch.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_adlatch_init.ys b/tests/techmap/dfflegalize_adlatch_init.ys index a55082d1d..8e371c528 100644 --- a/tests/techmap/dfflegalize_adlatch_init.ys +++ b/tests/techmap/dfflegalize_adlatch_init.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_aldff.ys b/tests/techmap/dfflegalize_aldff.ys index 1ee9e3af6..5be3e9742 100644 --- a/tests/techmap/dfflegalize_aldff.ys +++ b/tests/techmap/dfflegalize_aldff.ys @@ -24,8 +24,8 @@ design -save orig flatten equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_aldff_init.ys b/tests/techmap/dfflegalize_aldff_init.ys index f4db8dd32..ffa7cbf16 100644 --- a/tests/techmap/dfflegalize_aldff_init.ys +++ b/tests/techmap/dfflegalize_aldff_init.ys @@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_dffsr_init.ys b/tests/techmap/dfflegalize_dffsr_init.ys index ce5a32f76..b6160bb87 100644 --- a/tests/techmap/dfflegalize_dffsr_init.ys +++ b/tests/techmap/dfflegalize_dffsr_init.ys @@ -41,18 +41,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ADFFs. diff --git a/tests/techmap/dfflegalize_dlatchsr_init.ys b/tests/techmap/dfflegalize_dlatchsr_init.ys index b38a9eb3b..da4ca164e 100644 --- a/tests/techmap/dfflegalize_dlatchsr_init.ys +++ b/tests/techmap/dfflegalize_dlatchsr_init.ys @@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2])); $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3])); endmodule -module top(input C, E, R, S, D, output [17:0] Q); +module top(input C, E, R, S, D, output [7:0] Q); dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0])); dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4])); endmodule @@ -23,12 +23,12 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 # Convert everything to ADLATCHs. diff --git a/tests/techmap/dfflegalize_sr_init.ys b/tests/techmap/dfflegalize_sr_init.ys index 9d724de29..7cb1c629d 100644 --- a/tests/techmap/dfflegalize_sr_init.ys +++ b/tests/techmap/dfflegalize_sr_init.ys @@ -21,18 +21,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to SRs. diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 04477eb14..b0a7d6b7e 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -17,9 +17,11 @@ EOT simplemap design -save orig +read_liberty -lib dfflibmap.lib + +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib diff --git a/tests/techmap/dffunmap.ys b/tests/techmap/dffunmap.ys index b813078ee..247699f80 100644 --- a/tests/techmap/dffunmap.ys +++ b/tests/techmap/dffunmap.ys @@ -4,7 +4,7 @@ module top(...); input C, R, E, S; input [1:0] D; -output [20:0] Q; +output [17:0] Q; $dff #(.CLK_POLARITY(1'b0), .WIDTH(2)) ff0 (.CLK(C), .D(D), .Q(Q[1:0])); $dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b0), .WIDTH(2)) ff1 (.CLK(C), .EN(E), .D(D), .Q(Q[3:2])); diff --git a/tests/techmap/pmux2mux.ys b/tests/techmap/pmux2mux.ys index 1714a6b87..1e08485ef 100644 --- a/tests/techmap/pmux2mux.ys +++ b/tests/techmap/pmux2mux.ys @@ -12,4 +12,4 @@ output [3:0] O; endmodule EOT -equiv_opt techmap -map +/pmux2mux.v +equiv_opt -assert techmap -map +/pmux2mux.v diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys index f749e79b2..680681297 100644 --- a/tests/techmap/shiftx2mux.ys +++ b/tests/techmap/shiftx2mux.ys @@ -106,4 +106,4 @@ endmodule EOT opt wreduce -equiv_opt techmap +equiv_opt -assert techmap diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys index bc07f40e6..562db0776 100644 --- a/tests/techmap/zinit.ys +++ b/tests/techmap/zinit.ys @@ -13,6 +13,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -44,6 +46,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -91,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 48 t:$_NOT_ select -assert-count 0 w:Q a:init %i @@ -138,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 0 t:$_NOT_ select -assert-count 1 w:Q a:init=24'b0 %i |