For `XLEN = 64`, some tools (e.g. VCS) still elaborate the offset generation block for `XLEN = 32`, throwing an elaboration error (illegal bit access). Fix this by generating the AXI offset in an equivalent, parameter-agnostic and tool-friendly way.
The controller flushes the pipeline and all the unissued instructions in the presence of instructions with side effects (e.g., fence).
The accelerator dispatcher buffer (now used with the Ara RVV Vector processor) is flushed when this happens and avoids accepting a new instruction in that cycle, but it does not prevent the actual issuing of instructions during a flush cycle.
This fix avoids the issue during a flush cycle.
Both the ISA and design documentations use some parameters generated from the RTL (ports, parameters).
As of now, they are committed to the repository and can be out of sync with the code.
This PR removes them from the repository and freshly generates them from the code when building HTML files.
This PR also removes prebuilt HTML files (design & ISA docs) and generates them when building the top-level Read the Docs documentation (make -C docs).
- FIX: Replace riscv_pkg:VLEN by CVA6Cfg.VLEN
- Declare VLEN as new CVA6 parameter
- smoke-hwconfig: run with vcs-uvm and use return0 tests to speed-up CI light stage timing execution
- Use dedicated linker scripts for 65x configuration.
- Use dedicated spike.yaml for 65x configuration.
- Set BHTEntries=128, cache=WT, scoreboard entries=8 to improve Coremark and Dhrystone results
- Run 4 iterations of coremark to improve results
For reminder, the option --issrun_opts="+tb_performance_mode" allows to disable UVM features like assertion and log generation to reduce simulation time.
Fix following requirement:
The assertion included in the always_comb block apparently violates the requirements in [section 9.2.2.2.2 of the SystemVerilog standard](https://ieeexplore.ieee.org/document/10458102):
Statements in an always_comb shall not include those that block, have blocking timing or event
controls, or fork-join statements.
This modification allows:
- printing the results in the terminal
- running the script from the terminal (without the environment variables from CI)
The yaml report is only built in CI, but the results are always printed.
`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.
* INTERRUPT VERIF : Implement interrupt clear mechanism
* Interrupt Verif : Add irq_timeout to exit when we failed to write into irq_add
Also change uvm_warining to uvm_info
* Fix comment
