/**CHeaderFile***************************************************************** FileName [res.h] PackageName [res] Synopsis [Combinational verification by residue arithmetic.] Description [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. ] Author [Kavita Ravi and Abelardo Pardo ] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id: res.h,v 1.22 2002/09/08 23:53:32 fabio Exp $] ******************************************************************************/ #ifndef _RES #define _RES /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "io.h" #include "ord.h" #include "ntm.h" #include "cmd.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define RES_NETWORK_APPL_KEY "Res_NetworkApplKey" /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Information for every prime used in the verification.] ******************************************************************************/ typedef struct PerPrimeInfo { int primeNumber; float cpuTime; int bddSize; bdd_node *residueDd; }PerPrimeInfo_t; /**Struct********************************************************************** Synopsis [Structure holding the information related to the residual verification.] ******************************************************************************/ typedef struct Res_ResidueInfo { char *networkName; /* Name of the circuit verified */ char *networkNameVerifiedAgainst; /* Name of the circuit verified Against*/ int numInputs; /* Number of inputs*/ int numOutputs; /* Number of outputs */ int numDirectVerifiedOutputs; float cpuDirectVerif; /* Cpu time spent in direct * verification */ int numOfPrimes; /* Number of Primes needed for the * verification */ PerPrimeInfo_t *primeInfoArray; /* Information stored per prime */ int successDirectVerification; /* Outcome of the direct verification */ int success; /* Outcome of the verification */ bdd_manager *ddManager; /* Manager required to free the residue BDDs */ }Res_ResidueInfo_t; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN int Res_NetworkResidueVerify(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify, array_t *outputOrderArray, st_table *outputNameMatch, st_table *inputNameMatch); EXTERN void Res_Init(void); EXTERN void Res_End(void); EXTERN void Res_ResidueInfoFree(Res_ResidueInfo_t *residue); EXTERN void Res_ResidueInfoFreeCallback(void *data); EXTERN Res_ResidueInfo_t * Res_NetworkReadResidueInfo(Ntk_Network_t *network); EXTERN char * Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr); EXTERN int Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr); EXTERN void Res_ResidueInfoPrint(Res_ResidueInfo_t *result); /**AutomaticEnd***************************************************************/ #endif /* _RES */