From b1d9bcbb42bd4851e64f5062e8aca807c9a08d71 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 8 Jul 2025 15:44:02 +1200
Subject: [PATCH] tests: Add statusdb test

Ensures that `--statusreset` doesn't break the schema.
---
 tests/statusdb/reset.sby | 14 ++++++++++++++
 tests/statusdb/reset.sh  | 11 +++++++++++
 tests/statusdb/reset.sv  | 21 +++++++++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 tests/statusdb/reset.sby
 create mode 100644 tests/statusdb/reset.sh
 create mode 100644 tests/statusdb/reset.sv

diff --git a/tests/statusdb/reset.sby b/tests/statusdb/reset.sby
new file mode 100644
index 0000000..aaf03c4
--- /dev/null
+++ b/tests/statusdb/reset.sby
@@ -0,0 +1,14 @@
+[options]
+mode bmc
+depth 100
+expect fail
+
+[engines]
+smtbmc --keep-going boolector
+
+[script]
+read -formal reset.sv
+prep -top demo
+
+[files]
+reset.sv
diff --git a/tests/statusdb/reset.sh b/tests/statusdb/reset.sh
new file mode 100644
index 0000000..3030056
--- /dev/null
+++ b/tests/statusdb/reset.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+set -e
+
+# run task
+python3 $SBY_MAIN -f $SBY_FILE $TASK
+# task has 3 properties
+python3 $SBY_MAIN -f $SBY_FILE --status | wc -l | grep -q '3'
+# resetting task should work
+python3 $SBY_MAIN -f $SBY_FILE --statusreset
+# clean database should have no properties
+python3 $SBY_MAIN -f $SBY_FILE --status | wc -l | grep -q '0'
diff --git a/tests/statusdb/reset.sv b/tests/statusdb/reset.sv
new file mode 100644
index 0000000..4514a9d
--- /dev/null
+++ b/tests/statusdb/reset.sv
@@ -0,0 +1,21 @@
+module demo (
+  input clk,
+  output reg [5:0] counter
+);
+  initial counter = 0;
+
+  always @(posedge clk) begin
+    if (counter == 15)
+      counter <= 0;
+    else
+      counter <= counter + 1;
+  end
+
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (1);
+    assert (counter < 7);
+    assert (0);
+  end
+`endif
+endmodule