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.

Author: kroening

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$
+--

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

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)

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

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());
 }

src/verilog/verilog_expr.h

@@ -1378,22 +1378,23 @@ 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)
   {
   }
 };
 
 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<const verilog_procedural_continuous_assignt &>(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<verilog_procedural_continuous_assignt &>(expr);
 }
 

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";

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<verilog_continuous_assignt &>(
-      static_cast<exprt &>(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(

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 &);