From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 24 May 2022 08:35:37 +0000 (-0700)
Subject: add test for $divfloor and $modfloor with write_smt2
X-Git-Tag: divfloor-in-write_smt2-old-test
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e5e9efbdb8a6043be5b3f79bfb7b2b08d828382;p=yosys.git

add test for $divfloor and $modfloor with write_smt2
---

diff --git a/tests/various/floor_divmod.sh b/tests/various/floor_divmod.sh
new file mode 100755
index 000000000..6303e025b
--- /dev/null
+++ b/tests/various/floor_divmod.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+set -ex
+../../yosys -q -p 'read_verilog -icells -formal floor_divmod.v; prep; write_smt2 -wires floor_divmod.smt2'
+../../yosys-smtbmc --unroll --dump-vcd floor_divmod.vcd floor_divmod.smt2
diff --git a/tests/various/floor_divmod.v b/tests/various/floor_divmod.v
new file mode 100644
index 000000000..d23a5237e
--- /dev/null
+++ b/tests/various/floor_divmod.v
@@ -0,0 +1,33 @@
+module uut;
+	wire [7:0] a = $anyconst, b = $anyconst, fdiv, fmod, a2;
+	assign a2 = b * fdiv + fmod;
+
+	\$divfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fdiv_m (
+		.A(a),
+		.B(b),
+		.Y(fdiv)
+	);
+
+	\$modfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fmod_m (
+		.A(a),
+		.B(b),
+		.Y(fmod)
+	);
+
+	always @* begin
+		assume(b != 0);
+		assert(a == a2);
+	end
+endmodule