Refactor tests

Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.

See `cd tests; make help` for a description of supported make targets.

tests/unsorted/2props1trace.sby

@@ -0,0 +1,22 @@
+[options]
+mode bmc
+depth 1
+expect fail
+
+[engines]
+smtbmc
+
+[script]
+read -sv top.sv
+prep -top top
+
+[file top.sv]
+module top(
+input foo,
+input bar
+);
+always @(*) begin
+	assert (foo);
+	assert (bar);
+end
+endmodule

tests/unsorted/Makefile

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

tests/unsorted/both_ex.sby

@@ -0,0 +1,22 @@
+[tasks]
+btormc bmc
+pono bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 5
+expect pass
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+cover: btor btormc
+
+[script]
+read -sv both_ex.v
+prep -top test
+
+[files]
+both_ex.v

tests/unsorted/both_ex.v

@@ -0,0 +1,25 @@
+module test(
+  input clk,
+  input [7:0] data
+  );
+
+localparam MAX_COUNT = 8'd111;
+reg [7:0] count = 8'd0;
+reg [7:0] margin = MAX_COUNT;
+
+always @ (posedge clk) begin
+  if (data > margin) begin
+    count <= 8'd0;
+    margin <= MAX_COUNT;
+  end else begin
+    count <= count + data;
+    margin <= margin - data;
+  end
+
+  assume (data < 8'd40);
+  assert (count <= MAX_COUNT);
+  cover (count == 8'd42);
+  cover (count == 8'd111);
+end
+
+endmodule

tests/unsorted/cover.sby

@@ -0,0 +1,13 @@
+[options]
+mode cover
+expect pass
+
+[engines]
+btor btormc
+
+[script]
+read -formal cover.sv
+prep -top top
+
+[files]
+cover.sv

tests/unsorted/cover.sv

@@ -0,0 +1,17 @@
+module top (
+	input clk,
+	input [7:0] din
+);
+	reg [31:0] state = 0;
+
+	always @(posedge clk) begin
+		state <= ((state << 5) + state) ^ din;
+	end
+
+`ifdef FORMAL
+	always @(posedge clk) begin
+		cover (state == 'd 12345678);
+		cover (state == 'h 12345678);
+	end
+`endif
+endmodule

tests/unsorted/cover_fail.sby

@@ -0,0 +1,31 @@
+[options]
+mode cover
+depth 5
+expect pass,fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read -sv test.v
+prep -top test
+
+[file test.v]
+module test(
+input clk,
+input rst,
+output reg [3:0] count
+);
+
+initial assume (rst == 1'b1);
+
+always @(posedge clk) begin
+if (rst)
+  count <= 4'b0;
+else
+  count <= count + 1'b1;
+
+cover (count == 0 && !rst);
+cover (count == 4'd11 && !rst);
+end
+endmodule

tests/unsorted/demo.sby

@@ -0,0 +1,19 @@
+[tasks]
+btormc
+pono
+
+[options]
+mode bmc
+depth 100
+expect fail
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read -formal demo.sv
+prep -top demo
+
+[files]
+demo.sv

tests/unsorted/demo.sv

@@ -0,0 +1,19 @@
+module demo (
+  input clk,
+  output reg [5:0] counter
+);
+  initial counter = 0;
+
+  always @(posedge clk) begin
+    if (counter == 15)
+      counter <= 0;
+    else
+      counter <= counter + 1;
+  end
+
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (counter < 7);
+  end
+`endif
+endmodule

tests/unsorted/memory.sby

@@ -0,0 +1,19 @@
+[tasks]
+btormc
+pono
+
+[options]
+mode bmc
+depth 10
+expect fail
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read -formal memory.sv
+prep -top testbench
+
+[files]
+memory.sv

tests/unsorted/memory.sv

@@ -0,0 +1,60 @@
+module testbench (
+  input clk, wen,
+  input [9:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata
+);
+  memory uut (
+    .clk  (clk  ),
+    .wen  (wen  ),
+    .addr (addr ),
+    .wdata(wdata),
+    .rdata(rdata)
+  );
+
+  (* anyconst *) reg [9:0] test_addr;
+  reg test_data_valid = 0;
+  reg [7:0] test_data;
+
+  always @(posedge clk) begin
+    if (addr == test_addr) begin
+      if (wen) begin
+        test_data <= wdata;
+	test_data_valid <= 1;
+      end
+      if (test_data_valid) begin
+        assert(test_data == rdata);
+      end
+    end
+  end
+endmodule
+
+module memory (
+  input clk, wen,
+  input [9:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata
+);
+  reg [7:0] bank0 [0:255];
+  reg [7:0] bank1 [0:255];
+  reg [7:0] bank2 [0:255];
+  reg [7:0] bank3 [0:255];
+
+  wire [1:0] mem_sel = addr[9:8];
+  wire [7:0] mem_addr = addr[7:0];
+
+  always @(posedge clk) begin
+    case (mem_sel)
+      0: if (wen) bank0[mem_addr] <= wdata;
+      1: if (wen) bank1[mem_addr] <= wdata;
+      2: if (wen) bank1[mem_addr] <= wdata;  // BUG: Should assign to bank2
+      3: if (wen) bank3[mem_addr] <= wdata;
+    endcase
+  end
+
+  assign rdata =
+    mem_sel == 0 ? bank0[mem_addr] :
+    mem_sel == 1 ? bank1[mem_addr] :
+    mem_sel == 2 ? bank2[mem_addr] :
+    mem_sel == 3 ? bank3[mem_addr] : 'bx;
+endmodule

tests/unsorted/mixed.sby

@@ -0,0 +1,21 @@
+[tasks]
+cover
+btormc bmc
+pono bmc
+
+[options]
+cover: mode cover
+bmc: mode bmc
+bmc: depth 1
+
+[engines]
+cover: btor btormc
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read -formal mixed.v
+prep -top test
+
+[files]
+mixed.v

tests/unsorted/mixed.v

@@ -0,0 +1,17 @@
+module test (input CP, CN, CX, input A, B, output reg XP, XN, YP, YN);
+	always @* begin
+		assume (A || B);
+		assume (!A || !B);
+		assert (A != B);
+		cover (A);
+		cover (B);
+	end
+	always @(posedge CP)
+		XP <= A;
+	always @(negedge CN)
+		XN <= B;
+	always @(posedge CX)
+		YP <= A;
+	always @(negedge CX)
+		YN <= B;
+endmodule

tests/unsorted/multi_assert.sby

@@ -0,0 +1,24 @@
+[tasks]
+btormc
+pono
+
+[options]
+mode bmc
+depth 5
+expect fail
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read -sv multi_assert.v
+prep -top test
+
+[file multi_assert.v]
+module test();
+always @* begin
+assert (1);
+assert (0);
+end
+endmodule

tests/unsorted/preunsat.sby

@@ -0,0 +1,22 @@
+[tasks]
+btormc
+yices
+
+[options]
+mode bmc
+yices: expect error
+btormc: expect pass
+
+[engines]
+btormc: btor btormc
+yices: smtbmc yices
+
+[script]
+read -sv test.sv
+prep -top test
+
+[file test.sv]
+module test(input foo);
+always @* assume(0);
+always @* assert(foo);
+endmodule

tests/unsorted/prv32fmcmp.sby

@@ -0,0 +1,21 @@
+[tasks]
+btormc
+pono
+
+[options]
+mode bmc
+expect fail
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read -noverific
+read -sv picorv32.v
+read -sv prv32fmcmp.v
+prep -top prv32fmcmp
+
+[files]
+../../extern/picorv32.v
+prv32fmcmp.v

tests/unsorted/prv32fmcmp.v

@@ -0,0 +1,73 @@
+module prv32fmcmp (
+	input         clock,
+	input         resetn,
+	output        mem_valid_a, mem_valid_b,
+	output        mem_instr_a, mem_instr_b,
+	input         mem_ready_a, mem_ready_b,
+	output [31:0] mem_addr_a, mem_addr_b,
+	output [31:0] mem_wdata_a, mem_wdata_b,
+	output [ 3:0] mem_wstrb_a, mem_wstrb_b,
+	input  [31:0] mem_rdata_a, mem_rdata_b
+);
+	picorv32 #(
+		.REGS_INIT_ZERO(1),
+		.COMPRESSED_ISA(1)
+	) prv32_a (
+		.clk       (clock      ),
+		.resetn    (resetn     ),
+		.mem_valid (mem_valid_a),
+		.mem_instr (mem_instr_a),
+		.mem_ready (mem_ready_a),
+		.mem_addr  (mem_addr_a ),
+		.mem_wdata (mem_wdata_a),
+		.mem_wstrb (mem_wstrb_a),
+		.mem_rdata (mem_rdata_a)
+	);
+
+	picorv32 #(
+		.REGS_INIT_ZERO(1),
+		.COMPRESSED_ISA(1)
+	) prv32_b (
+		.clk       (clock      ),
+		.resetn    (resetn     ),
+		.mem_valid (mem_valid_b),
+		.mem_instr (mem_instr_b),
+		.mem_ready (mem_ready_b),
+		.mem_addr  (mem_addr_b ),
+		.mem_wdata (mem_wdata_b),
+		.mem_wstrb (mem_wstrb_b),
+		.mem_rdata (mem_rdata_b)
+	);
+
+	reg [31:0] rom [0:255];
+
+	integer mem_access_cnt_a = 0;
+	integer mem_access_cnt_b = 0;
+
+	always @* begin
+		assume(resetn == !$initstate);
+
+		if (resetn) begin
+			// only consider programs without data memory read/write
+			if (mem_valid_a) assume(mem_instr_a);
+			if (mem_valid_b) assume(mem_instr_b);
+
+			// when the access cnt matches, the addresses must match
+			if (mem_valid_a && mem_valid_b && mem_access_cnt_a == mem_access_cnt_b) begin
+				assert(mem_addr_a == mem_addr_b);
+			end
+
+			// hook up to memory
+			assume(mem_rdata_a == rom[mem_addr_a[9:2]]);
+			assume(mem_rdata_b == rom[mem_addr_b[9:2]]);
+		end
+
+		// it will pass when this is enabled
+		//assume(mem_ready_a == mem_ready_b);
+	end
+
+	always @(posedge clock) begin
+		mem_access_cnt_a <= mem_access_cnt_a + (resetn && mem_valid_a && mem_ready_a);
+		mem_access_cnt_b <= mem_access_cnt_b + (resetn && mem_valid_b && mem_ready_b);
+	end
+endmodule

tests/unsorted/redxor.sby

@@ -0,0 +1,13 @@
+[options]
+mode cover
+expect pass
+
+[engines]
+btor btormc
+
+[script]
+read -formal redxor.v
+prep -top test
+
+[files]
+redxor.v

tests/unsorted/redxor.v

@@ -0,0 +1,8 @@
+module test(input [7:0] I, output O);
+assign O = ^I;
+
+always @(*) begin
+cover(O==1'b0);
+cover(O==1'b1);
+end
+endmodule

tests/unsorted/stopfirst.sby

@@ -0,0 +1,16 @@
+[options]
+mode bmc
+expect fail
+
+[engines]
+btor btormc
+
+[script]
+read -sv test.sv
+prep -top test
+
+[file test.sv]
+module test(input foo);
+always @* assert(foo);
+always @* assert(!foo);
+endmodule

tests/unsorted/submod_props.sby

@@ -0,0 +1,33 @@
+[tasks]
+bmc
+cover
+flatten
+
+[options]
+bmc: mode bmc
+cover: mode cover
+flatten: mode bmc
+
+expect fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read -sv test.sv
+prep -top top
+flatten: flatten
+
+[file test.sv]
+module test(input foo);
+always @* assert(foo);
+always @* assert(!foo);
+always @* cover(foo);
+always @* cover(!foo);
+endmodule
+
+module top();
+test test_i (
+.foo(1'b1)
+);
+endmodule