Merge pull request #1313 from diffblue/smv-verilog-past

Instrument `$past` when generating SMV word level

Author: tautschnig

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

@@ -0,0 +1,9 @@
+CORE
+verilog5.sv
+--smv-word-level
+^INIT ebmc::\$past1@1 = FALSE$
+^TRANS next\(ebmc::\$past1@1\) = main\.in$
+^LTLSPEC G main\.in = \(X ebmc::\$past1@1\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog5.sv

@@ -0,0 +1,5 @@
+module main(input clk, input in);
+
+  p1: assert property (in iff s_nexttime $past(in));
+
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_version.h"
 #include "format_hooks.h"
 #include "instrument_buechi.h"
+#include "instrument_past.h"
 #include "liveness_to_safety.h"
 #include "netlist.h"
 #include "neural_liveness.h"
@@ -234,6 +235,8 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("smv-word-level"))
     {
+      // There is no $past in SMV.
+      instrument_past(transition_system, properties);
       auto filename = cmdline.value_opt("outfile").value_or("-");
       output_filet output_file{filename};
       output_smv_word_level(

src/temporal-logic/sva_to_ltl.cpp

@@ -272,7 +272,8 @@ exprt SVA_to_LTL(exprt expr)
   }
   else if(
     expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or ||
-    expr.id() == ID_not)
+    expr.id() == ID_not ||
+    (expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool))
   {
     for(auto &op : expr.operands())
     {

unit/Makefile

@@ -8,6 +8,7 @@ SRC += smvlang/expr2smv.cpp \
        temporal-logic/hoa.cpp \
        temporal-logic/ltl_sva_to_string.cpp \
        temporal-logic/sva_sequence_match.cpp \
+       temporal-logic/sva_to_ltl.cpp \
        temporal-logic/nnf.cpp \
        temporal-logic/trivial_sva.cpp \
        # Empty last line

unit/temporal-logic/sva_to_ltl.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: SVA to LTL
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <util/std_expr.h>
+
+#include <temporal-logic/sva_to_ltl.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("Generating LTL from SVA")
+{
+  GIVEN("A boolean formula")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+    auto q = symbol_exprt{"q", bool_typet{}};
+
+    REQUIRE(SVA_to_LTL(true_exprt{}) == true_exprt{});
+    REQUIRE(SVA_to_LTL(p) == p);
+    REQUIRE(SVA_to_LTL(equal_exprt{p, q}) == equal_exprt{p, q});
+  }
+}