21–28 of 28 posts
Cool! Is there a similarly simple core to compare with in Bluespec and Clash?
Very impressive work. I've only spent about an hour going through this post and its predecessor. I'm a career software engineer, although I've been working very closely with a team of FPGA developers for the last couple of years. HDL engineers have a very strong preference to see the types of all nets and registers clearly defined. The pain points are mostly in organizing and stitching together larger projects out of…
> They are fully aware of the message-passing model that backs the HDLs. To them that model is an obstacle to be overcome on the way to building circuits. Can you expand on this? I don't quite understand what you mean by "message passing model" in the context of HDL. Signals are sort of like messages in the no shared memory sense but there is still plenty of spooky action at a distance when synthesizing. Unless your…
See Section 9 of the SystemVerilog language reference manual, ieee1800. Bootleg pdfs of the 2005 revision are readily available.
The formal semantics of the language's execution are defined in terms of message-passing. Any lowering to physical hardware should respect the same semantics even if it isn't actually passing literal messages from one reg to the next.
Earlier quoted context omitted.
> They are fully aware of the message-passing model that backs the HDLs. To them that model is an obstacle to be overcome on the way to building circuits. Can you expand on this? I don't quite understand what you mean by "message passing model" in the context of HDL. Signals are sort of like messages in the no shared memory sense but there is still plenty of spooky action at a distance when synthesizing. Unless your…
> Can you expand on this? I don't quite understand what you mean by "message passing model" in the context of HDL. See Section 9 of the SystemVerilog language reference manual, ieee1800. Bootleg pdfs of the 2005 revision are readily available. The formal semantics of the language's execution are defined in terms of message-passing. Any lowering to physical hardware should respect the same semantics even if it isn't a…
For many hardware engineers, I think that the message-passing semantics is a conceptual framework for explaining how simulators work. It is considered as a "necessary evil" that must be taken into account when writing HDL code.
When I write VHDL, I don't think in terms of communicating processes. I think in terms of combinational and sequential circuits that I describe with processes. The description is written in a way that makes the synthesizer generate the hardware that I had in mind.
I see a possible explanation for this mindset: since only a subset of VHDL or Verilog is actually synthesizable, we cannot rely only on the language semantics to write code that will map to functional hardware.
Earlier quoted context omitted.
> Can you expand on this? I don't quite understand what you mean by "message passing model" in the context of HDL. See Section 9 of the SystemVerilog language reference manual, ieee1800. Bootleg pdfs of the 2005 revision are readily available. The formal semantics of the language's execution are defined in terms of message-passing. Any lowering to physical hardware should respect the same semantics even if it isn't a…
Now I think I understand what you mean. For many hardware engineers, I think that the message-passing semantics is a conceptual framework for explaining how simulators work. It is considered as a "necessary evil" that must be taken into account when writing HDL code. When I write VHDL, I don't think in terms of communicating processes. I think in terms of combinational and sequential circuits that I describe with pro…
Other formal models like the lambda calculus have an advantage in that lambda functions and the type systems to work with them aren't that far removed from the machines that execute them. So the practicing software engineer doesn't have a hard time using that model directly++.
As you so demonstrated, practicing HDL engineers don't generally find the actor model to be a good mental representation of their designs. Nevertheless, even in the synthesizeable subset, the languages are formally specified using message-passing processes. They just also happen to admit non-synthesizeable designs as well.
Earlier quoted context omitted.
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?
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.
Earlier quoted context omitted.
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.
Only because most models focus on functionality, not on timing.
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?
Earlier quoted context omitted.
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)
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.
Earlier quoted context omitted.
Only because most models focus on functionality, not on timing.
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?
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.