2 ms·
Yeah, formal verification of software is sort of a niche topic, formal verification of hardware is like, one of the primary tools. Shit even something like Buil
by uxp100 4y ago
Yeah, formal verification of software is sort of a niche topic, formal verification of hardware is like, one of the primary tools. Shit even something like Built in Self Test, which is common in hardware, I’ve seen only rarely, and never comprehensive (I’m also not sure comprehensive BiST is the right way to think about reliability for software, it’s probably only very specific things that actually want that)
- mhh__ 4y agoHardware is also much simpler than software conceptually at least. You might think of a modern CPU as a black-box that goes out and finds (the lack of) dependencies in the instruction stream to exploit them, but this all has to be condensed into a logical circuit that is bounded in memory (registers), can be pipelined, and verified. And even then with hardware you are typically verifying things like "The pipeline never locks up entirely" or "The cache never gives back memory from the wrong physical address" basic things like that whereas these same kinds of invariants in software are rarely profitable to try and verify.