Skip to content

Commit

Permalink
Trap DV plan: update after internal review
Browse files Browse the repository at this point in the history
Signed-off-by: André Sintzoff <[email protected]>
  • Loading branch information
ASintzoff committed Nov 10, 2023
1 parent 619c0c4 commit ba90355
Show file tree
Hide file tree
Showing 12 changed files with 253 additions and 243 deletions.
155 changes: 93 additions & 62 deletions verif/docs/VerifPlans/source/dvplan_traps.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@

#### Item: 000

* **Requirement location:** Unprivileged ISA Version 20191213, Chapter 1.5
* **Requirement location:** Unprivileged ISA Version 20191213, Chapter 2.2
* **Feature Description**

Opcodes that do not decode to a valid, supported instruction for the CVA6 core configuration shall raise an illegal instruction exception.
The behavior upon decoding a reserved instruction is unspecified. Opcodes that do not decode to a valid, supported instruction for the CVA6 core configuration shall raise an illegal instruction exception.
* **Verification Goals**

Check that when executing any illegal instruction, an exception is raised with `mcause` CSR set to 0x2.
Check that when executing any illegal instruction, an exception is raised with `mcause` set to 0x2.
* **Pass/Fail Criteria:** Check RM
* **Test Type:** Constrained Random
* **Coverage Method:** Code Coverage
Expand All @@ -21,30 +21,27 @@
* **Link to Coverage:**
* **Comments**

Covered by ISACOV
## Feature: Load x0

### Sub-feature: 000_load_x0
Covered by ISACOV tests, not yet in ISACOV DV plan
### Sub-feature: 001_mtval

#### Item: 000

* **Requirement location:** Unprivileged ISA Version 20191213, Chapter 2.6
* **Requirement location:** Privileged Architecture Version 20211203, Chapter 3.1.16
* **Feature Description**

`x0` register cannot have a value loaded into it but does not generate an exception when that is attempted, as the exception is not implemented.
When an illegal instruction exception is raised, the corresponding instruction is stored into `mtval` CSR.
* **Verification Goals**

Check that loading to `x0` register does not cause an exception.
* **Pass/Fail Criteria:** Check RM
* **Test Type:** Constrained Random
* **Coverage Method:** Functional Coverage
Check that when any illegal instruction exception is raised, `mtval` CSR contains the faulting instruction.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Unique verification tag:** VP_traps_F001_S000_I000
* **Unique verification tag:** VP_traps_F000_S001_I000
* **Link to Coverage:**
* **Comments**

*(none)*

ZERO_TVAL parameter value?
## Feature: CSR Access

### Sub-feature: 000_CSR_access
Expand All @@ -67,7 +64,8 @@
* **Comments**

Covered by CSR DV plan.
Verify if `mcause` value check is covered by CSR DV plan.
VP_csr-embedded-access_F001_S002_I000
Verify if `mcause` value check is covered by CSR tests.
#### Item: 001

* **Requirement location:** Privileged Architecture Version 20211203, Chapter 2.1
Expand All @@ -86,7 +84,8 @@
* **Comments**

Covered by CSR DV plan.
Verify if `mcause` value check is covered by CSR DV plan.
VP_csr-embedded-access_F001_S001_I000
Verify if `mcause` value check is covered by CSR tests.
## Feature: Machine Trap Vector

### Sub-feature: 000_mtvec
Expand All @@ -110,29 +109,6 @@

*(none)*

## Feature: Machine Cause

### Sub-feature: 000_mcause

#### Item: 000

* **Requirement location:** Privileged Architecture Version 20211203, 3.1.15
* **Feature Description**

`mcause` is set to exception cause upon entry into exception.
* **Verification Goals**

Check that `mcause` correctly identifies the exception taken.
* **Pass/Fail Criteria:** Check RM
* **Test Type:** Constrained Random
* **Coverage Method:** Functional Coverage
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Unique verification tag:** VP_traps_F004_S000_I000
* **Link to Coverage:**
* **Comments**

*(none)*

## Feature: Machine Exception Program Counter

### Sub-feature: 000_mepc
Expand Down Expand Up @@ -255,21 +231,23 @@
- code=0x8, 0x9, 0xB: Environment call from U-mode, from S-mode, from M-mode
- code=0x3: Environment break
- code=0x3: Load/store/AMO address breakpoint
- code=0x4, 0x6: Load address misaligned, store/AMO address misaligned (CHECK IF NOT LOWEST PRIORITY ON CVA6)
- code=0xD, 0xF, 0x5, 0x7: Load page fault, store/AMO page fault, load access fault, store/AMO access fault
- code=0xD, 0xF, 0x5, 0x7: Load page fault, store/AMO page fault, load access fault, store/AMO access fault
- code=0x4, 0x6: Load address misaligned, store/AMO address misaligned
* **Verification Goals**

Check that when raising an exception together with a lower priority one the cause of the higher priority exception is written in `mcause` register.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** Directed Non-SelfChk
* **Coverage Method:** Testcase
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F007_S000_I000
* **Link to Coverage:**
* **Comments**

*(none)*

### Sub-feature: 001_exception priority embedded

## Feature: Address Misaligned

### Sub-feature: 000_instr_misaligned
Expand Down Expand Up @@ -325,7 +303,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F008_S001_I001
* **Link to Coverage:**
* **Comments**
Expand Down Expand Up @@ -365,7 +343,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F008_S002_I001
* **Link to Coverage:**
* **Comments**
Expand All @@ -380,17 +358,37 @@
If not aligned AMO is attempted, a store/AMO access misaligned exception is taken.
* **Verification Goals**

Exception is entered with mcause set to 0x6.
Exception is entered with `mcause` set to 0x6.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F008_S002_I002
* **Link to Coverage:**
* **Comments**

*(none)*

### Sub-feature: 003_mtval

#### Item: 000

* **Requirement location:** Privileged Architecture Version 20211203, Chapter 3.1.16
* **Feature Description**

When an address misaligned exception is raised, the corresponding address is stored into `mtval` CSR.
* **Verification Goals**

Check that when any address misaligned exception is raised, `mtval` CSR contains the address of the portion of the access causing the fault.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Unique verification tag:** VP_traps_F008_S003_I000
* **Link to Coverage:**
* **Comments**

ZERO_TVAL parameter value?
## Feature: Access Fault

### Sub-feature: 000_instr_access
Expand Down Expand Up @@ -465,7 +463,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F009_S001_I001
* **Link to Coverage:**
* **Comments**
Expand Down Expand Up @@ -505,7 +503,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F009_S002_I001
* **Link to Coverage:**
* **Comments**
Expand All @@ -524,13 +522,33 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F009_S002_I002
* **Link to Coverage:**
* **Comments**

*(none)*

### Sub-feature: 003_mtval

#### Item: 000

* **Requirement location:** Privileged Architecture Version 20211203, Chapter 3.1.16
* **Feature Description**

When an access fault exception is raised, the corresponding address is stored into `mtval` CSR.
* **Verification Goals**

Check that when any access fault exception is raised, `mtval` CSR contains the address of the portion of the access causing the fault.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Unique verification tag:** VP_traps_F009_S003_I000
* **Link to Coverage:**
* **Comments**

ZERO_TVAL parameter value?
## Feature: Environment Call

### Sub-feature: 000_ecall
Expand Down Expand Up @@ -566,7 +584,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F010_S000_I001
* **Link to Coverage:**
* **Comments**
Expand All @@ -585,7 +603,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F010_S000_I002
* **Link to Coverage:**
* **Comments**
Expand All @@ -608,7 +626,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F011_S000_I000
* **Link to Coverage:**
* **Comments**
Expand All @@ -628,7 +646,7 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F011_S001_I000
* **Link to Coverage:**
* **Comments**
Expand All @@ -648,17 +666,30 @@
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F011_S002_I000
* **Link to Coverage:**
* **Comments**

MMU related
## Feature: Breakpoint

### Sub-feature: 000_instr_bkp

### Sub-feature: 001_data_bkp
### Sub-feature: 003_mtval

### Sub-feature: 002_environment_break
#### Item: 000

* **Requirement location:** Privileged Architecture Version 20211203, Chapter 3.1.16
* **Feature Description**

When an page fault exception is raised, the corresponding address is stored into `mtval` CSR.
* **Verification Goals**

Check that when any page fault exception is raised, `mtval` CSR contains the address of the portion of the access causing the fault.
* **Pass/Fail Criteria:** NDY (Not Defined Yet)
* **Test Type:** NDY (Not Defined Yet)
* **Coverage Method:** NDY (Not Defined Yet)
* **Applicable Cores:** CV32A6_v0.1.0, CV64A6-step3
* **Unique verification tag:** VP_traps_F011_S003_I000
* **Link to Coverage:**
* **Comments**

MMU related
ZERO_TVAL parameter value?
37 changes: 31 additions & 6 deletions verif/docs/VerifPlans/traps/VP_IP000.yml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
!Feature
next_elt_id: 1
next_elt_id: 2
name: Illegal Instruction
id: 0
display_order: 0
Expand All @@ -13,21 +13,46 @@ subfeatures: !!omap
- '000': !VerifItem
name: '000'
tag: VP_traps_F000_S000_I000
description: Opcodes that do not decode to a valid, supported instruction
for the CVA6 core configuration shall raise an illegal instruction exception.
reqt_doc: Unprivileged ISA Version 20191213, Chapter 1.5
description: The behavior upon decoding a reserved instruction is unspecified.
Opcodes that do not decode to a valid, supported instruction for the CVA6
core configuration shall raise an illegal instruction exception.
reqt_doc: Unprivileged ISA Version 20191213, Chapter 2.2
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: Check that when executing any illegal instruction, an exception
is raised with `mcause` CSR set to 0x2.
is raised with `mcause` set to 0x2.
pfc: 3
test_type: 3
cov_method: 3
cores: 56
coverage_loc: ''
comments: Covered by ISACOV
comments: Covered by ISACOV tests, not yet in ISACOV DV plan
- 001_mtval: !Subfeature
name: 001_mtval
tag: VP_traps_F000_S001
next_elt_id: 1
display_order: 1
items: !!omap
- '000': !VerifItem
name: '000'
tag: VP_traps_F000_S001_I000
description: When an illegal instruction exception is raised, the corresponding
instruction is stored into `mtval` CSR.
reqt_doc: Privileged Architecture Version 20211203, Chapter 3.1.16
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: Check that when any illegal instruction exception is raised,
`mtval` CSR contains the faulting instruction.
pfc: -1
test_type: -1
cov_method: -1
cores: 56
coverage_loc: ''
comments: ZERO_TVAL parameter value?
vptool_gitrev: '$Id: b0efb3ae3f9057b71a577d43c2b77f1cfb2ef82f $'
io_fmt_gitrev: '$Id: 7ee5d68801f5498a957bcbe23fcad87817a364c5 $'
config_gitrev: '$Id: 0422e19126dae20ffc4d5a84e4ce3de0b6eb4eb5 $'
Expand Down
Loading

0 comments on commit ba90355

Please sign in to comment.