From 0bf937a772bd7d12ab17b351c43391057e13bd77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=B4me?= <124148386+cathales@users.noreply.github.com>
Date: Fri, 18 Oct 2024 09:02:07 +0200
Subject: [PATCH] increase code coverage in commit stage (#2555)

`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.
---
 core/commit_stage.sv | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/core/commit_stage.sv b/core/commit_stage.sv
index 1b67179d2f..c193c9154e 100644
--- a/core/commit_stage.sv
+++ b/core/commit_stage.sv
@@ -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;