Verification¶

Verification covers the language constructs and special support to ease design verification.

Assertions¶

Assertions are considered debug statements. This means that they can not have side effects on non-debug statements.

Pyrope supports a syntax close to Verilog for assertions. The language is designed to have 3 levels of assertion checking: compilation time, simulation runtime, and formal verification time.

There are 3 verification statements, and the difference between them is who discharges the obligation:

cassert(expr [, "msg"]) — an elaboration check. The upass must fold it to true at compile time; if it cannot, that is a compile error. cassert never reaches the formal engine, never becomes a runtime check, and never appears in the netlist. Use it for facts about comptime values (generic parameters, widths, table contents).
assert(expr [, "msg"]) — a design obligation. pass.formal tries to prove it at compile time, and checks are emitted into the Verilog netlist. TBD: the runtime fallback for design-body assertions in lhd sim is not implemented; lhd sim currently checks only assertions inside test blocks.
assume(expr [, "msg"]) — a constraint the tool may rely on, and therefore one it must first justify. Every plain assume is always checked (an obligation), in a design body and in a formal block alike, whatever it touches. Each assume is proven independently (no other assume is used as a hypothesis, so assumes can never prove each other), and only a proven assume becomes a hypothesis for the surrounding asserts. A refuted assume is a build error — it can never silently prune a real counterexample. The compile-time check has a short budget, so an assume it cannot decide stays unchecked (a runtime check) until lhd formal verify checks it.
assume_nocheck(expr) — the only form that constrains without a check: an environment constraint by user fiat, disclosed in every verdict (see Formal blocks).

The distinction that matters in practice: cassert is "the compiler must know this now", assert is "this must be true of the hardware".

Use the parenthesized form: assert(expr), cassert(expr), assume(expr). A trailing message belongs to the statement: assert(expr, "message").

comptime const W = 8
cassert(W % 2 == 0)    // elaboration: folds to true, or the build fails

a = 3
assert(a == 3)         // design obligation: proven, else a runtime check

comb max_not_zero(a, b) -> (result) {
  assume(a > 0)        // proven first; only then used as a hypothesis
  result = if a > b { a } else { b }
}

Where an `assume` can be discharged¶

An assume over a lambda's free inputs cannot be proven in isolation — inputs are unconstrained, so some input value always falsifies it. What happens next depends on where the lambda sits:

At the top module, the inputs are the design boundary, so there is nothing left to constrain them: the assume is reported refuted and the build fails (assume-refuted). Pass --set compile.formal.on_refute=warn to downgrade it, or spell an intended environment constraint assume_nocheck(expr), which constrains without a check.
In an instantiated module, the parent's drivers are what make it true, so the check is deferred with a warning and kept as a runtime check.

Warning

A guarded verification statement does not inherit its guard today — if cond { assert(x) } is lowered as an unconditional assert(x). Write the guard into the condition instead:

assert(cond implies x == 3, "only claimed when cond holds")

The if-wrapped form is a known compiler bug, not a style choice.

The recommendation is to write as many assert and assume as possible. assume is the stronger statement: it tells the tool a case cannot happen, and a proven one is available to the optimizer as a don't-care.

Compile-time prints¶

cputs(msg) is the compile-time analog of puts. The compiler evaluates the single string argument during elaboration and emits it on the compiler's stderr, so the message is visible while the design is being built rather than during simulation. Like every puts/assert message, each cputs output is prefixed with its source origin — <file>:<line>:cputs: — on its own line so it can be grepped out of the surrounding compiler log and traced back to the statement that produced it:

<file>:<line>:cputs:<message>

Rules:

Exactly one argument is accepted.
The argument must resolve to a comptime-known string. String interpolation ("a is {a}") folds at compile time when its embedded values are comptime-known.
Any deviation — extra arguments, non-string operand, or an operand that cannot be folded to a known value at compile time — is a compile error, not a runtime print emitted at simulation.

a = 7
cputs("a is {a}")    // prints: foo.prp:2:cputs:a is 7
cputs("plain")       // prints: foo.prp:3:cputs:plain

b = some_runtime_signal
cputs("b is {b}")    // compile error: operand not comptime-known

Use cputs for elaboration-time diagnostics (which branch of a comptime if was taken, which generic parameter was selected, etc.); use puts for messages that should appear in the simulator at run time.

Note

cputs currently resolves only at file top-level scope. Inside a lambda body — including inside a comptime if within one — it is an undefined call. Until that is lifted, elaboration tracing inside a lambda is not available.

Illegal operations¶

The compiler never aborts on bad user input — every illegal operation is a clean compile error. An illegal or undefined low-level operation yields nil (e.g. division/modulo by zero, or arithmetic on a nil/uninitialized operand), and a nil produced by an arithmetic operation, or a nil used as an if / while condition, is reported as a compile error rather than silently folding to a degenerate value.

LEC¶

Logical equivalence checking is a tool command, not a language construct:

lhd lec --ref pyrope:gold.prp --impl pyrope:impl.prp --top mod_name

--ref is the gold model and --impl the implementation; the gold model's unknown output bits check against any value for the equivalent implementation bit. lec handles sequential designs as well as combinational ones — a flop-cut inductive miter plus BMC, so registers and reset are modelled.

lhd lec takes no formal block sidecar: a block is an independent test (see Formal blocks) while lec has a single obligation, so a block's assumes could only ever apply globally. Prove blocks with lhd formal verify; an environment constraint meant for lec belongs in the design itself, spelled assume_nocheck(expr) (a plain assume constrains the miter only once it is proven).

A plain assume over a module's own registers is the way to state a state invariant that makes an equivalence inductive. When lec can only prove a pair up to its bound, it prints the induction step's counterexample, including the register values it started from (state: last=0). If that state is unreachable, for example a one-hot register that is zero, write the invariant next to the register:

reg last:U4 = 1
assume(last#+[..] == 1)   // one-hot: proven by induction, then used by lec

The compile proves it by induction from the register's initial value, and lec then uses it as a hypothesis ("PROVEN under 1 proven assume(s)"), so the implementation does not have to copy the reference's behavior in states that can never occur.

Note

The recommendation is to use assume and assert frequently, including to check preconditions and postconditions of methods. The 1949 Turing quote of how to write assertions and programs is still valid "the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows."

Not implemented

An in-language lec(gold, `impl`) call and a lec_valid variant that compares only .[valid] outputs are both TBD; neither exists today. Use the lhd lec command above. See TBD.

Coverage¶

The goal of an assertion is to be true all the time; the goal of a coverage point is to be true at least once during testing.

Not implemented

cover and covercase are TBD — neither exists today, in a design body, a test, or a formal block. The intended meaning is recorded in TBD: cover(cond [, msg]) must be true at least once during verification, and covercase(grp, cond [, msg]) groups several covers so that one arm of the group must be true each time.

Reset and verification¶

In hardware it is common to have an undefined state during the reset period. An assert in a design body is checked in the run window after reset; an assert_always is checked at every cycle, reset included. That pair is the whole reset story — write assert_always when the claim must survive reset.

Not implemented

Valid-based gating (skipping a check while any operand is .[valid]-false) does not exist: only the condition itself is wired into the obligation. Neither does the always_ statement family (always_assert, always_cassert, always_assume, always_cover, always_covercase) — the implemented spelling is assert_always.

Random¶

Not implemented

.[rand] (simulation-time) and .[crand] (elaboration-time) random value generation are TBD. Both are rejected in test blocks and design bodies today; they survive only where they constant-fold. The intended semantics — pick within the type's min/max, pick an entry when applied to a tuple, and a compile error for string/range/lambda types — are recorded in TBD.

Test¶

A test is a debug-only block named by a dotted identifier (a selector path), with optional runtime parameters and no return: test name.path [(params)] { stmts+ }. See Testing for naming, parameters, and the tick cycle loop.

TBD

lhd sim runs neither form below yet: it finds no test nested in a top-scope for (no test blocks found), and it rejects a for statement inside a test body (unsupported statement in test: for_statement). Write a cycle loop as tick N { … }. See Implementation status.

Many parallel testsSingle large test

comb add(a, b) -> (r) { r = a + b }

for a in 0..=20 {
  for b in 0..=20 {
    test add.sweep {
       cassert(a + b == add(a=a, b=b))
    }
  }
}

comb add(a, b) -> (r) { r = a + b }

test add.batch {
  for a in 0..=20 {
    for b in 0..=20 {
       cassert(a + b == add(a=a, b=b))
    }
  }
}

To drive a stateful design across cycles, declare it once as an instance and run a tick N loop: each iteration is one cycle, field writes drive that cycle's inputs, step is the clock edge (exactly one per iteration), and reads below the step sample that cycle's outputs. The instance's Clock input auto-wires to the tick's minted clock. A mut declared before the loop captures the result for an end-of-simulation assert. This is the form the lhd sim runner executes (see Running cycles):

mod counter(enable:Bool) -> (value:U8@[0]) {
  reg count:U8 = 0

  value = count                     // combinational read of count.q -> @[0]

  if enable { wrap count += 1 }
}

test counter.held_high {
  mut acc     = counter             // one persistent instance
  mut v_final = nil
  tick 20 {                         // 20 cycles, one clock edge per iteration
    acc.enable = true               // drive this cycle's input (pre-edge)
    step                            // the clock edge
    v_final = acc.value             // sample this cycle's output (post-edge)
  }
  assert(v_final == 20)
}

A step may also appear outside a tick loop: it advances one clock cycle, and the test continues from that given point (the lower-level, manual-stepping style of the concurrent-thread testbench layer; not yet run by lhd sim). This is useful for when a lambda is instantiated and we want to check/update the inputs/outputs.

// mod: output 'value' is combinational (reads register directly)
mod counter_mod(update:Bool) -> (value:U8@[0]) {
  reg count:U8 = 0

  value = count              // combinational output (no extra flop) -> @[0]

  if update { wrap count = count + 1 }
}

// pipe: 'value' lands 1 cycle after the inputs (no comb input-to-output path)
// Same logic, but output is delayed by 1 cycle compared to mod version
pipe[1] counter_pipe(update:Bool) -> (value:U8) {
  reg count:U8 = 0

  value = count              // reads state q; the appended output flop lands it 1 cycle later

  if update { wrap count = count + 1 }
}

test counter.cycles {

  mut inp = true
  wire inp_w = inp                   // single-driver net feeding the call
  mut x = counter_mod(inp_w)

  assert(x == 0) // x.value == 0
  assert(inp == true)

  step

  assert(x == 1)
  inp = false

  step

  assert(x == 1)
  assert(inp == false)
  inp = true

  assert(inp == true)
  assert(x == 1)

  step

  assert(inp == true)
  assert(x == 2)
}

During test simulation, all the assertions are checked but the test does not stop with a failure until the end.

Not implemented

assert.[failed] — reading or clearing an accumulated failure flag so a test can assert that an assertion did fail — is TBD. There is no assert object to read today.

Warning

An assert written in a design body is not executed by lhd sim at all: the simulation code generator skips every property node, so a violated design assert reports PASS. Only assertions written inside the test block itself are checked at simulation time. Design-body asserts are checked by pass.formal at compile time and emitted into the Verilog netlist, but the simulation runtime fallback is TBD.

Formal blocks¶

A formal block is a declarative verification overlay, named by a dotted identifier exactly like a test: formal name.path { stmts+ }. It differs from a test in two ways: every statement is a claim that must hold at every cycle (there is no step/tick — nothing is procedural), and it never lowers to hardware or simulation — the design compile skips it entirely, and only lhd formal verify consumes it. This lets a design and its properties live in one file, or the properties in a separate sidecar file that is versioned and reviewed like source code.

Blocks are independent tests. Exactly like test blocks, they are not run together: each block's assumes constrain only that block's own obligations, so two blocks may carry mutually exclusive assumes and both still prove. A block bound to a submodule with N instances is still one block with one assume set (all N instances in force together). assumes written in the design itself are the other tier, shared by every block: an assume_nocheck is always in force, and a plain assume is in force once it is proven. A block whose own assume set is contradictory is named and fails the run; its proofs would be vacuous.

The body binds the design with the test-block import/alias style, then states properties over dotted signal paths: top input/output ports, registers reached through instance names, and — for a block bound to a submodule — the target instance's own input/output ports (the block is checked once per instance, reported [block@instance]):

assert(expr [, "msg"]) — must hold at every checked cycle (after reset).
assert_always(expr [, "msg"]) — must hold at every cycle, reset included.
assume(expr [, "msg"]) — always a proof obligation (prove-then-use), whatever expr touches: the tool proves it before using it, a proven cycle constrains the remaining properties, and a false claim is REFUTED — it can never silently fake a proof. Over primary inputs only nothing forces it to hold, so it refutes unless it is a tautology, and the refute points at assume_nocheck: an intended environment constraint is spelled assume_nocheck(expr) (below). A contradictory assume set is reported and fails the run, never silently vacuous.
assume_nocheck(expr) — the explicit environment constraint: a free constraint by user fiat, even over state, assumed without a check and disclosed in every verdict ("under N unchecked assume(s)"), with no warning. assume_nocheck_formal(expr) is the same constraint with a per-use warning. assume_nocheck_synth(expr) is invisible to verification (a synthesis-only don't-care).

// cnt.prp — the design
mod cnt(enable:Bool) -> (value:U8@[0]) {
  reg count:U8 = 0
  reg par:Bool = false
  value = count
  if enable {
    wrap count += 1
    par = not par
  }
}

// cnt.verify.prp — a sidecar of formal blocks (never becomes hardware)
const top = import("cnt.cnt")

formal cnt.parity {
  mut acc = top
  assert(U1(acc.par) == acc.count#[0], "parity tracks bit0")
}

formal cnt.bounded {
  mut acc = top
  assume_nocheck(not acc.enable)     // environment: the counter never runs
  assert(acc.count != 5, "frozen")   // provable under the assume
}

lhd formal verify cnt.prp cnt.verify.prp --top cnt --set formal.bound=10 --workdir w
#   assert at cnt.verify.prp:5 "'parity tracks bit0'" [cnt.parity]: PROVEN (inductive — every cycle of every bound)
#   assume at cnt.verify.prp:10 [cnt.bounded]: in force (UNCHECKED assume_nocheck; verdicts are conditional and unchecked)
#   assert at cnt.verify.prp:11 "'frozen'" [cnt.bounded]: PROVEN (inductive — every cycle of every bound)
lhd formal verify cnt.prp cnt.verify.prp --top cnt --formal 'cnt.parity'  # run one block
jq '.obligations' w/formal_report.json   # the same table machine-readable, every PASSED
                                         # obligation included; a REFUTED run adds
                                         # formalfail.prp/.json + a replay VCD under w/

The dotted block name is the enable/disable handle (--formal <glob> selects blocks); presence in the file list is the activation — there is no registration step. Property expressions are ordinary Pyrope (casts, bit selects, operators): the tool compiles each block through the normal compiler, so their semantics can never diverge from the language. The same sidecar format is the target for tool-mined invariants: proven helper facts are emitted as formal blocks with provenance comments, re-checked on every run, and speed up the remaining proofs.

Hierarchy access from verification code¶

A verification statement reads design signals the same way any other Pyrope code does: through the instance hierarchy, by name. A formal block binds the design with an alias and then uses dotted paths (acc.core0.count); a test block reads signals with bare dotted access and drives registers through a regref bound outside the tick loop.

Both reference spellings reach nested registers: regref(acc.core0.count) and regref("acc/core0.count"). Every intermediate component names a child instance; the last component must resolve to a writable register or memory word. An output such as acc.core0.fifo0.full is read directly and cannot be written through a reference.

Not implemented

The multi-match string path — one regref resolving to zero or many cells across the elaborated hierarchy, the synthesizable form described in Register reference — and the bind-style monitor pattern built on it are TBD, and are not needed for assert/assume today. See TBD.

Verification¶

Assertions¶

Where an assume can be discharged¶

Compile-time prints¶

Illegal operations¶

LEC¶

Coverage¶

Reset and verification¶

Random¶

Test¶

Formal blocks¶

Hierarchy access from verification code¶

Where an `assume` can be discharged¶