SVA/LTL property instrumentation

kroening · kroening · commit dfbcbbe3c7c6 · 2024-11-27T14:04:47.000Z
diff --git a/CHANGELOG b/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 --git a/lib/cbmc b/lib/cbmc
@@ -1 +1 @@
-Subproject commit beebdda9e501efd7605ec33045d1e0979463bdb7
+Subproject commit ee8d275038e4f717df5b737a6958741265e4fe07
diff --git a/regression/ebmc/Buechi/FGp1.desc b/regression/ebmc/Buechi/FGp1.desc
@@ -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 --git a/regression/ebmc/Buechi/FGp1.smv b/regression/ebmc/Buechi/FGp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F G p
diff --git a/regression/ebmc/Buechi/Fp1.desc b/regression/ebmc/Buechi/Fp1.desc
@@ -0,0 +1,9 @@
+CORE
+Fp1.smv
+--buechi --bound 2
+^\[.*\] F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Fp1.smv b/regression/ebmc/Buechi/Fp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F p
diff --git a/regression/ebmc/Buechi/GFp1.desc b/regression/ebmc/Buechi/GFp1.desc
@@ -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 --git a/regression/ebmc/Buechi/GFp1.smv b/regression/ebmc/Buechi/GFp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := !p;
+
+-- should pass
+LTLSPEC G F p
diff --git a/regression/ebmc/Buechi/Gp1.desc b/regression/ebmc/Buechi/Gp1.desc
@@ -0,0 +1,9 @@
+CORE
+Gp1.smv
+--buechi --bound 2
+^\[.*\] G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Gp1.smv b/regression/ebmc/Buechi/Gp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC G p
diff --git a/regression/ebmc/Buechi/Xp1.desc b/regression/ebmc/Buechi/Xp1.desc
@@ -0,0 +1,9 @@
+CORE
+Xp1.smv
+--buechi --bound 2
+^\[.*\] X p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Xp1.smv b/regression/ebmc/Buechi/Xp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC X p
diff --git a/regression/ebmc/Buechi/and1.desc b/regression/ebmc/Buechi/and1.desc
@@ -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 --git a/regression/ebmc/Buechi/and1.smv b/regression/ebmc/Buechi/and1.smv
@@ -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 --git a/regression/ebmc/Buechi/and2.desc b/regression/ebmc/Buechi/and2.desc
@@ -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 --git a/regression/ebmc/Buechi/and2.smv b/regression/ebmc/Buechi/and2.smv
@@ -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 --git a/regression/ebmc/Buechi/iff1.desc b/regression/ebmc/Buechi/iff1.desc
@@ -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 --git a/regression/ebmc/Buechi/iff1.smv b/regression/ebmc/Buechi/iff1.smv
@@ -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 --git a/regression/ebmc/Buechi/iff2.desc b/regression/ebmc/Buechi/iff2.desc
@@ -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 --git a/regression/ebmc/Buechi/iff2.smv b/regression/ebmc/Buechi/iff2.smv
@@ -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 --git a/regression/ebmc/Buechi/implies1.desc b/regression/ebmc/Buechi/implies1.desc
@@ -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 --git a/regression/ebmc/Buechi/implies1.smv b/regression/ebmc/Buechi/implies1.smv
@@ -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 --git a/regression/ebmc/Buechi/implies2.desc b/regression/ebmc/Buechi/implies2.desc
@@ -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 --git a/regression/ebmc/Buechi/implies2.smv b/regression/ebmc/Buechi/implies2.smv
@@ -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 --git a/regression/ebmc/Buechi/or1.desc b/regression/ebmc/Buechi/or1.desc
@@ -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 --git a/regression/ebmc/Buechi/or1.smv b/regression/ebmc/Buechi/or1.smv
@@ -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 --git a/regression/ebmc/Buechi/or2.desc b/regression/ebmc/Buechi/or2.desc
@@ -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 --git a/regression/ebmc/Buechi/or2.smv b/regression/ebmc/Buechi/or2.smv
@@ -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 --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -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 --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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 --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
@@ -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,
diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp
diff --git a/src/ebmc/instrument_buechi.h b/src/ebmc/instrument_buechi.h
diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile
diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp
diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h
diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp
diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h
diff --git a/unit/Makefile b/unit/Makefile
diff --git a/unit/temporal-logic/ltl_sva_to_string.cpp b/unit/temporal-logic/ltl_sva_to_string.cpp
