Merge https://github.com/cliffordwolf/yosys

backends/blif/blif.cc

@@ -77,9 +77,6 @@ struct BlifDumper
 						case State::S1:
 							init_bits[initsig[i]] = 1;
 							break;
-						case State::Sx:
-							init_bits[initsig[i]] = 2;
-							break;
 						default:
 							break;
 					}
@@ -126,7 +123,7 @@ struct BlifDumper
 		sigmap.apply(sig);
 
 		if (init_bits.count(sig) == 0)
-			return "";
+			return " 2";
 
 		string str = stringf(" %d", init_bits.at(sig));
 

backends/smt2/smtbmc.py

@@ -26,6 +26,7 @@ skip_steps = 0
 step_size = 1
 num_steps = 20
 vcdfile = None
+cexfile = None
 vlogtbfile = None
 inconstr = list()
 outconstr = None
@@ -61,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --smtc <constr_filename>
         read constraints file
 
+    --cex <cex_filename>
+        read cex file as written by ABC's "write_cex -n"
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -94,7 +98,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
 except:
     usage()
 
@@ -118,6 +122,8 @@ for o, a in opts:
         final_only = True
     elif o == "--smtc":
         inconstr.append(a)
+    elif o == "--cex":
+        cexfile = a
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -311,6 +317,37 @@ if topmod is None:
 assert topmod is not None
 assert topmod in smt.modinfo
 
+if cexfile is not None:
+    with open(cexfile, "r") as f:
+        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
+        for entry in f.read().split():
+            match = cex_regex.match(entry)
+            assert match
+
+            name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
+
+            if extra_name != "":
+                continue
+
+            if name not in smt.modinfo[topmod].inputs:
+                continue
+
+            if bit is None:
+                bit = 0
+            else:
+                bit = int(bit[1:-1])
+
+            step = int(step[1:])
+            val = int(val)
+
+            if smt.modinfo[topmod].wsize[name] == 1:
+                assert bit == 0
+                smtexpr = "(= [%s] %s)" % (name, "true" if val else "false")
+            else:
+                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val)
+
+            # print("cex@%d: %s" % (step, smtexpr))
+            constr_assumes[step].append((cexfile, smtexpr))
 
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)

passes/sat/clk2fflogic.cc

@@ -72,7 +72,47 @@ struct Clk2fflogicPass : public Pass {
 
 			for (auto cell : vector<Cell*>(module->selected_cells()))
 			{
-				if (cell->type.in("$dff", "$adff"))
+				if (cell->type.in("$dlatch"))
+				{
+					bool enpol = cell->parameters["\\EN_POLARITY"].as_bool();
+
+					SigSpec sig_en = cell->getPort("\\EN");
+					SigSpec sig_d = cell->getPort("\\D");
+					SigSpec sig_q = cell->getPort("\\Q");
+
+					log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(sig_en), log_signal(sig_d), log_signal(sig_q));
+
+					Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
+					module->addFf(NEW_ID, sig_q, past_q);
+
+					if (enpol)
+						module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q);
+					else
+						module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q);
+
+					Const initval;
+					bool assign_initval = false;
+					for (int i = 0; i < GetSize(sig_d); i++) {
+						SigBit qbit = sigmap(sig_q[i]);
+						if (initbits.count(qbit)) {
+							initval.bits.push_back(initbits.at(qbit));
+							del_initbits.insert(qbit);
+						} else
+							initval.bits.push_back(State::Sx);
+						if (initval.bits.back() != State::Sx)
+							assign_initval = true;
+					}
+
+					if (assign_initval)
+						past_q->attributes["\\init"] = initval;
+
+					module->remove(cell);
+					continue;
+				}
+
+				if (cell->type.in("$dff", "$adff", "$dffsr"))
 				{
 					bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool();
 
@@ -117,6 +157,22 @@ struct Clk2fflogicPass : public Pass {
 							module->addMux(NEW_ID, rstval, qval, arst, sig_q);
 					}
 					else
+					if (cell->type == "$dffsr")
+					{
+						SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
+						SigSpec setval = cell->getPort("\\SET");
+						SigSpec clrval = cell->getPort("\\CLR");
+
+						if (!cell->parameters["\\SET_POLARITY"].as_bool())
+							setval = module->Not(NEW_ID, setval);
+
+						if (cell->parameters["\\CLR_POLARITY"].as_bool())
+							clrval = module->Not(NEW_ID, clrval);
+
+						qval = module->Or(NEW_ID, qval, setval);
+						module->addAnd(NEW_ID, qval, clrval, sig_q);
+					}
+					else
 					{
 						module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q);
 					}

passes/sat/miter.cc

@@ -338,12 +338,12 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
 	else
 	{
 		Wire *assume_q = module->addWire(NEW_ID);
-		assume_q->attributes["\\init"] = State::S1;
+		assume_q->attributes["\\init"] = State::S0;
 		assume_signals.append(assume_q);
 
 		SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
 		SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
-		module->addFf(NEW_ID, assume_ok, assume_q);
+		module->addFf(NEW_ID, assume_nok, assume_q);
 
 		SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
 		module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);