  Traditional logical equivalence checking (LEC) which plays a major role in
entire chip design process faces challenges of meeting the requirements
demanded by the many emerging technologies that are based on logic models
different from standard complementary metal oxide semiconductor (CMOS). In this
paper, we propose a LEC framework to be employed in the verification process of
beyond-CMOS circuits. Our LEC framework is compatible with existing CMOS
technologies, but, also able to check features and capabilities that are unique
to beyond-CMOS technologies. For instance, the performance of some emerging
technologies benefits from ultra-deep pipelining and verification of such
circuits requires new models and algorithms. We, therefore, present the
Multi-Cycle Input Dependency (MCID) circuit model which is a novel model
representation of design to explicitly capture the dependency of primary
outputs of the circuit on sequences of internal signals and inputs. Embedding
the proposed circuit model and several structural checking modules, the process
of verification can be independent of the underlying technology and signaling.
We benchmark the proposed framework on post-synthesis rapid single-flux-quantum
(RSFQ) netlists. Results show a comparative verification time of RSFQ circuit
benchmark including 32-bit Kogge-Stone adder, 16-bit integer divider, and
ISCAS'85 circuits with respect to ABC tool for similar CMOS circuits.
