News for hackers. Stuff that matters.

A comment on Formal Verification of Y86-64 Processors.

Re:Formal Verification of Y86-64 Processors by jonas_o on Sunday February 17, 2019 @05:31AM (#19183747)
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.
[ Parent | on HN ]
Re:Formal Verification of Y86-64 Processors by mrefj on Sunday February 17, 2019 @01:11PM (#19185838)
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...

[ Parent | on HN ]