-
Notifications
You must be signed in to change notification settings - Fork 229
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
migrate Verification Plans from core-v-docs to core-v-verif
Break out ISA-level checks for instructions from core-specific vplans Signed-off-by: Steve Richmond <Steve.Richmond@silabs.com>
- Loading branch information
Showing
57 changed files
with
560 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
### Formal Verification documents for the CV32E40P RISC-V core |
Binary file added
BIN
+18.4 KB
...0p/docs/VerifPlans/Formal/base_instruction_set/CV32E40P_RV32C_Extension_Instructions.xlsx
Binary file not shown.
Binary file added
BIN
+16.2 KB
cv32e40p/docs/VerifPlans/Formal/base_instruction_set/CV32E40P_RV32IMC_Exceptions.xlsx
Binary file not shown.
Binary file added
BIN
+19.2 KB
cv32e40p/docs/VerifPlans/Formal/base_instruction_set/CV32E40P_RV32I_Base_Instructions.xlsx
Binary file not shown.
Binary file added
BIN
+20.1 KB
...0p/docs/VerifPlans/Formal/base_instruction_set/CV32E40P_RV32M_Extension_Instructions.xlsx
Binary file not shown.
Binary file added
BIN
+12.6 KB
...0p/docs/VerifPlans/Formal/base_instruction_set/CV32E40P_RV32Z_Extention_Instructions.xlsx
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,68 @@ | ||
<!--- SPDX-License-Identifier: Apache-2.0 WITH SHL-2.0 ---> | ||
This is the root directory of the CV32E40P Verification Plan (aka Test Plan). Each sub-directory is the Verification Plan a specific CV32E40P high-level feature of the same name. | ||
|
||
Use the provided CORE-V_Simulation VerifPlan_Template.xlsx spreadsheet as your template to capture a Verification Plan. | ||
|
||
## Verification Plan Status | ||
|
||
The tables below capture the current status of the Verification Plan for the CV32E40P by high-level feature. Under the heading `Review` is one of following: | ||
* **Ready for Review**: Vplan has been captured and is awaiting review. | ||
* **Reviewed**: Vplan has been reviewed, and is waiting for updates to address review feedback. | ||
* **Waiting for Signoff**: Vplan has been reviewed and review comments addressed by the author. Document is now waiting for reviewers to signoff on the post-review updates. | ||
* **Complete**: Post-preview updates have been signed-off. | ||
|
||
### Base instruction set plus standard instruction extensions | ||
|
||
_Refer to the VerifPlans/ISA/RV32/Simulation directory for specific Verification Plan status for each supported extension._ | ||
### Interrupts | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| CLINT | Captured | Complete | | | ||
| CLIC | | | Not a CV32E40P Feature | | ||
|
||
### Debug & Trace | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| Debug | Captured | Complete | | | ||
| Trigger module | Captured | Complete | Not a CV32E40P Feature | | ||
| Tracer | N/A | N/A | Behavioral model, not RTL | | ||
|
||
### Privileged spec | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| CSRs | Incomplete | | | | ||
| User mode | N/A| N/A | Not a CV32E40P Feature | | ||
| PMP | N/A | N/A | Not a CV32E40P Feature | | ||
|
||
### Micro-architecure | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| OBI | Complete | Reviewed | | | ||
| Sleep Unit | Complete | Reviewed | Updates pending based on review feedback | | ||
| Pipelines | Complete | Reviewed | Updates pending based on review feedback| | ||
|
||
### Xpulp instruction extensions | ||
**Note**: Xpulp instructions are "exercised, but not fully verified" in CV32E40P. | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| Post-increment load/store | Preliminary draft | | | | ||
| Hardware Loop | Preliminary draft | | On-going discussions with Cores TWG | | ||
| Bit Manipulation | Preliminary draft | | | | ||
| General ALU | Preliminary draft | | | | ||
| Immediate branching | Preliminary draft | | | | ||
| SIMD | Preliminary draft | | | | ||
|
||
### Custom circuitry | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| RI5CY performance counters | | | Not a CV32E40P Feature | | ||
| Advanced Processing Unit itf | | | Not a CV32E40P Feature | | ||
| 128-bit wide Instruction Bus itf | | | Not a CV32E40P Feature | | ||
| RI5CY interrupt scheme | | | Not a CV32E40P Feature | | ||
| PULP cluster itf | | | Not a CV32E40P Feature | |
Binary file not shown.
2 changes: 2 additions & 0 deletions
2
cv32e40p/docs/VerifPlans/Simulation/custom_circuitry/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
Placeholder directory for a specific [CV32E40P high-level feature](https://github.com/openhwgroup/core-v-verif/tree/master/doc). The Verification Plan (aka | ||
Test Plan) for this feature will be committed here as soon as is available. |
Binary file not shown.
Binary file added
BIN
+16.5 KB
cv32e40p/docs/VerifPlans/Simulation/debug-trace/CV32E40P_external-debugger.xlsx
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Directory for the CV32E40P Verification Plan for Debug and associated documentation. Note that only `CV32E40P_Debug` is relavent to the current release of CV32E40P. |
Binary file added
BIN
+358 KB
cv32e40p/docs/VerifPlans/Simulation/interrupts/CV32E40P_Interrupt_Vplan_Review.pptx
Binary file not shown.
Binary file added
BIN
+29.5 KB
cv32e40p/docs/VerifPlans/Simulation/interrupts/CV32E40P_interrupts.xlsx
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Directory for the CV32E40P Verification Plan for Interrupts and associated documentation. |
Binary file added
BIN
+15.9 KB
cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_OBI_VerifPlan.xlsx
Binary file not shown.
Binary file added
BIN
+13.1 KB
cv32e40p/docs/VerifPlans/Simulation/micro_architecture/CV32E40P_Pipeline_Sleep.xlsx
Binary file not shown.
1 change: 1 addition & 0 deletions
1
cv32e40p/docs/VerifPlans/Simulation/micro_architecture/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Verification Plans for CV32E40P physical interfaces. |
157 changes: 157 additions & 0 deletions
157
cv32e40p/docs/VerifPlans/Simulation/privileged_spec/CSR_Vplan.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,157 @@ | ||
## Functional verification of CSRs in a RISC-V core | ||
The Controll and Status Registers in a RISC-V core are distinct from CSRs in | ||
non-processor ASIC/FPGA RTL in ways that have a direct impact on RTL | ||
verification. Here, we discuss the problem in detail, using select RISC-V | ||
standard CSRs as examples. | ||
|
||
This document serves two purposes. The first purpose is a general discussion | ||
and tutorial on the topic of CSR verification in general and RISC-V CSR | ||
verification in particular. Its second purpose is form the Verification Plan | ||
(also known as a Testplan) for the CV32E40P CSRs. Note that this Vplan does | ||
not follow the same spreadsheet style template that is used for other CV32E40P | ||
Vplans. The reason for this will become apparent as you read the document. | ||
|
||
### Power-on-Reset Values | ||
|
||
Many (all?) RISC-V CSRs are expected to have a known value once the core comes | ||
out of hardware reset. Testing these values is typically straightforward and | ||
is done in a way that is familiar to anyone who has done this for non-processor | ||
ASIC/FPGA RTL. In both cases, care must be taken to read the value of a status | ||
register before the device-under-test experiences an event that causes an update | ||
to the register. For example, accessing a non-existant CSR should raise an | ||
illegal instruction exception which should, in turn, update the value of MCAUSE. | ||
Therefore a test that checks the PoR value of MCAUSE must not access a non-existant | ||
CSR before reading MCAUSE. | ||
|
||
### Access Mode Behavior | ||
|
||
Here, we are trying to answer the question, "how does the CSR behave when it is | ||
accessed (written to, or read from)?". In RISC-V cores, CSRs are accessed using | ||
the `CSRRC`, `CSRRCI`, `CSRRS`, `CSRRSI`, `CSRRW` and `CSRRWI` instructions. Note | ||
that there are also seven pseudoinstructions that will expand into one of these | ||
instructions. While in the general case a core may provide alternative means to | ||
access CSRs, in the CV32E40P, these instructions are the only access method available. | ||
|
||
Note that when verifying access mode behavior we are not (yet) concerned about | ||
what the core will do when a given CSR has a specific value. | ||
|
||
In RISC-V cores, access mode behavior has four dimensions: access mode, | ||
privilege, existance and field specification. These are discussed in turn, | ||
with emphasis placed on pre-silicon functional verification (as opposed to | ||
post-silicon use by software). | ||
|
||
#### Access Mode | ||
|
||
Access modes in RISC-V cores are simple and familar to those with prior experience | ||
with non-processor core ASIC/FPGA RTL. In fact, there are only two access modes | ||
to worry about: RW and RO: | ||
|
||
1. RW: all bits of a RW field must be writable and must return the last written | ||
value upon a read. | ||
2. RO: no bit of a RO field may be writable and must return the previous value upon | ||
read, event after being written to by either 0 or 1. | ||
|
||
#### Privilege | ||
|
||
Of course, nothing is ever _that_ simple with RISC-V. A core's privilege mode adds | ||
a second dimension to access mode. Is it often the case that a CSR that is | ||
accessible in a high privilege mode does not exist in lower modes. This must also | ||
be verified. | ||
|
||
For the purposes of CSR verification, it is permissible to consider Debug Mode as | ||
the highest privilege level. | ||
|
||
CV32E40P only supports Machine mode, which greatly simplifies the problem. | ||
|
||
#### Existance | ||
|
||
CSR "existance" is a concept unique to processor core and is not generally seen in | ||
non-processor ASIC/FPGA RTL designs. The RISC-V privileged and debug specifications | ||
define a set of CSRs, including both "required" and "optional" CSRs. Accessing an | ||
optional CSR may result in an illegal instruction (which must be veified). A | ||
complicating factor is that CSR existance may also be dependent on privlege level. | ||
For example reading a Debug CSR when the core is not in debug mode results in an | ||
illegal instruction exception while reading the same register in debug mode | ||
returns a value. | ||
|
||
#### Field Specification | ||
|
||
Although the "field specification" may sound familiar to those with a | ||
non-processor RTL background, the term is used differently in RISC-V where | ||
"field specification" refers to how software is expected to interact with | ||
specific fields of specific CSRs. This has a material impact on the strategy | ||
used for RTL verification of CSRs. There are three field specification types: | ||
|
||
1. **WPRI**: this field specification defines how software should interact | ||
with specific "protected" fields. This software action is wholly independent of RTL | ||
logic behavior, so WPRI fields may be treated as RO for the purposes of RTL | ||
functional verification of their access behavior. | ||
2. **WLRL**: once again, this field specification refers to how software should | ||
interact with specific RW fields. The difference is that reads will only return | ||
_legal_ values on reads, acting as a mask on return values of a RW test. In all | ||
other respects, WLRL fields may be treated as RW for the purposes of RTL | ||
functional verification of their access behavior. | ||
3. **WARL**: fields may be treated as RW (with read masking) for the purposes of RTL functional | ||
verification of their access behavior. | ||
|
||
|
||
### Control Actions | ||
|
||
CSRs are called Control and Status Registers for a reason. Control registers will | ||
change (control) the operation of the device under test in measureable ways and functional | ||
verification must coverage all legal values (or in some cases, important ranges of | ||
values) and then check that these values have the desired affect. A good example | ||
is ensuring that interrupts are asserted when MSTATUS[MIE] is both 0/1 and ensuring | ||
that interrupts are ignored or responded to, as appropriate. | ||
|
||
Control register verification of RISC-V cores is not conceptually different than | ||
control register verification of non-processor ASIC/FPGA RTL. One difference is | ||
that in non-processor RTL, the control path (reading the writing the CSRs) is | ||
typically independent of the data path (events that are affected by control | ||
register values). In processor cores a program executing on the core acts as both | ||
the control path (by executing CSR access instructions) and the data path (by | ||
executing code that is affected by the CSRs). | ||
|
||
### Status Capture | ||
|
||
Certain external and/or program events will be recorded in status registers. | ||
This sub-section will be updated at a later date. | ||
|
||
## CV32E40P CSR Verification Plan | ||
|
||
| Testcase | Targeted Aspect | Type | Reference | Status | | ||
|----------|-----------------|------|-----------|--------| | ||
| por\_csr.c | Power-on-Reset values | Manually written, directed | [1](#1) | Complete | | ||
| por\_debug\_csr.c | Power-on-Reset values for Debug CSRs | Manually written, directed | [2](#2) | | | ||
| csr\_existance.c | Illegal instruction exception for non-existant CSRs | Manually written, directed | [3](#3) | | | ||
| cv32e40p_csr\_access_test.c | Combined access mode behavior and field specification tests for all CSRs | Generated | [4](#4) | Under development | | ||
| csr\_privlege.c | Debug mode can access all CSRs | Manually written, directed | [5](#5) | | | ||
|
||
### ToDo: | ||
|
||
* Verification of status fields. | ||
* Verification of control fields. | ||
|
||
### 1 | ||
At the time of this writting (2020-10-07), this is implemented as two tests, `modeled_csr_por` and `requested_csr_por`. In the near (?) future these will be combined into a single test. For each machine-mode CSR in CV32E40P: | ||
- read current value | ||
- compare to documented PoR value in User Manual | ||
|
||
Failure conditions: | ||
- any read value does not match documented PoR | ||
- any illegal instruction exceptions | ||
|
||
### 2 | ||
Same as [1](#1) but first enter debug mode and then attempt to read all | ||
machine-mode and debug-mode registers | ||
|
||
### 3 | ||
Similar to [1](#1) with added accesses between address ranges of existing | ||
machine-mode CSRs. For example, address range 0x307 : 0x33F between Machine | ||
Trap Setup CSRs and Machine Trap Handling CSRs. | ||
|
||
### 4 | ||
Access mode test of all CSRs. This is a generated test based on [cv32e40p_csr_template.yaml](https://github.com/openhwgroup/core-v-verif/blob/master/vendor_lib/google/corev-dv/cv32e40p_csr_template.yaml). | ||
|
||
### 5 | ||
Same as [4](#4), run in Debug mode. Add access mode testing of Debug CSRs. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
The Verification Plan (aka Test Plan) documents for CV32E40P features related to the [RISC-V Privleged Specification](https://riscv.org/specifications/privileged-isa/). |
Binary file added
BIN
+10.1 KB
...s/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-bitmanipulations.xlsx
Binary file not shown.
Binary file added
BIN
+11.5 KB
...p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-general-alu.xlsx
Binary file not shown.
Binary file added
BIN
+9.13 KB
cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-hwloop.xlsx
Binary file not shown.
Binary file added
BIN
+8.88 KB
...erifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-immediate-branching.xlsx
Binary file not shown.
Binary file added
BIN
+11.3 KB
...erifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-multiply-accumulate.xlsx
Binary file not shown.
Binary file added
BIN
+22.5 KB
...p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-packed-simd.xlsx
Binary file not shown.
Binary file added
BIN
+10.6 KB
.../VerifPlans/Simulation/xpulp_instruction_extensions/CV32E40P_xpulp-postinc-loadstore.xlsx
Binary file not shown.
4 changes: 4 additions & 0 deletions
4
cv32e40p/docs/VerifPlans/Simulation/xpulp_instruction_extensions/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
## Verification (Test) Plans for the XPULP Instruction Extension | ||
At the time of this writting (2019-12-21), only the plan for Bit Manipulation Instructions has been published here. The plan is in both Excel (xlsx) and Markdown (md) formats. Also, the Excel format has multiple tabs to illustrate two different styles of recording features in a verificaiton plan. | ||
|
||
Send an email to mike@openhwgroup.org if you have a preference. Otherwise he'll pick _his_ favorite. |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
<!--- SPDX-License-Identifier: Apache-2.0 WITH SHL-2.0 ---> | ||
This is the root directory of the CV32E40X Verification Plan (aka Test Plan). | ||
Each sub-directory is the verification plan for a specific CV32E40X high-level feature of the same name. | ||
|
||
Use the provided CORE-V_Simulation VerifPlan_Template.xlsx spreadsheet as your template to capture a Verification Plan. | ||
|
||
## Verification Plan Status | ||
|
||
The tables below capture the current status of the Verification Plan for the CV32E40P by high-level feature. Under the heading `Review` is one of following: | ||
* **Ready for Review**: Vplan has been captured and is awaiting review. | ||
* **Reviewed**: Vplan has been reviewed, and is waiting for updates to address review feedback. | ||
* **Waiting for Signoff**: Vplan has been reviewed and review comments addressed by the author. Document is now waiting for reviewers to signoff on the post-review updates. | ||
* **Complete**: Post-preview updates have been signed-off. | ||
|
||
### Base instruction set plus standard instruction extensions | ||
|
||
_Refer to the VerifPlans/ISA/RV32/Simulation directory for specific Verification Plan status for each supported extension._ | ||
### Interrupts | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| CLINT | Incomplete | Incomplete | | | ||
|
||
### Debug & Trigger | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| Debug | Incomplete | Incomplete | | | ||
| Trigger module | Incomplete | Incomplete | | | ||
|
||
### Privileged spec | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| CSRs | Incomplete | Incomplete | | | ||
| PMA | Incomplete | Incomplete | | | ||
| User mode | N/A| N/A | Not a CV32E40X Feature | | ||
|
||
### Micro-architecure | ||
|
||
| Feature | Capture | Review | Comment | | ||
|---------|---------|--------|---------| | ||
| OBI | Inomplete | Incomplete | | | ||
| Sleep Unit | Incomplete | Incomplete | | | ||
| Pipelines | Incomplete | Incomplete | | | ||
|
Binary file not shown.
2 changes: 2 additions & 0 deletions
2
cv32e40x/docs/VerifPlans/Simulation/custom_circuitry/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
Placeholder directory for a specific CV32E40X high-level feature. | ||
The Verification Plan (aka Test Plan) for this feature will be committed here as soon as is available. |
Binary file not shown.
Binary file added
BIN
+16.5 KB
cv32e40x/docs/VerifPlans/Simulation/debug-trace/CV32E40X_external-debugger.xlsx
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Directory for the CV32E40XVerification Plan for Debug and associated documentation. Note that only `CV32E40X_Debug` is relevant to the current release of CV32E40X. |
Binary file added
BIN
+29.5 KB
cv32e40x/docs/VerifPlans/Simulation/interrupts/CV32E40X_interrupts.xlsx
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Directory for the CV32E40X Verification Plan for Interrupts and associated documentation. |
Binary file added
BIN
+15.9 KB
cv32e40x/docs/VerifPlans/Simulation/micro_architecture/CV32E40X_OBI_VerifPlan.xlsx
Binary file not shown.
Binary file added
BIN
+13.1 KB
cv32e40x/docs/VerifPlans/Simulation/micro_architecture/CV32E40X_Pipeline_Sleep.xlsx
Binary file not shown.
1 change: 1 addition & 0 deletions
1
cv32e40x/docs/VerifPlans/Simulation/micro_architecture/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Verification Plans for CV32E40X micro-architecture and physical interfaces. |
Oops, something went wrong.