Added smtbmc axicheck2, improved axicheck

6 files changed, 207 insertions, 20 deletions

diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore
index 39f1e56..5d927c4 100644
--- a/scripts/smtbmc/.gitignore
+++ b/scripts/smtbmc/.gitignore
@@ -4,6 +4,8 @@ tracecmp2.smt2
 tracecmp2.yslog
 axicheck.smt2
 axicheck.yslog
+axicheck2.smt2
+axicheck2.yslog
 notrap_validop.smt2
 notrap_validop.yslog
 mulcmp.smt2
diff --git a/scripts/smtbmc/axicheck.sh b/scripts/smtbmc/axicheck.sh
index 55c2b05..732b3b8 100644
--- a/scripts/smtbmc/axicheck.sh
+++ b/scripts/smtbmc/axicheck.sh
@@ -8,5 +8,6 @@ yosys -ql axicheck.yslog \
 	-p 'prep -top testbench -nordff' \
 	-p 'write_smt2 -wires axicheck.smt2'
 
-yosys-smtbmc -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2
+yosys-smtbmc -t 50 -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2
+# yosys-smtbmc -t 50 -i -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2
 
diff --git a/scripts/smtbmc/axicheck.v b/scripts/smtbmc/axicheck.v
index 0afe41b..80eda48 100644
--- a/scripts/smtbmc/axicheck.v
+++ b/scripts/smtbmc/axicheck.v
@@ -34,8 +34,7 @@ module testbench (
 		.ENABLE_COUNTERS64(1),
 		.ENABLE_REGS_16_31(1),
 		.ENABLE_REGS_DUALPORT(1),
-		.TWO_STAGE_SHIFT(1),
-		.BARREL_SHIFTER(0),
+		.BARREL_SHIFTER(1),
 		.TWO_CYCLE_COMPARE(0),
 		.TWO_CYCLE_ALU(0),
 		.COMPRESSED_ISA(0),
@@ -64,26 +63,50 @@ module testbench (
 		.mem_axi_rdata   (mem_axi_rdata  )
 	);
 
-	reg expect_bvalid_0 = 0;
-	reg expect_bvalid_1 = 0;
-	reg expect_rvalid = 0;
+	reg expect_bvalid_aw = 0;
+	reg expect_bvalid_w  = 0;
+	reg expect_rvalid    = 0;
+
+	reg [3:0] timeout_aw = 0;
+	reg [3:0] timeout_w  = 0;
+	reg [3:0] timeout_b  = 0;
+	reg [3:0] timeout_ar = 0;
+	reg [3:0] timeout_r  = 0;
+	reg [3:0] timeout_ex = 0;
+
+	always @(posedge clk) begin
+		timeout_aw <= !mem_axi_awvalid || mem_axi_awready ? 0 : timeout_aw + 1;
+		timeout_w  <= !mem_axi_wvalid  || mem_axi_wready  ? 0 : timeout_w  + 1;
+		timeout_b  <= !mem_axi_bvalid  || mem_axi_bready  ? 0 : timeout_b  + 1;
+		timeout_ar <= !mem_axi_arvalid || mem_axi_arready ? 0 : timeout_ar + 1;
+		timeout_r  <= !mem_axi_rvalid  || mem_axi_rready  ? 0 : timeout_r  + 1;
+		timeout_ex <= !{expect_bvalid_aw, expect_bvalid_w, expect_rvalid} ? 0 : timeout_ex + 1;
+		restrict(timeout_aw != 15);
+		restrict(timeout_w  != 15);
+		restrict(timeout_b  != 15);
+		restrict(timeout_ar != 15);
+		restrict(timeout_r  != 15);
+		restrict(timeout_ex != 15);
+		restrict(!trap);
+
+	end
 
 	always @(posedge clk) begin
 		if (resetn) begin
 			if (!$past(resetn)) begin
 				assert(!mem_axi_awvalid);
-				assert(!mem_axi_wvalid);
-				assume(!mem_axi_bvalid);
+				assert(!mem_axi_wvalid );
+				assume(!mem_axi_bvalid );
 				assert(!mem_axi_arvalid);
-				assume(!mem_axi_rvalid);
+				assume(!mem_axi_rvalid );
 			end else begin
 				// Only one read/write transaction in flight at each point in time
 
-				if (expect_bvalid_0) begin
+				if (expect_bvalid_aw) begin
 					assert(!mem_axi_awvalid);
 				end
 
-				if (expect_bvalid_1) begin
+				if (expect_bvalid_w) begin
 					assert(!mem_axi_wvalid);
 				end
 
@@ -91,20 +114,20 @@ module testbench (
 					assert(!mem_axi_arvalid);
 				end
 
-				expect_bvalid_0 = expect_bvalid_0 || (mem_axi_awvalid && mem_axi_awready);
-				expect_bvalid_1 = expect_bvalid_1 || (mem_axi_wvalid && mem_axi_wready);
-				expect_rvalid = expect_rvalid || (mem_axi_arvalid && mem_axi_arready);
+				expect_bvalid_aw = expect_bvalid_aw || (mem_axi_awvalid && mem_axi_awready);
+				expect_bvalid_w  = expect_bvalid_w  || (mem_axi_wvalid  && mem_axi_wready );
+				expect_rvalid    = expect_rvalid    || (mem_axi_arvalid && mem_axi_arready);
 
-				if (expect_bvalid_0 || expect_bvalid_1) begin
+				if (expect_bvalid_aw || expect_bvalid_w) begin
 					assert(!expect_rvalid);
 				end
 
 				if (expect_rvalid) begin
-					assert(!expect_bvalid_0);
-					assert(!expect_bvalid_1);
+					assert(!expect_bvalid_aw);
+					assert(!expect_bvalid_w);
 				end
 
-				if (!expect_bvalid_0 || !expect_bvalid_1) begin
+				if (!expect_bvalid_aw || !expect_bvalid_w) begin
 					assume(!mem_axi_bvalid);
 				end
 
@@ -113,8 +136,8 @@ module testbench (
 				end
 
 				if (mem_axi_bvalid && mem_axi_bready) begin
-					expect_bvalid_0 = 0;
-					expect_bvalid_1 = 0;
+					expect_bvalid_aw = 0;
+					expect_bvalid_w = 0;
 				end
 
 				if (mem_axi_rvalid && mem_axi_rready) begin
diff --git a/scripts/smtbmc/axicheck2.sh b/scripts/smtbmc/axicheck2.sh
new file mode 100644
index 0000000..df20855
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql axicheck2.yslog \
+	-p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+	-p 'read_verilog -formal axicheck2.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -wires axicheck2.smt2'
+
+yosys-smtbmc -t 6 -s yices --dump-vcd output.vcd --dump-smtc output.smtc --smtc axicheck2.smtc axicheck2.smt2
+
diff --git a/scripts/smtbmc/axicheck2.smtc b/scripts/smtbmc/axicheck2.smtc
new file mode 100644
index 0000000..1f8c5ea
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.smtc
@@ -0,0 +1,2 @@
+initial
+assume (= [uut_0] [uut_1])
diff --git a/scripts/smtbmc/axicheck2.v b/scripts/smtbmc/axicheck2.v
new file mode 100644
index 0000000..3d24a2e
--- /dev/null
+++ b/scripts/smtbmc/axicheck2.v
@@ -0,0 +1,147 @@
+module testbench (
+	input         clk,
+	input         resetn,
+	output        trap_0,
+	output        trap_1,
+
+	output        mem_axi_awvalid_0,
+	input         mem_axi_awready_0,
+	output [31:0] mem_axi_awaddr_0,
+	output [ 2:0] mem_axi_awprot_0,
+
+	output        mem_axi_awvalid_1,
+	input         mem_axi_awready_1,
+	output [31:0] mem_axi_awaddr_1,
+	output [ 2:0] mem_axi_awprot_1,
+
+	output        mem_axi_wvalid_0,
+	input         mem_axi_wready_0,
+	output [31:0] mem_axi_wdata_0,
+	output [ 3:0] mem_axi_wstrb_0,
+
+	output        mem_axi_wvalid_1,
+	input         mem_axi_wready_1,
+	output [31:0] mem_axi_wdata_1,
+	output [ 3:0] mem_axi_wstrb_1,
+
+	input         mem_axi_bvalid,
+	output        mem_axi_bready_0,
+	output        mem_axi_bready_1,
+
+	output        mem_axi_arvalid_0,
+	input         mem_axi_arready_0,
+	output [31:0] mem_axi_araddr_0,
+	output [ 2:0] mem_axi_arprot_0,
+
+	output        mem_axi_arvalid_1,
+	input         mem_axi_arready_1,
+	output [31:0] mem_axi_araddr_1,
+	output [ 2:0] mem_axi_arprot_1,
+
+	input         mem_axi_rvalid,
+	output        mem_axi_rready_0,
+	output        mem_axi_rready_1,
+	input  [31:0] mem_axi_rdata
+);
+	picorv32_axi #(
+		.ENABLE_COUNTERS(1),
+		.ENABLE_COUNTERS64(1),
+		.ENABLE_REGS_16_31(1),
+		.ENABLE_REGS_DUALPORT(1),
+		.BARREL_SHIFTER(1),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.CATCH_MISALIGN(1),
+		.CATCH_ILLINSN(1)
+	) uut_0 (
+		.clk             (clk              ),
+		.resetn          (resetn           ),
+		.trap            (trap_0           ),
+		.mem_axi_awvalid (mem_axi_awvalid_0),
+		.mem_axi_awready (mem_axi_awready_0),
+		.mem_axi_awaddr  (mem_axi_awaddr_0 ),
+		.mem_axi_awprot  (mem_axi_awprot_0 ),
+		.mem_axi_wvalid  (mem_axi_wvalid_0 ),
+		.mem_axi_wready  (mem_axi_wready_0 ),
+		.mem_axi_wdata   (mem_axi_wdata_0  ),
+		.mem_axi_wstrb   (mem_axi_wstrb_0  ),
+		.mem_axi_bvalid  (mem_axi_bvalid   ),
+		.mem_axi_bready  (mem_axi_bready_0 ),
+		.mem_axi_arvalid (mem_axi_arvalid_0),
+		.mem_axi_arready (mem_axi_arready_0),
+		.mem_axi_araddr  (mem_axi_araddr_0 ),
+		.mem_axi_arprot  (mem_axi_arprot_0 ),
+		.mem_axi_rvalid  (mem_axi_rvalid   ),
+		.mem_axi_rready  (mem_axi_rready_0 ),
+		.mem_axi_rdata   (mem_axi_rdata    )
+	);
+
+	picorv32_axi #(
+		.ENABLE_COUNTERS(1),
+		.ENABLE_COUNTERS64(1),
+		.ENABLE_REGS_16_31(1),
+		.ENABLE_REGS_DUALPORT(1),
+		.BARREL_SHIFTER(1),
+		.TWO_CYCLE_COMPARE(0),
+		.TWO_CYCLE_ALU(0),
+		.COMPRESSED_ISA(0),
+		.CATCH_MISALIGN(1),
+		.CATCH_ILLINSN(1)
+	) uut_1 (
+		.clk             (clk              ),
+		.resetn          (resetn           ),
+		.trap            (trap_1           ),
+		.mem_axi_awvalid (mem_axi_awvalid_1),
+		.mem_axi_awready (mem_axi_awready_1),
+		.mem_axi_awaddr  (mem_axi_awaddr_1 ),
+		.mem_axi_awprot  (mem_axi_awprot_1 ),
+		.mem_axi_wvalid  (mem_axi_wvalid_1 ),
+		.mem_axi_wready  (mem_axi_wready_1 ),
+		.mem_axi_wdata   (mem_axi_wdata_1  ),
+		.mem_axi_wstrb   (mem_axi_wstrb_1  ),
+		.mem_axi_bvalid  (mem_axi_bvalid   ),
+		.mem_axi_bready  (mem_axi_bready_1 ),
+		.mem_axi_arvalid (mem_axi_arvalid_1),
+		.mem_axi_arready (mem_axi_arready_1),
+		.mem_axi_araddr  (mem_axi_araddr_1 ),
+		.mem_axi_arprot  (mem_axi_arprot_1 ),
+		.mem_axi_rvalid  (mem_axi_rvalid   ),
+		.mem_axi_rready  (mem_axi_rready_1 ),
+		.mem_axi_rdata   (mem_axi_rdata    )
+	);
+
+	always @(posedge clk) begin
+		if (resetn && $past(resetn)) begin
+			assert(trap_0            == trap_1           );
+			assert(mem_axi_awvalid_0 == mem_axi_awvalid_1);
+			assert(mem_axi_awaddr_0  == mem_axi_awaddr_1 );
+			assert(mem_axi_awprot_0  == mem_axi_awprot_1 );
+			assert(mem_axi_wvalid_0  == mem_axi_wvalid_1 );
+			assert(mem_axi_wdata_0   == mem_axi_wdata_1  );
+			assert(mem_axi_wstrb_0   == mem_axi_wstrb_1  );
+			assert(mem_axi_bready_0  == mem_axi_bready_1 );
+			assert(mem_axi_arvalid_0 == mem_axi_arvalid_1);
+			assert(mem_axi_araddr_0  == mem_axi_araddr_1 );
+			assert(mem_axi_arprot_0  == mem_axi_arprot_1 );
+			assert(mem_axi_rready_0  == mem_axi_rready_1 );
+
+			if (mem_axi_awvalid_0) assume(mem_axi_awready_0 == mem_axi_awready_1);
+			if (mem_axi_wvalid_0 ) assume(mem_axi_wready_0  == mem_axi_wready_1 );
+			if (mem_axi_arvalid_0) assume(mem_axi_arready_0 == mem_axi_arready_1);
+
+			if ($fell(mem_axi_awready_0)) assume($past(mem_axi_awvalid_0));
+			if ($fell(mem_axi_wready_0 )) assume($past(mem_axi_wvalid_0 ));
+			if ($fell(mem_axi_arready_0)) assume($past(mem_axi_arvalid_0));
+
+			if ($fell(mem_axi_awready_1)) assume($past(mem_axi_awvalid_1));
+			if ($fell(mem_axi_wready_1 )) assume($past(mem_axi_wvalid_1 ));
+			if ($fell(mem_axi_arready_1)) assume($past(mem_axi_arvalid_1));
+
+			if ($fell(mem_axi_bvalid)) assume($past(mem_axi_bready_0));
+			if ($fell(mem_axi_rvalid)) assume($past(mem_axi_rready_0));
+
+			if (mem_axi_rvalid && $past(mem_axi_rvalid)) assume($stable(mem_axi_rdata));
+		end
+	end
+endmodule