4 ms·
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 p
by jonas_o 8y ago
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.
- mrefj 8y agoThat 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-composition.html http://www.ccs.neu.edu/home/pete/research/ieee-vlsi-composit... http://www.ccs.neu.edu/home/pete/research/todaes-safety-liveness-refinement.html http://www.ccs.neu.edu/home/pete/research/todaes-safety-live...