TY - GEN
T1 - Directed-logical testing for functional verification of microprocessors
AU - Katelman, Michael
AU - Meseguer, José
AU - Escobar, Santiago
PY - 2008
Y1 - 2008
N2 - The length of the microprocessor development cycle is largely determined by functional verification, where contemporary practice relies primarily on constraint-based random stimulus generation to drive a simulation-based methodology. However, formal methods are, in particular, gaining wider adoption and are seen as having potential to bridge large gaps left by current techniques. And many gaps still remain. In this paper we propose directed-logical testing: a new method of stimulus generation based on purely logical techniques (i.e. formal methods). As far as we know, our methodology represents the first endto-end mathematical formalization of the stimulus generation problem. Therefore, a major contribution of this paper is the definition of a class of logical propositions that relate the actual microprocessor implementation, the assembly program stimulus, and a coverage goal. These propositions are given in rewriting logic, and use the idea of rewriting semantics to automatically formalize within a common logical framework the microprocessor implementation and assembly programs. To solve these propositions, we demonstrate how narrowing and user-defined narrowing strategies can be used as a scalable logical framework. In addition, we describe two classes of effective strategies that can be used for many microprocessors and common coverage goals. Finally, we describe a prototype tool implementation and present empirical data to demonstrate the feasibility of our methodology. Since narrowing and user-defined narrowing strategies within rewriting logic do not yet have tool support, our prototype tool uses standard rewriting and user-defined rewriting strategies to simulate narrowing.
AB - The length of the microprocessor development cycle is largely determined by functional verification, where contemporary practice relies primarily on constraint-based random stimulus generation to drive a simulation-based methodology. However, formal methods are, in particular, gaining wider adoption and are seen as having potential to bridge large gaps left by current techniques. And many gaps still remain. In this paper we propose directed-logical testing: a new method of stimulus generation based on purely logical techniques (i.e. formal methods). As far as we know, our methodology represents the first endto-end mathematical formalization of the stimulus generation problem. Therefore, a major contribution of this paper is the definition of a class of logical propositions that relate the actual microprocessor implementation, the assembly program stimulus, and a coverage goal. These propositions are given in rewriting logic, and use the idea of rewriting semantics to automatically formalize within a common logical framework the microprocessor implementation and assembly programs. To solve these propositions, we demonstrate how narrowing and user-defined narrowing strategies can be used as a scalable logical framework. In addition, we describe two classes of effective strategies that can be used for many microprocessors and common coverage goals. Finally, we describe a prototype tool implementation and present empirical data to demonstrate the feasibility of our methodology. Since narrowing and user-defined narrowing strategies within rewriting logic do not yet have tool support, our prototype tool uses standard rewriting and user-defined rewriting strategies to simulate narrowing.
UR - http://www.scopus.com/inward/record.url?scp=51349119593&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=51349119593&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2008.4547694
DO - 10.1109/MEMCOD.2008.4547694
M3 - Conference contribution
AN - SCOPUS:51349119593
SN - 9781424424177
T3 - Proceedings - 6th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'08
SP - 89
EP - 99
BT - Proceedings - 6th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'08
T2 - 6th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'08
Y2 - 5 June 2008 through 7 June 2008
ER -