A functional-based approach to formal VLSI design verification

A functional approach to formal specification and verification of digital circuits is introduced. A past operator is defined in order to describe sequential behaviors. Prolog is used both as a hardware description language and also as an inference mechanism for proving the correctness of the design. The verification process runs largely automatically. Some designs with an interesting degree of complexity have already been verified.