From: Jannis Harder <me@jix.one>
Date: Fri, 3 Jun 2022 14:48:21 +0000 (+0200)
Subject: Test designs using $allconst
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4c110815ce1d6017c5380a07dd7dcb23f7a304c;p=SymbiYosys.git

Test designs using $allconst
---

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