Merge pull request #418 from diffblue/verilog-always

Verilog: `always_comb`, `always_ff`, `always_latch`

Author: kroening

regression/verilog/delays/delay_with_unit1.desc

@@ -3,5 +3,5 @@ delay_with_unit1.v
 
 ^EXIT=2$
 ^SIGNAL=0$
-^file .*: permanent assignment without event guard$
+^file .*: assignment in 'always' context without event guard$
 

regression/verilog/synthesis/always_comb1.desc

@@ -0,0 +1,8 @@
+CORE
+always_comb1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/synthesis/always_comb1.sv

@@ -0,0 +1,8 @@
+module main(input [7:0] data1);
+
+  logic [7:0] data2;
+  always_comb data2 = data1;
+
+  p1: assert property (data2 == data1);
+
+endmodule

regression/verilog/synthesis/always_comb2.desc

@@ -0,0 +1,11 @@
+CORE
+always_comb2.sv
+--bound 0
+^\[main\.property\.p0\] always \(main\.data == 0 |-> main\.decoded == 1\): PROVED up to bound 0$
+^\[main\.property\.p1\] always \(main\.data == 1 |-> main\.decoded == 2\): PROVED up to bound 0$
+^\[main\.property\.p2\] always \(main\.data == 2 |-> main\.decoded == 4\): PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/synthesis/always_comb2.sv

@@ -0,0 +1,16 @@
+module main(input [7:0] data);
+
+  // an 8-bit binary to unary decoder
+  reg [255:0] decoded;
+
+  always_comb begin
+    integer i;
+    for(i = 0; i < 256; i = i + 1)
+      decoded[i] = data == i;
+  end
+
+  p0: assert property (data == 0 |-> decoded == 1);
+  p1: assert property (data == 1 |-> decoded == 2);
+  p2: assert property (data == 2 |-> decoded == 4);
+
+endmodule

regression/verilog/synthesis/always_ff1.desc

@@ -0,0 +1,8 @@
+CORE
+always_ff1.sv
+--module main --k-induction
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.p0\] always main\.x >= 1 && main\.x <= 10: PROVED$
+--
+^warning: ignoring

regression/verilog/synthesis/always_ff1.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+  reg [31:0] x;
+
+  initial x=1;
+  always_ff @(posedge clk)
+    if(x<10)
+      x++;
+
+  // should pass
+  p0: assert property (x >= 1 && x <= 10);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -66,7 +66,10 @@ IREP_ID_ONE(force)
 IREP_ID_ONE(deassign)
 IREP_ID_ONE(continuous_assign)
 IREP_ID_ONE(wait)
-IREP_ID_ONE(always)
+IREP_ID_ONE(verilog_always)
+IREP_ID_ONE(verilog_always_comb)
+IREP_ID_ONE(verilog_always_ff)
+IREP_ID_ONE(verilog_always_latch)
 IREP_ID_ONE(named_port_connection)
 IREP_ID_ONE(verilog_final)
 IREP_ID_ONE(initial)

src/verilog/parser.y

@@ -2518,10 +2518,10 @@ always_construct: always_keyword statement
 	;
 
 always_keyword:
-	  TOK_ALWAYS       { init($$, ID_always); }
-	| TOK_ALWAYS_COMB  { init($$, ID_always); }
-	| TOK_ALWAYS_LATCH { init($$, ID_always); }
-	| TOK_ALWAYS_FF    { init($$, ID_always); }
+	  TOK_ALWAYS       { init($$, ID_verilog_always); }
+	| TOK_ALWAYS_COMB  { init($$, ID_verilog_always_comb); }
+	| TOK_ALWAYS_LATCH { init($$, ID_verilog_always_latch); }
+	| TOK_ALWAYS_FF    { init($$, ID_verilog_always_ff); }
 	;
 
 final_construct: TOK_FINAL function_statement

src/verilog/verilog_elaborate.cpp

@@ -729,9 +729,13 @@ void verilog_typecheckt::collect_symbols(
   {
     collect_symbols(to_verilog_decl(module_item));
   }
-  else if(module_item.id() == ID_always)
+  else if(
+    module_item.id() == ID_verilog_always ||
+    module_item.id() == ID_verilog_always_comb ||
+    module_item.id() == ID_verilog_always_ff ||
+    module_item.id() == ID_verilog_always_latch)
   {
-    collect_symbols(to_verilog_always(module_item).statement());
+    collect_symbols(to_verilog_always_base(module_item).statement());
   }
   else if(module_item.id() == ID_initial)
   {