From e289306e1868cdcff88582d2d2e43811e8970cdb Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 25 Feb 2025 18:27:25 +0000 Subject: [PATCH] SVA Monitors This adds an alternative flow for checking SVA properties, by translating the property into a monitor, which is added to the transition system. --- regression/ebmc/sva-monitor/always1.desc | 13 + regression/ebmc/sva-monitor/always1.sv | 5 + regression/ebmc/sva-monitor/initial1.desc | 6 + regression/ebmc/sva-monitor/initial1.sv | 5 + .../ebmc/sva-monitor/s_eventually1.desc | 7 + regression/ebmc/sva-monitor/s_eventually1.sv | 5 + regression/ebmc/sva-monitor/s_nexttime1.desc | 13 + regression/ebmc/sva-monitor/s_nexttime1.sv | 5 + regression/ebmc/sva-monitor/sequence1.desc | 6 + regression/ebmc/sva-monitor/sequence1.sv | 10 + src/ebmc/Makefile | 1 + src/ebmc/ebmc_parse_options.cpp | 13 +- src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/output_smv_word_level.cpp | 4 +- src/ebmc/sva_monitor.cpp | 341 ++++++++++++++++++ src/ebmc/sva_monitor.h | 17 + src/temporal-logic/temporal_logic.cpp | 5 + src/temporal-logic/temporal_logic.h | 3 + 18 files changed, 454 insertions(+), 7 deletions(-) create mode 100644 regression/ebmc/sva-monitor/always1.desc create mode 100644 regression/ebmc/sva-monitor/always1.sv create mode 100644 regression/ebmc/sva-monitor/initial1.desc create mode 100644 regression/ebmc/sva-monitor/initial1.sv create mode 100644 regression/ebmc/sva-monitor/s_eventually1.desc create mode 100644 regression/ebmc/sva-monitor/s_eventually1.sv create mode 100644 regression/ebmc/sva-monitor/s_nexttime1.desc create mode 100644 regression/ebmc/sva-monitor/s_nexttime1.sv create mode 100644 regression/ebmc/sva-monitor/sequence1.desc create mode 100644 regression/ebmc/sva-monitor/sequence1.sv create mode 100644 src/ebmc/sva_monitor.cpp create mode 100644 src/ebmc/sva_monitor.h diff --git a/regression/ebmc/sva-monitor/always1.desc b/regression/ebmc/sva-monitor/always1.desc new file mode 100644 index 00000000..4e663448 --- /dev/null +++ b/regression/ebmc/sva-monitor/always1.desc @@ -0,0 +1,13 @@ +CORE +always1.sv +--sva-monitor --smv-word-level +^VAR initial : boolean;$ +^VAR always_activated : boolean;$ +^INIT sva-monitor::initial$ +^INIT !sva-monitor::always_activated$ +^TRANS !next\(sva-monitor::initial\)$ +^TRANS next\(sva-monitor::always_activated\) = sva-monitor::always_active$ +^LTLSPEC G \(sva-monitor::always_active -> FALSE\)$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/sva-monitor/always1.sv b/regression/ebmc/sva-monitor/always1.sv new file mode 100644 index 00000000..a933472d --- /dev/null +++ b/regression/ebmc/sva-monitor/always1.sv @@ -0,0 +1,5 @@ +module main(input clk); + + p0: assert property (0); + +endmodule diff --git a/regression/ebmc/sva-monitor/initial1.desc b/regression/ebmc/sva-monitor/initial1.desc new file mode 100644 index 00000000..2ad1ef1c --- /dev/null +++ b/regression/ebmc/sva-monitor/initial1.desc @@ -0,0 +1,6 @@ +CORE +initial1.sv +--sva-monitor --smv-word-level +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/sva-monitor/initial1.sv b/regression/ebmc/sva-monitor/initial1.sv new file mode 100644 index 00000000..e8bbaf31 --- /dev/null +++ b/regression/ebmc/sva-monitor/initial1.sv @@ -0,0 +1,5 @@ +module main(input clk); + + initial p0: assert property (0); + +endmodule diff --git a/regression/ebmc/sva-monitor/s_eventually1.desc b/regression/ebmc/sva-monitor/s_eventually1.desc new file mode 100644 index 00000000..ea9ae3f9 --- /dev/null +++ b/regression/ebmc/sva-monitor/s_eventually1.desc @@ -0,0 +1,7 @@ +CORE +s_eventually1.sv +--sva-monitor --smv-word-level +^-- Verilog::main\.p0: not converted$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/sva-monitor/s_eventually1.sv b/regression/ebmc/sva-monitor/s_eventually1.sv new file mode 100644 index 00000000..86d33e71 --- /dev/null +++ b/regression/ebmc/sva-monitor/s_eventually1.sv @@ -0,0 +1,5 @@ +module main(input clk); + + p0: assert property (s_eventually 0); + +endmodule diff --git a/regression/ebmc/sva-monitor/s_nexttime1.desc b/regression/ebmc/sva-monitor/s_nexttime1.desc new file mode 100644 index 00000000..dd5f5208 --- /dev/null +++ b/regression/ebmc/sva-monitor/s_nexttime1.desc @@ -0,0 +1,13 @@ +CORE +s_nexttime1.sv +--sva-monitor --smv-word-level +^VAR initial : boolean;$ +^VAR delayed_active : boolean;$ +^INIT sva-monitor::initial$ +^INIT !sva-monitor::delayed_active$ +^TRANS !next\(sva-monitor::initial\)$ +^TRANS next\(sva-monitor::delayed_active\) = sva-monitor::initial$ +^LTLSPEC G \(sva-monitor::delayed_active -> FALSE\)$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/sva-monitor/s_nexttime1.sv b/regression/ebmc/sva-monitor/s_nexttime1.sv new file mode 100644 index 00000000..62e4777c --- /dev/null +++ b/regression/ebmc/sva-monitor/s_nexttime1.sv @@ -0,0 +1,5 @@ +module main(input clk); + + initial p0: assert property (s_nexttime 0); + +endmodule diff --git a/regression/ebmc/sva-monitor/sequence1.desc b/regression/ebmc/sva-monitor/sequence1.desc new file mode 100644 index 00000000..2d692b01 --- /dev/null +++ b/regression/ebmc/sva-monitor/sequence1.desc @@ -0,0 +1,6 @@ +CORE +sequence1.sv +--sva-monitor --smv-word-level +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/sva-monitor/sequence1.sv b/regression/ebmc/sva-monitor/sequence1.sv new file mode 100644 index 00000000..88794aa5 --- /dev/null +++ b/regression/ebmc/sva-monitor/sequence1.sv @@ -0,0 +1,10 @@ +module main(input clk); + + reg [31:0] x = 0; + + always_ff @(posedge clk) + x++; + + initial p0: assert property (x==0 ##1 x==1 ##1 x==2); + +endmodule diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index da61dc17..3613d98b 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -33,6 +33,7 @@ SRC = \ show_formula_solver.cpp \ show_properties.cpp \ show_trans.cpp \ + sva_monitor.cpp \ transition_system.cpp \ waveform.cpp \ #empty line diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 573c4393..48e07ae9 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ranking_function.h" #include "show_properties.h" #include "show_trans.h" +#include "sva_monitor.h" #include @@ -218,6 +219,13 @@ int ebmc_parse_optionst::doit() auto properties = ebmc_propertiest::from_command_line( cmdline, transition_system, ui_message_handler); + // possibly apply liveness-to-safety + if(cmdline.isset("liveness-to-safety")) + liveness_to_safety(transition_system, properties); + + if(cmdline.isset("sva-monitor")) + sva_monitor(transition_system, properties); + if(cmdline.isset("smv-word-level")) { auto filename = cmdline.value_opt("outfile").value_or("-"); @@ -239,10 +247,6 @@ int ebmc_parse_optionst::doit() return 0; } - // possibly apply liveness-to-safety - if(cmdline.isset("liveness-to-safety")) - liveness_to_safety(transition_system, properties); - if(cmdline.isset("show-varmap")) { auto netlist = @@ -373,6 +377,7 @@ void ebmc_parse_optionst::help() " {y--show-properties} \t list the properties in the model\n" " {y--property} {uid} \t check the property with given ID\n" " {y--liveness-to-safety} \t translate liveness properties to safety properties\n" + " {y--sva-monitor} \t translate SVA properties into a monitor circuit\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 index aa3b6968..d784fb73 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -49,7 +49,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)(sva-monitor)" "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" "(warn-implicit-nets)", argc, diff --git a/src/ebmc/output_smv_word_level.cpp b/src/ebmc/output_smv_word_level.cpp index ac8837ef..962ce258 100644 --- a/src/ebmc/output_smv_word_level.cpp +++ b/src/ebmc/output_smv_word_level.cpp @@ -119,7 +119,7 @@ smv_invar(const exprt &expr, const namespacet &ns, std::ostream &out) if(expr.id() == ID_and) { for(auto &conjunct : expr.operands()) - smv_initial_states(conjunct, ns, out); + smv_invar(conjunct, ns, out); } else if(expr.is_true()) { @@ -146,7 +146,7 @@ static void smv_transition_relation( if(expr.id() == ID_and) { for(auto &conjunct : expr.operands()) - smv_initial_states(conjunct, ns, out); + smv_transition_relation(conjunct, ns, out); } else if(expr.is_true()) { diff --git a/src/ebmc/sva_monitor.cpp b/src/ebmc/sva_monitor.cpp new file mode 100644 index 00000000..c4e92be0 --- /dev/null +++ b/src/ebmc/sva_monitor.cpp @@ -0,0 +1,341 @@ +/*******************************************************************\ + +Module: SVA Monitor + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "sva_monitor.h" + +#include + +#include +#include +#include +#include + +#include "ebmc_properties.h" +#include "transition_system.h" + +class monitor_resultt +{ +protected: + // use the factories below + monitor_resultt() + { + } + +public: + bool is_error() const + { + return !_error.empty(); + } + + const std::string &error() const + { + PRECONDITION(is_error()); + return _error; + } + + // factory for the 'error' case + static monitor_resultt error(std::string __error) + { + monitor_resultt monitor_result; + monitor_result._error = std::move(__error); + return monitor_result; + } + + // factory for the 'safe' case + static monitor_resultt safe(exprt __safe) + { + monitor_resultt monitor_result; + monitor_result._safe = std::move(__safe); + return monitor_result; + } + + const exprt &safe() const + { + return _safe; + } + + // factory for the 'safe' and 'done' case + static monitor_resultt safe_and_done(exprt __safe, exprt __done) + { + monitor_resultt monitor_result; + monitor_result._safe = std::move(__safe); + monitor_result._done = std::move(__done); + return monitor_result; + } + + const exprt &done() const + { + return _done; + } + + exprt as_LTL() const; + +protected: + std::string _error; + exprt _safe = true_exprt{}; + exprt _liveness = true_exprt{}; + exprt _done = false_exprt{}; +}; + +exprt monitor_resultt::as_LTL() const +{ + PRECONDITION(!is_error()); + + exprt::operandst conjuncts; + + if(!_safe.is_true()) + conjuncts.push_back(G_exprt{_safe}); + + if(!_liveness.is_true()) + conjuncts.push_back(G_exprt{F_exprt{_liveness}}); + + return conjunction(conjuncts); +} + +static symbol_exprt +aux_symbol(transition_systemt &transition_system, irep_idt base_name) +{ + auxiliary_symbolt symbol{ + "sva-monitor::" + id2string(base_name), + bool_typet{}, + transition_system.main_symbol->mode}; + + symbol.is_state_var = true; + symbol.module = transition_system.main_symbol->module; + symbol.base_name = base_name; + + auto result = transition_system.symbol_table.insert(std::move(symbol)); + CHECK_RETURN(result.second); + + return result.first.symbol_expr(); +} + +static exprt next(symbol_exprt symbol_expr) +{ + exprt tmp = std::move(symbol_expr); + tmp.id(ID_next_symbol); + return tmp; +} + +/// Recursion for creating a safety automaton for a safety property. +/// * the property is converted into NNF on the fly. +/// * the monitor starts with the given "active" signal, which +/// is expected to stay on once set. +monitor_resultt sva_sequence_monitor_rec( + transition_systemt &transition_system, + const exprt &active, + const exprt &sequence_expr) +{ + if(sequence_expr.id() == ID_sva_sequence_concatenation) + { + auto &concatenation = to_sva_sequence_concatenation_expr(sequence_expr); + auto &lhs = concatenation.lhs(); + auto &rhs = concatenation.rhs(); + + // 1. The 'active' signal of the rhs is the 'finish' signal of the lhs. + // 2. The overall 'safe' signal is the conjunction of lhs/rhs. + // 3. The overall 'done' signal is the rhs done signal. + auto lhs_rec = sva_sequence_monitor_rec(transition_system, active, lhs); + if(lhs_rec.is_error()) + return lhs_rec; + + auto rhs_rec = + sva_sequence_monitor_rec(transition_system, lhs_rec.done(), rhs); + if(rhs_rec.is_error()) + return rhs_rec; + + return monitor_resultt::safe_and_done( + and_exprt{lhs_rec.safe(), rhs_rec.safe()}, rhs_rec.done()); + } + else if(sequence_expr.id() == ID_sva_cycle_delay) + { + auto &delay = to_sva_cycle_delay_expr(sequence_expr); + + // Delay the 'active' signal as specified. + if(delay.to().is_nil()) + { + //return sva_monitor_rec(transition_system, delayed_active, delay.op()); + return monitor_resultt::error("no support for ##[x]"); + } + else if(delay.is_unbounded()) + { + return monitor_resultt::error("no support for ##[x:$]"); + } + else + { + return monitor_resultt::error("no support for ##[x:y]"); + } + } + else + return monitor_resultt::error( + "no support for " + sequence_expr.id_string()); +} + +/// Recursion for creating a safety automaton for a safety property. +/// * the property is converted into NNF on the fly. +/// * the monitor starts with the given "active" signal, which +/// is expected to stay on once set. +monitor_resultt sva_property_monitor_rec( + transition_systemt &transition_system, + const exprt &active, + const exprt &property_expr) +{ + if(!has_temporal_operator(property_expr)) + { + // A state formula only. Needs to hold in "active" states only. + // It is 'done' once 'active'. + return monitor_resultt::safe_and_done( + implies_exprt{active, property_expr}, active); + } + else if(property_expr.id() == ID_not) + { + // create NNF + auto &op = to_not_expr(property_expr).op(); + auto nnf_opt = negate_property_node(op); + if(nnf_opt) + return sva_property_monitor_rec(transition_system, active, *nnf_opt); + else + return monitor_resultt::error("no NNF for " + op.id_string()); + } + else if( + property_expr.id() == ID_implies || property_expr.id() == ID_nor || + property_expr.id() == ID_nand || property_expr.id() == ID_xor || + property_expr.id() == ID_xnor) + { + // We rely on NNF. + return monitor_resultt::error(property_expr.id_string() + " is TBD"); + } + else if(property_expr.id() == ID_and) + { + // The conjunction of safety automata is built by conjoining the + // 'safe' signal. + exprt::operandst conjuncts; + + for(auto &op : property_expr.operands()) + { + auto rec = sva_property_monitor_rec(transition_system, active, op); + if(rec.is_error()) + return rec; + conjuncts.push_back(rec.safe()); + } + + return monitor_resultt::safe(conjunction(conjuncts)); + } + else if(property_expr.id() == ID_or) + { + // Build automaton per disjunct. + // Keep a state bit per automaton to record an unsafe state. + // Signal an unsafe state when all subautomata signalled an unsafe state. + return monitor_resultt::error("OR is TBD"); + } + else if(property_expr.id() == ID_sva_always) + { + // Nondeterministically guess when to start monitoring. + const auto always_activated_expr = + aux_symbol(transition_system, "always_activated"); + + // "always activated" is false in the initial state + transition_system.trans_expr.init() = and_exprt{ + transition_system.trans_expr.init(), not_exprt{always_activated_expr}}; + + const auto always_active_expr = + aux_symbol(transition_system, "always_active"); + + transition_system.trans_expr.trans() = and_exprt{ + transition_system.trans_expr.trans(), + equal_exprt{next(always_activated_expr), always_active_expr}}; + + // once active, always active + transition_system.trans_expr.invar() = and_exprt{ + transition_system.trans_expr.invar(), + implies_exprt{always_activated_expr, always_active_expr}}; + + // recursion + auto &op = to_sva_always_expr(property_expr).op(); + + return sva_property_monitor_rec(transition_system, always_active_expr, op); + } + else if(property_expr.id() == ID_sva_s_always) + { + auto &s_always_expr = to_sva_s_always_expr(property_expr); + + if( + numeric_cast_v(to_constant_expr(s_always_expr.lower())) == + 1 && + numeric_cast_v(to_constant_expr(s_always_expr.upper())) == 1) + { + // Simply delay "active" one time frame. + const auto delayed_active_expr = + aux_symbol(transition_system, "delayed_active"); + + transition_system.trans_expr.init() = and_exprt{ + transition_system.trans_expr.init(), not_exprt{delayed_active_expr}}; + + transition_system.trans_expr.trans() = and_exprt{ + transition_system.trans_expr.trans(), + equal_exprt{next(delayed_active_expr), active}}; + + return sva_property_monitor_rec( + transition_system, delayed_active_expr, s_always_expr.op()); + } + else + return monitor_resultt::error("s_always is TBD"); + } + else if(property_expr.id() == ID_sva_sequence_property) + { + return sva_sequence_monitor_rec( + transition_system, + active, + to_sva_sequence_property_expr(property_expr).op()); + } + else + return monitor_resultt::error( + "no support for " + property_expr.id_string()); +} + +exprt sva_monitor_initial(transition_systemt &transition_system) +{ + const auto symbol_expr = aux_symbol(transition_system, "initial"); + + // true in the initial state + transition_system.trans_expr.init() = + and_exprt{transition_system.trans_expr.init(), symbol_expr}; + + // but false in subsequent states + transition_system.trans_expr.trans() = and_exprt{ + transition_system.trans_expr.trans(), not_exprt{next(symbol_expr)}}; + + return symbol_expr; +} + +void sva_monitor( + transition_systemt &transition_system, + ebmc_propertiest::propertyt &property) +{ + // Create the top-level "start" signal -- on in the initial states exactly. + auto start = sva_monitor_initial(transition_system); + + // start recursion over property expression + auto result = sva_property_monitor_rec( + transition_system, start, property.normalized_expr); + + if(result.is_error()) + property.unsupported(result.error()); + else + property.normalized_expr = G_exprt{result.safe()}; +} + +void sva_monitor( + transition_systemt &transition_system, + ebmc_propertiest &properties) +{ + for(auto &property : properties.properties) + { + sva_monitor(transition_system, property); + } +} diff --git a/src/ebmc/sva_monitor.h b/src/ebmc/sva_monitor.h new file mode 100644 index 00000000..abd3fe04 --- /dev/null +++ b/src/ebmc/sva_monitor.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +Module: SVA Monitor + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_SVA_MONITOR_H +#define CPROVER_TEMPORAL_LOGIC_SVA_MONITOR_H + +class transition_systemt; +class ebmc_propertiest; + +void sva_monitor(transition_systemt &, ebmc_propertiest &); + +#endif diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index a367b2c1..8f8275fd 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -142,6 +142,11 @@ bool is_SVA(const exprt &expr) return !has_subexpr(expr, non_SVA_operator); } +bool has_SVA_operator(const exprt &expr) +{ + return has_subexpr(expr, is_SVA_operator); +} + bool is_SVA_always_p(const exprt &expr) { return expr.id() == ID_sva_always && diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index fbe82eb7..e2a14457 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -68,6 +68,9 @@ bool is_SVA_sequence_operator(const exprt &); /// Returns true iff the given expression is an SVA temporal operator bool is_SVA_operator(const exprt &); +/// Returns true iff the given expression has an SVA temporal operator +bool has_SVA_operator(const exprt &); + /// Returns true iff the given expression is an SVA expression bool is_SVA(const exprt &);