Merge pull request #505 from diffblue/always_comb

Verilog: fix always_comb synthesis

Author: tautschnig

regression/verilog/synthesis/always_comb3.desc

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

regression/verilog/synthesis/always_comb3.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+  reg q;
+  
+  reg w;
+
+  // ff
+  always @(posedge clk)
+    q = !q;
+
+  always_comb
+    w = q;
+
+  p1: assert property (@(posedge clk) w == q);
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -3023,11 +3023,15 @@ exprt verilog_synthesist::current_value(
 
     if(
       construct == constructt::ALWAYS || construct == constructt::ALWAYS_FF ||
-      construct == constructt::ALWAYS_LATCH)
+      construct == constructt::ALWAYS_LATCH ||
+      construct == constructt::ALWAYS_COMB)
+    {
       return symbol_expr(symbol, CURRENT);
+    }
     else
     {
-      // make it some non-deterministic value
+      // Initial state computation, i.e., this is a value _before_ the
+      // initial state  -- make it non-deterministic
       exprt result=exprt(ID_nondet_symbol, symbol.type);
       result.set(ID_identifier, symbol.name);
       result.set("initial_value", true);