Carnegie Mellon University
file.pdf (126.58 kB)

Formal Methods for Functional Verification

Download (126.58 kB)
journal contribution
posted on 1995-07-01, 00:00 authored by Randal E. Bryant, James H. Kukula
Formal hardware verification ranges from proving that two combinational circuits compute the same functions to the much more ambitious task of proving that a sequential circuit obeys some abstract property expressed in temporal logic. In tracing the history of work in this area, we find a few efforts in the 1970s and 1980s, with a big increase in verification capabilities the late 1980s up through today. The advent of efficient Boolean inference methods, starting with Binary Decision Diagrams (BDDs) and more recently with efficient Boolean satisfiability (SAT) checkers has provided the enabling technology for these advances.




Usage metrics