add new blackbox test cases

tests/blackbox/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=blackbox
+include ../make/subdir.mk

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),

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

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

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