SVA/LTL property instrumentation

kroening · kroening · commit 9525b7bd48c0 · 2024-11-07T17:31:38.000-05:00
diff --git a/CHANGELOG b/CHANGELOG
@@ -1,3 +1,7 @@
+# EBMC 5.4
+
+* word-level BMC: LTL/SVA to Buechi with --buechi
+
 # EBMC 5.3
 
 * SystemVerilog: fix for nets implicitly declared for port connections
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/bmc.cpp b/src/ebmc/bmc.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "bmc.h"
 
 #include <solvers/prop/literal_expr.h>
+#include <temporal-logic/ltl_to_buechi.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
@@ -20,6 +21,7 @@ Author: Daniel Kroening, dkr@amazon.com
 void bmc(
   std::size_t bound,
   bool convert_only,
+  bool buechi,
   const transition_systemt &transition_system,
   ebmc_propertiest &properties,
   const ebmc_solver_factoryt &solver_factory,
@@ -46,6 +48,12 @@ void bmc(
     if(property.is_disabled() || property.is_failure())
       continue;
 
+    // LTL/SVA to Buechi?
+    if(buechi)
+    {
+      auto buechi = ltl_to_buechi(property.normalized_expr);
+    }
+
     // Is it supported by the BMC engine?
     if(!bmc_supports_property(property.normalized_expr))
     {
diff --git a/src/ebmc/bmc.h b/src/ebmc/bmc.h
@@ -22,6 +22,7 @@ class transition_systemt;
 void bmc(
   std::size_t bound,
   bool convert_only,
+  bool buechi,
   const transition_systemt &,
   ebmc_propertiest &,
   const ebmc_solver_factoryt &,
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -241,7 +241,6 @@ int ebmc_parse_optionst::doit()
       if(result != -1)
         return result;
 
-      // possibly apply liveness-to-safety
       if(cmdline.isset("liveness-to-safety"))
         liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
 
@@ -366,6 +365,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
@@ -46,7 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
-        "(liveness-to-safety)"
+        "(liveness-to-safety)(buechi)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",
         argc,
diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
@@ -202,7 +202,8 @@ void k_inductiont::induction_base()
 
   bmc(
     k,
-    false,
+    false, // convert_only
+    false, // buechi
     transition_system,
     properties,
     solver_factory,
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
@@ -83,6 +83,7 @@ property_checker_resultt word_level_bmc(
       bmc(
         bound,
         convert_only,
+        cmdline.isset("buechi"),
         transition_system,
         properties,
         solver_factory,
diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile
@@ -1,4 +1,5 @@
-SRC = nnf.cpp \
+SRC = ltl_to_buechi.cpp \
+      nnf.cpp \
       normalize_property.cpp \
       temporal_logic.cpp \
       trivial_sva.cpp \
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
