Adrian Sampson
This blog post is an extended metaphor that serves as an excuse to complain about Verilog. https://www.cs.cornell.edu/~asampson/blog/buildingblocks.html
Back to the Building Blocks’ Building Blocks

Verilog is the foundation of all hardware design, and it is fatally flawed. We should all be worried about a glut of hardware bugs caused by Verilog’s unpredictable semantics and simplistic type system.

May 26 at 2:37pmWeb
Show threadTheZoq24d ago

@adrian

"This footgun has a name: X-optimism. That’s the standard behavior for Verilog: if treats X as false, which incorrectly makes conditional assignments appear defined when they are actually unknown."

TIL, I more and more suspect that my rule about C++ that "Every feature, no matter how trivial, must have a pitfall" applies to Verilog too

Show threadTheZoq24d ago
@adrian Oh my god wat, the justification is _simulator performance_??????
Show threadAdrian Sampson4d ago
@thezoq2 yeah, I was surprised to find that quote! in their defense, the correct semantics do indeed seem slow to simulate… 🤪
Show threadKevin Laeufer4d ago
@thezoq2 @adrian VCS has an option to do the slow but more correct thing. X prop might still be unsound though.
Show threadAdrian Sampson4d ago
@ekiwi @thezoq2 Ah yeah, maybe I should mention somewhere that (despite X-optimism being the official semantics), different simulators disagree and some have configuration options…
Show threadTheZoq24d ago
@adrian @ekiwi Ah, even better!
Show threadCan Lehmann4d ago

@adrian I feel this. I am currently working on our SystemVerilog Frontend for @verijit and I was surprised how differently you think about Verilog when designing hardware vs when writing a simulator. I mean I knew in theory that Verilog is event driven, but the common subset people actually use does conveniently not run into this much.

I feel like I am actually writing half a synthesis toolchain to make our simulator fast. We gained an entire new intermediate representation for this reason.

Show threadCan Lehmann4d ago

@adrian Honestly, much of this feels like it comes from the idea that you can do verification and design in a single language + the very "I know it when I see it" approach to defining the synthesizable subset.

Essentially it feels a bit like bolting on a half baked imperative/OO language onto an existing HDL. Having separate languages seems like the way forward here.

(I don't have enough experience with embedded DSLs to really have an opinion on that yet)

Show threadTheZoq24d ago
@CanLehmann @adrian Absolutely! And given the popularity of cocotb it seems like the world is moving in a synth/sim language separation already. We just need to make sure that we stop using Verilog as the synth language :D
Show threadCan Lehmann4d ago
@thezoq2 @adrian Cocotb is greeat! While I have many smaller issues with it (performance and its bitvector API are two of them), I think the overall direction is correct.
Show threadTheZoq24d ago

@CanLehmann @adrian Yep, performance is a really big downside to it.

I'm really excited for @ethan's https://github.com/ethanuppal/marlin and need to get around to finishing the Spade support for it. Especially with Verilator's upcoming 4-valued simulation support

GitHub - ethanuppal/marlin: 🦀 No-nonsense hardware testing/simulation in Rust 🛠️ | Verilog, Spade, Veryl

🦀 No-nonsense hardware testing/simulation in Rust 🛠️ | Verilog, Spade, Veryl - ethanuppal/marlin

GitHub
Show threadTheZoq24d ago
@CanLehmann @adrian @ethan Oh wait, I just realized that Spade codegen inherits Verilog's "X is falsy" problem because we inherit Verilog semantics for things like this 
Show threadCan Lehmann4d ago

@thezoq2 @adrian @ethan I mean honestly it seems like the solution to that is to auto generate assert ~$isunknown(...) for all conditions. At least that what I will probably do for verijit (probably with a flag because we still need to support the actual behaviour somehow).

I mean in the if(1'bx) thing is a classic refinement issue, i.e. you are simulating one refinement of your model, but the synthesis tool might refine differently.

Show threadTheZoq24d ago

@CanLehmann @adrian Yeah, I guess I'm just annoyed by us potentially falling for a footgun like this and having to deal with it

Though on further reflection I remembered that we compile to ternaries and not if

Show threadKevin Laeufer4d ago
@thezoq2 @CanLehmann @adrian chisel was designed to be two state only. Thus, the original compiler would insert a lot of randomization in order to avoid any X. Now that SiFive is selling the generated SystemVerilog and customers combine it with other designs that have X, all of this has changed a bit.
Show threadKevin Laeufer4d ago
@thezoq2 @CanLehmann @adrian grumble grumble: https://github.com/chipsalliance/rocket-chip/pull/2659
Misc. fixes to make Rocket tolerant to X-propagation by aswaterman · Pull Request #2659 · chipsalliance/rocket-chip

grumble grumble Related issue: Type of change: other enhancement Impact: no functional change Development Phase: implementation Release Notes

GitHub
Show threadCan Lehmann4d ago
@ethan @thezoq2 @adrian To what extent is marlin testbench language agnostic? It seems like currently it is rust only, but what would be the overhead associated with having C++ bindings?
Show threadTheZoq24d ago
@CanLehmann @ethan @adrian Oh, Marlin is a simulator agnostic testbench library if you distill it. Currently, Verilator is the only backend so C++ bindings for Marlin would just be Verilator test benches :D
Show threadEthan4d ago
@thezoq2 @CanLehmann @adrian and cxxrtl which i am also working on supporting is C++ too. the only cases i can think of where C++ support wouldn't come for free as a result of me needing to generate C ffi (and so there is already a C interface) would be a rust simulator like veryl's new one
Show threadCan Lehmann4d ago

@thezoq2 @ethan @adrian Ok, that makes sense. So it seems like this would mostly be interesting once there is

a) handling of more complex data types from the HDL
b) simulators other than verilator

Show threadTheZoq24d ago

@CanLehmann @ethan @adrian

For me with Spade, the complex data types from the HDL is the big selling point of Marlin.

But I also am not sure if C++ is a particularly good choice for a testbench language, so even if I was writing Verilog I think i'd prefer Rust over C++ or taking the performance hit from Cocotb

Show threadCan Lehmann4d ago
@thezoq2 @ethan @adrian In the end it comes down to personal preference I think. The big advantage you have with C++ is its popularity in the embedded space: Since people are familiar with it, using it to implement a testbench has a lower barrier to entry. I realize increasingly many people also adopt Rust, though I am not sure where the actual adoption in industry is.
Show threadTheZoq24d ago

@CanLehmann @ethan @adrian Oh yeah, Rust certainly doesn't have the market share of C++ yet.

But with that argument, we should also use Verilog :P

Show threadCan Lehmann4d ago

@thezoq2 @ethan @adrian Oh yeah sure 🤣

Though I think in this aspirational world, Rust wouldn't be it either for me. I realize that I am going to make myself a bit unpopular in this thread by saying this, but I love C++ for how I can quickly bend it to do whatever I want. The safety vs. extra effort tradeoff has not made sense for me, since most of the bugs I actually sped time debugging are logic issues somewhere in some compiler pass, not memory issues.

Show threadTheZoq24d ago

@CanLehmann @ethan @adrian

Oh yeah, C++ certainly wouldn't be my last choice for a language, I love the fact that if I want to do something, there is almost certainly a way to do it, albeit a hacky one.

The reason I like Rust so much is that it brings a lot of that, but with more type safety and less footguns

Show threadCan Lehmann4d ago
@thezoq2 I think Swift has come closest for me personally, but I never got to use it as much as I would like to. Also especially if you want to interface with LLVM using a non C++ language is extremely annoying. So maybe the answer is "a secret third thing" 😅 or idk something like -fbounds-safety + praying that by using arenas and refcounting nothing breaks to badly 🤣
Show threadTheZoq24d ago

@CanLehmann I do need to try swift at some point, from what I hear it has some really good ideas.

And for what it's worth, I've often said that if I had to remove any feature from Rust, it'd be memory safety. I think you're right that logic bugs are more interesting generally, and the rest of the Rust type system does a very good job of catching those in my experience

Show threadCan Lehmann4d ago
@thezoq2 Oh thats an interesting take, which I don't think I've heard before. Isn't memory safety the reason why people use Rust in the first place?
Show threadTheZoq24d ago

@CanLehmann For me, memory safety is the thing that brought me to the language, but I'm staying for the functional inspired type system and top tier tooling. I assume I'm not alone in that

I guess it also depends on the context, I use it as a fast high level language for compilers, if I was doing more systems programming I'd care a lot more about memory safety

Show threadCan Lehmann4d ago
@thezoq2 Interesting! I mean I certainly wouldn't mind having a better type system in C++. Especially proper tagged unions which do not have std::variant's ugly interface would be great.
Show threadTheZoq24d ago
@CanLehmann Ah yes, tagged unions are one of the main things I miss in C++, and not having them in Verilog was a big reason to start Spade :D
Show threadAdrian Sampson4d ago
@CanLehmann FIRRTL is not without its own problems, but this is one thing they got right: it is strictly a design representation, so it forces anything unsynthesizable to go somewhere else.
Show threadAdrian Sampson4d ago

@CanLehmann @verijit
> I am actually writing half a synthesis toolchain to make our simulator fast

This is a *great* way to distill the ecosystem problem that Verilog causes. If we had better, more language-agnostic representations for hardware, much more of this stuff could be shared between (e.g.) synthesis and simulation.

Show threadCan Lehmann4d ago
@adrian Yes. I still quietly hope that CIRCT will get there eventually, but at least last I played with it, it wasn't there yet. (maybe its time to try again soonish...)
Show threadJohn Regehr4d ago
@adrian thankful to be working in software so I can deal with C and C++ instead 🙏
Show threadPete Bleackley4d ago
@adrian Your post doesn't mention #VHDL at all. As far as I remember from my brief use of it about 20 years ago, it doesn't require #Verilog as an intermediate stage. Can you comment on it?
Show threadAdrian Sampson4d ago
@PeteBleackley Ah yeah, great question! VHDL is sometimes the exception to the rule that "all EDA tools support Verilog and only Verilog." Not all tools support it, though, and it is sometimes a second-class citizen. For example, IIRC Yosys supports VHDL only by translating it to Verilog first via https://github.com/ldoolitt/vhd2vl !
GitHub - ldoolitt/vhd2vl

Contribute to ldoolitt/vhd2vl development by creating an account on GitHub.

GitHub
Show threadWilliam D. Jones4d ago
@adrian @PeteBleackley Nowadays, GHDL has a yosys plugin that I've successfully used: https://github.com/ghdl/ghdl-yosys-plugin
GitHub - ghdl/ghdl-yosys-plugin: VHDL synthesis (based on ghdl)

VHDL synthesis (based on ghdl). Contribute to ghdl/ghdl-yosys-plugin development by creating an account on GitHub.

GitHub
Show threadyuubi4d ago
@adrian i assume X-pessimism (in case the condition involves X, set all outputs that might be affected by any branch to X) would have even worse problems obvious to verilog knowers, but i don't immediately see a reason you'd actually want that case to not clobber all the possible outputs.
Show threadJoshua Wise4d ago
@adrian @lindsey I like this post and, as is my way, I agree strongly about some parts of it and I disagree strongly about other parts.

One of the things that I find most striking about the digital logic world vs. the software world is the approach to correctness. The software world has spent many years building tooling around making software correct by construction, and around reducing cognitive load of people building large systems in the hope that this will make the large systems more reliable. A lot of research has gone into human factors of software, and building good ways to analyze it and say meaningful things about it.

The digital logic world takes a very different approach to correctness. The assumption is that the implementation of hardware may be incorrect until it is shown to meet a specification (and that this continues all the way until production articles exist, and are shown to meet that specification!). For one thing, this means that a specification must exist! But for another thing, it means that the hardware world has instead built extensive tooling around demonstrating that hardware is, or is likely to be, correct. Load-bearing linters are a way to demonstrate that the hardware is *un*likely to have certain kinds of *in*correctnesses. Formal methods are a way to demonstrate that the described hardware always meets a certain element of a specification, and that the hardware that is sent to manufacturing is identical to the hardware that is described. And verification test vectors (and the reliance of coverage metrics in building them!) are a way to demonstrate that the HDL code meets the spec -- and *also* are a way to demonstrate that the physical thing that you have in your hand also meets the spec (and to demonstrate that it does it at all clock speeds and process variations!).

It is *wildly* uncommon for software projects to demand 100% line coverage and 100% memory data pattern coverage in tests. It is *wildly* uncommon for software projects, even projects that are at the core of almost every computer used, to have formal verification to show that their behavior always matches a specification. And, on the other side, it is *wildly* uncommon for digital logic to have any kind of type description other than "yes, this is a bit or a product of bits" (or, as you note in Verilog, "this is a sum of a bit, or a Something Else, or a high-impedance state").

This is not to say that the hardware world would not benefit from, like, modern human factors thinking about programming languages. And this is *definitely* not to say that I like Verilog. I imagine the initial bug rate of digital logic projects that designed with something more advanced than, uncharitably, "banging sticks together", would be much lower, and the development cost might even be moderately lower!

But I am not convinced that the bug *escape* rate would change dramatically. And, more to the point, I think that if the hardware world *replaced* the existing verification and correctness methodologies with strong type systems and "correct-by-construction" methodologies, you would find that the bug escape rate would get dramatically worse.

(If you can believe it, I have longer thoughts about this, and why this might be specific to how hardware is designed. But this has already gotten unreasonably wordy, so I'll spare you, for now...)
Show thread✧✦Catherine✦✧4d ago
@adrian have you read the HOPL paper on Verilog? it pretty soundly refutes the notion that Verilog was designed for simulation and retrofitted for synthesis. this is not widely known because (I would argue!) Verilog is not a great source language for synthesis, but it is indisputable that the intent was there considering the people who came up with it say so
Verilog HDL and its ancestors and descendants (HOPL IV - Papers) - HOPL IV

The Papers track of HOPL-IV will include published papers that will be complemented by oral presentations at the conference. The Program Committee encourages submissions that discuss and analyze the historical development of individual programming languages, programming language families, language features, design themes, and other strong influences on the direction of programming language design, implementation, and usage. Detailed information is listed on separate pages. Click on either the tabs above or the links in the list below. Prospective authors should read the Call for Papers, ...