[doc] Design and verification stages documented by marnovandermaas · Pull Request #502 · lowRISC/mocha

marnovandermaas · 2026-04-29T09:53:38Z

This PR also adds checklists for D1 and V1 stages as well as a sign-off procedure.

Closes: #479

martin-velay · 2026-04-29T12:47:48Z

+
+This table shows the current design and verification stage for each block in Mocha.
+
+| **Block name**    | **Design stage** | **Verification stage** |


Don't we need JTAG too?

I had considered that to be part of the debug module.

martin-velay · 2026-04-29T12:54:33Z

+
+## Sign-off procedure
+
+To advance a block from one stage to the next you must open a pull request with the checklist in a markdown file called `doc/verif/BLOCK.md`, where `BLOCK` is replaced by the block's name.


I was slightly confused with the location. And I'd prefer having that into a checklist directory as it's not only a verification thing but a design too.

Suggested change

To advance a block from one stage to the next you must open a pull request with the checklist in a markdown file called `doc/verif/BLOCK.md`, where `BLOCK` is replaced by the block's name.

To advance a block from one stage to the next you must open a pull request with the checklist in a Markdown file called `mocha/doc/checklist/BLOCK.md`, where `BLOCK` is replaced by the block's name.

Also, what do we do with the OT checklists, shall we remove them to avoid the confusion?

Or maybe we can call this directory maturity?

I agree it's confusing having design checklists in a verif directory. What about proj short for "project" which is a reference to the project governance documentation in OpenTitan?

It might be useful to keep the OpenTitan checklists in tree to be able to reference them? I'm not sure whether this is useful until I actually do a sign-off though.

martin-velay · 2026-04-29T12:55:37Z

+## Sign-off procedure
+
+To advance a block from one stage to the next you must open a pull request with the checklist in a markdown file called `doc/verif/BLOCK.md`, where `BLOCK` is replaced by the block's name.
+This pull request must be approved by at least three people, one of whom should be from a different organisation than the author.


If I understand well, we need a cross-functional approval: SW+DD+DV?

Yes, this is the ideal scenario. Also it would be nice if there is someone involved from a different organisation. I think I don't want to be too prescriptive in the sign-off procedure though.

martin-velay · 2026-04-29T14:01:46Z

+
+## Verification stages
+
+These are the verification stages each block goes through in case a **simulation-based approach** is taken.


Each block could be mixture of simulation and formal approaches. Let me try to make a proposal which works for both

It's not yet 100% correct, but most of it is there. I need to review it again later, as my brain needs some rest. WDYT in general?

Verification stages

A block may be verified using simulation, formal-property verification (FPV), or a mix of the two.
The stages and checklist below are methodology-neutral: the verification plan declares, per vPlan item (also referred as verification point), which methodology covers it, and the checklist items are then applied accordingly.

Verification documentation

Two documents are required for every block. Both are initiated at V0 and must be completed and reviewed for V1 sign-off.

Verification plan (vPlan) - what must be verified.
Lists features, and the required vPlan items to cover each feature. And also for each vPlan item, the methodology which will be used to covers it.
Reviewing the vPlan is a substantial task and must involve all stakeholders (system, design, DV, software, security, integration), since it locks in the scope of verification for the block.

Verification strategy - how it will be verified.
Describes the tools, testbench / formal-environment architecture, specific tests, stimuli, assumptions, and procedures used to meet the objectives set out in the verification plan.

Stage definitions

Stage Name Definition

V0 Initial Work

Verification plan and verification strategy being created
Methodology being decided per feature (simulation, FPV, or both)
Testbench and/or formal environment skeleton created (not yet functional)
Define DV specific requirements for the Continuous Integration (CI) pipeline

V1 Initial Testing

Documentation:

Verification Plan completed and reviewed (involves all stakeholders)
Verification Strategy being drafted

Testbench:

Verification environment / formal flow in place for initial testing
Initial functional coverage model bound in
VIPs / agents: main are ready and secondary are at least specified
Device Under Test (DUT) instantiated with major interfaces hooked up
Available interface assertion checkers hooked up
X / unknown checks on DUT outputs added

Tests / assertions: Interfaces and Sanity

Register / memory test suite completed
Sanity tests / assertions accessing the main functional paths
Connectivity checks

Regressions set up: sanity and nightly

V2 Complete Testing

Documentation:

Verification Strategy completed and reviewed
Verification Plan kept up to date with any in-flight changes

Design issues:

All high-priority bugs addressed
Low-priority bugs root-caused, tracked as issues, and triaged for V3

Environment:

Verification environment fully developed: scoreboard with end-to-end checks, reference / predictor models integrated
All interfaces exercised (if applicable: with protocol checkers enabled)
All FPV assumptions specified and reviewed

Tests / assertions:

≥ 90% of vPlan items implemented (sim tests / formal assertions) and passing
Functional covergroups implemented for the items covered so far

Regression:

Sim: nightly regression with multiple seeds, > 90% passing
Formal: ≥ 90% of properties proven in nightly regression

Coverage:

Sim: ≥ 90% code coverage and ≥ 90% functional coverage; gaps documented (not yet waived)
Formal: ≥ 90% code coverage and ≥ 75% cone-of-influence (COI) coverage

V3 Verification Complete

Documentation: Verification Plan and Verification Strategy final, reviewed, and signed off
Design issues:

All bugs fixed, or formally waived with sign-off
No open verification-blocking issues

Environment:

No outstanding TODOs in the environment
All assertions enabled; any disabled assertions documented and reviewed
FPV assumptions finalised and reviewed

Tests / assertions:

All vPlan items, including any post-V2 additions, implemented and passing
Error and corner-case scenarios exercised
All functional covergroups defined in the vPlan implemented

Regression:

Sim: 100% pass rate on all seeds, sustained over several consecutive nightly runs
Formal: 100% of properties proven with reviewed assumptions

Coverage:

Sim: 100% code and 100% functional coverage, with reviewed waivers
Formal: 100% code and 100% COI coverage, with reviewed waivers

V1 verification sign-off checklist

Each item below has an Applies to column:

Both - required regardless of methodology.

Sim - required if the verification plan assigns any vPlan item to simulation.

Formal - required if the verification plan assigns any vPlan item to FPV.

Items whose methodology is not used by the block are recorded as N/A. The
methodology mix declared in the V1 verification plan is locked at V1 sign-off;
changing it later requires a new vPlan review.

Item name Applies to Description

DV_PLAN_COMPLETED Both Verification plan drafted: full feature list organised into sections, with their associated coverage methodology (sim / formal / both). At this stage we don't expect to have all vPlan items defined.

DV_STRATEGY_COMPLETED Both Verification strategy drafted: tools, environment architecture, specific tests, stimuli, assumptions, and procedures used to meet the verification plan objectives.

DV_PLAN_REVIEWED Both Verification plan reviewed by all stakeholders (system, design, DV, software, security, integration).

DV_STRATEGY_REVIEWED Both Verification strategy reviewed.

DESIGN_SPEC_REVIEWED Both Design specification reviewed from a verification perspective.

PRE_VERIFIED_SUB_MODULES_V1 Both Pre-verified sub-modules must also have reached V1.

SIM_SMOKE_TEST_PASSING Sim Smoke test passing in simulation with a particular seed.

SIM_SMOKE_REGRESSION_SETUP Sim Smoke regression tests selected and defined.

SIM_NIGHTLY_REGRESSION_SETUP Sim Nightly regression tests selected and defined.

SIM_COVERAGE_MODEL_ADDED Sim Initial functional coverage model bound in.

FPV_MAIN_ASSERTIONS_PROVEN Formal Main functional-path assertions implemented and proven. Each input and each output of the module is part of at least one assertion.

FPV_REGRESSION_SETUP Formal FPV regression set up and added to top_chip_fpv_ip_cfgs.hjson.

V2 and V3 checklists to be added.

Good idea to add the "applies to" column. I've now added that. I've also tried to reduce the duplication between formal and the simulation tables but don't want to change the wording too much so that we can re-use OpenTitan sign-offs.

Ok, I've now also had a go at combining the simulation and formal tables.

martin-velay · 2026-04-29T15:28:29Z

+| SPEC_COMPLETED | Specification is 90% complete. |
+| CSR_DEFINED | Registers defined for the primary programming model. |
+| CLKRST_CONNECTED | Clock and reset connected to all submodules. |
+| IP_TOP | There is an IP top that can be included in the top design. |


Is this item related to the "ports frozen" item you've listed above?

Interesting, this was a copy from OpenTitan. I've removed the port frozen requirement because I think it is kind of unnecessary to re-do a D1 sign-off when an extra signal is added to the top.

martin-velay · 2026-04-29T15:33:33Z

+
+| **Item name** | **Description** |
+|---------------|-----------------|
+| SPEC_COMPLETED | Specification is 90% complete. |


Another point about specs, we should probably define the specs we are expecting: system spec (if applicable), detailed design spec (micro-architectural spec), others?

I think we should leave this up to the judgement of those making the sign-offs. If a micro-architectural spec is necessary then it should be included. I'm not sure what you mean by a system spec when doing a block-level sign-off.

Yes, the word system spec is confusing, it comes from my previous company doc flow.
The system spec was the high level doc where you describe the HW interface, the CSRs, the algos... this doc were derived from the requirements and made by the leads with the system team. Then based on this system spec, the design team were making their design spec (micro architectural description), and so DV team with their vPlan (note that the vPlan also contains elements from the design spec)

martin-velay · 2026-04-29T15:39:23Z

+
+| **Item name** | **Description** |
+|---------------|-----------------|
+| DV_DOC_DRAFT_COMPLETED | Verification document drafted with overall goal and strategy. |


We must have 2 docs:

Verification Plan: lists what should be verified

Verification Strategy: focuses on how to verify, detailing the tools, specific tests, stimuli and procedures to be followed to achieve the objectives set out in the verification plan...

They should be initiated from V0 and completed with reviews in V1. Note that reviewing the vPlan is a big task as it should involve all the stakeholders.

Although I am not opposed to having two documents in general, I am careful to make this a requirement specifically for blocks that we are importing from OpenTitan. We need to be able to re-use the sign-offs we did there otherwise we will not be able to reach our project timelines.

Yes, you're probably right on that point, I described more what it should be without considering project timelines. Something to discuss further though for OT too

martin-velay · 2026-04-30T09:08:41Z

+|-----------|----------|----------------|
+| D0  | Initial Work | RTL being developed, not functional. |
+| D1  | Functional | <ul> <li> Feature set finalized, spec complete </li> <li> CSRs identified; RTL/DV/SW collateral generated </li> <li> SW interface automation completed </li> <li> Clock(s) and reset(s) connected to all sub modules </li> <li> Lint run setup </li> <li> Ports frozen </li> </ul> |
+| D2  | Feature Complete | <ul> <li> All features implemented </li> <li> Feature frozen </li> </ul> |


A missing point: at this stage the UNR (auto-exclusion) flow should be in place and in D3 all auto-exclusions should have been reviewed. Also the manual exclusions should also be mentioned somewhere in D3 I believe

This is not part of the OpenTitan checklist so I would prefer not to mandate it.

This commit also adds checklists for D1 and V1 stages as well as a sign-off procedure. It also introduces a table with the status for each block.

marnovandermaas requested review from jayalp, johngt and martin-velay April 29, 2026 09:53

marnovandermaas force-pushed the checklists branch from 8b429d6 to 3772433 Compare April 29, 2026 12:06

johngt reviewed Apr 29, 2026

View reviewed changes

Comment thread doc/proj/stages.md

marnovandermaas force-pushed the checklists branch 2 times, most recently from e88fa55 to 100eb2a Compare April 30, 2026 08:14

martin-velay reviewed Apr 30, 2026

View reviewed changes

marnovandermaas force-pushed the checklists branch from 100eb2a to 44b3e22 Compare April 30, 2026 08:25

martin-velay reviewed Apr 30, 2026

View reviewed changes

marnovandermaas force-pushed the checklists branch 13 times, most recently from 699200e to 403c8d5 Compare May 12, 2026 10:32

[doc] Design and verification stages documented

18574dc

This commit also adds checklists for D1 and V1 stages as well as a sign-off procedure. It also introduces a table with the status for each block.

marnovandermaas force-pushed the checklists branch from 403c8d5 to 18574dc Compare May 12, 2026 10:36


		This table shows the current design and verification stage for each block in Mocha.

		\| Block name \| Design stage \| Verification stage \|


		## Sign-off procedure

		To advance a block from one stage to the next you must open a pull request with the checklist in a markdown file called `doc/verif/BLOCK.md`, where `BLOCK` is replaced by the block's name.


		## Verification stages

		These are the verification stages each block goes through in case a simulation-based approach is taken.

Stage	Name	Definition
V0	Initial Work	Verification plan and verification strategy being created Methodology being decided per feature (simulation, FPV, or both) Testbench and/or formal environment skeleton created (not yet functional) Define DV specific requirements for the Continuous Integration (CI) pipeline
V1	Initial Testing	Documentation: Verification Plan completed and reviewed (involves all stakeholders) Verification Strategy being drafted Testbench: Verification environment / formal flow in place for initial testing Initial functional coverage model bound in VIPs / agents: main are ready and secondary are at least specified Device Under Test (DUT) instantiated with major interfaces hooked up Available interface assertion checkers hooked up X / unknown checks on DUT outputs added Tests / assertions: Interfaces and Sanity Register / memory test suite completed Sanity tests / assertions accessing the main functional paths Connectivity checks Regressions set up: sanity and nightly
V2	Complete Testing	Documentation: Verification Strategy completed and reviewed Verification Plan kept up to date with any in-flight changes Design issues: All high-priority bugs addressed Low-priority bugs root-caused, tracked as issues, and triaged for V3 Environment: Verification environment fully developed: scoreboard with end-to-end checks, reference / predictor models integrated All interfaces exercised (if applicable: with protocol checkers enabled) All FPV assumptions specified and reviewed Tests / assertions: ≥ 90% of vPlan items implemented (sim tests / formal assertions) and passing Functional covergroups implemented for the items covered so far Regression: Sim: nightly regression with multiple seeds, > 90% passing Formal: ≥ 90% of properties proven in nightly regression Coverage: Sim: ≥ 90% code coverage and ≥ 90% functional coverage; gaps documented (not yet waived) Formal: ≥ 90% code coverage and ≥ 75% cone-of-influence (COI) coverage
V3	Verification Complete	Documentation: Verification Plan and Verification Strategy final, reviewed, and signed off Design issues: All bugs fixed, or formally waived with sign-off No open verification-blocking issues Environment: No outstanding TODOs in the environment All assertions enabled; any disabled assertions documented and reviewed FPV assumptions finalised and reviewed Tests / assertions: All vPlan items, including any post-V2 additions, implemented and passing Error and corner-case scenarios exercised All functional covergroups defined in the vPlan implemented Regression: Sim: 100% pass rate on all seeds, sustained over several consecutive nightly runs Formal: 100% of properties proven with reviewed assumptions Coverage: Sim: 100% code and 100% functional coverage, with reviewed waivers Formal: 100% code and 100% COI coverage, with reviewed waivers

Item name	Applies to	Description
DV_PLAN_COMPLETED	Both	Verification plan drafted: full feature list organised into sections, with their associated coverage methodology (sim / formal / both). At this stage we don't expect to have all vPlan items defined.
DV_STRATEGY_COMPLETED	Both	Verification strategy drafted: tools, environment architecture, specific tests, stimuli, assumptions, and procedures used to meet the verification plan objectives.
DV_PLAN_REVIEWED	Both	Verification plan reviewed by all stakeholders (system, design, DV, software, security, integration).
DV_STRATEGY_REVIEWED	Both	Verification strategy reviewed.
DESIGN_SPEC_REVIEWED	Both	Design specification reviewed from a verification perspective.
PRE_VERIFIED_SUB_MODULES_V1	Both	Pre-verified sub-modules must also have reached V1.
SIM_SMOKE_TEST_PASSING	Sim	Smoke test passing in simulation with a particular seed.
SIM_SMOKE_REGRESSION_SETUP	Sim	Smoke regression tests selected and defined.
SIM_NIGHTLY_REGRESSION_SETUP	Sim	Nightly regression tests selected and defined.
SIM_COVERAGE_MODEL_ADDED	Sim	Initial functional coverage model bound in.
FPV_MAIN_ASSERTIONS_PROVEN	Formal	Main functional-path assertions implemented and proven. Each input and each output of the module is part of at least one assertion.
FPV_REGRESSION_SETUP	Formal	FPV regression set up and added to `top_chip_fpv_ip_cfgs.hjson`.

Conversation

marnovandermaas commented Apr 29, 2026

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Verification stages

Verification documentation

Stage definitions

V1 verification sign-off checklist

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants