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);