# Formal-results examples

Original source and command files: MIT. Original observations: CC BY 4.0. Copy these text files into a separate working directory. No external solver, library or binary is distributed.

Pin: the measured binary reports Yosys 0.70+post and revision `0c11ea098be065e585a90a06e7b7da49936cf231`. The official `v0.70` tag points to `28ba3cb926fe376fa05ebfc1b921747d011d4557`. The tag and binary-reported revision are recorded separately; the binary was not independently rebuilt from the tag. The current run record includes its binary hash, operating-system version and architecture; the archived earlier record also retains the bottle hash. These examples use the built-in SAT engine.

## Exact commands

```sh
yosys -Q -T -s bounded_5.ys
yosys -Q -T -s deeper_6.ys
yosys -Q -T -s masked_bounded.ys
yosys -Q -T -s cover_masked.ys
yosys -Q -T -s cover_unmasked.ys
yosys -Q -T -s weak_induction.ys
yosys -Q -T -s strengthened_induction.ys
yosys -Q -T -s weak_induction_depth2.ys
```

The expected outcomes in order are: bounded success through 5 steps; counterexample at 6 steps; assumption-masked bounded success; no witness for the constrained four-step target; witness for the unconstrained four-step target; incomplete one-step induction; completed one-step strengthened induction; completed weak-property induction at length two. A zero process exit status is not by itself a proof verdict. Read the literal result in `/data/measurements/printed-hdl/P15-yosys.json`.

The three SystemVerilog files are printed verbatim on the page. Each `.ys` file preserves the exact preparation and SAT query. Yosys 0.70+post emits formal `$check` cells; `chformal -lower` converts them before SAT. The first rejected assumption import and the required lowering step are retained in the measurement record. No HDL workaround replaced the rejected assumption.

The cover statement names the target. The command removes that declarative cell after lowering and poses the same reachability question with `-set-at 4 target 1`. This is a bounded SAT target query, not a SymbiYosys cover run. The masked version enforces assumptions; the unmasked version does not. Initial register values are explicit in the source.

WaveJSON files retain the deeper counterexample, the unmasked target witness and the counterexample to the weak induction step. The last starts from an unreachable state permitted by the weak hypothesis; it is not a reachable initial-state bug. Strengthening the property proves the missing invariant rather than assuming it.

The corrected induction commands omit `-seq 1`, which under `-tempinduct` defers the property until after step one. Their base checks now include the declared initial state. Weak induction fails only at length one here; a depth-two induction proves the unchanged weak property. Earlier commands/witnesses remain in `earlier-p8/`; earlier records remain under `../../measurements/printed-hdl/earlier-p8/`.