V&V summary and checks

Verification and validation (V&V) is the evidence that a design does what it should and that the chip made from it can be manufactured. The project's V&V tab gathers every check the lab has for the project in one table, one row per check, so you can see at a glance what was measured, what failed, and what has not been run at all.

Open it from the project's tab row (Overview · Chip Layout · Code · Runs & Compare · Results & export · V&V).

What a row says#

The lab never shows pass for something it did not measure. A check the build did not record is not run; a check that does not exist for a process (for example LVS on the ASAP7 teaching process) is unsupported.

Where the rows come from#

• Build rows (DRC per rule deck, LVS, antenna, timing at every corner, electrical rule checks, IR drop, GDS stored, synthesis netlist and area) are read from the latest chip build's stored report, results and metrics. One row per timing corner shows the worst setup and hold slack there. If a build passed while a corner is violated, the build row says so and the corner row is fail.
• Simulation shows the latest run of all tests with the names of the tests that passed and failed. When the lab only recorded "Tool exited with code N", the row shows the first real error line from the stored log instead.
• Formal, line/branch coverage and toggle coverage are the latest runs from the Verification page.
• Lint and RTL vs synthesized netlist are the two new checks described below. Checks added later appear here automatically.

Download evidence index gives the same rows as a JSON file (<project>-vv-evidence.json), and /app/projects/<project>/vv.json serves it live.

Lint (Verilator 5.044, --lint-only -Wall)#

Lint reads your RTL the way a strict compiler would and reports anything that usually means the chip will not do what the code says: a latch where you wanted combinational logic, a width mismatch, a signal driven from two places, an incomplete case. Every finding comes with file, line and column.

• The row is fail when Verilator reports an error, or a warning in the fail on set. The default set is WIDTH, LATCH, MULTIDRIVEN, UNOPTFLAT, CASEINCOMPLETE, BLKSEQ, COMBDLY; you can choose errors only or every warning before pressing Run.
• Other warnings are listed as informational and do not fail the row.
• The full Verilator log is kept and linked.
• Limits: VHDL-only projects are unsupported (the lint image has no ghdl). Mixed Verilog + VHDL projects: the Verilog part is linted and the row says so. Lint runs on the files your openlane/config.json lists (or every file in rtl/); it does not change them.

RTL vs synthesized netlist (equivalence)#

After synthesis the chip is described as a netlist of standard cells. This check proves that the netlist your latest finished build kept (netlist.synthesis.v) is the same logic as your RTL. Since 31 October 2026 a build that ran to the end and failed only its sign-off checks (DRC, LVS, antenna) counts too; the result then says so. It runs the same Yosys that synthesized your chip (the build's own flow image: Yosys 0.46 for SKY130 and GF180, Yosys 0.62 for IHP, Yosys 0.68 of OpenROAD-flow-scripts for ASAP7) with the process kit's own liberty cell models: the RTL is synthesized the same way as the chip, and ABC proves that the two circuits always agree from reset (register correspondence lcorr/scorr first, then dprove: bounded model checking, induction, interpolation, property-directed reachability). On a mismatch Yosys' equiv_make / equiv_induct flow names the signals that differ.

Since 31 October 2026 the check follows the logic-equivalence recipe of LiveHD (University of California, Santa Cruz, MASC group; BSD 3-Clause; see the licence notices): before any engine runs, a soundness pass reads both circuits and refuses what the engines cannot decide honestly, and every result starts with one of LiveHD's verdict words. The same words are used on Seeds, proof limits, equivalence and the SystemVerilog subset.

What the soundness pass does, in plain words:

• Undefined output bits. An output your RTL never assigns is x (undefined) in the synthesized RTL, while the chip drives it with whatever synthesis chose (usually 0). LiveHD's power-on rule applies: an undefined gold bit is a don't-care the gate may refine. Those bits are taken out of the comparison on both sides and listed in the row (PicoRV32, with its coprocessor and trace interfaces switched off, has 68 such bits: pcpi_insn[31:0] and trace_data[35:0]). A defined power-on value in the RTL (reg q = 1) is reported: standard-cell flip-flops have none.
• One clock. Both sides must clock every flip-flop from the one clock input, on one edge, with no latches; the row reports the flip-flop count of each side. Otherwise REFUTED-unsupported.
• Same ports, known cells. Otherwise REFUTED-interface / REFUTED-unsupported.
• Start state. Both circuits start from the state after reset: your reset input, found by its name (such as rst_n), is held for one clock; registers the reset does not set start at 0 on both sides. Without a reset input every register starts at 0, and a difference at clock 0 may come from that assumption (the row then says so).
• The row also says whether your RTL is still the copy the build was made from. If you edited the RTL after the build, a difference is expected: build again.
• You choose the build to compare against and the induction depth (5, 10 or 20 clocks) used when naming the signals that differ. The whole check is limited to 9 minutes on one CPU core and 1 GB on the Student plan (since 31 October 2026 the time budget follows the plan: ×1.5 on Professional, University and licensed class students, ×3 on Enterprise; the DFT check's size cap grows the same way and says before running when a netlist is beyond it) (reference synthesis 90 s, soundness pass 20 s, miter 60 s, quick bounded check 25 s, proof 145 s, bounded check 100 s, sample 30 s, naming 70 s). Memories are mapped to flip-flops before the comparison (no size limit; a large memory makes the proof slow).
• Evidence kept with every run: both Yosys logs, the soundness pass (analysis.json), the wrapper modules, the miter statistics before and after preparation, the ABC logs and the time of every stage.
• Limits: ASAP7 builds made before 29 Oct 2026 kept no synthesis netlist (unsupported: build again); VHDL projects are unsupported here. Hierarchical proving (LiveHD proves sub-modules first) is not used because the lab's chip netlists are flat.
• Reader (for everyone since 31 October 2026): Slang elaborates the RTL first and the comparison uses the elaborated Verilog as the RTL side, for designs the build's Yosys cannot read as SystemVerilog; the row says which reader was used. The same option is on the Lint row. Caution (measured 31 October 2026): a chip built from the flow's own Yosys reading must not be judged against Slang's elaboration as if both came from one reading; the row then leads with a caution and names the two reader differences (incomplete case with full_case, unsized 'bx wider than 32 bits) and the start-state effect. To compare like with like, build the chip through the Slang reader (Chip build settings), which the lab does automatically for a design the flow's own Yosys refuses. Details and the measured feature table: Seeds, proof limits, equivalence and the SystemVerilog subset.
• Line and branch coverage run cocotb (Python) tests and SystemVerilog testbenches; a project tested by a plain Verilog testbench is unsupported there (toggle coverage of the latest waveform still works).

Coverage export and exclusions#

Line, branch, expression and toggle coverage come from a separate run of your own tests with Verilator 5.044 (the Verification page's Measure). From the V&V row you can get:

• JSON and CSV exports: every source line with its hit count and status (ran, never, nocode, excluded), the counts, the tests, the tool and image, and the exclusions applied.
• Annotated source: the hit count beside each line, never-run lines marked, excluded lines marked with their reason.
• Toggle coverage of the latest waveform has JSON and CSV exports too (one line per signal).

Exclusions. Create verify/coverage-exclusions.txt in your project, one rule per line, each with a reason:

# <file>[:<line>|:<from>-<to>]   <reason>
top.sv:12-14    debug counter, not in silicon
top.sv:30       default branch unreachable by construction
util.sv         third-party module, verified by its author

The summary then reports "N lines excluded, M never ran after exclusions" and lists each rule with its reason. A rule without a reason or with a pattern the lab does not understand is reported with its line number and not applied, never silently ignored. A rule that matches no line is reported too.

FSM coverage (did every state and transition of a state machine happen?) is not provided by Verilator; the lab says so in every export instead of inventing a number. Toggle, line, branch and expression coverage are what is measured.

Evidence hashes, coverage closure, corners and rule decks#

On for every account since 30 October 2026. The V&V tab and vv.json add the following. Nothing about how a check or a build runs changes, and no stored state is changed.

Every row names its evidence. Each row lists, under Details and in vv.json (evidence), the files it rests on (the build's report, manifest and the linked result files; a check's kept files and its stored result; a simulation's kept test results and log) with the sha256 of each, and rtl_fingerprint: the fingerprint of the design (RTL) the run measured. The fingerprint is a sha256 over every design file (.v .sv .vh .svh .vhd .vhdl, outside tb/, formal/ and build folders), sorted by path. For a build the lab also checks that the version's rtl/top.sv matches the build's own input hash.

• The hashes are written once, into a ledger the lab keeps: the check worker records them seconds after a run finishes; a build's result files carry the sha256 the build system wrote into its own manifest.json; runs from before 29 October 2026 are recorded the first time the lab sees them, and the row says so.
• If a kept report is changed afterwards, its row says EVIDENCE CHANGED: <file> no longer matches the sha256 recorded <date>, and the Tapeout page's readiness check Evidence unchanged since it was recorded blocks the package.
• Re-check every report (JSON) (and sudo nelix-vv-gates verify-evidence <user> <project> on the server, which exits with an error when a file changed) re-hashes everything.

Design class and coverage closure. In Evidence, coverage closure and waivers you declare what kind of design the project is. Each class has thresholds (you may raise them, never lower them):

The Coverage closure row compares the latest line/branch/toggle run (Verilator) and functional coverage run (cocotb-coverage) with them: pass when every metric is met, fail when one is below, not run when one was not measured or was measured on an older version of the design, waived when a metric below its threshold has an approved waiver (never pass). Coverage closure is a Tapeout readiness check: it blocks the package until it is closed or waived.

Waivers need a second person. You ask for a waiver (a coverage metric here, or a readiness check on the Tapeout page) with a reason of at least 10 characters. A reviewer of the project (shared with them on the Review tab) approves or refuses it on Shared with me → the project → Waivers to review (/app/shared/<share>/vv-waivers). Nobody can approve their own waiver: the lab refuses it and says why. Approved waivers go into the package's waivers.json.

Timing at every expected corner. Each process has a list of corners its flow must analyse (SKY130 and GF180: 9, typical/slow/fast transistors × nominal/minimum/maximum wiring; IHP: 3 at nominal wiring, because IHP's kit has nominal wiring rules only; ASAP7: the flow's one default corner). The row Timing analysed at every expected corner is fail with "timing not analysed at <corner>" when one is missing, and that readiness check blocks the package. A build the build system stored as PASSED whose own timing report shows negative setup or hold slack is shown as Built, timing not met on the runs list, the run page, the Overview and here (the stored state is not changed; for example ASAP7 build BLD-20261029-0025, setup −0.457 ns).

Which rule decks, and what they are. One Rule deck classification row per deck of the project's process names the deck file, the kit revision and the deck's sha256, and says open-kit deck, educational, not foundry signoff: they are the open process kits' own decks, not the decks a foundry releases for a production tapeout. ASAP7 has no DRC or LVS deck (unsupported, with the reason). vv.json carries the table for all four processes (deck_classification).

Where an LVS short is. On a build whose LVS fails because two nets are joined, the Violations page's LVS section adds Where the LVS short is: the two net names (from the build's netgen report) and an x/y location in µm (from the build's routed layout, DEF), including the block both nets end on. Where a build kept no LVS report or no routed layout, it says so as a limitation.

Limits worth knowing#

• The table reads what the lab recorded. It does not re-run anything by itself; press Run.
• Build rows describe the latest chip build, passed or failed. Older builds: see Runs & Compare.
• Checks run at the lowest priority and wait while students have builds queued; a queued row says so.
• The requirement IDs map rows to the lab's engineering checklist; they are not a certification.

Reading the list#

Checks are grouped by phase (Design, Simulation, Verification, Synthesis, Physical, Tapeout, Validation) with a count per group. Each row shows the state on the left, the check with its measured text and an evidence line (run id, time, report links) in the middle, and its buttons on the right: the check's main report, See the violations on the chip on DRC and LVS rows, Run or Run again (its options under Options) and Ask Nelix Agent. The bar at the top has Ask Nelix Agent to review the V&V, Download evidence, Open the chip report and Tapeout readiness. The chips above the list show only failing, not-run, passing or measured rows, and the search box finds a check by name.

Nelix Agent on the V&V tab#

Every row has Ask Nelix Agent. It opens Design Chat with a question about that row already written (a failing check asks what it means and what to change first; a passed check asks what it proves and what it does not cover; a row that has not run asks what the check does and whether it matters for your design). Ask Nelix Agent to review the V&V at the top asks for the whole picture: what fails, what has never run, what to do first, what still stands between the design and a tapeout. The same button is on the power-on page of a bring-up run.

The Agent reads the V&V evidence itself (the same rows and reports you see: states, run ids, detail lines, the kept logs and reports). It explains and recommends; it never changes a check's state. The states and numbers on the tab are measured by the lab's tools and stay authoritative: only a new run changes them. Class students on graded work get explanations only, as on the rest of Design Chat.

Class projects and your own projects#

The second-person rule and the coverage-closure block apply to class projects only: a project you submitted to an assignment. There, a waiver counts only after a reviewer of the project (such as your teacher) approves it, and coverage closure for the declared design class must be met or waived before a tapeout package. On your own projects you keep full authority: a waiver you record counts at once with your name as the approver, coverage closure is shown as advice, and no design class is required.