Automatic Formal Correspondence Checking of ISA and RTL Microprocessor 
Description

The paper proposes an automated approach with
a formal basis designed for checking correspondence between
an RTL implementation of a microprocessor and a description of
its instruction set architecture (ISA). The goals of the approach
are to find bugs not discovered by functional verification, to
minimize user intervention in the verification process, and to
provide a developer with practical results within a short period
of time. The main idea is to use bounded model checking to check
that the output produced by automatically derived RTL and ISA
models of a given processor are the same for each instruction and
each possible input. Although the approach does not provide full
formal verification, experiments with the approach confirm that
due to a different way it explores the state space of the design
under test, it can find bugs not found by functional verification,
and is thus a useful complement to functional verification.