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.
Abstract
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