Basic types of flip-flops: specification and automatic verification

Abstract

The computer's hardware components are regarded as very modern real systems, properly to be modeled through formal methods. Specifically, our interests are concerning an algebraic prototype for the entire computer behaviour based on interconnected hardware components. The author's contributions in this paper are following two directions: presenting the original specification and implementation agents for modeling all the four types of basic flip-flop circuits behaviour and applying automatic verification of the corresponding agent's equivalences. These results represent the background of the sequential part of our prototype.