From f39f9c4b4b4fa416bd0db9ba7db6f8ba6bfc0e6b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 18 May 2024 09:32:47 +0100
Subject: [PATCH] SystemVerilog: $stable, $rose, $fell, $changed

This adds $stable, $rose, $fell, $changed to the SystemVerilog frontend.
---
 .../stable-rose-fell-changed1.desc            |  7 ++++++
 .../stable-rose-fell-changed1.sv              | 18 +++++++++++++
 src/verilog/verilog_synthesis.cpp             | 25 +++++++++++++++++++
 src/verilog/verilog_typecheck_expr.cpp        | 14 +++++++++++
 4 files changed, 64 insertions(+)
 create mode 100644 regression/verilog/system-functions/stable-rose-fell-changed1.desc
 create mode 100644 regression/verilog/system-functions/stable-rose-fell-changed1.sv

diff --git a/regression/verilog/system-functions/stable-rose-fell-changed1.desc b/regression/verilog/system-functions/stable-rose-fell-changed1.desc
new file mode 100644
index 000000000..8b64f07d2
--- /dev/null
+++ b/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
diff --git a/regression/verilog/system-functions/stable-rose-fell-changed1.sv b/regression/verilog/system-functions/stable-rose-fell-changed1.sv
new file mode 100644
index 000000000..4df31fa6c
--- /dev/null
+++ b/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
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index c80f0c857..b24401bab 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/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.
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index c270f7bc3..58f46515b 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/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())