Sample prompts

These are representative, not exhaustive. Phrase things the way you would to an engineer — naming the unit and the spec path removes guesswork, and stating a time budget is more effective than asking for a depth.

Getting started

Set up this project for formal verification.

Bring-up: build, clocks, resets, initial constraints, scaffolding. Expect a report on what it black-boxed and why.

Use docs/spec.md to develop a formal checker for src/my_block.

Spec-driven assertion generation. Expect SVA plus the constraint modeling it needed, each property traced to a spec statement.

I don't have a spec. Use design intent to create a reasonable checker and let me know what you find.

Intent inference from RTL. Read the stated assumptions carefully — this is the path where a plausible-looking but wrong checker is most likely to appear.

Bug hunting

Look for bugs in this design unit.

Broad hunt. Engines run in concert; output is a triaged failure list with waveforms.

Do a ten minute run to shake out issues.

Time-boxed. Stating a budget is the cleanest way to control depth; the agent trades exhaustiveness for coverage of the easy space and tells you where it stopped.

I suspect there's a bug where a pop during the same cycle as a reset drops an entry. Use formal to investigate.

Directed. It builds a targeted property and, if reachable, a minimal counterexample. A clean result comes back with the bound, not as an unqualified pass.

Properties and proofs

Verify data integrity and ordering in this design unit.

The end-to-end data-transport class: no drop, no duplication, no corruption, ordering preserved. Typically needs abstraction to converge; expect it to propose one.

We need an unbounded proof of no_double_grant, which isn't converging. Strengthen it or find a violation.

The convergence loop: helpers, reductions, case splits, assume–guarantee, then induction or IC3. If it cannot close it, it should say what is blocking and what bound it achieved.

Do a scaling analysis on FIFO_DEPTH and NUM_PORTS to identify solver bottlenecks.

When parameters (depth, width, instance count) can be instantiated at lower values, this finds which ones are actually costing you proof time.

Quality of the verification

Do mutation analysis to see if our checker has teeth.

Injects faults and reports which ones the checkers catch. The gaps are the useful part of the output.

Run an overconstraint audit.

Confirms you have not proven something about a design that cannot happen. Ask for it rather than assuming it happened.

Prompting notes

• Name the unit and the spec path. "The ALU" may mean several blocks in a large design; src/exu/alu_ctl.sv means one.
• State a time budget rather than a depth.
• Ask for the plan first when you want to review methodology before compute is spent.
• "Why?" is a supported question. When a result is inconclusive, the agent explains what blocked the proof, not just the status.
• Override when you care. It picks formal by default and simulation when the request implies stimulus. If you want the other one, say so.

What Bitlevel Agents can do

The full menu. Anything in the right column is something you can ask for directly.