Merge pull request #472 from diffblue/immediate1

Verilog: procedural assert/assume/cover are guarded

Author: kroening

regression/verilog/SVA/immediate2.desc

@@ -0,0 +1,10 @@
+CORE broken-smt-backend
+immediate2.sv
+--bound 0
+^\[main\.property\.1\] always main\.index < 10: PROVED up to bound 0$
+^\[main\.property\.2\] always 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/immediate2.sv

@@ -0,0 +1,14 @@
+module main(input [31:0] index);
+
+  always @index begin
+    if(index >= 10)
+      assume(0);
+
+    // should pass
+    assert(index < 10);
+
+    // should fail
+    assert(0);
+  end
+
+endmodule

src/verilog/verilog_elaborate.cpp

@@ -611,7 +611,10 @@ void verilog_typecheckt::collect_symbols(const verilog_lett &let)
 
 void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
 {
-  if(statement.id() == ID_verilog_immediate_assert)
+  if(
+    statement.id() == ID_verilog_immediate_assert ||
+    statement.id() == ID_verilog_immediate_assume ||
+    statement.id() == ID_verilog_immediate_cover)
   {
   }
   else if(

src/verilog/verilog_expr.h

@@ -1845,6 +1845,7 @@ inline const verilog_assume_statementt &
 to_verilog_assume_statement(const verilog_statementt &statement)
 {
   PRECONDITION(
+    statement.id() == ID_verilog_immediate_assume ||
     statement.id() == ID_verilog_assume_property ||
     statement.id() == ID_verilog_smv_assume);
   binary_exprt::check(statement);
@@ -1855,6 +1856,7 @@ inline verilog_assume_statementt &
 to_verilog_assume_statement(verilog_statementt &statement)
 {
   PRECONDITION(
+    statement.id() == ID_verilog_immediate_assume ||
     statement.id() == ID_verilog_assume_property ||
     statement.id() == ID_verilog_smv_assume);
   binary_exprt::check(statement);

src/verilog/verilog_synthesis.cpp

@@ -111,6 +111,26 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
 /*******************************************************************\
 
+Function: verilog_synthesist::value_mapt::guarded_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt verilog_synthesist::value_mapt::guarded_expr(exprt expr) const
+{
+  if(guard.empty())
+    return expr;
+  else
+    return implies_exprt{conjunction(guard), std::move(expr)};
+}
+
+/*******************************************************************\
+
 Function: verilog_synthesist::function_locality
 
   Inputs:
@@ -1838,11 +1858,17 @@ void verilog_synthesist::synth_assert_cover(
       // procedural concurrent -- evaluated just before the clock tick
       cond = synth_expr(statement.condition(), symbol_statet::SYMBOL);
     }
+
+    // add the guard
+    cond = guarded_expr(cond);
   }
   else // one of the 'always' variants
   {
     cond = synth_expr(statement.condition(), symbol_statet::CURRENT);
 
+    // add the guard
+    cond = guarded_expr(cond);
+
     // assertions have an implicit 'always'
     if(
       statement.id() != ID_verilog_cover_property &&
@@ -1923,6 +1949,9 @@ void verilog_synthesist::synth_assume(
 
   auto condition = synth_expr(statement.condition(), symbol_statet::CURRENT);
 
+  // add the guard
+  condition = guarded_expr(condition);
+
   // add it as an invariant
   invars.push_back(condition);
 }
@@ -2138,9 +2167,9 @@ Function: verilog_synthesist::synth_if
 void verilog_synthesist::synth_if(
   const verilog_ift &statement)
 {
-  auto if_operand = synth_expr(statement.cond(), symbol_statet::CURRENT);
+  auto if_cond = synth_expr(statement.cond(), symbol_statet::CURRENT);
 
-  if(if_operand.is_true())
+  if(if_cond.is_true())
   {
     synth_statement(statement.then_case());
     return;
@@ -2151,8 +2180,12 @@ void verilog_synthesist::synth_if(
 
   // produce new value maps
   value_mapt true_map(*value_map), false_map(*value_map);
+
   true_map.clear_changed();
+  true_map.guard.push_back(if_cond);
+
   false_map.clear_changed();
+  false_map.guard.push_back(not_exprt{if_cond});
 
   // 'then' case
   {
@@ -2171,10 +2204,11 @@ void verilog_synthesist::synth_if(
   value_map=old_map;
 
   // merge current map
-  merge(if_operand, true_map.current, false_map.current, false, value_map->current);
-  
+  merge(
+    if_cond, true_map.current, false_map.current, false, value_map->current);
+
   // merge final map
-  merge(if_operand, true_map.final, false_map.final, true, value_map->final);
+  merge(if_cond, true_map.final, false_map.final, true, value_map->final);
 }
 
 /*******************************************************************\
@@ -2643,6 +2677,7 @@ void verilog_synthesist::synth_statement(
     synth_assert_cover(to_verilog_assert_assume_cover_statement(statement));
   }
   else if(
+    statement.id() == ID_verilog_immediate_assume ||
     statement.id() == ID_verilog_assume_property ||
     statement.id() == ID_verilog_smv_assume)
   {

src/verilog/verilog_synthesis_class.h

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include "verilog_symbol_table.h"
 #include "verilog_typecheck_base.h"
 
-#include <cassert>
 #include <map>
 #include <set>
 #include <unordered_set>
@@ -166,22 +165,33 @@ class verilog_synthesist:
       current.changed.clear();
       final.changed.clear();
     }
+
+    // current guard
+    exprt::operandst guard;
+
+    exprt guarded_expr(exprt) const;
   };
 
   exprt current_value(
     const value_mapt::mapt &map,
     const symbolt &symbol,
     bool use_previous_assignments);
-  
+
+  exprt guarded_expr(exprt expr) const
+  {
+    PRECONDITION(value_map != NULL);
+    return value_map->guarded_expr(expr);
+  }
+
   inline exprt current_value(const symbolt &symbol)
   {
-    assert(value_map!=NULL);
+    PRECONDITION(value_map != NULL);
     return current_value(value_map->current, symbol, false);
   }
 
   inline exprt final_value(const symbolt &symbol)
   {
-    assert(value_map!=NULL);
+    PRECONDITION(value_map != NULL);
     return current_value(value_map->final, symbol, true);
   }
 

src/verilog/verilog_typecheck.cpp

@@ -1443,6 +1443,7 @@ void verilog_typecheckt::convert_statement(
     convert_assert_cover(to_verilog_assert_assume_cover_statement(statement));
   }
   else if(
+    statement.id() == ID_verilog_immediate_assume ||
     statement.id() == ID_verilog_assume_property ||
     statement.id() == ID_verilog_smv_assume)
   {