forked from openhwgroup/programs
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request openhwgroup#310 from ntuszynski/master
FV Checklist Update
- Loading branch information
Showing
1 changed file
with
16 additions
and
16 deletions.
There are no files selected for viewing
32 changes: 16 additions & 16 deletions
32
program/milestones/CV32E40P/RTL_Freeze_v1.0.0/FormalVerificationChecklist.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 |
|---|---|---|
| @@ -1,16 +1,16 @@ | ||
| ## Formal Verification Checklist for Functional RTL Freeze | ||
| An item is "signed off" once the `Signed-off By` and `Sign-off Date` cells are filled in. `Signed-off By` should be an email address. If there is an Exception or Waiver, it should be captured as a GitHub issue in core-v-verif and the issue number recorded in the `Exceptions/Waiver/Comment` cell. | ||
|
|
||
| | Category | Item | Sign-off Criteria | Signed-off By | Sign-off Date | Exceptions/Waivers/Comments | | ||
| | --------------------- | -------------------------------- | ------------------------------------------------------ | --------------------------- | ------------- | ------------------------------------------ | | ||
| | Verification Planning | RV32I Vplan | Completed, reviewed and up-issued per review | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32C Vplan | Completed, reviewed and up-issued per review | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32M Vplan | Completed, reviewed and up-issued per review | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32Zicsr_Zifencei Vplan | Completed, reviewed and up-issued per review | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32IMC Exceptions Vplan | Completed, reviewed and up-issued per review | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | Formal Testbench Cross-reference | Each item in Vplan cross-ref’ed to assertions | sven.beyer@onespin.com | yyyy-mm-dd | Captured as cv32e40p GitHub issues | | ||
| | Regression | Formal Testbench | All assertions hold unbounded with reachable witnesses | [email protected] | yyyy-mm-dd | Partial results for M Extension Assertions | | ||
| | Final Report | Axiomise RISC-V Formal Toolkit | Posted to GitHub | [email protected] | 2020-12-03 | Filed in "Reports" directory | | ||
| | Final Report | Verification Plans | | sven.beyer@onespin.com | yyyy-mm-dd | | | ||
| | Final Report | Regression Results | | [email protected] | yyyy-mm-dd | | | ||
| | Final Report | Coverage Results | | [email protected] | yyyy-mm-dd | | | ||
| ## Formal Verification Checklist for Functional RTL Freeze | ||
| An item is "signed off" once the `Signed-off By` and `Sign-off Date` cells are filled in. `Signed-off By` should be an email address. If there is an Exception or Waiver, it should be captured as a GitHub issue in core-v-verif and the issue number recorded in the `Exceptions/Waiver/Comment` cell. | ||
|
|
||
| | Category | Item | Sign-off Criteria | Signed-off By | Sign-off Date | Exceptions/Waivers/Comments | | ||
| | --------------------- | -------------------------------- | ------------------------------------------------------ | --------------------------- | ------------- | ------------------------------------------ | | ||
| | Verification Planning | RV32I Vplan | Completed, reviewed and up-issued per review | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32C Vplan | Completed, reviewed and up-issued per review | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32M Vplan | Completed, reviewed and up-issued per review | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32Zicsr_Zifencei Vplan | Completed, reviewed and up-issued per review | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | RV32IMC Exceptions Vplan | Completed, reviewed and up-issued per review | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Verification Planning | Formal Testbench Cross-reference | Each item in Vplan cross-ref’ed to assertions | nicolae.tusinschi@onespin.com | 2020-12-10 | Captured as cv32e40p GitHub issues | | ||
| | Regression | Formal Testbench | All assertions hold unbounded with reachable witnesses | [email protected] | 2020-12-10 | Partial results for M Extension Assertions | | ||
| | Final Report | Axiomise RISC-V Formal Toolkit | Posted to GitHub | [email protected] | 2020-12-03 | Filed in "Reports" directory | | ||
| | Final Report | Verification Plans | RV32: I,M,C,Zicsr_Zfencei, Xcpt vPlans in GitHub | nicolae.tusinschi@onespin.com | 2020-12-10 | | | ||
| | Final Report | Regression Results | | [email protected] | yyyy-mm-dd | | | ||
| | Final Report | Coverage Results | | [email protected] | yyyy-mm-dd | | |