Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information