A unified framework for the formal verification of sequential circuits

Abstract

A unified framework for the verification of synchronous circuits is presented. Within this framework two verification tasks, verification by actual execution and by simulation, can be automatically performed using algorithms based on the same concepts. The first idea is to manipulate sets of states and sets of transitions instead of individual states and individual transitions. The second idea is to represent these sets by Boolean functions and to replace operations on sets with operations on Boolean functions. A definition is presented of the two problems addressed and then the authors present the verification algorithms. It is shown that these algorithms use the standard set operations in addition to two specific operations called 'Pre' and 'Img'. A brief explanation is presented as to why the basic set operations are very efficiently performed when sets are denoted by the typed decision graphs of their characteristic functions. The Boolean operators 'constrain' and 'restrict', and the function 'expand' that support efficiently the 'Img' and 'Pre' operations are presented. Experimental results are presented and discussed.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>