Hardware
/
picorv32
mirror of https://github.com/YosysHQ/picorv32.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Using assertpmux in "make check"

This commit is contained in:
Clifford Wolf 2016-09-07 12:40:19 +02:00
parent da37498191
commit 44d6feba2a
2 changed files with 29 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Makefile
View File

@ -23,11 +23,12 @@ check: check-yices
check-%: check.smt2
yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd check.smt2
yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd -i check.smt2
yosys-smtbmc -s $(subst check-,,$@) -t 20 --dump-vcd check.vcd -i check.smt2
check.smt2: picorv32.v
yosys -v2 -p 'read_verilog -formal picorv32.v' \
-p 'prep -top picorv32 -nordff' \
-p 'assertpmux -noinit; opt -fast' \
-p 'write_smt2 -wires check.smt2'
test_sp: testbench_sp.vvp firmware/firmware.hex

28
picorv32.v
View File

@ -1016,6 +1016,9 @@ module picorv32 #(
mem_rdata_q[14:12] == 3'b101 && mem_rdata_q[31:25] == 7'b0100000
};
is_lui_auipc_jal_jalr_addi_add_sub <= 0;
is_compare <= 0;
(* parallel_case *)
case (1'b1)
instr_jal:
@ -1032,6 +1035,29 @@ module picorv32 #(
decoded_imm <= 1'bx;
endcase
end
if (!resetn) begin
is_beq_bne_blt_bge_bltu_bgeu <= 0;
is_compare <= 0;
instr_addi <= 0;
instr_slti <= 0;
instr_sltiu <= 0;
instr_xori <= 0;
instr_ori <= 0;
instr_andi <= 0;
instr_add <= 0;
instr_sub <= 0;
instr_sll <= 0;
instr_slt <= 0;
instr_sltu <= 0;
instr_xor <= 0;
instr_srl <= 0;
instr_sra <= 0;
instr_or <= 0;
instr_and <= 0;
end
end
@ -1525,7 +1551,7 @@ module picorv32 #(
reg_op2 <= cpuregs_rs2;
(* parallel_case *)
case (1'b1)
is_sb_sh_sw && !instr_trap: begin
is_sb_sh_sw: begin
cpu_state <= cpu_state_stmem;
mem_do_rinst <= 1;
end