4 ms·
Would be possible to describe a modern CPU in something like TLA+ to find all non-electrical problems like these?
by Flow 3y ago
Would be possible to describe a modern CPU in something like TLA+ to find all non-electrical problems like these?
- boxfire 3y agoThere are still bit flipping tricks like rowhammer for RAM, I wouldn't be surprised if there are such vulnerabilities in some CPUs.
- sterlind 3y agoRowhammer is an electrical vulnerability though. PP specified non-electrical vulns.
- sterlind 3y agoI've heard Intel does use TLA+ extensively for specifying their designs and verifying their specs. But TLA+ specs are extremely high-level, so they don't capture implementation details that can lead to bugs. And model checking isn't a formal proof, only (tractably small) finite state spaces can be checked with TLC. And even there, you're only checking the invariants you specified. That said, I'm sure there's some verification framework like SPARK for VHDL, and this feels like exactly the kind of thing it should catch.
- dboreham 3y agoFormal methods have been used in CPU design for nearly 40 years [1] but not yet for everything, and the methods tend to not have "round-trip-engineering" properties (e.g. TLA+ is not actually proving validity of the code you will run in production, just your description of its behavior and your idea of exhaustive test cases). [1] https://www.academia.edu/60937699/The_IMS_T_800_Transputer https://www.academia.edu/60937699/The_IMS_T_800_Transputer
- foobiekr 3y agoCPU designers are so professional about verification and specification that they _dwarf_ software. There's just no comparison.