Re:Formal Verification of Y86-64 Processors
by pjc50 on Sunday February 17, 2019 @12:13PM
(#19185482)
For formal proof purposes the system is usually treated as purely digital, and you rely on the lower level designers handling all the tedious initialisation and metastability issues. Generally you have a global reset signal to put everything into a known state, and a proof that anything that isn't known isn't read before it's written.
Internal multi-driver buses where you need Z states are such a pain that they're avoided wherever possible.
Of course, this means that you're still vulnerable to "outside context" attacks if they're outside the proof scope, such as fault injection over the power supply lines.
Re:Formal Verification of Y86-64 Processors
by jonas_o on Sunday February 17, 2019 @05:18AM
(#19183717)
You can get rid of metastability and high impendance in the proofs provided cycle time is large enough. Then you have cyclical binary logic.
This is a classical result shown eg in "Computer Architecture" (Müller Paul)
I don't know anyone working on formal verification of quantum hardware, would be interesting if anyone does it.
Re:Formal Verification of Y86-64 Processors
by nickpsecurity on Sunday February 17, 2019 @11:46AM
(#19185318)
It's happening:
If/when many qubits circuits can be fabricated, that also sounds like a mucho fun challenge for formal verification. It's an educated guess that people are already working/worked on it because the math usually precedes the hardware.