We describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. The system works in two steps: first, it builds a labeled state graph; second, it uses an efficient algorithm called a Model Checker to determine the truth of a temporal formula with respect to the state graph. We generate the state graphs by two different techniques. The first extracts the state graph directly from the circuit by simulation. The second complies an HDL specification into a state graph. As examples we verify an asynchronous queue element using the first technique and a traffic light controller using the second.
|Original language||English (US)|
|Title of host publication||Unknown Host Publication Title|
|Editors||Cees-Jan Koomen, Tohru Moto-Oka|
|Number of pages||16|
|State||Published - Dec 1 1985|
ASJC Scopus subject areas