Methodolody and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications.
In this paper we describe a methodology and experience of simulation-based verification of microprocessor units based on cycle-accurate contract specifications. Such specifications describe behavior of a unit in the form of preconditions and
postconditions of microoperations. We have successfully applied the methodology to several units of the industrial microprocessor. The experience shows that cycle-accurate contract specifications are very suitable for simulation-based verification, since, first, they represent functional requirements on a unit in comprehensible declarative form, and second, they make it possible to automatically construct test oracles which verify unit correctness.
Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering, Volume 2, 2008. pp. 25-31.