equiv_make: Add -assert option

This adds an -assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv, which
means the equivalence check can be done with SymbiYosys.

Author: georgerennie

passes/equiv/equiv_make.cc

@@ -33,6 +33,7 @@ struct EquivMakeWorker
 	bool inames;
 	vector<string> blacklists;
 	vector<string> encfiles;
+	bool emit_assertions;
 
 	pool<IdString> blacklist_names;
 	dict<IdString, dict<Const, Const>> encdata;
@@ -143,6 +144,12 @@ struct EquivMakeWorker
 		delete gate_clone;
 	}
 
+	void add_eq_assertion(IdString sig_id, 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, eq_wire, State::S1, "$equiv_make$assert:" + sig_id.str());
+	}
+
 	void find_same_wires()
 	{
 		SigMap assign_map(equiv_mod);
@@ -240,18 +247,25 @@ 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));
+				if (emit_assertions)
+					add_eq_assertion(id, gold_wire, gate_wire);
+
+				else
+				{
+					Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+					wire->port_output = true;
+
+					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);
+					rd_signal_map.add(assign_map(gold_wire), wire);
+					rd_signal_map.add(assign_map(gate_wire), wire);
+				}
 			}
 			else
 			if (gold_wire->port_input || gate_wire->port_input)
@@ -265,26 +279,31 @@ struct EquivMakeWorker
 			}
 			else
 			{
-				Wire *wire = equiv_mod->addWire(id, gold_wire->width);
-				SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+				if (emit_assertions)
+					add_eq_assertion(id, 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);
+				}
 			}
 		}
 
@@ -353,12 +372,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 (emit_assertions)
+				{
+					if (gold_sig != gate_sig)
+						add_eq_assertion(id, 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 +513,9 @@ 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("    -assert\n");
+		log("        Create $eqx and $assert cells to encode equivalence instead of $equiv.\n");
+		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 +526,7 @@ struct EquivMakePass : public Pass {
 		EquivMakeWorker worker;
 		worker.ct.setup(design);
 		worker.inames = false;
+		worker.emit_assertions = false;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -512,6 +543,10 @@ struct EquivMakePass : public Pass {
 				worker.encfiles.push_back(args[++argidx]);
 				continue;
 			}
+			if (args[argidx] == "-assert") {
+				worker.emit_assertions = true;
+				continue;
+			}
 			break;
 		}