|
|
Session 5A: Techniques for Formal and Simulation-Based Verification
5A-1 (Time: 13:30 - 13:55)
| Title |
Verifying Full-Custom Multipliers by Boolean Equivalence Checking and an Arithmetic Bit Level Proof |
| Author |
*Udo Krautz, Markus Wedler, Wolfgang Kunz (Univ. Kaiserslautern, Germany), Kai Weber, Christian Jacobi, Matthias Pflanz (IBM, Germany) |
| 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. |
| PDF file |
5A-2 (Time: 13:55 - 14:20)
| Title |
A Symbolic Approach for Mixed-Signal Model Checking |
| Author |
*Alexander Jesser, Lars Hedrich (Univ. of Frankfurt a.M., Germany) |
| 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. |
| PDF file |
5A-3 (Time: 14:20 - 14:45)
| Title |
Faster Projection Based Methods for Circuit Level Verification/B> |
| Author |
*Chao Yan, Mark Greenstreet (Univ. of British Columbia, Canada) |
| 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. |
| PDF file |
5A-4 (Time: 14:45 - 15:10)
| 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 Univ. of Hong Kong, Hong Kong) |
| 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. |
| PDF file |
5A-5 (Time: 15:10 - 15:23)
| Title |
A Fast Two-Pass HDL Simulation with On-Demand Dump |
| Author |
*Kyuho Shim (Pusan Nat'l Univ., Korea), Youngrae Cho, Namdo Kim (Samsung Electronics, Korea), Hyuncheol Baik, Kyungkuk Kim, Dusung Kim (Pusan Nat'l Univ., Korea), Jaebum Kim, Byeongun Min, Kyumyung Choi (Samsung Electronics, Korea), Maciej Ciesielski (Logic-Mill Technology LLC, USA), Seiyang Yang (Pusan Nat'l Univ., Korea) |
| 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. |
| PDF file |
Last Updated on: January 31, 2008
|
|
