aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/clk2fflogic.cc190
-rw-r--r--passes/sat/miter.cc36
-rw-r--r--passes/sat/mutate.cc2
-rw-r--r--passes/sat/sat.cc29
-rw-r--r--passes/sat/sim.cc25
5 files changed, 156 insertions, 126 deletions
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/passes/sat/miter.cc b/passes/sat/miter.cc
index 37efadfbd..bf33c9ce3 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -31,6 +31,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_outcmp = false;
bool flag_make_assert = false;
bool flag_flatten = false;
+ bool flag_cross = false;
log_header(design, "Executing MITER pass (creating miter circuit).\n");
@@ -57,6 +58,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
flag_flatten = true;
continue;
}
+ if (args[argidx] == "-cross") {
+ flag_cross = true;
+ continue;
+ }
break;
}
if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
@@ -75,6 +80,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Module *gold_module = design->module(gold_name);
RTLIL::Module *gate_module = design->module(gate_name);
+ pool<Wire*> gold_cross_ports;
for (auto gold_wire : gold_module->wires()) {
if (gold_wire->port_id == 0)
@@ -82,12 +88,17 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
if (gate_wire == nullptr)
goto match_gold_port_error;
+ if (gold_wire->width != gate_wire->width)
+ goto match_gold_port_error;
+ if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+ gate_wire->port_input && !gate_wire->port_output) {
+ gold_cross_ports.insert(gold_wire);
+ continue;
+ }
if (gold_wire->port_input != gate_wire->port_input)
goto match_gold_port_error;
if (gold_wire->port_output != gate_wire->port_output)
goto match_gold_port_error;
- if (gold_wire->width != gate_wire->width)
- goto match_gold_port_error;
continue;
match_gold_port_error:
log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str());
@@ -99,12 +110,15 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
if (gold_wire == nullptr)
goto match_gate_port_error;
+ if (gate_wire->width != gold_wire->width)
+ goto match_gate_port_error;
+ if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+ gate_wire->port_input && !gate_wire->port_output)
+ continue;
if (gate_wire->port_input != gold_wire->port_input)
goto match_gate_port_error;
if (gate_wire->port_output != gold_wire->port_output)
goto match_gate_port_error;
- if (gate_wire->width != gold_wire->width)
- goto match_gate_port_error;
continue;
match_gate_port_error:
log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str());
@@ -123,6 +137,14 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
for (auto gold_wire : gold_module->wires())
{
+ if (gold_cross_ports.count(gold_wire))
+ {
+ RTLIL::Wire *w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
+ gold_cell->setPort(gold_wire->name, w);
+ gate_cell->setPort(gold_wire->name, w);
+ continue;
+ }
+
if (gold_wire->port_input)
{
RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
@@ -384,6 +406,12 @@ struct MiterPass : public Pass {
log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
log("\n");
+ log(" -cross\n");
+ log(" allow output ports on the gold module to match input ports on the\n");
+ log(" gate module. This is useful when the gold module contains additional\n");
+ log(" logic to drive some of the gate module inputs.\n");
+ log("\n");
+ log("\n");
log(" miter -assert [options] module [miter_name]\n");
log("\n");
log("Creates a miter circuit for property checking. All input ports are kept,\n");
diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc
index 42eb0c6d0..02174be53 100644
--- a/passes/sat/mutate.cc
+++ b/passes/sat/mutate.cc
@@ -527,6 +527,8 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
}
log("Raw database size: %d\n", GetSize(database));
+ if (N > GetSize(database))
+ log_warning("%d mutations requested but only %d could be created!\n", N, GetSize(database));
if (N != 0) {
database_reduce(database, opts, opts.none ? N-1 : N, rng);
log("Reduced database size: %d\n", GetSize(database));
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index df2725b3c..69f81e3df 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -65,11 +65,12 @@ struct SatHelper
int max_timestep, timeout;
bool gotTimeout;
- SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
+ SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
+ satgen.def_formal = set_def_formal;
set_init_def = false;
set_init_undef = false;
set_init_zero = false;
@@ -254,7 +255,13 @@ struct SatHelper
if (initstate)
{
- RTLIL::SigSpec big_lhs, big_rhs;
+ RTLIL::SigSpec big_lhs, big_rhs, forced_def;
+
+ // Check for $anyinit cells that are forced to be defined
+ if (set_init_undef && satgen.def_formal)
+ for (auto cell : module->cells())
+ if (cell->type == ID($anyinit))
+ forced_def.append(sigmap(cell->getPort(ID::Q)));
for (auto wire : module->wires())
{
@@ -323,6 +330,7 @@ struct SatHelper
if (set_init_undef) {
RTLIL::SigSpec rem = satgen.initial_state.export_all();
rem.remove(big_lhs);
+ rem.remove(forced_def);
big_lhs.append(rem);
big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
}
@@ -758,6 +766,7 @@ struct SatHelper
if (last_timestep == -2)
log(" no model variables selected for display.\n");
+ fprintf(f, "#%d\n", last_timestep+1);
fclose(f);
}
@@ -932,6 +941,9 @@ struct SatPass : public Pass {
log(" -set-def-inputs\n");
log(" add -set-def constraints for all module inputs\n");
log("\n");
+ log(" -set-def-formal\n");
+ log(" add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -1067,7 +1079,7 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false, set_def_formal = false;
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
bool show_regs = false, show_public = false, show_all = false;
@@ -1140,6 +1152,11 @@ struct SatPass : public Pass {
set_def_inputs = true;
continue;
}
+ if (args[argidx] == "-set-def-formal") {
+ enable_undef = true;
+ set_def_formal = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
@@ -1379,8 +1396,8 @@ struct SatPass : public Pass {
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
- SatHelper basecase(design, module, enable_undef);
- SatHelper inductstep(design, module, enable_undef);
+ SatHelper basecase(design, module, enable_undef, set_def_formal);
+ SatHelper inductstep(design, module, enable_undef, set_def_formal);
basecase.sets = sets;
basecase.set_assumes = set_assumes;
@@ -1569,7 +1586,7 @@ struct SatPass : public Pass {
if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
- SatHelper sathelper(design, module, enable_undef);
+ SatHelper sathelper(design, module, enable_undef, set_def_formal);
sathelper.sets = sets;
sathelper.set_assumes = set_assumes;
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index b68783f20..1cd1ebc71 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -813,18 +813,6 @@ struct SimInstance
std::string v = shared->fst->valueOf(item.second);
did_something |= set_state(item.first, Const::from_string(v));
}
- for (auto &it : ff_database)
- {
- ff_state_t &ff = it.second;
- SigSpec dsig = it.second.data.sig_d;
- Const value = get_state(dsig);
- if (dsig.is_wire()) {
- ff.past_d = value;
- if (ff.data.has_aload)
- ff.past_ad = value;
- did_something |= true;
- }
- }
for (auto cell : module->cells())
{
if (cell->is_mem_cell()) {
@@ -1019,6 +1007,16 @@ struct SimWorker : SimShared
top->update_ph3();
}
+ void initialize_stable_past()
+ {
+ if (debug)
+ log("\n-- ph1 (initialize) --\n");
+ top->update_ph1();
+ if (debug)
+ log("\n-- ph3 (initialize) --\n");
+ top->update_ph3();
+ }
+
void set_inports(pool<IdString> ports, State value)
{
for (auto portname : ports)
@@ -1191,6 +1189,7 @@ struct SimWorker : SimShared
if (initial) {
did_something |= top->setInitState();
+ initialize_stable_past();
initial = false;
}
if (did_something)
@@ -2015,7 +2014,7 @@ struct SimPass : public Pass {
log(" -r\n");
log(" read simulation results file\n");
log(" File formats supported: FST, VCD, AIW and WIT\n");
- log(" VCD support requires vcd2fst external tool to be present\n");
+ log(" VCD support requires vcd2fst external tool to be present\n");
log("\n");
log(" -map <filename>\n");
log(" read file with port and latch symbols, needed for AIGER witness input\n");
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-07 18:07:11 +0000