5 ms·

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

by anyfoo 8y ago

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.

pjmlp 8y ago
I have read somewhere that Intel uses Haskell for formal verification, but public information is scarce.
- KSteffensen 8y ago
  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.
- orbifold 8y ago
  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 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 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/asset/doc/1707/Big%20Proof%20Day%20Melham%2019-07-2017.pdf 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/spring03/abstract/moondanos.html 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.
  - pjmlp 8y ago
    Ah, I guess what I have read might have been about Forte and I mixed it up (ML and Haskell). Thanks for the clarification.
nickik 8y ago
You should checkout Chisel. https://chisel.eecs.berkeley.edu/ 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/freechipsproject/rocket-chip - https://github.com/ucb-bar/riscv-boom https://github.com/ucb-bar/riscv-boom
- monocasa 8y ago
  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.
  - nickik 8y ago
    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.
    - monocasa 8y ago
      Sure, but FIRRTL is a netlist format.
  - anyfoo 8y ago
    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.
sn 8y ago
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.
- gh02t 8y ago
  I'm curious to know more. Maybe some form/relative/precursor of EDIF (https://en.wikipedia.org/wiki/EDIF https://en.wikipedia.org/wiki/EDIF)? Not exactly Lisp, but an S-expression based format for describing netlists.
- nickpsecurity 8y ago
  The DDD system was used in quite a few projects: https://www.cs.indiana.edu/pub/techreports/TR544.pdf https://www.cs.indiana.edu/pub/techreports/TR544.pdf May have been that one. If not, yall might still find it interesting.
snaky 8y ago
> 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/ http://adam.chlipala.net/papers/KamiICFP17/

by anyfoo 8y ago

pjmlp 8y ago

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

KSteffensen 8y ago
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.
orbifold 8y ago
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 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 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/asset/doc/1707/Big%20Proof%20Day%20Melham%2019-07-2017.pdf 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/spring03/abstract/moondanos.html 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.
- pjmlp 8y ago
  Ah, I guess what I have read might have been about Forte and I mixed it up (ML and Haskell). Thanks for the clarification.

nickik 8y ago

You should checkout Chisel. https://chisel.eecs.berkeley.edu/ 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/freechipsproject/rocket-chip - https://github.com/ucb-bar/riscv-boom https://github.com/ucb-bar/riscv-boom

monocasa 8y ago
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.
- nickik 8y ago
  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.
  - monocasa 8y ago
    Sure, but FIRRTL is a netlist format.
- anyfoo 8y ago
  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.

sn 8y ago

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.

gh02t 8y ago
I'm curious to know more. Maybe some form/relative/precursor of EDIF (https://en.wikipedia.org/wiki/EDIF https://en.wikipedia.org/wiki/EDIF)? Not exactly Lisp, but an S-expression based format for describing netlists.
nickpsecurity 8y ago
The DDD system was used in quite a few projects: https://www.cs.indiana.edu/pub/techreports/TR544.pdf https://www.cs.indiana.edu/pub/techreports/TR544.pdf May have been that one. If not, yall might still find it interesting.

snaky 8y ago

> 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/ http://adam.chlipala.net/papers/KamiICFP17/