| Title | A Complete Approach to Unreachable State Diagnosability via Property Directed Reachability |
| Author | *Ryan Berryhill, Andreas Veneris (University of Toronto, Canada) |
| Page | pp. 127 - 132 |
| Keyword | diagnosis, debugging, reachability, pdr, ic3 |
| Abstract | In modern hardware design, substantial manual
effort is required to fix a design when verification discovers a
state unreachable. This paper addresses this growing pain where
given an unreachable target state, a methodology is presented to
return all design locations where a change can be implemented
to make the target state reachable. In contrast to previous state
reachability rectification techniques that use bounded model
checking, our approach addresses the issue using unbounded
model checking. It first enhances the circuit transition relation
by inserting a novel error model construction at each suspect
location. An unbounded model checking algorithm is then applied
to the enhanced transition relation to find which of the suspect
locations can be changed to make the target state reachable.
The use of unbounded model checking allows it to identify the
complete solution set of the problem. As an added benefit, it also
returns a proof that no further solution(s) exist in the form of
an inductive invariant. Empirical results on industrial designs
confirm the theoretical and practical gains of this approach. |
| Slides |
| Title | Formally Analyzing Fault Tolerance in Datapath Designs using Equivalence Checking |
| Author | Payman Behnam (University of Tehran, Iran), Bijan Alizadeh (University of Tehran, and IPM, Iran), Sajjad Taheri (University of Tehran, Iran), *Masahiro Fujita (University of Tokyo, Japan) |
| Page | pp. 133 - 138 |
| Keyword | Formal Verification, Equivalence checking, Fault tolerance, Decision Diagrams |
| Abstract | In this paper, we present an efficient formal approach to check the equivalence of synthesized Register Transfer Level (RTL) against the high level specification in the presence of pipelining transformations. With the proposed equivalence checking method, fault tolerance issues when some faults happen in the designs can be formally analyzed. Equivalence checking with the specification can reason about how quickly the design can come back to normal operations when some faults including soft errors happen. To increase the scalability of our proposed method, we dynamically divide the designs into several smaller parts called segments by introducing dynamic cut-points. Then we employ Modular Horner Expansion Diagram (M-HED) to check whether the specification and the implementation are equivalent or not. Our proposed method enables us to deal with the equivalence checking problem for behaviorally synthesized designs even in the presence of pipelines for nested loops. The empirical results demonstrate the efficiency and scalability of our proposed method in terms of run-time and memory usage for several large designs synthesized by a commercial behavioral synthesis tool. Average improvements in terms of the memory usage and run time in comparison with SMT- and SAT-based equivalence checking are 16.7× and 111.9×, respectively. |
| Title | Coupling Reverse Engineering and SAT to Tackle NP-Complete Arithmetic Circuitry Verification in ~O(# of gates) |
| Author | *Yi Diao, Xing Wei (Easy-Logic Technology Limited, Hong Kong), Tak.Kei Lam (The Chinese University of Hong Kong, Hong Kong), Yu.Liang Wu (Easy-Logic Technology Limited, Hong Kong) |
| Page | pp. 139 - 146 |
| Keyword | SAT, Multiplier, Arithmetic logic, Macro, Formal verification |
| Abstract | There are situations (e.g. for reverse engineering or formal verification) circuit designers would need to extract complicated arithmetic circuitry deeply embedded inside a fully synthesized (or manually touched) million-gate flattened netlist without the knowing of module boundary and IO positions. Besides not knowing the IO and boundary, a formal verification task like comparing two netlists implementing (4A+3B)×C and 4A×C+3B×C respectively is quite challenging for it is an NP-Complete Circuit-SAT problem too. To tackle this problem, we propose a novel Complementary Greedy Coupling (CGC) approach coupling reverse engineering and SAT techniques together for each of them only performs well at proving equality or inequality respectively. The scheme is quite powerful, being able to handle commonly implemented arithmetic modules (Ripple/CLA adders, MUX, various multipliers and their combinations) with runtime complexity nearly linear to the number of circuit gates. For an example, our scheme can verify two 32-bit multipliers (Wallace vs Modified-Booth) within 5 seconds (regardless of their equality or inequality), while running SAT alone might take 1010 centuries. We compared our tool Easy-LEC with the two on market commercial tools using the 182 open benchmarks posted for ICCAD CAD Contest 2014. Besides running at least 400 to 1400 times faster, our scheme also solves 32% to 45% more cases (93% vs 61% or 48%). |
| Slides |