Session

DescriptionAdvances in proof-centric RTL verification are showcased across agentic reasoning, scalable SAT/IC3, and high-throughput equivalence and model checking. Topics include a reasoning-enhanced programming agent, parallel SAT solving, and IC3 optimizations that cut SAT effort per obligation, complemented by data-driven lemma generation. Scalable combinational equivalence checking is addressed via miter-aware LUT mapping, parallel sweeping-based scheduling, and factored-form sharing. The session also covers complementary approximate reachability, invariant-driven verification of RISC-V cryptography extensions, and tensor-centric verification for domain-specific accelerators - highlighting how better structure and parallelism improve robustness and throughput on large designs.