2f-latch Full latch support — lgraph, Verilog, Pyrope, LEC (latch-only and mixed), simulation; unified with flops and multiple clocks

Where this stands (M8 LANDED 2026-07-24)

M0–M8 are LANDED. Latches and negedge state now work in both formal and simulation. All three false-PROVEN clock-blindness holes are closed, including the same-clock EDGE hole M4 could not reach, and every previously-vacuous latch verdict is now real. See Landed for the compressed record and Traps for what must not be re-derived.

The vehicle is M8 — edge normalization (pass.single_edge, pass/single_edge/): a conditional LGraph→LGraph pass that removes latches and negedge state before the solver ever sees them. M4's in-encoder approach stays RETIRED.

Pending M10 supersedes M8 only inside formal. M8 remains a landed standalone transformation and the independent source-vs-normalized Icarus oracle. The remaining hierarchy/memory work will not extend its phase counter or rewrite definitions in place: M10 gives LEC/BMC/verify a read-only hierarchy-aware phase schedule and encodes one combinational cone per consuming phase. Compile, synthesis, simulation and emitted LGraphs remain on the source representation.

The transformation is validated against an INDEPENDENT oracle, not against itself. single_edge_four_classes_test.sh runs the SOURCE netlist (real always_latch, real negedge) and the NORMALIZED one (posedge flops + phase divider) side by side under Icarus Verilog, the normalized side clocked P times per source period, sampled per the observation-visibility rule: they agree over 39 periods. Two negative controls prove the harness discriminates — clocking the normalized side at 1× fails, and swapping the two slot predicates fails. That is what the binding cross-model gating rule demands, and it is why the four lhd lec refutations beside it are not vacuous.

What is NOT done (deliberate, each with its reason): known-integer-ratio multi-clock slotting (step 6 — a second clock domain is SKIPPED, so encode.cpp's detected-edge branch and M6's sim model keep handling it); P>2; hierarchy (a stateful Sub fails closed); witness-index decimation back into periods (step 2d ships the honest SKIP instead); and the opposite-phase peephole. Full detail in the step tables.

2026-07-25 audit — 51 confirmed gaps, 8 soundness holes CLOSED

A 75-candidate audit (five finders, one adversarial verifier per claim; 51 CONFIRMED, 10 misscoped, 2 already-working) found that M8 closed the shapes it targeted but that the LEC encoder still had no general model of WHICH CLOCK a state element commits on. Its transition function is N = ITE(reset, initial, ITE(enable, din, Q)) and it attached a commit guard in exactly two special cases — the literal ICG shape <clock-input> & <enables> with the port named clk/clock, and ≥2 clock INPUT nets. Everything else encoded as "commits every step, the clock expression is dead code".

Eight reproducible FALSE PROVENs, all now honest (each was measured before and after):

And one two-directional error, the worst of the set: an inversion left in the CLOCK CONE (wire nclk = ~clk; always @(posedge nclk)) was invisible to commit_class_of, which kept only resolve_phase().net and took the edge from the posclk pin alone. Via the slang reader that gave a false PROVEN against posedge clk AND a false REFUTED against the identical negedge clk — while the yosys reader was correct, because its proc folds ~clk into CLK_POLARITY=0 first. So the whole negedge story was reader- and spelling-dependent. Fixed by folding .inverted into rising (the Latch branch already did this), teaching resolve_phase the x & 1 width mask, and counting negedges in the trigger from the COMMIT CLASS rather than from the pin. Pinned by two new cases in lec_clock_blindness_test.sh.

Five regressions M8 itself introduced, all fixed: the clock-gated-latch gate absorption dropped the gate's IDENTITY (now the miter refuses when the two sides normalize against different reference clocks); the lec trigger scanned only --lib cell models, never the design's own defs; the period-boundary guard rewired ASSUME conds too (an assume must constrain EVERY step — guarding it left mid-period steps free and produced a false REFUTED); a latch's ASYNC reset was folded inside the slot gate against M7's ruling; and a data-gated latch's slot depended on fast_class() order, violating condition 2. Two over-refusals also fixed: a def is only "needing normalization" if it holds a latch or a negedge flop (not merely two clock nets), and a def the user TRUSTED is a blackbox and is skipped — formal.lec.trust is the documented escape hatch for exactly the shape the pass was pre-empting.

Still open — six SILENT SIM bugs, each with a live 4-tick tracker in inou/prp/tests/sim/ (tagged fixme; every fixture carries CONTROL asserts that pass, so a failure is always attributable): latch_sim_clockgate_high (a latch gated by the clock net never commits — sim and formal verify disagree on this shape), latch_sim_l1_buffer (the L1 coincident-edge case, which the pass refuses for LEC and sim models wrongly), flop_sim_secondary_negedge (the previous-level bit is updated before phase 2, so the negedge guard is a dead false), mem_sim_negedge_write (a memory write emitted as 0 /*UNRESOLVED-CYCLE*/ when a negedge flop is present), hier_sim_negedge_sub (negedge state in a child lands a full period late), flop_sim_peek_secondary (a pre-step output read consumes a second-domain clock edge). Also open from the audit: four reader shapes that build a WRONG GRAPH from clean-compiling source (partial bit-range hold, always_latch under a for-loop, latch-on-an-unpacked-array, blocking write to an internal signal in an edge process), the latch-inference OVER-fire on a fully covered case with no default, and the oracle gaps below.

Two oracle corrections. The 8 prp-v2prp2v latch targets CANNOT FAIL: the harness returns 0 for INCONCLUSIVE and UNKNOWN, so step 3f's stated gate was never implemented. And the iverilog leg — the only INDEPENDENT oracle for the whole transformation — skips silently when iverilog is absent, and CI never installs it. Combined with latch-only designs normalizing to a clockless flop, the independent oracle covers zero latch-only, negedge or multi-clock designs today.

CLOCK GATING — recognized and encoded as a FLOP ENABLE (2026-07-25)

An ICG is the commonest latch structure in real hardware, and it was refused as a second clock domain until now. Modelling it as a gated CLOCK is both unsound here (the encoder has no clock-identity model, so a gated clock and an ungated one look identical unless the ICG name heuristic happens to fire) and wasteful (a per-step commit term on every flop). But a gated clock is a flop enable — the flop commits on the reference edge exactly when the enables hold there — so pass.single_edge now recognizes the pattern and rewrites it into the enable, which the encoder models natively at zero extra cost (user direction, 2026-07-25):

  always_latch  if (!clk) enl <= en;        always @(posedge clk)
  wire gclk = clk & enl;              -->       if (en) f <= d;
  always @(posedge gclk) f <= d;

The ENABLE-LATCH BYPASS is what makes it exact, and it is the easy thing to get wrong. A real ICG latches its enable on the opposite phase purely to suppress glitches: the latch CLOSES exactly when the flop SAMPLES, so the flop sees the value the latch is passing THROUGH, not its previously-held one. Taking the latch's Q is a full cycle late — the classic L1 error — and it is invisible to a symmetric before/after gate because both sides would be wrong identically. Measured: the first cut did exactly that, because the rewrite loop had already retyped the latch to a Flop by the time it reached the gated flop, so the bypass silently did not fire. The resolution now happens during PLANNING, before any mutation. Pinned by single_edge_icg_test.sh, whose iverilog leg agrees over 29 cycles with the gate toggling and whose negative control (use the held Q instead) FAILS.

Two scoping rules keep the blast radius honest. A CONSTANT operand is a width mask, not an enable — reading And(Not(Get_mask(clk)), 1)'s 1 as an enable made an INVERTED clock look like a gated one and silently un-fixed the negedge case. And the fold only applies in a SINGLE-clock design: a gate on a second domain (gclk = clk_b & gate while other flops run on clock) has no reference clock to be relative to, so it stays skipped for pass/lec's multi-clock machinery — which is what equiv/mclk_derived pins.

REAL DESIGNS INSTANTIATE THE GATE, and that is the case that matters. Nobody spells an ICG inline — minion has 32 prim_clk_gate u_cg(.clk_i(clk), .en_i(en), .clk_o(gclk)); instances (they are exactly the 32 defs lhdsuite's lec_trust knob lists). The gate then sits ONE MODULE LEVEL AWAY and the flop's clock_pin is an opaque Sub output that nothing downstream can recognize — so the in-graph fold above never fires and, once the encoder started refusing unmodelled derived clocks, every such flop refused. Handled by INLINING exactly those cells first: an instance that drives a state element's clock_pin AND whose def contains a latch (latch_contract::inline_clock_gate_cells, reusing the landed graph_util::inline_sub_instance). Inlining is unconditionally semantics-preserving and idempotent, so it runs on every side before any analysis, and afterwards the ordinary fold applies. Both halves of the predicate matter: "drives a clock" alone would inline a clock buffer or PLL wrapper for nothing, and "contains a latch" alone would inline half the design.

Two traps that cost time here. (1) The same pin reached through an EDGE and through Node::out_pins() does not compare equal, so a pin-keyed "does this instance drive a clock?" set silently matched nothing — key on the driving NODE instead. (2) inline_sub deliberately leaves the def in the library for its other instantiation sites, so a def_needs scan over every library graph stayed stale after the inline and refused anyway. It now walks the design's own INSTANCE TREE, and intersects that with the caller's allow-list so a def the user TRUSTED stays a blackbox (lec_trust_test — trust is the documented escape hatch for "the encoder cannot model this leaf", and refusing on its contents pre-empts the very mechanism that makes such a design provable).

Resolution FAILS CLOSED when it cannot tell the clock operand from the enable: in the canonical clk & en BOTH are graph inputs, so "is it an input?" cannot decide, and guessing backwards classifies the enable as the clock and drops the gate entirely. A cone with no identifiable clock operand, or more than one, is not an ICG — and since the encoder now refuses an unmodelled derived clock, that is an honest refusal rather than a wrong answer.

M9 — Clock_cell: ONE recognized clock operator LANDED (formal half) 2026-07-26

STATUS 2026-07-26 — steps 0-2 are LANDED; step 3 (sim) and step 4 (shrink lec_trust) are not. The design below is the record; what follows is what it actually does now.

• Ntype_op::Clock_cell = 52 (even ⇒ combinational), pins clk_ref=2 / div=3 / en=4 / invert=6. The pin ids are NOT free: get_sink_pid's fast path derives the pid from the leading char for a-f (pid == c - 'a'), so clk_ref must sit at 2 and en at 4. Mirroring Flop's clock_pin/enable is what makes that safe.
• The guardrails were not theoretical. cgen_verilog's only unknown-op guard was an I() that compiles out under -c opt, after which it emitted the cell's FIRST OPERAND — the ungated clk_ref, gate silently dropped. Named fail-closed arms now sit in build_simple_expr (unsupported-cell), create_registers (clock-cell-emission, which otherwise emitted always @(posedge 'hx)) and cgen_sim::node_expr (clock-cell-unsupported).
• Recognition lives in graph/latch_contract.cpp: match_icg_def (structural — the port both AND-ed into the output AND gating the latch's window is the clock; no name heuristic), Cone_cloner (clones ONLY the combinational enable cone into the parent, re-rooted on the instance's drivers; fails closed on any state, Sub or Memory in the cone), and materialize_clock_cells, which creates the cell, rewires the gate's readers and DELETES the instance — which is what makes the ICG's latch disappear from every latch-counting consumer.
• resolve_phase gained a Clock_cell arm so a gated clock's ROOT is its REFERENCE clock. Without it Design_clocks inserts the cell's own output into roots_, is_clock starts answering true for gated nets, and two flops committing on the very same edge land in different slots.
• Wired CONSUMER-SIDE ONLY (lhd_kernel_formal.cpp, both lec_command and verify_command), before the older inline+fold. It deliberately passes NO is_boxed: recognition respects trust rather than fighting it, and that is exactly what lets a TRUSTED gate be recognized.
• LEC lowering in pass/lec/encode.cpp: the flop path (commits = en != 0; div != 1 and invert refuse BY NAME) and the memory path (folded at ALL THREE commit points — per-port write mask, whole-array update, and the sync-read register). A Clock_cell is skipped in the encode fixpoint because it has NO DATA VALUE — and so is a Get_mask/Sext WRAPPER on a gated clock, which was a measured regression on minion (a typed 1-bit port read wraps the clock, and every such wrapper became “operand has no encodable driver”).
• Gate: lhd/tests/clock_cell_test.sh, 8 cases, every proof paired with a refutation that must still fire — including the two shapes inlining structurally cannot reach (a TRUSTED gate, and a gated MEMORY).
• The binding rule is enforced for Pyrope: illegal_clock_op (upass/tolg/upass_tolg.cpp) rejects an arithmetic or data-merging op in a clock cone with a clock-op-unsupported diagnostic; fixture inou/prp/tests/errors/clock_or_data.prp. It is a DENY-list, not an allow-list, and it is scoped to the Pyrope front-end: a hard error on any derived clock would break lec_clock_blindness_test's clk ^ sel case, which wants an ENCODER refusal, not a compile error. (Trap for that fixture: the tests/errors/ harness runs tolg:false, so a lowering-stage error needs :tolg: 1 in the header or it silently reports “no error emitted”.)

Measured. livehd //... 1446/1447 pass (baseline 1444/1445; the two extra are the new tests), zero failures; dino_lec, dino_lec_bug, dino_synth_lec_flat unchanged. //bench:minion_lec: the 30 encode refusals are GONE — it reaches the solver for the first time and now REFUTES (exit 7 → exit 10) at minion_dcache_cache_op_unit_l2, with 110/140 proven, 32 trusted, and 10 gates recognized symmetrically per side.

Still open, honestly. (1) That refutation: the earliest diverging state cut is id_running_q (ref=0 impl=1 after step s3). Two things are already ruled out — the checked-in Pyrope is NOT stale (regeneration is byte-identical) and the gate's enable cone matches TEXTUALLY on both sides (dft_i is tied to '0 on both), so this is a candidate REAL translation difference of exactly the class minion_lec exists to surface. (2) A gate whose output crosses into a Sub instance's clock PORT is not recognized — materialize_clock_cells scans only clock_pins in the SAME graph, and ctrl_frf_clk (gated in txfmafrac_top, consumed by txfma_f0) is the residual “derived clock” refusal. (3) Steps 3-4 (sim lowering, shrinking lec_trust).

User direction, 2026-07-26. M8 folds a clock gate into a flop enable when the gate is visible in the body. That is not how real designs are written: they instantiate the gate, and a Sub output is an opaque symbol. Measured on //bench:minion_lec (2026-07-26): 30 defs refuse to encode — 22 flop … has a derived clock + 8 memory … has a derived clock — while 110/140 prove and 32 more are trusted. Nothing times out; they never reach the solver.

The intuition this inverts: for a clock gate, blackboxing the proven leaf is precisely what breaks the parent. Every other leaf is fine opaque — its outputs become free symbols the parent compares. But an ICG’s output is a clock, and the encoder has no clock-identity model, so a flop whose clock_pin is an opaque Sub output cannot be given a commit condition. “Prove it, then box it” does not compose for an ICG — which is why prim_clk_gate sitting on minion’s formal.lec.trust list is self-defeating.

What the cell buys, beyond this bug. One recognized operator is the enforcement point for “nothing may be done to a clock” — the clock network becomes auditable structure instead of arbitrary logic. Formal is the first consumer, and that means BOTH drivers: lhd lec and lhd formal verify funnel into the single Encoder in pass/lec/encode.cpp (instantiated from query.cpp’s prove_equal AND prove_properties), so one lowering helper serves both. And it is deliberately the anchor for FUTURE POWER WORK: the shared ICG surviving to mapping is a power feature, not just area — gating-coverage metrics, automatic clock-gate insertion (the REVERSE of the LEC lowering: turn a flop-enable cone into a Clock_cell), and eventually power-gating domains all hang off the same operator. That is why the cell is a representation to KEEP, not a normalization to fold away.

The cell

  out_clk = Clock_cell(clk_ref, en, div=1, invert=false)

• clk_ref, en are runtime inputs; div, invert are comptime attributes. Keep the split explicit — the attributes are structural facts decided at compile time, en becomes data feeding the downstream enable cone.
• en is sampled at the ACTIVE EDGE of clk_ref — the glitch-free ICG contract. Encoding the CONTRACT, not the latch, is what keeps the physical enable latch out of the graph: the cell is combinational, so every latch-counting consumer (needs_single_edge, the pass.single_edge def scan) stops seeing ICG latches entirely.
• Everything reduces to a commit condition on the reference clock, and all three mechanisms already exist: gate → enable (M8 fold, P=1); invert → the opposite edge (slot assignment, P=2); divide → every 2^N-th edge (the single_edge_phase counter, P=2^N).

v1 is div=1 ONLY — div>1 is an honest error

User ruling 2026-07-26: “ship div=1 first as we do not have test cases for div=2 or div=4 (just flag error as not implemented)”. The syntax admits div; the lowering refuses anything but 1. Three independent reasons, all measured or cited:

• pass/single_edge/pass_single_edge.cpp:521 already refuses slots > 2 (“only P<=2 is implemented”), and the phase counter is not port-threaded across a module boundary (open question 6).
• SOUNDNESS — a divider’s INITIAL PHASE must be part of its identity. Two div-by-2 cells off one reference can run 180° apart depending on reset state; recording only div=2 makes them compare equal. That is exactly the clock-blindness false-PROVEN class the guards exist to stop. Gate and invert have no such state, which is why they are safe first.
• 2^N only: a power-of-two maps onto a phase counter with a clean duty cycle; divide-by-3/5 does not ⇒ blackbox with an honest error.

Recognition — ONE shared recognizer, THREE entry points

All three must call the same function and each must be pinned by a test. If any one is missed, that design silently falls back to the refusal path and looks like a tool bug.

• inline RTL: clk & en / clk & latch(en);
• an instantiated cell whose body matches the pattern (minion’s prim_clk_gate) — recognized at the Sub boundary, with NO inlining, so formal.lec.trust is respected rather than fought;
• a DECLARED blackbox — an attribute naming the clk/en/out pins of a bodyless foundry ICG. Not optional: minion/verilog/prim_clk_gate.sv says “ASIC: swap this for the foundry ICG cell”, and without a declaration every ASIC configuration silently loses formal on every gated flop — the same 30-refusal hole in a different costume. The declaration must admit more than one enable pin, OR-combined: every real foundry ICG carries a test-enable (TE/SCE) beside the functional enable, and minion’s own behavioral gate has one (below).

The enable is a CONE, not a wire — measured on the real gate. prim_clk_gate.sv latches en_i | dft_i.scanmode (scan forces the clock ON), and dft_i is a packed struct that graph flows keep as one FLAT 5-bit bus (struct_port_bundles=false), so the compiled def’s latch din is or(en_i, and(sra(dft_i, k), 1)) behind tolg’s hold mux. The body match must accept ANY combinational cone of the non-clock input ports as the latched value, and bind the cell’s en to that cone re-rooted on the instance’s actual nets. Dropping the scanmode term is UNSOUND, not conservative — gate sites wire a live dft (minion_frontend_thread_buffer.sv:327, txfmafrac_top.sv:354) and minion_top exposes it as a primary input.

Clock identity inside the matched def is STRUCTURAL, never the port name. prim_clk_gate’s own graph holds no flop, so Design_clocks’ roots are empty there and only the name heuristic could identify clk_i — and the heuristic is being retired (Rules below). The anchor that replaces it: the port that is BOTH AND-ed into the output AND gates the latch’s transparency window is the clock; equivalently, at the Sub boundary, clockness flows TOP-DOWN from the instantiation (the net wired to the port is a clock in the parent). Both resolutions agree on every real ICG and neither reads a name.

Lowering — the cell is the REPRESENTATION; each consumer lowers its own view

• LEC + verify encode: resolve the clock through the cell to {clk, commits}. ONE helper serving BOTH the memory cut (pass/lec/encode.cpp ~:754) and the flop clock path (~:2400) — the memory half is unreachable any other way, because the M8 fold rewrites flop clocks into enables and never touches a Memory’s clock_pin. lhd formal verify gets the helper for free: both drivers instantiate the same Encoder.
• sim cgen: same recognizer → commit guard. This is lhdsuite fixme issue 12 — and the gap is NARROWER than that issue first recorded: cgen_sim.cpp already folds the inline <clock> & <enables> shape (M5, Cgen_sim::icg_guards ~:1075, with a fail-closed gated-clock-unsupported diagnostic for what the fold cannot see); only lhd_kernel_sim.cpp is truly clock-free. What icg_guards cannot see is a Sub-driven clock_pin — exactly what the recognizer resolves. The sim lowering’s HARD CASE is prim_rf_single_1r1w_par_preview: ONE gated clock consumed by a posedge flop, a NEGEDGE flop, and a transparent-low latch at once (instantiated with rf_clk_i = preview_clk_i = clkgt in minion_dcache_tensor_load; LEC dodges the def via lec_trust, sim compiles everything). A negedge consumer composes as invert-at-the-consumer: it commits at the reference FALL iff en as sampled at the rise that OPENED the pulse was high — the same {clk_ref, en} condition, opposite edge.
• synthesis: the cell SURVIVES to mapping as a real ICG cell, so the shared gate is preserved — the power half of the motivation, not just area, and the reason not to eager-fold. Until that lowering ships, pass/abc already fails closed BY NAME on an unknown comb op (unsupported-cell, abc_map.cpp ~:1537), so a Clock_cell reaching mapping early refuses rather than mismaps. semdiff digests a new op distinguishably with no work, and the Pyrope writer is unreachable from a graph op (no LGraph→LNAST decompiler) — which is also why GRAPH-level recognition cannot churn lhdsuite’s checked-in pyrope/ trees, where an LNAST-level recognizer would.

Canonicalization — required, or structural matching degrades

• double invert → the reference;
• gate of gate → AND the enables;
• div=1, invert=false with no en → identity, remove.
• Corpus note (measured): gate-of-gate occurs ONLY across Sub boundaries in minion (clock→cgate in vpu_lane, re-gated in txfmafrac_top) — never inside one def — so per-def recognition sees at most one gate level, and this canonicalization is pinned by a SYNTHETIC test, off minion’s acceptance path.

Rules — BINDING

• A Clock_cell output is legal ONLY on a clock sink: a state element’s clock_pin, a Latch’s gate (the RF-preview shape — a transparent-low latch gated by the gated clock), another cell’s clk_ref, or a Sub instance INPUT port (the gated clock crossing hierarchy; minion exercises all four). Reading it as DATA is an error (or forces the blackbox path). People do sample gated clocks in DFT and clock-monitor logic; without this rule the “it is an enable” model and the “it is a bit value” reading diverge silently. This is the dual of “nothing may be done with a clock”.
• Anything else on a clock (clock+1, an odd divider, arbitrary logic) ⇒ compile error naming the blackbox escape hatch.
• Stage that error: WARN first, measure with R4, then promote to an error. It is a breaking change and the allowed set is wider than “gating” — posedge ~clk is legitimate and lhd/tests/lec_clock_blindness_test.sh already pins it PROVEN equal to negedge clk.
• is_clock becomes STRUCTURAL: a net is a clock iff it is a declared clock input, a Clock_cell output, or a Sub input port fed by a clock in the parent — clockness propagates TOP-DOWN through the instance tree. This retires the name heuristic in Design_clocks::is_clock (“else a conventional spelling”, pinned by ClockNameHeuristicBoundaries). Caveat that gates the retirement: NO “declared clock input” mechanism exists yet — the slang reader’s only clock ID is itself a name match — so defining the declaration is part of the staged rollout, and until it lands the heuristic stays as the top-level seed only.
• WHERE recognition runs is part of the contract: inside the formal (lhd lec / formal verify) and sim pipelines ONLY, never on the compile/emission path — mirroring pass.single_edge’s placement and for the same reasons: single_edge_scope_test’s byte-identical-emission rule, the ABC incremental cache’s digest-keyed regions, and lhdsuite’s checked-in trees. Pin it 1h-style: compile emission byte-identical on an ICG design, recipe log never names the recognizer. Revisit only when the synthesis ICG lowering ships.
• The escape-hatch inventory is already known — name it, so the first refusal is a diagnosis, not a surprise. Two clock primitives sit in minion’s tree UNINSTANTIATED (absent from filelist.f, no sites): prim_clk_mux.sv, a 2:1 clock mux that dft_pkg.sv:16 names as the mechanism for the sram_clk_override DFT field every dft_t port already carries — blackbox path for now, a comptime-sel candidate later; and prim_clk_gate_n.sv, the active-low OR-form dual (clk_no = clk_i | ~en_latch, latch transparent while the clock is HIGH) — representable as invert∘gate∘invert once invert lands. The day either is wired, the failure must be a named “not implemented”, not a recognizer surprise. (prim_phase_pair_* was checked and stays OUT of scope: its latches are clock-AND-data gated and its outputs are consumed strictly as data — M8/latch_contract business.)

Implementation order — do NOT skip step 0

• (0) Close the silently-accepted gated-memory hole FIRST. memory_clock_shape_ok (pass/lec/encode.cpp) accepts any Sub on a memory clock_pin — the exemption was written for the ABC-mapped clock BUFFER cell, and an ICG Sub satisfies it by accident, so a gated memory encodes as “commits every step”, which the guard’s own comment calls “silently WRONG”. MEASURED on the compiled minion library: 21 memory clock_pin edges, all 21 driven by a Sub — intpipe_csr_file 7, vpu_trans 6, minion_dcache_tensor_load 3, _p1 3, minion_frontend_thread_buffer 1, _p1 1. Masked today only because those defs are UNKNOWN for other reasons — fix the flop side first and several become false PROVENs. Narrow the exemption to a buffer-shaped def, fail closed otherwise. Acceptance: minion_lec’s table stays byte-identical (110 proven / 32 trusted / 30 refusals), only the NAMED element changing in some defs — that identity is the receipt the hole was fully masked.
• (1) Guardrails first, then the cell, then the recognizer. (1a) Ntype_op slot — a combinational cell takes an EVEN slot per graph/cell.hpp’s bit-0 loop_last invariant, and 52 is free (between Nconst=50 and AttrSet=56, outside the pipelined block) — with the matching static_assert and the name-table entry in the SAME commit, so every diagnostic prints a real name. In that same commit, add named fail-closed default arms to cgen_verilog and cgen_sim: today cgen_verilog’s only unknown-op guard is I(!txt_op.empty()), which compiles out under NDEBUG (the -c opt default) and then emits a silent first-operand pass-through — for a Clock_cell that is clk_ref wired straight through, i.e. the gate silently DROPPED — and cgen_sim’s expression default does the same. Pin with a test that a hand-built Clock_cell graph is REFUSED BY NAME in both emitters. (1b) the shared recognizer (3 entry points) + canonicalization.
• (2) LEC + verify lowering — memory cut and flop path through one helper (the shared Encoder serves both drivers). After step 0’s narrowing, a Clock_cell on a memory clock_pin gets its own NAMED accept arm in memory_clock_shape_ok, not a ride through the generic comb refusal.
• (3) sim cgen lowering (closes fixme issue 12; the hard case is prim_rf_single_1r1w_par_preview — see Lowering).
• (4) Only then shrink CORES.lec_trust in ../lhdsuite/bench/defs.bzl.

Acceptance — what must move

• //bench:minion_lec: 30 encode refusals → 0; proven 110/140 → higher; prim_clk_gate leaves lec_trust (32 → 31).
• minion METRIC sim_cpu_top_ok: 0 → 1, then flip CORES.sim_top_assert for minion.
• lhd formal verify moves with it for free (shared encoder): prp-verify-latch_icg_hier (3 obligations) stays green through the switch from inline+fold to recognition, and gains a Sub-boundary / declared-blackbox twin.
• Unchanged: dino 14/14; livehd //... green; lec_clock_blindness_test must STILL refute gated-vs-ungated, two-clock-vs-one, and negedge-vs-posedge.

Traps — measured, do not re-derive

• Enable-latch bypass: use the value the latch is passing THROUGH at the sampling edge, never its held Q. The L1 error, invisible to a symmetric before/after comparison — which is why the ICG fixture validates against Icarus.
• Polarity: for gclk = clk & g the commit condition is enable & g — NOT & !g. Also invisible to a symmetric check.
• Do NOT eager-fold into enables as the representation. It destroys the shared ICG (power/area at synthesis), changes the netlist ABC sees, invalidates incremental-synth cache regions, and collides with single_edge_scope_test’s byte-identical-emission requirement. Represent as a node; lower per consumer.
• Inlining a TRUSTED def to expose its gate is not the answer: it pulls internals the user declared out of scope into the compared cone. Pinned by single_edge_hier_latch_test.sh case 5b — trusting a clock gate may return UNKNOWN, never a REFUTATION. Recognition at the Sub boundary avoids this entirely.

Measured on real designs — lhdsuite dino + minion (2026-07-25)

Run with cd ../lhdsuite && bazel test //bench:<core>_lec* --override_module=livehd=../livehd (opt build; minion_lec ~200 s).

NO REGRESSION — which was the real risk, since the new fail-closed guard for unmodelled clocks could easily have refused an industrial core full of gated clocks. It did not, because minion's ICGs sit in defs the suite already trusts.

But minion also found two shapes the in-graph work had missed, and both are now fixed (see Clock gating): real designs INSTANTIATE the gate (32 prim_clk_gate instances — exactly the lec_trust list), and prim_phase_pair gates a latch on !clk && lo_en, a clock ANDed with a data enable.

The one thing blocking minion's trust list is HIERARCHY. Measured directly: minion_lec with an EMPTY trust list refuses with def `prim_rf_1r1w_preview_p2` holds 1 latch cell(s), 1 negedge flop(s), and normalizing across a module boundary is not supported yet. At that measurement 32 names were configured; Clock_cell recognition later made prim_clk_gate inert, leaving 31 effective trusted definitions. Those 31 are not a workaround for the encoder's old Latch refusal (that is gone): their remaining blocker is hierarchy. What will close it: M10 schedules instantiated state directly in the formal encoder. It does not normalize definitions, synthesize a phase counter, or port-thread timing state through hierarchy. Tracker: lhd/tests/single_edge_hier_latch_test.sh continues to pin today's honest refusal until the formal pipeline stops depending on that pass.

M10 — hierarchy-aware formal phase scheduler PENDING

No coloring and no graph rewrite. Starting at the selected top, the formal driver resolves clocks through the actual instance bindings and assigns a semantic phase to every instantiated register/latch and every synchronous memory port. For each endpoint it walks data, enable, reset, address and write-data cones backward across non-opaque hierarchy, stopping at constants, primary inputs, state, and opaque boxes. Gates are memoized inside one phase; a gate feeding two phases is deliberately encoded twice.

Single-root v1 schedule

1. active-LOW clock-role latches close immediately before rise;
2. posedge flops, posedge memory ports and data-gated latches update simultaneously;
3. active-HIGH clock-role latches close immediately before fall;
4. negedge flops and negedge memory ports update simultaneously.

A same-batch state read sees the incoming value; a later batch in the same period sees the earlier committed value. The latch-close microstep and its edge batch share one symbolic input snapshot, while rise and fall get independent snapshots shared between REF and IMPL. LEC observes external outputs after rise and after fall. An unclocked formal assertion is evaluated at the full-period boundary by default.

Data-role is not clock-role. A data-gated latch has Pyrope's ordinary tick semantics and joins the rise/base batch; active-low polarity changes its write test, not its phase. Only a latch whose controlling cone resolves to the root clock gets close-before-edge treatment. This is the live latch_mixed_flop behavior and corrects the old “data gate → last slot” planning text.

Clock_cell remains timing metadata, never an SMT data value or scheduled endpoint. Canonicalize a chain to its reference clock, parity and active-high guard. Sample the guard before the reference rise, reuse it for the affected rise/fall consumers, and combine it as endpoint_enable & clock_guard. Inversion changes the consumer edge; div != 1 remains a named refusal.

Memories are scheduled per synchronous port. The Memory IR must retain read and write edge polarity per port (with a compatibility fallback for the current global value); the Yosys import must stop dropping RD_CLK_POLARITY. Each phase applies only its ports, while writes in the same phase retain the existing simultaneous forwarding/collision policy. This formal correction does not close the separate 2m-multiport_mem Verilog-codegen issue.

Hierarchy composes through phase-aware state boxes. Replace the current one-transition-per-period State_box with shared transition and Moore-output contracts per semantic phase. A child collapses only after those intermediate contracts prove; otherwise it stays expanded. Each instance resolves the child's phases through its own parent clock binding and sampled Clock_cell guard. A body-less trusted blackbox is conservatively allowed to transition on both edges of each declared clock.

Scope and failure policy. v1 orders one root clock. An unrelated-root, flop-only design retains the encoder's existing detected-edge path. If a latch, phase-sensitive memory, or phase box would require a total order between unrelated roots, formal fails closed. Fluid flops, unresolved latch clock/data classification, and clock division also remain named refusals.

Delivery and gates

1. read-only schedule analysis plus deterministic per-phase diagnostics;
2. flop/latch phase encoding with edge-specific inputs and output compares;
3. per-port memory scheduling, including registered reads;
4. phase-aware sequential boxes and hierarchical collapse;
5. remove mandatory pass.single_edge preprocessing from LEC and verify;
6. measure minion and remove trust entries only for definitions that prove.

Acceptance covers posedge→negedge pipelines, both clock-latch polarities, the simultaneous data-latch/flop case, one Clock_cell feeding both phases with one rise-sampled guard, hierarchical rise-to-fall communication, mixed-edge memory ports, resets, and the unrelated-clock fallback. Bounds and reset counts remain source periods; cache keys include the schedule signature; witnesses name (cycle,rise|fall) and replay refuses explicitly until it can reproduce edge-specific stimulus.

Scope ruling (user, 2026-07-20) — BINDING: SIMPLE LATCHES, NO TIME BORROWING

Time borrowing is a backend / physical-design technique. LiveHD's scope ends at the ABC call, and ABC's output netlist has no clock borrowing either. This ruling collapses the expensive half of the problem. Under it a latch is exactly a flop-with-enable that commits at the CLOSING edge of its transparent window:

• transparent-HIGH latch (transparent while gate == 1) → commits at the FALL of its gate
• transparent-LOW latch (transparent while gate == 0) → commits at the RISE of its gate

That is Conformal's set flatten model -latch_fold / the IBM LEC normalization (US7624363). It is an ABSTRACTION WITH A PRECONDITION, not a semantics — and the scope ruling is that precondition, so it must be CHECKED, never assumed (M3 does, in graph/latch_contract.cpp). What it buys: no transparency mux in the sim scheduler, no settle/fixpoint loop, no MDL phase abstraction, no counterexample lifting — nothing research-grade on the critical path.

The abstraction changes OBSERVABILITY, and that must be stated: while a window is OPEN a real latch reads through (Q follows D combinationally) but the commit-class model shows the previous commit. The two agree exactly at closed-window, end-of-cycle observations. Three consequences run through everything below: (1) any latch encoding in LEC is sound only as a both-sides normalization — never encode one side with transparency and the other without; (2) sim asserts and differential oracles may observe a latch Q only under the observation-visibility rule; (3) the shared observation point for sim / BMC / Icarus is end-of-cycle, all edges settled — pinned executable by inou/prp/tests/fixme/flop_verify_posneg.prp (under the alternative "between rise and fall" convention that fixture's correct answer would be indistinguishable from today's clock-blind encoding).

The abstraction is for SIM and LEC ONLY. Verilog emission must still emit a real always_latch — the netlist handed to ABC has to contain a real latch. Terminology trap: an AIGER/ABC "latch" is an edge-triggered unit-delay register on an implicit global clock, NOT a level-sensitive latch; ABC's BLIF reader silently discards the .latch control tokens, so a real latch reaching ABC is a silent mismodel, not an error. Everything on this page means level-sensitive.

Rules — BINDING

Cross-model gating is mandatory. "PROVEN before AND after the transformation" cannot see a transformation that is WRONG but applied identically to both sides — two identically-wrong machines prove equal, so a symmetric gate is vacuous by construction. Every latch/clock transformation must be gated against an INDEPENDENT checker: lgyosys for latch polarity, iverilog for anything clock/edge-shaped, never our own encoder on both sides. This one mechanism catches mux placement, posclk double-negation, a flavour-blind ICG fold, and an unstable phase gate.

There is NO in-repo formal oracle for flop EDGES. lgcheck's cascade ends in a bounded miter (LGCHECK_BMC_STEPS default 5, inou/yosys/lgcheck:399) that decides latch designs and genuinely discriminates enable polarity — pinned by lhd/tests/lec_latch_polarity_test.sh. But it is exactly as edge- and gate-blind for flops as our own encoder was (reproduced: PROVEN on negedge-vs-posedge and gated-vs-ungated). So an equiv pair of mixed-edge designs "proving" via lgcheck is vacuous with respect to the edges; only event-driven simulation discriminates them.

Verdict discipline (inherited from 2f-lec): PASS ⇒ definitively equivalent; FAIL ⇒ definitively different; anything else is inconclusive. An abstraction may only cause extra work, never a wrong verdict. Trackers that demand a refutation must grep a verbatim REFUTED — an encoder that merely degrades a false-PROVEN to UNKNOWN has not fixed the bug.

Observation-visibility rule (used by every sim/BMC fixture): an observation of a latch Q — a settled-region assert, a differential-oracle sample, or a sequential element in Q's fanin cone at its firing boundary — is valid iff (a) the latch was OPAQUE in the tick immediately preceding the observation, (b) at least one closing edge has completed since power-on, and (c) the data was STABLE across the closing edge being observed. Under (a)-(c) the real-transparency semantics (Icarus), the commit-at-closing-edge model, and a flop-with-enable encoding all agree, so fixtures pin the RULING, not an implementation choice. Divergence is not confined to transparent ticks — it PERSISTS through any state element that sampled a latch while open (taint).

Traps and ruled-out approaches — do not re-derive

• posclk on a Latch is the ENABLE POLARITY, not a clock (user ruling 2026-07-20, graph/cell.cpp:266-288). unset/true ⇒ active HIGH, commits on the net's FALL; known-false ⇒ active LOW, commits on its RISE. The name is inherited from Flop and is a poor fit, but find_sink_pin() resolves an unknown pin name to invalid silently, so a rename that missed one consumer would drop the polarity without a word. Pyrope may spell it enable_high.
• enable_high=false is REFUSED from Pyrope — a bare polarity-pin flip is a measured SILENT MISCOMPILE. tolg lowers if cond { l = d } to BOTH din = cond ? d : q AND enable = cond, so the enable is active-HIGH by construction; flipping only the pin emits if (!cond) q <= (cond ? d : q), so while transparent the latch writes ITSELF forever and never captures d. The polarity still lives on the CELL for the yosys importer, whose raw-D + EN shape has no hold mux and for which the flip IS sound. Two shapes, and any latch consumer must handle both.
• Do NOT change the Ntype_op encoding. is_loop_break() reads bit 0 of the type word; graph/cell.hpp:113 static_asserts Latch = 45 odd. Flipping it ripples into abc/lec/semdiff/color/isabelle/lean.
• Any new Query_result/Verify_result field must be added to the fork-race wire codec. lhd lec and lhd formal verify run their ind|bmc portfolio in a FORKED race through a hand-rolled codec; a field missing there is SILENTLY LOST and the parent reports a clean exit-0. This already bit M0 once (fixed for Query_result at query.cpp:347) and is still live for Verify_result — see step 0a.
• Folding the commit class into the state key is PROVABLY INSUFFICIENT. Implemented and measured pre-M4: the keys really did diverge (k:iclock+ vs k:and(get_mask(…) and gated-vs-ungated still returned PROVEN. Keying only decides which state symbols CORRESPOND; it puts nothing about the clock into the transition function. Necessary for correspondence, never sufficient to refute a clocking difference.
• The dynamic edge model was REVERTED — do not retry it as-is. Encoding the clock as an ordinary signal with a previous-level bit and gating on a real edge made all three reproducers REFUTE, then broke ~40 existing tests with FALSE REFUTEDs. Root cause: the BMC reset prologue assumes ONE STEP = ONE COMMIT, so a prologue step where the clock does not toggle commits nothing and a SYNC reset never lands. M8 sidesteps this entirely by keeping one free-running clock and a statically scheduled phase counter.
  Two things worth keeping if it is ever retried: the previous-level element must be SHARED by both miter sides, keyed by FRAME (drop a leading r/i from the caller's prefix); and the "~half the cycles at the same formal.bound" cost belongs to this reverted model, not to M8.
• The state-pairing diagnosis in the old M4 was WRONG. It read "the work is in the state-pairing layer … not in the encoder". Measured cause: a Latch never reaches shared_inputs at all — the seed loop encode.cpp:610-612 and all eight state collections in query.cpp (:2713, 2883, 2924, 3060, 3836, 3914, 5543, 5642) are != Ntype_op::Flop → continue, so encode.cpp:605-607 mints a per-side free constant. That is the q(ref=254 impl=255) step-1 CEX. The tier-2 confirm step (query.cpp:1801-1818) runs only after a paired solve already refuted and can never break a working pairing. M8 dissolves this rather than fixing it.
• NEW (M8) — a CLOCK-gated latch's gate must be ABSORBED by the slot, never AND-ed with it. After normalization ONE CLOCK TICK IS ONE SUB-STEP, so any combinational cone that reads the clock as data — which is exactly what a latch gate is — gets evaluated P times per source period. The enable becomes clk & (phase == slot) and only commits when the free clock input happens to be high at the slot step. Measured with iverilog: the latch outputs stay x forever. The fix is that the enable becomes the slot predicate ALONE and din becomes the TRANSPARENT arm of tolg's hold mux. A DATA gate must be left completely alone — collapsing the two cases is what blinds the transparent-low polarity canary.
• NEW (M8) — rule 4 must key on the COMMIT CLASS, not the slot. Two elements can share a slot without sharing an edge: a data-gated latch defaults to slot 0 alongside the posedge flops, and that pairing IS the ordinary flop-with-enable abstraction the task is scoped to. Keyed on the slot, rule 4 immediately rejected latch_mixed_flop, a live fixture.
• NEW (M8) — the period boundary is phase == 0, not phase == P-1. A step READS state and COMMITS at its end, so the state visible at the phase-k step is what committed through slot k−1. The period is fully settled at the phase-0 step that STARTS the next period. Off by one sub-step, the guard checks mid-period and an equivalent design refutes.
• NEW (M8) — a SYNC reset must move INSIDE the slot gate, and its initial pin must go with it. The encoder nests reset outside the commit for every flop (async for all), which is harmless only while one step is one commit. Folding it into the data path needs THREE things together: din := rst ? initial : din, enable |= rst (reset still wins over the enable, as Verilog says), and drop initial — keeping it leaves a concrete power-on value the other miter side does not have, the state pairing reports "kind/init mismatch", and the unpaired reset-less flop gets a FREE per-side constant, i.e. the q(ref=254 impl=255) step-1 CEX all over again.
• NEW (M8) — the trigger must SKIP what the pass does not OWE. The plan's trigger includes "≥2 clock input nets", and refusing on it immediately degraded lec_clock_blindness_test's CORRECT two-clock-vs-one-clock REFUTED into an unsupported exit. The pass owes a lowering only for what the engines get WRONG (a Latch the encoder refuses; a negedge edge it is blind to). A second clock domain that ALSO holds a latch cannot be skipped and must fail closed by name.
• NEW (M8) — the yosys reader's register NAMES are not stable across two variants of the same design ($procdff$32 vs $procdff$34, n12 vs n13). Any LEC fixture that needs state CORRESPONDENCE has to come from Pyrope, or every verdict is a per-side free-constant CEX that looks like a real inequivalence. This is what made the first cut of the four-class fixture unusable.
• NEW (M8) — a computed single-fanout flop enable was emitted UNDECLARED by cgen_verilog (get_wire_or_const ignores pin2expr). The same bug M1 fixed for the latch's din/enable and for clock_pin, previously unreachable because every emitter gave a flop enable fanout ≥2. iverilog refuses to elaborate it; yosys silently invents an implicit wire reading X, which is worse. Any pass that synthesizes a control pin with exactly one consumer will hit this class again.
• NEW (M8) — lhd sim cannot take a yosys-read design with a Pyrope test block ("cannot mix pyrope and verilog sources"; via lg: the test block cannot resolve the module name). So the sim oracle is scoped to tolg-emittable shapes, and any cgen_sim fix for a yosys-only cell shape (an active-low $dlatch) is unreachable-today code — the same status as M7's importer guards.
• A Latch inside a resolution-library def is not covered by fixing the top graph. encode.cpp:926-931 screens defs separately and sends a stateful one to the blackbox path (def = nullptr).

M8 — edge normalization LANDED; FORMAL WORKAROUND

One LGraph→LGraph pass — pass.single_edge (name open) — that removes latches and negedge state, and is conditional: it does not run at all unless the design has them. Scope, settled by the user 2026-07-24: verification and simulation only, never on the synthesis path (slot enables and a divider cost QoR) — but it must stand as a genuinely semantics-preserving transformation, not a formal-only hack.

Trigger. Scan for any Latch cell, any Flop with posclk known-false, or ≥2 clock input nets. None present ⇒ the pass is skipped entirely — not run-as-a-no-op. A plain posedge single-clock design never enters this code path, is never re-emitted, and cannot change verdict. That is the whole blast-radius argument, and it is why this can land without re-baselining the corpus.

When the trigger fires, every state element becomes a plain Flop on a single posedge clock, with the original timing carried by a synthesized phase counter (a divider off the design's own clock) plus per-flop slot enables. Commit-class → slot is a table, not an analysis — and the table is the output of M3's landed commit_class_of():

Why it closes both holes

negedge vs posedge. The blocker is that both flops commit exactly once per step and differ only in WHERE in the step — which a step-granular relational encoding cannot express. Slotting converts an intra-step ordering problem into a cross-step one: at slot 1 the negedge flop's din reads a Q that already committed at slot 0. Ordinary, and the existing Flop encoding handles it unchanged.

Latches — dissolved, not fixed. Emit Flop cells only and the free-per-side-constant problem in Traps cannot arise. Verified 2026-07-24: latch_hold_basic hand-lowered to a flop-with-enable, keeping the same l↔q rename that breaks the real pair, comes back PROVEN — the existing tier-2 pairing plus the inductive self-certifying relation handle it with no new machinery.

The deferred clock-waveform model is mostly subsumed. The reverted attempt was hard because commits were gated on a free, data-dependent clock. Here the schedule is static: at unroll step j you know exactly which slot commits, so the prologue reduces to "reset_cycles = N means N·P steps". Only sub-item (a) of the old deferred pair survives — sync-vs-async reset placement, carried into step 5.

Cost — it is not 2×

P slots multiply BMC depth, but not work, on one condition: initialize the phase counter concretely. Then at unroll step j the solver knows phase == j mod P statically, every slot predicate const-folds, and step j encodes only slot-k's commits plus their cones. Summed over P steps that is ≈ one fat two-phase step. (Risk: under phase=after_reset the encoder deliberately discards flop initial values at query.cpp:2942-2951 — see Risks 2.)

Two cheap wins: the pass never runs on a clean design, so P>1 is paid only by designs that genuinely mix edges or hold latches; and the opposite-phase peephole — a master/slave latch pair is a posedge flop — can retire the mixed structures outright so the trigger goes quiet and P returns to 1.

NOT needed, dropped after reading the code: "make induction period-aware (k mod P)". There is no k: verify's V3 rung is hard-coded to two frames (query.cpp:6605) and lec's ind engine is a single-step flop-cut miter (:3828-3831), not an unroll. With step 3's guard the property is 1-inductive with zero solver change. Plumbing P through Lec_options and the fork-race codecs goes with it.

Conditions that must hold

1. The trigger must be evaluated over the MITER, not per side. If one side holds a latch and the other is its already-lowered round-trip, the pass fires on one side only and the two are compared in different time bases — a guaranteed false REFUTED, and exactly the shape of the prp-v2prp2v-latch_* corpus. If either side needs normalization, both are normalized.
2. Slot assignment derived structurally from the commit class — never from node or traversal order. In LEC the pass must run inside the pipeline on both sides with identical options, never as a manual pre-step.
3. Obligations and miter comparisons gated to the period boundary (phase == P-1), or mid-period states are compared and equivalent designs refute.
4. Latch classification must survive the lowering. Gate-driven-by-clock → slot from polarity; gate-driven-by-data (the latch_verify_hold shape, en = (c==0) or (c==4)) → ordinary flop-with-enable in the domain's last slot. Collapse those two classes and latch_verify_low's polarity canary goes blind.
5. Coincident commit edges must share ONE slot — a soundness precondition. Slotting does not fix M3's rule 4 (coincident-edge latch → buffer, the US7624363 L1 case); it reproduces it. A transparent-low latch on clk commits on the RISE, and a posedge flop on clk also commits on the RISE — put them in different slots and the flop reads the latch's previous commit, a persistent full-cycle error. So equal (net, edge) ⇒ equal slot, and the L1→buffer rewrite (or an explicit rejection) lands before the lowering. This is not the opposite-phase peephole: that collapses a master/slave PAIR into one flop and is optional; this turns a SINGLE latch into a buffer and is mandatory.
6. Known integer ratios only. A genuinely free second clock — a clock port the testbench drives as data, which M6 models in sim and encode.cpp:2245-2269 models in LEC — has no ratio and must be DECLINED, not slotted.
7. Witness / VCD must map back. lecfail replay, formal_report.json cycle indices and VCD timestamps all count sub-steps after normalization and must be reported in periods.

How the transformation itself is validated

The transformation is not cycle-preserving (one source cycle becomes P steps), so no cycle-accurate equivalence checker can validate it — neither lhd lec nor lgcheck. Validation is trace-level against an independent model:

• Differential simulation with period-boundary sampling, source vs normalized. prp-simeq cannot be the vehicle (measured): a normalized graph only exists as lg:, and lhd compile lg:DIR --emit-dir pyrope: exits 7 ("no LGraph → LNAST decompiler") while lhd sim lg:DIR exits 2. What works is --emit-dir sim: and --emit-dir verilog: (both rc 0). Build a new harness by reusing inou/prp/tests/equiv_sim_fail_test.py (already a two-DUT --emit-dir sim: differential harness) and inou/cgen/tests/sim/diff_test.py (the verilog+iverilog leg).
• iverilog is the primary leg for anything edge-shaped — source-sim vs normalized-sim is our own model on both sides, which the gating rule forbids.
• WHAT ACTUALLY LANDED (2026-07-24), which is simpler than the plan above. No new Python harness was needed: --emit-dir verilog: works on BOTH the source and the normalized graph, so the two are instantiated in ONE iverilog testbench and compared directly — see lhd/tests/single_edge_four_classes_test.sh. The normalized side is clocked P× per source period; stimulus changes at a point that keeps it stable across every sampling edge of the period on both sides (otherwise the two legitimately sample different inputs and the comparison means nothing); and each latch Q is read only in the half-period where THAT latch is opaque. The two complementary latches make it impossible to observe both at one instant, which is exactly why the visibility rule exists rather than "sample at the end". Getting the normalized graph to elaborate at all required the two cgen fixes recorded in the status table.
• lgcheck stays on the SOURCE side for latch polarity. A normalized graph's divergence depth multiplies by P, so a 5-step bounded miter would pass vacuously.
• Corollary — do NOT migrate lhd sim to the normalized graph early. Keeping sim on the source graph (M5's two-phase tick, already iverilog-validated) is what makes it an independent oracle. Migrating later is attractive as a simplification — it deletes cgen_sim.cpp:2675-2790 and both fail-closed paths (negedge-through-instance, negedge-operand-unresolved) — but doing it early costs the oracle.

Implementation steps

STATUS 2026-07-24 — the tables below are the LANDED record. The step text is kept verbatim (its file:line references are still the map), with the outcome of each step here. Sizes S/M/L were relative estimates.

Sizes S/M/L are relative. Every "GATE" is the observable test that proves the step done. The step text below was written 2026-07-24 against the pre-M8 tree.

(0) Independent — start now, no deps

(1) The pass

(2) Solver-side

Explicitly NOT subtasks — keep these as invariants. The ICG fold encode.cpp:2318-2356 stays: an ICG design has one clock input, all-posedge flops and no latch, so it never fires the trigger and is never normalized — delete the fold and gated-vs-ungated goes back to falsely PROVEN. The multi-clock edge branch :2245-2269 stays for the free/aperiodic clock. The eight Flop-only collections in query.cpp need no edit — they become correct by construction, which is a dependency of the pass (hence 1e's fail-closed), not work. pass/abc and cgen_verilog stay untouched on the source graph.

(3) Tests

Critical path and parallelism

0b (Commit_class role) → 0c (trigger) → 1a (skeleton+BUILD)
   → 1b (rule 4)  ─┬→ 1c (Latch→Flop retype, P=1) ───────────┐
                   └→ 1d (assert guard) → 1e (divider, P=2) ─┤
                                                             ↓
                            1g (inject into verify_command)
                                                             ↓
        latch_verify_hold ✅   latch_verify_low ✅   flop_verify_posneg ✅

• The three fixtures run through formal verify, not lhd lec — the lec_command half of 1g is not on this path; it belongs to 3c/3f.
• The two latch fixtures need only P=1 — no divider, no slot enables, no solver change. 0b → 0c → 1a → 1b → 1c → 1g is the cheapest first green and it validates the whole vehicle.
• flop_verify_posneg needs 1d before 1e, or it REFUTES at slot 1 no matter how correct the rewrite is.
• Parallel from day one: 0a, 0d, 3a, 2b, all doc hygiene, and building 3b's harness against the hand-lowered graph before any pass exists.

Risks — cheapest experiment that settles each

1. Does the phase counter actually const-fold? The whole cost argument depends on it, and under phase=after_reset the encoder deliberately discards flop initial values (query.cpp:2942-2951, verify twin :5665-5669). A free phase does not just cost speed — 1d's guard would then check at an arbitrary offset, i.e. silently vacuous. Experiment: encode flop_verify_posneg normalized and assert via an explicit solver query that phase == j mod P at every checked j, on a design with no reset input. If free, a documented keep-init exception for the normalizer-owned key is required.
2. Does lhd sim survive as the oracle at all? Measured on latch_hold_basic from the same lg:: iverilog gives cyc1 q=11, lhd sim gives cyc1 q=0. They agree only at closed ticks — cgen_sim models a latch as an end-of-cycle flop-with-enable while always_latch is truly transparent. Experiment: run 3b's iverilog leg on the un-normalized latch fixtures with visibility-rule sampling. If it cannot be made green there, Validation needs re-scoping before any normalized comparison means anything.
3. Primary inputs are minted fresh per sub-step (query.cpp:3233, :5970), so at P=2 each source cycle gets two independent input values — a strict superset of source behaviour. Sound for proofs, but it yields CEXes with no source counterpart and weakens env assumes. Experiment: normalize by hand, add a hold-across-period assumption, diff the CEX set.
4. Gate the LEC miter compare, or not? Condition 3 says gate; the counter-argument is that with identically-normalized sides mid-period equality already holds, so gating monotonically removes compare points and opens a false-PROVEN surface. Experiment: hand-lower latch_hold_basic two ways (data-gated slot vs clock-gated slot) and LEC them ungated. REFUTES ⇒ gating mandatory; PROVES ⇒ skip it.
5. Reset placement per slot — the one deferred item NOT subsumed. encode.cpp:2282-2289 nests reset outside commits unconditionally, i.e. async for every flop. Harmless for a primary reset held through the prologue; wrong for a design-computed soft reset, which then clears at a slot it does not own. M7's landed ruling answers the latch half: a latch's reset is inherently ASYNCHRONOUS, so a lowered latch's reset goes OUTSIDE the slot gate. Experiment: a negedge flop cleared by a non-primary soft reset, PROVEN against its normalized form and REFUTED against a one-slot-early variant, with iverilog agreeing.
6. Hierarchy: port-thread the phase counter, or one divider per def? Unresolved. All three gate fixtures are flat, so fail closed on Sub for now. Experiment: latch_icg has an instance — try both.
7. Naming stability of the synthesized phase register. It must survive canon_flop_name (encode.cpp:52-77) identically on both sides so it lands in shared_inputs instead of the per-side fallback. Never derive it from a NID. Experiment: LEC_DUMP_FLOPS lists the phase key once per side with identical spelling; rename it on one side and confirm the miter REFUTES.

M4 residue

Two of the three clock-blindness holes CLOSED 2026-07-20 (d572ad005), and that code ships — do not touch it:

• ICG cone <clock-input> & <enables> folds to "commit iff the enables are true" — no edge detection, no prologue interaction. gated vs ungated REFUTES. TRAP: both operands of clk & en are graph inputs, so "is it an input?" cannot tell the clock from the enable; match by NAME against the nets the design already uses as clocks, falling back to the conventional spellings.
• Two or more clock INPUT nets — each flop commits on a detected edge of its own net, with the previous level SHARED per FRAME. two-clock vs one-clock REFUTES.

Gating is applied only where "one step = one commit" is already false. A plain flop whose clock_pin resolves straight to a clock input gets NO gating term and encodes byte-for-byte as before — note the ICG branch DOES fire in a design with just one clock input, via the name fallback. lec_clock_blindness_test.sh is live.

The third hole is CLOSED (2026-07-24, M8). negedge vs posedge on one clock now REFUTES, and lec_clock_blindness_test.sh case 3 is an assertion rather than a note. It was NOT closed by teaching the encoder about edges — that is provably impossible at step granularity — but by slotting, which turns the intra-step ordering difference into an ordinary cross-step one. The retired approaches (two-phase encoding of each BMC step; a tier-1 auto-promotion hook for latch pairs) stay recorded under Traps so they are not re-derived.

M4's own residue — sync-vs-async reset placement — is also CLOSED, and it turned out to be load-bearing rather than a footnote: flop_reset_matrix FALSE-REFUTED against its own round-trip at P=2 until the pass started folding a SYNC reset into the data path (inside the slot gate) and leaving only an ASYNC one on reset_pin. See step 1e.

Gate (met): all three false-PROVEN reproducers return verbatim REFUTED with a vacuity guard beside each; the three BMC twins are green and each mutates to a REFUTED; latch work is gated against lgyosys (lec_latch_polarity_test.sh) and edge work against iverilog (single_edge_four_classes_test.sh, 39 periods plus two negative controls); the no-op proof (3a) holds. The minion trigger scan is the one gate item NOT run — the pass is conditional and skips a design with no latch, no negedge state and one clock net, so the scan is what decides whether a re-baseline is even needed. Run lhd pass single_edge --top <top> lg:<minion> and check for single-edge-applied.

Landed (M0–M8)

Compressed record. The rulings and traps these produced are in Scope, Rules and Traps — this section is provenance only.

• M0 — fail closed, tell the truth LANDED (cce180aa8). Encoded/Query_result/Verify_result gain an unsupported flag separating a structural REFUSAL from a budget-out, hard-failed in both CLI paths regardless of formal.strict (exit 7, class unsupported). Latch scan in sim before the schedule walk replaces a phantom combinational-loop; gated-clock and multi-clock sim refusals; tolg ERRORS on dropped latch attrs; the reg-in-comb check extended to uninitialized regs. Gate met: lhd/tests/latch_fail_closed_test.sh. Still open from M0: the Verify_result half of the fork-race codec — step 0a.
• M1 — Verilog emission + round-trip LANDED. process_latch uses get_expression; emission is always_latch + <= so output round-trips through our own slang reader; create_locals uses is_type_register. Corrected recon claim: the undeclared-identifier bug is unreachable from Pyrope or slang — tolg's hold mux gives the enable fanout ≥2 — so any test for it MUST drive --reader yosys-verilog. Gate met: latch_verilog_emission_test.sh.
• M2 — the Latch cell gets a full pin set LANDED (c12b97bb8). All five reserved pins added at Flop-IDENTICAL pin ids (async 0, initial 1, clock_pin 2, negreset 5, reset_pin 7), so every consumer that resolves a flop's control pins by name resolves a latch's the same way. Consumer touches landed: abc boundary + blast exclusion, bitwidth dispatch, partition is_type_register, semdiff commit-class fold. Produced the enable-polarity ruling and the enable_high=false refusal — both in Traps. Gate: met except "LEC-PROVEN vs pre-abc", which needs M8.
• M3 — shared commit-class classifier + contract check LANDED as graph/latch_contract.{hpp,cpp}. commit_class_of() resolves an enable/clock cone back to a ROOT NET plus a parity, walking the shapes tolg emits for a boolean control (Mux(s,0,1), EQ(x,0)/EQ(x,1), Not, Get_mask/Sext) — which is what makes if clk and if !clk land on the same net at opposite parity, so a master/slave pair is recognizable. check() enforces rules A (self-gated enable), B (Q→own D) and C (simultaneously-transparent pair). Rule 3 was dissolved by the M2 ruling. Rule 4 (coincident-edge L1→buffer) is NOT implemented, and M8 makes it a precondition — see condition 5. Correction: the claim that this is "the same call M4 and M5 use" is aspirational — see step 0e.
• M5 — simulation LANDED (4af917e6e, hardened by 17b29f574). All 5 trackers green and promoted to inou/prp/tests/sim/. Latches needed no scheduler machinery — a Latch joins the flops vector and the ordinary flop update is transparency observed at end-of-tick. The two-phase tick (cgen_sim.cpp:2474-2790) commits posedge state at the rise, then drops the pin2var bindings reachable from a posedge Q and re-emits that cone so negedge state observes post-rise values. A Sub in that cone is REFUSED (re-running it would double-advance the child); a phase-2 operand that cannot be re-readied is also refused.
• M6 — multiple clocks (design side) LANDED. A flop whose clock_pin resolves to a graph input that is NOT the reference clock commits on a DETECTED EDGE of its own net, tracked by one shared previous-level bit per net. Coincident edges come out right by construction — every secondary commit reads PRE-TICK state, pinned by sim/multiclock_two_domain.prp (qb == 28, not 45). Relation to M8: complementary, not conflicting. KNOWN integer ratio ⇒ M8 slots; FREE / testbench-driven clock ⇒ M6's detected-edge model and encode.cpp:2245-2269 survive. Crossover constraint: coincident edges must share ONE slot, never adjacent ones. Deliberately not built: a second clock waveform in the VCD (cosmetic).
• M7 — async/SR latches importer half LANDED. $dlatchsr and $adlatch are now hard errors instead of silent drops; both guards are provably UNREACHABLE today because the yosys script lowers those shapes into a plain $dlatch first — inou/yosys/tests/latch_async.v and latch_sr.v pin both that the fold is LOSSLESS and that the situation has not changed. Latch reset semantics LANDED: a latch's reset is inherently ASYNCHRONOUS, emitted as the FIRST branch ahead of the transparency test. Sim needed no change. Efficiency (b) landed (-O2 host compile, measured free); (a) — killing the step()+peek() double cycle() — is a sub-instance-semantics change, not a reordering, left deliberately.
  Item (e) STRUCK as subsumed: teaching pass/formal's BMC the commit-class latch model is moot on a normalized graph — prove.cpp:87/:175 never fire when there is no Latch cell.

Tests (inventory re-verified 2026-07-24, post-M8)

NEW at M8 — the three that carry the whole argument:

• lhd/tests/single_edge_four_classes_test.sh — the independent-oracle gate. All four commit classes in one module, then (a) lhd lec must REFUTE each of three collapses and PROVE a semantically-identical rewrite, and (b) the SOURCE netlist (real always_latch, real negedge) and the NORMALIZED one run side by side under iverilog for 39 periods, the normalized side clocked P× and sampled per the visibility rule. TWO negative controls: clocking the normalized side at 1× must FAIL, and swapping the two slot predicates must FAIL. Skips the iverilog leg with a loud note when iverilog is absent (a host tool, not a bazel dep).
• lhd/tests/single_edge_scope_test.sh — the blast-radius gate. lhd compile still emits a real always_latch/negedge; the recipe never names the pass; a skipped design emits BYTE-IDENTICAL Verilog; the pass DOES fire where it must (so "skipped" is falsifiable); rule 4 rejects a coincident-edge latch/flop pair by name AND still accepts the data-gated latch_mixed_flop shape; a second clock domain is skipped, not slotted and not refused — unless it also holds a latch, where it fails closed.
• graph/latch_contract_test.cpp — the commit-class analysis on hand-built graphs (data vs clock gate, master/slave = one net at opposite parity, an implicitly-clocked reg HAS a class, posclk false meaning FALL on a flop and RISE on a latch, the trigger in both directions, and the clock-name heuristic's boundaries).

LIVE — green today, guard against regression:

• Seven equiv pairs in inou/prp/tests/equiv/ (latch_enable_hold, latch_hold_basic, latch_active_low, latch_master_slave, latch_icg, latch_mixed_flop, plus latch_reset from M7), all PROVEN via lgcheck's bounded miter. Their prp-v2prp2v-latch_* reverse targets now carry REAL verdicts (all 8 including prp-v2prp2v-flop_reset_matrix); they used to pass VACUOUSLY with encoder REFUSED a cell … equivalence UNCHECKED. Step 3f.
• lhd/tests/lec_latch_polarity_test.sh — pins the lgyosys latch oracle: identical pair PROVEN (vacuity guard) AND a port-matched transparent-high vs transparent-low flip REFUTED, divergence depth 1 ≤ the 5-step bound.
• lhd/tests/lec_clock_blindness_test.sh — LIVE (no fixme tag). Asserts ALL THREE holes REFUTED since M8 (gated-vs-ungated, two-clock-vs-one-clock, AND negedge-vs-posedge), plus a vacuity guard: an EQUIVALENT mixed pos/neg pair, structurally different so the structural-identity shortcut cannot answer it, must still PROVE. The stale note below is kept for the reasoning it records; the header comment claiming fixme — stale, fix in the same batch.
• lhd/tests/latch_contract_check_test.sh — LIVE. Rules A, B, C rejected with the directed diagnostic. Step 1b adds a rule-4 case.
• lhd/tests/latch_fail_closed_test.sh — LIVE, but three of its cases assert the encoder refusal as CORRECT and go red when 1c lands. Step 3d.
• Seven sim fixtures in inou/prp/tests/sim/: latch_sim_hold, latch_sim_low, latch_sim_master_slave, latch_sim_negedge_enable, latch_sim_reset, flop_sim_posneg, flop_sim_gated_clock — all green since M5, plus edge_negpos.prp and multiclock_two_domain.prp. latch_sim_negedge_enable (a transparent latch qualifying a negedge flop's enable) has no formal twin — the one design where both M8 holes interact.

GREEN since M8 — the three :type: verify fixtures (they still live in inou/prp/tests/fixme/ only because moving them would renumber every prp-tbd-* target; the fixme TAG is what mattered and it is gone):

• latch_verify_hold.prp, latch_verify_low.prp — PROVEN via the P=1 Latch→Flop retype. Both mutate to a verbatim REFUTED at cycle 3, so neither proof is vacuous. The low twin is the anti-double-negation tripwire: it refutes if the polarity fold is wrong while the high twin still proves. Note: their polarity lives in the enable CONE (if !g), not in the posclk pin, so they are blind to the yosys-importer polarity path — which is why single_edge_four_classes_test.sh exercises the pin path separately.
• flop_verify_posneg.prp — PROVEN via the phase divider at P=2. Non-vacuity is checked the strongest possible way: the BLIND encoder's own answer (bq == previous aq) now REFUTES at cycle 4, so the encoder genuinely distinguishes the half-cycle transfer rather than having become permissive. Pins the end-of-cycle observation model.

Dual-fixture conventions (every sim+BMC twin follows these; they exist because of verified harness traps, not style):

• State the property TWICE: design-body asserts for lhd formal verify, test-block asserts for lhd sim — the two planes cannot see each other today (2f-formal runtime-fallback item merges them; when it lands, collapse the twins).
• assert(guard implies p), never if guard { assert(p) } — the formal obligation DROPS the if-guard and refutes spuriously at cycle 0.
• Snapshot every reg before any write (const c = cyc) — a reg read after a write sees the written next-state.
• Closed tb: ZERO data inputs; all stimulus is a pure function of an explicitly-initialized cycle counter. A cyclic schedule lets obligations prove INDUCTIVELY, not just to the bound.
• Validate every assert schedule against iverilog on the golden BEFORE baking it.
• REFUTED cycle numbers include the 2-cycle reset prologue: design-cycle k reports "REFUTED at cycle k+2". Under M8 they also count sub-steps — step 2d.

The last "still to write" item is now WRITTEN: inou/prp/tests/verify/latch_negedge_enable.prp is the formal twin of latch_sim_negedge_enable — a transparent latch QUALIFYING a negedge flop's enable, the register-file write-strobe shape, and the one design where both M8 holes interact. After normalization the two sit in DIFFERENT slots of one period, so slot 1's din reads a latch Q that already committed in slot 0. Four obligations PROVEN; each mutates to a verbatim REFUTED, and the c==3 mutant is exactly the value a WRONG slot assignment would produce (13 instead of 12), so the fixture is sensitive to the slot and not just to arithmetic.

One design choice in it is worth reading before writing a similar fixture: the latch there is gated by the CLOCK, not by data. A negedge flop samples its enable AT THE FALL, and a DATA-gated latch is generally still OPEN then — so the flop would sample the latch READING THROUGH, an observation the visibility rule forbids and a point where the commit-at-closing-edge model and real hardware genuinely disagree. A transparent-LOW latch is closed for the whole high half, so the fall lies inside its opaque window. The sim twin gets away with a data gate only because it samples q at end-of-tick and never through the enable. Everything else in the 3a–3h list is landed; see the status table.

NOT caused by this work, but red in the same suite (recorded so nobody attributes them to M8): lhd_sim_args_test, lhd_sim_clock_reset_test and lhd_sim_located_assert_test fail on driver-emission details in inou/prp/prp_sim.cpp (__clk_ratio, a literal operand rendered as Slop instead of a long, and the C++-keyword rejection message). None of the three involves a latch, a negedge or a second clock; prp_sim.cpp was last touched by ef0f79b9d / 17b29f574. One was fixed here because it blocked a latch test: an if-expression used as a VALUE in a test block (acc.d = if clock == 0 { 5 } else { 99 }) fell through to the binary-chain walker and died with "unsupported expression form in test: { 5 }", which took the ICG case of latch_fail_closed_test.sh down with it.

References

• Baumgartner, Heyman, Singhal, Aziz — Minimal-Dependent-Layer phase abstraction (CAV'99 / FMSD 2003): 8096 → 2586 state bits on an IBM GHz processor. NOT needed under the no-time-borrowing scope; kept in case scope widens.
• IBM US7624363 — LEC normalization: L1 → buffers, L2 → unit-delay registers, set all clocks constant 1, then ordinary register correspondence works with no solver changes. This is M8's lineage, and the L1-buffer rule is M3's unimplemented rule 4 — now a precondition (condition 5).
• Bjesse & Kukula, ICCAD'05 — extension to gated / overlapping clocks (ternary simulation for clock-like periodic signals; 41% average register reduction).
• Yosys async2sync / clk2fflogic — the mux-in-front lowering (Q = EN ? D : Q_prev, mux output IS Q). clk2fflogic is the closest published analogue of M8, but models the clock as data with explicit edge detection; M8 statically schedules the phases instead, which is what keeps the reset prologue tractable. (Observable difference: the mux-OUTPUT-as-Q form models transparency; our flop-output-as-Q form does not — the both-sides rule exists because of this.)
• Verilator: domain/trigger-gated evaluation (~100×, their number); ESSENT (DAC'20) activity skipping 1.5–11.5×; GSIM (2025) a further 2.5×.
• Working notes that fed this page: latch_formal.md (current-state audit), todo_edge_normalize.md (the M8 design), todo_multiclock.md (the user's seed note). All three are untracked repo-root scratch — this page is the plan of record.