mirror of https://github.com/YosysHQ/picorv32.git
Added next gen yosys-smtbmc verification scripts
This commit is contained in:
Clifford Wolf
parent
98d248d2c2
commit
d1d3c3c5e1
|
|
@ -1145,6 +1145,9 @@ module picorv32 #(
|
|||
if (ENABLE_COUNTERS) begin
|
||||
count_cycle <= resetn ? count_cycle + 1 : 0;
|
||||
if (!ENABLE_COUNTERS64) count_cycle[63:32] <= 0;
|
||||
end else begin
|
||||
count_cycle <= 'bx;
|
||||
count_instr <= 'bx;
|
||||
end
|
||||
|
||||
next_irq_pending = ENABLE_IRQ ? irq_pending & LATCHED_IRQ : 'bx;
|
||||
|
|
@ -1667,11 +1670,11 @@ module picorv32 #(
|
|||
reg [4:0] last_mem_ready;
|
||||
always @(posedge clk)
|
||||
last_mem_ready <= {last_mem_ready, mem_ready};
|
||||
assume property (|last_mem_ready);
|
||||
restrict property (|last_mem_ready);
|
||||
|
||||
reg ok;
|
||||
always @* begin
|
||||
assume (resetn == |cycle);
|
||||
restrict (resetn == |cycle);
|
||||
if (cycle) begin
|
||||
// instruction fetches are read-only
|
||||
if (mem_valid && mem_instr)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,3 @@
|
|||
tracecmp.smt2
|
||||
tracecmp.vcd
|
||||
tracecmp.yslog
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
[*]
|
||||
[*] GTKWave Analyzer v3.3.65 (w)1999-2015 BSI
|
||||
[*] Fri Aug 26 15:42:37 2016
|
||||
[*]
|
||||
[dumpfile] "/home/clifford/Work/picorv32/scripts/smtbmc/tracecmp.vcd"
|
||||
[dumpfile_mtime] "Fri Aug 26 15:33:18 2016"
|
||||
[dumpfile_size] 80106
|
||||
[savefile] "/home/clifford/Work/picorv32/scripts/smtbmc/tracecmp.gtkw"
|
||||
[timestart] 0
|
||||
[size] 1216 863
|
||||
[pos] -1 -1
|
||||
*-2.860312 10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
|
||||
[treeopen] testbench.
|
||||
[sst_width] 241
|
||||
[signals_width] 337
|
||||
[sst_expanded] 1
|
||||
[sst_vpaned_height] 252
|
||||
@28
|
||||
smt_clock
|
||||
testbench.resetn
|
||||
testbench.trap_0
|
||||
testbench.trap_1
|
||||
@200
|
||||
-
|
||||
-Trace CMP
|
||||
@28
|
||||
testbench.trace_valid_0
|
||||
testbench.trace_valid_1
|
||||
@22
|
||||
testbench.trace_data_0[35:0]
|
||||
testbench.trace_data_1[35:0]
|
||||
@420
|
||||
testbench.trace_balance[7:0]
|
||||
@200
|
||||
-
|
||||
-CPU #0
|
||||
@28
|
||||
testbench.mem_valid_0
|
||||
testbench.mem_ready_0
|
||||
testbench.mem_instr_0
|
||||
@22
|
||||
testbench.mem_addr_0[31:0]
|
||||
testbench.mem_rdata_0[31:0]
|
||||
testbench.mem_wdata_0[31:0]
|
||||
@28
|
||||
testbench.mem_wstrb_0[3:0]
|
||||
@22
|
||||
testbench.cpu_0.cpu_state[7:0]
|
||||
@28
|
||||
testbench.cpu_0.mem_state[1:0]
|
||||
@200
|
||||
-
|
||||
-CPU #1
|
||||
@28
|
||||
testbench.mem_valid_1
|
||||
testbench.mem_ready_1
|
||||
testbench.mem_instr_1
|
||||
@22
|
||||
testbench.mem_addr_1[31:0]
|
||||
testbench.mem_rdata_1[31:0]
|
||||
testbench.mem_wdata_1[31:0]
|
||||
@28
|
||||
testbench.mem_wstrb_1[3:0]
|
||||
@22
|
||||
testbench.cpu_1.cpu_state[7:0]
|
||||
@28
|
||||
testbench.cpu_1.mem_state[1:0]
|
||||
@200
|
||||
-
|
||||
[pattern_trace] 1
|
||||
[pattern_trace] 0
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -ex
|
||||
|
||||
yosys -ql tracecmp.yslog \
|
||||
-p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
|
||||
-p 'read_verilog -formal tracecmp.v' \
|
||||
-p 'prep -top testbench -nordff' \
|
||||
-p 'write_smt2 -mem -bv -wires tracecmp.smt2'
|
||||
|
||||
yosys-smtbmc -s yices --smtc tracecmp.smtc --dump-vcd tracecmp.vcd tracecmp.smt2
|
||||
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
initial
|
||||
assume (= [mem_0] [mem_1])
|
||||
assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
|
||||
assume (= [trace_data_0] [trace_data_1])
|
||||
|
||||
always
|
||||
assume (=> (not [mem_valid_0]) (not [mem_ready_0]))
|
||||
assume (=> (not [mem_valid_1]) (not [mem_ready_1]))
|
||||
# assume (= [mem_ready_0] [mem_ready_1])
|
||||
|
||||
always -1
|
||||
assert (=> (= [trace_balance] #x00) (= [trace_data_0] [trace_data_1]))
|
||||
|
|
@ -0,0 +1,109 @@
|
|||
module testbench(input clk, mem_ready_0, mem_ready_1);
|
||||
// set this to 1 to test generation of counter examples
|
||||
localparam ENABLE_COUNTERS = 0;
|
||||
|
||||
reg resetn = 0;
|
||||
always @(posedge clk) resetn <= 1;
|
||||
|
||||
(* keep *) wire trap_0, trace_valid_0, mem_valid_0, mem_instr_0;
|
||||
(* keep *) wire [3:0] mem_wstrb_0;
|
||||
(* keep *) wire [31:0] mem_addr_0, mem_wdata_0, mem_rdata_0;
|
||||
(* keep *) wire [35:0] trace_data_0;
|
||||
|
||||
(* keep *) wire trap_1, trace_valid_1, mem_valid_1, mem_instr_1;
|
||||
(* keep *) wire [3:0] mem_wstrb_1;
|
||||
(* keep *) wire [31:0] mem_addr_1, mem_wdata_1, mem_rdata_1;
|
||||
(* keep *) wire [35:0] trace_data_1;
|
||||
|
||||
reg [31:0] mem_0 [0:2**30-1];
|
||||
reg [31:0] mem_1 [0:2**30-1];
|
||||
|
||||
assign mem_rdata_0 = mem_0[mem_addr_0 >> 2];
|
||||
assign mem_rdata_1 = mem_1[mem_addr_1 >> 2];
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (resetn && mem_valid_0 && mem_ready_0) begin
|
||||
if (mem_wstrb_0[3]) mem_0[mem_addr_0 >> 2][31:24] <= mem_wdata_0[31:24];
|
||||
if (mem_wstrb_0[2]) mem_0[mem_addr_0 >> 2][23:16] <= mem_wdata_0[23:16];
|
||||
if (mem_wstrb_0[1]) mem_0[mem_addr_0 >> 2][15: 8] <= mem_wdata_0[15: 8];
|
||||
if (mem_wstrb_0[0]) mem_0[mem_addr_0 >> 2][ 7: 0] <= mem_wdata_0[ 7: 0];
|
||||
end
|
||||
if (resetn && mem_valid_1 && mem_ready_1) begin
|
||||
if (mem_wstrb_1[3]) mem_1[mem_addr_1 >> 2][31:24] <= mem_wdata_1[31:24];
|
||||
if (mem_wstrb_1[2]) mem_1[mem_addr_1 >> 2][23:16] <= mem_wdata_1[23:16];
|
||||
if (mem_wstrb_1[1]) mem_1[mem_addr_1 >> 2][15: 8] <= mem_wdata_1[15: 8];
|
||||
if (mem_wstrb_1[0]) mem_1[mem_addr_1 >> 2][ 7: 0] <= mem_wdata_1[ 7: 0];
|
||||
end
|
||||
end
|
||||
|
||||
(* keep *) reg [7:0] trace_balance;
|
||||
reg [7:0] trace_balance_q;
|
||||
|
||||
always @* begin
|
||||
trace_balance = trace_balance_q;
|
||||
if (trace_valid_0) trace_balance = trace_balance + 1;
|
||||
if (trace_valid_1) trace_balance = trace_balance - 1;
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
trace_balance_q <= resetn ? trace_balance : 0;
|
||||
end
|
||||
|
||||
picorv32 #(
|
||||
// do not change this settings
|
||||
.ENABLE_COUNTERS(ENABLE_COUNTERS),
|
||||
.ENABLE_TRACE(1),
|
||||
|
||||
// change this settings as you like
|
||||
.ENABLE_REGS_DUALPORT(1),
|
||||
.TWO_STAGE_SHIFT(1),
|
||||
.BARREL_SHIFTER(0),
|
||||
.TWO_CYCLE_COMPARE(0),
|
||||
.TWO_CYCLE_ALU(0),
|
||||
.COMPRESSED_ISA(0),
|
||||
.ENABLE_MUL(0),
|
||||
.ENABLE_DIV(0)
|
||||
) cpu_0 (
|
||||
.clk (clk ),
|
||||
.resetn (resetn ),
|
||||
.trap (trap_0 ),
|
||||
.mem_valid (mem_valid_0 ),
|
||||
.mem_instr (mem_instr_0 ),
|
||||
.mem_ready (mem_ready_0 ),
|
||||
.mem_addr (mem_addr_0 ),
|
||||
.mem_wdata (mem_wdata_0 ),
|
||||
.mem_wstrb (mem_wstrb_0 ),
|
||||
.mem_rdata (mem_rdata_0 ),
|
||||
.trace_valid (trace_valid_0),
|
||||
.trace_data (trace_data_0 )
|
||||
);
|
||||
|
||||
picorv32 #(
|
||||
// do not change this settings
|
||||
.ENABLE_COUNTERS(ENABLE_COUNTERS),
|
||||
.ENABLE_TRACE(1),
|
||||
|
||||
// change this settings as you like
|
||||
.ENABLE_REGS_DUALPORT(1),
|
||||
.TWO_STAGE_SHIFT(1),
|
||||
.BARREL_SHIFTER(0),
|
||||
.TWO_CYCLE_COMPARE(0),
|
||||
.TWO_CYCLE_ALU(0),
|
||||
.COMPRESSED_ISA(0),
|
||||
.ENABLE_MUL(0),
|
||||
.ENABLE_DIV(0)
|
||||
) cpu_1 (
|
||||
.clk (clk ),
|
||||
.resetn (resetn ),
|
||||
.trap (trap_1 ),
|
||||
.mem_valid (mem_valid_1 ),
|
||||
.mem_instr (mem_instr_1 ),
|
||||
.mem_ready (mem_ready_1 ),
|
||||
.mem_addr (mem_addr_1 ),
|
||||
.mem_wdata (mem_wdata_1 ),
|
||||
.mem_wstrb (mem_wstrb_1 ),
|
||||
.mem_rdata (mem_rdata_1 ),
|
||||
.trace_valid (trace_valid_1),
|
||||
.trace_data (trace_data_1 )
|
||||
);
|
||||
endmodule
|
||||
Loading…
Reference in New Issue