Using the workspace
Goals and evaluation
Numeric and behavior goals, verification plans, and how results stay tied to the tool that measured them.
Goals describe behavior or measurable limits the design should meet. A goal has a name/metric key, target, comparison, unit, and optional verification plan.
Goals#
| Kind | How it works |
|---|---|
| Numeric target | Compare a measured number against a limit using at most, at least, exactly, or an inclusive range. |
| Behavior goal | Describe expected behavior in text. The Architect can translate it into a testbench check; it passes only when the supported run produces matching evidence. |
- AI can derive behavior goals from requirements and project behavior. It may only keep a tool goal when a compatible run reports the exact expected metric; it must not invent performance targets or measurements.
Goals proven for every input#
A testbench checks the cases it tries. A formal proof checks every input sequence: it either shows a property always holds, or gives the exact inputs that break it. When a behavior goal states something that must be true in every cycle (“the FIFO never overflows”, “two requesters are never granted at once”, “a request is granted within 4 cycles”), the Architect backs it with a proof as well as the test.
It writes the goal as a named property in the design, inside `ifdef FORMAL, so simulation and synthesis never see it. The label is the goal's key:
`ifdef FORMAL
always @(posedge clk) if (f_past_valid && !$past(rst)) begin
fifo_no_overflow: assert (count <= DEPTH);
end
`endif| Result | What it means |
|---|---|
| Proven | The property holds in every reachable state, for every input sequence. The goal is marked Proven in Goals when its test passes too. |
| Fails | SymbiYosys found inputs that break it. The step shows the counterexample, the design's signals step by step, and it is saved under generated/formal/counterexamples/ for the waveform viewer. The workflow's repair loop gives it to the Architect, which fixes the design or the property and says which. |
| Bounded | It held for every input sequence for the proof depth (20 cycles from reset by default), but neither proof method (k-induction or PDR) closed it. The goal stays Inconclusive. Another named assert about internal state usually completes the proof. |
Note
Note
Plans and results#
- Goals can be added, edited, removed, planned, and run again.
- Prepare / update plan chooses a compatible adapter, project inputs, and a measurement, and adds the proposal to the Architect chat as a card: Apply it there. Run saved plans executes the saved steps; preparing a plan does not itself run the check.
- Reports distinguish pass, failure, missing inputs, tool errors, stale evidence, and checks that need review. A result is stale when one of its own input files changed after it was measured.
- Scenario coverage appears only when the testbench emits named coverage records; it is not automatic code coverage.
- Each measured result names its tool and links to the Workflow stage that produced it (Measured in Workflow → stage), where you can inspect and rerun that stage.
What can be measured#
Available adapters include the configured simulation, synthesis, timing, physical design, and signoff tools.
Note