Merge pull request #104 from nakengelhardt/more_tests

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 output_callback(line):
 
     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