Matthias Kaiserswerth
IEEE/ACM Transactions on Networking
In an effort to fully exploit CMOS performance, custom design techniques are used extensively in commercial microprocessor design. However, given the complexity of current-generation processors and the necessity for manual designer intervention throughout the design process, proving design correctness is a major concern. In this paper we discuss Verity, a formal verification program for symbolically proving the equivalence between a high-level design specification and a MOS transistor-level implementation. Verity applies efficient logic comparison techniques which implicitly exercise the behavior for all possible input patterns. For a given register-transfer level (RTL) system model, which is commonly used in present-day methodologies, Verity validates the transistor implementation with respect to functional simulation and verification performed at the RTL level.
Matthias Kaiserswerth
IEEE/ACM Transactions on Networking
Yun Mao, Hani Jamjoom, et al.
CoNEXT 2006
Bowen Zhou, Bing Xiang, et al.
SSST 2008
Alfonso P. Cardenas, Larry F. Bowman, et al.
ACM Annual Conference 1975