3 ms·
Interesting. Formally-proving a classical processor circuit design (as opposed to the ISA and RTL) must be fun as sequential and bus logic aren't just 0 and 1,
by iceninenines 8y ago
Interesting. Formally-proving a classical processor circuit design (as opposed to the ISA and RTL) must be fun as sequential and bus logic aren't just 0 and 1, as there's high-impedance, time where a result isn't yet stable and uninitialized. Also, there are don't care states and values in the design which aim to reduce circuit complexity and latency.
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.
- jonas_o 8y agoYou 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.
- nickpsecurity 8y agoIt's happening: https://www.seas.upenn.edu/~rrand/qpl_2017_talk.pdf https://www.seas.upenn.edu/~rrand/qpl_2017_talk.pdf
- pjc50 8y agoFor 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.