> You make this sound like you are the first person (team?) to do this. I'm thinking the other major ARM fab houses have already figured this out. Or are you the first person to release this outside your company?
The author doesn't work at just some ARM fab house... Author works for ARM Ltd.
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.
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.
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.
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.
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/
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.
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.
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.
I'm very confused and as the author I hope you can clarify this. The conclusion of the paper states:
》 This paper describes the steps needed to turn the basic idea into a scal- able, reusable technique: automation, dealing with a range of diferent micro- architectural design techniques, and initial bringup issues. We have applied this method to 8 diferent ARM processors spanning all stages of development up to release. In all processors, this has found bugs that would have been hard for conventional simulation-based methods to find and ISA-Formal is now a key part of ARM’s formal verification strategy. (emphasis mine)
Are you verifying that the Verilog code provided by ARM for the former type of partner matches what's on the processor after the whole synthesis and fabrication process or are you verifying that the Verilog matces a higher level spec?
