| Title | Dependent Latch Identification in the Reachable State Space |
| Author | Chen-Hsuan Lin, *Chun-Yao Wang (National Tsing Hua University, Taiwan) |
| Page | pp. 630 - 635 |
| Keyword | dependent latch, functional dependency, reachability analysis |
| Abstract | The large number of latches in current designs increase the complexity of formal verification and logic synthesis, since the growth of latch number leads the state space to explode exponentially. One solution to this problem is to find the functional dependencies among these latches. Then, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. This paper proposes an approach to find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, the proposed approach detects sequential functional dependencies existing in the reachable state space only. Experimental results show that our approach could deal with large sequential circuits with up to 1.5K latches in a reasonable time and simultaneously identify the combinational and sequential dependent latches. |
| Title | Complete-k-Distinguishability for Retiming and Resynthesis Equivalence Checking without Restricting Synthesis |
| Author | Nikolaos Liveris, *Hai Zhou (Northwestern University, United States), Prithviraj Banerjee (HP Labs, United States) |
| Page | pp. 636 - 641 |
| Keyword | sequential equivalence checking, retiming and resynthesis, verification |
| Abstract | Iterative retiming and resynthesis is a powerful way to optimize sequential circuits but its massive adoption has been hampered by the hardness of verification. This paper tackles the problem of retiming and resynthesis equivalence checking on a pair of circuits. For this purpose we define the Complete-$k$-Distinguishability (C-$k$-D) property for any natural number $k$ based on C-1-D. We show how the equivalence checking problem can be simplified if the circuits satisfy this property and prove that the method is complete for any number of retiming and resynthesis steps. We also provide a way to enforce C-$k$-D on the circuits without restricting the optimization power of retiming and resynthesis or increasing their complexity. Experimental results demonstrate that enforcing C-$k$-D property can speed up the verification process. |
| Title | Multi-Clock SVA Synthesis without Re-writing |
| Author | *Jiang Long, Andrew Seawright, Paparao Kavalipati (Mentor Graphics Corp., United States) |
| Page | pp. 648 - 653 |
| Keyword | SVA, Formal verification, Multi-Clock |
| Abstract | This paper presents a compilation procedure for synthesiz- ing multi-clock SVA properties for formal verification. The synthesis framework is built upon an existing compilation al- gorithm for single-clock SVA properties. While we could use the SVA rewriting rules to transform a multi-clock property into a single-clocked property and then apply existing tech- niques, instead we propose techniques to selectively model the multi-clock operators to produce a smaller checker logic. Through recursive construction and syntactic transforma- tion, we are able demonstrate the efficiency of the technique and the generated checker logic is provably equivalent to the rewriting version. |
| Title | Automatic Formal Verification of Clock Domain Crossing Signals |
| Author | *Bing Li, Chris Ka-Kei Kwok (Mentor Graphics Corporation, United States) |
| Page | pp. 654 - 659 |
| Keyword | formal verification, clock domain crossing, assertion logic |
| Abstract | In this paper, we present an approach that uses formal methods to verify Clock Domain Crossing (CDC) issues in a fully automatic way. First, we discuss various CDC schemes and the corresponding checks that need to be formally verified. Then we demonstrate how to synthesize them into assertion logic. After that a fully automatic, on-the-fly formal CDC approach is proposed. To the best of our knowledge, this is the first paper discussing fully automatic, on-the-fly formal verification of CDC signals. Experiment results show that our automatic formal CDC, when compared with the conventional post-CDC formal CDC, takes much less time, but still prove significant number of CDC checks. |
| Slides | |