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;