Enhanced verification by temporal decomposition
- 1 November 2009
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper addresses the presence of logic which has relevance only during initial time frames in a hardware design. We examine transient logic in the form of signals which settle to deterministic constants after some prefix number of time frames, as well as primary inputs used to enumerate complex initial states which thereafter become irrelevant. Experience shows that a large percentage of hardware designs (industrial and benchmarks) have such logic, and this creates overhead in the overall verification process. In this paper, we present automated techniques to detect and eliminate such irrelevant logic, enabling verification efficiencies in terms of greater logic reductions, deeper Bounded Model Checking (BMC), and enhanced proof capability using induction and interpolation.Keywords
This publication has 7 references indexed in Scilit:
- Temporal decomposition for logic optimizationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Sequential equivalence checking based on k-th invariants and circuit SAT solvingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Automatic generalized phase abstraction for formal verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Automatic Formal Verification of Fused-Multiply-Add FPUsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Sequential equivalence checking based on structural similaritiesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2000
- Equivalence checking using cuts and heapsPublished by Association for Computing Machinery (ACM) ,1997
- MIS: A Multiple-Level Logic Optimization SystemIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1987