 |
 |
 |
 |
 |
 |
 |
|
|
|
| WEDNESDAY, June 15, 2005, 2:00 PM - 4:00 PM | Room: 210AB | ||
|
TOPIC AREA: SYSTEM-LEVEL DESIGN AND VERIFICATION (tools) | ||
| SESSION 28 | |||
| Effective Formal Verification Using Word-level Reasoning, Bit-level Generality, and Parallelism | |||
| Chair: Howard Wong-Toi - Jasper Design Automation, Mountain View, CA | |||
| Organizers: Adnan Aziz, Pei-Hsin Ho | |||
| The papers in this session address the challenges of formally verifying real-world designs. The first two papers exploit designer intent inferred from the RT-level description. The third paper uses bit-level arithmetic to reduce the complexity of SAT-based BMC. The fourth paper presents a new low-cost approach to sequential redundancy removal. The final paper leverages parallelism to speed-up BDD-based reachability analysis. | |||
 28.1 |
Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog |
||
| Speaker(s): | Himanshu Jain - Carnegie Mellon Univ., Pittsburgh, PA | ||
| Author(s): | Himanshu Jain - Carnegie Mellon Univ., Pittsburgh, PA Daniel Kroening - ETH Zurich, Zuerich, Switzerland Natasha Sharygina - Carnegie Mellon Univ., Pittsburgh, PA Edmund M. Clarke - Carnegie Mellon Univ., Pittsburgh, PA | ||
| 28.2 | Structural Search for RTL with Predicate Learning | ||
| Speaker(s): | Ganapathy Parthasarathy - Univ. of California, Santa Barbara, CA | ||
| Author(s): | Ganapathy Parthasarathy - Univ. of California, Santa Barbara, CA Madhu K Iyer - Univ. of California, Santa Barbara, CA Kwang-Ting Cheng - Univ. of California, Santa Barbara, CA Forrest Brewer - Univ. of California, Santa Barbara, CA | ||
| 28.3 | Normalization at the Arithmetic Bit Level | ||
| Speaker(s): | Markus Wedler - Univ. of Kaiserslautern, Kaiserslautern, Germany | ||
| Author(s): | Markus Wedler - Univ. of Kaiserslautern, Kaiserslautern, Germany Dominik Stoffel - Univ. of Kaiserslautern, Kaiserslautern, Germany Wolfgang Kunz - Univ. of Kaiserslautern, Kaiserslautern, Germany | ||
| 28.4s | Exploiting Suspected Redundancy Without Proving It | ||
| Speaker(s): | Hari Mony - IBM Corp., Austin, TX | ||
| Author(s): | Hari Mony - IBM Corp., Austin, TX Jason R. Baumgartner - IBM Corp., Austin, TX Viresh Paruthi - IBM Corp., Austin, TX Robert L. Kanzelman - IBM Corp., Rochester, NY | ||
| 28.5s | Multi-threaded Reachability | ||
| Speaker(s): | Debashis Sahoo - Stanford Univ., Stanford, CA | ||
| Author(s): | Debashis Sahoo - Stanford Univ., Stanford, CA Jawahar Jain - Fujitsu Labs. Ltd., Sunnyvale, CA Subramanian K. Iyer - Univ. of Texas, Austin, TX David L. Dill - Stanford Univ., Stanford, CA Allen E. Emerson - Univ. of Texas, Austin, TX | ||
 | |||