aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2023-02-14 17:15:55 +0100
committerGitHub <noreply@github.com>2023-02-14 17:15:55 +0100
commit85f611fb23ea6f10505299a2f2329e2efedd1dbc (patch)
tree23f9e752033dc542dc6583cf9e45b81028c0313d /passes
parentf37073050b5628aaf6b95f41068f84bc2fc3722e (diff)
parentfbf5d89587decd2886d501d8c6e1cde076a5476f (diff)
downloadyosys-85f611fb23ea6f10505299a2f2329e2efedd1dbc.tar.gz
yosys-85f611fb23ea6f10505299a2f2329e2efedd1dbc.tar.bz2
yosys-85f611fb23ea6f10505299a2f2329e2efedd1dbc.zip
Merge pull request #3126 from georgerennie/equiv_make_assertions
equiv_make: Add -make_assert option
Diffstat (limited to 'passes')
-rw-r--r--passes/equiv/equiv_make.cc92
1 files changed, 65 insertions, 27 deletions
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;
}