From 0a0837b26b22ebb00d2aa898230e2e9ce62fd5d9 Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Sun, 7 Mar 2021 18:31:05 -0700
Subject: [PATCH] liveness testing proof of concept with Super_Prove

---
 li.sby             | 15 +++++++++++++++
 liveness_example.v | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 li.sby
 create mode 100644 liveness_example.v

diff --git a/li.sby b/li.sby
new file mode 100644
index 0000000..0e2d262
--- /dev/null
+++ b/li.sby
@@ -0,0 +1,15 @@
+[options]
+mode live
+multiclock off
+
+[engines]
+aiger suprove
+
+[script]
+read -formal liveness_example.v
+prep -top top
+show -format dot -notitle
+
+
+[files]
+liveness_example.v
\ No newline at end of file
diff --git a/liveness_example.v b/liveness_example.v
new file mode 100644
index 0000000..68edd1f
--- /dev/null
+++ b/liveness_example.v
@@ -0,0 +1,41 @@
+`default_nettype none
+
+module top
+(
+    input wire clock,
+    output reg [3:0] egg,
+);
+    reg [3:0] counter = 1;
+    reg [7:0] bigcounter = 7'h3;
+    reg stop = 0;
+    always @ (posedge clock) begin
+
+
+        if (counter == 9)
+        begin
+            stop <= 1;
+        end
+        if (stop == 0)
+        begin
+            counter <= counter + 1;
+        end
+
+        egg <= counter;
+
+        //if (counter < 7) begin
+        assert property (s_eventually counter == 7);
+        //end
+
+
+        if (stop == 1) begin
+        bigcounter <= bigcounter - 1;
+        end
+
+        if (bigcounter == 0) begin
+        stop <= 0;
+        counter <= 0;
+        bigcounter <=7;
+        end
+
+    end // always @ (posedge clock)
+endmodule
-- 
GitLab