Design verification on the way to tapeout

Verification is reported to consume 60 to 70% of engineering effort in chip projects, per Wilson Research Group functional verification study data, and a respin is the most expensive outcome in the calendar. That effort is bounded by what simulation and coverage can establish, which is not the same as correctness.

Coverage is a proxy, not a proof

Not all of signoff is empirical, and the parts that aren't are the parts that work. Logic equivalence checking proves that a netlist implements the RTL it came from, over every input. Formal property verification proves a stated property holds on every input. Both are ordinary practice, and both need something written down to check against: an earlier design, or a property somebody wrote.

Whether the RTL does what the specification meant has neither. Simulation, emulation, and coverage closure answer that question, and they answer a narrower one than the tapeout decision actually depends on. They establish that the design behaved correctly on the stimulus it was given. The decision needs to know it behaves correctly on stimulus nobody wrote.

The gap between those two statements is where respins come from, and it does not close by adding engineers or simulation hours. It's the same limit that model compilation runs into, met from the other end of the pipeline.

Source: Harry Foster, Siemens EDA, on Wilson Research Group functional verification study data, Verification Horizons, September 2025(opens in a new tab)

Signoff

Verified against manufacturing rules

The same toolchain that proves a lowering also produces layouts that pass manufacturing checks, so the verification argument and the physical result come from one pipeline rather than two.

Clean manufacturing signoff on a real PDK: zero DRC, LVS, antenna and routing violations under Sky130 signoff parameters. Behavior is confirmed on physical silicon, on a Nexys A7-100T, Artix-7, flashed over JTAG and read back over UART.

Four vectors, independently

One toolchain serves all four, one at each layer of the lowering. The specification is solved as logic, the interpreter's run is held against a separately written implementation, the sequential model is simulated as RTL, and the placement is executed on the fabric. The four methods share no failure mode, so agreement across them is evidence that no single method provides on its own.

LOGOS Supercompiler

one language, English. one tool, LOGOS.

  1. Specify

    One executable source

  2. Compile

    Placement onto the fabric

  3. Prove

    Obligations discharged

  4. Check

    Re-derived independently

Four layers of one chip, pulled apart, each checked by its own vectorFour square layers seen from a low camera, pulled apart so each can be read: the source, drawn as lines of English; the interpreter, drawn as an evaluation tree; the register virtual machine, drawn as a register file; and the dataflow tiles, drawn as an eight by eight grid. One beam drops from the toolchain through the center of every layer, glowing where it lands, and dashed guides between the corners show that the layers stack into one chip. From the right, four probes touch the four layers, one each, numbered to match the list below.01020304

  1. Layer 01.

    Source

    LOGOS, the executable specification

    checked by Formal SAT solving

    Exhaustive across the primitive's input boundaries

    from the toolchain: the specification parsed to logic, and the obligations the lowering opens

  2. Layer 02.

    Interpreter

    Reference semantics, software

    checked by Reference oracle

    Continuous comparison, independent implementation

    from the toolchain: the interpreter's run of the same source, held against a separately written implementation

  3. Layer 03.

    Register VM

    Sequential execution model

    checked by Soft core RTL

    Simulated against the same reference

    from the toolchain: the same program in its sequential form, and the reference to hold it to

  4. Layer 04.

    Dataflow tiles

    Spatial placement, physical fabric

    checked by Physical fabric

    Executed on hardware, results read back over UART

    from the toolchain: the placement onto the fabric, flashed over JTAG

one language, one toolThe specification is written in English. LOGOS carries it down through every layer, and the meaning does not change on the way. What every layer computes is the int8 quantized matmul primitive: the same program, in another form.

agreementFour layers, four independent readings of one primitive. The methods share no failure mode, so agreement across them is evidence that no single method establishes on its own.

One chip pulled apart into its four layers, from the English source down to the dataflow tiles, with one toolchain serving one check at every layer: exhaustive solving at the source, a separately written implementation against the interpreter, RTL simulation against the sequential model, and execution on hardware for the fabric. Because none of the checks shares a failure mode with another, agreement across all four is stronger evidence than any one of them repeated. The scope is the int8 quantized matmul primitive, not arbitrary programs.

The specification is the input, not a document beside it

Assertions are written by hand today, from a specification that is prose. The prose is where the ambiguity lives, and an assertion that faithfully encodes a sentence somebody misread is a passing check on the wrong property.

The toolchain parses the sentence itself. Below are three protocol properties, each one an English sentence from the compiler's hardware test corpus and the assertion it produced.

  1. Specification, in LOGOS

    SystemVerilog assertion

    AXI write address stability, a strong until

    assert property (@(posedge clk) Assert_AWVALID_ |-> (Assert_AWREADY_ || (Remain_AWVALID_ && s_eventually((Remain_AWVALID_ until Assert_AWREADY_)))));

  2. Specification, in LOGOS

    SystemVerilog assertion

    APB access phase

    assert property (@(posedge clk) (psel && Assert_PENABLE_) |-> ##[0:1] Follow_PREADY_);

  3. Specification, in LOGOS

    SystemVerilog assertion

    APB protocol exclusion

    assert property (@(posedge clk) !(Assert_PSEL_) |-> !(Assert_PENABLE_));

Real output from the LOGOS compiler, at a posedge clk clock. Symbol names are shared with the parsed specification on purpose, so a solver can check the assertion and the sentence agree. Every pair here can be regenerated in your browser: press Compile and the compiler produces the assertion again, locally. Edit the sentence to compile something the corpus does not contain.

Each assertion is derived from a formally parsed sentence, and the parse is the artifact a reviewer can check. The output is a set of properties to run against RTL in the tool the program already uses, so what changes is where they come from.

Source: The compiler and its hardware test corpus, on GitHub(opens in a new tab)

Buying the silicon rather than designing it? Model bring-up on new silicon

How is that established without relying on coverage?

How the obligation is discharged