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 (executable)
index 0000000..6303e02
--- /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 (file)
index 0000000..d23a523
--- /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