Merge pull request #1238 from diffblue/verilog-genvar-prepostincdec

SystemVerilog: `++`/`--` for generate `for`

Author: kroening

regression/verilog/generate/generate-for4.desc

@@ -0,0 +1,6 @@
+CORE
+generate-for4.sv
+--bound 1
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/generate/generate-for4.sv

@@ -0,0 +1,14 @@
+module main;
+
+  wire [15:0] some_wire;
+
+  generate
+    genvar i;
+    for (i = 0; i <= 15; ++i)
+      assign some_wire[i] = (i%2) == 0;
+  endgenerate
+
+  // should pass
+  always assert property1: some_wire == 'b0101_0101_0101_0101;
+
+endmodule

regression/verilog/generate/generate-for5.desc

@@ -0,0 +1,6 @@
+CORE
+generate-for5.sv
+--bound 1
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/generate/generate-for5.sv

@@ -0,0 +1,14 @@
+module main;
+
+  wire [15:0] some_wire;
+
+  generate
+    genvar i;
+    for (i = 16; i != 0; i--)
+      assign some_wire[i - 1] = ((i-1)%2) == 0;
+  endgenerate
+
+  // should pass
+  always assert property1: some_wire == 'b0101_0101_0101_0101;
+
+endmodule

src/verilog/parser.y

@@ -3123,8 +3123,8 @@ generate_item_brace:
 
 loop_generate_construct:
 	  TOK_FOR '(' genvar_initialization ';'
-	              constant_expression ';'
-                      genvar_initialization ')'
+	              genvar_expression ';'
+                      genvar_iteration ')'
           generate_block
 		{ init($$, ID_generate_for);
 		  stack_expr($$).reserve_operands(4);
@@ -3135,11 +3135,22 @@ loop_generate_construct:
 		}
         ;
 
+genvar_expression: constant_expression;
+
 genvar_initialization:
 	  genvar_identifier '=' constant_expression
 	  	{ init($$, ID_generate_assign); mto($$, $1); mto($$, $3); }
 	;
 
+genvar_iteration:
+	  genvar_identifier assignment_operator genvar_expression
+		{ init($$, ID_generate_assign); mto($$, $1); mto($$, $3); }
+	| inc_or_dec_operator genvar_identifier
+		{ $$ = $1; mto($$, $2); }
+	| genvar_identifier inc_or_dec_operator
+		{ $$ = $2; mto($$, $1); }
+	;
+
 conditional_generate_construct:
 	  if_generate_construct
 	| case_generate_construct
@@ -4441,6 +4452,11 @@ unary_operator:
 	| TOK_TILDECARET   { init($$, ID_reduction_xnor); }
         ;
 
+inc_or_dec_operator:
+	  TOK_PLUSPLUS     { init($$, ID_preincrement); }
+	| TOK_MINUSMINUS   { init($$, ID_predecrement); }
+	;
+
 // System Verilog standard 1800-2017
 // A.8.7 Numbers
 

src/verilog/verilog_expr.h

@@ -408,6 +408,12 @@ inline verilog_module_itemt &to_verilog_module_item(irept &irep)
 class verilog_generate_assignt : public verilog_module_itemt
 {
 public:
+  verilog_generate_assignt(exprt __lhs, exprt __rhs)
+    : verilog_module_itemt{ID_generate_assign}
+  {
+    add_to_operands(std::move(__lhs), std::move(__rhs));
+  }
+
   const exprt &lhs() const
   {
     return op0();
@@ -562,9 +568,10 @@ class verilog_generate_fort : public verilog_module_itemt
     return op1();
   }
 
-  const verilog_generate_assignt &increment() const
+  // assignment, ++, --
+  const verilog_module_itemt &iteration() const
   {
-    return static_cast<const verilog_generate_assignt &>(op2());
+    return static_cast<const verilog_module_itemt &>(op2());
   }
 
   const verilog_module_itemt &body() const

src/verilog/verilog_generate.cpp

@@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include "verilog_typecheck.h"
+#include <util/arith_tools.h>
 
 #include "verilog_expr.h"
+#include "verilog_typecheck.h"
 
 /*******************************************************************\
 
@@ -268,7 +269,34 @@ void verilog_typecheckt::elaborate_generate_for(
 
     elaborate_generate_item(copy_of_body, dest);
 
-    // Now increase the loop counter.
-    elaborate_generate_assign(for_statement.increment(), dest);
+    // Now increase/decrease the loop counter.
+    {
+      auto statement = for_statement.iteration().id();
+      if(statement == ID_generate_assign)
+      {
+        elaborate_generate_assign(
+          to_verilog_generate_assign(for_statement.iteration()), dest);
+      }
+      else if(statement == ID_preincrement || statement == ID_predecrement)
+      {
+        // turn ++x and x++ into x = x + 1
+        // turn --x and x-- into x = x - 1
+        // The expressions are parse trees, prior to typechecking
+        auto &op = to_unary_expr(for_statement.iteration()).op();
+        auto one = constant_exprt{ID_1, typet{}};
+        auto new_value = binary_exprt{
+          op, statement == ID_preincrement ? ID_plus : ID_minus, one, typet{}};
+        auto assignment = verilog_generate_assignt{op, new_value};
+
+        elaborate_generate_assign(assignment, dest);
+      }
+      else
+      {
+        DATA_INVARIANT_WITH_DIAGNOSTICS(
+          false,
+          "unexpected genvar_iteration item",
+          for_statement.iteration().pretty());
+      }
+    }
   }
 }