[thezoq2]

Spade author here!

That is a good point, sadly I'm not experienced enough with verification to know what is actually needed for verification from a language design perspective which is why I just offload to cocotb. There are a few interesting HDLs that do focus more on verification, ReWire, PDVL, Silver Oak, and Kôika are the ones I know about if you're interested in looking into them

Also, nitpick but amaranth does have its own simulator as far as I know

[polalavik]

Sorry hardcaml and amaranth were my examples of things with baked in sim features.

Also great work with spade. I love to hate, but the hardware industry needs folks like you pushing it forward. I just fear most people are making toys or focusing a ton of effort on the wrong issues (how to write HDL in a different way) instead of solving industry issues like verification, wrangling hand written modules with enormous I/O, stitching IP together, targeting real FPGAs, auto generating memory maps, etc. some of that is a tough solve because it’s proprietary.

[1] https://github.com/janestreet/hardcaml/blob/master/docs/wave...

[thezoq2]

Ah right, I didn't know hardcaml has a simulator

> wrangling hand written modules with enormous I/O, stitching IP together

This is something where I'm confident a good type system can help significantly, part of the problem imo is that the module interfaces are often communicated with prefixes on variable names. The Spade type system bundles them together as one interface, and with methods on that interface you can start to transform things in a predictable way

Generating memory maps is also an obvious problem to solve with a language that attaches more semantics to things. I haven't looked into it with Spade, but I believe the Clash people are working on something there

[imtringued]

What you need to do is have first party formal verification/design by contract support. Instead of the old school test bench approach, you should prioritize tools like fuzzing and model checking to find counter examples (e.g. bugs).

If there is something worth checking, but its only possible to check it in simulation (think UBSan), then you should add it anyway, just so that it can get triggered by a counterexample. (Think debug only signals/wires/record fields/inputs/outputs/components) You don't want people to write lengthy exhaustive tests or stare at waveforms all day.

Note that the point of formal verification here isn't to be uptight about writing perfect software in a vacuum. It's in fact the opposite. It's about being lazy and getting away with it. If you fuzz Rust code merely to make sure that you're not triggering panics, you've already made a huge improvement in software correctness, even though you haven't defined any application specific contracts yet!

[IshKebab]

This is another good reason to generate clean SV with meaningful stable signal names etc. There's absolutely no way you are going to replace e.g. SVA and formal verification tools.