Re:Verifying ARM processors against the official ARM specifi...
by runeks on Wednesday July 27, 2016 @05:46PM
(#12176753)
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?
Re:Verifying ARM processors against the official ARM specifi...
by wyager on Wednesday July 27, 2016 @10:53PM
(#12178050)
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.
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.