diff --git a/tests/blackbox/Makefile b/tests/blackbox/Makefile new file mode 100644 index 0000000..c904ebe --- /dev/null +++ b/tests/blackbox/Makefile @@ -0,0 +1,2 @@ +SUBDIR=blackbox +include ../make/subdir.mk diff --git a/tests/unsorted/blackbox.sby b/tests/blackbox/blackbox.sby similarity index 73% rename from tests/unsorted/blackbox.sby rename to tests/blackbox/blackbox.sby index ca9400e..cf4951a 100644 --- a/tests/unsorted/blackbox.sby +++ b/tests/blackbox/blackbox.sby @@ -1,14 +1,15 @@ [options] mode bmc depth 1 -expect error +expect fail [engines] smtbmc [script] -read_verilog -formal test.v +read -formal test.v prep -top top +cutpoint -blackbox [file test.v] (* blackbox *) @@ -18,7 +19,8 @@ module submod(a, b); endmodule module top; - wire [7:0] a = $anyconst, b; + (*anyconst*) wire [7:0] a; + wire [7:0] b; submod submod( .a(a), diff --git a/tests/blackbox/parameter.sby b/tests/blackbox/parameter.sby new file mode 100644 index 0000000..d08bd47 --- /dev/null +++ b/tests/blackbox/parameter.sby @@ -0,0 +1,31 @@ +[options] +mode bmc +depth 1 +expect fail + +[engines] +smtbmc + +[script] +read -formal test.v +prep -top top +cutpoint -blackbox + +[file test.v] +(* blackbox *) +module submod #(parameter WIDTH = 24) (input [WIDTH-1:0] a, output [WIDTH-1:0] b); +endmodule + +module top; + (*anyconst *) wire [7:0] a; + wire [7:0] b; + + submod #(.WIDTH(8)) submod( + .a(a), + .b(b) + ); + + always @* begin + assert(~a == b); + end +endmodule diff --git a/tests/blackbox/unknown_cells.sby b/tests/blackbox/unknown_cells.sby new file mode 100644 index 0000000..d9189ae --- /dev/null +++ b/tests/blackbox/unknown_cells.sby @@ -0,0 +1,62 @@ +[options] +mode bmc +depth 1 +expect error + +[engines] +smtbmc + +[script] +read_rtlil test.il +cutpoint -blackbox + +[file test.il] +autoidx 31 +attribute \keep 1 +attribute \top 1 +attribute \library "work" +attribute \hdlname "top" +module \top + wire $auto$rtlil.cc:2739:Not$26 + wire $auto$rtlil.cc:2739:Not$28 + wire width 8 $verific$n12$4 + attribute \anyconst 1 + wire width 8 \a + wire width 8 \b + cell $assert $auto$verificsva.cc:1732:import$24 + connect \A $auto$rtlil.cc:2739:Not$28 + connect \EN $auto$rtlil.cc:2739:Not$26 + end + cell $not $auto$verificsva.cc:1745:import$25 + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \Y_WIDTH 1 + connect \A $auto$rtlil.cc:2739:Not$28 + connect \Y $auto$rtlil.cc:2739:Not$26 + end + cell $anyconst $verific$a$test.v:8$2 + parameter \WIDTH 8 + connect \Y \a + end + cell $eq $verific$equal_4$test.v:17$22 + parameter \A_SIGNED 0 + parameter \A_WIDTH 8 + parameter \B_SIGNED 0 + parameter \B_WIDTH 8 + parameter \Y_WIDTH 1 + connect \A $verific$n12$4 + connect \B \b + connect \Y $auto$rtlil.cc:2739:Not$28 + end + cell $not $verific$inv_3$test.v:17$21 + parameter \A_SIGNED 0 + parameter \A_WIDTH 8 + parameter \Y_WIDTH 8 + connect \A \a + connect \Y $verific$n12$4 + end + cell \submod \submod + connect \a \a + connect \b \b + end +end diff --git a/tests/blackbox/wider.sby b/tests/blackbox/wider.sby new file mode 100644 index 0000000..12510c1 --- /dev/null +++ b/tests/blackbox/wider.sby @@ -0,0 +1,72 @@ +[tasks] +parameter_signed_unsigned: parameter port_signed +parameter_signed_signed: parameter port_signed signal_signed +parameter_unsigned_signed: parameter signal_signed +parameter_unsigned_unsigned: parameter +signed_unsigned: port_signed +signed_signed: port_signed signal_signed +unsigned_signed: signal_signed +unsigned_unsigned: + +[options] +mode bmc +depth 1 +expect pass + +[engines] +smtbmc + +[script] +port_signed: read -define PORT_SIGNED +parameter: read -define PARAMETER +read -formal test.v +prep -top top +cutpoint -blackbox + +[file test.v] +`ifdef PARAMETER +`define DEF_PARAMETER #(parameter WIDTH = 24) +`define USE_PARAMETER #(.WIDTH(8)) +`define PORT_WIDTH WIDTH +`else +`define DEF_PARAMETER +`define USE_PARAMETER +`define PORT_WIDTH 8 +`endif + +`ifdef PORT_SIGNED +`define PORT_SIGNED_WORD signed +`else +`define PORT_SIGNED_WORD +`endif + +`ifdef SIGNAL_SIGNED +`define SIGNAL_SIGNED_WORD signed +`else +`define SIGNAL_SIGNED_WORD +`endif + + +(* blackbox *) +module submod `DEF_PARAMETER (a, b); + input [`PORT_WIDTH - 1:0] a; + output `PORT_SIGNED_WORD [`PORT_WIDTH - 1:0] b; +endmodule + +module top; + (*anyconst *) wire [7:0] a; + wire `SIGNAL_SIGNED_WORD [9:0] b; + + submod `USE_PARAMETER submod( + .a(a), + .b(b) + ); + + always @* begin +`ifdef PORT_SIGNED + assert(b[9] == b[7] && b[8] == b[7]); +`else + assert(b[9:8] == 0); +`endif + end +endmodule