Skip to content

Commit

Permalink
Merge pull request #2476 from pascalgouedo/cv32e40p/dev_dd_pgo
Browse files Browse the repository at this point in the history 
CV32E40Pv2 RISC-V ISA Formal Verif document and plan adition and README update
  • Loading branch information
pascalgouedo authored Jun 21, 2024
2 parents b928395 + 36b063b commit 2a85de3
Show file tree
Hide file tree
Showing 3 changed files with 25 additions and 22 deletions.
47 changes: 25 additions & 22 deletions cv32e40p/docs/VerifPlans/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,10 @@ Below are two different chapters describing verification plans status and direct
# CV32E40P (V2) Verification Plans

## Short verification methodology introduction
For CV32E40P**v2** verification, the formal verification methodology has been choosen over the stimuli-based simulation that was done for version one of the core. However, full verification closure is not feasible using only formal verification due to complexity of specific scenarios. All these specific uncoverable scenarios from formal verification are then exercised by stimuli-based simulation using a reference model of the core. These scenarios along with formal assertions are described inside verifications plans, for which details are given in a table below. Regarding already available v1 plans, their re-use or not is specified in this table.
For CV32E40Pv2 verification, the formal verification methodology has been chosen over the stimuli-based simulation that was done for v1 version of the core. However, full verification closure is not feasible using only formal verification due to complexity of specific scenarios. All these specific uncoverable scenarios from formal verification are then exercised by stimuli-based simulation using a reference model of the core. These scenarios along with formal assertions are described inside verifications plans, for which details are given in a table below. Regarding already available v1 plans, their re-use or not is specified in this table.

RISC-V ISA Formal Verification methodology is described [here](https://github.com/openhwgroup/core-v-verif/tree/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_RISCV_vPlan_v1.1.pdf).
Setup and script files to launch RISC-V ISA Formal Verification using Siemens Questa Processor tool are available [here](https://github.com/openhwgroup/cv32e40p/tree/dev/scripts/riscv_isa_formal).

## Verification Plan Status

Expand All @@ -29,27 +32,27 @@ Under the heading `Link`, the name shown corresponds to the filename of the vpla

| Category | Feature | VPlan Status | Review Status | Comment | Link |
|---------------------|----------------|--------------|---------------|---------|------|
| **Base Instruction Set** | RV32IMC + F + Zfinx + Zifencei | v2-formal-new | Not Available for Review | Waiting Approval from Siemens | |
| **Interrupts** | CLINT | v1-updated | **Ready for Review** | Addition of missing XPULP / F / Zfinx interrupts | [CV32E40P_interrupts.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/interrupts/CV32E40P_interrupts.xlsx "Interrupts Vplan")|
| **Debug & Trace** | Debug | v1-reused | Reviewed | Missing XPULP-specific debug are in a separate vplan | [CV32E40P_debug.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/debug-trace/CV32E40P_debug.xlsx "Debug Vplan")|
| **Privileged Spec** | CSRs / Zicsr | v2-formal-new | Not Available for Review | Waiting Approval from Siemens | |
| **Micro-architecture** | OBI | v1-reused | Reviewed | | [CV32E40P_OBI_VerifPlan.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_OBI_VerifPlan.xlsx "OBI Vplan") |
| | Pipeline / SleepUnit | v1-reused | Reviewed | | [CV32E40P_Pipeline_Sleep.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_Pipeline_Sleep.xlsx "Pipeline Sleep Vplan") |
| | FPU Register File | v2-sim-new | **Ready for Review** | | [CV32E40P_FPU_register_file.xlsx](https://github.com/XavierAubert/core-v-verif/blob/b654922fa6ac061b9fe2757e3928eb25603b3e89/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_FPU_register_file.xlsx "FPU Reg. File Vplan") |
| **Additional ISA** | F / Zfinx | v2-sim-new | **Ready for Review** | Includes uncoverable items from formal verification | [CV32E40P_F-Zfinx-instructions.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/Zfinx_F_instructions/CV32E40P_F-Zfinx-instructions.xlsx "Add. F/Zfinx Vplan") |
| **XPULP** | Post-Increment Load/Store (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens |
| | Post-Increment Load/Store (Simulation) | v2-sim-new | **Ready for Review** | Addition of "pipeline" with simulation (preceeding F multicycle) | [CV32E40P_xpulp-postinc-loadstore.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-postinc-loadstore.xlsx "Post-Inc Load/Store simu Vplan") |
| | Bitmanipulation (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens | |
| | Bitmanipulation (Simulation) | v2-sim-new | **Ready for Review** | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40P_xpulp-bitmanipulation.xlsx](https://github.com/XavierAubert/core-v-verif/blob/2234255b7e5a2c83099dbb5755a2bdc9768c7009/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-bitmanipulations.xlsx "Bitmanip simu Vplan") |
| | General ALU (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens | |
| | General ALU (Simulation) | v2-simu-new | **Ready for Review** | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40P_xpulp-general-alu.xlsx](https://github.com/XavierAubert/core-v-verif/blob/2234255b7e5a2c83099dbb5755a2bdc9768c7009/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-general-alu.xlsx "General ALU simu Vplan") |
| | Immediate Branching (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens | |
| | Immediate Branching (Simulation) | v2-simu-new | **Ready for Review** | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40P_xpulp-immediate-branching.xlsx](https://github.com/XavierAubert/core-v-verif/blob/2234255b7e5a2c83099dbb5755a2bdc9768c7009/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-immediate-branching.xlsx "Imm Branching simu Vplan") |
| | MAC (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens |
| | MAC (Simulation) | v2-sim-new | **Ready for Review** | Addition of missing coverage from formal (operands "toggle") | [CV32E40P_xpulp-multiply-accumulate.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-multiply-accumulate.xlsx "MAC simu Vplan") |
| | SIMD (Formal) | v2-formal-new | Not Available for Review | Waiting Approval from Siemens |
| | SIMD (Simulation) | v2-sim-new | **Ready for Review** | Addition of missing coverage from formal (operands "toggle") | [CV32E40P_xpulp-packed-simd.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-packed-simd.xlsx "SIMD simu Vplan") |
| | HWLoop (Simulation) | v2-sim-new | **Ready for Review** | Feature not test at all in formal verification | [CV32E40P_xpulp-hwloop.xlsx](https://github.com/openhwgroup/core-v-verif/blob/2378099bfce1c7b2b3d089ea2cb60ad422c05e94/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-hwloop.xlsx "HWLoop Vplan") |
| **Base Instruction Set** | RV32IMC + F + Zfinx + Zifencei | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| **Interrupts** | CLINT | v1-updated | Reviewed | Addition of missing XPULP / F / Zfinx interrupts | [CV32E40Pv2_interrupts.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/interrupts/CV32E40Pv2_interrupts.xlsx "Interrupts Vplan")|
| **Debug & Trace** | Debug | v1-reused | Reviewed | Missing XPULP-specific debug are in a separate vplan | [CV32E40Pv2_debug.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/debug-trace/CV32E40Pv2_debug.xlsx "Debug Vplan")|
| **Privileged Spec** | CSRs / Zicsr | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| **Micro-architecture** | OBI | v1-reused | Reviewed | | [CV32E40P_OBI_VerifPlan.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_OBI_VerifPlan.xlsx "OBI Vplan") |
| | Pipeline / Sleep Unit | v1-reused | Reviewed | | [CV32E40P_Pipeline_Sleep.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_Pipeline_Sleep.xlsx "Pipeline Sleep Vplan") |
| | FPU Register File | v2-sim-new | Reviewed | | [CV32E40Pv2_FPU_register_file.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40Pv2_FPU_register_file.xlsx "FPU Reg. File Vplan") |
| **Additional ISA** | F / Zfinx | v2-sim-new | Reviewed | Includes uncoverable items from formal verification | [CV32E40Pv2_F-Zfinx-instructions.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/Zfinx_F_instructions/CV32E40Pv2_F-Zfinx-instructions.xlsx "Add. F/Zfinx Vplan") |
| **XPULP** | Post-Increment Load/Store (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | Post-Increment Load/Store (Simulation) | v2-sim-new | Reviewed | Addition of "pipeline" with simulation (preceeding F multicycle) | [CV32E40Pv2_xpulp-postinc-loadstore.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-postinc-loadstore.xlsx "Post-Inc Load/Store simu Vplan") |
| | Bitmanipulation (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | Bitmanipulation (Simulation) | v2-sim-new | Reviewed | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40Pv2_xpulp-bitmanipulation.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-bitmanipulations.xlsx "Bitmanip simu Vplan") |
| | General ALU (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | General ALU (Simulation) | v2-simu-new | Reviewed | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40Pv2_xpulp-general-alu.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-general-alu.xlsx "General ALU simu Vplan") |
| | Immediate Branching (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | Immediate Branching (Simulation) | v2-simu-new | Reviewed | Lowest priority as formal already checks everything needed, added because corev-dv generator will generate those instructions anyway | [CV32E40Pv2_xpulp-immediate-branching.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-immediate-branching.xlsx "Imm Branching simu Vplan") |
| | MAC (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | MAC (Simulation) | v2-sim-new | Reviewed | Addition of missing coverage from formal (operands "toggle") | [CV32E40Pv2_xpulp-multiply-accumulate.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-multiply-accumulate.xlsx "MAC simu Vplan") |
| | SIMD (Formal) | v2-formal-new | Reviewed | | [CV32E40Pv2_Formal_VerificationPlans.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx) |
| | SIMD (Simulation) | v2-sim-new | Reviewed | Addition of missing coverage from formal (operands "toggle") | [CV32E40Pv2_xpulp-packed-simd.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-packed-simd.xlsx "SIMD simu Vplan") |
| | HWLoop (Simulation) | v2-sim-new | Reviewed | Feature not test at all in formal verification | [CV32E40Pv2_xpulp-hwloop.xlsx](https://github.com/openhwgroup/core-v-verif/blob/cv32e40p/dev/cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40Pv2_xpulp-hwloop.xlsx "HWLoop Vplan") |


</br>
Expand Down
Binary file added cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx
View file
Binary file not shown.
Binary file added cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_RISCV_vPlan_v1.1.pdf
View file
Binary file not shown.

0 comments on commit 2a85de3

Please sign in to comment.