SVA/LTL property instrumentation

Author: kroening

Diff for: CHANGELOG

@@ -5,6 +5,7 @@
   use --bmc-with-assumptions to re-enable the previous algorithm.
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 * SystemVerilog: set membership operator
+* word-level BMC: LTL/SVA to Buechi with --buechi
 
 # EBMC 5.3
 

Diff for: lib/cbmc

@@ -0,0 +1,9 @@
+CORE
+FGp1.smv
+--buechi --bound 2
+^\[.*\] F G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/FGp1.desc

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F G p

Diff for: regression/ebmc/Buechi/FGp1.smv

@@ -0,0 +1,9 @@
+CORE
+Fp1.smv
+--buechi --bound 2
+^\[.*\] F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/Fp1.desc

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F p

Diff for: regression/ebmc/Buechi/Fp1.smv

@@ -0,0 +1,9 @@
+CORE
+GFp1.smv
+--buechi --bound 2
+^\[.*\] G F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/GFp1.desc

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := !p;
+
+-- should pass
+LTLSPEC G F p

Diff for: regression/ebmc/Buechi/GFp1.smv

@@ -0,0 +1,9 @@
+CORE
+Gp1.smv
+--buechi --bound 2
+^\[.*\] G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/Gp1.desc

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC G p

Diff for: regression/ebmc/Buechi/Gp1.smv

@@ -0,0 +1,9 @@
+CORE
+Xp1.smv
+--buechi --bound 2
+^\[.*\] X p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/Xp1.desc

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC X p

Diff for: regression/ebmc/Buechi/Xp1.smv

@@ -0,0 +1,9 @@
+CORE
+and1.smv
+--buechi --bound 2
+^\[.*\] X p & X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/and1.desc

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X p & X q
+

Diff for: regression/ebmc/Buechi/and1.smv

@@ -0,0 +1,9 @@
+CORE
+and2.smv
+--buechi --bound 2
+^\[.*\] X \(p & q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/and2.desc

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X (p & q)
+

Diff for: regression/ebmc/Buechi/and2.smv

@@ -0,0 +1,9 @@
+CORE
+iff1.smv
+--buechi --bound 2
+^\[.*\] X p <-> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/iff1.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p <-> X q

Diff for: regression/ebmc/Buechi/iff1.smv

@@ -0,0 +1,9 @@
+CORE
+iff2.smv
+--buechi --bound 2
+^\[.*\] X \(p <-> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/iff2.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p <-> q)

Diff for: regression/ebmc/Buechi/iff2.smv

@@ -0,0 +1,9 @@
+CORE
+implies1.smv
+--buechi --bound 2
+^\[.*\] X p -> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/implies1.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p -> X q

Diff for: regression/ebmc/Buechi/implies1.smv

@@ -0,0 +1,9 @@
+CORE
+implies2.smv
+--buechi --bound 2
+^\[.*\] X \(p -> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/implies2.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p -> q)

Diff for: regression/ebmc/Buechi/implies2.smv

@@ -0,0 +1,9 @@
+CORE
+or1.smv
+--buechi --bound 2
+^\[.*\] X p \| X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/or1.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p | X q

Diff for: regression/ebmc/Buechi/or1.smv

@@ -0,0 +1,9 @@
+CORE
+or2.smv
+--buechi --bound 2
+^\[.*\] X \(p \| q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/ebmc/Buechi/or2.desc

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p | q)

Diff for: regression/ebmc/Buechi/or2.smv

@@ -15,6 +15,7 @@ SRC = \
       ebmc_parse_options.cpp \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
+      instrument_buechi.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
       live_signal.cpp \

Diff for: src/ebmc/Makefile

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_error.h"
 #include "ebmc_version.h"
 #include "ic3_engine.h"
+#include "instrument_buechi.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
 #include "property_checker.h"
@@ -241,7 +242,14 @@ int ebmc_parse_optionst::doit()
       if(result != -1)
         return result;
 
-      // possibly apply liveness-to-safety
+      // LTL/SVA to Buechi?
+      if(cmdline.isset("buechi"))
+        instrument_buechi(
+          ebmc_base.transition_system,
+          ebmc_base.properties,
+          ui_message_handler);
+
+      // Liveness to safety?
       if(cmdline.isset("liveness-to-safety"))
         liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
 
@@ -366,6 +374,7 @@ void ebmc_parse_optionst::help()
     " {y--systemverilog}             \t force SystemVerilog instead of Verilog\n"
     " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
+    " {y--buechi}                    \t translate LTL/SVA properties to Buechi acceptance\n"
     "\n"
     "Methods:\n"
     " {y--k-induction}               \t do k-induction with k=bound\n"

Diff for: src/ebmc/ebmc_parse_options.cpp

@@ -48,7 +48,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)(buechi)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",
         argc,