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

Added more asserts to picorv32, more smtbmc examples

This commit is contained in:
Clifford Wolf 2016-08-29 17:23:00 +02:00
parent 72158ba4a5
commit 28fe45ffe9
8 changed files with 275 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Makefile
View File

@ -19,9 +19,13 @@ testbench.vcd: testbench.vvp firmware/firmware.hex
view: testbench.vcd
gtkwave $< testbench.gtkw
check: check.smt2
yosys-smtbmc -t 30 --dump-vcd check.vcd check.smt2
yosys-smtbmc -t 30 --dump-vcd check.vcd -i check.smt2
check-z3: check.smt2
yosys-smtbmc -s z3 -t 30 --dump-vcd check.vcd check.smt2
yosys-smtbmc -s z3 -t 30 --dump-vcd check.vcd -i check.smt2
check-yices: check.smt2
yosys-smtbmc -s yices -t 30 --dump-vcd check.vcd check.smt2
yosys-smtbmc -s yices -t 30 --dump-vcd check.vcd -i check.smt2
check.smt2: picorv32.v
yosys -v2 -p 'read_verilog -formal picorv32.v' \
@ -133,5 +137,5 @@ clean:
firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
testbench.vvp testbench_sp.vvp testbench_synth.vvp testbench.vcd testbench.trace
.PHONY: test view test_sp test_axi test_synth download-tools toc clean
.PHONY: test view test_sp test_axi test_synth check-z3 check-yices download-tools build-tools toc clean

127
picorv32.v
View File

@ -31,8 +31,10 @@
`ifdef FORMAL
`define FORMAL_KEEP (* keep *)
`define assert(assert_expr) assert(assert_expr)
`else
`define FORMAL_KEEP
`define assert(assert_expr)
`endif
/***************************************************************
@ -454,64 +456,85 @@ module picorv32 #(
end
always @(posedge clk) begin
if (mem_la_read || mem_la_write) begin
mem_addr <= mem_la_addr;
mem_wdata <= mem_la_wdata;
mem_wstrb <= mem_la_wstrb & {4{mem_la_write}};
if (resetn) begin
if (mem_do_prefetch || mem_do_rinst || mem_do_rdata)
`assert(!mem_do_wdata);
if (mem_do_wdata)
`assert(!(mem_do_prefetch || mem_do_rinst || mem_do_rdata));
end
if (!resetn) begin
end
always @(posedge clk) begin
if (!resetn || trap) begin
mem_state <= 0;
mem_valid <= 0;
if (!resetn || mem_ready)
mem_valid <= 0;
mem_la_secondword <= 0;
prefetched_high_word <= 0;
end else case (mem_state)
0: begin
if (mem_do_prefetch || mem_do_rinst || mem_do_rdata) begin
mem_valid <= !mem_la_use_prefetched_high_word;
mem_instr <= mem_do_prefetch || mem_do_rinst;
mem_wstrb <= 0;
mem_state <= 1;
end
if (mem_do_wdata) begin
mem_valid <= 1;
mem_instr <= 0;
mem_state <= 2;
end
end else begin
if (mem_la_read || mem_la_write) begin
mem_addr <= mem_la_addr;
mem_wdata <= mem_la_wdata;
mem_wstrb <= mem_la_wstrb & {4{mem_la_write}};
end
1: begin
if (mem_xfer) begin
if (COMPRESSED_ISA && mem_la_read) begin
case (mem_state)
0: begin
if (mem_do_prefetch || mem_do_rinst || mem_do_rdata) begin
mem_valid <= !mem_la_use_prefetched_high_word;
mem_instr <= mem_do_prefetch || mem_do_rinst;
mem_wstrb <= 0;
mem_state <= 1;
end
if (mem_do_wdata) begin
mem_valid <= 1;
mem_la_secondword <= 1;
if (!mem_la_use_prefetched_high_word)
mem_16bit_buffer <= mem_rdata[31:16];
end else begin
mem_valid <= 0;
mem_la_secondword <= 0;
if (COMPRESSED_ISA && !mem_do_rdata) begin
if (~&mem_rdata[1:0] || mem_la_secondword) begin
mem_16bit_buffer <= mem_rdata[31:16];
prefetched_high_word <= 1;
end else begin
prefetched_high_word <= 0;
end
end
mem_state <= mem_do_rinst || mem_do_rdata ? 0 : 3;
mem_instr <= 0;
mem_state <= 2;
end
end
end
2: begin
if (mem_xfer) begin
mem_valid <= 0;
mem_state <= 0;
1: begin
`assert(mem_wstrb == 0);
`assert(mem_do_prefetch || mem_do_rinst || mem_do_rdata);
`assert(mem_valid == !mem_la_use_prefetched_high_word);
`assert(mem_instr == (mem_do_prefetch || mem_do_rinst));
if (mem_xfer) begin
if (COMPRESSED_ISA && mem_la_read) begin
mem_valid <= 1;
mem_la_secondword <= 1;
if (!mem_la_use_prefetched_high_word)
mem_16bit_buffer <= mem_rdata[31:16];
end else begin
mem_valid <= 0;
mem_la_secondword <= 0;
if (COMPRESSED_ISA && !mem_do_rdata) begin
if (~&mem_rdata[1:0] || mem_la_secondword) begin
mem_16bit_buffer <= mem_rdata[31:16];
prefetched_high_word <= 1;
end else begin
prefetched_high_word <= 0;
end
end
mem_state <= mem_do_rinst || mem_do_rdata ? 0 : 3;
end
end
end
end
3: begin
if (mem_do_rinst) begin
mem_state <= 0;
2: begin
`assert(mem_wstrb != 0);
`assert(mem_do_wdata);
if (mem_xfer) begin
mem_valid <= 0;
mem_state <= 0;
end
end
end
endcase
3: begin
`assert(mem_wstrb == 0);
`assert(mem_do_prefetch);
if (mem_do_rinst) begin
mem_state <= 0;
end
end
endcase
end
if (clear_prefetched_high_word)
prefetched_high_word <= 0;
@ -1668,12 +1691,16 @@ module picorv32 #(
reg [3:0] last_mem_nowait;
always @(posedge clk)
last_mem_nowait <= {last_mem_nowait, mem_ready || !mem_valid};
// stall the memory interface for max 4 cycles
restrict property (|last_mem_nowait || mem_ready || !mem_valid);
// resetn low in first cycle, after that resetn high
restrict property (resetn != $initstate);
reg ok;
always @* begin
restrict (resetn == !$initstate);
if (!$initstate) begin
if (resetn) begin
// instruction fetches are read-only
if (mem_valid && mem_instr)
assert (mem_wstrb == 0);

5
scripts/smtbmc/.gitignore vendored
View File

@ -1,3 +1,6 @@
tracecmp.smt2
tracecmp.vcd
tracecmp.yslog
notrap_validop.smt2
notrap_validop.yslog
output.vcd
output.smtc

13
scripts/smtbmc/notrap_validop.sh Normal file
View File

@ -0,0 +1,13 @@
#!/bin/bash
set -ex
yosys -ql notrap_validop.yslog \
-p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
-p 'read_verilog -formal notrap_validop.v' \
-p 'prep -top testbench -nordff' \
-p 'write_smt2 -mem -bv -wires notrap_validop.smt2'
#yosys-smtbmc -s yices -t 50 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2
yosys-smtbmc -s yices -i -t 27 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2

67
scripts/smtbmc/notrap_validop.v Normal file
View File

@ -0,0 +1,67 @@
module testbench(input clk, mem_ready);
`include "opcode.v"
reg resetn = 0;
always @(posedge clk) resetn <= 1;
(* keep *) wire trap, mem_valid, mem_instr;
(* keep *) wire [3:0] mem_wstrb;
(* keep *) wire [31:0] mem_addr, mem_wdata, mem_rdata;
(* keep *) wire [35:0] trace_data;
reg [31:0] mem [0:2**30-1];
assign mem_rdata = mem[mem_addr >> 2];
always @(posedge clk) begin
if (resetn && mem_valid && mem_ready) begin
if (mem_wstrb[3]) mem[mem_addr >> 2][31:24] <= mem_wdata[31:24];
if (mem_wstrb[2]) mem[mem_addr >> 2][23:16] <= mem_wdata[23:16];
if (mem_wstrb[1]) mem[mem_addr >> 2][15: 8] <= mem_wdata[15: 8];
if (mem_wstrb[0]) mem[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0];
end
end
reg [1:0] mem_ready_stall = 0;
always @(posedge clk) begin
mem_ready_stall <= {mem_ready_stall, mem_valid && !mem_ready};
restrict(&mem_ready_stall == 0);
if (mem_instr && mem_ready && mem_valid) begin
assume(opcode_valid(mem_rdata));
assume(!opcode_branch(mem_rdata));
assume(!opcode_load(mem_rdata));
assume(!opcode_store(mem_rdata));
end
if (!mem_valid)
assume(!mem_ready);
if (resetn)
assert(!trap);
end
picorv32 #(
// 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 (
.clk (clk ),
.resetn (resetn ),
.trap (trap ),
.mem_valid (mem_valid ),
.mem_instr (mem_instr ),
.mem_ready (mem_ready ),
.mem_addr (mem_addr ),
.mem_wdata (mem_wdata ),
.mem_wstrb (mem_wstrb ),
.mem_rdata (mem_rdata )
);
endmodule

104
scripts/smtbmc/opcode.v Normal file
View File

@ -0,0 +1,104 @@
function opcode_jump;
input [31:0] opcode;
begin
opcode_jump = 0;
if (opcode[6:0] == 7'b1101111) opcode_jump = 1; // JAL
if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100111) opcode_jump = 1; // JALR
end
endfunction
function opcode_branch;
input [31:0] opcode;
begin
opcode_branch = 0;
if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BEQ
if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BNE
if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLT
if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGE
if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLTU
if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGEU
end
endfunction
function opcode_load;
input [31:0] opcode;
begin
opcode_load = 0;
if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LB
if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LH
if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LW
if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LBU
if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LHU
end
endfunction
function opcode_store;
input [31:0] opcode;
begin
opcode_store = 0;
if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SB
if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SH
if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SW
end
endfunction
function opcode_alui;
input [31:0] opcode;
begin
opcode_alui = 0;
if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ADDI
if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTI
if (opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTIU
if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // XORI
if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ORI
if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ANDI
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLLI
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRLI
if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRAI
end
endfunction
function opcode_alu;
input [31:0] opcode;
begin
opcode_alu = 0;
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // ADD
if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SUB
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLL
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLT
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLTU
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // XOR
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRL
if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRA
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // OR
if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // AND
end
endfunction
function opcode_sys;
input [31:0] opcode;
begin
opcode_sys = 0;
if (opcode[31:20] == 12'hC00 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLE
if (opcode[31:20] == 12'hC01 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIME
if (opcode[31:20] == 12'hC02 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRET
if (opcode[31:20] == 12'hC80 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLEH
if (opcode[31:20] == 12'hC81 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIMEH
if (opcode[31:20] == 12'hC82 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRETH
end
endfunction
function opcode_valid;
input [31:0] opcode;
begin
opcode_valid = 0;
if (opcode_jump (opcode)) opcode_valid = 1;
if (opcode_branch(opcode)) opcode_valid = 1;
if (opcode_load (opcode)) opcode_valid = 1;
if (opcode_store (opcode)) opcode_valid = 1;
if (opcode_alui (opcode)) opcode_valid = 1;
if (opcode_alu (opcode)) opcode_valid = 1;
if (opcode_sys (opcode)) opcode_valid = 1;
end
endfunction

2
scripts/smtbmc/tracecmp.gtkw
View File

@ -2,7 +2,7 @@
[*] 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] "/home/clifford/Work/picorv32/scripts/smtbmc/output.vcd"
[dumpfile_mtime] "Fri Aug 26 15:33:18 2016"
[dumpfile_size] 80106
[savefile] "/home/clifford/Work/picorv32/scripts/smtbmc/tracecmp.gtkw"

2
scripts/smtbmc/tracecmp.sh
View File

@ -8,5 +8,5 @@ yosys -ql tracecmp.yslog \
-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
yosys-smtbmc -s yices --smtc tracecmp.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp.smt2