Merge pull request #427 from diffblue/continuous_assignment_to_variable

Verilog: continuous assignments to variables

Author: tautschnig

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\.$
 --

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

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)
       {