aboutsummaryrefslogtreecommitdiffstats
path: root/picorv32.v
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2017-05-11 00:13:01 +0200
committerClifford Wolf <clifford@clifford.at>2017-05-11 00:13:01 +0200
commitcd30db3425a08261f749523dff1f60f396143e37 (patch)
treee1e08b57fe8509fcdc4272314988947e20cc0b62 /picorv32.v
parentbf9687028df7570e7524a8a7b43f9c180c6dd1c7 (diff)
downloadpicorv32-cd30db3425a08261f749523dff1f60f396143e37.tar.gz
picorv32-cd30db3425a08261f749523dff1f60f396143e37.zip
Add riscv-formal alu/regs blackboxing
Diffstat (limited to 'picorv32.v')
-rw-r--r--picorv32.v14
1 files changed, 14 insertions, 0 deletions
diff --git a/picorv32.v b/picorv32.v
index 11d9e55..6de2bd4 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -1249,6 +1249,11 @@ module picorv32 #(
BARREL_SHIFTER && (instr_srl || instr_srli || instr_sra || instr_srai):
alu_out = alu_shr;
endcase
+
+`ifdef RISCV_FORMAL_BLACKBOX_ALU
+ alu_out_0 = $anyseq;
+ alu_out = $anyseq;
+`endif
end
reg clear_prefetched_high_word_q;
@@ -1303,11 +1308,20 @@ module picorv32 #(
always @* begin
decoded_rs = 'bx;
if (ENABLE_REGS_DUALPORT) begin
+`ifndef RISCV_FORMAL_BLACKBOX_REGS
cpuregs_rs1 = decoded_rs1 ? cpuregs[decoded_rs1] : 0;
cpuregs_rs2 = decoded_rs2 ? cpuregs[decoded_rs2] : 0;
+`else
+ cpuregs_rs1 = decoded_rs1 ? $anyseq : 0;
+ cpuregs_rs2 = decoded_rs2 ? $anyseq : 0;
+`endif
end else begin
decoded_rs = (cpu_state == cpu_state_ld_rs2) ? decoded_rs2 : decoded_rs1;
+`ifndef RISCV_FORMAL_BLACKBOX_REGS
cpuregs_rs1 = decoded_rs ? cpuregs[decoded_rs] : 0;
+`else
+ cpuregs_rs1 = decoded_rs ? $anyseq : 0;
+`endif
cpuregs_rs2 = cpuregs_rs1;
end
end