Merge pull request #510 from diffblue/stable-rose-fell-changed

SystemVerilog: $stable, $rose, $fell, $changed

Author: tautschnig

regression/verilog/system-functions/stable-rose-fell-changed1.desc

@@ -0,0 +1,7 @@
+CORE
+stable-rose-fell-changed1.sv
+--bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/stable-rose-fell-changed1.sv

@@ -0,0 +1,18 @@
+module main(input clk);
+
+  reg [31:0] counter = 0;
+
+  always @(posedge clk)
+    counter++;
+
+  initial p0: assert property ($stable(counter));
+  initial p1: assert property (!$rose(counter));
+  initial p2: assert property (!$fell(counter));
+  initial p3: assert property (!$changed(counter));
+
+  initial p4: assert property (##1 !$stable(counter));
+  initial p5: assert property (##1 $rose(counter));
+  initial p6: assert property (##1 !$fell(counter));
+  initial p7: assert property (##1 $changed(counter));
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -192,6 +192,31 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
                      : call.arguments()[1];
       return verilog_past_exprt{what, ticks}.with_source_location(call);
     }
+    else if(
+      identifier == "$stable" || identifier == "$rose" ||
+      identifier == "$fell" || identifier == "$changed")
+    {
+      DATA_INVARIANT(call.arguments().size() >= 1, "must have argument");
+      auto what = call.arguments()[0];
+      auto past = verilog_past_exprt{what, from_integer(1, integer_typet())}
+                    .with_source_location(call);
+
+      auto lsb = [](exprt expr) {
+        return extractbit_exprt{
+          std::move(expr), from_integer(0, integer_typet{})};
+      };
+
+      if(identifier == "$stable")
+        return equal_exprt{what, past};
+      else if(identifier == "$changed")
+        return notequal_exprt{what, past};
+      else if(identifier == "$rose")
+        return and_exprt{not_exprt{lsb(past)}, lsb(what)};
+      else if(identifier == "$fell")
+        return and_exprt{lsb(past), not_exprt{lsb(what)}};
+      else
+        DATA_INVARIANT(false, "all cases covered");
+    }
     else
     {
       // Attempt to constant fold.

src/verilog/verilog_typecheck_expr.cpp

@@ -676,6 +676,20 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
+  else if(
+    identifier == "$stable" || identifier == "$rose" || identifier == "$fell" ||
+    identifier == "$changed")
+  {
+    if(arguments.size() != 1 && arguments.size() != 2)
+    {
+      throw errort().with_location(expr.source_location())
+        << identifier << " takes one or two arguments";
+    }
+
+    expr.type() = bool_typet();
+
+    return std::move(expr);
+  }
   else
   {
     throw errort().with_location(expr.function().source_location())