Time: 10:15 - 12:20 Thursday, January 22, 2009
Location: Room 413
7B-1 (Time: 10:15 - 10:40)
| Title | Dependent Latch Identification in the Reachable State Space |
| Author | Chen-Hsuan Lin, Chun-Yao Wang (National Tsing Hua University, Taiwan) |
| 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. The reason for this is that 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. With the identification of functional dependencies, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. Although much research has been devoted to exploring the functional dependencies among latches by BDD-based symbolic algorithms, this issue is still unresolved for large sequential circuits. In this work, we find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, our proposed approach detects sequential functional dependencies existing in the reachable state space only. The sequential functional dependencies can identify additional dependent latches after a specific timeframe in order to achieve additional reduction of the state space. Experimental results show that this 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) |
| Keyword | sequential equivalence checking, retiming and resynthesis, verification |
| Abstract | Performing retiming and resynthesis iteratively is a powerful way to optimize sequential circuits. In this paper we tackle the problem of verifying the equivalence of a pair of circuits, one of which has been obtained from the other by a sequence of retiming and resynthesis operations. For this purpose we extend the Complete-1-Distinguishability (C-1-D) property to C-$k$-D for any natural $k$. We show how we can simplify the equivalence checking problem, if one of the circuits satisfies this property. Our method for checking equivalence is complete for any number of retiming and resynthesis steps. Moreover, we show a way to enforce C-$k$-D to one of the circuits without restricting the optimization power of retiming and resynthesis or increasing their complexity. Our experimental results show that by enforcing the C-$k$-D property we can speed up the verification process. |
| Title | Disjunctive Transition Relation Decompositions for Multithreaded Image Computation |
| Author | Stergios Stergiou, Jawahar Jain (Fujitsu Laboratories of America, United States) |
| Keyword | formal verification, model checking, disjunctive decomposition |
| Abstract | We investigate disjunctive Transition Relation decompositions in the context of multi-threaded symbolic model checking. We propose an algorithm that generates such decompositions and an adaptive image computation algorithm which efficiently exploits the multi-threaded platform. We integrated the algorithms in VIS and tested them on the VIS benchmarks. We show that the obtained decompositions are well-balanced and the algorithm compares favorably with more traditional conjunctive image computation approaches. |
| Title | Multi-Clock SVA Synthesis without Re-writing |
| Author | Jiang Long, Andrew Seawright, Paparao Kavalipati (Mentor Graphics Corp., United States) |
| 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 Kwok (Mentor Graphics Corporation, United States) |
| 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. |
博文
没有评论:
发表评论