/**CHeaderFile***************************************************************** FileName [resInt.h] PackageName [res] Synopsis [Internal declarations of the residue package.] 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: resInt.h,v 1.31 2002/09/08 23:55:58 fabio Exp $] ******************************************************************************/ #ifndef _RESINT #define _RESINT /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include #include #include #include "res.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define RES_NOT_VERIFIED -1 /* constant to indicate verification not taken * place */ #define RES_PASS 1 /* constant to indicate verification success */ #define RES_FAIL 0 /* constant to indicate verification failure */ #define ResDefaultComposeMethod_c ResVector_c #define ResDefaultScheduleLayerMethod_c ResLayerAlap_c #define IMMEDIATE_FANIN 1 /* Static flag to indicate that the BDD/MDD has to * be built in terms of immediate fanin */ #define PRIMARY_INPUTS 2 /* Static flag to indicate PIs * used to indicate that the BDD/MDD has to be * built in terms of primary inputs * also used to flag the building of input * match tables */ #define PRIMARY_OUTPUTS 3 /* Static flag to indicate PIs * also used to flag the building of input * match tables */ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /**Enum************************************************************************ Synopsis [Different methods to compute the layers for functional compositions.] SeeAlso [ResComputeCompositionLayers] ******************************************************************************/ typedef enum { ResLayerAsap_c, ResLayerAlap_c } ResLayerScheduleMethod; /**Enum************************************************************************ Synopsis [Different composition methods.] SeeAlso [ComposeLayersIntoResidue] ******************************************************************************/ typedef enum { ResVector_c, /* Compose when fanout gates have been composed */ ResOneGateAtATime_c, /* Compose one gate at a time */ ResPreimageComputation_c, /* Treat the compositions like * partitioned transition relation */ ResSuperG_c /* new cudd vector compose that creates a super G */ } ResCompositionMethod; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /* variables to measure times of different components of residue verification*/ extern long Res_composeTime; extern long Res_shuffleTime; extern long Res_smartVarTime; extern long Res_orderTime; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Macro to fetch the i-th layer in the layer Array.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResLayerFetchIthLayer(layerArray, i) \ array_fetch(array_t *, layerArray, i) /**Macro*********************************************************************** Synopsis [Macro to determine number of nodes in current layer] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResLayerNumNodes(layer) \ array_n(layer) /**Macro*********************************************************************** Synopsis [Iterate through each node in a layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerForEachNode(layer, i, nodePtr) \ arrayForEachItem(Ntk_Node_t *, layer, i, nodePtr) /**Macro*********************************************************************** Synopsis [Add node in the i-th position in the layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerAddNodeAtIthPosition(layer, i, nodePtr) \ array_insert(Ntk_Node_t *, layer, i, nodePtr) /**Macro*********************************************************************** Synopsis [Add node at the end of the layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerAddNodeAtEnd(layer, nodePtr) \ array_insert_last(Ntk_Node_t *, layer, nodePtr) /**Macro*********************************************************************** Synopsis [Fetch the i-th node in the layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerFetchIthNode(layer, i) \ array_fetch(Ntk_Node_t *, layer, i) /**Macro*********************************************************************** Synopsis [Sort the layer nodes according to the given function.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerSort(layer, func) \ array_sort(layer, func) /**Macro*********************************************************************** Synopsis [Free current layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerFree(layer) \ array_free(layer) /**Macro*********************************************************************** Synopsis [Create an empty layer.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define LayerCreateEmptyLayer() \ array_alloc(Ntk_Node_t *, 0) /**Macro*********************************************************************** Synopsis [Macro to read the network name field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNetworkName(rPtr) \ (rPtr)->networkName /**Macro*********************************************************************** Synopsis [Macro to read the name of the circuit that has been verified against.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNameVerifiedAgainst(rPtr) \ (rPtr)->networkNameVerifiedAgainst /**Macro*********************************************************************** Synopsis [Macro to set the name filed of Res_ResidueInfo] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNetworkName(rPtr, value) \ (rPtr)->networkName = (value) /**Macro*********************************************************************** Synopsis [Macro to set the name field of the circuit that this one has been verified against.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNameVerifiedAgainst(rPtr, value) \ (rPtr)->networkNameVerifiedAgainst = (value) /**Macro*********************************************************************** Synopsis [Macro to read the numInputs field of Res_ResidueInfo] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNumInputs(rPtr) \ (rPtr)->numInputs /**Macro*********************************************************************** Synopsis [Macro to set the numInputs field of Res_ResidueInfo] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNumInputs(rPtr, value) \ (rPtr)->numInputs = (value) /**Macro*********************************************************************** Synopsis [Macro to read the numOutputs field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNumOutputs(rPtr) \ (rPtr)->numOutputs /**Macro*********************************************************************** Synopsis [Macro to set the numOutputs field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNumOutputs(rPtr, value) \ (rPtr)->numOutputs = (value) /**Macro*********************************************************************** Synopsis [Macro to read the numDirectVerifiedOutputs field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNumDirectVerifiedOutputs(rPtr) \ (rPtr)->numDirectVerifiedOutputs /**Macro*********************************************************************** Synopsis [Macro to set the numDirectVerifiedOutputs field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNumDirectVerifiedOutputs(rPtr, value) \ (rPtr)->numDirectVerifiedOutputs = (value) /**Macro*********************************************************************** Synopsis [Macro to read the cpuDirectVerif field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadCpuDirectVerif(rPtr) \ (rPtr)->cpuDirectVerif /**Macro*********************************************************************** Synopsis [Macro to set the cpuDirectVerif field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetCpuDirectVerif(rPtr, value) \ (rPtr)->cpuDirectVerif = (value) /**Macro*********************************************************************** Synopsis [Macro to read the numOfPrimes field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadNumOfPrimes(rPtr) \ (rPtr)->numOfPrimes /**Macro*********************************************************************** Synopsis [Macro to set the numOfPrimes field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetNumOfPrimes(rPtr, value) \ (rPtr)->numOfPrimes = (value) /**Macro*********************************************************************** Synopsis [Macro to read the success field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadSuccess(rPtr) \ ((Res_ResidueInfo_t *)rPtr)->success /**Macro*********************************************************************** Synopsis [Macro to read the direct verification success field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadDirectVerificationSuccess(rPtr) \ (rPtr)->successDirectVerification /**Macro*********************************************************************** Synopsis [Macro to read the success field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResNetworkReadResidueInfo(network) \ (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network,RES_NETWORK_APPL_KEY); /**Macro*********************************************************************** Synopsis [Macro to set the success field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetSuccess(rPtr, value) \ ((Res_ResidueInfo_t *)rPtr)->success = (value) /**Macro*********************************************************************** Synopsis [Macro to set the direct verification success field of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetDirectVerificationSuccess(rPtr, value) \ ((Res_ResidueInfo_t *)rPtr)->successDirectVerification = (value) /**Macro*********************************************************************** Synopsis [Macro to read one entry of the PerPrimeInfo array of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoReadPerPrimeInfo(rPtr, i) \ (&((rPtr)->primeInfoArray[(i)])) /**Macro*********************************************************************** Synopsis [Macro to set one entry of the PerPrimeInfo array of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetPerPrimeInfo(rPtr, idx, num, time, size, dd) \ ((rPtr)->primeInfoArray)[(idx)].primeNumber = (num); \ ((rPtr)->primeInfoArray)[(idx)].cpuTime = (time); \ ((rPtr)->primeInfoArray)[(idx)].bddSize = (size); \ ((rPtr)->primeInfoArray)[(idx)].residueDd = (dd) /**Macro*********************************************************************** Synopsis [Macro to set DdNodeof the entry of the PerPrimeInfo array of Res_ResidueInfo.] SideEffects [] SeeAlso [Res_ResidueInfo] ******************************************************************************/ #define ResResidueInfoSetPerPrimeDd(rPtr, idx, dd) \ ((rPtr)->primeInfoArray)[(idx)].residueDd = (dd) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN bdd_node * BuildBDDforNode(Ntk_Network_t *network, Ntk_Node_t *nodePtr, int fanin); EXTERN bdd_node * ComposeLayersIntoResidue(Ntk_Network_t *network, array_t *layerArray, bdd_node *residueDd, array_t *outputArray); EXTERN array_t * ResComputeCompositionLayers(Ntk_Network_t *network, array_t *outputArray, array_t *ignoreArray); EXTERN void ResLayerPrintInfo(Ntk_Network_t *network, array_t *layerArray); EXTERN void ResLayerArrayFree(array_t *layerArray); EXTERN Res_ResidueInfo_t * ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network); EXTERN Res_ResidueInfo_t * ResResidueInfoAllocate(char *name); EXTERN void ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo, int numOfPrimes, int *tableOfPrimes); EXTERN void MddCreateVariables(mdd_manager *mgr, int numVarsToBeAdded); EXTERN int * ResResidueVarAllocate(bdd_manager *ddManager, lsList orderList, array_t *newIdArray); EXTERN void ResResidueVarDeallocate(array_t *currentLayer); EXTERN void ResResidueFreeVariableManager(void); EXTERN void ResResidueInitializeVariableManager(int numOfVars); EXTERN int * ResResidueVarUseAllocate(int howManyVars, boolean recicleVarIds, int consecutive); EXTERN void ResResidueVarUseDeallocate(int *varPool, int size); EXTERN int ResResidueVarHighestIndex(void); /**AutomaticEnd***************************************************************/ #endif /* _RESINT */