riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3502 from jix/equiv_opt_fixes 

equiv_opt and clk2fflogic fixes
This commit is contained in:
Jannis Harder 2022-10-11 12:02:16 +02:00 committed by GitHub
parent 5c7a1eda92 0113f44faa
commit fcf742837e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
28 changed files with 208 additions and 268 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

93
passes/equiv/equiv_make.cc
View File

@ -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();

14
passes/equiv/equiv_opt.cc
View File

@ -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");
}

192
passes/sat/clk2fflogic.cc
View File

@ -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;
else
return module->Not(NEW_ID, 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});
}
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);
// 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
sig = module->AndGate(NEW_ID, sig, past_sig);
if (polarity)
return sig;
module->addFf(NEW_ID, sig, sampled_sig);
return {sampled_sig, 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
return module->NotGate(NEW_ID, 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->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);
auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled;
if (!ff.is_fine)
module->addFf(NEW_ID, ff.sig_clk, past_clk);
else
module->addFfGate(NEW_ID, ff.sig_clk, past_clk);
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);
}
}
}

5
tests/arch/ice40/bug1597.ys
View File

@ -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

1
tests/arch/ice40/ice40_opt.ys
View File

@ -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:*

4
tests/arch/intel_alm/counter.ys
View File

@ -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

7
tests/arch/xilinx/abc9_dff.ys
View File

@ -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

1
tests/arch/xilinx/opt_lut_ins.ys
View File

@ -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

12
tests/arch/xilinx/xilinx_dffopt.ys
View File

@ -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 ;

2
tests/opt/opt_dff_en.ys
View File

@ -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;

2
tests/opt/opt_dff_mux.ys
View File

@ -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;

2
tests/opt/opt_dff_qd.ys
View File

@ -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;

25
tests/opt/opt_dff_sr.ys
View File

@ -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_

8
tests/opt/opt_expr_xor.ys
View File

@ -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

2
tests/techmap/adff2dff.ys
View File

@ -16,4 +16,4 @@ EOT
proc
equiv_opt -async2sync techmap -map +/adff2dff.v
#equiv_opt -assert -async2sync techmap -map +/adff2dff.v

2
tests/techmap/dff2ff.ys
View File

@ -13,4 +13,4 @@ EOT
proc
equiv_opt techmap -map +/dff2ff.v
equiv_opt -assert techmap -map +/dff2ff.v

2
tests/techmap/dfflegalize_adlatch.ys
View File

@ -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

2
tests/techmap/dfflegalize_adlatch_init.ys
View File

@ -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

4
tests/techmap/dfflegalize_aldff.ys
View File

@ -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.

8
tests/techmap/dfflegalize_aldff_init.ys
View File

@ -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.

24
tests/techmap/dfflegalize_dffsr_init.ys
View File

@ -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.

14
tests/techmap/dfflegalize_dlatchsr_init.ys
View File

@ -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.

24
tests/techmap/dfflegalize_sr_init.ys
View File

@ -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.

6
tests/techmap/dfflibmap.ys
View File

@ -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

2
tests/techmap/dffunmap.ys
View File

@ -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]));

2
tests/techmap/pmux2mux.ys
View File

@ -12,4 +12,4 @@ output [3:0] O;
endmodule
EOT
equiv_opt techmap -map +/pmux2mux.v
equiv_opt -assert techmap -map +/pmux2mux.v

2
tests/techmap/shiftx2mux.ys
View File

@ -106,4 +106,4 @@ endmodule
EOT
opt
wreduce
equiv_opt techmap
equiv_opt -assert techmap

14
tests/techmap/zinit.ys
View File

@ -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