The res package
Combinational verification by residue arithmetic.
By Kavita Ravi and
Abelardo Pardo
This package implements residue verification between two
networks. The method used is based on residue arithmetic and the
Chinese Remainder theorem. Verification is performed by interpreting
the outputs of the circuits as integers and verifying the residues
of the outputs with respect to a set of moduli. The choice of moduli
is directed by the Chinese Remainder Theorem in order to prove
equivalence of the two circuits. This method works well with
multipliers and possibly other arithmetic circuits (due to its
dependence on residue arithmetic). Discretion should be exercised
in applying this method to general combinational circuits. Residue
verification is provided with vis-cu ONLY. It reads both blif and
blif-mv files. However, it does NOT support multi-valued
variables. Residue verification is primarily for combinational
verification, but may be applied to sequential circuits with the
same state encoding. The latch outputs are then considered to be
combinational inputs of the circuits and the latch inputs and reset
are considered to be combinational outputs of the circuits. This
package provides some combinational verification also. Some/all of
the outputs of the circuit may be verified directly (without using
residues). In using both direct and residue verification,
verification of arithmetic circuits may become easier.
Last updated on 20050519 00h50