Symbolic model checking for sequential circuit verification

摘要: The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) partitioned transition relations. Because this representation captures some the regularity in space circuits with data path logic, we are able verify an extremely large number states. We demonstrate new technique on a synchronous pipelined design approximately 5/spl times/10/sup 120/ Our handles full CTL fairness constraints. Consequently, express important liveness properties, which would otherwise not be expressible CTL. give empirical results performance applied both asynchronous logic. >