From b98e2173890475a672626246423dff7b100b5e58 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Mar 2024 12:58:54 -0700 Subject: [PATCH] SystemVerilog: distinguish assertions This changes the front-end to distinguish three kinds of assertions/assumptions: 1) concurrent assertions/assumptions ("assert property"), which can be module items or statements, 2) immediate assertion/assumption statements, and 3) SMV-style assertions/assumptions. Front-end and BMC back-end support for initial concurrent assertion statements is added. --- .../ebmc/Output-Register-Passing/main.v | 4 +- regression/ebmc/smv/initial1.desc | 9 ++ regression/ebmc/smv/initial1.smv | 12 +++ regression/verilog/SVA/initial1.desc | 10 ++- regression/verilog/SVA/initial1.sv | 11 ++- regression/verilog/modules/parameters2.v | 4 +- regression/verilog/tasks/tasks1.v | 2 +- src/hw-cbmc/Makefile | 1 + src/hw_cbmc_irep_ids.h | 6 +- src/temporal-logic/temporal_logic.cpp | 33 ++++---- src/temporal-logic/temporal_logic.h | 4 + .../instantiate_word_level.cpp | 77 ++++++++--------- src/trans-word-level/property.cpp | 29 ++++++- src/verilog/parser.y | 57 ++++--------- src/verilog/sva_expr.h | 66 +++++++++++++++ src/verilog/verilog_elaborate.cpp | 16 +++- src/verilog/verilog_expr.h | 48 +++++++---- src/verilog/verilog_interfaces.cpp | 5 +- src/verilog/verilog_synthesis.cpp | 83 ++++++++++++------- src/verilog/verilog_synthesis_class.h | 4 +- src/verilog/verilog_typecheck.cpp | 67 +++++++-------- 21 files changed, 355 insertions(+), 193 deletions(-) create mode 100644 regression/ebmc/smv/initial1.desc create mode 100644 regression/ebmc/smv/initial1.smv diff --git a/regression/ebmc/Output-Register-Passing/main.v b/regression/ebmc/Output-Register-Passing/main.v index 808971b83..11c08c078 100644 --- a/regression/ebmc/Output-Register-Passing/main.v +++ b/regression/ebmc/Output-Register-Passing/main.v @@ -13,12 +13,12 @@ module main(in1, in2); and1 A1 (in1, in2, o1, o2); - assert property1: o1 == (in1 & in2); + always assert property1: o1 == (in1 & in2); /* A2 is another instance of ports are referenced to the declaration by name. */ and1 A2 (.c(o1),.d(o2),.a(o1),.b(in2)); - assert property2: o1 == (in1 & in2); + always assert property2: o1 == (in1 & in2); endmodule // MODULE DEFINITION diff --git a/regression/ebmc/smv/initial1.desc b/regression/ebmc/smv/initial1.desc new file mode 100644 index 000000000..43ca566e8 --- /dev/null +++ b/regression/ebmc/smv/initial1.desc @@ -0,0 +1,9 @@ +CORE +initial1.smv +--bound 0 +^\[main::spec1\] main::var::tmp1 = TRUE: PROVED up to bound 0$ +^\[main::spec2\] main::var::tmp2 = TRUE: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/ebmc/smv/initial1.smv b/regression/ebmc/smv/initial1.smv new file mode 100644 index 000000000..21c1ecb23 --- /dev/null +++ b/regression/ebmc/smv/initial1.smv @@ -0,0 +1,12 @@ +MODULE main + +VAR tmp1: boolean; +VAR tmp2: boolean; + +ASSIGN init(tmp1):=1; + +-- should pass +SPEC tmp1 = 1; + +-- should fail +SPEC tmp2 = 1; diff --git a/regression/verilog/SVA/initial1.desc b/regression/verilog/SVA/initial1.desc index 557611a9c..a8c48a345 100644 --- a/regression/verilog/SVA/initial1.desc +++ b/regression/verilog/SVA/initial1.desc @@ -1,9 +1,13 @@ -KNOWNBUG +CORE initial1.sv --module main --bound 1 -^EXIT=0$ +^\[main\.property\.1\] main\.counter == 0: PROVED up to bound 1$ +^\[main\.property\.2\] main\.counter == 100: REFUTED$ +^\[main\.property\.3\] ##1 main\.counter == 1: PROVED up to bound 1$ +^\[main\.property\.4\] ##1 main\.counter == 100: REFUTED$ +^\[main\.property\.5\] s_nexttime main\.counter == 1: PROVED up to bound 1$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -Syntax is missing for initial label: assert property (...); diff --git a/regression/verilog/SVA/initial1.sv b/regression/verilog/SVA/initial1.sv index 79badcd0d..7bb6a06a7 100644 --- a/regression/verilog/SVA/initial1.sv +++ b/regression/verilog/SVA/initial1.sv @@ -14,7 +14,16 @@ module main(input clk); // expected to pass initial p0: assert property (counter == 0); + // expected to fail + initial p1: assert property (counter == 100); + + // expected to pass + initial p2: assert property (##1 counter == 1); + + // expected to fail + initial p2: assert property (##1 counter == 100); + // expected to pass if there are timeframes 0 and 1 - initial p1: assert property (s_nexttime counter == 1); + initial p3: assert property (s_nexttime counter == 1); endmodule diff --git a/regression/verilog/modules/parameters2.v b/regression/verilog/modules/parameters2.v index 45659fbc3..685c4d815 100644 --- a/regression/verilog/modules/parameters2.v +++ b/regression/verilog/modules/parameters2.v @@ -10,7 +10,7 @@ module test(in1, in2); my_m #( .Ptop(P), .Qtop(Q) ) m_instance(in1, in2, o1, o2); - assert property1: tmp == 4; // should pass + always assert property1: tmp == 4; // should pass endmodule @@ -25,6 +25,6 @@ module my_m(a, b, c, d); wire [3:0] tmp_in_m = Ptop; // tmp1 should be 4 now - assert property2: tmp_in_m == 4; // should pass + always assert property2: tmp_in_m == 4; // should pass endmodule diff --git a/regression/verilog/tasks/tasks1.v b/regression/verilog/tasks/tasks1.v index 3adf50294..4ae8e2000 100644 --- a/regression/verilog/tasks/tasks1.v +++ b/regression/verilog/tasks/tasks1.v @@ -12,6 +12,6 @@ module main; some_task(x, y); end - assert p1: y==x+1; + always assert p1: y==x+1; endmodule diff --git a/src/hw-cbmc/Makefile b/src/hw-cbmc/Makefile index eaec1a9c4..36a01d8b8 100644 --- a/src/hw-cbmc/Makefile +++ b/src/hw-cbmc/Makefile @@ -35,6 +35,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \ $(CPROVER_DIR)/solvers/solvers$(LIBEXT) \ $(CPROVER_DIR)/util/util$(LIBEXT) \ $(CPROVER_DIR)/json/json$(LIBEXT) \ + ../temporal-logic/temporal-logic$(LIBEXT) \ ../trans-netlist/trans_trace$(OBJEXT) \ ../trans-word-level/trans-word-level$(LIBEXT) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index b1eef9284..bdff43b95 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -66,6 +66,11 @@ IREP_ID_ONE(force) IREP_ID_ONE(deassign) IREP_ID_ONE(continuous_assign) IREP_ID_ONE(wait) +IREP_ID_ONE(verilog_assert_property) +IREP_ID_ONE(verilog_assume_property) +IREP_ID_ONE(verilog_cover_property) +IREP_ID_ONE(verilog_smv_assert) +IREP_ID_ONE(verilog_smv_assume) IREP_ID_ONE(verilog_always) IREP_ID_ONE(verilog_always_comb) IREP_ID_ONE(verilog_always_ff) @@ -76,7 +81,6 @@ IREP_ID_ONE(initial) IREP_ID_ONE(verilog_label_statement) IREP_ID_ONE(disable) IREP_ID_ONE(fork) -IREP_ID_ONE(cover) IREP_ID_ONE(instance) IREP_ID_ONE(named_parameter_assignment) IREP_ID_ONE(parameter_assignment) diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index e943a43b6..aa7416670 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -10,31 +10,28 @@ Author: Daniel Kroening, kroening@kroening.com #include +bool is_temporal_operator(const exprt &expr) +{ + return expr.id() == ID_AG || expr.id() == ID_EG || expr.id() == ID_AF || + expr.id() == ID_EF || expr.id() == ID_AX || expr.id() == ID_EX || + expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U || + expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F || + expr.id() == ID_X || expr.id() == ID_sva_always || + expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime || + expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until || + expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with || + expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually || + expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay; +} + bool has_temporal_operator(const exprt &expr) { for(auto subexpr_it = expr.depth_cbegin(), subexpr_end = expr.depth_cend(); subexpr_it != subexpr_end; subexpr_it++) { - // clang-format off - if( - subexpr_it->id() == ID_AG || subexpr_it->id() == ID_EG || - subexpr_it->id() == ID_AF || subexpr_it->id() == ID_EF || - subexpr_it->id() == ID_AX || subexpr_it->id() == ID_EX || - subexpr_it->id() == ID_A || subexpr_it->id() == ID_E || - subexpr_it->id() == ID_U || subexpr_it->id() == ID_R || - subexpr_it->id() == ID_G || subexpr_it->id() == ID_F || - subexpr_it->id() == ID_X || - subexpr_it->id() == ID_sva_always || subexpr_it->id() == ID_sva_always || - subexpr_it->id() == ID_sva_nexttime || subexpr_it->id() == ID_sva_s_nexttime || - subexpr_it->id() == ID_sva_until || subexpr_it->id() == ID_sva_s_until || - subexpr_it->id() == ID_sva_until_with || subexpr_it->id() == ID_sva_s_until_with || - subexpr_it->id() == ID_sva_eventually || - subexpr_it->id() == ID_sva_s_eventually) - { + if(is_temporal_operator(*subexpr_it)) return true; - } - // clang-format on } return false; diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index f9a8d9330..f636e942d 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -14,4 +14,8 @@ Author: Daniel Kroening, dkr@amazon.com /// Returns true iff the given expression contains a temporal operator bool has_temporal_operator(const exprt &); +/// Returns true iff the given expression has a temporal operator +/// as its root +bool is_temporal_operator(const exprt &); + #endif diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp index 2812c870d..8e9beb3c1 100644 --- a/src/trans-word-level/instantiate_word_level.cpp +++ b/src/trans-word-level/instantiate_word_level.cpp @@ -148,60 +148,55 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const } else if(expr.id()==ID_sva_cycle_delay) // ##[1:2] something { - if(expr.operands().size()==3) + auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr); + + if(sva_cycle_delay_expr.to().is_nil()) { - auto &ternary_expr = to_ternary_expr(expr); + mp_integer offset; + if(to_integer_non_constant(sva_cycle_delay_expr.from(), offset)) + throw "failed to convert sva_cycle_delay offset"; - if(ternary_expr.op1().is_nil()) - { - mp_integer offset; - if(to_integer_non_constant(ternary_expr.op0(), offset)) - throw "failed to convert sva_cycle_delay offset"; + const auto u = t + offset; - const auto u = t + offset; + // Do we exceed the bound? Make it 'true' + if(u >= no_timeframes) + return true_exprt(); + else + return instantiate_rec(sva_cycle_delay_expr.op(), u); + } + else + { + mp_integer from, to; + if(to_integer_non_constant(sva_cycle_delay_expr.from(), from)) + throw "failed to convert sva_cycle_delay offsets"; - // Do we exceed the bound? Make it 'true' - if(u >= no_timeframes) - return true_exprt(); - else - return instantiate_rec(ternary_expr.op2(), u); + if(sva_cycle_delay_expr.to().id() == ID_infinity) + { + assert(no_timeframes != 0); + to = no_timeframes - 1; } - else + else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to)) + throw "failed to convert sva_cycle_delay offsets"; + + // This is an 'or', and we let it fail if the bound is too small. + + exprt::operandst disjuncts; + + for(mp_integer offset = from; offset < to; ++offset) { - mp_integer from, to; - if(to_integer_non_constant(ternary_expr.op0(), from)) - throw "failed to convert sva_cycle_delay offsets"; + auto u = t + offset; - if(ternary_expr.op1().id() == ID_infinity) + if(u >= no_timeframes) { - assert(no_timeframes!=0); - to=no_timeframes-1; } - else if(to_integer_non_constant(ternary_expr.op1(), to)) - throw "failed to convert sva_cycle_delay offsets"; - - // This is an 'or', and we let it fail if the bound is too small. - - exprt::operandst disjuncts; - - for(mp_integer offset=from; offset= no_timeframes) - { - } - else - { - disjuncts.push_back(instantiate_rec(ternary_expr.op2(), u)); - } + disjuncts.push_back(instantiate_rec(sva_cycle_delay_expr.op(), u)); } - - return disjunction(disjuncts); } + + return disjunction(disjuncts); } - else - return expr; } else if(expr.id()==ID_sva_sequence_concatenation) { diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index ce559df30..308ef2a7b 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "instantiate_word_level.h" @@ -34,8 +35,19 @@ Function: bmc_supports_property bool bmc_supports_property(const exprt &expr) { - if(expr.is_constant()) - return true; + if(!is_temporal_operator(expr)) + { + if(!has_temporal_operator(expr)) + return true; // initial state only + else + return false; + } + else if(expr.id() == ID_sva_cycle_delay) + return !has_temporal_operator(to_sva_cycle_delay_expr(expr).op()); + else if(expr.id() == ID_sva_nexttime) + return !has_temporal_operator(to_sva_nexttime_expr(expr).op()); + else if(expr.id() == ID_sva_s_nexttime) + return !has_temporal_operator(to_sva_s_nexttime_expr(expr).op()); else if(expr.id() == ID_AG) return true; else if(expr.id() == ID_G) @@ -68,9 +80,20 @@ void property( { messaget message(message_handler); - if(property_expr.is_true()) + // Initial state only property? + if( + !is_temporal_operator(property_expr) || + property_expr.id() == ID_sva_cycle_delay || + property_expr.id() == ID_sva_nexttime || + property_expr.id() == ID_sva_s_nexttime) { prop_handles.resize(no_timeframes, true_exprt()); + if(no_timeframes > 0) + { + exprt tmp = instantiate(property_expr, 0, no_timeframes, ns); + prop_handles.push_back(solver.handle(tmp)); + } + return; } diff --git a/src/verilog/parser.y b/src/verilog/parser.y index d289b4d48..5554c1135 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1908,32 +1908,34 @@ concurrent_assertion_statement: | cover_property_statement ; -assert_property_statement: - TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block - { init($$, ID_assert); mto($$, $4); mto($$, $6); } - | /* this one is in because SMV does it */ +/* This one mimicks functionality in Cadence SMV */ +smv_assertion_statement: TOK_ASSERT property_identifier TOK_COLON expression ';' - { init($$, ID_assert); stack_expr($$).operands().resize(2); + { init($$, ID_verilog_smv_assert); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); stack_expr($$).set(ID_identifier, stack_expr($2).id()); } - ; - -assume_property_statement: - TOK_ASSUME TOK_PROPERTY '(' property_expr ')' action_block - { init($$, ID_assume); mto($$, $4); mto($$, $6); } - | /* this one is in because SMV does it */ - TOK_ASSUME property_identifier TOK_COLON expression ';' - { init($$, ID_assume); stack_expr($$).operands().resize(2); + | TOK_ASSUME property_identifier TOK_COLON expression ';' + { init($$, ID_verilog_smv_assume); stack_expr($$).operands().resize(2); to_binary_expr(stack_expr($$)).op0().swap(stack_expr($4)); to_binary_expr(stack_expr($$)).op1().make_nil(); stack_expr($$).set(ID_identifier, stack_expr($2).id()); } ; +assert_property_statement: + TOK_ASSERT TOK_PROPERTY '(' property_expr ')' action_block + { init($$, ID_verilog_assert_property); mto($$, $4); mto($$, $6); } + ; + +assume_property_statement: + TOK_ASSUME TOK_PROPERTY '(' property_expr ')' action_block + { init($$, ID_verilog_assume_property); mto($$, $4); mto($$, $6); } + ; + cover_property_statement: TOK_COVER TOK_PROPERTY '(' expression ')' action_block - { init($$, ID_cover); mto($$, $4); mto($$, $6); } + { init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); } ; assertion_item_declaration: @@ -2602,32 +2604,6 @@ par_block: addswap($$, ID_base_name, $3); } ; -concurrent_assert_statement: - assert_property_statement - | block_identifier TOK_COLON assert_property_statement - { - $$=$3; - stack_expr($$).set(ID_identifier, stack_expr($1).id()); - } - ; - -concurrent_assume_statement: - assume_property_statement - | block_identifier TOK_COLON assume_property_statement - { - $$=$3; - stack_expr($$).set(ID_identifier, stack_expr($1).id()); - } - ; - -concurrent_cover_statement: cover_property_statement - | block_identifier TOK_COLON cover_property_statement - { - $$=$3; - stack_expr($$).set(ID_identifier, stack_expr($1).id()); - } - ; - // System Verilog standard 1800-2017 // A.6.4 Statements @@ -2850,6 +2826,7 @@ procedural_assertion_statement: concurrent_assertion_statement | immediate_assertion_statement /* | checker_instantiation */ + | smv_assertion_statement ; immediate_assertion_statement: diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index bf92c6b88..1ed1bb685 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -323,4 +323,70 @@ to_sva_non_overlapped_implication_expr(exprt &expr) return static_cast(expr); } +class sva_cycle_delay_exprt : public ternary_exprt +{ +public: + explicit sva_cycle_delay_exprt(exprt from, exprt to, exprt op) + : ternary_exprt( + ID_sva_cycle_delay, + std::move(from), + std::move(to), + std::move(op), + bool_typet()) + { + } + + const exprt &from() const + { + return op0(); + } + + exprt &from() + { + return op0(); + } + + // may be nil (just the singleton 'from') or + // infinity (half-open interval starting at 'from') + const exprt &to() const + { + return op1(); + } + + exprt &to() + { + return op1(); + } + + const exprt &op() const + { + return op2(); + } + + exprt &op() + { + return op2(); + } + +protected: + using ternary_exprt::op0; + using ternary_exprt::op1; + using ternary_exprt::op2; +}; + +static inline const sva_cycle_delay_exprt & +to_sva_cycle_delay_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay); + sva_cycle_delay_exprt::check(expr); + return static_cast(expr); +} + +static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay); + sva_cycle_delay_exprt::check(expr); + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 9cc0a7f4c..9ccdf970c 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -649,6 +649,17 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement) if(statement.id() == ID_assert || statement.id() == ID_assume) { } + else if( + statement.id() == ID_verilog_assert_property || + statement.id() == ID_verilog_assume_property || + statement.id() == ID_verilog_cover_property) + { + } + else if( + statement.id() == ID_verilog_smv_assert || + statement.id() == ID_verilog_smv_assume) + { + } else if(statement.id() == ID_block) { // These may be named @@ -779,7 +790,10 @@ void verilog_typecheckt::collect_symbols( else if(module_item.id() == ID_continuous_assign) { } - else if(module_item.id() == ID_assert || module_item.id() == ID_assume) + else if( + module_item.id() == ID_verilog_assert_property || + module_item.id() == ID_verilog_assume_property || + module_item.id() == ID_verilog_cover_property) { } else if(module_item.id() == ID_parameter_override) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index f4d1eb86b..c23801028 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -1598,11 +1598,12 @@ inline verilog_non_blocking_assignt &to_verilog_non_blocking_assign(exprt &expr) return static_cast(expr); } -/// Verilog concurrent assertions +/// Verilog concurrent assertion module item class verilog_assert_module_itemt : public verilog_module_itemt { public: - verilog_assert_module_itemt() : verilog_module_itemt(ID_assert) + verilog_assert_module_itemt() + : verilog_module_itemt(ID_verilog_assert_property) { operands().resize(2); } @@ -1631,7 +1632,7 @@ class verilog_assert_module_itemt : public verilog_module_itemt inline const verilog_assert_module_itemt & to_verilog_assert_module_item(const verilog_module_itemt &module_item) { - PRECONDITION(module_item.id() == ID_assert); + PRECONDITION(module_item.id() == ID_verilog_assert_property); binary_exprt::check(module_item); return static_cast(module_item); } @@ -1639,16 +1640,17 @@ to_verilog_assert_module_item(const verilog_module_itemt &module_item) inline verilog_assert_module_itemt & to_verilog_assert_module_item(verilog_module_itemt &module_item) { - PRECONDITION(module_item.id() == ID_assert); + PRECONDITION(module_item.id() == ID_verilog_assert_property); binary_exprt::check(module_item); return static_cast(module_item); } -/// Verilog concurrent assumptions +/// Verilog concurrent assumption module item class verilog_assume_module_itemt : public verilog_module_itemt { public: - verilog_assume_module_itemt() : verilog_module_itemt(ID_assume) + verilog_assume_module_itemt() + : verilog_module_itemt(ID_verilog_assume_property) { operands().resize(2); } @@ -1677,7 +1679,7 @@ class verilog_assume_module_itemt : public verilog_module_itemt inline const verilog_assume_module_itemt & to_verilog_assume_module_item(const verilog_module_itemt &module_item) { - PRECONDITION(module_item.id() == ID_assume); + PRECONDITION(module_item.id() == ID_verilog_assume_property); binary_exprt::check(module_item); return static_cast(module_item); } @@ -1685,12 +1687,15 @@ to_verilog_assume_module_item(const verilog_module_itemt &module_item) inline verilog_assume_module_itemt & to_verilog_assume_module_item(verilog_module_itemt &module_item) { - PRECONDITION(module_item.id() == ID_assume); + PRECONDITION(module_item.id() == ID_verilog_assume_property); binary_exprt::check(module_item); return static_cast(module_item); } -// Intermediate assertion statements, and SMV-style assertions. +// Can be one of three: +// 1) Intermediate assertion statement +// 2) Concurrent assertion statement +// 3) SMV-style assertion statement class verilog_assert_statementt : public verilog_statementt { public: @@ -1725,7 +1730,10 @@ class verilog_assert_statementt : public verilog_statementt inline const verilog_assert_statementt & to_verilog_assert_statement(const verilog_statementt &statement) { - PRECONDITION(statement.id() == ID_assert); + PRECONDITION( + statement.id() == ID_assert || + statement.id() == ID_verilog_assert_property || + statement.id() == ID_verilog_smv_assert); binary_exprt::check(statement); return static_cast(statement); } @@ -1733,12 +1741,18 @@ to_verilog_assert_statement(const verilog_statementt &statement) inline verilog_assert_statementt & to_verilog_assert_statement(verilog_statementt &statement) { - PRECONDITION(statement.id() == ID_assert); + PRECONDITION( + statement.id() == ID_assert || + statement.id() == ID_verilog_assert_property || + statement.id() == ID_verilog_smv_assert); binary_exprt::check(statement); return static_cast(statement); } -// Intermediate assumption statements, and SMV-style assumptions. +// Can be one of three: +// 1) Intermediate assumption statement +// 2) Concurrent assumption statement +// 3) SMV-style assumption statement class verilog_assume_statementt : public verilog_statementt { public: @@ -1773,7 +1787,10 @@ class verilog_assume_statementt : public verilog_statementt inline const verilog_assume_statementt & to_verilog_assume_statement(const verilog_statementt &statement) { - PRECONDITION(statement.id() == ID_assume); + PRECONDITION( + statement.id() == ID_assume || + statement.id() == ID_verilog_assume_property || + statement.id() == ID_verilog_smv_assume); binary_exprt::check(statement); return static_cast(statement); } @@ -1781,7 +1798,10 @@ to_verilog_assume_statement(const verilog_statementt &statement) inline verilog_assume_statementt & to_verilog_assume_statement(verilog_statementt &statement) { - PRECONDITION(statement.id() == ID_assume); + PRECONDITION( + statement.id() == ID_assume || + statement.id() == ID_verilog_assume_property || + statement.id() == ID_verilog_smv_assume); binary_exprt::check(statement); return static_cast(statement); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 7a6c97c26..194e435c6 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -264,7 +264,10 @@ void verilog_typecheckt::interface_module_item( interface_generate_block(to_verilog_generate_block(module_item)); else if(module_item.id() == ID_set_genvars) interface_module_item(to_verilog_set_genvars(module_item).module_item()); - else if(module_item.id() == ID_assert || module_item.id() == ID_assume) + else if( + module_item.id() == ID_verilog_assert_property || + module_item.id() == ID_verilog_assume_property || + module_item.id() == ID_verilog_cover_property) { // done later } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 852310468..0880d392a 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr2verilog.h" +#include "sva_expr.h" #include "verilog_expr.h" #include "verilog_typecheck_expr.h" @@ -1797,15 +1798,37 @@ Function: verilog_synthesist::synth_assert void verilog_synthesist::synth_assert( const verilog_assert_statementt &statement) { - const irep_idt &identifier=statement.get(ID_identifier); + const irep_idt &identifier = statement.identifier(); symbolt &symbol=symbol_table_lookup(identifier); - - symbol.value = synth_expr(symbol.value, symbol_statet::CURRENT); + + // Are we in an initial or always block? + if(construct == constructt::INITIAL) + { + if(statement.id() == ID_assert) + { + // immediate + symbol.value = synth_expr(statement.condition(), symbol_statet::CURRENT); + } + else + { + // Verilog concurrent or SMV-style assertion + symbol.value = synth_expr(statement.condition(), symbol_statet::SYMBOL); + } + } + else // one of the 'always' variants + { + auto cond = synth_expr(statement.condition(), symbol_statet::CURRENT); + + if(cond.id() != ID_sva_always) + cond = sva_always_exprt(cond); // implicit 'always' + + symbol.value = std::move(cond); + } } /*******************************************************************\ -Function: verilog_synthesist::synth_assert_module_item +Function: verilog_synthesist::synth_assert Inputs: @@ -1815,21 +1838,21 @@ Function: verilog_synthesist::synth_assert_module_item \*******************************************************************/ -void verilog_synthesist::synth_assert_module_item( - const verilog_module_itemt &module_item) +void verilog_synthesist::synth_assert( + const verilog_assert_module_itemt &module_item) { - if(module_item.operands().size()!=2) - { - throw errort().with_location(module_item.source_location()) - << "assert module_item expected to have two operands"; - } - - const irep_idt &identifier=module_item.get(ID_identifier); + const irep_idt &identifier = module_item.identifier(); symbolt &symbol=symbol_table_lookup(identifier); - + construct=constructt::OTHER; - symbol.value = synth_expr(symbol.value, symbol_statet::SYMBOL); + auto cond = synth_expr(module_item.condition(), symbol_statet::SYMBOL); + + // concurrent assertions come with an implicit 'always' + if(cond.id() != ID_sva_always) + cond = sva_always_exprt(cond); + + symbol.value = std::move(cond); } /*******************************************************************\ @@ -1857,7 +1880,7 @@ void verilog_synthesist::synth_assume( /*******************************************************************\ -Function: verilog_synthesist::synth_assume_module_item +Function: verilog_synthesist::synth_assume Inputs: @@ -1867,15 +1890,9 @@ Function: verilog_synthesist::synth_assume_module_item \*******************************************************************/ -void verilog_synthesist::synth_assume_module_item( - const verilog_module_itemt &module_item) +void verilog_synthesist::synth_assume( + const verilog_assume_module_itemt &module_item) { - if(module_item.operands().size()!=2) - { - throw errort().with_location(module_item.source_location()) - << "assume module item expected to have two operands"; - } - auto condition = synth_expr(to_binary_expr(module_item).op0(), symbol_statet::SYMBOL); // add it as an invariant @@ -2568,9 +2585,15 @@ void verilog_synthesist::synth_statement( throw errort().with_location(statement.source_location()) << "synthesis of procedural continuous assignment not supported"; } - else if(statement.id()==ID_assert) + else if( + statement.id() == ID_assert || + statement.id() == ID_verilog_assert_property || + statement.id() == ID_verilog_smv_assert) synth_assert(to_verilog_assert_statement(statement)); - else if(statement.id()==ID_assume) + else if( + statement.id() == ID_assume || + statement.id() == ID_verilog_assume_property || + statement.id() == ID_verilog_smv_assume) synth_assume(to_verilog_assume_statement(statement)); else if(statement.id()==ID_non_blocking_assign) synth_assign(statement, false); @@ -2665,10 +2688,10 @@ void verilog_synthesist::synth_module_item( synth_module_item(block_item, trans); } } - else if(module_item.id()==ID_assert) - synth_assert_module_item(module_item); - else if(module_item.id()==ID_assume) - synth_assume_module_item(module_item); + else if(module_item.id() == ID_verilog_assert_property) + synth_assert(to_verilog_assert_module_item(module_item)); + else if(module_item.id() == ID_verilog_assume_property) + synth_assume(to_verilog_assume_module_item(module_item)); else if(module_item.id()==ID_task) { // ignore for now diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h index cd308bc18..905a287a5 100644 --- a/src/verilog/verilog_synthesis_class.h +++ b/src/verilog/verilog_synthesis_class.h @@ -220,8 +220,8 @@ class verilog_synthesist: void synth_module_item(const verilog_module_itemt &, transt &); void synth_always_base(const verilog_always_baset &); void synth_initial(const verilog_initialt &); - void synth_assert_module_item(const verilog_module_itemt &); - void synth_assume_module_item(const verilog_module_itemt &); + void synth_assert(const verilog_assert_module_itemt &); + void synth_assume(const verilog_assume_module_itemt &); void synth_continuous_assign(const verilog_continuous_assignt &); void synth_force_rec(exprt &lhs, exprt &rhs, transt &); void synth_module_instance(const verilog_instt &, transt &); diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index c6352a498..51f27d107 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr2verilog.h" -#include "sva_expr.h" #include "verilog_expr.h" #include "verilog_types.h" @@ -986,23 +985,18 @@ void verilog_typecheckt::convert_assert( convert_expr(cond); make_boolean(cond); - - // There is an implicit 'always' - exprt property; - - if(cond.id()==ID_sva_always) - property=cond; - else - property = sva_always_exprt(cond); - - assertion_counter++; + // We create a symbol for the property. + // The 'value' of the symbol is set by synthesis. const irep_idt &identifier = module_item.identifier(); irep_idt base_name; if(identifier == irep_idt()) + { + assertion_counter++; base_name=std::to_string(assertion_counter); + } else base_name=identifier; @@ -1019,14 +1013,11 @@ void verilog_typecheckt::convert_assert( module_item.identifier(full_identifier); - symbolt symbol; + symbolt symbol{base_name, bool_typet{}, mode}; - symbol.mode=mode; symbol.module=module_identifier; - symbol.value.swap(property); - symbol.base_name=base_name; - symbol.name=full_identifier; - symbol.type=bool_typet(); + symbol.value = nil_exprt{}; // set by synthesis + symbol.name = full_identifier; symbol.is_property=true; symbol.location = module_item.find_source_location(); symbol.pretty_name=strip_verilog_prefix(full_identifier); @@ -1037,7 +1028,7 @@ void verilog_typecheckt::convert_assert( /*******************************************************************\ -Function: verilog_typecheckt::convert_assume +Function: verilog_typecheckt::convert_assume_property Inputs: @@ -1075,22 +1066,17 @@ void verilog_typecheckt::convert_assert(verilog_assert_statementt &statement) convert_expr(cond); make_boolean(cond); - // There is an implicit 'always' - exprt property; - - if(cond.id() == ID_sva_always) - property = cond; - else - property = sva_always_exprt(cond); - - assertion_counter++; - + // We create a symbol for the property. + // The 'value' is set by synthesis. const irep_idt &identifier = statement.identifier(); irep_idt base_name; if(identifier == irep_idt()) + { + assertion_counter++; base_name = std::to_string(assertion_counter); + } else base_name = identifier; @@ -1108,7 +1094,7 @@ void verilog_typecheckt::convert_assert(verilog_assert_statementt &statement) symbolt symbol{base_name, bool_typet{}, mode}; symbol.module = module_identifier; - symbol.value.swap(property); + symbol.value = nil_exprt{}; // set by synthesis symbol.name = full_identifier; symbol.is_property = true; symbol.location = statement.find_source_location(); @@ -1436,10 +1422,19 @@ void verilog_typecheckt::convert_statement( else if(statement.id()==ID_continuous_assign) convert_procedural_continuous_assign( to_verilog_procedural_continuous_assign(statement)); - else if(statement.id()==ID_assert) + else if( + statement.id() == ID_assert || + statement.id() == ID_verilog_assert_property || + statement.id() == ID_verilog_smv_assert) convert_assert(to_verilog_assert_statement(statement)); - else if(statement.id()==ID_assume) + else if( + statement.id() == ID_assume || + statement.id() == ID_verilog_assume_property || + statement.id() == ID_verilog_smv_assume) convert_assume(to_verilog_assume_statement(statement)); + else if(statement.id() == ID_verilog_cover_property) + { + } else if(statement.id()==ID_non_blocking_assign) convert_assign(to_verilog_assign(statement), false); else if(statement.id()==ID_if) @@ -1513,10 +1508,16 @@ void verilog_typecheckt::convert_module_item( module_item.id() == ID_verilog_always_comb || module_item.id() == ID_verilog_always_ff || module_item.id() == ID_verilog_always_latch) + { convert_always_base(to_verilog_always_base(module_item)); - else if(module_item.id()==ID_assert) + } + else if( + module_item.id() == ID_verilog_assert_property || + module_item.id() == ID_verilog_smv_assert) convert_assert(to_verilog_assert_module_item(module_item)); - else if(module_item.id()==ID_assume) + else if( + module_item.id() == ID_verilog_assume_property || + module_item.id() == ID_verilog_smv_assume) convert_assume(to_verilog_assume_module_item(module_item)); else if(module_item.id()==ID_initial) convert_initial(to_verilog_initial(module_item));