The beauty of using different computation paradigms is that you get to avoid this whole circuitous process. Instead of writing some code in e.g. C, then a TLA+ model for that code, proving the equivalence of the two and then making proofs about that model, you could just code for TLA+ directly. Then you can write code normally, have the proofs inline as assertions and there's nothing to laboriously adjust or get out of sync. If we chose our primitives carefully, we might not even have to prove anything at all and our code will just have certain properties By Construction.

Of course on CPUs we don't do that because it's hard to turn that into efficient CPU assembly and people aren't used to thinking that way. But in hardware design this is ubiquitous and easy. Languages like verilog were actually originally built for formal verification and newer ones like bluespec are directly inspired by things like TLA+. You just write your model of how the hardware should behave, say "on every clock cycle, the value needs to be one larger than the last" and the toolchain figures out how to make that happen.

GPUs are admittedly a lot closer to CPUs in this regard, but there's still plenty to be lost here by moving to C-likes instead of embracing the unique parallel computational model of modern hardware.

Posted Jan 10, 2024 16:07 UTC (Wed) by farnz (subscriber, #17727) [Link]

On the other hand, when you write code in Agda, TLA+ or Bluespec, you're writing two things in the same language:

1. A set of proofs that the code has the properties you want.
2. The implementation that has those properties - bearing in mind that if your properties are well-specified, the implementation can be inferred for you by the compiler (anywhere where there's only one way to do it can be inferred, and where there's a common way to do it, that can be inferred unless you override it with a different implementation).

They're interlinked, so that you get the machine-checking and the assistance in understanding why your description does not meet the specification as part of the compilation process, but it's telling that none of the options for doing this sort of thing with software (Agda, Coq, Epigram, Idris, Alloy, TLA+, Lean, ATS, Eiffel) have made a significant impact on software development practices.

Posted Jan 10, 2024 16:20 UTC (Wed) by Vipketsh (guest, #134480) [Link]

Vcc: a Clang compiler for Vulkan

One problem of "formal verification" is not that same as another. What you often hear with "formal verification" in hardware is really "proof that the synthesis tool's input and output are functionally equivalent"*. That is very different from "I have a proof that my code has these properties" being discussed above.

The former is so common that no-one goes into manufacturing without such a proof and the whole ecosystem is geared toward making this proof happen even at the expense of performance/power/area (e.g. synthesis tools have avoided any state-machine recoding because of the difficulty it has in making the proof). The later has been successfully used a few times for some things (e.g. FPU designs) but as farnz said before this is an open area of research and nowhere as easy in practice as the sales people would have you believe.

* At least insofar as the tools themselves are correct. I have personally had cases where the formal verification tool has miss-interpreted the input the same way the synthesis tool did.

Posted Jan 10, 2024 23:24 UTC (Wed) by atnot (subscriber, #124910) [Link]

Vcc: a Clang compiler for Vulkan

Vcc: a Clang compiler for Vulkan

They generally fall into two categories, which I've seen called native HDLs and meta HDLs.

Meta HDLs are things like SpinalHDL, Chisel, Amaranth, MyHDL, Hardcaml and many more. You write code in a host language like Python that builds a big data structure that describes your design, and then dump it out as a big verilog file. They're pretty popular because they're easy to make and much more pleasant to do metaprogramming in than things like standard verilog. Think of it like programming by writing scripts that output LLVM IR. Very powerful, but also a bit clumsy. But because they're just fancy macro tools, they're pretty restricted to what can be done in their host language.

This is different from native HDLs like (System) Verilog and VHDL, which work the traditional way by having bespoke syntax with a parser, passes etc. There's a lot fewer of these in active development: Bluespec SV, PipelineC, Silice, Spade, that's about it. Of those only Bluespec has any significant users. This is generally what people mean when they complain about the state of input languages and where there's a lot of potential to improve things.