From cd57c5adb39d2343e81ed1024cb2848983bfede2 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 2 Jun 2022 22:37:29 -0700 Subject: smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions --- tests/various/smtlib2_module.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/various/smtlib2_module.v (limited to 'tests/various/smtlib2_module.v') diff --git a/tests/various/smtlib2_module.v b/tests/various/smtlib2_module.v new file mode 100644 index 000000000..4aad86905 --- /dev/null +++ b/tests/various/smtlib2_module.v @@ -0,0 +1,33 @@ +(* smtlib2_module *) +module smtlib2(a, b, add, sub, eq); + input [7:0] a, b; + (* smtlib2_comb_expr = "(bvadd a b)" *) + output [7:0] add; + (* smtlib2_comb_expr = "(bvadd a (bvneg b))" *) + output [7:0] sub; + (* smtlib2_comb_expr = "(= a b)" *) + output eq; +endmodule + +(* top *) +module uut; + wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2; + wire eq; + + assign add2 = a + b; + assign sub2 = a - b; + + smtlib2 s ( + .a(a), + .b(b), + .add(add), + .sub(sub), + .eq(eq) + ); + + always @* begin + assert(add == add2); + assert(sub == sub2); + assert(eq == (a == b)); + end +endmodule -- cgit v1.2.3