Hacker News new | past | comments | ask | show | jobs | submit login
Formal Verification of Y86-64 Processors (csappbook.blogspot.com)
49 points by deepaksurti 6 months ago | hide | past | web | favorite | 8 comments



Didn't know what Y86 meant, but found this:

'The Y86 is a “toy” machine that is similar to the x86 but much simpler. It is a gentler introduction to assembly level programming than the x86. Just a few instructions as opposed to hundreds for the x86. Fewer addressing modes. Simpler system state. Absolute addressing.'


Yes, it's widely used among universities teaching intro computer systems, I believe.


Nice! Seems however like there is no obvious approach to scale this proof to a machine with caches and multicycle memory accesses, where you can not flush the pipeline quite as conveniently.


That is true. Scaling this to processor with caches and deep pipelines is completely non-trivial. There has been some attempt to scale to more "realistic" designs with compositional (stepwise) verification.

http://www.ccs.neu.edu/home/pete/research/ieee-vlsi-composit...

http://www.ccs.neu.edu/home/pete/research/todaes-safety-live...


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.


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.


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.





Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: