2 ms·
This is extremely cool. It sort of begs the question: does Intel have a golden formal model? They must right? The most recent thing I’ve read about it is The P
by benreesman 4y ago
This is extremely cool. It sort of begs the question: does Intel have a golden formal model? They must right?
The most recent thing I’ve read about it is The Pentium Chronicles (highly recommended incidentally), but that’s eons ago.
Does anyone happen to know (and be at liberty to share) how the vendors cope with this internally?
- haskellandchill 4y agoI believe Intel has a model in the sense of model checking or symbolic execution as well as virtual simulations. Not sure what you mean by "golden model", but I don't believe they have a formal model to the level of compcert or related models in Coq/Agda/Isabelle.
- colejohnson66 4y agoWould it even be possible to formally verify such a system as a whole? From my limited experience with formal verification, even small designs can take over an hour to verify.