From b4c110815ce1d6017c5380a07dd7dcb23f7a304c Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 3 Jun 2022 16:48:21 +0200
Subject: [PATCH] Test designs using $allconst

---
 tests/unsorted/allconst.sby | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 tests/unsorted/allconst.sby

diff --git a/tests/unsorted/allconst.sby b/tests/unsorted/allconst.sby
new file mode 100644
index 0000000..0d43f12
--- /dev/null
+++ b/tests/unsorted/allconst.sby
@@ -0,0 +1,30 @@
+[tasks]
+yices
+z3
+
+[options]
+mode cover
+depth 1
+
+[engines]
+yices: smtbmc --stbv yices
+z3: smtbmc --stdt z3
+
+[script]
+read -noverific
+read -formal primegen.sv
+prep -top primegen
+
+[file primegen.sv]
+
+module primegen;
+	(* anyconst *) reg [9:0] prime;
+	(* allconst *) reg [4:0] factor;
+
+	always @* begin
+		if (1 < factor && factor < prime)
+			assume ((prime % factor) != 0);
+		assume (prime > 800);
+		cover (1);
+	end
+endmodule
-- 
2.30.2