From 17fdbb01fa74b6854e504b8885991a7d18448f74 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 2 May 2025 14:26:38 -0700 Subject: [PATCH] BDD engine: transform SVA to LTL, then LTL to CTL The BDD engine now transforms SVA to LTL, when possible, which in turn is transformed to CTL, when possible. This is strictly more general than the current direct mapping. --- regression/verilog/SVA/followed-by1.bdd.desc | 10 ++ ...ollowed-by1.desc => followed-by1.bmc.desc} | 0 regression/verilog/SVA/followed-by2.bdd.desc | 10 ++ ...ollowed-by2.desc => followed-by2.bmc.desc} | 0 regression/verilog/SVA/followed-by4.bdd.desc | 11 +++ ...ollowed-by4.desc => followed-by4.bmc.desc} | 0 regression/verilog/SVA/initial1.bdd.desc | 14 +++ .../SVA/{initial1.desc => initial1.bmc.desc} | 0 regression/verilog/SVA/nexttime1.bdd.desc | 11 +++ .../{nexttime1.desc => nexttime1.bmc.desc} | 0 regression/verilog/SVA/restrict1.bdd.desc | 10 ++ .../{restrict1.desc => restrict1.bmc.desc} | 0 regression/verilog/SVA/s_eventually1.bdd.desc | 8 ++ ...ventually1.desc => s_eventually1.bmc.desc} | 0 regression/verilog/SVA/sequence4.bdd.desc | 8 ++ .../{sequence4.desc => sequence4.bmc.desc} | 0 regression/verilog/SVA/sequence_and1.bdd.desc | 13 +++ ...uence_and1.desc => sequence_and1.bmc.desc} | 0 .../verilog/SVA/sequence_repetition1.sv | 4 +- .../verilog/SVA/sequence_repetition2.sv | 4 +- .../verilog/SVA/sequence_repetition3.sv | 4 +- .../verilog/system-functions/past1.bdd.desc | 3 +- regression/verilog/system-functions/past1.sv | 2 +- src/ebmc/bdd_engine.cpp | 92 ++++++------------- 24 files changed, 129 insertions(+), 75 deletions(-) create mode 100644 regression/verilog/SVA/followed-by1.bdd.desc rename regression/verilog/SVA/{followed-by1.desc => followed-by1.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/followed-by2.bdd.desc rename regression/verilog/SVA/{followed-by2.desc => followed-by2.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/followed-by4.bdd.desc rename regression/verilog/SVA/{followed-by4.desc => followed-by4.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/initial1.bdd.desc rename regression/verilog/SVA/{initial1.desc => initial1.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/nexttime1.bdd.desc rename regression/verilog/SVA/{nexttime1.desc => nexttime1.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/restrict1.bdd.desc rename regression/verilog/SVA/{restrict1.desc => restrict1.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/s_eventually1.bdd.desc rename regression/verilog/SVA/{s_eventually1.desc => s_eventually1.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/sequence4.bdd.desc rename regression/verilog/SVA/{sequence4.desc => sequence4.bmc.desc} (100%) create mode 100644 regression/verilog/SVA/sequence_and1.bdd.desc rename regression/verilog/SVA/{sequence_and1.desc => sequence_and1.bmc.desc} (100%) diff --git a/regression/verilog/SVA/followed-by1.bdd.desc b/regression/verilog/SVA/followed-by1.bdd.desc new file mode 100644 index 000000000..4f0cd64bd --- /dev/null +++ b/regression/verilog/SVA/followed-by1.bdd.desc @@ -0,0 +1,10 @@ +CORE +followed-by1.sv +--bdd +^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED$ +^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/followed-by1.desc b/regression/verilog/SVA/followed-by1.bmc.desc similarity index 100% rename from regression/verilog/SVA/followed-by1.desc rename to regression/verilog/SVA/followed-by1.bmc.desc diff --git a/regression/verilog/SVA/followed-by2.bdd.desc b/regression/verilog/SVA/followed-by2.bdd.desc new file mode 100644 index 000000000..7184dbb69 --- /dev/null +++ b/regression/verilog/SVA/followed-by2.bdd.desc @@ -0,0 +1,10 @@ +CORE +followed-by2.sv +--bdd +^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED$ +^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): FAILURE: property not supported by BDD engine$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/followed-by2.desc b/regression/verilog/SVA/followed-by2.bmc.desc similarity index 100% rename from regression/verilog/SVA/followed-by2.desc rename to regression/verilog/SVA/followed-by2.bmc.desc diff --git a/regression/verilog/SVA/followed-by4.bdd.desc b/regression/verilog/SVA/followed-by4.bdd.desc new file mode 100644 index 000000000..028efaeaf --- /dev/null +++ b/regression/verilog/SVA/followed-by4.bdd.desc @@ -0,0 +1,11 @@ +CORE +followed-by4.sv +--bdd +^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$ +^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: FAILURE: property not supported by BDD engine$ +^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: FAILURE: property not supported by BDD engine$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/followed-by4.desc b/regression/verilog/SVA/followed-by4.bmc.desc similarity index 100% rename from regression/verilog/SVA/followed-by4.desc rename to regression/verilog/SVA/followed-by4.bmc.desc diff --git a/regression/verilog/SVA/initial1.bdd.desc b/regression/verilog/SVA/initial1.bdd.desc new file mode 100644 index 000000000..85b8b1cfe --- /dev/null +++ b/regression/verilog/SVA/initial1.bdd.desc @@ -0,0 +1,14 @@ +CORE +initial1.sv +--bdd +^\[main\.p0\] main\.counter == 0: PROVED$ +^\[main\.p1\] main\.counter == 100: REFUTED$ +^\[main\.p2\] ##1 main\.counter == 1: PROVED$ +^\[main\.p3\] ##1 main\.counter == 100: REFUTED$ +^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$ +^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/initial1.desc b/regression/verilog/SVA/initial1.bmc.desc similarity index 100% rename from regression/verilog/SVA/initial1.desc rename to regression/verilog/SVA/initial1.bmc.desc diff --git a/regression/verilog/SVA/nexttime1.bdd.desc b/regression/verilog/SVA/nexttime1.bdd.desc new file mode 100644 index 000000000..5cd127650 --- /dev/null +++ b/regression/verilog/SVA/nexttime1.bdd.desc @@ -0,0 +1,11 @@ +CORE +nexttime1.sv +--bdd +^\[main\.p1\] s_nexttime\[0\] main\.counter == 0: PROVED$ +^\[main\.p2\] s_nexttime\[1\] main\.counter == 1: PROVED$ +^\[main\.p3\] nexttime\[8\] main\.counter == 8: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/nexttime1.desc b/regression/verilog/SVA/nexttime1.bmc.desc similarity index 100% rename from regression/verilog/SVA/nexttime1.desc rename to regression/verilog/SVA/nexttime1.bmc.desc diff --git a/regression/verilog/SVA/restrict1.bdd.desc b/regression/verilog/SVA/restrict1.bdd.desc new file mode 100644 index 000000000..571ee2b74 --- /dev/null +++ b/regression/verilog/SVA/restrict1.bdd.desc @@ -0,0 +1,10 @@ +CORE +restrict1.sv +--bdd +^\[main\.p0\] always main\.x != 5: ASSUMED$ +^\[main\.p1\] always main\.x != 6: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/restrict1.desc b/regression/verilog/SVA/restrict1.bmc.desc similarity index 100% rename from regression/verilog/SVA/restrict1.desc rename to regression/verilog/SVA/restrict1.bmc.desc diff --git a/regression/verilog/SVA/s_eventually1.bdd.desc b/regression/verilog/SVA/s_eventually1.bdd.desc new file mode 100644 index 000000000..15ae3a152 --- /dev/null +++ b/regression/verilog/SVA/s_eventually1.bdd.desc @@ -0,0 +1,8 @@ +CORE +s_eventually1.sv +--bdd +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/s_eventually1.desc b/regression/verilog/SVA/s_eventually1.bmc.desc similarity index 100% rename from regression/verilog/SVA/s_eventually1.desc rename to regression/verilog/SVA/s_eventually1.bmc.desc diff --git a/regression/verilog/SVA/sequence4.bdd.desc b/regression/verilog/SVA/sequence4.bdd.desc new file mode 100644 index 000000000..186f02085 --- /dev/null +++ b/regression/verilog/SVA/sequence4.bdd.desc @@ -0,0 +1,8 @@ +CORE +sequence4.sv +--bdd +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sequence4.desc b/regression/verilog/SVA/sequence4.bmc.desc similarity index 100% rename from regression/verilog/SVA/sequence4.desc rename to regression/verilog/SVA/sequence4.bmc.desc diff --git a/regression/verilog/SVA/sequence_and1.bdd.desc b/regression/verilog/SVA/sequence_and1.bdd.desc new file mode 100644 index 000000000..98b9bd1fc --- /dev/null +++ b/regression/verilog/SVA/sequence_and1.bdd.desc @@ -0,0 +1,13 @@ +CORE +sequence_and1.sv +--bdd +^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$ +^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$ +^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$ +^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$ +^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sequence_and1.desc b/regression/verilog/SVA/sequence_and1.bmc.desc similarity index 100% rename from regression/verilog/SVA/sequence_and1.desc rename to regression/verilog/SVA/sequence_and1.bmc.desc diff --git a/regression/verilog/SVA/sequence_repetition1.sv b/regression/verilog/SVA/sequence_repetition1.sv index 80456c394..7973497c5 100644 --- a/regression/verilog/SVA/sequence_repetition1.sv +++ b/regression/verilog/SVA/sequence_repetition1.sv @@ -1,13 +1,13 @@ module main(input clk); - reg [31:0] x = 0; + reg [7:0] x = 0; // 0 1 2 3 4 ... always_ff @(posedge clk) x<=x+1; // 0 0 1 1 2 2 3 3 ... - wire [31:0] half_x = x/2; + wire [7:0] half_x = x/2; // should pass initial p0: assert property (half_x==0[*2]); diff --git a/regression/verilog/SVA/sequence_repetition2.sv b/regression/verilog/SVA/sequence_repetition2.sv index d46b95147..52ad1afe1 100644 --- a/regression/verilog/SVA/sequence_repetition2.sv +++ b/regression/verilog/SVA/sequence_repetition2.sv @@ -1,13 +1,13 @@ module main(input clk); - reg [31:0] x = 0; + reg [7:0] x = 0; // 0 1 2 3 4 ... always_ff @(posedge clk) x<=x+1; // 0 0 1 1 2 2 3 3 ... - wire [31:0] half_x = x/2; + wire [7:0] half_x = x/2; // should pass initial p0: assert property (x==0[*]); diff --git a/regression/verilog/SVA/sequence_repetition3.sv b/regression/verilog/SVA/sequence_repetition3.sv index e7a7b2f4a..e0ab91765 100644 --- a/regression/verilog/SVA/sequence_repetition3.sv +++ b/regression/verilog/SVA/sequence_repetition3.sv @@ -1,13 +1,13 @@ module main(input clk); - reg [31:0] x = 0; + reg [7:0] x = 0; // 0 1 2 3 4 ... always_ff @(posedge clk) x<=x+1; // 0 0 1 1 2 2 3 3 ... - wire [31:0] half_x = x/2; + wire [7:0] half_x = x/2; // should pass initial p0: assert property (x==0[*1] #=# x==1[*1]); diff --git a/regression/verilog/system-functions/past1.bdd.desc b/regression/verilog/system-functions/past1.bdd.desc index 6260e4935..622402c7c 100644 --- a/regression/verilog/system-functions/past1.bdd.desc +++ b/regression/verilog/system-functions/past1.bdd.desc @@ -1,7 +1,6 @@ CORE past1.sv --bdd -^\[main\.p0\] ##0 \$past\(main\.counter, 0\) == 0: FAILURE: property not supported by BDD engine$ -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/past1.sv b/regression/verilog/system-functions/past1.sv index b11902469..f2d02e140 100644 --- a/regression/verilog/system-functions/past1.sv +++ b/regression/verilog/system-functions/past1.sv @@ -1,6 +1,6 @@ module main(input clk); - reg [31:0] counter = 0; + reg [7:0] counter = 0; always @(posedge clk) counter++; diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index 9de9b961e..2fb032c40 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch #include #include #include -#include #include "netlist.h" @@ -66,7 +65,7 @@ class bdd_enginet const namespacet ns; netlistt netlist; - static bool property_supported(const exprt &); + static std::optional property_supported(const exprt &); // the Manager must appear before any BDDs // to do the cleanup in the right order @@ -199,9 +198,20 @@ property_checker_resultt bdd_enginet::operator()() << ", nodes: " << netlist.number_of_nodes() << messaget::eom; - for(const auto &property : properties.properties) - if(property_supported(property.normalized_expr)) - get_atomic_propositions(property.normalized_expr); + for(auto &property : properties.properties) + { + if(!property.is_disabled() && !property.is_assumed()) + { + auto converted_opt = property_supported(property.normalized_expr); + if(converted_opt.has_value()) + { + property.normalized_expr = *converted_opt; + get_atomic_propositions(*converted_opt); + } + else + property.failure("property not supported by BDD engine"); + } + } message.status() << "Building BDD for netlist" << messaget::eom; @@ -449,40 +459,29 @@ Function: bdd_enginet::property_supported \*******************************************************************/ -bool bdd_enginet::property_supported(const exprt &expr) +std::optional bdd_enginet::property_supported(const exprt &expr) { // Our engine knows all of CTL. if(is_CTL(expr)) - return true; + return expr; if(is_LTL(expr)) { // We can map selected path properties to CTL. - return LTL_to_CTL(expr).has_value(); + return LTL_to_CTL(expr); } if(is_SVA(expr)) { - if( - expr.id() == ID_sva_always && - !has_temporal_operator(to_sva_always_expr(expr).op())) - { - // always p - return true; - } - - if( - expr.id() == ID_sva_always && - to_sva_always_expr(expr).op().id() == ID_sva_s_eventually && - !has_temporal_operator( - to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op())) - { - // always s_eventually p - return true; - } + // We can map some SVA to LTL. In turn, some of that can be mapped to CTL. + auto ltl_opt = SVA_to_LTL(expr); + if(ltl_opt.has_value()) + return property_supported(ltl_opt.value()); + else + return {}; } - return false; + return {}; } /*******************************************************************\ @@ -505,51 +504,12 @@ void bdd_enginet::check_property(propertyt &property) if(property.is_assumed()) return; - if(!property_supported(property.normalized_expr)) - { - property.failure("property not supported by BDD engine"); + if(property.is_failure()) return; - } message.status() << "Checking " << property.name << messaget::eom; property.status=propertyt::statust::UNKNOWN; - if( - property.normalized_expr.id() == ID_sva_always && - to_sva_always_expr(property.normalized_expr).op().id() == - ID_sva_s_eventually && - !has_temporal_operator(to_sva_s_eventually_expr( - to_sva_always_expr(property.normalized_expr).op()) - .op())) - { - // always s_eventually p --> AG AF p - auto p = to_sva_s_eventually_expr( - to_sva_always_expr(property.normalized_expr).op()) - .op(); - property.normalized_expr = AG_exprt{AF_exprt{p}}; - } - - if( - property.normalized_expr.id() == ID_sva_always && - !has_temporal_operator(to_sva_always_expr(property.normalized_expr).op())) - { - // always p --> AG p - auto p = to_sva_always_expr(property.normalized_expr).op(); - property.normalized_expr = AG_exprt{p}; - } - - // Our engine knows CTL only. - // We map selected path properties to CTL. - if( - has_temporal_operator(property.normalized_expr) && - is_LTL(property.normalized_expr)) - { - auto CTL_opt = LTL_to_CTL(property.normalized_expr); - CHECK_RETURN(CTL_opt.has_value()); - property.normalized_expr = CTL_opt.value(); - CHECK_RETURN(is_CTL(property.normalized_expr)); - } - if(is_AGp(property.normalized_expr)) { check_AGp(property);