SVA Monitors

This adds an alternative flow for checking SVA properties, by translating
the property into a monitor, which is added to the transition system.

Author: kroening

regression/ebmc/sva-monitor/always1.desc

@@ -0,0 +1,13 @@
+CORE
+always1.sv
+--sva-monitor --smv-word-level
+^VAR initial : boolean;$
+^VAR always_activated : boolean;$
+^INIT sva-monitor::initial$
+^INIT !sva-monitor::always_activated$
+^TRANS !next\(sva-monitor::initial\)$
+^TRANS next\(sva-monitor::always_activated\) = sva-monitor::always_active$
+^LTLSPEC G \(sva-monitor::always_active -> FALSE\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/sva-monitor/always1.sv

@@ -0,0 +1,5 @@
+module main(input clk);
+
+  p0: assert property (0);
+
+endmodule

regression/ebmc/sva-monitor/initial1.desc

@@ -0,0 +1,6 @@
+CORE
+initial1.sv
+--sva-monitor --smv-word-level
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/sva-monitor/initial1.sv

@@ -0,0 +1,5 @@
+module main(input clk);
+
+  initial p0: assert property (0);
+
+endmodule

regression/ebmc/sva-monitor/s_eventually1.desc

@@ -0,0 +1,7 @@
+CORE
+s_eventually1.sv
+--sva-monitor --smv-word-level
+^-- Verilog::main\.p0: not converted$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/sva-monitor/s_eventually1.sv

@@ -0,0 +1,5 @@
+module main(input clk);
+
+  p0: assert property (s_eventually 0);
+
+endmodule

regression/ebmc/sva-monitor/s_nexttime1.desc

@@ -0,0 +1,13 @@
+CORE
+s_nexttime1.sv
+--sva-monitor --smv-word-level
+^VAR initial : boolean;$
+^VAR delayed_active : boolean;$
+^INIT sva-monitor::initial$
+^INIT !sva-monitor::delayed_active$
+^TRANS !next\(sva-monitor::initial\)$
+^TRANS next\(sva-monitor::delayed_active\) = sva-monitor::initial$
+^LTLSPEC G \(sva-monitor::delayed_active -> FALSE\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/sva-monitor/s_nexttime1.sv

@@ -0,0 +1,5 @@
+module main(input clk);
+
+  initial p0: assert property (s_nexttime 0);
+
+endmodule

regression/ebmc/sva-monitor/sequence1.desc

@@ -0,0 +1,6 @@
+CORE
+sequence1.sv
+--sva-monitor --smv-word-level
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/sva-monitor/sequence1.sv

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always_ff @(posedge clk)
+    x++;
+
+  initial p0: assert property (x==0 ##1 x==1 ##1 x==2);
+
+endmodule

src/ebmc/Makefile

@@ -33,6 +33,7 @@ SRC = \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      sva_monitor.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line

src/ebmc/ebmc_parse_options.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include "ranking_function.h"
 #include "show_properties.h"
 #include "show_trans.h"
+#include "sva_monitor.h"
 
 #include <iostream>
 
@@ -218,6 +219,13 @@ int ebmc_parse_optionst::doit()
     auto properties = ebmc_propertiest::from_command_line(
       cmdline, transition_system, ui_message_handler);
 
+    // possibly apply liveness-to-safety
+    if(cmdline.isset("liveness-to-safety"))
+      liveness_to_safety(transition_system, properties);
+
+    if(cmdline.isset("sva-monitor"))
+      sva_monitor(transition_system, properties);
+
     if(cmdline.isset("smv-word-level"))
     {
       auto filename = cmdline.value_opt("outfile").value_or("-");
@@ -239,10 +247,6 @@ int ebmc_parse_optionst::doit()
       return 0;
     }
 
-    // possibly apply liveness-to-safety
-    if(cmdline.isset("liveness-to-safety"))
-      liveness_to_safety(transition_system, properties);
-
     if(cmdline.isset("show-varmap"))
     {
       auto netlist =
@@ -373,6 +377,7 @@ void ebmc_parse_optionst::help()
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
+    " {y--sva-monitor}               \t translate SVA properties into a monitor circuit\n"
     "\n"
     "Methods:\n"
     " {y--k-induction}               \t do k-induction with k=bound\n"

src/ebmc/ebmc_parse_options.h

@@ -49,7 +49,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(bmc-with-assumptions)"
-        "(liveness-to-safety)"
+        "(liveness-to-safety)(sva-monitor)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",
         argc,

src/ebmc/output_smv_word_level.cpp

@@ -119,7 +119,7 @@ smv_invar(const exprt &expr, const namespacet &ns, std::ostream &out)
   if(expr.id() == ID_and)
   {
     for(auto &conjunct : expr.operands())
-      smv_initial_states(conjunct, ns, out);
+      smv_invar(conjunct, ns, out);
   }
   else if(expr.is_true())
   {
@@ -146,7 +146,7 @@ static void smv_transition_relation(
   if(expr.id() == ID_and)
   {
     for(auto &conjunct : expr.operands())
-      smv_initial_states(conjunct, ns, out);
+      smv_transition_relation(conjunct, ns, out);
   }
   else if(expr.is_true())
   {