I recall a talk years ago from someone in hardware design. They used a mix of high level theorem proving and low level solvers, like SAT. To prove the whole design correct, from gates to funtionality, they worked from both ends. They used high level provers to decompose the funtionality into blocks and properties. They figured out how to represent chunks to get the low level solvers to prove larger and larger pieces. (They fixed problems they found in either approach.) As time went by, the amount they covered increased until finally they overlapped: they could prove that low level chunks that certain properties, and that those properties when composed yielded the final desired functionality.
So "simple" hardware verification problems can be solved with approaches like model checking, but higher level languages and semi-automated theorem proving are needed to put everything together. -paul- Paul E. Black 100 Bureau Drive, Stop 8970 paul.bl...@nist.gov Gaithersburg, Maryland 20899-8970 voice: +1 301 975-4794 fax: +1 301 975-6097 http://hissa.nist.gov/~black/ KC7PKT ________________________________________ From: shengyu shen <shengyus...@icloud.com> Sent: Friday, November 20, 2015 4:44 AM To: hol-info@lists.sourceforge.net Subject: [Hol-info] what is the application of manual theorem proving today in hardware verification Dear all: I am a new learner of HOL , and I am also a researcher on hardware verification. After learning HOL and COQ, and according to my experience in hardware verification, I get a feeling that : most, if not all, hardware verification problem can be solved with a framework similar to model checking, which generate CNF and call SAT/SMT solver. And it seems that almost all papers about coq and how appears in software language that reason about higher order logic. Is this correct? ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
