8 ms·
Verifying ARM processors against the official ARM specification
- AstroJetson 10y agoYou 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?
- Alupis 10y ago> 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.
- GauntletWizard 10y agoThat would probably put them on the first team to do this :)
- HammadB 10y agoIs it just me or does it seem weird that ARM wouldn't already have a system in place to do this...
- nardi 10y agoFormal 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 agoFormal 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 agoFormal 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 agoExhaustive 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 agoI 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 agoIntel 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 agoThe 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 agoDown 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 agoThis 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 agoA 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
- jcbeard 10y agoYup, as someone who works with him...I can indeed confirm that he does in fact work for ARM Ltd. :)
- femto 10y agoIt's interesting (and no coincidence?) that the one caveat with the OK Labs (now General Dynamics) verified micro-kernel was "assuming the hardware satisfies its specification". This work neatly plugs that gap, so the verification goes further down (with the new caveat that the EDA tools correctly implement the verilog source?) Does ARM have a supervisor mode, along the lines of the Intel Management Engine, which would leave a chink in the provably correct operation?
- jdub 10y agoNitpick: It was NICTA's (now Data61 at CSIRO) seL4 that was verified, not OK Labs' OKL4. The seL4 copyright is owned by General Dynamics.
- femto 10y agoThanks for the correction. I'm curious: what was the exact relationship between NICTA (now Data61) and OK Labs? I thought the verified kernel work was spun off into OK Labs, but that's not the case? Answering my own question, based on a bit of web surfing: OK Labs was spun out in 2007. The formal proof was completed by NICTA in 2009. This verification work continues today, within Data61. http://ssrg.nicta.com.au/projects/TS/ http://ssrg.nicta.com.au/projects/TS/
- happypanther 10y agolets see how much I get right here, NICTA was the australian government side, OK Labs was private company that spun out of it. Some early versions of OKL4 were opensource and based on code from NICTA(&others) but there was an internal rewrite that was OK Labs proprietary-only seL4 is yet another entirely separate codebase, written by NICTA, but where the copyright was given to OK Labs by NICTA.
- jdub 10y agoThe copyright of seL4 was not given (or licensed) to OK Labs AFAIK. It's currently owned by General Dynamics, and OK Labs no longer exists.
- ChuckMcM 10y agoThis is important work. And the author is not wrong about the sad state of hardware description through verilog. One of the reasons I chose to use VHDL over verilog was that it was somewhat more robust in terms of complete implementations you could get (especially cheaply) I find it interesting that ARM is doing this now versus all along. Was V8 the point where their licensees revolted and said "Hey, your spec is full of bugs, we're not going to pay a license fee for this crap." ?
- wolfgke 10y ago> It's interesting (and no coincidence?) that the one caveat with the OK Labs (now General Dynamics) verified micro-kernel was "assuming the hardware satisfies its specification". There is also SystemVerilog.
- fizixer 10y agoI'm seriously thinking of looking into MyHDL (myhdl.org). It's a way of specifying spec in python syntax and I think it automatically compiles down to VHDL (and probably more). It's especially good for programmers like me who would also be interested in building layers of abstraction to offload some of the cognitive burden. Anyone tried it?
- asimuvPR 10y agoI will try it now that you have linked to it. Email if you want to compare notes. :)
- bsder 10y agoIt's ... okay. However, full programming languages really aren't very good for specifying hardware, though. There are simply far too many constructs that don't actually map to to an implementation.
- sliverstorm 10y agoAnd of those that map to implementations, many are physically infeasible implementations
- raldi 10y agoWhy does "Cumulative Defects %" go up over time instead of down?
- astrange 10y agoBecause it's cumulative!
- therein 10y agoWouldn't "Cumulative Defects %" going up imply delta defects is greater than delta non-defects? Which shouldn't be the case.
- nardi 10y agoIt's not a very interesting graph. Just a measure of the % of defects they found through time with respect to the total number of defects they found. It shows that the process was mostly linear (indicating that there are probably still more defects to find).
- frozenport 10y agoReal problem is 100% of the cumulative means you didn't run it long enough.
- runeks 10y agoAs I read it: they found a number of defects over a period of time and this graph shows the time distribution of defects found.
- gravypod 10y agoSo I don't understand. Why make the "formal" specification for the processor rather then one in verilog (or some other immediately testable system) to start with? If you can't directly check from a provable formal system then it doesn't really help with validation and you have to jump through a lot of hoops to get there (like OP did).
- jlg23 10y agoThe "formal" specification is the goal, but the starting point is a rather informal specification. So it is an iterative process where you discover a bug and then have to figure out whether the bug is in the implementation or the interpretation of the presentation (i.e. the test).
- adreid 10y agoIt takes a lot of effort to write a specification. Just think how much software you have ever seen complete specifications for - and how close that number is to zero. So if you are going to write a specification, you really want to get maximum bang per buck out of the effort. Which means that it has to be good for many purposes: - documentation - verifying processors - dynamic verification (i.e., testing) - formal verification - testing test suites - verifying application software - dynamic and formal verification - verifying OSes, RTOSes, microkernels and other bare-metal software - verifying compilers - generating machine readable descriptions Verilog is great for one of these - but less good for all the others. Starting with a relatively neutral language gives you a lot more flexibility. It makes any individual task a bit harder than if that was your only goal but you save effort overall. There is also the virtuous cycle that bug fixes and improvements that help any one goal are folded into the master copy - so all other sub-projects benefit.
- unstatusthequo 10y agoAnd before many mobile providers and ISPs support the actual DNS routing
- kev009 10y agoIt's amazing how pretty much all HW development does formal verification business as usual.
- rkangel 10y agoMuch smaller state space so a much easier problem than formally verifying software.
- pjc50 10y agoIt's because you can't update hardware, and the NRE is huge. If every deploy cost you $250k you'd want formal verification too. Mostly the existing toolchain does formal equivalence checking, which isn't quite the same thing; it verifies that the behaviour of the output circuit is the same as the input RTL written HDL. The input HDL is subject to testing in a very recognisable manner - unit tests and integration tests that verify intended functionality. Usually with coverage reporting so you can be sure you've not forgotten areas of functionality. I feel that hardware formal verification is easier than software verification because the hardware can't be dynamically created, and there aren't weird non-local effects so it's easier to partition the problem. (Incidentally, this is the big failure flag for Ethereum: people building smart contracts without formal verification, in an environment where redeployment is extremely difficult and expensive.)
- snaky 10y agoThere is use in software too, for critical parts mostly. Microsoft and Amazon use TLA+.
- cia48621793 10y agoARM is just a mess. There are too many derives of original ARM implementation and they had made a battleground like Game of Thrones.