Verifying ARM processors against the official ARM specification | Hacker News Reader

Verifying ARM processors against the official ARM specification

alastairreid.github.io

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

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

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?

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

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.

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.

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.

Chisel is another new contender in the HDL space

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.

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.

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.

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

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

An old one here:

http://ghdl.free.fr/

Just found this verification toolkit Googling for the one above:

http://osvvm.org/about-os-vvm

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

https://github.com/nickg/nvc

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

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

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.

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.

http://ssrg.nicta.com.au/projects/TS/

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.

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

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

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

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

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

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

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

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

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.

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.

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

Reply on news.ycombinator.com