Added $initstate support to smtbmc flow

backends/smt2/smt2.cc

@@ -49,6 +49,7 @@ struct Smt2Worker
 			regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0)
 	{
 		decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
+		decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", log_id(module), log_id(module)));
 
 		for (auto cell : module->cells())
 		for (auto &conn : cell->connections()) {
@@ -324,6 +325,16 @@ struct Smt2Worker
 		exported_cells.insert(cell);
 		recursive_cells.insert(cell);
 
+		if (cell->type == "$initstate")
+		{
+			SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
+					log_id(module), idcounter, log_id(module), log_id(module), log_signal(bit)));
+			register_bool(bit, idcounter++);
+			recursive_cells.erase(cell);
+			return;
+		}
+
 		if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
 		{
 			registers.insert(cell);
@@ -755,7 +766,9 @@ struct Smt2Backend : public Backend {
 		log("the assumptions in the module.\n");
 		log("\n");
 		log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
-		log("to the initial state.\n");
+		log("to the initial state. Furthermore the '<mod>_is' function should be asserted\n");
+		log("to be true for initial states in addition to '<mod>_i', and should be\n");
+		log("asserted to be false for non-initial states.\n");
 		log("\n");
 		log("For hierarchical designs, the '<mod>_h' function must be asserted for each\n");
 		log("state to establish the design hierarchy. The '<mod>_h <cellname>' function\n");

backends/smt2/smtbmc.py

@@ -130,6 +130,7 @@ if tempind:
         smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
         smt.write("(assert (%s_u s%d))" % (topmod, step))
         smt.write("(assert (%s_h s%d))" % (topmod, step))
+        smt.write("(assert (not (%s_is s%d)))" % (topmod, step))
 
         if step == num_steps:
             smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
@@ -172,9 +173,11 @@ else: # not tempind
 
         if step == 0:
             smt.write("(assert (%s_i s0))" % (topmod))
+            smt.write("(assert (%s_is s0))" % (topmod))
 
         else:
             smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+            smt.write("(assert (not (%s_is s%d)))" % (topmod, step))
 
         if step < skip_steps:
             if assume_skipped is not None and step >= assume_skipped:

examples/smtbmc/demo1.v

@@ -1,5 +1,5 @@
 module demo1(input clk, input addtwo, output iseven);
-	reg [3:0] cnt = 0;
+	reg [3:0] cnt;
 	wire [3:0] next_cnt;
 
 	inc inc_inst (addtwo, iseven, cnt, next_cnt);
@@ -8,6 +8,7 @@ module demo1(input clk, input addtwo, output iseven);
 		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
 	
 	assert property (cnt != 15);
+	initial assume (!cnt[3] && !cnt[0]);
 	// initial predict ((iseven && addtwo) || cnt == 9);
 endmodule