From 28fe45ffe929c2f6788314e5ff27923c8dc770b6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Aug 2016 17:23:00 +0200 Subject: [PATCH] Added more asserts to picorv32, more smtbmc examples --- Makefile | 12 ++- picorv32.v | 127 +++++++++++++++++++------------ scripts/smtbmc/.gitignore | 5 +- scripts/smtbmc/notrap_validop.sh | 13 ++++ scripts/smtbmc/notrap_validop.v | 67 ++++++++++++++++ scripts/smtbmc/opcode.v | 104 +++++++++++++++++++++++++ scripts/smtbmc/tracecmp.gtkw | 2 +- scripts/smtbmc/tracecmp.sh | 2 +- 8 files changed, 275 insertions(+), 57 deletions(-) create mode 100644 scripts/smtbmc/notrap_validop.sh create mode 100644 scripts/smtbmc/notrap_validop.v create mode 100644 scripts/smtbmc/opcode.v diff --git a/Makefile b/Makefile index c585588..eb3aa8a 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/picorv32.v b/picorv32.v index f6c6fc3..d95c74f 100644 --- a/picorv32.v +++ b/picorv32.v @@ -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); diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore index b27c0e6..54541e1 100644 --- a/scripts/smtbmc/.gitignore +++ b/scripts/smtbmc/.gitignore @@ -1,3 +1,6 @@ tracecmp.smt2 -tracecmp.vcd tracecmp.yslog +notrap_validop.smt2 +notrap_validop.yslog +output.vcd +output.smtc diff --git a/scripts/smtbmc/notrap_validop.sh b/scripts/smtbmc/notrap_validop.sh new file mode 100644 index 0000000..10a7ca5 --- /dev/null +++ b/scripts/smtbmc/notrap_validop.sh @@ -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 + diff --git a/scripts/smtbmc/notrap_validop.v b/scripts/smtbmc/notrap_validop.v new file mode 100644 index 0000000..8e50304 --- /dev/null +++ b/scripts/smtbmc/notrap_validop.v @@ -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 diff --git a/scripts/smtbmc/opcode.v b/scripts/smtbmc/opcode.v new file mode 100644 index 0000000..4c3792d --- /dev/null +++ b/scripts/smtbmc/opcode.v @@ -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 diff --git a/scripts/smtbmc/tracecmp.gtkw b/scripts/smtbmc/tracecmp.gtkw index 5f0e578..09dd9b2 100644 --- a/scripts/smtbmc/tracecmp.gtkw +++ b/scripts/smtbmc/tracecmp.gtkw @@ -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" diff --git a/scripts/smtbmc/tracecmp.sh b/scripts/smtbmc/tracecmp.sh index 4520082..6f471bd 100644 --- a/scripts/smtbmc/tracecmp.sh +++ b/scripts/smtbmc/tracecmp.sh @@ -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