4 ms·

Is it just me or does it seem weird that ARM wouldn't already have a system in place to do this...

by HammadB 10y ago

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/
moflome 10y ago
The key is that the "formal verification" methods[0] the author is describing are still novel in the hardware industry, especially involving "human readable" ISA specifications and HDL's. [0] https://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/vis_user/node4.html https://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/...
AstroJetson 10y ago
Down karma, so might as well comment some more, so yes it seems weird that ARM wouldn't have a way to do this in-house. How do they prove to the fab houses that the chip specs are good and don't have errors. With the high cost to make one, I think I'd like know that it's really going to work. Since the OP works for ARM, good that they are starting to do this. And since they are in the best position to see everything, it will be something that other vendors can rely on for their designs.
- akiselev 10y ago
  This article is about testing the implementations of various ARM processors (eight different product lines in various stages of design and production, according to the conclusion section) against the general ARM-v8m architecture specification that the manufacturers received as part of their licensing deal. Many of the processors already exist in the real world in smartphones and other hardware, this is just testing how many errors each manufacturer made when they took the IP and designed a physical chip, which are much bigger than just the ARM architecture. This is not verifying whether the specification and architectural decisions are bug free.
  - adreid 10y ago
    A few clarifications: The paper is about searching for bugs in ARM's designs - not designs by ARM's architecture licensees. (ARM has two types of partner: those who use ARM designed processors exactly as provided by ARM and those who create their own processors implementing ARM's architecture.) The tests are performed on the Verilog. There are very good and thorough techniques such as Logical Equivalence Checking (LEC) for verifying that what gets taped out actually matches the Verilog. We used the v8-A architecture spec that provides Virtual Memory and other features you need to support Linux, Android, etc. This is the architecture that applies to phones, tablets, servers, etc. And we used the v8-M architecture spec that applies to micro-controllers. Also, it is worth saying that this is only one of many verification techniques used. This one focuses on the processor pipeline rather than the memory system, instruction fetch, etc.
    - 10y ago

Is it just me or does it seem weird that ARM wouldn't already have a system in place to do this...

by HammadB 10y ago

Is it just me or does it seem weird that ARM wouldn't already have a system in place to do this...

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/

moflome 10y ago

The key is that the "formal verification" methods[0] the author is describing are still novel in the hardware industry, especially involving "human readable" ISA specifications and HDL's. [0] https://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/vis_user/node4.html https://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/...

AstroJetson 10y ago

Down karma, so might as well comment some more, so yes it seems weird that ARM wouldn't have a way to do this in-house. How do they prove to the fab houses that the chip specs are good and don't have errors. With the high cost to make one, I think I'd like know that it's really going to work. Since the OP works for ARM, good that they are starting to do this. And since they are in the best position to see everything, it will be something that other vendors can rely on for their designs.

akiselev 10y ago
This article is about testing the implementations of various ARM processors (eight different product lines in various stages of design and production, according to the conclusion section) against the general ARM-v8m architecture specification that the manufacturers received as part of their licensing deal. Many of the processors already exist in the real world in smartphones and other hardware, this is just testing how many errors each manufacturer made when they took the IP and designed a physical chip, which are much bigger than just the ARM architecture. This is not verifying whether the specification and architectural decisions are bug free.
- adreid 10y ago
  A few clarifications: The paper is about searching for bugs in ARM's designs - not designs by ARM's architecture licensees. (ARM has two types of partner: those who use ARM designed processors exactly as provided by ARM and those who create their own processors implementing ARM's architecture.) The tests are performed on the Verilog. There are very good and thorough techniques such as Logical Equivalence Checking (LEC) for verifying that what gets taped out actually matches the Verilog. We used the v8-A architecture spec that provides Virtual Memory and other features you need to support Linux, Android, etc. This is the architecture that applies to phones, tablets, servers, etc. And we used the v8-M architecture spec that applies to micro-controllers. Also, it is worth saying that this is only one of many verification techniques used. This one focuses on the processor pipeline rather than the memory system, instruction fetch, etc.
  - 10y ago