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" desig

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-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...