#include "resInt.h"
Include dependency graph for res.c:
Go to the source code of this file.
Defines | |
| #define | RES_VERIFY_NOTHING 0 |
| #define | RES_VERIFY_DONE 1 |
| #define | RES_VERIFY_IGNORE_PREV_RESULTS 2 |
| #define | LOG2_FIRST_PRIME 8 |
Functions | |
| static int | ChoosePrimes (int numOutputs, int **pool, int numDirectVerify) |
| static int | ComputeMaxNumberOfOutputs (void) |
| static void | RestoreOldMddIds (Ntk_Network_t *network, st_table *table) |
| static st_table * | GeneratePointerMatchTableFromNameMatch (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *nameMatchTable) |
| static st_table * | GenerateDirectVerifyPointerTable (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, array_t *outputOrderArray, int numDirectVerify) |
| static st_table * | GenerateIdentityMatchTable (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int inputOrOutput) |
| static bdd_manager * | Initializebdd_manager (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int *initManagerHere) |
| static int | SetBasicResultInfo (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify) |
| static void | Cleanup (int error, Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int initManagerHere, int done, st_table *outputMatch, st_table *inputMatch, st_table *directVerifyMatch, st_table *oldSpecMddIdTable, st_table *oldImplMddIdTable, array_t *specLayerArray, array_t *implLayerArray) |
| static st_table * | SaveOldMddIds (Ntk_Network_t *network) |
| static int | DirectVerification (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *directVerifyMatch, st_table *inputMatch, st_table *outputMatch, array_t *outputOrderArray) |
| static bdd_reorder_type_t | DecodeDynMethod (char *dynMethodString) |
| static int | ResidueVerification (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, st_table *inputMatch, int numDirectVerify, array_t *specLayerArray, array_t *implLayerArray, array_t *outputArray) |
| static void | ExtractACubeOfDifference (bdd_manager *mgr, Ntk_Network_t *specNetwork, bdd_node *fn1, bdd_node *fn2) |
| int | Res_NetworkResidueVerify (Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify, array_t *outputOrderArray, st_table *outputNameMatch, st_table *inputNameMatch) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: res.c,v 1.55 2009/04/11 21:31:29 fabio Exp $" |
| static int | PrimePool [] |
| static int | PrimePoolSize = 100 |
Define Documentation
Function Documentation
| static int ChoosePrimes | ( | int | numOutputs, |
| int ** | pool, | ||
| int | numDirectVerify | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Chooses the primes to process a circuit with those many outputs.]
Description [Chooses the primes to process a circuit with those many outputs. It returns an allocated array of primes selected from PrimePool. The number of primes required should exceed the quotient from dividing 2^number of outputs by 2^number of directly verified outputs. If there are no directly verified outputs, the first prime chosen is 2^LOG2_FIRST_PRIME. The procedure is passed the following parameters: number of outputs, the array of primes (to be filled) and the number of directly verified outputs.]
SideEffects [Fills the primes array.]
See Also [Res_NetworkResidueVerify]
Definition at line 597 of file res.c.
{
double accumulator = 0.0;
int i,max, index = 0;
double factor = log10((double)2.0);
assert(*pool == NIL(int));
if (numDirectVerify) {
accumulator = (double)numDirectVerify;
} else {
/* make first prime 2^LOG2_FIRST_PRIME */
if (numOutputs >= LOG2_FIRST_PRIME) {
accumulator = (double)LOG2_FIRST_PRIME;
} else {
accumulator = (double)numOutputs;
}
}
/* step through primes till their product exceeds the max value of outputs */
max = 0;
while (accumulator < ((double)numOutputs)) {
accumulator += log10((double)PrimePool[max])/factor;
max++;
}
index = 0;
/* if no direct verification, then set the first prime to be 2^LOG2_FIRST_PRIME */
if (!numDirectVerify) {
*pool = ALLOC(int, max+1);
if (numOutputs >= LOG2_FIRST_PRIME) {
(*pool)[index++] = (int)pow((double)2.0, (double)LOG2_FIRST_PRIME);
} else {
(*pool)[index++] = (int)pow((double)2.0, (double)numOutputs);
}
} else {
*pool = ALLOC(int, max);
}
/* fill the array with other primes */
for(i=0; i < max; i++) {
(*pool)[index++] = PrimePool[i];
}
return index;
} /* End of ChoosePrimes */
Here is the caller graph for this function:
| static void Cleanup | ( | int | error, |
| Ntk_Network_t * | specNetwork, | ||
| Ntk_Network_t * | implNetwork, | ||
| int | initManagerHere, | ||
| int | done, | ||
| st_table * | outputMatch, | ||
| st_table * | inputMatch, | ||
| st_table * | directVerifyMatch, | ||
| st_table * | oldSpecMddIdTable, | ||
| st_table * | oldImplMddIdTable, | ||
| array_t * | specLayerArray, | ||
| array_t * | implLayerArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Cleanup procedure to free all data structures allocated here.]
Description [Cleanup procedure to free all data structures allocated here. Quit manager if created here. Quit result data structures if created here. The check against RES_VERIFY_NOTHING is to check if the cleanup is called before the result structures were allocated. The arguments to this procedure are an error flag staying if this cleanup is under an error condition, the spec network, impl. network, a flag that says if the manager was initialized here, a flag that indicates if this verification has already been performed, an output pointer match table, an input pointer match table, a directly verified output pointer match table, a table that contains saved mdds for the spec. and the impl., and the layer structures for the spec. and the impl.]
SideEffects [All data structures allocated in the Res_NetworkResidueVerify procedure will be freed here.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 1059 of file res.c.
{
bdd_manager *ddManager;
if (initManagerHere) {
ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
if (ddManager != NIL(bdd_manager)) {
mdd_quit(ddManager);
Ntk_NetworkSetMddManager(specNetwork, NIL(mdd_manager));
Ntk_NetworkSetMddManager(implNetwork, NIL(mdd_manager));
}
}
if (done != RES_VERIFY_NOTHING) { /* if result structure allocated */
if (error) { /* on error free results */
if (done == RES_VERIFY_IGNORE_PREV_RESULTS) {
/* if spec result was created here */
Ntk_NetworkFreeApplInfo(specNetwork,RES_NETWORK_APPL_KEY);
}
Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
}
}
if (outputMatch != NIL(st_table)) {
st_free_table(outputMatch);
}
if (inputMatch != NIL(st_table)) {
st_free_table(inputMatch);
}
if (directVerifyMatch != NIL(st_table)) {
st_free_table(directVerifyMatch);
}
if (oldSpecMddIdTable != NIL(st_table)) {
RestoreOldMddIds(specNetwork, oldSpecMddIdTable);
st_free_table(oldSpecMddIdTable);
}
if (oldImplMddIdTable != NIL(st_table)) {
RestoreOldMddIds(implNetwork, oldImplMddIdTable);
st_free_table(oldImplMddIdTable);
}
if (specLayerArray != NULL) {
ResLayerArrayFree(specLayerArray);
}
if (implLayerArray != NULL) {
ResLayerArrayFree(implLayerArray);
}
return;
} /* End of Cleanup */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ComputeMaxNumberOfOutputs | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Computes the maximum number of outputs a circuit may have in order to be processed with the array PrimePool.]
Description [Computes the maximum number of outputs a circuit may have in order to be processed with the array PrimePool. This is the product of all the primes in the Prime Pool Table.]
SideEffects [Updates the static variable maxNumberOfOutputs.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 662 of file res.c.
{
int i;
double result = 0;
int maxNumberOfOutputs;
result = LOG2_FIRST_PRIME;
for(i = 0; i < PrimePoolSize; i++) {
result += log10((double)PrimePool[i]);
} /* End of for */
maxNumberOfOutputs = (int) (result/log10((double) 2.0)) - 1;
return (maxNumberOfOutputs);
} /* End of ComputeMaxNumberOfOutputs */
Here is the caller graph for this function:
| static bdd_reorder_type_t DecodeDynMethod | ( | char * | dynMethodString | ) | [static] |
Function********************************************************************
Synopsis [Decode the option of reordering.]
Description [Decode the option of reordering. Returns the dynMethod value.]
SideEffects []
Definition at line 1560 of file res.c.
{
bdd_reorder_type_t dynMethod;
/* Translate reordering string to specifying method */
if (dynMethodString == NIL(char)) {
dynMethod = BDD_REORDER_SIFT;
} else if (strcmp(dynMethodString, "same") == 0) {
dynMethod = BDD_REORDER_SAME;
} else if (strcmp(dynMethodString, "none") == 0) {
dynMethod = BDD_REORDER_NONE;
} else if (strcmp(dynMethodString, "random") == 0) {
dynMethod = BDD_REORDER_RANDOM;
} else if (strcmp(dynMethodString, "randompivot") == 0) {
dynMethod = BDD_REORDER_RANDOM_PIVOT;
} else if (strcmp(dynMethodString, "sift") == 0) {
dynMethod = BDD_REORDER_SIFT;
} else if (strcmp(dynMethodString, "siftconverge") == 0) {
dynMethod = BDD_REORDER_SIFT_CONVERGE;
} else if (strcmp(dynMethodString, "symmsift") == 0) {
dynMethod = BDD_REORDER_SYMM_SIFT;
} else if (strcmp(dynMethodString, "symmsiftconverge") == 0) {
dynMethod = BDD_REORDER_SYMM_SIFT_CONV;
} else if (strcmp(dynMethodString, "window2") == 0) {
dynMethod = BDD_REORDER_WINDOW2;
} else if (strcmp(dynMethodString, "window3") == 0) {
dynMethod = BDD_REORDER_WINDOW3;
} else if (strcmp(dynMethodString, "window4") == 0) {
dynMethod = BDD_REORDER_WINDOW4;
} else if (strcmp(dynMethodString, "window2converge") == 0) {
dynMethod = BDD_REORDER_WINDOW2_CONV;
} else if (strcmp(dynMethodString, "window3converge") == 0) {
dynMethod = BDD_REORDER_WINDOW3_CONV;
} else if (strcmp(dynMethodString, "window4converge") == 0) {
dynMethod = BDD_REORDER_WINDOW4_CONV;
} else if (strcmp(dynMethodString, "groupsift") == 0) {
dynMethod = BDD_REORDER_GROUP_SIFT;
} else if (strcmp(dynMethodString, "groupsiftconverge") == 0) {
dynMethod = BDD_REORDER_GROUP_SIFT_CONV;
} else if (strcmp(dynMethodString, "anneal") == 0) {
dynMethod = BDD_REORDER_ANNEALING;
} else if (strcmp(dynMethodString, "genetic") == 0) {
dynMethod = BDD_REORDER_GENETIC;
} else if (strcmp(dynMethodString, "linear") == 0) {
dynMethod = BDD_REORDER_LINEAR;
} else if (strcmp(dynMethodString, "linearconverge") == 0) {
dynMethod = BDD_REORDER_LINEAR_CONVERGE;
} else if (strcmp(dynMethodString, "exact") == 0) {
dynMethod = BDD_REORDER_EXACT;
} else {
dynMethod = BDD_REORDER_SIFT;
}
return dynMethod;
} /* End of DecodeDynMethod */
Here is the caller graph for this function:
| static int DirectVerification | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| st_table * | directVerifyMatch, | ||
| st_table * | inputMatch, | ||
| st_table * | outputMatch, | ||
| array_t * | outputOrderArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Perform direct verification of the given outputs.]
Description [Perform direct verification of the given outputs. If error, returns 1, if successful returns 0. The directVerifyMatch table contains the node pointer matches for the outputs to be directly verified. The procedure first checks if the input variables are ordered. If not ordered, it orders the variables. builds two array with corresponding nodes to be directly verified and a permutation array for the correspondence of the inputs. The outputs arrays are ordered starting with the LSB. For each of these nodes in the array, the bdd is built and compared. Since the primary input variables in the spec and the impl may have different mdd ids, a step of bdd permute is performed on the impl bdd to represent it in terms of the spec PI variables. The resultant Bdds are checked to see if they are identical. The result structure is updated. The parameters to this procedure are the spec. and the impl. network, the match table of the pointers of the directly verified outputs, the tables with the input and output pointer matches and the order array of the outputs.]
SideEffects [Result Structure is updated.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 1175 of file res.c.
{
Ntk_Node_t *nodePtr, *implNodePtr; /* node variables */
long startTime, endTime, directVerifyTime; /* to measure elapsed time */
long lapTimeSpec, lapTimeImpl; /* to measure elapsed time */
bdd_node *specBDD, *implBDD, *permutedBDD; /* bdds of direct verified outputs */
lsGen listGen; /* To iterate over outputList */
int *permut; /* permutation array to store
* correspondence of inputs
*/
int specMddId, implMddId;
Ntk_Node_t **specArray, **implArray; /* arrays to store the
* corresponding nodes of the
* spec. and the impl.
*/
st_generator *stGen;
lsList dummy; /* dummy list fed to the ord
* package.
*/
char *key, *value; /* variables to read values
* from the st_table
*/
int index, i; /* iterators */
char *name; /* variable to read node name */
int numOutputs; /* total number of outputs of
* the spec.(impl).
*/
bdd_manager *ddManager; /* the bdd manager */
bdd_reorder_type_t oldDynMethod, dynMethod = BDD_REORDER_SAME;
/* dynamic reordering methods */
int dynStatus = 0; /* original status of the manager
* w. r. t. dynamic reordering
*/
boolean dyn; /* current dynamic reordering
* status
*/
int verbose; /* verbosity level */
char *flagValue; /* string to hold "Set" variable
* value
*/
Res_ResidueInfo_t *resultSpec; /* result structure for the
* spec.
*/
Res_ResidueInfo_t *resultImpl; /* result structure for the
* impl.
*/
int specSize, implSize; /* sizes of bdds */
mdd_t *fnMddT; /* mdd_t structure to calculate sizes */
/* Initializations */
dummy = (lsList)0;
lapTimeSpec = 0;
lapTimeImpl = 0;
dyn = FALSE;
verbose = 0;
/* read verbosity value */
flagValue = Cmd_FlagReadByName("residue_verbosity");
if (flagValue != NIL(char)) {
verbose = atoi(flagValue);
}
/* read if dynamic ordering is required */
flagValue = Cmd_FlagReadByName("residue_autodyn_direct_verif");
if (flagValue != NIL(char)) {
dyn = (strcmp(flagValue, "1") == 0) ? TRUE : FALSE;
}
/* read method for dynamic reordering */
if (dyn == TRUE) {
flagValue = Cmd_FlagReadByName("residue_direct_dyn_method");
if (flagValue != NULL) {
dynMethod = DecodeDynMethod(flagValue);
} else {
dynMethod = BDD_REORDER_SAME;
}
}
/* read manager from network */
ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
/* save old values for dynamic reordering */
if (dyn == TRUE) {
dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);
bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
}
/* find total time elapsed */
directVerifyTime = util_cpu_time();
/* find number of outputs to be directly verified */
numOutputs = st_count(directVerifyMatch);
/*
* Order primary input variables in the network to build the BDDs for
* outputs to be directly verified.
*/
if (Ord_NetworkTestAreVariablesOrdered(specNetwork,
Ord_InputAndLatch_c) == FALSE) {
/* order the variables in the network since not done */
startTime = util_cpu_time();
Ord_NetworkOrderVariables(specNetwork, Ord_RootsByDefault_c,
Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
Ord_Unassigned_c, dummy, 0);
endTime = util_cpu_time();
lapTimeSpec += endTime - startTime;
startTime = endTime;
Ord_NetworkOrderVariables(implNetwork, Ord_RootsByDefault_c,
Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
Ord_Unassigned_c, dummy, 0);
lapTimeImpl += endTime - startTime;
} else {
/* if order is not specified, assume the same order for spec.
* and implementation
*/
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
assert(Ntk_NodeReadMddId(nodePtr) != NTK_UNASSIGNED_MDD_ID);
st_lookup(inputMatch, (char *)nodePtr, &implNodePtr);
Ntk_NodeSetMddId(implNodePtr, Ntk_NodeReadMddId(nodePtr));
}
}
if (verbose >= 5) {
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
specMddId = Ntk_NodeReadMddId(nodePtr);
if (specMddId != NTK_UNASSIGNED_MDD_ID) {
fprintf(vis_stdout, "%s ", Ntk_NodeReadName(nodePtr));
}
}
fprintf(vis_stdout, "\n");
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
specMddId = Ntk_NodeReadMddId(nodePtr);
if (specMddId != NTK_UNASSIGNED_MDD_ID) {
fprintf(vis_stdout, "%d ", specMddId);
}
}
fprintf(vis_stdout, "\n");
}
/* build arrays of corresponding nodes to be directly verified */
specArray = ALLOC(Ntk_Node_t *, numOutputs);
implArray = ALLOC(Ntk_Node_t *, numOutputs);
index = 0;
/* Order array starting from the LSB, so direct verification is performed
* starting from the inputs.
*/
for (i = 0; i < array_n(outputOrderArray); i++) {
name = array_fetch(char *, outputOrderArray, array_n(outputOrderArray)-1-i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
/* find node in direct verify match table */
if (st_lookup(directVerifyMatch, (char *)nodePtr, (char **)&value)) {
specArray[index] = (Ntk_Node_t *)nodePtr;
implArray[index] = (Ntk_Node_t *)value;
index++;
}
}
/* number of outputs in the arrays should be as many entries as the match
* table.
*/
assert(numOutputs == index);
/* Create a permutation array for the specMddId and implMddId input nodes */
permut = ALLOC(int, bdd_num_vars(ddManager));
for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
permut[i] = i;
}
st_foreach_item(inputMatch, stGen, &key, &value) {
nodePtr = (Ntk_Node_t *)key;
implNodePtr = (Ntk_Node_t *)value;
if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
error_append("Input match values do not return");
error_append("valid node pointers.\n");
/* Clean up */
FREE(permut);
FREE(specArray);
FREE(implArray);
st_free_gen(stGen);
return 1;
}
/* create the array with the impl. vars to be composed with spec. vars. */
specMddId = Ntk_NodeReadMddId(nodePtr);
implMddId = Ntk_NodeReadMddId(implNodePtr);
/* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
* ordering above
*/
assert(specMddId != NTK_UNASSIGNED_MDD_ID);
assert(implMddId != NTK_UNASSIGNED_MDD_ID);
permut[implMddId] = specMddId;
} /* end of input match */
/*
* Build BDDs for each output to be directly verified and check
* for identical BDDs in spec. and impl.
*/
for (i = 0; i < numOutputs; i++) {
/* build the spec BDD */
startTime = util_cpu_time();
specBDD = BuildBDDforNode(specNetwork, specArray[i], PRIMARY_INPUTS);
if (specBDD == NIL(bdd_node)) {
error_append("Unable to build spec. BDD for the direct verification output");
error_append(Ntk_NodeReadName(specArray[i]));
error_append(".\n");
/* Clean up */
FREE(permut);
FREE(specArray);
FREE(implArray);
return 1; /* error status */
} /* end of if spec BDD is NIL */
endTime = util_cpu_time();
lapTimeSpec += endTime - startTime;
/* build the impl BDD */
startTime = endTime;
implBDD = BuildBDDforNode(implNetwork, implArray[i], PRIMARY_INPUTS);
if (implBDD == NIL(bdd_node)) {
error_append("Unable to build spec. BDD for the direct verification output");
error_append(Ntk_NodeReadName(implArray[i]));
error_append(".\n");
/* Clean up */
bdd_recursive_deref(ddManager, specBDD);
FREE(permut);
FREE(specArray);
FREE(implArray);
return 1; /* error status */
} /* end of if spec BDD is NIL */
endTime = util_cpu_time();
lapTimeImpl += endTime - startTime;
/* call bdd permute to compose the impl variables with the spec
* variables.
*/
startTime = endTime;
bdd_ref(permutedBDD = bdd_bdd_permute(ddManager, implBDD, permut));
bdd_recursive_deref(ddManager, implBDD);
endTime = util_cpu_time();
lapTimeSpec += (endTime - startTime)/2;
lapTimeImpl += (endTime - startTime)/2;
implBDD = permutedBDD;
if (implBDD == NIL(bdd_node)) {
error_append("Permuting the impl bdd in terms of spec bdd vars failed\n");
/* Clean up */
bdd_recursive_deref(ddManager, specBDD);
FREE(permut);
FREE(specArray);
FREE(implArray);
return 1; /* error status */
}
/* compare the bdds */
if(specBDD != implBDD) {
/* error since spec and impl are not the same */
/* update result structure */
if (verbose >= 2) {
(void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
(void)fprintf(vis_stdout, "Specification Input Names :\n");
ExtractACubeOfDifference(ddManager, specNetwork, specBDD, implBDD);
}
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_FAIL);
ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_FAIL);
(void) fprintf(vis_stdout, "%.2f (secs) spent in failed direct verification.\n",
(util_cpu_time() - directVerifyTime)/1000.0);
fprintf(vis_stdout, "Residue Direct Verification failed at output node ");
fprintf(vis_stdout, "%s", Ntk_NodeReadName(specArray[i]));
fprintf(vis_stdout, " of the spec.\n");
fprintf(vis_stdout, "Spec. did not match Impl.\n");
/* Clean up */
/* free the bdds just created */
bdd_recursive_deref(ddManager, specBDD);
bdd_recursive_deref(ddManager, implBDD);
FREE(permut);
FREE(specArray);
FREE(implArray);
return 0;
} /* end if spec BDD != impl BDD */
/* if the bdds are equal, print some information */
if (verbose >= 2) {
fprintf(vis_stdout, "%d out of %d ", i + 1 ,numOutputs);
fprintf(vis_stdout, "direct verification outputs done.\n");
}
if (verbose >= 3) {
fprintf(vis_stdout, "%s(spec)/%s(impl) output verified. \n",
Ntk_NodeReadName(specArray[i]), Ntk_NodeReadName(implArray[i]));
bdd_ref(specBDD);
fnMddT = bdd_construct_bdd_t(ddManager, specBDD);
specSize = bdd_size(fnMddT);
bdd_free(fnMddT);
bdd_ref(implBDD);
fnMddT = bdd_construct_bdd_t(ddManager, implBDD);
implSize = bdd_size(fnMddT);
bdd_free(fnMddT);
fprintf(vis_stdout, "Size of %s(spec) = %d, Size of %s(impl) = %d\n",
Ntk_NodeReadName(specArray[i]) ,specSize, Ntk_NodeReadName(implArray[i]), implSize);
fprintf(vis_stdout, "%.3f spec time elapsed, %.3f impl. time elapsed.\n", lapTimeSpec/1000.0,
lapTimeImpl/1000.0);
}
/* free the bdds just created */
bdd_recursive_deref(ddManager, specBDD);
bdd_recursive_deref(ddManager, implBDD);
} /* end of for-loop that iterates through the nodes to be directly
* verified.
*/
FREE(permut);
FREE(specArray);
FREE(implArray);
/* set direct verification success info */
/* update result structure */
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_PASS);
ResResidueInfoSetCpuDirectVerif(resultSpec, (float) lapTimeSpec);
ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_PASS);
ResResidueInfoSetCpuDirectVerif(resultImpl, (float) lapTimeImpl);
/* Print success message */
fprintf(vis_stdout, "Residue Direct Verification successful.\n");
/* Print Time taken for direct verification */
if (verbose >= 1) {
(void) fprintf(vis_stdout, "%.2f (secs) spent in Direct verification.\n",
(util_cpu_time() - directVerifyTime)/1000.0);
}
/* Print which outputs were directly verified and time spent for
* the spec and the impl
*/
if (verbose >= 2) {
fprintf(vis_stdout, "Time taken to build spec. BDD = %.3f\n",
ResResidueInfoReadCpuDirectVerif(resultSpec)/1000.0);
fprintf(vis_stdout, "Time taken to build impl. BDD = %.3f\n",
ResResidueInfoReadCpuDirectVerif(resultImpl)/1000.0);
st_foreach_item(directVerifyMatch, stGen, &key, &value) {
fprintf(vis_stdout, "%s ", Ntk_NodeReadName((Ntk_Node_t *)key));
}
fprintf(vis_stdout, "verified successfully.\n");
}
/* Print order of variables of this verification */
if (verbose >= 3) {
Ord_NetworkPrintVariableOrder(vis_stdout, specNetwork,
Ord_InputAndLatch_c);
Ord_NetworkPrintVariableOrder(vis_stdout, implNetwork,
Ord_InputAndLatch_c);
}
/* restore the old values for dynamic reordering */
if(dyn == TRUE) {
bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
if (!dynStatus) {
bdd_dynamic_reordering_disable(ddManager);
}
}
return 0; /* direct verification success */
} /* End of Direct Verification */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ExtractACubeOfDifference | ( | bdd_manager * | mgr, |
| Ntk_Network_t * | specNetwork, | ||
| bdd_node * | fn1, | ||
| bdd_node * | fn2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [ Prints out a cube in the XOR of the 2 Bdds]
Description [ ] value]
SideEffects [.]
SeeAlso []
Definition at line 2054 of file res.c.
{
bdd_t *fnMddT, *fnMddT1; /* mdd_t structure to calculate sizes */
bdd_t *fnMddT2, *fnMddT3; /* mdd_t structure to calculate sizes */
bdd_gen *gen;
array_t *cube, *namesArray;
lsGen listGen;
int i, literal;
Ntk_Node_t *nodePtr;
/* make bdd_ts of the two functions */
bdd_ref(fn2);
fnMddT = bdd_construct_bdd_t(mgr, fn2);
bdd_ref(fn1);
fnMddT1 = bdd_construct_bdd_t(mgr, fn1);
fnMddT2 = bdd_not(fnMddT1);
/* extracts some cubes in the intersection of fn1' and fn2 */
fnMddT3 = bdd_intersects(fnMddT, fnMddT2);
/* check not zero */
if (bdd_is_tautology(fnMddT3, 0)) {
bdd_free(fnMddT3);
bdd_free(fnMddT2);
/* extracts some cubes in the intersection of fn2' and fn1 */
fnMddT2 = bdd_not(fnMddT);
fnMddT3 = bdd_intersects(fnMddT1, fnMddT2);
}
assert(!bdd_is_tautology(fnMddT3, 0));
bdd_free(fnMddT);
bdd_free(fnMddT1);
bdd_free(fnMddT2);
/* pick a cube from the xor of fn1 and fn2 */
gen = bdd_first_cube(fnMddT3, &cube);
bdd_free(fnMddT3);
/* store the names to be printed out later */
namesArray = array_alloc(char *, array_n(cube));
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
array_insert(char *, namesArray , Ntk_NodeReadMddId(nodePtr), Ntk_NodeReadName(nodePtr));
}
/* print out the cube */
arrayForEachItem(int, cube, i, literal) {
if (literal != 2) {
(void) fprintf(vis_stdout, "%s ", array_fetch(char *, namesArray, i));
}
}
fprintf(vis_stdout, "\n");
arrayForEachItem(int, cube, i, literal) {
if (literal != 2) {
(void) fprintf(vis_stdout, "%1d", literal);
}
}
fprintf(vis_stdout, "\n");
array_free(namesArray);
bdd_gen_free(gen);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * GenerateDirectVerifyPointerTable | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| st_table * | outputMatch, | ||
| array_t * | outputOrderArray, | ||
| int | numDirectVerify | ||
| ) | [static] |
Function********************************************************************
Synopsis [Generates a pointer match table for the directly verified outputs.]
Description [Generates a pointer match table for the directly verified outputs. Returns NIL if a node isn't found, else returns the table.The procedure takes as arguments the spec., the impl., the output match table with pointers, the output order array and the number of directly verified outputs.]
SideEffects []
SeeAlso [Res_NetworkResidueVerify]
Definition at line 785 of file res.c.
{
char *specName;
int i;
Ntk_Node_t *nodePtr, *implNodePtr;
st_table *directVerifyMatch;
directVerifyMatch = st_init_table(st_ptrcmp, st_ptrhash);
for (i = 0; i < numDirectVerify; i++) {
specName = array_fetch(char *, outputOrderArray, array_n(outputOrderArray) - 1 - i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, specName);
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
error_append("Couldn't find nodes to directly verify\n");
st_free_table(directVerifyMatch);
return NIL(st_table);
}
st_insert(directVerifyMatch, (char *)nodePtr, (char *)implNodePtr);
}
return (directVerifyMatch);
} /* End of GenerateDirectVerifyPointerTable */
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * GenerateIdentityMatchTable | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| int | inputOrOutput | ||
| ) | [static] |
Function********************************************************************
Synopsis [ A procedure to generate a pointer Match table with from nodes with identical names.]
Description [A procedure to generate a pointer Match table with from nodes with identical names. This procedure does it for either the inputs or outputs depending on the flag. Returns NULL if the impl. does not have a node corresponding to the spec. The procedure takes as arguments the spec., the impl. and the flag specifying whether the pointer match table is to be built for the output or the input.]
SideEffects []
SeeAlso [Res_NetworkResidueVerify]
Definition at line 831 of file res.c.
{
Ntk_Node_t *nodePtr, *implNodePtr;
st_table *matchTable;
lsGen listGen;
char *name;
matchTable = st_init_table(st_ptrcmp, st_ptrhash);
if (matchTable == NULL) return(NIL(st_table));
if (inputOrOutput == PRIMARY_INPUTS) {
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
name = Ntk_NodeReadName(nodePtr);
implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, name);
if (implNodePtr == NIL(Ntk_Node_t)) {
error_append(name);
error_append(" node does not have corresponding node in impl.");
st_free_table(matchTable);
return (NIL(st_table));
}
st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
}
} else if (inputOrOutput == PRIMARY_OUTPUTS) {
Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
name = Ntk_NodeReadName(nodePtr);
implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,name);
if (implNodePtr == NIL(Ntk_Node_t)) {
error_append(name);
error_append(" node does not have corresponding node in impl.");
st_free_table(matchTable);
return (NIL(st_table));
}
st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
}
}
return (matchTable);
} /* End of GenerateIdentityMatchTable */
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * GeneratePointerMatchTableFromNameMatch | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| st_table * | nameMatchTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Procedure to generate a match Table with node pointers from a match table with names.]
Description [Procedure to generate a match Table with node pointers from a match table with names.The name match table will have pairs of names which may be from the spec or the impl. So for each unique pair there are two entries in the name match table. The pointer match table is constructed with the spec. node pointer as the key. If the node pointer for a name isn't found in either network, return NIL (error). The procedure takes in the parameters: spec., impl and a name match table and returns a pointer match table corresponding to the names.]
SideEffects []
SeeAlso [Res_NetworkResidueVerify]
Definition at line 735 of file res.c.
{
st_table *pointerMatch;
Ntk_Node_t *nodePtr, *implNodePtr;
st_generator *stGen;
char *key, *value;
pointerMatch = st_init_table( st_ptrcmp, st_ptrhash);
st_foreach_item(nameMatchTable, stGen, &key, &value) {
/* find node in spec */
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, key);
if (nodePtr == NIL(Ntk_Node_t)) {
/* if node not in spec, find in impl */
implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, key);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, value);
} else {
implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,value);
}
if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
/* error */
error_append("Nodes not found by the keys in match table.\n");
st_free_gen(stGen);
return NIL(st_table);
}
st_insert(pointerMatch, (char *)nodePtr, (char *)implNodePtr);
} /* end of st_foreach_item */
return(pointerMatch);
} /* End of GeneratePointerMatchTableFromNameMatch */
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_manager * Initializebdd_manager | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| int * | initManagerHere | ||
| ) | [static] |
Function********************************************************************
Synopsis [Initialize bdd_managers for the networks.]
Description [Initialize bdd_managers for the networks. If both managers are NIL , initialize a DD Manager here and set it in both networks. If the manager is not NIL, then they have to be the same. If different, keep the spec network manager. Return a flag if managers are initialized here. The procedure takes as arguments the spec., the impl. and the flag specifying whether the the manager was initialized here (to be filled).]
SideEffects [Network manager values might change.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 888 of file res.c.
{
bdd_manager *ddManager;
/* Read the mdd Manager (or create it if necessary) */
ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
/* To set the spec manager the same as the impl. manager, either
* both are nil, or the impl manager is freed and set to the
* spec manager
*/
if(ddManager != (bdd_manager *)Ntk_NetworkReadMddManager(implNetwork)) {
if ((bdd_manager *)Ntk_NetworkReadMddManager(implNetwork) != NIL(bdd_manager)) {
/* unacceptable if the impl. manager is different from NIl or
* from the spec manager
*/
mdd_quit(Ntk_NetworkReadMddManager(implNetwork));
}
Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
}
/* if the spec. manager is NIL, then network initialize manager */
if (ddManager == NIL(bdd_manager)) {
/* flag to say that manager is verified here */
*initManagerHere = 1;
ddManager = (bdd_manager *)Ntk_NetworkInitializeMddManager(specNetwork);
Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
}
return (ddManager);
} /* End of Initializebdd_manager */
Here is the call graph for this function:
Here is the caller graph for this function:
| int Res_NetworkResidueVerify | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| int | numDirectVerify, | ||
| array_t * | outputOrderArray, | ||
| st_table * | outputNameMatch, | ||
| st_table * | inputNameMatch | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Performs direct and residue verification of a given network.]
Description [ Performs direct and residue verification of a given network. This function is the core routine for residue verification. The network parameters are in a specific order: SPECIFICATION first, IMPLEMENTATION second. The two networks are differentiated because the specification is the only circuit which may store previously computed results. Also all other parameters are with reference to the specification. The next parameter is the number of outputs to directly verify. The output order array gives the order of the outputs, starting from the MSB. The output and input match table contain name matches for the output and input. The key in this table belongs to the specification and the value to the implementation. The procedure initializes the manager, computes maximum number of outputs that can be verified, sets basic result information. It also sets up the match tables with pointers and saves the old MDD Ids in a table. It then calls the direct verification procedure, if there are any outputs to be verified. For residue verification, the procedure calls the layering procedure on both networks and creates layers. It calls the main residue verification procedure and updates the result structures. Returns the value 0 on success. The procedure takes in as arguments the specification network, the implementation network in that order, the number of outputs that need to be directly verified, the order of all the outputs, the table with outputs name matches of the spec. and the impl. and a similar input name match table.]
SideEffects [The residue Info structure gets updated.]
Definition at line 120 of file res.c.
{
Ntk_Node_t *nodePtr; /* To iterate over nodes */
Ntk_Node_t *implNodePtr; /* To iterate over nodes */
Res_ResidueInfo_t *resultSpec; /* Structure holding all the info */
Res_ResidueInfo_t *resultImpl; /* Structure holding all the info */
array_t *specLayerArray; /* array containing the reverse
* topological layers of the spec.
*/
array_t *implLayerArray; /* array containing the reverse
* topological layers of the impl.
*/
st_table *oldSpecMddIdTable; /* Tables to store MDD IDs of the spec
* if already assigned
*/
st_table *oldImplMddIdTable; /* Tables to store MDD IDs of the impl.
* if already assigned
*/
st_table *outputMatch; /* Output match table with node
* pointers, spec node pointer is
* the key
*/
st_table *inputMatch; /* Input match table with node
* pointers, spec node pointer is
* the key
*/
bdd_manager *ddManager; /* Manager read from the network */
int initManagerHere; /* Flag to indicate the network Mdd
* managers initialized here
*/
lsGen listGen; /* To iterate over outputList */
long overallLap; /* To measure overall execution time */
int maxNumberOfOutputs; /* max number of outputs that can be
* verified here
* = product(100 primes)
*/
int numOutputs; /* Store the number of outputs in spec.,
* impl
*/
int done; /* flag to determine the status of
* previous verification
*/
int error; /* error flag, set for cleanup, 1 failed,
* 0 if successful
*/
int status; /* error status of residue verification */
int directVerifyStatus; /* direct verification status, 1 if failed,
* 0 if successful
*/
st_table *directVerifyMatch; /* match table with pointers for the
* directly verified outputs, spec pointer
* is key
*/
char *name; /* variable to store name of node */
array_t *outputArray; /* array to store output nodes */
array_t *ignoreOutputArray; /* array to store outputs nodes to be
* ignored
*/
int verbose; /* variable to read residue_verbosity value */
char *flagValue; /* string to read flag values */
int i; /* Loop iterators */
int unassignedValue; /* NTK_UNASSIGNED_MDD_ID value holder */
/* Initialize some variables to default values */
overallLap = 0;
initManagerHere = 0;
ddManager = NIL(bdd_manager);
done = RES_VERIFY_NOTHING;
error = 0;
status = 1;
verbose = 0;
unassignedValue = NTK_UNASSIGNED_MDD_ID;
directVerifyStatus = 1;
directVerifyMatch = NIL(st_table);
specLayerArray = NIL(array_t);
implLayerArray = NIL(array_t);
outputArray = NIL(array_t);
ignoreOutputArray = NIL(array_t);
outputMatch = NIL(st_table);
inputMatch = NIL(st_table);
oldSpecMddIdTable = NIL(st_table);
oldImplMddIdTable = NIL(st_table);
resultSpec = NIL(Res_ResidueInfo_t);
resultImpl = NIL(Res_ResidueInfo_t);
/* Initialize global time values*/
Res_composeTime = 0;
Res_smartVarTime = 0;
Res_shuffleTime = 0;
Res_orderTime = 0;
/* Read verbosity value */
flagValue = Cmd_FlagReadByName("residue_verbosity");
if (flagValue != NIL(char)) {
verbose = atoi(flagValue);
}
/* Read the mdd Manager (or create it if necessary) */
ddManager = Initializebdd_manager(specNetwork, implNetwork, &initManagerHere);
if (ddManager == NIL(bdd_manager)) {
/* error, but nothing allocated, so no cleanup */
return 1;
}
/* Set up the correct maximum number of outputs */
maxNumberOfOutputs = ComputeMaxNumberOfOutputs();
if (verbose >= 2) {
fprintf(vis_stdout, "The Maximum Number of outputs that can be");
fprintf(vis_stdout, " verified are %d.\n", maxNumberOfOutputs);
}
/* check number of outputs */
numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
/* Check if the circuit has too many outputs */
if (numOutputs >= maxNumberOfOutputs) {
error_append("Circuit with too many outputs.\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1;
} /* End of if */
/* Create result data structure for both the spec and the implementation */
done = SetBasicResultInfo(specNetwork, implNetwork, numDirectVerify);
if (done == RES_VERIFY_DONE) {/* same verification as previous time */
/* Clean up before you leave */
fprintf(vis_stdout, "Verification has been previously performed\n");
error = 0;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 0; /* success */
} /* end of case RES_VERIFY_DONE */
/* if output match table does not exist, create one with matching names
* in the two networks. Insert with spec network node pointer as key
* in the outputMatch table. If match table does exist, convert name table
* to pointer table.
*/
if(outputNameMatch == NIL(st_table)) {
outputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_OUTPUTS);
} else {
outputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
implNetwork,outputNameMatch);
if (outputMatch == NIL(st_table)) {
error_append("Output pointer table is NULL\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1; /* error return */
}
}
/* if input match table does not exist, create one with matching names
* in the two networks. Insert with spec network node pointer as key
* in the inputMatch table. If match table does exist, convert name table
* to pointer table.
*/
if(inputNameMatch == NIL(st_table)) {
inputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_INPUTS);
} else {
inputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
implNetwork,inputNameMatch);
if (inputMatch == NIL(st_table)) {
error_append("Input pointer table is NULL\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1; /* error return */
}
}
/* Save the old MDD IDs in a st_table */
oldSpecMddIdTable = SaveOldMddIds(specNetwork);
if (oldSpecMddIdTable == NIL(st_table)) {
error_append("Unable to save old Mdd Ids for spec\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1;
}
/* Save the old MDD IDs in a st_table */
oldImplMddIdTable = SaveOldMddIds(implNetwork);
if (oldImplMddIdTable == NIL(st_table)) {
error_append("Unable to save old Mdd Ids for impl\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1;
}
/* Initialize time to measure overall lap time */
overallLap = util_cpu_time();
/* Perform direct verification of the given outputs. */
if (numDirectVerify) {
/* generate output match table for outputs to be directly verified */
directVerifyMatch = GenerateDirectVerifyPointerTable(specNetwork,
implNetwork, outputMatch, outputOrderArray, numDirectVerify);
if (directVerifyMatch == NIL(st_table)) {
error_append("Directly verify pointer table is NULL\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1; /* error return */
}
/* perform direct verification of the outputs in the match table */
directVerifyStatus = DirectVerification(specNetwork, implNetwork,
directVerifyMatch, inputMatch, outputMatch, outputOrderArray);
/* Direct verification error */
if (directVerifyStatus == 1) {
error_append("Direct Verification error\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1; /* error return */
}
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
/* Direct verification failed */
if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_FAIL) &&
(ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_FAIL)) {
ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
/* Clean up before you leave */
error = 0;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 0;
} else if (numDirectVerify == numOutputs) {
if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS) &&
(ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) {
/* if all outputs are directly verified */
ResResidueInfoSetSuccess(resultSpec, RES_PASS);
ResResidueInfoSetSuccess(resultImpl, RES_PASS);
}
} /* end of else */
} /* Direct Verification, done and successful */
(void) fprintf(vis_stdout, "Total Direct Verification Time = %.3f (secs).\n",
(util_cpu_time() - overallLap)/1000.0);
if (verbose >= 1) {
util_print_cpu_stats(vis_stdout);
}
/* RESIDUE VERIFICATION starts here */
if (numOutputs - numDirectVerify) { /* if residue verification required */
/* reset all Ids after direct verification as residue verification
* assigns new Ids.
*/
Ntk_NetworkForEachNode(specNetwork, listGen, nodePtr) {
Ntk_NodeSetMddId(nodePtr, unassignedValue);
}
Ntk_NetworkForEachNode(implNetwork, listGen, nodePtr) {
Ntk_NodeSetMddId(nodePtr, unassignedValue);
}
/* check if directly verified outputs are to be involved in residue
* verification
*/
flagValue = Cmd_FlagReadByName("residue_ignore_direct_verified_outputs");
if (flagValue != NIL(char)) {
if ((strcmp(flagValue, "1") == 0) && (numDirectVerify)) {
ignoreOutputArray = array_alloc(Ntk_Node_t *, numDirectVerify);
}
}
if (ignoreOutputArray == NIL(array_t)) {
/* fill the output array with all output nodes */
outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray));
arrayForEachItem(char *, outputOrderArray, i, name) {
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
}
} else {
outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray)-numDirectVerify);
/* fill the output array with nodes not directly verified */
for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
name = array_fetch(char *, outputOrderArray, i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
}
/* fill ignore array with outputs directly verified. */
for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
name = array_fetch(char *, outputOrderArray, i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify) , implNodePtr);
}
}
/* Compute the layers to be used for function composition */
implLayerArray = ResComputeCompositionLayers(implNetwork, outputArray, ignoreOutputArray);
/* create the output array for the spec. */
if (ignoreOutputArray == NIL(array_t)) {
/* fill the output array with all output nodes */
arrayForEachItem(char *, outputOrderArray, i, name) {
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
}
} else {
/* fill the output array with nodes not directly verified */
for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
name = array_fetch(char *, outputOrderArray, i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
}
/* fill ignore array with outputs directly verified. */
for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
name = array_fetch(char *, outputOrderArray, i);
nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify), nodePtr);
}
}
/* Compute the layers to be used for function composition */
specLayerArray = ResComputeCompositionLayers(specNetwork, outputArray, ignoreOutputArray);
/* print the array */
if (verbose >=3) {
ResLayerPrintInfo(specNetwork, specLayerArray);
ResLayerPrintInfo(implNetwork, implLayerArray);
}
/* free the ignore array */
if (ignoreOutputArray != NIL(array_t)) {
array_free(ignoreOutputArray);
}
/* Perform residue verification on the spec. and impl. */
status = ResidueVerification(specNetwork, implNetwork, outputMatch, inputMatch, numDirectVerify, specLayerArray, implLayerArray, outputArray);
/* free output array */
array_free(outputArray);
if (status) {
error_append("Residue Verification error\n");
/* Clean up before you leave */
error = 1;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 1; /* error return */
}
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
/* Print success message and info */
if ((ResResidueInfoReadSuccess(resultSpec) == RES_FAIL) &&
(ResResidueInfoReadSuccess(resultImpl) == RES_FAIL)) {
/* Clean up before you leave */
error = 0;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
return 0;
}
if(verbose >= 2) {
(void) fprintf(vis_stdout, "Total Compose Time = %3f(secs).\n",
Res_composeTime/1000.0);
(void) fprintf(vis_stdout, "Total Order Time = %3f(secs).\n",
Res_orderTime/1000.0);
(void) fprintf(vis_stdout, "Total Shuffle Time = %3f(secs).\n",
Res_shuffleTime/1000.0);
(void) fprintf(vis_stdout, "Total Smart Var Time = %3f(secs).\n",
Res_smartVarTime/1000.0);
}
} /* end of residue verification */
/* Print success message and info */
if ((ResResidueInfoReadSuccess(resultSpec) == RES_PASS) &&
(ResResidueInfoReadSuccess(resultImpl) == RES_PASS))
(void) fprintf(vis_stdout, "Verification of %s and %s successful.\n",
Res_ResidueInfoReadName(resultSpec),
Res_ResidueInfoReadName(resultImpl));
if (verbose >= 1) {
fprintf(vis_stdout, "Specification:\n");
(void) Res_ResidueInfoPrint(resultSpec);
fprintf(vis_stdout, "Implementation:\n");
(void) Res_ResidueInfoPrint(resultImpl);
}
if (verbose >= 1) {
util_print_cpu_stats(vis_stdout);
}
(void) fprintf(vis_stdout, "Total Time = %.3f (secs).\n",
(util_cpu_time() - overallLap)/1000.0);
/* no error */
error = 0;
Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
oldImplMddIdTable, specLayerArray, implLayerArray);
/* End of clean up */
return 0;
} /* End of Res_NetworkResidueVerify */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ResidueVerification | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| st_table * | outputMatch, | ||
| st_table * | inputMatch, | ||
| int | numDirectVerify, | ||
| array_t * | specLayerArray, | ||
| array_t * | implLayerArray, | ||
| array_t * | outputArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Main Function to perform residue verification.]
Description [Main Function to perform residue verification. The network parameters are in a specific order: SPECIFICATION first, IMPLEMENTATION second. All other parameters store values of the specification. The procedure first turns off dynamic reordering unless specified otherwise. The array of required primes are computed and the cudd manager is initialized. The main loop iterates over the primes. The residue ADD is constructed for as many variables as POs with respect to each prime. Then calls a procedure which composes the networks (in layers) into the residue ADD. The final ADD is compared for both the spec and the impl. A sub-routine composes the network into the residue ADD depending on the composition method. The final ADDs for the specification and the implementation are checked against each other. The procedure returns 0 if it were unable to complete for some reason, like memory failure, incomplete networks, etc. The procedure returns 0 if successful in building the BDDs of the two circuits. The parameters to this procedure are spec. network, impl. network, output pointer match table, input pointer match table, number of directly verified outputs, layer structure of the spec. and the impl. and an array of nodes with outputs for residue verification.]
SideEffects []
Definition at line 1644 of file res.c.
{
int numOutputs; /* number of outputs in the networks */
int actualOutputs; /* number of outputs in the networks */
int msbId; /* stores the top Id available */
int msbLsb; /* 1 means Msb on top */
Ntk_Node_t *nodePtr, *implNodePtr; /* variables to store nodes in networks */
Res_ResidueInfo_t *resultSpec; /* spec. result structure */
Res_ResidueInfo_t *resultImpl; /* impl. result structure */
int verbose; /* verbosity value */
char *flagValue; /* string to store flag values */
int i; /* iterating index */
lsGen listGen; /* list generator for looping over nodes
* in a network.
*/
st_generator *stGen; /* generator to step through st_table */
char *key, *value; /* variables to read in st-table values */
long overallLap; /* to measure elapsed time */
long lap; /* to measure elapsed time */
int primeIndex; /* index to iterate over prime array */
bdd_manager *ddManager; /* Manager read from the network */
bdd_node *implADD, *specADD, *tmpDd; /* final ADDs after composition */
int specSize, implSize; /* sizes of bdds */
int specMddId, implMddId; /* id variables for nodes */
bdd_node *residueDd; /* residue ADD (n x m) */
int *permut; /* array to permute impl ADD variables to spec.
* ADD variables.
*/
int numOfPrimes; /* Number of primes needed for verification */
int *primeTable; /* array to store primes needed for current
* verification
*/
bdd_reorder_type_t oldDynMethod, dynMethod; /* dynamic reordering
* methods
*/
int dynStatus; /* Status of manager w.r.t. original
* reordering
*/
boolean dyn; /* flag to indicate dynamic reordering
* is turned on.
*/
mdd_t *fnMddT; /* mdd_t structure to calculate sizes */
int unassignedValue; /* NTK_UNASSIGNED_MDD_ID value holder */
array_t *implOutputArray; /* array of output nodes of the impl.in consideration
* for composition
*/
/* Initialization */
verbose = 0;
unassignedValue = NTK_UNASSIGNED_MDD_ID;
numOfPrimes = 0;
msbLsb = 1; /* default value msb is on top */
primeTable = NULL;
overallLap = util_cpu_time();
dyn = FALSE; /* default dynamic reordering disabled */
permut = NULL;
/* specify if the top var of the residue ADD is the MSB/LSB */
flagValue = Cmd_FlagReadByName("residue_top_var");
if (flagValue != NIL(char) && strcmp(flagValue,"lsb") == 0) {
msbLsb = 0;
} else {
msbLsb = 1;
}
/* initialize number of outputs */
actualOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
/* Read the mdd Manager (or create it if necessary) */
ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
/* save old dynamic reordering values */
dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);
/* read verbosity value */
flagValue = Cmd_FlagReadByName("residue_verbosity");
if (flagValue != NIL(char)) {
verbose = atoi(flagValue);
}
/* read if dynamic ordering is required */
flagValue = Cmd_FlagReadByName("residue_autodyn_residue_verif");
if (flagValue != NIL(char)) {
dyn = (strcmp(flagValue,"1")==0) ? TRUE : FALSE;
}
/* read method of dynamic reordering */
if (dyn == TRUE) {
flagValue = Cmd_FlagReadByName("residue_residue_dyn_method");
if ( flagValue != NULL) {
dynMethod = DecodeDynMethod(flagValue);
} else {
dynMethod = BDD_REORDER_SAME;
}
/* update manager with dynamic reordering and the method */
bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
} else {
/* unless specified, TURN REORDERING OFF for residue verification */
bdd_dynamic_reordering_disable(ddManager);
}
/*
* Choose the set of primes that will be used, primeTable is allocated
* here.
*/
numOfPrimes = ChoosePrimes(actualOutputs, &primeTable, numDirectVerify);
/* get result structures */
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
/* update result with primes info */
if ((resultSpec != NIL(Res_ResidueInfo_t)) && (resultImpl != NIL(Res_ResidueInfo_t))) {
ResResidueInfoAllocatePrimeInfoArray(resultSpec, numOfPrimes, primeTable);
ResResidueInfoAllocatePrimeInfoArray(resultImpl, numOfPrimes, primeTable);
ResResidueInfoSetNumOfPrimes(resultSpec, numOfPrimes);
ResResidueInfoSetNumOfPrimes(resultImpl, numOfPrimes);
} else {
/* error - the result structure should be there */
error_append("Result structures are missing\n");
FREE(primeTable);
return 1;
}
/* Print the list of primes depending on the verbosity level*/
if (verbose >= 0) {
(void) fprintf(vis_stdout, "List of Primes used: ");
for(i=0; i<numOfPrimes; i++) {
(void) fprintf(vis_stdout, "%d ", primeTable[i]);
}
(void) fprintf(vis_stdout, "\n");
} /* End of if */
/* form impl Output Array */
implOutputArray = array_alloc(Ntk_Node_t *, array_n(outputArray));
arrayForEachItem(Ntk_Node_t *, outputArray, i, nodePtr) {
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
array_insert(Ntk_Node_t *, implOutputArray, i, implNodePtr);
}
/* number of outputs in consideration */
numOutputs = array_n(outputArray);
/* Main Loop in which the verification is done for each prime. */
for(primeIndex = 0; primeIndex < numOfPrimes; primeIndex++) {
int currentPrime;
/* Read current prime from table */
currentPrime = primeTable[primeIndex];
if (verbose >=2)
(void) fprintf(vis_stdout, "Processing prime %d:\n", currentPrime);
/* update the mdd manager with the first set of output variables */
MddCreateVariables((mdd_manager *)ddManager, numOutputs-bdd_num_vars(ddManager));
/* Obtain the residue bdd for the given prime, assume top id is
* always 0i.e. msbId = 0;
*/
msbId = 0;
bdd_ref(residueDd = bdd_add_residue(ddManager, numOutputs, currentPrime,
msbLsb, msbId));
/* Set the output Id. Needs to be set each time because it gets
* cleared each time.
*/
arrayForEachItem(Ntk_Node_t *, outputArray, i , nodePtr) {
st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
if (msbLsb == 1) {
Ntk_NodeSetMddId(nodePtr, i);
Ntk_NodeSetMddId(implNodePtr, i);
} else {
Ntk_NodeSetMddId(nodePtr, numOutputs - i);
Ntk_NodeSetMddId(implNodePtr, numOutputs - i);
}
}
/* Set the cpu usage lap */
lap = util_cpu_time();
if (verbose >= 1) {
fprintf(vis_stdout, "Specification being built\n");
}
/* the actual composition of the spec. network into the residue ADD
* is done here. The composed ADD return is referenced
*/
specADD = ComposeLayersIntoResidue(specNetwork, specLayerArray, residueDd, outputArray);
if (specADD == NIL(bdd_node)) {
error_append("Composition of spec. failed.\n");
/* Clean up before you leave */
array_free(implOutputArray);
FREE(primeTable);
bdd_recursive_deref(ddManager, residueDd);
return 1; /* error return */
}
/* Store the information in the result structure of the spec.*/
bdd_ref(specADD);
fnMddT = bdd_construct_bdd_t(ddManager, specADD);
specSize = bdd_size(fnMddT);
bdd_free(fnMddT);
ResResidueInfoSetPerPrimeInfo(resultSpec, primeIndex, currentPrime,
(util_cpu_time() - lap)/1000.0, specSize, specADD);
/* Print info regarding this prime if pertinent */
if (verbose >=3) {
(void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->cpuTime);
(void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", specSize);
}
/* Set the cpu usage lap */
lap = util_cpu_time();
/*
* the actual composition of the impl. network into the residue ADD
* is done here. The composed ADD return is referenced
*/
if (verbose >= 1) {
fprintf(vis_stdout, "Implementation being built\n");
}
implADD = ComposeLayersIntoResidue(implNetwork, implLayerArray, residueDd, implOutputArray);
bdd_recursive_deref(ddManager, residueDd);
if (implADD == NIL(bdd_node)) {
error_append("Composition of spec. failed.\n");
/* Clean up before you leave */
bdd_recursive_deref(ddManager, specADD);
array_free(implOutputArray);
FREE(primeTable);
return 1; /* error return */
}
/* Create a permutation array for the specMddId and implMddId input nodes */
permut = ALLOC(int, bdd_num_vars(ddManager));
for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
permut[i] = i;
}
st_foreach_item(inputMatch, stGen, &key, &value) {
nodePtr = (Ntk_Node_t *)key;
implNodePtr = (Ntk_Node_t *)value;
if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
error_append("Input match values do not return");
error_append("valid node pointers.\n");
/* Clean up */
FREE(permut);
FREE(primeTable);
array_free(implOutputArray);
bdd_recursive_deref(ddManager, specADD);
bdd_recursive_deref(ddManager, implADD);
st_free_gen(stGen);
return 1;
}
/* create the array with the impl. vars to be composed with spec. vars. */
specMddId = Ntk_NodeReadMddId(nodePtr);
implMddId = Ntk_NodeReadMddId(implNodePtr);
/* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
* ordering above
*/
#if 0
if (Ntk_NodeReadNumFanouts(nodePtr) != 0) {
assert(specMddId != NTK_UNASSIGNED_MDD_ID);
}
if (Ntk_NodeReadNumFanouts(implNodePtr) != 0) {
assert(implMddId != NTK_UNASSIGNED_MDD_ID);
}
#endif
if ((specMddId != NTK_UNASSIGNED_MDD_ID) &&
(implMddId != NTK_UNASSIGNED_MDD_ID)) {
permut[implMddId] = specMddId;
} else {
assert(specMddId == implMddId);
}
} /* end of st_foreach_item */
/* permute the variables so that the impl variables are replaced by
* spec. variables
*/
bdd_ref(tmpDd = bdd_add_permute(ddManager, implADD, permut));
bdd_recursive_deref(ddManager, implADD);
FREE(permut);
implADD = tmpDd;
if(implADD == NIL(bdd_node)) { /* error */
error_append("Last composition failed,");
error_append("Cannot compose spec. ADD PI vars into Impl. ADD.\n");
FREE(primeTable);
array_free(implOutputArray);
return 1; /* error return */
}
if (verbose > 0) {
(void) fprintf(vis_stdout, "%.2f (secs) spent in residue verification.\n",
(util_cpu_time() - overallLap)/1000.0);
}
/* Store the information in the result structure of the impl.*/
bdd_ref(implADD);
fnMddT = bdd_construct_bdd_t(ddManager, implADD);
implSize = bdd_size(fnMddT);
bdd_free(fnMddT);
ResResidueInfoSetPerPrimeInfo(resultImpl, primeIndex, currentPrime,
(util_cpu_time() - lap)/1000.0, implSize, implADD);
/* Print info regarding this prime if pertinent */
if (verbose >=3) {
(void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->cpuTime);
(void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", implSize);
}
/* Compare the Spec and the Impl composed Dds */
if (ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd !=
ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd) {
ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
(void) fprintf(vis_stdout, "Verification of %s and %s failed.\n",
Res_ResidueInfoReadName(resultSpec),
Res_ResidueInfoReadName(resultImpl));
(void)fprintf(vis_stdout,"The composed ADDs with residue are not the same.\n");
(void)fprintf(vis_stdout,"Verification failed at prime %d.\n", currentPrime);
if (verbose >= 2) {
(void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
(void)fprintf(vis_stdout, "Specification Input Names :\n");
ExtractACubeOfDifference(ddManager, specNetwork, specADD, implADD);
}
/* Clean up before you leave */
bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));
bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
array_free(implOutputArray);
FREE(primeTable);
return 0;
} else {
/* free the result Dd*/
bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));
bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
}
/* reset node Ids of primary inputs */
Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
Ntk_NodeSetMddId(nodePtr, unassignedValue);
}
Ntk_NetworkForEachCombInput(implNetwork, listGen, nodePtr) {
Ntk_NodeSetMddId(nodePtr, unassignedValue);
}
} /* End of the main for-loop */
FREE(primeTable);
array_free(implOutputArray);
/* restore old dynamic reordering values */
bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
if (!dynStatus) {
bdd_dynamic_reordering_disable(ddManager);
}
/* set pass flag if residue verification success and direct verification
* success.
*/
if (((numDirectVerify) &&
(ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS)) ||
(ResResidueInfoReadDirectVerificationSuccess(resultSpec) != RES_FAIL)) {
ResResidueInfoSetSuccess(resultSpec, RES_PASS);
}
if (((numDirectVerify) &&
(ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) ||
(ResResidueInfoReadDirectVerificationSuccess(resultImpl) != RES_FAIL)) {
ResResidueInfoSetSuccess(resultImpl, RES_PASS);
}
return 0;
} /* End of ResidueVerification */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void RestoreOldMddIds | ( | Ntk_Network_t * | network, |
| st_table * | table | ||
| ) | [static] |
Function********************************************************************
Synopsis [A procedure restore MDD Ids from an st table.]
Description [A procedure restore MDD Ids from an st table. This is to leave the network in the state it was in before residue verification was called. The procedure's parameters are the network whose IDs need to be restored and a table to restore from.]
SideEffects [The mdd Ids of the network change.]
SeeAlso [Res_NetworkResidueVerify SaveOldMddIds]
Definition at line 694 of file res.c.
{
lsGen listGen;
Ntk_Node_t *nodePtr;
int value;
if (table != NULL) {
Ntk_NetworkForEachNode(network, listGen, nodePtr) {
if(st_lookup_int(table, (char *)nodePtr, &value)) {
Ntk_NodeSetMddId(nodePtr, value);
} else {
error_append("Node");
error_append(Ntk_NetworkReadName(network));
error_append("should have been in the table.\n");
(void) lsFinish(listGen);
}
}
}
} /* End of RestoreOldMddIds */
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * SaveOldMddIds | ( | Ntk_Network_t * | network | ) | [static] |
Function********************************************************************
Synopsis [Save mdd ids for each node.]
Description [Save old mdd ids for each node and returns a table with the nodes and the Ids.]
SideEffects []
SeeAlso [Res_NetworkResidueVerify RestoreOldMddIds]
Definition at line 1133 of file res.c.
{
st_table *oldMddIdTable;
Ntk_Node_t *nodePtr;
lsGen listGen; /* To iterate over outputList */
oldMddIdTable = st_init_table(st_ptrcmp, st_ptrhash);
if (oldMddIdTable == NULL) return NIL(st_table);
Ntk_NetworkForEachNode(network, listGen, nodePtr) {
st_insert(oldMddIdTable, (char *)nodePtr,
(char *)(long)Ntk_NodeReadMddId(nodePtr));
}
return(oldMddIdTable);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int SetBasicResultInfo | ( | Ntk_Network_t * | specNetwork, |
| Ntk_Network_t * | implNetwork, | ||
| int | numDirectVerify | ||
| ) | [static] |
Function********************************************************************
Synopsis [Create the basic result structures for both the specification and implementation.]
Description [Create the basic result structures for both the specification and implementation. This procedure returns a flag that specifies if the previous verification was a success. If previous information is to be used only the condition that either the same spec and impl were verified before, is allowed. If the previous verification had the same number of directly verified outputs and the verification was a success, a success is returned. The impl. result will be overwritten in any case. Returns a flag that indicates if verification is to be done. The procedure records the number of outputs, inputs, directly verified outputs, spec and impl name. Adds the result structure as a hook to the network. The procedure takes as arguments the spec., the impl. and the number of directly verified outputs.]
SideEffects [Changes the result structure in the 2 networks.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 944 of file res.c.
{
int numInputs;
int numOutputs;
char *specName;
char *implName;
Res_ResidueInfo_t *resultSpec;
Res_ResidueInfo_t *resultImpl;
/* if previous verification to be considered, make sure the
* verification was with the same spec network and the number
* of directly verified outputs are the same.
*/
resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
if (resultSpec != NIL(Res_ResidueInfo_t)) {
if ((strcmp(ResResidueInfoReadNameVerifiedAgainst(resultSpec),
Ntk_NetworkReadName(implNetwork)) == 0) &&
(ResResidueInfoReadNumDirectVerifiedOutputs(resultSpec) ==
numDirectVerify) &&
(ResResidueInfoReadSuccess(resultSpec) == RES_PASS)) {
/* if already verified then done, return success (0) */
return RES_VERIFY_DONE;
}
/* if the above conditions are not satisfied, attempt
* verification again
*/
Ntk_NetworkFreeApplInfo(specNetwork, RES_NETWORK_APPL_KEY );
}
/* create result structure */
resultSpec = (Res_ResidueInfo_t *)
ResNetworkResidueInfoReadOrCreate(specNetwork);
/* add hook to network */
Ntk_NetworkAddApplInfo(specNetwork, RES_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
(void *)resultSpec);
/* number of outputs */
numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
ResResidueInfoSetNumOutputs(resultSpec, numOutputs);
/* number of Inputs */
numInputs = Ntk_NetworkReadNumCombInputs(specNetwork);
ResResidueInfoSetNumInputs(resultSpec, numInputs);
/* impl name */
implName = util_strsav(Ntk_NetworkReadName(implNetwork));
ResResidueInfoSetNameVerifiedAgainst(resultSpec, implName);
/* number of directly verified outputs */
ResResidueInfoSetNumDirectVerifiedOutputs(resultSpec, numDirectVerify);
/*
* Assumption: The implementation residue information is invalid even
* if it does exist and will be overwritten
*/
resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
RES_NETWORK_APPL_KEY);
/* free existing structure */
if (resultImpl != NIL(Res_ResidueInfo_t)) {
Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
}
/* create a new structure for the implementation network */
resultImpl = (Res_ResidueInfo_t *)
ResNetworkResidueInfoReadOrCreate(implNetwork);
Ntk_NetworkAddApplInfo(implNetwork, RES_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
(void *)resultImpl);
/*
* Get some information about the network and initialize the residue
* information for the implementation network.
*/
/* number of outputs */
assert (numOutputs == Ntk_NetworkReadNumCombOutputs(implNetwork));
ResResidueInfoSetNumOutputs(resultImpl, numOutputs);
/* number of Inputs */
assert (numInputs == Ntk_NetworkReadNumCombInputs(implNetwork));
ResResidueInfoSetNumInputs(resultImpl, numInputs);
/* spec name */
specName = util_strsav(Ntk_NetworkReadName(specNetwork));
ResResidueInfoSetNameVerifiedAgainst(resultImpl, specName);
/* number of directly verified outputs */
ResResidueInfoSetNumDirectVerifiedOutputs(resultImpl, numDirectVerify);
return RES_VERIFY_IGNORE_PREV_RESULTS;
} /* End of SetBasicResultInfo */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
int PrimePool[] [static] |
Initial value:
{ 5, 7, 9, 11, 13, 17, 19, 23, 29,
31, 37, 41, 43, 47, 53, 59, 61, 67, 71,
73, 79, 83, 89, 97, 101, 103, 107, 109, 113,
127, 131, 137, 139, 149, 151, 157, 163, 167, 173,
179, 181, 191, 193, 197, 199, 211, 223, 227, 229,
233, 239, 241, 251, 257, 263, 269, 271, 277, 281,
283, 293, 307, 311, 313, 317, 331, 337, 347, 349,
353, 359, 367, 373, 379, 383, 389, 397, 401, 409,
419, 421, 431, 433, 439, 443, 449, 457, 461, 463,
467, 479, 487, 491, 499, 503, 509, 521, 523, 541,
547}
int PrimePoolSize = 100 [static] |
char rcsid [] UNUSED = "$Id: res.c,v 1.55 2009/04/11 21:31:29 fabio Exp $" [static] |
CFile***********************************************************************
FileName [res.c]
PackageName [res]
Synopsis [ The main file that incorporates procedures for residue verification.]
Author [ Kavita Ravi <ravi@boulder.colorado.edu>, 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.]
