Added $initstate support to smtbmc flow

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 02d6f3fb62ac7fbd8ac15c73afcdb9844343f646..584a1df1a786ba5502f4fe07f9f82466b1bfd516 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/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");

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index f74908f8763d027daecbb88369f860a75ef39aa9..0e94a1675a9952049d53602f88e8446a5f12806b 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/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:

diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
index 2e628b7da554121b3dc5834e17aebd04ec1e4cf9..b1e505bdd6b17967b5ebdc7fa278ff88ff414335 100644 (file)
--- a/examples/smtbmc/demo1.v
+++ b/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