Workflows

Two patterns

Testplan-guided. Point the agent at a design unit and its spec, ask for a verification testplan, review it, then work through the items. Best when you are standing up verification on a new block and want coverage you can account for.

Freeform. Just ask. Best for debugging, exploring an unfamiliar design, or a quick sanity check — "is there any way full and empty are both high?"

They are not modes; they are habits. A typical session opens with a testplan to get oriented, drops into freeform to chase one failure, and returns to the plan. The agent keeps the artifacts consistent either way.

Testplan-guided verification

Scenario: you are bringing up soc_ifc, the SoC-facing boundary of the Caliptra core, and you have its spec as a PDF or Markdown in the repo.

1. Scope

Read the Caliptra integration spec in docs/ and src/soc_ifc. Give me a design summary, a proposed methodology, and a testplan for the mailbox — but show me the plan before you build anything.

The agent returns a design summary, a proposed methodology (end-to-end vs. interface vs. property-set), a decomposition if the unit is too large to attack whole, and a testplan enumerating features and the checks that cover them. Review it. Correct wrong assumptions now — it is far cheaper than after the checkers exist. The plan is saved as a file in the repo, so you can edit it directly too.

2. Bring-up

Go ahead and set up the environment.

Build, clock and reset setup, initial constraints, black-boxing and abstraction of anything out of scope. Expect a sanity report: covers reachable, no properties passing vacuously, the reset sequence actually completing. If it does not volunteer that report, ask for it.

3. Checkers

Implement the plan. Interface checkers first, then the end-to-end properties, then covers.

Constraints are written as modeling code with the intent recorded, not as bare assumes. Ask for the mapping from testplan item to assertion so you can see what is and is not covered:

Show me which assertion covers each testplan item, and which items have no assertion yet.

4. First-pass bug hunt

Do a ten minute bounded run plus ABH and triage what fires.

Short bounded runs and agentic bug-hunting shake out the easy failures before you spend hours on proofs. The output is a triaged list — real design bugs, checker bugs, environment or constraint artifacts — and every bounded result carries the depth it reached, so you know how clean the design is.

5. Convergence

This is where the main work lies. For each property that will not close, the agent applies helper assertions, safe reductions, case splitting, abstraction and assume–guarantee decomposition, then hands the strengthened problem to k-induction or IC3.

mbox_data_integrity is stuck at bounded pass. Strengthen it or find a violation, and tell me which technique moved the needle.

It should tell you which technique worked and what the residual proof depth is. If it cannot close the proof, it says what is blocking and what bound it achieved — never an unqualified pass.

6. Sign-off

Give me proof status per property, an overconstraint audit, and run mutation analysis on the checkers.

Coverage analysis, mutation analysis to confirm the checkers have teeth, an overconstraint audit to confirm you have not proven something about a design that cannot happen, and a regression that reproduces every result. Status per property is one of proven, bounded-proven to depth N, or inconclusive with a reason.

Freeform chat

Scenario: you want to sanity-check the mailbox arbiter and see a concrete sequence.

Ask for a directed simulation

The agent defaults to formal, which is exhaustive for assertion-style questions. When you want stimulus-driven behavior — this input, that output — ask for simulation explicitly:

Write a directed test that pushes four entries into the mailbox from the SoC side while the uC is reading, and show me the waveform.

It writes the test, runs it, and hands back a VCD. Phrases like "prove that…" bias toward formal; "show me a trace where…" biases toward simulation.

Look at the trace

Open the VCD in GTKWave or Surfer on the VNC desktop, or read the .delta file next to it — a plain listing of every value change, usually faster than the waveform for a first look.

Ask the spec

When you do not know how something is supposed to work, ask. Name the spec file and the agent grounds its answer in it, with the section it drew from:

According to the integration spec in docs/, what happens to a pending mailbox command on a warm reset, and does the RTL do that?

Request formal explicitly

Use formal to prove that mbox_lock is never granted to both the uC and the SoC in the same cycle. I want an unbounded proof.

If it holds, you get the proof and the assumptions it relied on. If not, a counterexample waveform, and an explanation of whether it is a bug or a missing constraint.