Skip to content

Commit

Permalink
increase code coverage in commit stage (#2555)
Browse files Browse the repository at this point in the history
`exception_o.valid` is always 0 here because the context requires:

- `commit_ack_o[0]`
- `commit_instr_i[0].fu != CSR`

Proof.

***********************************************************
We have `commit_ack_o[0]` and `commit_instr_i[0].fu != CSR`
We need to prove `!exception_o.valid`.
***********************************************************

`exception_o.valid` is built such that:
    `exception_o.valid => !commit_drop_i[0] && (csr_exception_i.valid || commit_instr_i[0].ex.valid)`
By contraposition:
    `!(!commit_drop_i[0] && (csr_exception_i.valid || commit_instr_i[0].ex.valid)) => !exception_o.valid`
By De Morgan:
    `commit_drop_i[0] || !(csr_exception_i.valid || commit_instr_i[0].ex.valid) => !exception_o.valid`
    `commit_drop_i[0] || (!csr_exception_i.valid && !commit_instr_i[0].ex.valid) => !exception_o.valid`
    `(commit_drop_i[0] || !csr_exception_i.valid) && (commit_drop_i[0] || !commit_instr_i[0].ex.valid) => !exception_o.valid`
Goal split.

***********************************************************
We have `commit_ack_o[0]` and `commit_instr_i[0].fu != CSR`
We need to prove both:
1.`commit_drop_i[0] || !csr_exception_i.valid`
2. `commit_drop_i[0] || !commit_instr_i[0].ex.valid`
***********************************************************

`csr_exception_i.valid` is built such that (see `core/csr_regfile.sv`):
    `csr_exception_i.valid => commit_instr_i[0].fu == CSR`
By contraposition:
    `commit_instr_i[0].fu != CSR => !csr_exception_i.valid`
Because `commit_instr_i[0].fu != CSR`:
    `!csr_exception_i.valid`
By implication:
    `commit_drop_i[0] || !csr_exception_i.valid`
Goal 1 reached.

`commit_ack_o[0]` is built such that:
    `commit_ack_o[0] => commit_instr_i[0].ex.valid && commit_drop_i[0] || !commit_instr_i[0].ex_valid`
Which can be simplified (AB+!A = AB+!A(B+1) = AB+!AB+!A = (A+!A)B+!A = B+!A):
    `commit_ack_o[0] => commit_drop_i[0] || !commit_instr_i[0].ex_valid`
Because `commit_ack_o[0]`:
    `commit_drop_i[0] || !commit_instr_i[0].ex.valid`
Goal 2 reached.
Qed.
  • Loading branch information
cathales authored Oct 18, 2024
1 parent cff48e4 commit 0bf937a
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions core/commit_stage.sv
Original file line number Diff line number Diff line change
Expand Up @@ -318,8 +318,7 @@ module commit_stage
&& !single_step_i) begin
// only if the first instruction didn't throw an exception and this instruction won't throw an exception
// and the functional unit is of type ALU, LOAD, CTRL_FLOW, MULT, FPU or FPU_VEC
if (!exception_o.valid && !commit_instr_i[1].ex.valid
&& (commit_instr_i[1].fu inside {ALU, LOAD, CTRL_FLOW, MULT, FPU, FPU_VEC})) begin
if (!commit_instr_i[1].ex.valid && (commit_instr_i[1].fu inside {ALU, LOAD, CTRL_FLOW, MULT, FPU, FPU_VEC})) begin

if (CVA6Cfg.RVZCMP && commit_instr_i[1].is_macro_instr && commit_instr_i[1].is_last_macro_instr)
commit_macro_ack[1] = 1'b1;
Expand Down

0 comments on commit 0bf937a

Please sign in to comment.