/**CFile*********************************************************************** FileName [resRes.c] PackageName [res] Synopsis [Data manipulation routines of the Res_ResidueInfo structure.] SeeAlso [Res_ResidueInfo] 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.] ******************************************************************************/ #include "resInt.h" static char rcsid[] UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Frees the structure storing the information related to the residual verification.] SideEffects [] SeeAlso [Res_ResidualInfo] ******************************************************************************/ void Res_ResidueInfoFree(Res_ResidueInfo_t *residue) { int i; /* Deallocate the information in the primeInfoArray, if any */ if (residue->primeInfoArray != NIL(PerPrimeInfo_t)) { for (i = 0; i < residue->numOfPrimes; i++) { if ((residue->primeInfoArray[i]).residueDd != NIL(bdd_node)) { bdd_recursive_deref(residue->ddManager, (residue->primeInfoArray[i]).residueDd); } } FREE(residue->primeInfoArray); } /* End of if */ FREE(residue->networkName); FREE(residue->networkNameVerifiedAgainst); FREE(residue); return; } /* End of Res_ResidueInfoFree */ /**Function******************************************************************** Synopsis [Call-back function to free the residue information.] Description [A pointer to this function will be stored in the network together with the pointer to the structure. Whenever the network needs to deallocate the residue information this function is called.] SideEffects [] SeeAlso [Ntk_NetworkAddApplInfo] ******************************************************************************/ void Res_ResidueInfoFreeCallback(void *data) { Res_ResidueInfoFree((Res_ResidueInfo_t *) data); ResResidueFreeVariableManager(); } /* End of Res_ResidueInfoFreeCallback */ /**Function******************************************************************** Synopsis [Reads the residue information attached to a network.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ Res_ResidueInfo_t * Res_NetworkReadResidueInfo(Ntk_Network_t *network) { return (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY); } /* End of Res_NetworkReadResidueInfo */ /**Function******************************************************************** Synopsis [External function to read the name field of Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ char * Res_ResidueInfoReadName(Res_ResidueInfo_t *residuePtr) { return (char *)(ResResidueInfoReadNetworkName(residuePtr)); } /* End of Res_ResidueInfoReadName */ /**Function******************************************************************** Synopsis [External function to read the number of inputs in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadNumInputs(Res_ResidueInfo_t *residuePtr) { return ResResidueInfoReadNumInputs(residuePtr); } /* End of Res_ResidueInfoReadNumInputs */ /**Function******************************************************************** Synopsis [External function to read the number of outputs in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadNumOutputs(Res_ResidueInfo_t *residuePtr) { return ResResidueInfoReadNumOutputs(residuePtr); } /* End of Res_ResidueInfoReadNumOutputs */ /**Function******************************************************************** Synopsis [External function to read the number of directly verified outputs in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadNumDirectVerifiedOutputs(Res_ResidueInfo_t *residuePtr) { return ResResidueInfoReadNumDirectVerifiedOutputs(residuePtr); } /* End of Res_ResidueInfoReadNumDirectVerifiedOutputs */ /**Function******************************************************************** Synopsis [External function to read the cpu seconds spent in directly verifying outputs in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadCpuDirectVerif(Res_ResidueInfo_t *residuePtr) { return (int) ResResidueInfoReadCpuDirectVerif(residuePtr); } /* End of Res_ResidueInfoReadCpuDirectVerif */ /**Function******************************************************************** Synopsis [External function to read the number of primes in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadNumOfPrimes(Res_ResidueInfo_t *residuePtr) { return ResResidueInfoReadNumOfPrimes(residuePtr); } /* End of Res_ResidueInfoReadNumOfPrimes */ /**Function******************************************************************** Synopsis [External function to read the success field in Res_ResidueInfo.] SideEffects [] SeeAlso [CommandResVerify] ******************************************************************************/ int Res_ResidueInfoReadSuccess(Res_ResidueInfo_t *residuePtr) { return ResResidueInfoReadSuccess(residuePtr); } /* End of Res_ResidueInfoReadNumOfPrimes */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Wrapper procedure to create a result data structure.] SideEffects [] ******************************************************************************/ Res_ResidueInfo_t * ResNetworkResidueInfoReadOrCreate(Ntk_Network_t *network) { Res_ResidueInfo_t *result; assert(network != NIL(Ntk_Network_t)); result = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY); if (result == NIL(Res_ResidueInfo_t)) { result = ResResidueInfoAllocate(Ntk_NetworkReadName(network)); result->ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network); } /* End of if */ return result; } /* End of ResNetworkResidueInfoReadOrCreate*/ /**Function******************************************************************** Synopsis [Function that allocates the Res_ResidueInfo_t.] Description [Only the name field is initialized. The field primeInfoArray it is initialized to NIL. In a later phase, that field may be initialized with the array of the correct size by means of Res_ResidueAllocatePrimeInfo.] SideEffects [] SeeAlso [ResResidueAllocatePrimeInfo] ******************************************************************************/ Res_ResidueInfo_t * ResResidueInfoAllocate(char *name) { Res_ResidueInfo_t *result = ALLOC(Res_ResidueInfo_t, 1); result->networkName = util_strsav(name); result->networkNameVerifiedAgainst = NULL; result->numInputs = 0; result->numOutputs = 0; result->numDirectVerifiedOutputs = 0; result->cpuDirectVerif = 0.0; result->numOfPrimes = 0; result->primeInfoArray = NIL(PerPrimeInfo_t); result->success = RES_NOT_VERIFIED; result->successDirectVerification = RES_NOT_VERIFIED; result->ddManager = NIL(bdd_manager); return result; } /* End of ResResidueInfoAllocate */ /**Function******************************************************************** Synopsis [Allocates the array primeInfoArray inside the Res_ResidueInfo_t.] SideEffects [] SeeAlso [Res_ResidueAllocate] ******************************************************************************/ void ResResidueInfoAllocatePrimeInfoArray(Res_ResidueInfo_t *residueInfo, int numOfPrimes, int *tableOfPrimes) { int i; residueInfo->primeInfoArray = ALLOC(PerPrimeInfo_t, numOfPrimes); for (i = 0; i < numOfPrimes; i++) { ResResidueInfoSetPerPrimeInfo(residueInfo, i, tableOfPrimes[i], 0, 0, NIL(bdd_node)); } return; } /* End of ResResidualAllocatePrimeInfoArray */ /**Function******************************************************************** Synopsis [Prints the residue and primeInfoArray information.] SideEffects [] SeeAlso [Res_ResidueAllocate] ******************************************************************************/ void Res_ResidueInfoPrint(Res_ResidueInfo_t *result) { int i; if (result->success) { fprintf(vis_stdout, "The circuit %s was successfully verified against %s.\n", (char *)result->networkName, (char *)result->networkNameVerifiedAgainst); fprintf(vis_stdout, "The circuit has %d inputs and %d outputs ", result->numInputs, result->numOutputs); fprintf(vis_stdout, "of which %d were directly verified.\n", result->numDirectVerifiedOutputs); if (result->numDirectVerifiedOutputs) { fprintf(vis_stdout, "Direct verification took %.3f seconds\n", result->cpuDirectVerif/1000.0); } if (result->numOfPrimes) { fprintf(vis_stdout, "In residue verification using %d primes, \n", result->numOfPrimes); fprintf(vis_stdout, "Primes: "); for (i = 0; i < result->numOfPrimes; i++) { fprintf(vis_stdout, "%d ", result->primeInfoArray[i].primeNumber); } fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "Times: "); for (i = 0; i < result->numOfPrimes; i++) { fprintf(vis_stdout, "%.2f ", result->primeInfoArray[i].cpuTime); } fprintf(vis_stdout, "\n"); } } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/