A Multiple-Valued Logic Approach to the Design and Verification of Hardware Circuits

TL;DR

This paper introduces a multiple-valued logic (MVL) approach for digital hardware verification, providing more detailed simulation insights than traditional binary or ternary methods, and includes theoretical foundations and algorithms.

Contribution

It presents a novel MVL-based verification method with theoretical analysis and algorithms, extending beyond common ternary/quaternary approaches.

Findings

MVL simulations reveal details invisible in binary/ternary simulations

MVL-based equivalence verification can detect genuine nonequivalence

Theoretical analysis of MVL algebra and verification complexity

Abstract

We present a novel approach, which is based on multiple-valued logic (MVL), to the verification and analysis of digital hardware designs, which extends the common ternary or quaternary approaches for simulations. The simulations which are performed in the more informative MVL setting reveal details which are either invisible or harder to detect through binary or ternary simulations. In equivalence verification, detecting different behavior under MVL simulations may lead to the discovery of a genuine binary nonequivalence or to a qualitative gap between two designs. The value of a variable in a simulation may hold information about its degree of truth and its "place of birth" and "date of birth." Applications include equivalence verification, initialization, assertions generation and verification, partial control on the flow of data by prioritizing and block-oriented simulations. Much of the paper is devoted to theoretical aspects behind the MVL approach, including the reason for choosing a specific algebra for computations, and the introduction of the verification complexity of a Boolean expression. Two basic algorithms are presented.