High-Level vs. RTL Combinational Equivalence: An Introduction

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?