---

System-Level Timing Analysis and Verification

SUPPORTED BY

SRC-2002-TJ-1024: System-Level Timing Verification With Automatic Abstraction

SRC-99-TJ-694: Timing Verification using Automatic Abstraction

SRC-97-TJ-487.001: Verification of Timed Circuits

NSF Japan Program Award INT-0087281

NSF CAREER award MIP-9625014

---

---

The goal of this research task is to develop methodology and tools to support system-level timing verification. Systems are composed of a heterogeneous collection of digital, mixed signal/analog, and software components. As a result, their state space tends to be very large. Therefore, to be practical this tool must support automatic abstraction. Our group has developed one of the most efficient timing verification tools for circuit-level analysis. This tool has been utilized by companies such as Intel and IBM for analysis of their aggressively optimized high performance circuits. Our verification tool was used during the design of several of the critical circuits in the Intel RAPPID design. Our tool has also been used to verify several circuits from the IBM guTS processor which is pictured above. Most recently, we developed automatic abstraction techniques that allowed our tool to be used to efficiently verify several variations of IBM's Synchronous Interlocked Pipelines.

The objective of this project is to extend our tools applicability to the system-level. Key to this will be developing methods for specifying properties of a system composed of heterogeneous components in a high level functional model. This model must be related formally to lower level structural descriptions so that properties of the whole system can be verified efficiently. To achieve efficient verification of such systems, techniques to automatically abstract the environment to support assume/guarantee methods must be developed. Our primary interest is in verifying timing properties of these systems. The addition of real-time complicates reachability analysis, so we will need to continue to produce even more efficient timed state space reachability analysis methods. We plan to further improve our abstraction and verification algorithms by targeting the properties that are to be verified. Finally, it is likely that exhaustive methods cannot be applied to many large systems, so we will also investigate bounded model checking techniques with our goal of finding the most bugs possible. When exhaustive methods cannot be applied, we plan to also provide coverage metrics to give the designer feedback on the quality of the verification result. In our previous research, our collaborations with industry have been essential to our success. These companies provided motivating examples for our timing verification tool that helped not only validate the utility of our tool, but also to provide future research directions. In this project, we plan to continue to use examples from industry to drive the direction of this research.

Faculty:

• Chris J. Myers
• Tomohiro Yoneda

Students:

• Scott Little
• David Walter
• Nicolas Seegmiller
• Robert Thacker

Alumni:

• Wendy Belluomini
• Eric Mercer
• Hao Zheng

Books:

• Chris J. Myers, Asynchronous Circuit Design, John Wiley & Sons, July, 2001.

PhD Theses:

• Eric Mercer, Correctness and Reduction in Timed Circuit Analysis , PhD Thesis, University of Utah, December, 2002.
• Hao Zheng, Modular Synthesis and Verification of Timed Circuits Using Automatic Abstraction, PhD Thesis, University of Utah, August, 2001. (pdf)
• Wendy Belluomini, Algorithms for Synthesis and Verification of Timed Circuits and Systems, PhD Thesis, University of Utah, September, 1999. (pdf)
• Chris J. Myers, Computer Aided Synthesis and Verification of Gate-Level Timed Circuits, PhD Thesis, Stanford University, October, 1995. (pdf)

Master's Theses:

• Eric G Mercer, Stochastic Cycle Period Analysis in Timed Circuits, MS Thesis, University of Utah, May 1999. (pdf)

Bachelor's Theses:

• S. Little, A Comparison of Timed State Space Analysis Methods, BS Thesis, University of Utah, June, 2003. (pdf)

Journal Papers:

• H. Zheng, E. Mercer, and C. Myers, Modular verification of timed circuits using automatic abstraction, in IEEE Transactions on CAD, 22(9), September, 2003. (pdf)
• B. Zhou, T. Yoneda, and C. Myers, Framework of Timed Trace Theoretic Verification Revisited, to appear in IEICE Transactions. (pdf)
• Wendy J. Belluomini and Chris J. Myers, Timed circuit verification using TEL structures, in IEEE Transactions on CAD, 20(1): 129-146, January, 2001. (pdf)
• Wendy J. Belluomini and Chris J. Myers, Timed state space exploration using POSETs, in IEEE Transactions on CAD, 19(5), May, 2000. (pdf)
• Chris J. Myers, Tom G. Rokicki, and Teresa H.-Y. Meng, POSET timing and its application to the synthesis and verification of gate-level timed cirucits, in IEEE Transactions on CAD, 18(6), June, 1999. (pdf)

Conference Papers:

• C. Myers, R. Harrison, D. Walter, N. Seegmiller, and S. Little, The case for analog circuit verification , in The Workshop on Formal Verification of Analog Circuits, April, 2005. (pdf)
• S. Little, D. Walter, N. Seegmiller, C. Myers, and T. Yoneda, Verification of analog and mixed-signal circuits using timed hybrid Petri nets, in Automated Technology for Verification and Analysis, November, 2004. (pdf)
• D. Pradubsuwun, T. Yoneda, and C. Myers, Partial order reduction for detecting safety and timing failures of timed circuits, in Automated Technology for Verification and Analysis, November, 2004. (pdf)
• H. Zheng, C. Myers, D. Walter, S. Little, and T. Yoneda, Verification of timed circuits with failure directed abstractions, in IEEE International Conference on Computer Design, October, 2003. (pdf)
• T. Kitai, Y. Oguro, T. Yoneda, E. Mercer, and C. Myers, Level oriented formal model for asynchronous circuit verification and its efficient analysis method, in 2002 Pacific Rim International Symposium on Dependable Computing, pages 210-218, November, 2002. (pdf)
• T. Yoneda, T. Kitai, and C. Myers, Automatic derivation of timing constraints by failure analyis, in Computer Aided Verification (CAV '02), July, 2002. (pdf)
• E. Mercer, C. J. Myers, T. Yoneda, and H. Zheng, Modular synthesis of timed circuits using partial orders on LPNs, in Theory and Practice of Timed Systems, TPTS '02, April, 2002. (pdf)
• B. Zhou, T. Yoneda, C. Myers, Framework of timed trace theoretic verification revisited, in The Tenth Asian Test Symposium, November, 2001. (pdf)
• H. Zheng, E. Mercer, and C. Myers, Automatic abstraction for verification of timed circuits and systems, in Computer Aided Verification (CAV), pages 182-193, July, 2001. (pdf)
• Chris Myers, Wendy Belluomini, Kip Killpack, Eric Mercer, Eric Peskin, and Hao Zheng, Timed Circuits: A New Paradigm for High-Speed Design, in 2001 Asia and South Pacific Design Automation Conference, February, 2001 (invited paper). (pdf)
• Eric G. Mercer and Chris J. Myers, Stochastic Cycle Period Analysis in Timed Circuits, in Proc. International Symposium on Circuits and Systems(ISCAS), May, 2000. (pdf)
• Wendy Belluomini, Chris J. Myers and H. Peter Hofstee Verification of Delayed Reset Domino Circuits using ATACS,'' in The Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, April, 1999. (pdf)
• Wendy Belluomini and Chris J. Myers Verification of Timed Systems using POSETs,'' in Computer Aided Verification (CAV), June, 1998. (pdf)
• Wendy Belluomini and Chris J. Myers, Efficient timing analysis algorithms for timed state space exploration, in The Third International Symposium on Advanced Research in Asynchronous Circuits and Systems, April, 1997.(pdf)
• Tom G. Rokicki and Chris J. Myers, Automatic verification of timed circuits, in Computer Aided Verification (CAV), June, 1994. (pdf)

Workshop Papers:

• E. Mercer, C. Myers, and T. Yoneda, Improved POSET timing analysis in timed Petri nets, in The Tenth Workshop on Synthesis and System Integration of MIxed Technologies (SASIMI 2001), October, 2001. (pdf)
• Hao Zheng and Chris J. Myers, Automatic Abstraction for Synthesis and Verification of Deterministic Timed Systems, in 2000 ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, December, 2000. (pdf)
• Eric G. Mercer and Chris J. Myers, Stochastic Cycle Period Analysis in Timed Circuits , in 1999 International Workshop on Logic Synthesis, July. (pdf)
• Wendy Belluomini, Chris J. Myers, and H. Peter Hofstee Verification of Delayed Reset Domino Circuits using ATACS, in 1999 ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, March, 1999. (pdf)
• Wendy Belluomini and Chris J. Myers, Timed Event/Level Structures, in 1997 ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, December, 1997. (pdf)