User guide

References such as “ADR 0189” name design records in Nilavon’s source repository, which is not public. Questions about any of them: hello@nilavon.com.

Nilavon 0.1.0 Beta (release notes). For RTL engineers, verification engineers and students. Every capability claim below points to the committed document that supports it; when this guide and those documents disagree, the documents win. Questions and problem reports: hello@nilavon.com. Studio’s Open the user guide and User guide links open this guide on nilavon.com in your browser. Every package also carries a copy for computers without internet access: Help → User guide (offline copy). Nilavon is proprietary software, licensed by subscription under the Nilavon Subscription License Agreement (Help → License agreement).

Start here.

1. What Nilavon Studio is

Nilavon Studio is a desktop app that takes your Verilog/SystemVerilog RTL and a Markdown specification and produces a reviewed verification plan, a managed cocotb test, a local simulation run and a record of what was checked (product context). The workflow is:

requirement → reviewed intent → generated test → local simulation → result → evidence

You review every assumption before anything runs. Nothing runs that you have not approved.

What it is not (product context):

• not a replacement for your simulator or a commercial verification suite;
• not an IDE or code editor (generated files stay usable in your own editor);
• not a general-purpose waveform tool (Studio shows a run’s recorded waveform read-only; section 8);
• not a chat agent or autonomous copilot (it is a guided, step-by-step workflow);
• not a general-purpose verifier for any RTL. It supports specific, bounded design shapes (section 11).

2. Install and check local simulation

Nilavon ships unsigned Beta packages for macOS (Apple Silicon), Windows x64 and Ubuntu x64 (development guide). The macOS arm64 and Linux x64 packages of this version have been installed and checked; its Windows package has not yet been checked on Windows (an earlier build passed on Windows 11 in September 2026) (release notes).

• Every package bundles its own Icarus Verilog 13.0 simulator and Python engine. You do not install Icarus, Python or uv, and you do not edit PATH (development guide).
• The packages are not signed. macOS may show a Gatekeeper warning and Windows a SmartScreen warning (Beta notice). These are the operating systems’ usual routes past such a warning; Nilavon has not yet recorded them on a downloaded package (the 2026-09-12 macOS check used a locally built one), so expect the wording to differ:
  • macOS: after the first attempt is refused, open System Settings → Privacy & Security, find the message about Nilavon Studio and choose Open Anyway.
  • Windows: on the SmartScreen window choose More info, then Run anyway.
• An installed Studio has no developer tools: the View menu has no Toggle Developer Tools item and its shortcut does nothing, and the app ignores ELECTRON_RUN_AS_NODE, NODE_OPTIONS and --inspect, so another program on your computer cannot borrow Studio as a Node.js runtime. Studio run from source (npm run desktop:start) keeps the developer tools (installation guide).
• To uninstall, remove the app the usual way for your system (drag it to the Bin on macOS, Apps in Windows Settings, or your package manager on Linux). Your projects and their .nilavon/ folders stay where they are. People qualifying a release candidate follow the installation and qualification guide.

The local simulation check. At the bottom of the left sidebar, Local simulation shows Ready, Needs attention, Unavailable or Checking…. Select it to open Local simulation diagnostics, which lists Python/engine, Icarus and an End-to-end smoke simulation, with Check again to rerun it. A green result means only that the bundled toolchain ran a fixed smoke test on this machine. It says nothing about your RTL, protocol behavior or coverage.

If the packaged simulator is missing or was changed, simulation is blocked and the message asks you to reinstall Studio. Studio never falls back to a system Icarus (development guide).

The nilavon command line. Commands in this guide and in failure details (such as nilavon run --project …) use the bundled engine’s command line (ADR 0171). Where it is depends on the package:

Install the nilavon command from Studio. Choose Settings > Advanced > Command line (or Install nilavon Command… in the Nilavon Studio menu on macOS, the Help menu on Windows and Linux; the item is there only where Studio can install it). Studio first lists what it will change and changes nothing until you press Install; Remove nilavon command… in the same place undoes it (ADR 0193):

Studio never replaces a nilavon that belongs to something else. Uninstalling Studio does not undo the install, so press Remove first; otherwise a link or PATH entry pointing to the removed app stays behind (a later install replaces the link). Until the command is installed, Failure details shows and copies its rerun command with the launcher’s full path in place of nilavon, so a copied command works as pasted; the run’s record and reports keep nilavon.

Without Studio’s install, run the launcher by its full path:

Keep the quotes: the default install folders contain a space. In PowerShell, put & and a space in front of a quoted path (& "…\nilavon.cmd" --version). On Linux and macOS you can link the launcher into a folder on your PATH yourself; it finds its own files through a link. On Windows add the resources\cli folder to PATH instead: a link or copy of nilavon.cmd elsewhere looks for the engine beside itself and stops with “the bundled engine is missing”. On Linux and macOS the installed launcher runs the package’s own Icarus, as Studio does, so a copied rerun command uses the same simulator. The Windows launcher does the same, and hands every argument and the engine’s exit code through unchanged. Failure details quote an unusual argument for a Unix shell ('like this'); in Command Prompt use double quotes instead, and quote any argument that holds &, |, <, > or ^. From another batch file, start it with call nilavon … so that your file carries on after it.

Help, man page and tab completion. nilavon --help (or just nilavon) lists the commands you need, grouped by task: set up, plan and run, after a run, shell. Every command takes --help, and nilavon help <command> is the same. nilavon help --all lists every command, including the evaluation and internal ones. A mistyped command name is named with a close match (nilavon: 'comapre-runs' is not a nilavon command. Did you mean 'compare-runs'?). Every command that takes --project accepts the project folder as well as its nilavon-project.json. nilavon man prints a manual page with every command and option: read it with nilavon man | man -l - (Linux) or nilavon man > nilavon.1 && man ./nilavon.1 (macOS). nilavon completion bash and nilavon completion zsh print tab-completion scripts for commands, options, choices and file names:

The Linux DEB sets these up for you. It links the man page to /usr/share/man/man1/nilavon.1, so man nilavon works, and the completion scripts to /usr/share/bash-completion/completions/nilavon and /usr/share/zsh/vendor-completions/_nilavon, so completion works in a new shell with nothing in ~/.bashrc or ~/.zshrc. A completion link is made only when that shell’s completion support is installed (the bash-completion package, or zsh); install it and reinstall the DEB to add the link later. As for /usr/bin/nilavon, a file another package owns is left alone, and uninstalling removes only the package’s own links. The AppImage and the .tar.gz carry the same three files in resources/cli/ for you to link yourself.

A mistyped option prints the usage of the command you typed and the option it did not recognise (nilavon init: error: unrecognized arguments: --top x), not the list of every command.

Use the full launcher path from the table above where nilavon is not on PATH; completion then needs nilavon (or a link to it) on PATH to be useful. The scripts and the page are generated from the command’s own option definitions, so they match the installed version; the source tree keeps copies in packaging/shell/ and packaging/man/. Only the Linux DEB installs them for you (above); on macOS and Windows, and from the AppImage or tarball, set them up yourself as in the table.

Running from a source checkout (developers) needs Python 3.11–3.13, Node.js 22.12–25, uv and Icarus Verilog 11 or newer on PATH; see Development setup.

3. The workflow

The home screen lists your Recent projects (once you have any) and four Exercises; Open project and New project sit at the top right. Whether you start from an exercise or your own design, the steps are the same (product context):

1. Create or open a project. New project asks for one folder (Choose folder…). Studio lists the folder’s .v/.sv files, header folders and specification files, with the likely ones checked: files that look like testbenches (tb_*, *_tb.*, test*) and hidden or build folders are left out. Change any choice, then choose Continue. Without a specification, write one in Studio from a short template: it is saved as specification.md in your folder when you continue (a new file; an existing one is never replaced). Reading the folder changes nothing. Folders that look like simulation models of vendor cells (lib, sim_models, cells, unisims, …) are not offered as your design: Simulation libraries proposes them as library folders, and Choose single model files takes a model file that holds several cells. Their models are compiled only for the cells your design uses (ADR 0199). You can also drop the design folder on the Studio window: it opens the same list. Open project reopens a folder that already has a nilavon-project.json (section 9 lists the other ways back in). You never write that file by hand.
2. Review the setup. Studio compiles your RTL and walks you through four stages: Files; Design block, clock and reset; Verification recipe and signals; Confirm and create. Pick the top module (an ambiguous top is never picked for you), confirm clock and reset, map signals, and choose Create project. If you change a setting after the design was checked, use Recheck design setup. When none of Studio’s recipes fits your design, setup picks No recipe: General RTL or your own expected behavior and asks only for the top module, clock and reset; the project then opens on General RTL (Beta). You can still choose a recipe from the menu. Any notes the compiler has about your design (for example, a construct the simulator cannot compile) are listed before Create project; none of them stops it.
3. Review the verification intent. Choose Create local plan for the deterministic plan. Each check needs a decision: Approve check or Cannot verify. Choose Save review decisions, then approve the whole plan separately with Approve reviewed plan. Saving and approving are two steps on purpose: approval binds the exact plan you reviewed.
4. Generate. Generate verification writes the managed cocotb test. If the plan or inputs changed, Studio asks you to regenerate (Regenerate safely) and never silently overwrites a file you edited.
5. Run. Run verification runs the test with the local Icarus. Run again reruns it.
6. Read the result and evidence. See sections 8 and 9.

The sidebar names the same journey in six steps, in a guided exercise and in your own project: Choose design, Check setup, Review detected signals, Confirm plan, Run and Understand result. Generating the test is part of Run; the current task card says when to choose Generate verification first. In your own project, a recipe that no longer fits the design shows as Check setup, and on the step-by-step (generic) path, drafting and classifying the ports is Review detected signals (ADR 0174). General RTL (Beta) has its own five steps instead: Draft, Review, Approve, Run and Result (section 5).

Beginner and Professional presentation. In a project, the Presentation control in the project bar offers Beginner (the current step only, technical records folded under Advanced details or Technical details) and Professional (the complete technical record). Both show the same project, decisions and evidence; the choice changes only what is shown and is not saved (ADR 0107, ADR 0188).

Finding the current step. The sidebar lists the steps and marks the current one. The page header names the step, the project, its RTL revision and its state (for example Plan needs review or Checks failed), and holds the step’s main action: Check setup or Continue to plan in an exercise, the next setup stage’s button in a new project (Beginner), then Create local plan, Generate verification or Run verification. It stays in view while you scroll.

When a run is done, Start another exercise or Start another project, Open evidence and Return home take you onward.

4. Built-in exercises

Five exercises sit at the top of the home screen. Each copies a small design and specification into a fresh local project you can edit:

An exercise follows six steps: Choose design, Check setup, Review detected signals, Confirm plan, Run, Understand result, listed in the sidebar. On Review detected signals each role has a short name (Clock input, Load enable), a one-line description of what it does, and its technical role id. Known-safe settings are filled in for you but stay visible for review. Exercise files are editable input, not verified evidence: you still pass every review, approval, generation and run step yourself.

Starting an exercise first asks where to put it: pick a folder, and Studio creates a new nilavon-counter-basics (or -fifo-, -handshake-, -register-) folder inside it with the example design and its specification. If that folder already exists there, Studio says so; pick another folder.

Your first run (Counter, about ten minutes).

1. On the home screen, under Exercises, choose Start beside Counter and pick a folder.
2. Check setup: the compiler has already read the files. Choose Check setup so it builds the design block and lists its ports.
3. Review detected signals: each role (clock, reset, increment, load…) is filled in. Read them and choose Continue to plan. The read-only settings below say how many random transactions the test drives, how long a run may take, how many cycles a check waits for progress, and the seed.
4. Confirm plan: choose Create local plan. Read What you are confirming (the assumptions, the checks, what the specification leaves open, and the limits), then choose Use the exercise’s suggested decisions (or decide each item yourself) and Save review decisions. Tick the confirmation, then choose Approve reviewed plan at the top of the page.
5. Run: choose Generate verification, then Run verification.
6. Understand result: a pass shows Counter basics is complete with what the pass does and does not show. Then Start another exercise, Open evidence or Return home.

If a check fails, its row in the checks table opens to show what it expected and observed, and the result says what to do next in one line (section 8).

The General RTL tour (no key, about ten minutes). General RTL (Beta) usually needs an online key or the local model before anything happens. The tour lets you try it first (ADR 0200). It creates a nilavon-general-rtl-tour folder with a small PWM generator, its specification, its project file and a draft prepared in advance. No AI is called and nothing leaves the computer. The draft is labelled “AI-drafted: claimed, not verified” like any draft, because you check it like one.

1. Choose Start beside General RTL and pick a folder. The project opens on Draft, without a recipe.
2. Choose Import the prepared draft… at the top right and pick prepared-draft.json in the project folder.
3. Review: the draft has three requirements, each with one check, as well as its timing, input defaults, scenarios and the specification’s passages. One check reads the specification wrongly on purpose. Compare each check with its passage. PWM-OUT-001 says pwm_out is registered, so at the start of a period (cycle_start high) it is still low, but the drafted check expects it high. Choose Correct this item on that check and change Check field expect to !pwm_out. This creates a corrected revision. Accept every item in it.
4. Approve, then Run with Record a waveform. Every check passes. If you approve the draft as it came instead, the run fails on that check at 25 ns, and the result and the waveform show where. Correct it on Review and run again.

5. Your own RTL: three routes

After you create a project from your own design, the project bar’s Verify with choice offers Built-in recipe, Your own expected behavior and General RTL (Beta). The choice affects only what Studio shows; it does not change the project file (ADR 0188, ADR 0189). Studio remembers it per project in its own app data, so a project reopens on the route you left it on; a project you have not chosen for yet opens on the route of its newest run. Your own expected behavior does not use simulation library files yet, so a project that lists library files or folders shows it unavailable and opens on General RTL (Beta) (ADR 0199).

Use the built-in recipe (registered capabilities)

Pick this when your design matches one of the eight registered capabilities and the recipe’s documented behavior matches your specification (development guide): synchronous FIFO; bounded ready/valid stream; bounded APB register file; FIFO-to-ready/valid and ready/valid-to-FIFO compositions; loadable single-clock bounded state; loadable up/down bounded state; and registered fixed-priority arbitration.

The engine checks the compiled structure, your signal bindings, the reviewed assumptions and the execution settings before generating anything. A shape the recipe does not support fails with a reason, not a guess. Studio never picks a different recipe or a signal role for you because a name looks familiar.

Describe the expected behavior yourself (generic, no-pack route)

Pick this when no recipe fits a plain single-clock design. Every signal starts unclassified. You go through five short reviews: inspect the structural draft (Draft generic model), classify each visible port, define finite expected observations, group them into bounded scenarios, and choose which scenarios become finite checks. Then Prepare test inputs, Prepare observation timing, Build the test and Run the test, each as a separate action.

What it can check today is narrow (development guide): reset plus static input drives; constant output samples a finite number of cycles after reset; one observation that a transfer event occurs between two reviewed one-bit signals; one constant sample at the final reset edge; plus two exact reference relations (a SIZE=4 serial deglitcher and one fixed-width UART accepted-word/frame/busy relation). Each passing run proves only those reviewed observations.

General RTL (Beta): draft with AI, then review each item

For any design, including one no recipe covers, choose General RTL (Beta) under Verify with (ADR 0189). A project created without a recipe opens here, and its Built-in recipe choice is unavailable (ADR 0198). Each step below is a page of the project: the sidebar opens the steps the project has reached, and each page’s main action is at the top right (ADR 0194).

No key yet? The General RTL tour (section 4) walks these steps with a prepared draft.

1. Draft. Under Draft with, choose Online AI with your key (Anthropic or OpenAI, your own API key, usually minutes) or Local model (an Apple Silicon Mac with the optional model, about 50 minutes, nothing leaves the computer). Save the key in Settings > AI or on the page. For an online job, Review what will be sent… lists every file and instruction with its size and SHA-256; nothing is sent until you choose Agree and start drafting. A job never switches to the other route on its own.
2. Import. Every drafted item is labelled “AI-drafted: claimed, not verified”; nothing enters the review until you choose Import into review.
3. Review. The review has three panes: the items (filter by Needs decision, Accepted or Declined), the source with the cited passage marked, and the item with Accept meaning, Decline and Correct this item. Keys: j/k (or the arrows in the list) move, a accepts, d declines. Studio asks your name at your first decision and remembers it for the project. A drafted question is accepted on its exact reading, with your reason; one with no reading yet gets yours first through Correct this item. A declined question keeps the revision from being approved.
4. Approve and run the exact revision you decided. Only approved checks run, on the simulator with your RTL; coverage is not measured. Result shows the newest run, with sharing, comparing and waivers below it.

General RTL is Beta and not qualified (online drafting guide, local drafting guide; ADR 0163, ADR 0167, ADR 0185).

What review and approval mean

• Review is where you confirm or reject each interpretation the engine or an AI proposed. Refusing to invent a check is valid: an item without a trustworthy check is marked Cannot verify, and Studio shows Approval is blocked until you revise the intent or the specification. Nothing is silently dropped.
• Approval is a separate step that locks the exact reviewed revision. Generation and runs use only approved revisions. Change the plan, RTL or settings afterwards and earlier runs stop counting as evidence for the current plan (section 8).
• AI never approves anything and never writes executable test code; the engine builds and runs every check. The compiler, the engine’s checks, your review and the simulator’s output outrank any AI output (product context).

6. AI options

AI is optional. Studio never switches to an AI provider on its own, and none is a fallback (product context). Settings (bottom of the sidebar) has five sections: General (theme), Simulation (the local simulator check), AI (OpenAI access, Anthropic access and Local AI), Projects (recent and trusted projects) and Advanced (contained runs and the nilavon command line). AI shows the status of each option.

Every AI output is an unapproved proposal. You review it exactly like a deterministic plan.

7. Privacy

Nilavon is local-first (product context):

• RTL, specifications, generated tests, simulator logs and evidence stay on your machine.
• Studio has no auto-update or publishing configuration (Beta notice), no usage telemetry or analytics, and no crash reporting. Its spellchecker is off, so it downloads no dictionaries. The privacy statement (also in every package as PRIVACY.md) lists every time Nilavon goes online and what it sends.
• The deterministic path and Local AI send nothing off the machine. Downloading a local model contacts only its publisher, and only when you ask.
• An OpenAI request needs fresh consent each time. It sends the specification text, the compiled top-level interface and your reviewed configuration. Raw RTL, project paths, generated files, shell commands and run logs are not sent.
• Online General RTL drafting sends, per job and only after you agree to its list, the project files that job lists (specification, RTL sources, manifest) and the role instructions to the provider you chose, with your key. Each request and answer is kept in the job’s online-calls/ folder; the key is never kept there (guide).
• API keys are kept in OS-backed secure storage, or in memory for the session only if you choose. They never go into project files.
• Studio keeps a small log of its own start-ups, crashes and errors in its app data folder (at most four files of 256 KB). It never holds your design, file contents or keys; paths keep only their last folder or file name. Help → Save support bundle… zips that log with versions, the simulator check and settings (no keys, no project names) so you can attach it to an email; nothing is sent unless you send it (ADR 0191).
• Saved runs stay in the project’s .nilavon/ folder until you remove them; nothing expires. What they hold (paths of this computer, your design, reviewers’ names) and what you may delete is in section 9, How much space saved runs take, and what you may delete.

Projects from someone else: opening a project only reads it. Running it simulates its RTL with your own file permissions, and Verilog can read and write files ($fopen, $readmemh, $writememh); a shared project can also carry its own generated tests. Run only designs you trust. Details: security review 2026-10-31.

Project trust. Studio trusts a project it created on this computer (New project and the built-in exercises). Any other project opens read-only until you trust it: you can read its plan, runs, failure details, waveforms and reports, and export reports and evidence packs, but Studio will not run it, generate tests for it, re-check its RTL or change its plan, reviews or waivers. The workspace says Read-only: you haven’t trusted this project. Pressing Run verification, Generate verification or Re-check RTL (or running approved checks in General RTL review) asks first and says what running can do; Keep it read-only is the default, and Trust and continue carries on with what you pressed. You can also trust from the read-only notice with Trust this project….

Trust belongs to the folder, as in a code editor. A trusted project stays trusted when its files change: fixing your RTL in an editor and pressing Re-check RTL never asks again. When the files that run (the project manifest, RTL sources, included headers or generated tests) changed outside Studio since Studio last worked on the project, the workspace shows a note, Code in this project changed outside Studio, naming them; it does not stop you, and Dismiss note clears it. This means a change pulled into a trusted folder (git pull) is not asked about again, only named in that note: trusting a folder is trusting what you put in it, so read the note before you run someone else’s changes. Studio keeps its trust records in its own app-data folder (project-trust.json), never in the project, so a project cannot mark itself trusted, and a project moved or copied to another folder asks again. Trusting is consent, not a sandbox: a trusted project still runs with your file access.

Contained runs (Linux). Settings → Advanced → Contained runs → Contain every run (recipe, generic and General RTL) (off by default) runs a project’s RTL and tests contained: a run can then write only to its own run folder, can read only the system, Nilavon and the project folder (not the rest of your home folder), cannot change any file’s permissions or dates, has no network, and cannot keep running after the run ends. Use it for projects you did not write. Settings says whether this computer can contain runs; it needs Linux 5.13 or later with Landlock, which many current distributions have. On macOS and Windows, or a Linux kernel without Landlock, Settings says why not, and while the setting is on a run there is refused rather than run uncontained. A contained run’s result card shows Contained: Yes, no network, and its reports say how it was contained. A contained run that leaves links in its run folder (a way to make Nilavon write outside for it) is an error that names them; they are removed before Nilavon reads the folder. A General RTL run says Contained: Yes, no network on its result. The simulations a draft job runs while it drafts checks (its tool runs, its exploratory run and its check-strength sample) are contained too while this setting is on; where they cannot be, drafting is refused rather than run uncontained. Containment for macOS and Windows is designed but not built. From the command line: nilavon run --contain, nilavon general run --contain, nilavon general-draft start --contain (and resume --contain) and nilavon containment-status (ADR 0181).

Stop trusting a project. Settings → Projects → Trusted projects (Settings is at the bottom of the sidebar) lists every project Studio may run without asking: each folder’s name, Created in Studio or Trusted by you, when Studio last worked on it, and Open now or Folder not found where that applies. Stop trusting makes that project read-only again; if it is open, the workspace shows the read-only notice at once, and running it asks the trust question again. Nothing in the project changes and its saved runs stay. The list shows folder names, not paths, so open a project first if two folders share a name (ADR 0176 addendum). The command line does not ask: nilavon run and the other commands run what you point them at, as make or pytest would (ADR 0176).

8. Reading a result

What a pass proves. A passing run means the checks that ran passed, on this RTL, with these settings, in this one simulation. It does not prove that the specification was interpreted correctly, that coverage is adequate, that a protocol is fully compliant, or that the design is correct in general (product context; development guide). Every result reports Coverage: not claimed (coverage: not_claimed). Coverage is a separate kind of evidence that Nilavon does not produce today.

What was not checked. Look for Not verified by this plan in the plan summary, items marked Cannot verify, and anything reported as unsupported or No executable check. These are part of the result, not errors to hide.

Outcome words you will see

Reading a result. A run result opens with its answer (ADR 0195): how many checks or requirements passed, the RTL revision, when it ran, and on a failure the first failing check with the first line of its message, then the next actions (Failure details, Open waveform when one was recorded, Re-check RTL, Run again). The checks table follows, then one row with Share, Compare, Waivers, Rerun command, Run evidence and Saved-run storage; each opens below the row.

Failure details. When a check does not pass, the result’s table (and every exported report) shows its failure details: which check failed first and where (the sample or clock cycle in its scenario, or the recipe test), what was expected and what was observed, the signal values recorded there (for a recipe test, the check’s own message and the comparison it made, such as “FIFO must be empty after reset” and “assert 0 == 1”; runs saved before 1 November 2026 say only “Test failed”, so run again to see it; ADR 0179), the seed, and (under Rerun command) the command that repeats the run from the command line, with a Copy button. A generic run records no command: Rerun command names the operation and lists the identities its reviewed files must give. It lists only what the run recorded and never names a cause. A recipe run that recorded a waveform also records where each failing test stopped in simulation time (“Failed at 145 ns of simulation time, where the test stopped”) and offers Go to failure in waveform (section 8). A generic run that recorded a waveform records when its failing sample was taken (“Its failing sample was taken at 145 ns of simulation time (cycle 4)”) and where the check’s test ran (“Its check ran from 60.001 ns to 145 ns of simulation time”), and offers Go to failure in waveform too. Generic runs recorded before 2 November 2026 have only the window: they offer Show check window in waveform and say that the run did not record the failing sample’s own time. A General RTL run that recorded a waveform has one file per scenario, each on its own timeline: its failure details say when the failing sample was read in that scenario (“its failing sample (sample 7 of SCN-…) was read at 85 ns of that scenario’s simulation”), a time derived from the runtime’s sample timing, and offer the scenario’s waveform at that time (ADR 0180). Runs without a recording show no time (ADR 0177 and its addenda).

A failing check is a question, not a verdict. The RTL may be wrong, or the specification may have been read differently from what you meant. You decide which. In a guided project: open the failed check’s row in the checks table, find its plan item (such as PLAN-2) in the plan and the specification line it links to, then decide whether the RTL, an assumption you accepted or the specification is wrong. Running again with nothing changed repeats the same checks with the same seed.

Fixing the RTL. Edit the RTL in place, in the same project folder. Nilavon records your RTL’s fingerprint at each check, so the next time you open the project (or press a button that reopens it) Studio says Your RTL changed since this project’s last check. Choose Re-check RTL (ADR 0172): Nilavon analyses the edited RTL and records it in the project as a new RTL revision, keeping the earlier revision’s file hashes in the project’s history. Then:

• Only the logic changed (the design’s ports and parameters are the same): the approved plan still applies. Choose Generate verification again, then Run verification.
• A port or parameter changed: the plan goes back to review. A recipe plan is rebuilt for the new RTL; a plan drafted with Local AI keeps its content with every decision reset. Review and approve it, then generate and run. The earlier plan is kept under .nilavon/plans/. A project created before this release cannot compare ports on its first re-check, so its plan goes back to review once.
• The RTL does not compile, or no longer fits the recipe (for example, a renamed reset or flag): nothing is changed. Fix the RTL and choose Re-check RTL again, or make a New project if the design is now a different shape.

Earlier runs are never rewritten. They stay in the run history as Not evidence for the current plan because they used older RTL, and an exported report of a recipe or generic run says which RTL revision it used (“this run used RTL revision 1; the project’s RTL is now revision 2”). The run’s card in Studio says it too, as an RTL revision line beside the run’s facts (“1 (the project is now at 2)”, or “2 (current)” for a run of today’s RTL; “None recorded” when the run’s RTL matches no revision the project recorded, for example RTL edited after the last re-check). A JUnit report carries the same as the properties nilavon.rtl_revision (the run’s revision, or none) and nilavon.project_rtl_revision. A project whose RTL was never re-checked has one revision, and neither its cards nor its reports mention it. From the command line: nilavon recheck-rtl --project nilavon-project.json.

The RTL a failed run used is kept. Every recipe and generic run keeps a copy of the RTL files it ran in .nilavon/kept-rtl/, named by each file’s SHA-256 and never rewritten (ADR 0172 addendum). So after you fix the RTL, the failed run’s report lists its source as “kept from RTL revision 1” instead of “changed since the run”, and its evidence pack includes the file that ran, checked by its SHA-256 like every other packed file: you can share the failing run, with its RTL, in a bug report or a review of the fix. Failure details says plainly that its rerun command runs today’s RTL, not the RTL the run used. To run the old RTL again, use the copy from the run’s evidence pack in a separate project. Runs made before this release kept no copy: their reports still say the source changed, and both the report and the pack say why there is no copy. A General RTL run made with nilavon general run keeps its RTL the same way, and its report lists it under “RTL this run used” (addendum). A run from Studio’s General RTL pages already runs a saved copy of its reviewed inputs.

Looking at the waveform. A run can record the design’s signals while the test runs (ADR 0170). Recording is off by default: tick Record a waveform of the run beside Run verification (or on the generic route’s run step, or the General RTL Run page) before you run. A General RTL run records one file per scenario, each up to 32 MiB, and stops recording new scenarios once the run’s files reach 128 MiB; its Result page lists the files (ADR 0180). Then open Run evidence on the result and choose View waveform on the waveform row. Studio checks that the file is the one the run recorded (an edited or replaced file is refused, as with Reveal) and opens it read-only. It reads the file in the background, so Studio stays responsive while a large recording loads; a file it cannot read within a minute is refused with a note to use Export copy and a dedicated waveform tool:

• Signals lists the design’s ports first, then its other signals, parameters and inner scopes. Tick a signal to add it to the timeline; × on its timeline row takes it off; Filter signals narrows the list. Ports are tagged port; hover a signal for its kind and width.
• Timeline shows each signal over time with its value at the cursor in the Value at cursor column: 0/1 for a bit, hexadecimal for a vector (0x0a), and x (unknown) or z (not driven) in their own colours. Click the drawing to move the cursor.
• Zoom in, Zoom out, Show all, Earlier and Later move the view; Previous change and Next change move the cursor to the nearest value change of a shown signal. From the keyboard, focus the timeline and use Left/Right (previous/next change), Shift+Left/Right (pan), +/− (zoom), 0 (show everything), Home and End. With the pointer on the timeline, Ctrl (⌘ on macOS) with the scroll wheel zooms around the pointer and Shift with the wheel pans. These are listed under Keyboard shortcuts for the timeline. The readout at the end of the toolbar shows the cursor time and the time span in view.
• On each timeline row, the arrows ↑ and ↓ (shown when you point at the row or tab to it) move the signal up or down, and a vector’s number format can be Auto (hexadecimal, or decimal for parameters and integers), Hex, Binary, Decimal or Signed (two’s complement). A value with an unknown or undriven bit is always shown as bits.

Saved layouts. Studio remembers the signals you show, their order, their number formats and the zoom, for each project and each kind of waveform: one layout for the recipe test’s runs and one for each generic route’s runs. The next time you open a waveform of the same kind in that project, even from a newer run, it opens the same way and says Showing the layout you saved. A saved signal the new recording no longer has (for example after you renamed it in the RTL) is left out and counted in that line; nothing is refused. Reset layout goes back to the automatic layout and forgets the saved one. Opening a waveform from Failure details still goes to the failure or the check window. Layouts are kept in Studio’s own app-data folder on this computer (waveform-layouts.json), never in the project, so they are not evidence and are not shared with the project (ADR 0170 addendum).

Where the check failed. A recipe run that records a waveform also records the simulation time at which each test started and stopped. A failed recipe test stops at the moment its failure is raised, so that time is where the failure is on the waveform (ADR 0177). The viewer draws it as a solid red line, names the failing test and the time above the timeline, and Go to failure moves the cursor there (the Value at cursor column then shows every signal as the test saw it). In Failure details, Go to failure in waveform on a failing test opens the viewer with the cursor already on that test’s failure. If a recording was cut short before the failure, the viewer says so and draws nothing. Runs recorded before this marker existed show no marker.

Where a generic check failed. A generic check samples its signals and decides pass or fail only after its samples, so the moment its test stops is not the moment of the failing sample. A generic run that records a waveform therefore runs a timed copy of its generated test: the same test, which also prints the simulation time at which it read each sample. The timed copy sits beside the usual one in the project’s .nilavon/generic-generated folder (its name ends in _timed.py), so recording never changes or replaces the usual test, and both check exactly the same things. The viewer shades the failed check’s window and draws a solid red line where the sample its first mismatch names was read, naming the check, the cycle and the time above the timeline; Go to failure moves the cursor there. In Failure details, Go to failure in waveform opens the viewer that way.

Generic runs recorded before 2 November 2026 recorded only the window: the viewer shades it, says the run did not record the sample’s own time, and Show check window zooms to it (the failing sample is inside, at the cycle Failure details names). Rerun with a waveform to get the sample’s time. Nilavon never turns a cycle or a duration into a time the run did not record (ADR 0177 addenda). Comparing a run with a waveform to one without treats them as the same checks: the comparison lists the test edition as a difference that does not block lining the checks up, and a waiver written on either applies to both.

The viewer never changes the file. It opens files up to 40 MiB; the engine stops recording at 32 MiB, and the viewer says when a recording may end before the simulation did. Use Export copy to open the file in another waveform tool (it is a standard VCD). Runs made without recording, including all earlier runs, have no waveform.

9. Where evidence lives and how to reopen it

Everything is stored inside your project folder under .nilavon/ (ADR 0018, ADR 0020):

Do not hand-edit files under .nilavon/: Studio validates them, and a changed file is reported rather than trusted.

Reopen a project

To come back to a project, pick it under Recent projects on the start screen or in File > Open Recent, drop its folder (or its nilavon-project.json) on the Studio window, or choose Open project and pick the manifest. The recent list keeps your last 20 projects in Studio’s app data, never inside a project; a project that was moved or deleted is marked Folder not found with Remove from list, and Settings > Projects clears the whole list. Each project shows how its newest run ended, whichever route made it: a recipe run, a generic run or a General RTL execution (Last run inconclusive when a General RTL run’s requirements neither passed nor failed). nilavon latest-runs --project MANIFEST prints the same on the command line. Opening a project this way never trusts it: one Studio did not create still opens read-only until you trust it (ADR 0192). Studio rebuilds the view from what the engine validates on disk, not from saved screen state, so the current task and earlier runs reappear as they were recorded. Refresh earlier runs reloads the history. On a result, Reveal shows a file in Finder/Explorer and Export copy saves a checked copy elsewhere (ADR 0019); a run’s waveform file also has View waveform (section 8).

Share a run: a report or an evidence pack

Every run result has a Share this run group with Export report… and Export evidence pack…: a built-in exercise or recipe run, a generic run (new or reopened from earlier runs), and a run in General RTL review. On every result it is the Share area in the row below the checks table. The controls inside are the same everywhere.

A report is a readable copy of the run’s results and of what they do not prove. Choose a format (an HTML page by default, or Markdown, JSON or JUnit XML), then pick where to save it. The engine checks the saved run again before writing; for a General RTL run it also adds the approved requirement text when it can. The saved run itself is unchanged. A report cannot be saved inside the project’s .nilavon/ folder or over its manifest. If the run’s own log or results file changed after the run, the report is refused; if your RTL or the generated test changed since, the report lists those files as changed since the run.

An evidence pack is one zip with the run’s record, log, results, generated test, your RTL and the approved plan (for a recipe run) or the approved bundle and the review’s run receipt (for a General RTL review run), plus the HTML report as a convenience copy. pack-manifest.json lists each file with its size and fingerprint (SHA-256). The fingerprints show the files were not changed after export, not who made the pack, so Studio shows the manifest’s own SHA-256 after saving: send it separately (in a message or ticket) so the reviewer can confirm the pack is yours. A pack contains your RTL, so share it only where the design may go. Like a report, a pack cannot be saved inside .nilavon/ or over the manifest, and the saved run is unchanged.

Sharing a pack without your RTL. Tick Leave out source files before choosing Export evidence pack… (the file name then ends in -without-sources.zip). The pack keeps each source file’s name, size and SHA-256 but not its contents, so a vendor or tool reviewer can check the run record, logs and results without seeing the design, and anyone who has your originals can confirm they are the files that ran (nilavon verify-evidence-pack PACK.zip --originals PROJECT_FOLDER). Logs and the report can still mention module and signal names. A pack without sources still verifies; Studio’s verdict says how many files were left out and that they cannot be checked from the pack.

From the command line: nilavon export-run-report --project nilavon-project.json --run-id run-… --format html (a recipe run) or --project-root . --run-id generic-run-… (a generic run) writes a report, and nilavon export-evidence-pack … --output PACK.zip (add --redact sources to leave out your RTL) writes a pack. See Recipe and generic run reports and Evidence packs.

Check an evidence pack you received

On the home screen, with no project open, choose Verify evidence pack… under Verify an evidence pack and pick the zip. Studio checks every file against the pack’s manifest, offline, and says in one sentence whether the pack is intact and which run it holds (for example “pack.zip is intact: all 14 files match its manifest. It holds a General RTL run, general-run-…, which recorded the status “failed”.”). It also shows the manifest’s SHA-256: compare it with the one the sender gave you separately. If a file was changed, added, removed or damaged, Studio says the pack did not verify and lists the problems; do not rely on its files and ask the sender to export it again. A verified pack shows integrity only: it is not signed and never claims coverage. Nothing is written. Without Studio, nilavon verify-evidence-pack PACK.zip gives the same verdict as JSON.

Compare two runs

When the project has an earlier saved run of the same kind, the result also has Compare with…: pick an earlier run and choose Compare with earlier run. Each earlier run is labelled with when it ran, and with its status (recipe and generic runs) or whether it is from this review revision or an earlier one (General RTL review). So after you fix your RTL and choose Re-check RTL, the failed run from before the fix is there. (A generic run’s earlier runs appear once they are listed.)

Studio says in one sentence what changed (for example “2 checks fixed, 1 regressed; 7 unchanged.”) and which RTL revision each run used (“Earlier run: RTL revision 1 · This run: RTL revision 2 (current)”). The check-by-check table is under Check-by-check changes, changed checks first:

• Regressed: a check that passed before now observes a mismatch.
• Fixed: the reverse.
• Newly exercised and No longer exercised: the run did, or did not, reach the situation the check looks at.
• A waived check reads failed (waived by …).

If the two runs used a different simulator or different settings, or the plan or generated test changed between them (for example after a port change sent the plan back to review), Studio says the checks cannot be compared one by one, lists what differs under What differs between the runs, and shows the results of both runs side by side only. For recipe runs made from 1 November 2026 on, it also says which: a plan change (a different approved plan) or a generator change (the same plan, generated by a newer Nilavon into a different test); older runs say “plan or test change”. Both saved runs stay unchanged, and coverage is not claimed.

From the command line, nilavon compare-runs --project nilavon-project.json --before run-… --after run-… (or --project-root . --manifest nilavon-project.json for generic runs; --manifest only adds the RTL revision labels) does the same, and --fail-on-regression makes a CI job fail when a check lost its pass (see Comparing recipe and generic runs). For General RTL runs, use nilavon general compare-runs (see Comparing two runs).

Accept a known failure for a while: waivers

A waiver lets you accept a known failure for a limited time (a bug filed upstream, an open specification question) without editing any result (ADR 0168). One person proposes it and a colleague approves it. The failure still shows in every report, labelled with the waiver and its expiry date. A waiver stops applying when it expires or when the checks it covers change.

• Recipe and generic runs. A result with failed checks has a Waivers area in the row below its checks table. Enter Your name, choose the failed checks, give a reason and the last date the waiver applies, and choose Propose waiver. A colleague enters their name and a note and chooses Approve (or Reject, or later Revoke). A waived check reads failed (waived by …). From the command line: nilavon run-waiver propose, review, list and show (--project nilavon-project.json for a recipe run, --project-root . for a generic one).
• General RTL review. A saved run with failed checks has the same Waivers section. A waived check still reads Observed a mismatch, with the waiver beside it. A General RTL waiver covers the checks themselves, so approving the same checks again in a new review revision keeps it. The command line has nilavon general waiver propose and waiver review (see Waivers).

Running Nilavon in CI

The Python engine runs on its own, without Studio.

• Recipe and generic runs. nilavon export-run-report … --format junit --fail-on-failure writes test results and makes the job fail when a check failed. Add --honor-waivers to pass only when every failed check has an approved, unexpired waiver for these exact generated tests and settings (recipe) or reviewed checks (generic). For a recipe run it also needs the simulator to have exited normally: a run whose simulator crashed after recording its results, or one recorded before Nilavon logged the simulator’s exit (before 1 November 2026), is never excused; run it again. nilavon compare-runs … --fail-on-regression fails the job when a check lost its pass.
• General RTL runs. nilavon general run --fail-on-failure makes the job fail when a check observes a mismatch, and nilavon general export-run --format junit (test results) or --format markdown (the job summary) publishes the saved run; --honor-waivers works as above. See General-route results in CI for every format and docs/examples/general-run-ci.yml for a copy-ready GitHub Actions job.

How much space saved runs take, and what you may delete

In the row below a run result (or at the bottom of a project with no result yet), Saved-run storage shows what the project keeps in .nilavon/ (ADR 0178). Open it (Studio measures the folder then; Measure again refreshes) to see the total, a table By kind, largest first (run records, simulation logs, test results, waveforms, build scratch, generated tests, plans, waivers, reviews, kept RTL of earlier runs) and a table By run, largest first (the 20 largest runs, each with how much of it is build scratch). Each kind says what it holds (paths of this computer, your design, reviewers’ names) and whether you may delete it. Reports and evidence packs check this file’s hash (simulation logs and test results) means a report or pack compares the file with the fingerprint recorded when the run finished, so a file changed or removed outside Nilavon makes them refuse the run. Measuring never deletes, runs or changes anything, so it works for a project you have not trusted. The run table also says when each run ran (Ran (UTC)).

Reminders. Above the tables, the view reminds you when the project keeps more than 1 GiB in .nilavon/, when saved runs ran more than 90 days ago (with how much they hold, and how much of it is waveforms that Delete old waveforms with 90 days would remove), and when build scratch passes 256 MiB. A reminder only informs: nothing expires and nothing is deleted until you choose to (ADR 0178, 2026-11-02 addendum).

Deleting. Each recipe, generic and General RTL run in the table has a Delete… button. It offers only what that run holds: its Waveform, its Simulation log, its Results files (the simulator’s raw results; every outcome, count and failure detail stays in the run record), its Build scratch, or the Whole run. Choose one and press Show what will be deleted: Studio lists the exact files and their size and says what reports will show afterwards. Nothing is deleted until you press the red Delete … button under that list. Below the table, Delete old waveforms does the same for the waveform of every run that finished more than the number of days you enter (30 by default).

Two kinds of run are protected: the latest run of its kind (the one the project shows) and a run a waiver was proposed from. Studio says why, and you must also tick Delete from this protected run anyway (for old waveforms, Also delete from the protected run; otherwise protected runs are skipped). Deleting changes the project, so an untrusted project asks the trust question first.

Every deletion is recorded before anything is removed, in .nilavon/deletions/ (who: you, from Studio or the command line; when; which run and files; and the hash each file had). So:

• A report, comparison or evidence pack of the run says the file was “deleted by the user on date” and still works; it never reads as a changed or tampered file. The pack leaves the file out and carries the deletion record instead.
• A deleted whole run leaves the history. Reports, comparisons, packs and waivers that name it say it was deleted on that date. The view lists every deletion under Deleted from this project.
• Opening a deleted waveform says it was deleted, instead of “no longer exists”.
• After deleting a log, --honor-waivers can no longer excuse that run in CI, because the log was what showed how the simulator exited.
• After deleting results files, reports (JUnit too), comparisons and failure details are unchanged; what is gone is only the raw simulator output, such as pytest’s + where … explanation lines.
• Nilavon refuses to delete a file that already changed since the run, because the record would hide the change.

The policy, in short:

• Nilavon never deletes or expires saved runs by itself; they stay until you remove them.
• A run’s build/ folder is simulator scratch. You may delete it, here or by hand: reports, evidence packs, comparisons and the run history do not read it.
• Delete a waveform, a log, results files or a whole run only through Nilavon. Deleted by hand, a record, log, results or waveform makes its report and evidence pack refuse the run, because nothing records that you removed it on purpose. A run record is never deleted on its own (it is the run: delete the whole run), and review executions are not offered.
• Records, logs and results contain paths of this computer, and an evidence pack copies them byte for byte; waveforms, generated tests, plans, review copies and Kept RTL of earlier runs contain your design; waivers and review approvals contain the reviewer’s name.
• Kept RTL of earlier runs (.nilavon/kept-rtl/) is a copy of each RTL file a run used, kept so a run’s report and evidence pack still have its sources after you re-check edited RTL. One copy serves every run that used the same file, so deleting a run does not remove it; it stays while the project does. Removing a copy by hand only makes that run’s report say its source changed again, as for runs from before copies were kept.
• Reports and evidence packs you saved are your own files outside .nilavon/ and are not counted.

From the command line, nilavon project-storage --project-root . --format markdown prints the same view, and nilavon delete-saved-run deletes (add --dry-run first to see the plan):

nilavon delete-saved-run --project nilavon-project.json --run-id run-… --what waveform --dry-run
nilavon delete-saved-run --project nilavon-project.json --run-id run-… --what results
nilavon delete-saved-run --project nilavon-project.json --run-id run-… --what run --reason "old"
nilavon delete-saved-run --project-root . --waveforms-older-than 30 [--allow-protected]

--allow-protected is the command line’s second confirmation. See Saved-run storage and retention and the ADR 0178 addendum.

10. Troubleshooting

11. Supported today and not supported

Taken only from the committed documents cited in each row.