Formal property catalogue¶
This is the public proof inventory for the MIF-owned SymbiYosys layer. Each stable ID names one semantic assertion or non-vacuity witness. The generated JSON manifest binds these names to exact proof inputs and digests.
A prove task uses its configured depth as a k-induction horizon; a cover task uses it as a bounded witness horizon. Neither is a nanosecond claim. Device timing remains separately hardware-gated.
The catalogue currently names 40 properties: 25 safety, 8 liveness, and 7 cycle-timing. The MIF-010 target is 70; the generated manifest reports target status from named entries only.
Raw assert/cover/assume token counts are retained in the JSON only as CI hygiene. Shared macro definitions can be counted in several tasks, so token totals are not proof identities or evidence of specification coverage.
mif_adc_to_spike_quantiser_safety¶
- Suite:
safety - Mode:
prove - Depth:
12(k-induction horizon) - Task:
hdl/formal/safety/mif_adc_to_spike_quantiser_safety.sby
Depth rationale: Prove mode uses k-induction. The properties need reset anchoring plus one defined $past cycle; depth 12 conservatively exceeds that two-cycle semantic horizon while exercising presentation, stall, acceptance, and queued-event state transitions.
Named properties:
mif.adc.backpressure.valid-held(assertion) — A presented AER event remains valid while the sink is stalled.mif.adc.backpressure.address-stable(assertion) — The presented AER address remains stable while the sink is stalled.mif.adc.address.legal(assertion) — The AER address is always one of the configured positive or negative spike codes.mif.adc.handshake.withdraw-requires-ready(assertion) — A valid event can be withdrawn only after an accepting ready cycle.mif.adc.handshake.address-change-requires-valid(assertion) — The AER address changes only while a live event is presented.
mif_aer_cdc_synchroniser_safety¶
- Suite:
safety - Mode:
prove - Depth:
8(k-induction horizon) - Task:
hdl/formal/safety/mif_aer_cdc_synchroniser_safety.sby
Depth rationale: Prove mode uses k-induction. Depth 8 covers the reset edge, the two-destination-cycle reference-pipeline warm-up, and the one-cycle registered-stage history with additional induction margin.
Named properties:
mif.aer-cdc.output.exact-two-stage-delay(assertion) — The synchronised output equals the asynchronous input delayed by exactly two destination flops after warm-up.mif.aer-cdc.output.registered-second-stage(assertion) — The synchronised output is a pure registered copy of the first-stage sample, with no combinational bypass.mif.aer-cdc.input.registered-first-stage(assertion) — The first synchroniser stage is the asynchronous input sampled on the preceding destination edge.
mif_fast_veto_gate_safety¶
- Suite:
safety - Mode:
prove - Depth:
2(k-induction horizon) - Task:
hdl/formal/safety/mif_fast_veto_gate_safety.sby
Depth rationale: Prove mode uses k-induction, but the DUT and properties are combinational. Depth 2 supplies a solver scheduling edge and an induction step; no temporal state or $past history exists in this task.
Named properties:
mif.fast-veto.veto-dominance(assertion) — An asserted safety veto immediately blocks permit and fire and raises the veto surface.mif.fast-veto.subtractive-origin(assertion) — A fast fire can only pass through an existing qualified fire under a live permit.mif.fast-veto.permit.exact-gating(assertion) — The permit exactly equals the armed, bank-ready, unvetoed threshold predicate.mif.fast-veto.interlock.exact-mirror(assertion) — The exposed veto-active signal exactly mirrors the safety veto.mif.fast-veto.disarm-blocks-output(assertion) — A disarmed lane emits neither permit nor fire.mif.fast-veto.bank-unready-blocks-permit(assertion) — A bank that is not ready cannot receive a fast permit.
mif_trigger_fabric_safety¶
- Suite:
safety - Mode:
prove - Depth:
14(k-induction horizon) - Task:
hdl/formal/safety/mif_trigger_fabric_safety.sby
Depth rationale: Prove mode uses k-induction. With LOCK_HOLD_CYCLES=5, depth 14 spans reset, a complete five-cycle debounce, the following one-shot latch, disarm/reload, and another full debounce horizon, while all $past properties have defined history.
Named properties:
mif.trigger-fabric.veto-dominance(assertion) — A safety veto prevents a trigger.mif.trigger-fabric.fire.exact-final-step(assertion) — A trigger occurs only on the final debounce step before the one-shot is latched.mif.trigger-fabric.fire.full-gating(assertion) — A trigger requires arm, bank readiness, no veto, and a current lock.mif.trigger-fabric.one-shot.blocks-retrigger(assertion) — A latched one-shot blocks concurrent retriggering.mif.trigger-fabric.counter.legal-range(assertion) — The debounce counter never exceeds its configured reload value.mif.trigger-fabric.lock.bounded-resolution(assertion) — A sustained armed lock cannot exceed the debounce bound without the one-shot firing.mif.trigger-fabric.trigger.latches-one-shot(assertion) — A trigger latches the fired state on the next cycle.mif.trigger-fabric.one-shot.persists-while-armed(assertion) — Once fired, the one-shot remains latched throughout continuous arming.mif.trigger-fabric.disarm.reloads-and-clears(assertion) — Disarming reloads the debounce counter and clears the one-shot on the next edge.mif.trigger-fabric.broken-lock.reloads(assertion) — A broken lock reloads the full debounce requirement.mif.trigger-fabric.counter.monotone-countdown(assertion) — A sustained armed lock decrements a nonzero debounce counter by exactly one per cycle.
mif_adc_to_spike_quantiser_liveness¶
- Suite:
liveness - Mode:
cover - Depth:
20(bounded witness horizon) - Task:
hdl/formal/liveness/mif_adc_to_spike_quantiser_liveness.sby
Depth rationale: Cover mode uses bounded model checking. Depth 20 comfortably spans reset release, event accumulation and presentation, at least one stalled cycle, and the subsequent ready-cycle drain witness.
Named properties:
mif.adc.witness.event-presentable(cover) — An AER event can be presented.mif.adc.witness.backpressure-reachable(cover) — A presented event can encounter sink back-pressure.mif.adc.witness.stalled-event-drains(cover) — A stalled event can be accepted when the sink returns ready.
mif_fast_veto_gate_liveness¶
- Suite:
liveness - Mode:
cover - Depth:
2(bounded witness horizon) - Task:
hdl/formal/liveness/mif_fast_veto_gate_liveness.sby
Depth rationale: Cover mode uses bounded model checking. The DUT is combinational, so depth 2 is sufficient to schedule and witness both a permitted fire and a same-cycle veto suppression without temporal warm-up.
Named properties:
mif.fast-veto.witness.fire-reachable(cover) — A qualified and permitted fast fire is reachable.mif.fast-veto.witness.veto-suppression-reachable(cover) — A qualified fire suppressed by an asserted veto is reachable.
mif_trigger_fabric_liveness¶
- Suite:
liveness - Mode:
cover - Depth:
20(bounded witness horizon) - Task:
hdl/formal/liveness/mif_trigger_fabric_liveness.sby
Depth rationale: Cover mode uses bounded model checking. Depth 20 exceeds reset plus the five-cycle debounce, trigger and one-shot latch, disarm clear, and a second arming horizon, so all three non-vacuity witnesses fit in one bound.
Named properties:
mif.trigger-fabric.witness.trigger-reachable(cover) — A trigger is reachable.mif.trigger-fabric.witness.fire-at-latency-bound(cover) — The trigger can fire on the configured final debounce step.mif.trigger-fabric.witness.one-shot-clear-reachable(cover) — The fired one-shot can clear, permitting a later re-arm.
mif_aer_cdc_synchroniser_stage_timing¶
- Suite:
timing - Mode:
prove - Depth:
10(k-induction horizon) - Task:
hdl/formal/timing/mif_aer_cdc_synchroniser_stage_timing.sby
Depth rationale: Prove mode uses k-induction. Depth 10 exceeds reset, reference-history warm-up, both one-cycle stage deadlines, and their monitor-observation edges, leaving induction margin beyond the two-cycle end-to-end contract.
Named properties:
mif.aer-cdc.timing.stage-one-within-one-cycle(assertion) — An input/first-stage disagreement is captured within one destination cycle.mif.aer-cdc.timing.stage-two-within-one-cycle(assertion) — A first-stage/output disagreement advances into the second stage within one destination cycle.
mif_fast_veto_gate_timing¶
- Suite:
timing - Mode:
prove - Depth:
10(k-induction horizon) - Task:
hdl/formal/timing/mif_fast_veto_gate_timing.sby
Depth rationale: Prove mode uses k-induction. Both monitored bounds are zero added cycles; depth 10 conservatively covers reset release, activation, monitor observation, and induction despite the stateless combinational DUT.
Named properties:
mif.fast-veto.timing.veto-zero-added-cycles(assertion) — A veto suppresses a pending qualified fire with zero added cycles.mif.fast-veto.timing.disarm-zero-added-cycles(assertion) — A disarm suppresses a pending qualified fire with zero added cycles.
mif_trigger_fabric_response_timing¶
- Suite:
timing - Mode:
prove - Depth:
20(k-induction horizon) - Task:
hdl/formal/timing/mif_trigger_fabric_response_timing.sby
Depth rationale: Prove mode uses k-induction. Depth 20 spans reset, arbitrary reachable debounce/one-shot state, each one-cycle control-response deadline, and more than two complete five-cycle debounce horizons.
Named properties:
mif.trigger-fabric.timing.disarm-response-within-one-cycle(assertion) — A disarm reloads the debounce and clears the one-shot within one cycle.mif.trigger-fabric.timing.veto-reload-within-one-cycle(assertion) — An armed veto reloads the debounce within one cycle.
mif_trigger_fabric_timing¶
- Suite:
timing - Mode:
prove - Depth:
20(k-induction horizon) - Task:
hdl/formal/timing/mif_trigger_fabric_timing.sby
Depth rationale: Prove mode uses k-induction. The monitor bound is LOCK_HOLD_CYCLES+1 (six cycles at the harness default); depth 20 exceeds reset, one complete monitored resolution window, and a second full window for induction closure.
Named properties:
mif.trigger-fabric.timing.lock-resolution-within-six-cycles(assertion) — A qualified lock resolves by trigger, lock loss, or an existing one-shot within LOCK_HOLD_CYCLES+1 cycles.