Comment by anyfoo | Hacker News Reader

Comment by anyfoo | Hacker News Reader

Parent Full thread

Though generally, mimicking imperative languages (C and Ada for Verilog and VHDL respectively) is just such a bad fit for the massively parallel, circuit combining nature of FPGAs.

For my private projects (admittedly the only setting I currently use FPGAs for), I’ve since discovered clash, which is essentially Haskell for FPGAs, and am impressed how much more productive I am, how much abstraction a more fitting paradigm opens up, and how much more terse and readable the code is as a result.

I came about searching for an alternative when I got fed up with reimplement the same AXI protocol schemes over and over again, mostly through slightly altered cut and paste, and have instead slowly been building my own library of commonly used patterns and AXI protocol abstractions.

However, the one thing I’m not so sure about is whether I would be able to effectively use clash if I didn’t have any experience in using Haskell for software before, or whether I would be constantly banging my head against it just to finally give up instead. I suspect that the price of clash’s power of abstraction is a very steep learning curve.

You should checkout Chisel.

https://chisel.eecs.berkeley.edu/

Its a HDL in Scala. It used extensively by Berkeley for things like the Open-Source RISC-V Rocket and Boom SoC chips. There are lots of projects based on it and you have some of the best open-source cores implemented in it.

See:

- https://github.com/freechipsproject/rocket-chip

- https://github.com/ucb-bar/riscv-boom

And I'm going to throw out there that, unlike most of the "software language used as HDL" crap you see, Chisel is fundamentally different and better for it.

It's not really compiling Scala to a netlist; it's more that you're writing a Scala program who's output is a generated netlist. It's pretty fantastic to use.

Its actually a frontend that compiles to FIRRTL and the idea is basically that FIRRTL is like LLVM bytecode. All the optimization run on FIRRTL.

The idea is that eventually different people will use different methods to produce the FIRRTL.

Sure, but FIRRTL is a netlist format.

Sounds good. That is the case for clash, too, by the way. Every type passed in from the top level is wrapped in a higher-level "Signal" type which represents the whole stream, and you essentially combine circuits which have those types as input and output.

That type is Applicative, so you can lift functions on "normal" types into it. Conveniently, the type of the moore and measly functions for state machines happens to be pretty much exactly the type of a State monad, so you can use that, too, to make sequential state machines.

You can then simulate Signal streams for development and testing.

Totally agreed. Additionally, BlueSpec looks pretty nice too, but I haven't had a chance to play with it.

I was mainly directing my comment at those OpenCL to HDL compilers you see, and terrible stuff like this abomination https://reconfigure.io/

I would not recommend Chisel unless you have some experience in RTL design. Although it is less documented and has a smaller community, I find SpinalHDL to be quite a bit better (it's based on Chisel but has taken the idea a step further).

Chisel allows you to make many obvious mistakes that will be hard to debug and fix unless you've already got some experience. SpinalHDL catches many design errors (with info resembling tracebacks in some cases) before you get to simulation or synthesis.

> Kami, a Coq library that uses labeled transition systems to enable similar expressive and modular reasoning for hardware designs expressed in the style of the Bluespec language. We can specify, implement, and verify realistic designs entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in FPGAs. Our methodology has been evaluated in a case study verifying an infinite family of multicore systems, with cache-coherent shared memory and pipelined cores implementing (the base integer subset of) the RISC-V instruction set.

http://adam.chlipala.net/papers/KamiICFP17/

At Lockheed Martin I worked on a SIMD processor designed before VHDL and Verilog existed. The reference design was written in a lisp-like language. I don't know if the language had a name or if it was ever publicized in any way.

I'm curious to know more. Maybe some form/relative/precursor of EDIF (https://en.wikipedia.org/wiki/EDIF)? Not exactly Lisp, but an S-expression based format for describing netlists.

The DDD system was used in quite a few projects:

https://www.cs.indiana.edu/pub/techreports/TR544.pdf

May have been that one. If not, yall might still find it interesting.

I have read somewhere that Intel uses Haskell for formal verification, but public information is scarce.

Intel uses SystemVerilog for implementation and most likely also verification, some of the verification features in the system verilog standard were actually contributed by Intel. At some point they were using a ML derivative called reflect https://www.cs.ox.ac.uk/tom.melham/res/reflect.html in a verification environment called Forte https://www.cs.ox.ac.uk/tom.melham/res/forte.html. The implementation of Forte was open source at some point but sadly has (as far as I can tell) vanished from the internet. Here is a fairly recent presentation on formal verification by Intel (https://www.turing-gateway.cam.ac.uk/sites/default/files/ass...)

Here is another mention of Forte (https://ptolemy.berkeley.edu/projects/embedded/esd-seminar/s...) the link there is dead and the wayback machine apparently does not index ftp servers unfortunately.

Ah, I guess what I have read might have been about Forte and I mixed it up (ML and Haskell).

Thanks for the clarification.

Standard tools for formal verification of RTL is either SystemVerilog assertions or PSL. In my (limited) experience these are expressive enough to not be the problem with formal verification.

They must have some very specialized or large properties they want to prove if they decided to roll their own formal proving tool. That's not a small task. Of course, Intel does have more resources than most ASIC design shops.

Reply on news.ycombinator.com