Ivannikov Institute for System Programming of the RAS

Methodolody and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications.


M.Chupilko, A.Kamkin, D.Vorobyev.


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.

Full text of the paper in pdf


Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering, Volume 2, 2008. pp. 25-31.

DOI: 10.15514/SYRCOSE-2008-2-17

ISBN 978-5-91474-006-8

Research Group

Software Engineering

All publications during 2008 All publications