Verifying ARM processors against the official ARM specification

Re:Verifying ARM processors against the official ARM specifi... by jldugger on Tuesday July 26, 2016 @10:43PM (#12170174)

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.

[ Parent | on HN ]

Re:Verifying ARM processors against the official ARM specifi... by zerohp on Wednesday July 27, 2016 @12:29AM (#12170531)

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

[ Parent | on HN ]

Re:Verifying ARM processors against the official ARM specifi... by AstralStorm on Wednesday July 27, 2016 @12:56AM (#12170607)

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.

[ Parent | on HN ]