#include "resInt.h"
Include dependency graph for resRes.c:
Go to the source code of this file.
Functions | |
| void | Res_ResidueInfoFree (Res_ResidueInfo_t *residue) |
| void | Res_ResidueInfoFreeCallback (void *data) |
| Res_ResidueInfo_t * | Res_NetworkReadResidueInfo (Ntk_Network_t *network) |
| char * | Res_ResidueInfoReadName (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadNumInputs (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadNumOutputs (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadNumDirectVerifiedOutputs (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadCpuDirectVerif (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadNumOfPrimes (Res_ResidueInfo_t *residuePtr) |
| int | Res_ResidueInfoReadSuccess (Res_ResidueInfo_t *residuePtr) |
| Res_ResidueInfo_t * | ResNetworkResidueInfoReadOrCreate (Ntk_Network_t *network) |
| Res_ResidueInfo_t * | ResResidueInfoAllocate (char *name) |
| void | ResResidueInfoAllocatePrimeInfoArray (Res_ResidueInfo_t *residueInfo, int numOfPrimes, int *tableOfPrimes) |
| void | Res_ResidueInfoPrint (Res_ResidueInfo_t *result) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $" |
Function Documentation
| Res_ResidueInfo_t* Res_NetworkReadResidueInfo | ( | Ntk_Network_t * | network | ) |
Function********************************************************************
Synopsis [Reads the residue information attached to a network.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 125 of file resRes.c.
{
return (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(network, RES_NETWORK_APPL_KEY);
} /* End of Res_NetworkReadResidueInfo */
Here is the call graph for this function:
| void Res_ResidueInfoFree | ( | Res_ResidueInfo_t * | residue | ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Frees the structure storing the information related to the residual verification.]
SideEffects []
SeeAlso [Res_ResidualInfo]
Definition at line 74 of file resRes.c.
{
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 */
Here is the caller graph for this function:
| void Res_ResidueInfoFreeCallback | ( | void * | data | ) |
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]
Definition at line 109 of file resRes.c.
{
Res_ResidueInfoFree((Res_ResidueInfo_t *) data);
ResResidueFreeVariableManager();
} /* End of Res_ResidueInfoFreeCallback */
Here is the call graph for this function:
Here is the caller graph for this function:
| void Res_ResidueInfoPrint | ( | Res_ResidueInfo_t * | result | ) |
Function********************************************************************
Synopsis [Prints the residue and primeInfoArray information.]
SideEffects []
SeeAlso [Res_ResidueAllocate]
Definition at line 336 of file resRes.c.
{
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");
}
}
}
Here is the caller graph for this function:
| int Res_ResidueInfoReadCpuDirectVerif | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the cpu seconds spent in directly verifying outputs in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 204 of file resRes.c.
{
return (int) ResResidueInfoReadCpuDirectVerif(residuePtr);
} /* End of Res_ResidueInfoReadCpuDirectVerif */
| char* Res_ResidueInfoReadName | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the name field of Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 140 of file resRes.c.
{
return (char *)(ResResidueInfoReadNetworkName(residuePtr));
} /* End of Res_ResidueInfoReadName */
Here is the caller graph for this function:
| int Res_ResidueInfoReadNumDirectVerifiedOutputs | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the number of directly verified outputs in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 188 of file resRes.c.
{
return ResResidueInfoReadNumDirectVerifiedOutputs(residuePtr);
} /* End of Res_ResidueInfoReadNumDirectVerifiedOutputs */
| int Res_ResidueInfoReadNumInputs | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the number of inputs in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 156 of file resRes.c.
{
return ResResidueInfoReadNumInputs(residuePtr);
} /* End of Res_ResidueInfoReadNumInputs */
| int Res_ResidueInfoReadNumOfPrimes | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the number of primes in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 219 of file resRes.c.
{
return ResResidueInfoReadNumOfPrimes(residuePtr);
} /* End of Res_ResidueInfoReadNumOfPrimes */
| int Res_ResidueInfoReadNumOutputs | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the number of outputs in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 172 of file resRes.c.
{
return ResResidueInfoReadNumOutputs(residuePtr);
} /* End of Res_ResidueInfoReadNumOutputs */
| int Res_ResidueInfoReadSuccess | ( | Res_ResidueInfo_t * | residuePtr | ) |
Function********************************************************************
Synopsis [External function to read the success field in Res_ResidueInfo.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 234 of file resRes.c.
{
return ResResidueInfoReadSuccess(residuePtr);
} /* End of Res_ResidueInfoReadNumOfPrimes */
Here is the caller graph for this function:
| Res_ResidueInfo_t* ResNetworkResidueInfoReadOrCreate | ( | Ntk_Network_t * | network | ) |
Function********************************************************************
Synopsis [Wrapper procedure to create a result data structure.]
SideEffects []
Definition at line 251 of file resRes.c.
{
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*/
Here is the call graph for this function:
Here is the caller graph for this function:
| Res_ResidueInfo_t* ResResidueInfoAllocate | ( | char * | name | ) |
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]
Definition at line 282 of file resRes.c.
{
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 */
Here is the caller graph for this function:
| void ResResidueInfoAllocatePrimeInfoArray | ( | Res_ResidueInfo_t * | residueInfo, |
| int | numOfPrimes, | ||
| int * | tableOfPrimes | ||
| ) |
Function********************************************************************
Synopsis [Allocates the array primeInfoArray inside the Res_ResidueInfo_t.]
SideEffects []
SeeAlso [Res_ResidueAllocate]
Definition at line 310 of file resRes.c.
{
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 */
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: resRes.c,v 1.18 2002/08/26 05:53:31 fabio Exp $" [static] |
CFile***********************************************************************
FileName [resRes.c]
PackageName [res]
Synopsis [Data manipulation routines of the Res_ResidueInfo structure.]
SeeAlso [Res_ResidueInfo]
Author [Kavita Ravi <ravi@boulder.colorado.edu> and Abelardo Pardo <abel@boulder.colorado.edu>]
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.]
