Merge pull request #493 from diffblue/verilog_past

SystemVerilog: $past

Author: tautschnig

regression/verilog/system-functions/past1.desc

@@ -0,0 +1,7 @@
+CORE
+past1.sv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/past1.sv

@@ -0,0 +1,20 @@
+module main(input clk);
+
+  reg [31:0] counter = 0;
+
+  always @(posedge clk)
+    counter++;
+
+  initial p0: assert property (##0 $past(counter, 0) == 0);
+  initial p1: assert property (##1 $past(counter, 1) == 0);
+  initial p2: assert property (##2 $past(counter, 2) == 0);
+  initial p3: assert property (##3 $past(counter, 3) == 0);
+  initial p4: assert property (##4 $past(counter, 4) == 0);
+
+  initial q0: assert property (##0 $past(counter, 1) == 0);
+  initial q1: assert property (##1 $past(counter, 1) == 0);
+  initial q2: assert property (##2 $past(counter, 1) == 1);
+  initial q3: assert property (##3 $past(counter, 1) == 2);
+  initial q4: assert property (##4 $past(counter, 1) == 3);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -49,6 +49,7 @@ IREP_ID_ONE(verilog_priority)
 IREP_ID_ONE(verilog_non_indexed_part_select)
 IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
+IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(chandle)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)

src/trans-word-level/instantiate_word_level.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
+#include <verilog/verilog_expr.h>
 
 #include "property.h"
 
@@ -91,6 +92,27 @@ class wl_instantiatet
 
 /*******************************************************************\
 
+Function: default_value
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt default_value(const typet &type)
+{
+  auto zero = from_integer(0, type);
+  if(zero.is_nil())
+    throw "failed to create $past default value";
+  else
+    return std::move(zero);
+}
+
+/*******************************************************************\
+
 Function: wl_instantiatet::instantiate_rec
 
   Inputs:
@@ -303,6 +325,24 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 
     return instantiate_rec(tmp, t);
   }
+  else if(expr.id() == ID_verilog_past)
+  {
+    auto &verilog_past = to_verilog_past_expr(expr);
+
+    mp_integer ticks;
+    if(to_integer_non_constant(verilog_past.ticks(), ticks))
+      throw "failed to convert $past number of ticks";
+
+    if(ticks > t)
+    {
+      // return the 'default value' for the type
+      return default_value(verilog_past.type());
+    }
+    else
+    {
+      return instantiate_rec(verilog_past.what(), t - ticks);
+    }
+  }
   else
   {
     for(auto &op : expr.operands())

src/verilog/expr2verilog.cpp

@@ -1061,7 +1061,10 @@ std::string expr2verilogt::convert(
 
   else if(src.id()==ID_constraint_select_one)
     return convert_function("$ND", src);
-    
+
+  else if(src.id() == ID_verilog_past)
+    return convert_function("$past", src);
+
   else if(src.id()==ID_onehot)
     return convert_function("$onehot", src);
 

src/verilog/verilog_expr.h

@@ -1946,4 +1946,47 @@ to_verilog_implicit_typecast_expr(exprt &expr)
   return static_cast<verilog_implicit_typecast_exprt &>(expr);
 }
 
+class verilog_past_exprt : public binary_exprt
+{
+public:
+  verilog_past_exprt(exprt __what, exprt __ticks)
+    : binary_exprt(__what, ID_verilog_past, std::move(__ticks), __what.type())
+  {
+  }
+
+  const exprt &what() const
+  {
+    return op0();
+  }
+
+  exprt &what()
+  {
+    return op0();
+  }
+
+  const exprt &ticks() const
+  {
+    return op1();
+  }
+
+  exprt &ticks()
+  {
+    return op1();
+  }
+};
+
+inline const verilog_past_exprt &to_verilog_past_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_past);
+  verilog_past_exprt::check(expr);
+  return static_cast<const verilog_past_exprt &>(expr);
+}
+
+inline verilog_past_exprt &to_verilog_past_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_past);
+  verilog_past_exprt::check(expr);
+  return static_cast<verilog_past_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_synthesis.cpp

@@ -184,6 +184,14 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
       select_one.set(ID_identifier, identifier);
       return select_one.with_source_location(call);
     }
+    else if(identifier == "$past")
+    {
+      auto what = call.arguments()[0];
+      auto ticks = call.arguments().size() < 2
+                     ? from_integer(1, integer_typet())
+                     : call.arguments()[1];
+      return verilog_past_exprt{what, ticks}.with_source_location(call);
+    }
     else
     {
       // Attempt to constant fold.

src/verilog/verilog_typecheck_expr.cpp

@@ -653,6 +653,29 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
+  else if(identifier == "$past")
+  {
+    if(arguments.size() == 0 || arguments.size() >= 4)
+    {
+      throw errort().with_location(expr.source_location())
+        << "$past takes one to four arguments";
+    }
+
+    if(arguments.size() >= 2)
+    {
+      auto tmp = elaborate_constant_expression(arguments[1]);
+      if(!tmp.is_constant())
+      {
+        throw errort().with_location(arguments[1].source_location())
+          << "expected elaboration-time constant, but got `" << to_string(tmp)
+          << '\'';
+      }
+    }
+
+    expr.type() = arguments.front().type();
+
+    return std::move(expr);
+  }
   else
   {
     throw errort().with_location(expr.function().source_location())