From d147813c6557e2aa47ad783843182c2294520e1f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 22 Mar 2024 10:56:01 -0700 Subject: [PATCH] Verilog: procedural continuous assignments This gives a separate id to procedural continuous assignments, to avoid confusion with continuous assignments. These are on path to deprecation, and we do not have synthesis support for them. --- ...ral_continuous_assignment_to_variable.desc | 7 ++++ ...edural_continuous_assignment_to_variable.v | 13 +++++++ src/hw_cbmc_irep_ids.h | 1 + src/verilog/parser.y | 2 +- src/verilog/verilog_elaborate.cpp | 3 ++ src/verilog/verilog_expr.h | 7 ++-- src/verilog/verilog_synthesis.cpp | 2 +- src/verilog/verilog_typecheck.cpp | 37 ++++++++++++++++--- src/verilog/verilog_typecheck.h | 10 ++++- 9 files changed, 70 insertions(+), 12 deletions(-) create mode 100644 regression/verilog/synthesis/procedural_continuous_assignment_to_variable.desc create mode 100644 regression/verilog/synthesis/procedural_continuous_assignment_to_variable.v diff --git a/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.desc b/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.desc new file mode 100644 index 000000000..c2d11d18f --- /dev/null +++ b/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.desc @@ -0,0 +1,7 @@ +CORE +procedural_continuous_assignment_to_variable.v + +^file .* line 7: synthesis of procedural continuous assignment not supported$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.v b/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.v new file mode 100644 index 000000000..8af58d9f6 --- /dev/null +++ b/regression/verilog/synthesis/procedural_continuous_assignment_to_variable.v @@ -0,0 +1,13 @@ +module main(input i); + + reg some_reg; + + // procedural continuous assignment + always @i begin + assign some_reg = i; + end + + // should pass + always assert p1: some_reg == i; + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index bdff43b95..2a650aa0d 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -65,6 +65,7 @@ IREP_ID_ONE(release) IREP_ID_ONE(force) IREP_ID_ONE(deassign) IREP_ID_ONE(continuous_assign) +IREP_ID_ONE(procedural_continuous_assign) IREP_ID_ONE(wait) IREP_ID_ONE(verilog_assert_property) IREP_ID_ONE(verilog_assume_property) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 5554c1135..57e3a0e93 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2542,7 +2542,7 @@ nonblocking_assignment: procedural_continuous_assignment: TOK_ASSIGN variable_assignment - { init($$, ID_continuous_assign); mto($$, $2); } + { init($$, ID_procedural_continuous_assign); mto($$, $2); } | TOK_DEASSIGN variable_lvalue { init($$, ID_deassign); mto($$, $2); } | TOK_FORCE variable_assignment diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 9ccdf970c..52794eadd 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -736,6 +736,9 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement) { collect_symbols(to_verilog_label_statement(statement).statement()); } + else if(statement.id() == ID_procedural_continuous_assign) + { + } else DATA_INVARIANT(false, "unexpected statement: " + statement.id_string()); } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index c23801028..155692698 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -1378,7 +1378,8 @@ inline verilog_repeatt &to_verilog_repeat(exprt &expr) class verilog_procedural_continuous_assignt:public verilog_statementt { public: - verilog_procedural_continuous_assignt():verilog_statementt(ID_continuous_assign) + verilog_procedural_continuous_assignt() + : verilog_statementt(ID_procedural_continuous_assign) { } }; @@ -1386,14 +1387,14 @@ class verilog_procedural_continuous_assignt:public verilog_statementt inline const verilog_procedural_continuous_assignt & to_verilog_procedural_continuous_assign(const exprt &expr) { - PRECONDITION(expr.id() == ID_continuous_assign); + PRECONDITION(expr.id() == ID_procedural_continuous_assign); return static_cast(expr); } inline verilog_procedural_continuous_assignt & to_verilog_procedural_continuous_assign(exprt &expr) { - PRECONDITION(expr.id() == ID_continuous_assign); + PRECONDITION(expr.id() == ID_procedural_continuous_assign); return static_cast(expr); } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0880d392a..98dd2da85 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -2580,7 +2580,7 @@ void verilog_synthesist::synth_statement( synth_case(statement); else if(statement.id()==ID_blocking_assign) synth_assign(statement, true); - else if(statement.id()==ID_continuous_assign) + else if(statement.id() == ID_procedural_continuous_assign) { throw errort().with_location(statement.source_location()) << "synthesis of procedural continuous assignment not supported"; diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 51f27d107..b910e1b06 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -725,7 +725,17 @@ void verilog_typecheckt::check_lhs( << to_string(symbol.type) << " on line " << symbol.location.get_line() << '.'; } + break; + case A_PROCEDURAL_CONTINUOUS: + if(!symbol.is_state_var && !symbol.is_lvalue) + { + throw errort().with_location(lhs.source_location()) + << "procedural continuous assignment to a net\n" + << "Identifier " << symbol.display_name() << " is declared as " + << to_string(symbol.type) << " on line " << symbol.location.get_line() + << '.'; + } break; } } @@ -755,10 +765,27 @@ Function: verilog_typecheckt::convert_procedural_continuous_assign void verilog_typecheckt::convert_procedural_continuous_assign( verilog_procedural_continuous_assignt &statement) { - // down and up again - convert_continuous_assign( - static_cast( - static_cast(statement))); + // On path to deprecation. + for(auto &assignment : statement.operands()) + { + if(assignment.id() != ID_equal || assignment.operands().size() != 2) + { + throw errort().with_location(assignment.source_location()) + << "malformed procedural continuous assignment"; + } + + assignment.type() = bool_typet(); + + exprt &lhs = to_binary_expr(assignment).lhs(); + exprt &rhs = to_binary_expr(assignment).rhs(); + + convert_expr(lhs); + convert_expr(rhs); + + propagate_type(rhs, lhs.type()); + + check_lhs(lhs, A_PROCEDURAL_CONTINUOUS); + } } /*******************************************************************\ @@ -1419,7 +1446,7 @@ void verilog_typecheckt::convert_statement( convert_case(to_verilog_case_base(statement)); else if(statement.id()==ID_blocking_assign) convert_assign(to_verilog_assign(statement), true); - else if(statement.id()==ID_continuous_assign) + else if(statement.id() == ID_procedural_continuous_assign) convert_procedural_continuous_assign( to_verilog_procedural_continuous_assign(statement)); else if( diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index d01b1c63e..ae8d48508 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -126,8 +126,14 @@ class verilog_typecheckt: void interface_statement(const class verilog_statementt &); // type checking - - typedef enum { A_CONTINUOUS, A_BLOCKING, A_NON_BLOCKING } vassignt; + + typedef enum + { + A_CONTINUOUS, + A_BLOCKING, + A_NON_BLOCKING, + A_PROCEDURAL_CONTINUOUS + } vassignt; // statements void convert_statement(class verilog_statementt &);