Using formal tools to study complex circuits behaviour

We use a formal tool to extract Finite State Machines (FSM) based representations (lists of states and transitions) of sequential circuits described by flip-flops and gates. These complete and optimized representations help the designer to understand the accurate behaviour of the circuit. This deep understanding is a prerequisite for any verification or test process. An example is fully presented to illustrate our method. This simple pipelined processor comes from our experience in computer architecture and digital design education.