colin
/
picorv32
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Added smtbmc axicheck2, improved axicheck

This commit is contained in:
Clifford Wolf 2016-10-01 17:08:19 +02:00
parent a6f5bc4f05
commit 51b1a88333
6 changed files with 207 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
scripts/smtbmc/.gitignore vendored
View File

@ -4,6 +4,8 @@ tracecmp2.smt2
tracecmp2.yslog
axicheck.smt2
axicheck.yslog
axicheck2.smt2
axicheck2.yslog
notrap_validop.smt2
notrap_validop.yslog
mulcmp.smt2

3
scripts/smtbmc/axicheck.sh
View File

@ -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

61
scripts/smtbmc/axicheck.v
View File

@ -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

12
scripts/smtbmc/axicheck2.sh Normal file
View File

@ -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

2
scripts/smtbmc/axicheck2.smtc Normal file
View File

@ -0,0 +1,2 @@
initial
assume (= [uut_0] [uut_1])

147
scripts/smtbmc/axicheck2.v Normal file
View File

@ -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