Added more asserts to picorv32, more smtbmc examples

6 files changed, 190 insertions, 3 deletions

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