add tests directory with additional tests

Makefile

@@ -44,7 +44,8 @@ test: \
   test_multiclk_dpmem \
   test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
   test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
-  test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory
+  test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \
+  run_tests
 
 test_demo1:
 	cd sbysrc && python3 sby.py -f demo1.sby
@@ -103,10 +104,12 @@ test_quickstart_prove:
 test_quickstart_memory:
 	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
 
+run_tests:
+	make -C tests test
+
 html:
 	make -C docs html
 
 clean:
 	make -C docs clean
 	rm -rf docs/build sbysrc/sby sbysrc/__pycache__
-

sbysrc/sby_engine_btor.py

@@ -190,7 +190,7 @@ def run(mode, job, engine_idx, engine):
 
     def exit_callback(retcode):
         if solver_args[0] == "pono":
-            assert retcode in [1, 2]
+            assert retcode in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
         else:
             assert retcode == 0
         if common_state.expected_cex != 0:

tests/.gitignore

@@ -0,0 +1,9 @@
+/both_ex*/
+/cover*/
+/demo*/
+/memory*/
+/mixed*/
+/preunsat*/
+/prv32fmcmp*/
+/redxor*/
+/stopfirst*/

tests/Makefile

@@ -0,0 +1,9 @@
+SBY_FILES=$(wildcard *.sby)
+SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=))
+
+.PHONY: test $(SBY_TESTS)
+
+test: $(SBY_TESTS)
+
+test_%: %.sby
+	python3 ../sbysrc/sby.py -f $<

tests/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_verilog -sv both_ex.v
+prep -top test
+
+[files]
+both_ex.v

tests/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/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/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/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/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/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/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/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/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/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_verilog -sv test.sv
+prep -top test
+
+[file test.sv]
+module test(input foo);
+always @* assume(0);
+always @* assert(foo);
+endmodule

tests/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]
+picorv32.v
+prv32fmcmp.v

tests/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/redxor.sby

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

tests/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/stopfirst.sby

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