latch support

CMakeLists.txt

@@ -159,8 +159,10 @@ ExternalProject_Add(cadical_external
     CONFIGURE_COMMAND ${CMAKE_COMMAND} -E env
         "CC=${CMAKE_C_COMPILER}"
         "CXX=${CMAKE_CXX_COMPILER}"
-        "CFLAGS=${CADICAL_KITTEN_SYMBOL_PREFIX_FLAGS}"
-        "CXXFLAGS=${CADICAL_KITTEN_SYMBOL_PREFIX_FLAGS}"
+        # Match the consumer's sanitizer policy, including libc++ container
+        # annotations. Mixing instrumented and plain STL instantiations is unsafe.
+        "CFLAGS=${CADICAL_KITTEN_SYMBOL_PREFIX_FLAGS} $<JOIN:$<TARGET_PROPERTY:sanitizers_config,INTERFACE_COMPILE_OPTIONS>, >"
+        "CXXFLAGS=${CADICAL_KITTEN_SYMBOL_PREFIX_FLAGS} $<JOIN:$<TARGET_PROPERTY:sanitizers_config,INTERFACE_COMPILE_OPTIONS>, >"
         ./configure -q --no-tracing --no-contrib ${KEPLER_EXTERNAL_PIC_ARG}
     BUILD_COMMAND make -C build libcadical.a
     INSTALL_COMMAND ""

docs/sec-clock-handling.md

@@ -105,9 +105,9 @@ next_state = enable ? data_next : current_state
 
 This means clock gating is modeled as state enable behavior rather than as a
 new independent clock when the gate is combinational and fully modelable.
-A gated clock cone that reaches a latch is opaque because SEC does not model
-level-sensitive state. Latch handling and strict fallback behavior are documented in
-[sec-sequential-models.md](sec-sequential-models.md).
+A latch in the clock path requires event modeling to preserve transparency and
+generated edges; see the [latch algorithm](sec-latch-support.md).
+Without that modeling, latch-dependent observations remain opaque.
 
 ## Complex Clock Trees
 

docs/sec-flags-spec.md

@@ -232,9 +232,6 @@ the final output property.
 The YAML spelling `learn_ineternal_relations` is accepted as an alias for
 `learn_internal_relations`; specifying both spellings is an error.
 
-The algorithm follows the candidate/refinement and inductive correspondence
-approach in [Mishchenko et al., ICCAD 2008](https://people.eecs.berkeley.edu/~alanmi/publications/2008/iccad08_seq.pdf).
-The ternary representation follows [Khasidashvili and Hanna, 2003](https://people.eecs.berkeley.edu/~alanmi/courses/2007_290N/papers/sec_intel_bmc03.pdf).
 The X option applies only to the internal candidate check; the existing output
 property and selected engine are unchanged. Turning off both switches retains
 the pre-learning SEC path.

docs/sec-internal-relations.md

@@ -40,7 +40,7 @@ exactly as it does without learning. Counting stops at the limit, so a large
 design is never built in memory just to be measured. tinyrocket has about 0.9
 million nodes; nangate45_black_parrot, with 666,543 candidates, exceeds the
 limit and would otherwise need over 13 GiB and tens of minutes. The gate is an
-engineering limit, not a technique from the papers.
+engineering limit.
 
 ## 4. Inductive step
 
@@ -51,33 +51,31 @@ one transition.
 - **Speculative reduction.** The hypotheses are applied by literal
   substitution: both registers of a pair share one current-frame literal. The
   two sides' transitions are then encoded over the same literals, so identical
-  logic collapses structurally and needs no search. (Mony et al., DAC 2005;
-  Mishchenko et al., ICCAD 2008, section 3.2.)
+  logic collapses structurally and needs no search.
 - **Partitioning.** One-step register correspondence needs a single time frame,
   so the candidates are split into partitions bounded by solver variables.
   Every hypothesis is merged in every partition and each candidate is proved in
   exactly one, so splitting loses no relation. A large design is split rather
-  than skipped. (Mishchenko et al., section 3.3.)
+  than skipped.
 - **Variables on first use.** A partition reads a small part of the design, so
   its solver creates a variable only when the encoded logic first mentions a
-  symbol, not one per symbol per frame. This is an implementation choice, not a
-  technique from the papers. It lowers memory and encode time per partition.
+  symbol, not one per symbol per frame. This implementation choice lowers
+  memory and encode time per partition.
 - **Query.** Each partition asks whether some candidate in it can differ in the
   next frame.
   - UNSAT: all of its candidates hold under the hypotheses.
   - SAT: the counterexample is replayed (below).
   - Undecided within budget: each pair of that partition is asked separately
     on the same solver with its own budget, and only the pairs that stay
-    undecided are dropped. (Mony et al., sections 2 and 4.1.)
+    undecided are dropped.
 
 ## 5. Refinement by simulation
 
 A counterexample is replayed on the original transitions as one of 64 parallel
 patterns; the other 63 are random states that also satisfy the hypotheses. The
 replay runs for up to 16 steps, and every candidate seen differing on a valid
 pattern is dropped. One counterexample therefore refines all candidates, not
-only the pairs the solver model happens to separate. (Mony et al., section
-3.2.)
+only the pairs the solver model happens to separate.
 
 Simulation only drops candidates. It never proves one.
 
@@ -95,5 +93,5 @@ nothing; if the round limit is reached first, nothing is returned.
   reach; the output check still reports the counterexample.
 - Equivalent designs whose logic was rebuilt (for example synthesis netlist
   versus final netlist) prove few pairs: register equalities alone are often
-  not inductive there. Mishchenko et al. address this with signal
-  correspondence, which also relates internal nodes. That is not implemented.
+  not inductive there. Signal correspondence, which also relates internal
+  nodes, is not implemented.

docs/sec-latch-implementation.md

@@ -0,0 +1,176 @@
+# Latch Event Behavior
+
+This is a zero-delay Boolean model of latches, gates, and flip-flops. One
+external transaction changes permitted inputs; internal events then propagate
+until a complete, stable boundary is reached. Only those boundaries are
+observed. The environment cannot interrupt an unfinished settling episode.
+The [latch-support design](sec-latch-support.md) gives the proof obligations
+and the distinction between current broad-region handling and safe local
+scheduling.
+
+## External transactions
+
+An ordinary step is an input event, not a hardware clock cycle or one internal
+wave. Enables can open and close between flip-flop edges, and data propagates
+through an open latch without any clock edge.
+
+By default, a transaction may change any number of external input bits,
+including none. A restriction to at most one external bit per transaction is
+a different environment assumption. It does not restrict internally generated
+changes or remove their possible arrival orders. Both comparison designs
+receive the same external stimulus and use the same event contract.
+
+## Primitive behavior
+
+### Basic latch primitive: register plus transparent mux
+
+For an active-high latch without asynchronous controls, `H` is the remembered
+bit, `D` the data, `E` the enable, and `Q` the visible output:
+
+```text
+Q       = E ? D : H
+next(H) = Q
+```
+
+```mermaid
+flowchart LR
+    D["Data D"] -->|Open| M["Transparent<br/>mux"]
+    E["Enable E"] --> M
+    H["Abstract register<br/>H"] -->|Closed| M
+    M --> Q["Output Q"]
+    Q -->|next H = Q| H
+```
+
+The register represents remembered history, not a flip-flop driven by a
+hardware clock. The visible value is the mux result: open selects current
+data; closed selects remembered storage.
+
+The actual event model composes both operations into one primitive. For each
+permitted ordering, changed pins are visited once each; every visit uses the
+storage and pin history left by the preceding visit:
+
+```mermaid
+flowchart TD
+    A["Incoming storage<br/>and pin history"] --> P
+    subgraph L["One latch primitive"]
+        P["Visit next<br/>changed pin"] --> M
+        M["Select data<br/>or stored value"] --> R
+        R["Private update:<br/>storage and output"]
+        R -->|"More pins:<br/>carry history"| P
+    end
+    R -->|Last pin| S["Stage final<br/>storage and output"]
+    S --> W["Commit with<br/>the whole wave"]
+    W --> N["Changed outputs<br/>activate consumers<br/>for next wave"]
+```
+
+Only the ordering's final values are published at the wave boundary; intermediate
+storage updates remain part of that primitive's history. These are the same
+latch equations, but this correspondence does not prove equivalence to an
+arbitrary separately scheduled register/mux decomposition. Splitting the blocks
+can add waves, change capture ordering, or alter pulses seen downstream.
+
+For example, start with `D=0, E=1, H=0`, then change data to `1` while closing
+the latch. Data-first can retain `1`; close-first retains `0`. Both orders must
+be considered. A unique-result claim cannot silently choose the favorable one.
+
+Active-low latches reverse the enable polarity. Defined asynchronous clear or
+preset rules override transparency. Physical outputs may invert stored state
+or combine it with current inputs, as in an integrated clock gate. Undefined
+or unsupported control combinations are errors if reached.
+
+Gates compute their Boolean functions from the current wave's inputs.
+Flip-flops instead apply their specified edge and asynchronous-control rules,
+threading history through changed-pin visits; a later data visit cannot reuse
+an earlier clock edge. No blanket clock-cycle update is applied to all storage.
+
+## Initialization and propagation
+
+Unspecified external inputs and storage begin as arbitrary Boolean values,
+not assumed zero and not literal unknown-valued logic. Concrete restrictions
+apply only when explicitly requested. Initial external levels are shared
+between comparison designs; their internal storage origins are independent.
+
+Initialization is itself a checked settling episode:
+
+1. Project physical storage outputs from remembered state and the defined output
+   expressions. Treat auxiliary internal-net seeds as arbitrary.
+2. Set previous pin values equal to current values. Starting with a high clock
+   does not fabricate a rising edge.
+3. Force an initial evaluation: gates compute, latches apply transparency and
+   asynchronous rules, and flip-flops apply asynchronous rules without an
+   invented edge. Generated clock changes in subsequent waves are real events.
+4. Require every auxiliary seed and permitted ordering to settle to the same
+   complete boundary for each genuine input/storage origin. Different genuine
+   origins may yield different boundaries; all remain represented.
+
+A closed, unreset latch therefore keeps its unspecified history even when
+other storage is reset. Initialization is not an implicit reset sequence.
+
+For ordinary propagation, activated primitives read one frozen pre-wave
+snapshot. Their final storage/output tuples commit together; changed nets
+activate all consumers for the next wave. Independent evaluations can proceed
+in parallel without their completion order choosing a capture. Each producer's
+result is shared across its fanout. Intermediate pin visits are private, but
+transitions between network waves are preserved.
+
+### Reset-cycle adapter
+
+A requested reset duration remains a count of complete clock cycles, not input
+events. With one unambiguous source clock and one reset, the reset episode
+composes already-settled event transitions:
+
+1. Assert reset and settle; establish a low source clock and settle. Any
+   alignment edge from an initially high clock is represented while reset is
+   active.
+2. For each requested cycle, sample all non-clock/non-reset inputs. Admit them
+   together when simultaneous external changes are allowed; otherwise compose
+   one-bit transactions covering every arrival order. Hold the sampled levels
+   through both clock edges.
+3. Drive the clock high and settle, then low and settle, completing that cycle.
+4. After the final cycle, release reset and settle before observation resumes.
+
+The two designs share these input and ordering choices. This is a cycle-sampled
+reset environment, not arbitrary asynchronous activity inside a cycle. No clock
+is guessed from signal names or latch enables. Multiple clocks or resets,
+ambiguous clock roots, and latch-only designs need an explicit justified
+schedule; a cycle request cannot silently become an event count. Afterward,
+ordinary event transactions resume with reset held inactive.
+
+## Regions and safety
+
+Current whole-design handling groups every primitive connected through
+internally driven data or control nets into broad event-connected regions.
+Shared read-only external inputs alone do not join regions. Feedback groups
+are also identified, but their size does not supply a settling bound, and a
+flip-flop does not automatically cut generated-clock or asynchronous-control
+dependencies. Certification currently covers each whole broad region; this
+can make large, otherwise useful designs impractical to certify.
+
+Safe event scheduling follows changed-net dependencies and preserves every
+consumer-visible wave, including transient clock, enable, and asynchronous
+control activity. Replacing broad regions with independently settled local
+summaries requires a preservation argument; publishing only final region
+outputs can lose consequential pulses. The latch primitive representation
+does not itself establish that optimized scheduling is solved.
+
+Certification requires error-free progress to stability under every admitted
+transaction and internal ordering, plus one complete resulting state—not just
+matching visible outputs. Complete state includes stored bits and remembered
+net/pin values. Initialization must satisfy the same requirements,
+and the accepted boundary set must remain closed under future transactions.
+Feedback is accepted only when these obligations hold; a possible infinite
+internal execution is not repaired by choosing a settling execution.
+
+Bounded symbolic reasoning or exhaustive finite exploration can establish
+these obligations. A failed bound or exhausted resources means unproved,
+not necessarily oscillating. Unsupported or uncertified regions remain opaque
+by default: affected outputs are excluded, not proved. A strict policy may
+instead reject any opaque behavior. No troublesome event or initial origin is
+discarded to manufacture success.
+
+## Limits
+
+This contract does not model propagation delays, setup/hold violations,
+metastability, unknown/high-impedance logic, multiple drivers, or arbitrary
+hardware/HDL scheduling. Broad-region certification remains a coverage and
+scalability limitation; safe local reductions require additional justification.