[_mouvantsillage]

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.

[ampdepolymerase]

Can 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__]

The 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]

Physical 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]

A 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]

My 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.

[amelius]

Since 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?

[mhh__]

Spectre 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]

Only because most models focus on functionality, not on timing.

[mhh__]

No 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]

You 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.

[_mouvantsillage]

While 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

While this is still a long-term goal, I am planning to experiment how formal verification can be used in Racket-based hardware tools.

[i_don_t_know]

This is great! I also like your other posts in the series on tiny-hdl. Thank you for writing this up!

[mainland]

Great post! What do you use to draw your state diagrams?

[senshu]

All diagrams were created with Inkscape.

[spfzero]

Fascinating work, thanks for creating it!