CQ-SAT/GCC v0.28.0 adds a bounded experimental dense predicate quotient for state-dependent firmware and robotics models with 9–16 relevant inputs and 1–4 latches.
Highlights:
- exact BDD predicate compilation without enumerating all input patterns
- powered temporal relation composition and concrete trace reconstruction
- dual-direction agreement with persistent CDCL and maintained Yosys
- three separately authored interrupt, actuator, and sensor-fusion controllers
- reproducible 120-row evidence matrix and timing-free static admission boundary
- fail-closed support, latch, horizon, BDD-node, and cache limits
Admitted controlled rows show median end-to-end ratios of 1.21x–2.35x against persistent CDCL. Negative short-horizon rows are retained and rejected by the static gate.
Claim boundary: this is an experimental research backend, not default portfolio integration, a general SAT/model-checking speedup, a production-grade claim, or evidence of scholarly novelty.