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

equiv_make: Add -make_assert option 

This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv.
This commit is contained in:
George Rennie 2021-12-23 01:10:32 +00:00
parent 34804f3fb6
commit fbf5d89587
2 changed files with 97 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

92
passes/equiv/equiv_make.cc
View File

@ -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;
@ -143,6 +144,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);
@ -240,15 +247,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);
@ -265,26 +281,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;
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));
}
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));
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);
}
}
@ -353,12 +374,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);
}
@ -486,6 +515,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");
@ -496,6 +529,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++)
@ -512,6 +546,10 @@ struct EquivMakePass : public Pass {
worker.encfiles.push_back(args[++argidx]);
continue;
}
if (args[argidx] == "-make_assert") {
worker.make_assert = true;
continue;
}
break;
}

32
tests/various/equiv_make_make_assert.ys Normal file
View File

@ -0,0 +1,32 @@
read_verilog <<EOT
module gold(
input wire [7:0] a,
input wire [7:0] b,
output wire [7:0] c
);
wire [7:0] b_neg;
assign b_neg = -b;
assign c = a + b_neg;
endmodule
module gate(
input wire [7:0] a,
input wire [7:0] b,
output wire [7:0] c
);
wire [7:0] b_neg;
assign b_neg = ~b + 1;
assign c = a + b_neg;
endmodule
EOT
equiv_make -make_assert gold gate miter
select -assert-count 0 t:$equiv
select -assert-count 2 t:$assert
prep -top miter
sat -prove-asserts -verify