From 9e0161ff56533cecdf5c10fb93072592642ce1a8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 22 Mar 2024 11:44:16 -0700 Subject: [PATCH] Verilog: continuous assignments to variables SystemVerilog allows (non-procedural) continuous assignments to variables. --- .../synthesis/continuous_assignment_to_variable.desc | 7 +++---- .../verilog/synthesis/continuous_assignment_to_variable.v | 4 +++- src/verilog/verilog_typecheck.cpp | 8 +++----- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable.desc b/regression/verilog/synthesis/continuous_assignment_to_variable.desc index e0b28210e..7b1b33d64 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_variable.desc @@ -1,8 +1,7 @@ CORE continuous_assignment_to_variable.v - -^EXIT=2$ +--bound 0 +^\[main\.property\.p1\] always main\.some_reg == main\.i: PROVED up to bound 0$ +^EXIT=0$ ^SIGNAL=0$ -^file continuous_assignment_to_variable\.v line 6: continuous assignment to a variable$ -^Identifier main\.some_reg is declared as bool on line 3\.$ -- diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable.v b/regression/verilog/synthesis/continuous_assignment_to_variable.v index b7d31ed4b..9968d34d8 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable.v +++ b/regression/verilog/synthesis/continuous_assignment_to_variable.v @@ -2,7 +2,9 @@ module main(input i); reg some_reg; - // should error assign some_reg = i; + // should pass + always assert p1: some_reg == i; + endmodule diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 51f27d107..ef5f37f74 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -666,7 +666,9 @@ void verilog_typecheckt::check_lhs( vassignt vassign) { if(lhs.id()==ID_index) + { check_lhs(to_index_expr(lhs).array(), vassign); + } else if(lhs.id()==ID_extractbit) { if(lhs.operands().size()!=2) @@ -701,11 +703,7 @@ void verilog_typecheckt::check_lhs( case A_CONTINUOUS: if(symbol.is_state_var) { - throw errort().with_location(lhs.source_location()) - << "continuous assignment to a variable\n" - << "Identifier " << symbol.display_name() << " is declared as " - << to_string(symbol.type) << " on line " << symbol.location.get_line() - << '.'; + // Continuous assignments can drive variables. } else if(symbol.is_input && !symbol.is_output) {