4 ms·
Author here. This post is part of an ongoing experiment to use Racket as a platform for hardware description languages. Describing a RISC-V core in Racket is a
by _mouvantsillage 5y ago
Author here.
This post is part of an ongoing experiment to use Racket as a platform for hardware description languages.
Describing a RISC-V core in Racket is a step in this direction, but the ultimate goal is neither to use Racket itself as an HDL, nor to define an embedded hardware description DSL in Racket.
The long-term goal is to create an HDL that would benefit from Racket's "language-oriented programming" facilities, with the ability to simulate digital hardware, but also to generate standard Verilog or VHDL.
- i_don_t_know 5y agoThis is great! I also like your other posts in the series on tiny-hdl. Thank you for writing this up!
- ampdepolymerase 5y agoCan you do a write up on the lower level algorithms like place and route, circuit constraints solving optimization, the process from the netlist stage to autorouting? The engineering behind VHDL and Verilog systems are way too opaque for most software engineers.
- mhh__ 5y agoThe book "Electronic Design automation" by Wang, Chang, and Cheng is quite approachable. The reason why they are opqaue is partly because the problem is hard, and secondly because the developers of the code make money directly off the tools (like compilers were in the past)
- User23 5y agoPhysical layout CAD software is really interesting though and heavily scriptable. I’m pretty sure at least one major offering uses some kind of lisp as its extension language.
- monocasa 5y agoA lot of the were written fully in lisp back in the day, and might still be underneath it all. ie. it might be more than just being used as an extension language.
- _mouvantsillage 5y agoMy experience in the lower-level aspects of hardware synthesis is limited but I would love to explore this topic. I use proprietary synthesis tools for FPGAs everyday but I do not develop them. My situation is similar to that of a software engineer who uses compilers and who could only explain how they work in general terms.
- mainland 5y agoGreat post! What do you use to draw your state diagrams?
- senshu 5y agoAll diagrams were created with Inkscape.
- spfzero 5y agoFascinating work, thanks for creating it!
- amelius 5y agoSince there was a post about Spectre on the HN front page today, I wonder if HDLs should perhaps contain more formal verification tools; is that on the roadmap?
- _mouvantsillage 5y agoWhile simulation is a well-established practice among digital hardware developers, I have the impression that formal verification is still largely ignored. I hope it changes as free tools are emerging such as SymbiYosys https://symbiyosys.readthedocs.io https://symbiyosys.readthedocs.io While this is still a long-term goal, I am planning to experiment how formal verification can be used in Racket-based hardware tools.
- mhh__ 5y agoSpectre isn't really something that you can catch with formal verification. It sort of isn't a bug, that's why it's such a problem.
- amelius 5y agoOnly because most models focus on functionality, not on timing.
- mhh__ 5y agoNo it's because they focus on speed. Eliminating spectre is either very hard or very slow. Of course you could verify that spectre does or doesn't happen formally, but at what cost?
- sitkack 5y agoYou changed your argument flavor like a neutrino, used a false dilemma and had it swim with red herring. Don't take this as a harsh judgement but as something to work on. There are ways to solve this now with type systems, dependent type systems, affine type systems, session types, etc. That allow us to track and prove what pieces of data should be visible (for many definitions) to whom. We also will not know the cost unless we start designing our systems rigorously. Think of it as an accounting problem, and economics problem and engineering is made of up primarily as the combination of economics and failure analysis. We have the means and methods to solve these problems now, we should use them.