A Unified Formal Framework for Analyzing Functional and Speed-path Properties

O. Olivo, S. Ray, J. Bhadra, and V. Vedula

In M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 12th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2011), Austin, TX, December 2011, pages 44-45. IEEE Computer Society.

© 2012 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


We develop a formal tool for speed-path analysis and debug. We encode speed-path requirements in a formal hardware description language providing the semantics of both the functional behavior and timing constraints, and the disciplined use of an SMT solver to analyze speed-path requirements. We are applying our framework for speed-path analysis of several RTL designs from Opencores.

Relevant files