|
Not at apple: The following is about 10 years out of date, would be interesting to know what's changed: 10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators and validity checkers and/or assertions, and then work on the stimulators until you reached 100%coverage (signing off the cases that couldn't happen). That's not just line coverage, but each branch of an if, each component of a boolean expression must toggle, each bit of a signal must toggle, etc. Reaching 100% coverage was a tedious exercise so the first use of formal was as a sumplement, to find the last,most difficult test cases that completed your coverage (or prove that the cases were impossible). The next use was to try and prove directly that assertions or test failures could not occur, or provide a counterexample. this is all based on the tool being able to read low level verilog or systemC code. What it couldn't do at the time, which would be interesting to know if it can now, is as follows: Often, you actually have a higher level model of the behavior of your system. The RTL code is written to have the same behavior (manually, because it takes expertise to choose RTL code that will work efficiently). Ideally, provers would simply prove that your RTL has the same behavior. |
https://blogs.synopsys.com/from-silicon-to-software/2021/02/...