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." ?
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.
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.
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 . 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?
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?
Just found this verification toolkit Googling for the one above:
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.
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.
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.
Anyone tried it?
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.
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.
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?
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.
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.
There is also SystemVerilog.
Does ARM have a supervisor mode, along the lines of the Intel Management Engine, which would leave a chink in the provably correct operation?
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.
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.
Sort of if you count TrustZone?
There are tools for verifying that, too. LEC & LVS
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.)
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).
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:
- 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
The author doesn't work at just some ARM fab house... Author works for ARM Ltd.
It feels like most of the recent architecture grad students that I know have gone into formal verification in industry.
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.
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/
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 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.
》 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 ﬁnd and ISA-Formal is now a key part of ARM’s formal veriﬁcation 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?