High-Level vs. RTL Combinational Equivalence:  An Introduction

Alan J. Hu

IEEE International Conference on Computer Design, 2006.

With increasing use of higher-than-RTL specifications as the starting
point of designs, a pressing need has emerged for equivalence
verification between a high-level (e.g., non-synthesizable software)
model and RTL.  Other papers in this invited session discuss techniques
for dealing with the sequential aspects of this problem.  This paper
presents an introduction to the main ideas for the combinational
aspect:  assuming we are given two combinational descriptions, one
high-level and one RTL, how do we automatically and efficiently verify
equivalence?