Introduction to formal processor verification at logic level : a case study

International audienceThis paper presents the case study proposed to 3rd year students in our department of computer science. It is a practical activity in the first Computer Architecture Unit of the curriculum. This practical activity has several aims : 1) understanding a subtle mechanism in processor architecture, 2) experimenting the relations between logic level and RTL level descriptions and 3) practicing formal methods of verification. The main original point is the use of extraction (and minimization) of the full description of an automaton from the logic schema based on flip-flops and gates. In a certain way, the reverse of classic automaton synthesis