| Title | Verifying Full-Custom Multipliers by Boolean Equivalence Checking and an Arithmetic Bit Level Proof |
| Author | *Udo Krautz, Markus Wedler, Wolfgang Kunz (University Kaiserslautern, Germany), Kai Weber, Christian Jacobi, Matthias Pflanz (IBM, Germany) |
| Page | pp. 398 - 403 |
| Keyword | formal verification |
| Abstract | In this paper we describe a methodology to formally verify highly optimized multipliers. We define a multiplier description language which abstracts from low-level optimizations and which can model a wide range of common implementations at a structural and arithmetic level. The correctness of the created model is established by bit level transformations matching the model against a standard multiplication specification. The model is also translated into a gate netlist to be compared with the full-custom implementation of the multiplier by standard equivalence checking. |
| Title | A Symbolic Approach for Mixed-Signal Model Checking |
| Author | *Alexander Jesser, Lars Hedrich (University of Frankfurt a.M., Germany) |
| Page | pp. 404 - 409 |
| Keyword | Formal Verification, Model Checking, Mixed-Signal, multi terminal binary decision diagram |
| Abstract | In this paper we firstly introduce a novel symbolic model checker MScheck for mixed-signal circuits. MScheck is capable to conflate the continuous behavior, typical for analog designs, and the discrete behavior in the digital domain for formal verification. Timing information of both systems will be symbolically stored within multi terminal binary decision diagrams (MTBDDs) for the entire verification procedure. The effectiveness of our approach is demonstrated on a phase locked loop (PLL) by formal verification of the locking property. |
| Title | Faster Projection Based Methods for Circuit Level Verification |
| Author | *Chao Yan, Mark Greenstreet (University of British Columbia, Canada) |
| Page | pp. 410 - 415 |
| Keyword | Formal Verification, Reachability Analysis, ODE |
| Abstract | As VLSI fabrication technology progresses to 65nm feature sizes and smaller, transistors no longer operate as ideal switches. This motivates the verification of digital circuits using continuous models. Recently, we showed how such verification can be performed using projection based methods.However, the verification was slow, requiring nearly four CPU days to verify a nine-transistor toggle flip-flop. Here, we describe improvements to the reachability algorithms and optimizations of the software architecture. These produce a 15x reduction in computation time and significant reductions in the over-approximation errors. With these changes, the same toggle flip-flop can be verified in a few hours, making formal verification a viable alternative to circuit simulation. |
| Title | A Debug Probe for Concurrently Debugging Multiple Embedded Cores and Inter-Core Transactions in NoC-Based Systems |
| Author | Shan Tang, *Qiang Xu (The Chinese University of Hong Kong, Hong Kong) |
| Page | pp. 416 - 421 |
| Keyword | Post-silicon validation, Debug probe, Transaction, NoC |
| Abstract | Existing SoC debug techniques mainly target bus-based systems. They are not readily applicable to the emerging system that use Network-on-Chip (NoC) as on-chip communication scheme. In this paper, we present the detailed design of a novel debug probe (DP) inserted between the core under debug (CUD) and the NoC. With embedded configurable triggers, delay control and timestamping mechanism, the proposed DP is very effective for inter-core transaction analysis as well as controlling embedded cores' debug processes. Experimental results show the functionalities of the proposed DP and its area overhead. |
| Title | A Fast Two-Pass HDL Simulation with On-Demand Dump |
| Author | *Kyuho Shim (Pusan Nat'l Univ., Republic of Korea), Youngrae Cho, Namdo Kim (Samsung Electronics, Republic of Korea), Hyuncheol Baik, Kyungkuk Kim, Dusung Kim (Pusan Nat'l Univ., Republic of Korea), Jaebum Kim, Byeongun Min, Kyumyung Choi (Samsung Electronics, Republic of Korea), Maciej Ciesielski (Logic-Mill Technology LLC, United States), Seiyang Yang (Pusan Nat'l Univ., Republic of Korea) |
| Page | pp. 422 - 427 |
| Keyword | Simulation |
| Abstract | Simulation-based functional verification is characterized by two inherently conflicting targets: the signal visibility and simulation performance. Achieving a proper trade-off between these two targets is of paramount importance. Even though HDL simulators are the most widely used verification platform at the RTL and gate level, their major drawback is the low performance in verifying complex SOCs, especially when the high visibility over the design under verification is required. This paper presents a new, fast simulation method as an effective way to achieve both high simulation speed and full signal visibility. It is based on an original two-pass simulation approach. During the 1st pass, with the simulation running at full speed, a set of design states is saved periodically at predetermined checkpoints. During the 2nd pass, another simulation is performed, using any of saved checkpoints and providing 100% signal visibility for debugging. Our method differs from the traditional simulation snapshot approach in the amount and the way the design state is saved. Experimental results show significant speed-up compared to existing traditional simulation methods while maintaining 100% visibility. |