From ec7e96accaa29c9f917603a80e50d7b637da30ea Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 15 Apr 2025 06:12:08 -0700 Subject: [PATCH] SVA to LTL now converts SVA sequences This adds support for mapping some SVA sequences to equivalent LTL. --- regression/ebmc/smv-netlist/cycle_delay1.desc | 7 + regression/ebmc/smv-netlist/cycle_delay1.sv | 10 + regression/ebmc/smv-netlist/cycle_delay2.desc | 7 + regression/ebmc/smv-netlist/cycle_delay2.sv | 10 + regression/verilog/SVA/cycle_delay2.desc | 7 + regression/verilog/SVA/cycle_delay2.sv | 10 + src/temporal-logic/temporal_logic.cpp | 209 ++++++++++++++++-- src/verilog/sva_expr.h | 34 +++ 8 files changed, 280 insertions(+), 14 deletions(-) create mode 100644 regression/ebmc/smv-netlist/cycle_delay1.desc create mode 100644 regression/ebmc/smv-netlist/cycle_delay1.sv create mode 100644 regression/ebmc/smv-netlist/cycle_delay2.desc create mode 100644 regression/ebmc/smv-netlist/cycle_delay2.sv create mode 100644 regression/verilog/SVA/cycle_delay2.desc create mode 100644 regression/verilog/SVA/cycle_delay2.sv diff --git a/regression/ebmc/smv-netlist/cycle_delay1.desc b/regression/ebmc/smv-netlist/cycle_delay1.desc new file mode 100644 index 00000000..0df214c4 --- /dev/null +++ b/regression/ebmc/smv-netlist/cycle_delay1.desc @@ -0,0 +1,7 @@ +CORE +cycle_delay1.sv +--smv-netlist +^LTLSPEC node22 & X node25 & X X node28 & X X X node31$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv-netlist/cycle_delay1.sv b/regression/ebmc/smv-netlist/cycle_delay1.sv new file mode 100644 index 00000000..df3f0e8d --- /dev/null +++ b/regression/ebmc/smv-netlist/cycle_delay1.sv @@ -0,0 +1,10 @@ +module main(input clk); + + reg [3:0] x = 0; + + always_ff @(posedge clk) + x++; + + initial assert property (x == 0 ##1 x == 1 ##1 x == 2 ##1 x == 3); + +endmodule diff --git a/regression/ebmc/smv-netlist/cycle_delay2.desc b/regression/ebmc/smv-netlist/cycle_delay2.desc new file mode 100644 index 00000000..707568ab --- /dev/null +++ b/regression/ebmc/smv-netlist/cycle_delay2.desc @@ -0,0 +1,7 @@ +CORE +cycle_delay2.sv +--smv-netlist +^LTLSPEC X node22 \| X X node25$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv-netlist/cycle_delay2.sv b/regression/ebmc/smv-netlist/cycle_delay2.sv new file mode 100644 index 00000000..a3190bb7 --- /dev/null +++ b/regression/ebmc/smv-netlist/cycle_delay2.sv @@ -0,0 +1,10 @@ +module main(input clk); + + reg [3:0] x = 0; + + always_ff @(posedge clk) + x++; + + initial assert property (##[1:2] x == 2); + +endmodule diff --git a/regression/verilog/SVA/cycle_delay2.desc b/regression/verilog/SVA/cycle_delay2.desc new file mode 100644 index 00000000..92e83d0d --- /dev/null +++ b/regression/verilog/SVA/cycle_delay2.desc @@ -0,0 +1,7 @@ +CORE +cycle_delay2.sv +--bound 10 +^\[.*\] ##\[1:2\] main\.x == 2: PROVED up to bound 10$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/SVA/cycle_delay2.sv b/regression/verilog/SVA/cycle_delay2.sv new file mode 100644 index 00000000..a3190bb7 --- /dev/null +++ b/regression/verilog/SVA/cycle_delay2.sv @@ -0,0 +1,10 @@ +module main(input clk); + + reg [3:0] x = 0; + + always_ff @(posedge clk) + x++; + + initial assert property (##[1:2] x == 2); + +endmodule diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 9a14c397..7d1c6fce 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -225,6 +225,108 @@ static exprt n_Xes(mp_integer n, exprt op) return n_Xes(n - 1, X_exprt{std::move(op)}); } +// Returns a set of match conditions (given as LTL formula) +struct ltl_sequence_matcht +{ + ltl_sequence_matcht(exprt __cond, mp_integer __length) + : cond(std::move(__cond)), length(std::move(__length)) + { + PRECONDITION(length >= 0); + } + + exprt cond; // LTL + mp_integer length; // match_end - match_start + 1 + + bool empty() const + { + return length == 0; + } +}; + +std::vector LTL_sequence_matches(const exprt &sequence) +{ + if(!is_SVA_sequence_operator(sequence)) + { + // atomic proposition + return {{sequence, 1}}; + } + else if(sequence.id() == ID_sva_sequence_concatenation) + { + auto &concatenation = to_sva_sequence_concatenation_expr(sequence); + auto matches_lhs = LTL_sequence_matches(concatenation.lhs()); + auto matches_rhs = LTL_sequence_matches(concatenation.rhs()); + + if(matches_lhs.empty() || matches_rhs.empty()) + return {}; + + std::vector result; + // cross product + for(auto &match_lhs : matches_lhs) + for(auto &match_rhs : matches_rhs) + { + // Concatenation is overlapping, hence deduct one from + // the length. + auto delay = match_lhs.length - 1; + auto rhs_delayed = n_Xes(delay, match_rhs.cond); + result.emplace_back( + and_exprt{match_lhs.cond, rhs_delayed}, + match_lhs.length + match_rhs.length - 1); + } + return result; + } + else if(sequence.id() == ID_sva_cycle_delay) + { + auto &delay = to_sva_cycle_delay_expr(sequence); + auto matches = LTL_sequence_matches(delay.op()); + auto from_int = numeric_cast_v(delay.from()); + + if(matches.empty()) + return {}; + + if(delay.to().is_nil()) + { + for(auto &match : matches) + { + // delay as instructed + match.length += from_int; + match.cond = n_Xes(from_int, match.cond); + } + return matches; + } + else if(delay.to().id() == ID_infinity) + { + return {}; // can't encode + } + else if(delay.to().is_constant()) + { + auto to_int = numeric_cast_v(to_constant_expr(delay.to())); + std::vector new_matches; + + for(mp_integer i = from_int; i <= to_int; ++i) + { + for(const auto &match : matches) + { + // delay as instructed + auto new_match = match; + new_match.length += from_int; + new_match.cond = n_Xes(i, match.cond); + new_matches.push_back(std::move(new_match)); + } + } + + return new_matches; + } + else + return {}; + } + else + { + return {}; // unsupported + } +} + +/// takes an SVA property as input, and returns an equivalent LTL property, +/// or otherwise {}. std::optional SVA_to_LTL(exprt expr) { // Some SVA is directly mappable to LTL @@ -318,25 +420,104 @@ std::optional SVA_to_LTL(exprt expr) else return {}; } - else if(expr.id() == ID_sva_overlapped_implication) + else if( + expr.id() == ID_sva_overlapped_implication || + expr.id() == ID_sva_non_overlapped_implication) { - auto &implication = to_sva_overlapped_implication_expr(expr); - auto rec_lhs = SVA_to_LTL(implication.lhs()); - auto rec_rhs = SVA_to_LTL(implication.rhs()); - if(rec_lhs.has_value() && rec_rhs.has_value()) - return implies_exprt{rec_lhs.value(), rec_rhs.value()}; - else + auto &implication = to_sva_implication_base_expr(expr); + auto matches = LTL_sequence_matches(implication.sequence()); + + if(matches.empty()) + return {}; + + // All matches must be followed + // by the property being true + exprt::operandst conjuncts; + + auto property_rec = SVA_to_LTL(implication.property()); + + if(!property_rec.has_value()) return {}; + + for(auto &match : matches) + { + const auto overlapped = expr.id() == ID_sva_overlapped_implication; + if(match.empty() && overlapped) + { + // ignore the empty match + } + else + { + auto delay = match.length + (overlapped ? 0 : 1) - 1; + auto delayed_property = n_Xes(delay, property_rec.value()); + conjuncts.push_back(implies_exprt{match.cond, delayed_property}); + } + } + + return conjunction(conjuncts); } - else if(expr.id() == ID_sva_non_overlapped_implication) + else if( + expr.id() == ID_sva_nonoverlapped_followed_by || + expr.id() == ID_sva_overlapped_followed_by) { - auto &implication = to_sva_non_overlapped_implication_expr(expr); - auto rec_lhs = SVA_to_LTL(implication.lhs()); - auto rec_rhs = SVA_to_LTL(implication.rhs()); - if(rec_lhs.has_value() && rec_rhs.has_value()) - return implies_exprt{rec_lhs.value(), X_exprt{rec_rhs.value()}}; - else + auto &followed_by = to_sva_followed_by_expr(expr); + auto matches = LTL_sequence_matches(followed_by.sequence()); + + if(matches.empty()) + return {}; + + // There must be at least one match that is followed + // by the property being true + exprt::operandst disjuncts; + + auto property_rec = SVA_to_LTL(followed_by.property()); + + if(!property_rec.has_value()) return {}; + + for(auto &match : matches) + { + const auto overlapped = expr.id() == ID_sva_overlapped_followed_by; + if(match.empty() && overlapped) + { + // ignore the empty match + } + else + { + auto delay = match.length + (overlapped ? 0 : 1) - 1; + auto delayed_property = n_Xes(delay, property_rec.value()); + disjuncts.push_back(and_exprt{match.cond, delayed_property}); + } + } + + return disjunction(disjuncts); + } + else if(expr.id() == ID_sva_sequence_property) + { + // should have been turned into sva_implicit_weak or sva_implicit_strong + PRECONDITION(false); + } + else if( + expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || + expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) + { + auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); + + // evaluates to true if there's at least one non-empty match of the sequence + auto matches = LTL_sequence_matches(sequence); + + if(matches.empty()) + return {}; + + exprt::operandst disjuncts; + + for(auto &match : matches) + { + if(!match.empty()) + disjuncts.push_back(match.cond); + } + + return disjunction(disjuncts); } else if(expr.id() == ID_sva_s_until) { diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index de8b68f8..455cb5bc 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -663,6 +663,16 @@ class sva_implication_base_exprt : public binary_predicate_exprt return lhs(); } + const exprt &sequence() const + { + return op0(); + } + + exprt &sequence() + { + return op0(); + } + // a property const exprt &consequent() const { @@ -673,8 +683,32 @@ class sva_implication_base_exprt : public binary_predicate_exprt { return rhs(); } + + const exprt &property() const + { + return op1(); + } + + exprt &property() + { + return op1(); + } }; +static inline const sva_implication_base_exprt & +to_sva_implication_base_expr(const exprt &expr) +{ + sva_implication_base_exprt::check(expr); + return static_cast(expr); +} + +static inline sva_implication_base_exprt & +to_sva_implication_base_expr(exprt &expr) +{ + sva_implication_base_exprt::check(expr); + return static_cast(expr); +} + /// |-> class sva_overlapped_implication_exprt : public sva_implication_base_exprt {