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