In a recent blog for EETimes, Mike Bartley (founder and CEO of TVS) posed the question “Are formal apps a Trojan horse for full formal adoption?”. A short abstract of the article is enclosed below.
Mythology tells us that the Greeks finally sacked Troy after a 10-year siege by being invited into the city hidden inside a now famous wooden “Trojan” horse. Similarly, formal verification (FV) has threatened to become mainstream for as long as I can remember. However, could it be that “formal apps” are the disguised guest that finally see us realize the Kathryn Kranen prediction that “formal will dominate verification”?
Formal apps are automated applications to achieve specific verification tasks such as verifying that signals correctly cross clock domain boundaries, that post-reset X’s do not cause functional issues, or that a SoC (system-on-chip) correctly implements signal connectivity as specified in a spreadsheet or an IP-XACT description.