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

Stronger property for correct predecode

This commit is contained in:
Luke Wren 2022-04-05 08:14:49 +01:00
parent 20cf408632
commit 35651f52a7
2 changed files with 19 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
hdl/hazard3_core.v
View File

@ -82,7 +82,6 @@ assign dbg_running = DEBUG_SUPPORT && !debug_mode;
// ----------------------------------------------------------------------------
// Pipe Stage F
wire f_jump_req;
wire [W_ADDR-1:0] f_jump_target;
wire f_jump_rdy;
@ -366,13 +365,17 @@ always @ (posedge clk or negedge rst_n) begin
end
`ifdef FORMAL
always @ (posedge clk) begin
if (rst_n && !x_stall) begin
if (~|d_rs1_predecoded)
assert(~|d_rs1);
if (~|d_rs2_predecoded)
assert(~|d_rs2);
end
always @ (posedge clk) if (rst_n && !x_stall) begin
// If stage 2 sees a reg operand, it must have been correctly predecoded too.
if (|d_rs1)
assert(d_rs1_predecoded == d_rs1);
if (|d_rs2)
assert(d_rs2_predecoded == d_rs2);
// If no reg was predecoded, stage 2 decode must agree there is no reg operand.
if (~|d_rs1_predecoded)
assert(~|d_rs1);
if (~|d_rs2_predecoded)
assert(~|d_rs2);
end
`endif
@ -850,10 +853,10 @@ end else begin: fast_branchcmp
hazard3_branchcmp #(
`include "hazard3_config_inst.vh"
) branchcmp_u (
.aluop (d_aluop),
.op_a (x_rs1_bypass),
.op_b (x_rs2_bypass),
.cmp (x_branch_cmp)
.aluop (d_aluop),
.op_a (x_rs1_bypass),
.op_b (x_rs2_bypass),
.cmp (x_branch_cmp)
);
end
@ -865,6 +868,7 @@ assign x_jump_req = !x_stall_on_raw && (
d_branchcond == BCOND_ZERO && !x_branch_cmp ||
d_branchcond == BCOND_NZERO && x_branch_cmp
);
// ----------------------------------------------------------------------------
// Pipe Stage M

6
hdl/hazard3_frontend.v
View File

@ -53,11 +53,11 @@ module hazard3_frontend #(
// Provide the rs1/rs2 register numbers which will be in CIR next cycle.
// Coarse: valid if this instruction has a nonzero register operand.
// (suitable for regfile read)
// (Suitable for regfile read)
output reg [4:0] predecode_rs1_coarse,
output reg [4:0] predecode_rs2_coarse,
// Fine: same as coarse, but more accurate zeroing when e.g. the operand is implicit.
// (suitable for bypass)
// Fine: like coarse, but accurate zeroing when the operand is implicit.
// (Suitable for bypass. Still not precise enough for stall logic.)
output reg [4:0] predecode_rs1_fine,
output reg [4:0] predecode_rs2_fine,