3 ms·

Formal verification is still a pretty young field, and almost entirely academic. This is the first time I've heard of verification of mainstream processors agai

by nardi 10y ago

Formal verification is still a pretty young field, and almost entirely academic. This is the first time I've heard of verification of mainstream processors against a formal specification. I am not at all surprised that ARM did not already have people working on this.

zerohp 10y ago
Formal verification is being used by virtually every big name in chip design. That said, this is the first I've read of someone starting by parsing the ISA specification. It has been talked about but some people (myself included) were not sure if it would be reasonable in practice. It feels like most of the recent architecture grad students that I know have gone into formal verification in industry.
jldugger 10y ago
Formal verification of software is basically never done, but I was under the impression that chip vendors relied pretty heavily on both exhaustive state testing and formal verification.
- zerohp 10y ago
  Exhaustive state testing is intractable for any modern design. Some combination of constrained random verification and directed testing is used. http://chipdesignmag.com/display.php?articleId=4913 http://chipdesignmag.com/display.php?articleId=4913
  - AstralStorm 10y ago
    I wouldn't be so sure to call it intractable. It is pretty hard and time consuming, but not impossible by any stretch of imagination. Critical parts are hopefully exhaustively tested. Say, memory protection and security. That said, formal methods are better. ISA-Verifier is a pretty small tool though, nowhere near as strong as Isabelle model used for seL4 for example.
aseipp 10y ago
Intel has been doing it for years, and it's suggested they by far have the best hardware verification systems there are. They certainly learned from the FDIV bug. One of the engineers who works on verification of floating point stuff at Intel has written an excellent book on automated formal reasoning tools: http://www.cl.cam.ac.uk/~jrh13/ http://www.cl.cam.ac.uk/~jrh13/

by nardi 10y ago

zerohp 10y ago

Formal verification is being used by virtually every big name in chip design. That said, this is the first I've read of someone starting by parsing the ISA specification. It has been talked about but some people (myself included) were not sure if it would be reasonable in practice. It feels like most of the recent architecture grad students that I know have gone into formal verification in industry.

jldugger 10y ago

Formal verification of software is basically never done, but I was under the impression that chip vendors relied pretty heavily on both exhaustive state testing and formal verification.

zerohp 10y ago
Exhaustive state testing is intractable for any modern design. Some combination of constrained random verification and directed testing is used. http://chipdesignmag.com/display.php?articleId=4913 http://chipdesignmag.com/display.php?articleId=4913
- AstralStorm 10y ago
  I wouldn't be so sure to call it intractable. It is pretty hard and time consuming, but not impossible by any stretch of imagination. Critical parts are hopefully exhaustively tested. Say, memory protection and security. That said, formal methods are better. ISA-Verifier is a pretty small tool though, nowhere near as strong as Isabelle model used for seL4 for example.

aseipp 10y ago

Intel has been doing it for years, and it's suggested they by far have the best hardware verification systems there are. They certainly learned from the FDIV bug. One of the engineers who works on verification of floating point stuff at Intel has written an excellent book on automated formal reasoning tools: http://www.cl.cam.ac.uk/~jrh13/ http://www.cl.cam.ac.uk/~jrh13/