Several emerging Design-for-Debug (DFD) methodologies are addressing silicon debug by making internal signal values and other data observable. Most of these methodologies require the instrumentation of on-chip logic for extracting the internal register data from in situ silicon. Unfortunately, lack of visibility of the combinational network values impedes the ability to functionally debug the silicon part. Visibility enhancement techniques enable the virtual observation of combinational nodes with minimal computational overhead. These techniques also cover the register selection analysis for DFD and multi-level design abstraction correlation for viewing values at the register transfer level (RTL). Experimental results show that visibility enhancement techniques can leverage a small amount of extracted data to provide a high amount of computed combinational signal data. Visibility enhancement provides the needed connection between data obtained from the DFD logic and HDL simulation-related debug systems.

Verification of gate-level implementations of arithmetic circuits is challenging for a number of reasons: the existence of some hard-to-verify arithmetic operators, the use of different operand ordering, the incorporation of merged arithmetic with cross-operator implementations, and the employment of circuit transformations based on arithmetic relations. It is hence a peculiar problem that does not fit well within the existing register-transfer-level-to-gate equivalence-checking methodology. We propose a self-referential functional verification approach which uses the gate-level implementation of the arithmetic circuit under verification to verify itself. The verification task is decomposed into a sequence of equivalence-checking subproblems, each of which compares structurally similar circuit pairs derived from the implementation under verification. These equivalence-checking subproblems represent the functional equations that uniquely define the intended arithmetic function. Based on these self-referential functional equations, a decomposition heuristic using structural information is employed to guide the verification process for better efficiency. Experimental results on a number of implementations of the multipliers, the multiply-add units, and the inner product units with different architectures demonstrate the versatility of this approach.

Verification of gate-level implementations of arithmetic circuits is challenging due to a number of reasons: the existence of some hard-to-verify arithmetic operators (e.g. multiplication), the use of different operand ordering, the incorporation of merged arithmetic with cross-operator implementations, and the employment of circuit transformations based on arithmetic relations. It is hence a peculiar problem that does not fit quite well into the existing RTL-to-gate equivalence checking methodology. In this paper, we propose a self-referential functional verification approach which uses the gate-level implementation of the arithmetic circuit under verification to verify itself. Specifically, the verification task is decomposed into a sequence of equivalence checking subproblems, each of which compare circuit pairs derived from the implementation under verification based on the proposed self-referential functional equations. A decomposition-based heuristic using structural information is employed to guide the verification process for better efficiency. Experimental results on a number of implementations of the multiply-add units and the inner product units with different architectures demonstrate the versatility of this approach.

We propose a method based on unrolling the inductive definition of binary number multiplication to verify gate-level implementations of multipliers. The induction steps successively reduce the size of the multiplier under verification. Through induction, the verification of an n-bit multiplier is decomposed into n equivalence checking problems. The resulting equivalence checking problems could be significantly sped up by simple structural analysis. This method could be generalized to the verification of more general arithmetic circuits and the equivalence checking of complex datapaths.