Abstract
Static timing analysis tools verify temporal signal arrival across integrated circuit paths. However, these tools rely on user-specified timing exceptions without validating underlying logical soundness. Incorrect timing exceptions applied to active logical paths can lead to physical functional failures after chip fabrication. A closed-loop automated framework translates timing constraints into formal properties using a generative large language model, combined with a deterministic formal verification engine. Structural logic cones associated with target timing paths are extracted from register-transfer level code to provide concise context to the large language model. The large language model generates formal property assertions representing the logical conditions implicit in the timing exceptions. The formal verification engine attempts to prove the assertions against the design logic. If an assertion is proven, the timing exception is marked validated. If an assertion fails, counter-example execution traces are automatically reformatted into structured textual feedback and returned to the large language model, which formulates explanation reports and remedial design guidance.
Keywords: static timing analysis, standard design constraints, SystemVerilog Assertions, large language models, formal verification, closed-loop timing validation, false path verification, logic cone extraction, clock domain crossing.
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.
Recommended Citation
N/A and , "Closed-Loop Automated Framework For Validating Timing Exceptions Via Model-Generated Formal Assertions", Technical Disclosure Commons, (November 02, 2026)
https://www.tdcommons.org/dpubs_series/12609