aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/chformal.cc19
-rw-r--r--passes/equiv/equiv_make.cc92
2 files changed, 84 insertions, 27 deletions
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc
index 66044b161..da97ff71d 100644
--- a/passes/cmds/chformal.cc
+++ b/passes/cmds/chformal.cc
@@ -55,6 +55,14 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n");
+ log(" -coverenable\n");
+ log(" add cover statements for the enable signals of the constraints\n");
+ log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+ log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
+ log(" reachable SVA statement corresponds to an active enable signal.\n");
+ log("\n");
+#endif
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");
@@ -114,6 +122,10 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str());
continue;
}
+ if (mode == 0 && args[argidx] == "-coverenable") {
+ mode = 'p';
+ continue;
+ }
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true;
mode = 'c';
@@ -263,6 +275,13 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
}
else
+ if (mode =='p')
+ {
+ for (auto cell : constr_cells)
+ module->addCover(NEW_ID_SUFFIX("coverenable"),
+ cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
+ }
+ else
if (mode == 'c')
{
for (auto cell : constr_cells)
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 27cec7549..e15e510be 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -33,6 +33,7 @@ struct EquivMakeWorker
bool inames;
vector<string> blacklists;
vector<string> encfiles;
+ bool make_assert;
pool<IdString> blacklist_names;
dict<IdString, dict<Const, Const>> encdata;
@@ -133,6 +134,12 @@ struct EquivMakeWorker
delete gate_clone;
}
+ void add_eq_assertion(const SigSpec &gold_sig, const SigSpec &gate_sig)
+ {
+ auto eq_wire = equiv_mod->Eqx(NEW_ID, gold_sig, gate_sig);
+ equiv_mod->addAssert(NEW_ID_SUFFIX("assert"), eq_wire, State::S1);
+ }
+
void find_same_wires()
{
SigMap assign_map(equiv_mod);
@@ -231,15 +238,24 @@ struct EquivMakeWorker
if (gold_wire->port_output || gate_wire->port_output)
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- wire->port_output = true;
gold_wire->port_input = false;
gate_wire->port_input = false;
gold_wire->port_output = false;
gate_wire->port_output = false;
- for (int i = 0; i < wire->width; i++)
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ wire->port_output = true;
+
+ if (make_assert)
+ {
+ add_eq_assertion(gold_wire, gate_wire);
+ equiv_mod->connect(wire, gold_wire);
+ }
+ else
+ {
+ for (int i = 0; i < wire->width; i++)
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ }
rd_signal_map.add(assign_map(gold_wire), wire);
rd_signal_map.add(assign_map(gate_wire), wire);
@@ -259,26 +275,31 @@ struct EquivMakeWorker
}
else
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+ if (make_assert)
+ add_eq_assertion(gold_wire, gate_wire);
- for (int i = 0; i < wire->width; i++) {
- if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
- continue;
- }
- if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
- continue;
+ else {
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+
+ for (int i = 0; i < wire->width; i++) {
+ if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
+ continue;
+ }
+ if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
+ continue;
+ }
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ rdmap_gold.append(SigBit(gold_wire, i));
+ rdmap_gate.append(SigBit(gate_wire, i));
+ rdmap_equiv.append(SigBit(wire, i));
}
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
- rdmap_gold.append(SigBit(gold_wire, i));
- rdmap_gate.append(SigBit(gate_wire, i));
- rdmap_equiv.append(SigBit(wire, i));
- }
- rd_signal_map.add(rdmap_gold, rdmap_equiv);
- rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ rd_signal_map.add(rdmap_gold, rdmap_equiv);
+ rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ }
}
}
@@ -335,12 +356,20 @@ struct EquivMakeWorker
continue;
}
- for (int i = 0; i < GetSize(gold_sig); i++)
- if (gold_sig[i] != gate_sig[i]) {
- Wire *w = equiv_mod->addWire(NEW_ID);
- equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
- gold_sig[i] = w;
- }
+ if (make_assert)
+ {
+ if (gold_sig != gate_sig)
+ add_eq_assertion(gold_sig, gate_sig);
+ }
+ else
+ {
+ for (int i = 0; i < GetSize(gold_sig); i++)
+ if (gold_sig[i] != gate_sig[i]) {
+ Wire *w = equiv_mod->addWire(NEW_ID);
+ equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
+ gold_sig[i] = w;
+ }
+ }
gold_cell->setPort(gold_conn.first, gold_sig);
}
@@ -417,6 +446,10 @@ struct EquivMakePass : public Pass {
log(" Match FSM encodings using the description from the file.\n");
log(" See 'help fsm_recode' for details.\n");
log("\n");
+ log(" -make_assert\n");
+ log(" Check equivalence with $assert cells instead of $equiv.\n");
+ log(" $eqx (===) is used to compare signals.");
+ log("\n");
log("Note: The circuit created by this command is not a miter (with something like\n");
log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
@@ -427,6 +460,7 @@ struct EquivMakePass : public Pass {
EquivMakeWorker worker;
worker.ct.setup(design);
worker.inames = false;
+ worker.make_assert = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -443,6 +477,10 @@ struct EquivMakePass : public Pass {
worker.encfiles.push_back(args[++argidx]);
continue;
}
+ if (args[argidx] == "-make_assert") {
+ worker.make_assert = true;
+ continue;
+ }
break;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-03 16:49:04 +0000