Formal verification of CPU in laboratory work

We have compared the quality between CPUs designed by a conventional testing method and those designed by a formal verification method, on the practical designing processes in CPU designing laboratory work for undergraduate students. About eighty students were divided into two groups; GROUP V (by a formal verification method) and GROUP T (by a conventional testing method). Students in GROUP V used our provers to prove the correctness of their designs, while students in GROUP T carefully check the design with waveform simulators. Nobody correctly designed CPUs in GROUP T by a deadline, while almost every student correctly designed CPUs in GROUP V by the sane deadline. From the comparison results, we can conclude that the formal method is useful for designing CPUs correctly.