| Title | Managing Complexity in Design Debugging with Sequential Abstraction and Refinement |
| Author | *Brian Keng, Andreas Veneris (University of Toronto, Canada) |
| Page | pp. 479 - 484 |
| Keyword | debugging, diagnosis, abstraction, refinement, verification |
| Abstract | In this work, a novel abstraction and refinement technique for design debugging is presented that addresses two key components of the debugging complexity, the design size and the error trace length. Experimental results show that the proposed algorithm is able to return solutions for all instances compared to only 41% without the technique demonstrating the viability of this approach in tackling real-world debugging problems. |
| Slides |
| Title | Facilitating Unreachable Code Diagnosis and Debugging |
| Author | Hong-Zu Chou (National Taiwan University, Taiwan), *Kai-Hui Chang (Avery Design Systems, Inc., U.S.A.), Sy-Yen Kuo (National Taiwan University, Taiwan) |
| Page | pp. 485 - 490 |
| Keyword | RTL symbolic simulation, Unreachability analysis, Error diagnosis, Reachability analysis |
| Abstract | Code coverage is a popular method to find design bugs and verification loopholes. However, once a piece of code is determined to be unreachable, diagnosing the cause of the problem can be challenging: since the code is unreachable, no counterexample can be returned for debugging. Therefore, engineers need to analyze the legality of nonexistent execution paths, which can be difficult.
To address such a problem, we analyzed the cause of unreachability in several industrial designs and proposed a diagnosis technique that can explain the cause of unreachability. In addition, our method provides suggestions on how to solve the unreachability problem, which can further facilitate debugging. Our experimental results show that this technique can greatly reduce an engineer's
effort in analyzing unreachable code. |
| Slides |
| Title | Deterministic Test for the Reproduction and Detection of Board-Level Functional Failures |
| Author | Hongxia Fang (Duke University, U.S.A.), Zhiyuan Wang, Xinli Gu (Cisco Systems Inc., U.S.A.), *Krishnendu Chakrabarty (Duke University, U.S.A.) |
| Page | pp. 491 - 496 |
| Keyword | á-coverage, board-level diagnosis, functional failure, functional scan, functional state space |
| Abstract | A common scenario in industry today is "No Trouble Found" (NTF) due to functional failures. A component on a board fails during board-level functional test, but it passes the Automatic Test Equipment (ATE) test when it is returned to the supplier for warranty replacement or service repair. To find the root cause of NTF, we propose an innovative functional test approach and DFT methods for the detection of boardlevel functional failures. These DFT and test methods allow us to reproduce and detect functional failures in a controlled deterministic environment, which can provide ATE tests to the supplier for early screening of defective parts. Experiments on an industry design show that functional scan test with appropriate functional constraints can adequately mimic the functional state space well (measured by appropriate coverage metrics). Experiments also show that most functional failures due to stuck-at, dominant bridging, and crosstalk faults can be reproduced and detected by functional scan test. |
| Title | Equivalence Checking of Scheduling with Speculative Code Transformations in High-Level Synthesis |
| Author | *Chi-Hui Lee, Che-Hua Shih, Juinn-Dar Huang, Jing-Yang Jou (National Chiao Tung University, Taiwan) |
| Page | pp. 497 - 502 |
| Keyword | equivalence checking, formal verification, finite state machine with datapath (FSMD), high-level synthesis (HLS), scheduling |
| Abstract | This paper presents a formal method for equivalence checking between the descriptions before and after scheduling in high-level synthesis (HLS). Both descriptions are represented by finite state machine with datapaths (FSMDs) and are then characterized through finite sets of paths. The main target of our proposed method is to verify scheduling employing code transformations - such as speculation and common subexpression extraction (CSE), across basic block (BB) boundaries - which have not been properly addressed in the past. Nevertheless, our method can verify typical BB-based and path-based scheduling as well. The experimental results demonstrate that the proposed method can indeed outperform an existing state-of-the-art equivalence checking algorithm. |