Hacker News new | comments | show | ask | jobs | submit login
Verifying ARM processors against the official ARM specification (alastairreid.github.io)
219 points by jsnell on July 26, 2016 | hide | past | web | favorite | 64 comments

This 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." ?

Clash (Haskell) and Chisel (Scala) are vastly superior HDLs. Clash is actually a compiler plugin that compiles a large subset of Haskell to hardware, while chisel is a DSL.

Thanks for the pointers to other HDLs. I was aware of Chisel but had not seen Clash before.

Another Haskell Hardware DSL is Lava: http://ku-fpg.github.io/software/kansas-lava/ Chisel is very similar to Lava in many ways although I think Chisel has been used for larger designs.

Reduceron is written in York Lava and is not a tiny project. Lava predates Chisel, Clash, and MyHDL and in my personal opinion is superiour. There are room for more improvement though and Real Soon Now I'll start work on that.

Do you have any experience with Clash? It almost sounds too good to be true, even if it's only a large subset it can translate.

Yep. Used it for my university's upper division processor design course. It's super kick ass. Here's some example code for an associative cache (which is part of one of the CPUs I made): https://github.com/wyager/Lambda16/blob/master/CPU/Cache/Ass...

As you can see, it's just plain old Haskell. Clash is really just a few GHC extensions and plugins. Spits out Verilog, SystemVerilog, or VHDL. You can also compile it to a regular executable, which means you don't have to use shitty HDL debugging software; you just debug the executable like normal (including error messages and stuff).

Here's a blog post for a Clash project I did, including actual hardware http://yager.io/HaSKI/HaSKI.html

And some slides from a talk I gave http://yager.io/talks/CLaSH.pdf which should give you an idea of how it works.

This is really cool! I have been thinking about the possibility of this for a long time.

How much hardware experience do you have? I'm curious to know how much effort there would be in porting a Haskell library consisting of pure functions, like the Elliptic Curve Cryptography library [1]. ECC is fairly CPU intensive to verify (the best hand-written assembly implementation takes 0.5 ms per signature). This makes it a bottleneck for some operations, like verifying the Bitcoin blockchain, which contains millions of them.

I can't wait for high level libraries to start forming on top of the Clash library. The only thing left is more competition in the FPGA market, I guess, but perhaps this won't happen until non-hardware folks can actually program an FPGA?

[1] https://hackage.haskell.org/package/eccrypto

Being a pure function isn't sufficient; it also can't use general recursion or dynamically sized data structures. You could certainly write an ECC implementation using Clash, but you might have to do a bit of porting work.

> 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)

A) Icarus Verilog is open source and free, and the author works with a couple of people on the Verilog committee last I checked ...

B) What VHDL implementations are free and open source?

Also Verilator (http://www.veripool.org/wiki/verilator) supports SystemVerilog, is open source, stable, and FAST. There are also a number of commercial users: https://en.wikipedia.org/wiki/Verilator#Commercial

An old one here:


Just found this verification toolkit Googling for the one above:


nvc (LLVM based) is also impressively complete for the number of people who have worked on it.


I found the free VHDL tools from Altera and Xilinx to be quite good from a spec completeness point of view. At least for their tools what you "paid" for was a better synthesis back end. I built a 7 segment HEX decoder which should have synthesized to 2 LUTs on a Xilinx chip but it kept synthesizing to 14. I finally spec'd it in VHDL as a series of gates (practically RTL) and that worked. The paid version got it into 2 LUTs pretty much no matter how I specified it.

Altera Quartus has supported SV (SystemVerilog) quite well for some time now. I tend to work in 9.1sp2 as that was the last version of Quartus with integrated simulator (waaa!).

Xilinx requires you to use their newer tooling in order to write in SV. As these tools tend to be incredibly bloated, this is a disadvantage IMO (you want to use the earliest and therefore least bloaty tool that does the job).

I started out in VHDL and was forced by the other person on the "team" to learn verilog for a project. As with ANY language, you end up trying a bunch of stuff out to see how things are implemented, what breaks, etc. in order to get your footing. Over time I grew to appreciate the C like nature of verilog - its reduced verboseness over VHDL makes it an easier language to get actual things done in. And it makes switching between C and verilog pretty natural.

I resisted looking into SystemVerilog for forever as I was under the impression that it was more of a systems verification thing, but it is actually just plain old verilog with some incredibly useful extensions for synthesis. The package system is really, really nice. Look online for papers by Stuart Sutherland. No language is perfect, and there are things I would change in SV (support for negative bit indices, less awkward sub vector select, etc.) but SV comes closest to the ideal HDL IMO. HW design via HDL is fascinating, and a strangely small space for the times we live in.

Using high level languages to do clock-based concurrent stuff is IMO insane as it just adds to the chain breakage, and few will be trained and able to easily use the source. Would you listen to anyone who proposed a VHDL to Haskell converter for writing everyday conventional software? HDLs are close to the metal for a reason.

Do the makers of these open source implementations make any money off it? Or is the motivation just fun?

The motivation is generally that Electronic Design Automation software sucks .. for black hole levels of suck.

EDA software exists in a weird reality of a small number of people who use it and an even smaller number of people who understand, really, how to program it while being excessively valuable to a very captive market base.

A small number of users combined with an even smaller programmer base results in a large number of features per user. Consequently, if you aren't using the absolute, bog-standard central features, you are going to hit bugs. And, if your feature is even slightly esoteric, you may be 1 of 2 users of that feature worldwide.

Add in to this mix that the programmers of EDA software often don't actually know how to use that use that software, and you have an absolute nightmare of misfeatures combined with bad usability with a whole bunch of bugginess on top.

The only way around this is open-source. Sure, your open source version is worse. However, a sufficiently motivated user can pull the code and fix a bug. A sufficiently motivated user can pull the code and add a missing feature. Open source can accumulate the effort of the very small number of individuals who can both code software and design hardware over a very large block of time without interference from market pressures.

Finally, EDA tools have software lifetimes of decades. We are still using SPICE decks that trace to late 70s FORTRAN.

An example of all of this coming together is software I wrote probably 15 years ago. I once wrote an HSPICE reader in Python. No big deal you say? Well, it could read 15 years of HSPICE files--some of which had been transferred from strange things like fixed-record file machines. It was WAY better than anything any HSPICE vendor ever coughed up. I released it open source.

And about 10 years ago, somebody found it, and extended it to even MORE HSPICE formats. It is now even better than any commercial HSPICE reader will likely ever be. However, had I made the code closed source, the person who found it would have created his own code that only dealt with a couple of formats that he was interested in.

So, the fact that I made that code open source means that if I ever need to come back to it, it is now fundamentally better than anything I could have written and is available to me regardless of what company I'm working for.

So, not only does my itch get scratched, it gets scratched better than I could possibly have ever done myself.

I don't have too much knowledge of ARM, but from what I hear the errata are surprisingly few in number (compared to say, an x86 cpu).

Also, that is not to say companies like ARM are only recently verifying their chips. This is only in regards to formal validation, which others have explained the circumstances of pretty well. There are still entire teams dedicated to code and functional validation.

The novel aspect is "formal verification" methods[0] the author is describing, especially involving "human readable" ISA specifications and HDL's.

[0] https://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/....

Chisel is another new contender in the HDL space

I'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?

It'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.

Sure, if you just try to write software and expect it to work as hardware you're going to have a bad time, but that's not really the point of these tools.

The reason to use a programming language for hardware design is that modern programming languages are monumentally better at abstraction than pretty much any available HDL or hardware design tools.

However those abstractions rarely map to hardware well.

For example, I use hash maps and vectors for almost all of the adhoc data structures in my programs. Neither of these have a useful abstraction in hardware.

At that point, why am I using a modern programming language?

Again, those are software concepts. That's not what I'm talking about.

The point is, there are many hardware level constructions (FIFOs, BRAMs, CAMs, etc.) which can be very usefully abstracted.

And you use a software language to do it, simply because the hardware languages are so bad at it. There's no reason a HDL couldn't be good at expressing these abstractions (indeed Bluespec exists and does a fairly good job), but since they don't, using a programming language simply as a metalanguage is still better than actual HDLs.

And of those that map to implementations, many are physically infeasible implementations

And the designs that are feasibly synthesizable usually have to be tweaked until the timing works out, which gets harder the faster your clock speed and the more different clock/power domains you have.

There's a significant risk that any high level abstraction would be leaky enough that you might have to rip up large parts of the design and start from scratch with Verilog/HDL anyway.

I will try it now that you have linked to it. Email if you want to compare notes. :)

> 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.

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". 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?

Nitpick: It was NICTA's (now Data61 at CSIRO) seL4 that was verified, not OK Labs' OKL4. The seL4 copyright is owned by General Dynamics.

Thanks 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.


lets 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.

The 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.

> Does ARM have a supervisor mode, along the lines of the Intel Management Engine, which would leave a chink in the provably correct operation?

Sort of if you count TrustZone?

with the new caveat that the EDA tools correctly implement the verilog source?

There are tools for verifying that, too. LEC & LVS

It's amazing how pretty much all HW development does formal verification business as usual.

It'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.)

There is use in software too, for critical parts mostly. Microsoft and Amazon use TLA+.

Much smaller state space so a much easier problem than formally verifying software.

Why does "Cumulative Defects %" go up over time instead of down?

Because it's cumulative!

Wouldn't "Cumulative Defects %" going up imply delta defects is greater than delta non-defects? Which shouldn't be the case.

It'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).

As I read it: they found a number of defects over a period of time and this graph shows the time distribution of defects found.

Real problem is 100% of the cumulative means you didn't run it long enough.

So 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).

The "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).

It 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.


> 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.

That would probably put them on the first team to do this :)

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

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/...

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.

Exhaustive state testing is intractable for any modern design. Some combination of constrained random verification and directed testing is used.


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.

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.

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.

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?

Yup, as someone who works with him...I can indeed confirm that he does in fact work for ARM Ltd. :)

And before many mobile providers and ISPs support the actual DNS routing

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact