From 3f32deb8c9a8deffeff339c5447464b4f80dea22 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 24 May 2022 17:51:48 -0700
Subject: [PATCH] add test for yosys's $divfloor and $modfloor cells

Depends on: https://github.com/YosysHQ/yosys/pull/3335
---
 tests/unsorted/floor_divmod.sby | 44 +++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 tests/unsorted/floor_divmod.sby

diff --git a/tests/unsorted/floor_divmod.sby b/tests/unsorted/floor_divmod.sby
new file mode 100644
index 0000000..53218cc
--- /dev/null
+++ b/tests/unsorted/floor_divmod.sby
@@ -0,0 +1,44 @@
+[options]
+mode bmc
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -icells -formal test.v
+prep -top top
+
+[file test.v]
+module top;
+	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
-- 
2.30.2