Assertions, functional coverage and test history
Check your RTL's assertions in simulation, measure which values your tests really reached, see every test's result run by run, open a failed run's waveform at the failure, and read which requirement the last run verified.
On this page
Assertions in simulationFunctional coveragePer-test history and "what changed"The waveform opens at the first failureRequirements traceYour own clock constraints in the chip buildAsk Nelix AgentThese five tools live on Simulation V&V (Project → Verification → Simulation V&V). They are available on every project. Everything they show is measured by the lab's own tools from your files; nothing is estimated or assumed.
Assertions in simulation#
Write what must always be true straight into your RTL, in SystemVerilog:
assert property (@(posedge clk) disable iff (!rst_n) count <= 8'd200);
always_ff @(posedge clk) if (push && full) assert (0) else $error("push while full");Run the assertions compiles your design with Verilator 5.044 (--assert) in a separate container and runs it:
- with your own SystemVerilog testbench from
tb/when the project has one (see Creating projects, which lists the test languages), or - with a harness the lab writes for that run only: it holds reset for three clocks, then clocks the design for the number of cycles you chose (200, 1,000 or 5,000) and drives every input with a random value each cycle. Your files are copied and never changed.
Every failed assertion is listed with its file and line, the simulation time and the text Verilator printed; the same assertion failing again and again is shown once with a count. The simulation log and a VCD waveform of the run are kept under the result, so you can download the trace and look at the signals around the failure. A design with no assertion statements is reported as not run, never as passed.
Limits: VHDL projects are not supported (Verilator reads SystemVerilog only). Verilator supports immediate assertions and simple concurrent properties; sequences with ## delays or |=> may be refused by the tool, and the log then says so. The run stops after 50 failures. Your normal Simulate results come from Icarus Verilog and do not change.
Functional coverage#
Line coverage says which lines ran. Functional coverage says which values your tests reached. You define the values that matter as coverpoints in tb/coverage.py, using cocotb-coverage:
from cocotb_coverage.coverage import CoverPoint
@CoverPoint("top.count", xf=lambda dut: int(dut.count.value), bins=[(0, 0), (1, 127), (128, 254), (255, 255)],
rel=lambda v, b: b[0] <= v <= b[1])
def sample(dut):
passWrite a starter coverage file writes a first tb/coverage.py with one coverpoint per port and a cross of the first two one-bit inputs; edit the bins to the values that matter for your design. Measure functional coverage runs your own cocotb tests once more (cocotb 2.1, Icarus 12) and samples sample(dut) on every rising clock edge while each test runs, so your tests need no change (you may also call sample(dut) yourself at the moments that matter). The result lists, per coverpoint, the bins hit and the bins no test ever reached, with coverage.xml (cocotb-coverage's own format) and fcov.json to download. 100 % means every bin of every coverpoint was hit at least once; the test verdicts of that run are listed too.
Limits: VHDL projects are not supported here yet. export_to_yaml and constrained-random (crv) from cocotb-coverage are not included.
Per-test history and "what changed"#
Every finished simulation is recorded test by test the first time the lab sees it: pass or fail, the time it ended and, for a failure, its message. The table on Verification and on Simulation V&V shows the last ten runs as columns and every test as a row. Below it, What changed compares the last two runs: tests that flipped from pass to fail or back, failures whose message changed, tests that are new or gone. The whole history is also available as JSON. When the project's results.xml from the newest run is still there, it is kept with the record.
The waveform opens at the first failure#
On the waveform page of a failed run, a red line names the first failing test, its time and its message, with Copy. When the trace's time unit can be read, the lab also asks the viewer to put its cursor and a marker named First failure at that time and to show the window around it; Jump to it repeats that if the viewer was still loading. A run that failed before any test (a compile error) has no time to jump to, and the line says so.
Requirements trace#
Each recorded run also writes a trace: for every requirement in docs/DESIGN.md, the tests linked to it (the ID named in the test's assertion message or a # checks: line) and their result in that run. The Requirements page shows Last verified by run TST-… (date) with met / not met / not run / no test per requirement, and the trace can be exported as JSON or CSV. A specification without IDs (an Autopilot spec) gets R-01, R-02, … assigned by the lab in reading order, and the page says so; those are only met once a test names them.
Your own clock constraints in the chip build#
A chip build on SKY130, GF180MCU or IHP applies your constraints/clock.sdc in synthesis and timing analysis instead of the flow's default made from CLOCK_PERIOD. See Timing constraints for what the file may contain and how it is checked before a build starts. If the file is not accepted, the build does not start and the project Overview shows the exact reason (for example which line has unmatched brackets) under "Not started", with an Ask Nelix Agent button that asks how to fix it.
Ask Nelix Agent#
Ask Nelix Agent on these pages opens Design Chat with the run already in the question: next to an assertions or functional-coverage run (what the failure means, which bins were missed), under the per-test history (why a test started failing, or looks flaky), on the Requirements trace (which requirements lack evidence), on the first-failure banner of the waveform page (what happened at that time), and on the annotated coverage page (what the lines that never ran mean, and whether the exclusions are legitimate).
Something unclear or missing? Send feedbackSign in and use Feedback to tell us.