Merge pull request #1089 from diffblue/smv-word-level-SVA

SMV word-level output now converts SVA

Author: tautschnig

regression/ebmc/smv-word-level/verilog1.desc

@@ -1,11 +1,12 @@
 CORE
-verilog1.v
+verilog1.sv
 --smv-word-level
 ^MODULE main$
 ^VAR x : unsigned word\[32\];$
 ^INIT main\.x = 0ud32_0$
 ^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
 ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
+^LTLSPEC F main\.x = 0sd32_10$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-word-level/verilog1.v …gression/ebmc/smv-word-level/verilog1.svregression/ebmc/smv-word-level/verilog1.v renamed to regression/ebmc/smv-word-level/verilog1.sv regression/ebmc/smv-word-level/verilog1.v renamed to regression/ebmc/smv-word-level/verilog1.sv

@@ -7,4 +7,6 @@ module main(input clk);
   always @(posedge clk)
     x = x + 1;
 
+  initial assert property (s_eventually x == 10);
+
 endmodule

src/ebmc/output_smv_word_level.cpp

@@ -186,6 +186,15 @@ static void smv_properties(
     {
       out << "LTLSPEC " << expr2smv(property.normalized_expr, ns);
     }
+    else if(is_SVA(property.normalized_expr))
+    {
+      // we can turn some SVA properties into LTL
+      auto ltl_opt = SVA_to_LTL(property.normalized_expr);
+      if(ltl_opt.has_value())
+        out << "LTLSPEC " << expr2smv(ltl_opt.value(), ns);
+      else
+        out << "-- " << property.identifier << ": SVA not converted\n";
+    }
     else
       out << "-- " << property.identifier << ": not converted\n";