#include "absInt.h"
Include dependency graph for absInternal.c:
Go to the source code of this file.
Functions | |
| static mdd_t * | ComputeEGtrue (Abs_VerificationInfo_t *absInfo, mdd_t *careStates) |
| static void | SelectIdentifierVertices (AbsVertexInfo_t *vertexPtr, array_t *result, st_table *visited) |
| Abs_VerificationInfo_t * | Abs_VerificationComputeInfo (Ntk_Network_t *network) |
| AbsVertexInfo_t * | AbsVertexInitialize (void) |
| void | AbsVertexFree (AbsVertexCatalog_t *catalog, AbsVertexInfo_t *v, AbsVertexInfo_t *fromVertex) |
| Abs_VerificationInfo_t * | AbsVerificationInfoInitialize (void) |
| void | AbsVerificationInfoFree (Abs_VerificationInfo_t *v) |
| AbsOptions_t * | AbsOptionsInitialize (void) |
| void | AbsOptionsFree (AbsOptions_t *unit) |
| AbsStats_t * | AbsStatsInitialize (void) |
| void | AbsStatsFree (AbsStats_t *unit) |
| AbsEvalCacheEntry_t * | AbsCacheEntryInitialize (void) |
| void | AbsCacheEntryFree (AbsEvalCacheEntry_t *unit) |
| void | AbsEvalCacheInsert (st_table *solutions, mdd_t *key, mdd_t *result, mdd_t *careSet, boolean approx, boolean replace) |
| boolean | AbsEvalCacheLookup (st_table *solutions, mdd_t *key, mdd_t *careSet, boolean approx, mdd_t **result, boolean *storedApprox) |
| void | AbsVerificationFlushCache (Abs_VerificationInfo_t *absInfo) |
| void | AbsVertexFlushCache (AbsVertexInfo_t *vertexPtr) |
| mdd_t * | AbsImageReadOrCompute (Abs_VerificationInfo_t *absInfo, Img_ImageInfo_t *imageInfo, mdd_t *set, mdd_t *careSet) |
| array_t * | AbsFormulaArrayVerify (Abs_VerificationInfo_t *absInfo, array_t *formulaArray) |
| Fsm_Fsm_t * | AbsCreateReducedFsm (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, Fsm_Fsm_t **approxFsm) |
| boolean | AbsMddEqualModCareSet (mdd_t *f, mdd_t *g, mdd_t *careSet) |
| boolean | AbsMddLEqualModCareSet (mdd_t *f, mdd_t *g, mdd_t *careSet) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: absInternal.c,v 1.30 2005/04/16 04:22:21 fabio Exp $" |
| static int | vertexCounter = 0 |
Function Documentation
| Abs_VerificationInfo_t* Abs_VerificationComputeInfo | ( | Ntk_Network_t * | network | ) |
AutomaticEnd Function********************************************************************
Synopsis [Fill the fields of the data structure storing the information required for the verification process]
SideEffects []
Definition at line 56 of file absInternal.c.
{
Abs_VerificationInfo_t *absInfo;
Ntk_Node_t *nodePtr;
graph_t *partition;
mdd_manager *mddManager;
st_table *table;
lsGen lsgen;
/* Create the data structure to store all the needed info */
absInfo = AbsVerificationInfoInitialize();
/* Fill the data structure in */
AbsVerificationInfoSetNetwork(absInfo, network);
partition = Part_NetworkReadPartition(network);
AbsVerificationInfoSetPartition(absInfo, partition);
mddManager = Part_PartitionReadMddManager(partition);
AbsVerificationInfoSetMddManager(absInfo, mddManager);
/* Compute the state variable pairs */
table = st_init_table(st_numcmp, st_numhash);
Ntk_NetworkForEachLatch(network, lsgen, nodePtr) {
Ntk_Node_t *latchInputPtr;
int mddId, mddId2;
mddId = Ntk_NodeReadMddId(nodePtr);
latchInputPtr = Ntk_NodeReadShadow(nodePtr);
mddId2 = Ntk_NodeReadMddId(latchInputPtr);
st_insert(table, (char *)(long)mddId, (char *)(long)mddId2);
}
AbsVerificationInfoSetStateVars(absInfo, table);
/* Compute the quantify variables */
table = st_init_table(st_numcmp, st_numhash);
Ntk_NetworkForEachInput(network, lsgen, nodePtr) {
int mddId;
mddId = Ntk_NodeReadMddId(nodePtr);
st_insert(table, (char *)(long)mddId, NIL(char));
}
AbsVerificationInfoSetQuantifyVars(absInfo, table);
/* Initalize the catalog to detect common expressions */
AbsVerificationInfoSetCatalog(absInfo, AbsVertexCatalogInitialize());
return absInfo;
} /* End of Abs_VerificationComputeInfo */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsCacheEntryFree | ( | AbsEvalCacheEntry_t * | unit | ) |
Function********************************************************************
Synopsis [Function to de-allocate the AbsEvalCacheEntry]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 526 of file absInternal.c.
{
mdd_free(AbsEvalCacheEntryReadKey(unit));
mdd_free(AbsEvalCacheEntryReadResult(unit));
mdd_free(AbsEvalCacheEntryReadCareSet(unit));
FREE(unit);
} /* End of AbsCacheEntryFree */
Here is the caller graph for this function:
| AbsEvalCacheEntry_t* AbsCacheEntryInitialize | ( | void | ) |
Function********************************************************************
Synopsis [Initalize the entry of the cache for previously computed results]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 501 of file absInternal.c.
{
AbsEvalCacheEntry_t *result;
result = ALLOC(AbsEvalCacheEntry_t, 1);
AbsEvalCacheEntrySetKey(result, NIL(mdd_t));
AbsEvalCacheEntrySetApprox(result, FALSE);
AbsEvalCacheEntrySetComplement(result, 0);
AbsEvalCacheEntrySetResult(result, NIL(mdd_t));
AbsEvalCacheEntrySetCareSet(result, NIL(mdd_t));
return result;
} /* End of AbsCacheEntryInitialize */
Here is the caller graph for this function:
| Fsm_Fsm_t* AbsCreateReducedFsm | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| Fsm_Fsm_t ** | approxFsm | ||
| ) |
Function********************************************************************
Synopsis [Given a FSM and operational graph, simplify the FSM based on topological analysis of the FSM]
SideEffects []
Definition at line 1080 of file absInternal.c.
{
AbsVertexInfo_t *vPtr;
Ntk_Network_t *network;
Ntk_Node_t *nodePtr;
Fsm_Fsm_t *result;
lsGen gen;
array_t *vertexArray;
array_t *nodeArray;
array_t *supportArray;
array_t *inputs;
array_t *latches;
st_table *visited;
int i;
if (vertexPtr == NIL(AbsVertexInfo_t)) {
return NIL(Fsm_Fsm_t);
}
network = AbsVerificationInfoReadNetwork(absInfo);
/* Select the vertices of type "identifier" */
visited = st_init_table(st_ptrcmp, st_ptrhash);
vertexArray = array_alloc(AbsVertexInfo_t *, 0);
SelectIdentifierVertices(vertexPtr, vertexArray, visited);
st_free_table(visited);
if (array_n(vertexArray) == 0) {
array_free(vertexArray);
return NIL(Fsm_Fsm_t);
}
/* Create the array of network nodes corresponding to the identifiers */
visited = st_init_table(st_ptrcmp, st_ptrhash);
nodeArray = array_alloc(Ntk_Node_t *, 0);
arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vPtr) {
nodePtr = Ntk_NetworkFindNodeByName(network, AbsVertexReadName(vPtr));
assert(nodePtr != NIL(Ntk_Node_t));
if (!st_is_member(visited, (char *)nodePtr)) {
array_insert_last(Ntk_Node_t *, nodeArray, nodePtr);
st_insert(visited, (char *)nodePtr, NIL(char));
}
}
array_free(vertexArray);
/* Create the input and array latches to compute the approxFsm */
inputs = array_alloc(Ntk_Node_t *, 0);
Ntk_NetworkForEachInput(network, gen, nodePtr) {
array_insert_last(Ntk_Node_t *, inputs, nodePtr);
}
latches = array_alloc(Ntk_Node_t *, 0);
Ntk_NetworkForEachLatch(network, gen, nodePtr) {
if (st_is_member(visited, (char *)nodePtr)) {
array_insert_last(Ntk_Node_t *, latches, nodePtr);
}
else {
array_insert_last(Ntk_Node_t *, inputs, nodePtr);
}
}
st_free_table(visited);
/* Obtain the approximated system */
*approxFsm = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs,
NIL(array_t));
array_free(inputs);
array_free(latches);
/* Obtain the transitive fanin of the nodes */
supportArray = Ntk_NodeComputeCombinationalSupport(network, nodeArray, FALSE);
array_free(nodeArray);
/* If the transitive fanin of the nodes is empty, return */
if (array_n(supportArray) == 0) {
array_free(supportArray);
return NIL(Fsm_Fsm_t);
}
/* Divide the nodes between inputs and latches and create the final FSM */
inputs = array_alloc(Ntk_Node_t *, 0);
latches = array_alloc(Ntk_Node_t *, 0);
arrayForEachItem(Ntk_Node_t *, supportArray, i, nodePtr) {
if (Ntk_NodeTestIsInput(nodePtr)) {
array_insert_last(Ntk_Node_t *, inputs, nodePtr);
}
else {
assert(Ntk_NodeTestIsLatch(nodePtr));
array_insert_last(Ntk_Node_t *, latches, nodePtr);
}
}
array_free(supportArray);
/* If the collection of inputs and latches is the whole FSM, return */
if (array_n(inputs) == Ntk_NetworkReadNumInputs(network) &&
array_n(latches) == Ntk_NetworkReadNumLatches(network)) {
array_free(inputs);
array_free(latches);
return NIL(Fsm_Fsm_t);
}
result = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs,
NIL(array_t));
/* Clean up */
array_free(inputs);
array_free(latches);
return result;
} /* End of AbsCreateReducedFsm */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsEvalCacheInsert | ( | st_table * | solutions, |
| mdd_t * | key, | ||
| mdd_t * | result, | ||
| mdd_t * | careSet, | ||
| boolean | approx, | ||
| boolean | replace | ||
| ) |
Function********************************************************************
Synopsis [Insert an item in the evaluation cache]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 546 of file absInternal.c.
{
AbsEvalCacheEntry_t *entry;
int complement;
bdd_node *f;
entry = NIL(AbsEvalCacheEntry_t);
f = bdd_get_node(key, &complement);
/* If the replacement is required, delete the element from the table */
if (replace) {
st_delete(solutions, &f, &entry);
mdd_free(AbsEvalCacheEntryReadKey(entry));
mdd_free(AbsEvalCacheEntryReadResult(entry));
mdd_free(AbsEvalCacheEntryReadCareSet(entry));
}
assert(!st_is_member(solutions, (char *)f));
if (entry == NIL(AbsEvalCacheEntry_t)) {
entry = AbsCacheEntryInitialize();
}
AbsEvalCacheEntrySetKey(entry, mdd_dup(key));
AbsEvalCacheEntrySetApprox(entry, approx);
AbsEvalCacheEntrySetComplement(entry, complement);
AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
/* Insert the new entry in the cache */
st_insert(solutions, (char *)f, (char *)entry);
return;
} /* End of AbsEvalCacheInsert */
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean AbsEvalCacheLookup | ( | st_table * | solutions, |
| mdd_t * | key, | ||
| mdd_t * | careSet, | ||
| boolean | approx, | ||
| mdd_t ** | result, | ||
| boolean * | storedApprox | ||
| ) |
Function********************************************************************
Synopsis [Lookup a previous evaluation in the cache]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 598 of file absInternal.c.
{
AbsEvalCacheEntry_t *entry;
bdd_node *f;
int complement;
f = bdd_get_node(key, &complement);
if (st_lookup(solutions, f, &entry)) {
if (complement == AbsEvalCacheEntryReadComplement(entry) &&
(approx || !AbsEvalCacheEntryReadApprox(entry)) &&
mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
*result = AbsEvalCacheEntryReadResult(entry);
if (storedApprox != 0) {
*storedApprox = AbsEvalCacheEntryReadApprox(entry);
}
return TRUE;
}
else {
st_delete(solutions, &f, &entry);
AbsCacheEntryFree(entry);
}
}
return FALSE;
} /* End of AbsEvalCacheLookup */
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* AbsFormulaArrayVerify | ( | Abs_VerificationInfo_t * | absInfo, |
| array_t * | formulaArray | ||
| ) |
Function********************************************************************
Synopsis [Procedure to fire the evaluation process for a collection of formulas given in an array]
Description [This is the main procedure of the package. The command abs_model_check invokes this function. This procedure invokes the procedure AbsSubFormulaVerify]
SideEffects []
Definition at line 794 of file absInternal.c.
{
AbsOptions_t *options;
AbsVertexInfo_t *formulaPtr;
Fsm_Fsm_t *fsm;
array_t *result;
mdd_manager *mddManager;
int fIndex;
int numReorderings;
/* Initialize some variables */
options = AbsVerificationInfoReadOptions(absInfo);
mddManager = AbsVerificationInfoReadMddManager(absInfo);
numReorderings = bdd_read_reorderings(mddManager);
/* Print the configuration of the system */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PIFF) {
(void) fprintf(vis_stdout, "ABS: System with (PI,FF) = (%d,%d)\n",
st_count(AbsVerificationInfoReadQuantifyVars(absInfo)),
st_count(AbsVerificationInfoReadStateVars(absInfo)));
}
/* Create the array of results */
result = array_alloc(AbsVerificationResult_t, array_n(formulaArray));
/* Obtain the fsm representing the complete circuit */
fsm = Fsm_FsmCreateFromNetworkWithPartition(
AbsVerificationInfoReadNetwork(absInfo), NIL(graph_t));
/* Traverse the array of formulas and verify all of them */
arrayForEachItem(AbsVertexInfo_t *, formulaArray, fIndex, formulaPtr) {
Fsm_Fsm_t *localSystem;
Fsm_Fsm_t *approxSystem;
array_t *stateVarIds;
mdd_t *initialStates;
mdd_t *careStates;
long cpuTime;
int numBddVars;
int mddId;
int i;
/* Variable Initialization */
approxSystem = NIL(Fsm_Fsm_t);
/* Set the cpu-time lap */
cpuTime = util_cpu_time();
/* Print the labeled operational graph */
if (AbsOptionsReadVerbosity(options) & ABS_VB_GRAPH) {
(void) fprintf(vis_stdout, "ABS: === Labeled Operational Graph ===\n");
AbsVertexPrint(formulaPtr, NIL(st_table), TRUE,
AbsOptionsReadVerbosity(options));
(void) fprintf(vis_stdout, "ABS: === End of Graph ===\n");
}
/* Simplify the system with respect to the given formula */
localSystem = AbsCreateReducedFsm(absInfo, formulaPtr, &approxSystem);
if (localSystem == NIL(Fsm_Fsm_t)) {
localSystem = fsm;
}
if (approxSystem == NIL(Fsm_Fsm_t)) {
approxSystem = fsm;
}
AbsVerificationInfoSetFsm(absInfo, localSystem);
/* Compute the number of bdd variables needed to encode the state space */
stateVarIds = Fsm_FsmReadPresentStateVars(localSystem);
numBddVars = 0;
arrayForEachItem(int, stateVarIds, i, mddId) {
array_t *mvarList = mdd_ret_mvar_list(mddManager);
mvar_type mddVar = array_fetch(mvar_type, mvarList, mddId);
numBddVars += mddVar.encode_length;
}
AbsVerificationInfoSetNumStateVars(absInfo, numBddVars);
AbsVerificationInfoSetApproxFsm(absInfo, approxSystem);
if (AbsOptionsReadVerbosity(options) & ABS_VB_SIMPLE) {
(void) fprintf(vis_stdout,
"ABS: System Simplified from %d to %d latches\n",
array_n(Fsm_FsmReadPresentStateVars(fsm)),
array_n(Fsm_FsmReadPresentStateVars(localSystem)));
(void) fprintf(vis_stdout,
"ABS: System Approximated by %d of %d latches\n",
array_n(Fsm_FsmReadPresentStateVars(approxSystem)),
array_n(Fsm_FsmReadPresentStateVars(localSystem)));
}
/* Compute reachability if requested */
if (AbsOptionsReadReachability(options)) {
mdd_t *reachableStates;
long cpuTime;
cpuTime = util_cpu_time();
reachableStates = Fsm_FsmComputeReachableStates(localSystem, 0, 1, 0, 0,
0, 0, 0,Fsm_Rch_Default_c, 0, 0, NIL(array_t), FALSE,
NIL(array_t));
if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
(void) fprintf(vis_stdout, "ABS: %7.1f secs spent in reachability \n",
(util_cpu_time() - cpuTime)/1000.0);
}
/* Print the number of reachable states */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PRCH) {
array_t *sVars;
sVars = Fsm_FsmReadPresentStateVars(localSystem);
(void) fprintf(vis_stdout, "ABS: System with %.0f reachable states.\n",
mdd_count_onset(mddManager, reachableStates, sVars));
}
careStates = reachableStates;
} /* End of reachability analysis */
else {
careStates = mdd_one(mddManager);
}
/* Compute the initial states */
initialStates = Fsm_FsmComputeInitialStates(localSystem);
if (initialStates == NIL(mdd_t)) {
(void) fprintf(vis_stdout, "** abs error: Unable to compute initial states.\n");
(void) fprintf(vis_stdout, "ABS: %s\n", error_string());
AbsVerificationInfoFree(absInfo);
array_free(result);
/* Deallocate the FSM if the system was reduced */
if (localSystem != fsm) {
Fsm_FsmFree(localSystem);
}
return NIL(array_t);
}
/* Set the don't care information */
if (AbsVerificationInfoReadCareSet(absInfo) != NIL(mdd_t)) {
mdd_free(AbsVerificationInfoReadCareSet(absInfo));
}
AbsVerificationInfoSetCareSet(absInfo, careStates);
if (AbsVerificationInfoReadTmpCareSet(absInfo) != NIL(mdd_t)) {
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
}
AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
/* Compute the formula EG(true) if required */
if (AbsOptionsReadEnvelope(options)) {
mdd_t *newCareStates;
mdd_t *tmp1;
newCareStates = ComputeEGtrue(absInfo, careStates);
tmp1 = mdd_and(newCareStates, careStates, 1, 1);
mdd_free(careStates);
mdd_free(newCareStates);
careStates = tmp1;
AbsVerificationInfoSetCareSet(absInfo, careStates);
}
/* Print verbosity message */
if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
(void) fprintf(vis_stdout, "ABS: === Initial Verification ===\n");
}
/* Create the initial evaluation of the formula */
AbsSubFormulaVerify(absInfo, formulaPtr);
assert(!AbsVertexReadTrueRefine(formulaPtr));
/* Print verbosity message */
if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
(void) fprintf(vis_stdout, "ABS: === End of Initial Verification ===\n");
}
/* Print cpu-time information */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
(void) fprintf(vis_stdout, "ABS: Initial verification: %7.1f secs.\n",
(util_cpu_time() - cpuTime)/1000.0);
}
/* Check if the initial states satisfy the formula */
if (mdd_lequal(initialStates, AbsVertexReadSat(formulaPtr), 1, 1)) {
array_insert(int, result, fIndex, trueVerification_c);
}
else {
if (AbsVertexReadGlobalApprox(formulaPtr)) {
mdd_t *goalSet;
mdd_t *refinement;
/*
* Compute the set of states remaining in the goal. We are assuming
* that the parity of the top vertex is negative
*/
assert(!AbsVertexReadPolarity(formulaPtr));
/* Compute the initial goal set */
goalSet = mdd_and(initialStates, AbsVertexReadSat(formulaPtr), 1, 0);
/* Notify that the refinement process is beginning */
if (AbsOptionsReadVerbosity(options) &ABS_VB_PPROGR) {
(void) fprintf(vis_stdout,
"ABS: Verification has been approximated. ");
(void) fprintf(vis_stdout, "Beginning approximation refinement\n");
}
/* Print the number of states to refine */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PRINIT) {
array_t *sVars;
sVars = Fsm_FsmReadPresentStateVars(fsm);
(void) fprintf(vis_stdout,
"ABS: %.0f states out of %.0f to be refined\n",
mdd_count_onset(mddManager, goalSet, sVars),
mdd_count_onset(mddManager, initialStates, sVars));
}
/* Effectively perform the refinement */
refinement = AbsSubFormulaRefine(absInfo, formulaPtr, goalSet);
/* Insert the outcome of the refinement in the solution */
if (mdd_is_tautology(refinement, 0)) {
array_insert(int, result, fIndex, trueVerification_c);
}
else {
if (!AbsVertexReadTrueRefine(formulaPtr)) {
array_insert(int, result, fIndex, inconclusiveVerification_c);
}
else {
array_insert(int, result, fIndex, falseVerification_c);
}
}
mdd_free(goalSet);
mdd_free(refinement);
}
else {
array_insert(int, result, fIndex, falseVerification_c);
}
}
mdd_free(initialStates);
/* Print cpu-time information */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
(void) fprintf(vis_stdout, "ABS: Formula #%d verified in %7.1f secs.\n",
fIndex + 1, (util_cpu_time() - cpuTime)/1000.0);
}
/* Print the number of states in the on set of Sat */
if (AbsOptionsReadVerbosity(options) & ABS_VB_TSAT) {
array_t *sVars;
sVars = Fsm_FsmReadPresentStateVars(localSystem);
(void) fprintf(vis_stdout, "ABS: %.0f States in sat of the formula.\n",
mdd_count_onset(mddManager, AbsVertexReadSat(formulaPtr),
sVars));
}
/* Clean up */
AbsVertexFlushCache(formulaPtr);
AbsVerificationFlushCache(absInfo);
if (approxSystem != fsm) {
Fsm_FsmFree(approxSystem);
}
if (localSystem != fsm) {
Fsm_FsmFree(localSystem);
}
} /* End of the loop over the array of formulas to be verified */
/* Set the number of reorderings in the stats */
AbsStatsSetNumReorderings(AbsVerificationInfoReadStats(absInfo),
bdd_read_reorderings(mddManager) - numReorderings);
/* Clean up */
Fsm_FsmFree(fsm);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* AbsImageReadOrCompute | ( | Abs_VerificationInfo_t * | absInfo, |
| Img_ImageInfo_t * | imageInfo, | ||
| mdd_t * | set, | ||
| mdd_t * | careSet | ||
| ) |
Function********************************************************************
Synopsis [Read an image computation from the cache, and if it is not present, invoke the image algorithm and store its result]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 716 of file absInternal.c.
{
AbsEvalCacheEntry_t *entry;
st_table *table;
bdd_node *f;
mdd_t *result;
long cpuTime;
int complement;
entry = NIL(AbsEvalCacheEntry_t);
table = AbsVerificationInfoReadImageCache(absInfo);
f = bdd_get_node(set, &complement);
/* See if the table has been created */
if (table == NIL(st_table)) {
table = st_init_table(st_ptrcmp, st_ptrhash);
AbsVerificationInfoSetImageCache(absInfo, table);
}
else {
/* Look up for the operation */
if (st_lookup(table, f, &entry)) {
if (complement == AbsEvalCacheEntryReadComplement(entry) &&
mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
result = mdd_dup(AbsEvalCacheEntryReadResult(entry));
return result;
}
else {
st_delete(table, &f, &entry);
mdd_free(AbsEvalCacheEntryReadKey(entry));
mdd_free(AbsEvalCacheEntryReadResult(entry));
mdd_free(AbsEvalCacheEntryReadCareSet(entry));
}
}
}
/* The result has not been found. Compute it and insert it in the cache */
cpuTime = util_cpu_time();
result = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, set, set, careSet);
AbsStatsReadImageCpuTime(AbsVerificationInfoReadStats(absInfo))+=
util_cpu_time() - cpuTime;
AbsStatsReadExactImage(AbsVerificationInfoReadStats(absInfo))++;
if (entry == NIL(AbsEvalCacheEntry_t)) {
entry = AbsCacheEntryInitialize();
}
AbsEvalCacheEntrySetKey(entry, mdd_dup(set));
AbsEvalCacheEntrySetComplement(entry, complement);
AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
/* Insert the new entry in the cache */
st_insert(table, (char *)f, (char *)entry);
AbsStatsReadImageCacheEntries(AbsVerificationInfoReadStats(absInfo))++;
return result;
} /* End of AbsImageReadOrCompute */
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean AbsMddEqualModCareSet | ( | mdd_t * | f, |
| mdd_t * | g, | ||
| mdd_t * | careSet | ||
| ) |
Function********************************************************************
Synopsis [Check if two functions are identical modulo the don't care function provided]
SideEffects []
Definition at line 1203 of file absInternal.c.
{
boolean result = mdd_equal_mod_care_set(f, g, careSet);
return result;
} /* End of AbsMddEqualModCareSet */
Here is the caller graph for this function:
| boolean AbsMddLEqualModCareSet | ( | mdd_t * | f, |
| mdd_t * | g, | ||
| mdd_t * | careSet | ||
| ) |
Function********************************************************************
Synopsis [Check if function f is contained in function g but taking into account the provided care set]
SideEffects []
Definition at line 1221 of file absInternal.c.
{
boolean result = mdd_lequal_mod_care_set(f, g, 1, 1, careSet);
return result;
} /* End of AbsMddLEqualModCareSet */
Here is the caller graph for this function:
| void AbsOptionsFree | ( | AbsOptions_t * | unit | ) |
Function********************************************************************
Synopsis [Deallocate the structure storing the value of the options.]
SideEffects []
SeeAlso [AbsOptions]
Definition at line 416 of file absInternal.c.
{
if (AbsOptionsReadFileName(unit) != NIL(char)) {
FREE(AbsOptionsReadFileName(unit));
}
if (AbsOptionsReadFairFileName(unit) != NIL(char)) {
FREE(AbsOptionsReadFairFileName(unit));
}
FREE(unit);
return;
} /* End of AbsOptionsInitialize */
Here is the caller graph for this function:
| AbsOptions_t* AbsOptionsInitialize | ( | void | ) |
Function********************************************************************
Synopsis [Allocate the structure to store the value of the options.]
SideEffects []
SeeAlso [AbsOptions]
Definition at line 386 of file absInternal.c.
{
AbsOptions_t *result;
result = ALLOC(AbsOptions_t, 1);
AbsOptionsSetVerbosity(result, 0);
AbsOptionsSetTimeOut(result, 0);
AbsOptionsSetFileName(result, NIL(char));
AbsOptionsSetReachability(result, FALSE);
AbsOptionsSetFairFileName(result, NIL(char));
AbsOptionsSetExact(result, FALSE);
AbsOptionsSetPrintStats(result, FALSE);
AbsOptionsSetMinimizeIterate(result, FALSE);
AbsOptionsSetNegateFormula(result, FALSE);
AbsOptionsSetPartApprox(result, FALSE);
return result;
} /* End of AbsOptionsInitialize */
Here is the caller graph for this function:
| void AbsStatsFree | ( | AbsStats_t * | unit | ) |
Function********************************************************************
Synopsis [Function to free the AbsStats structure]
SideEffects []
SeeAlso [AbsStats]
Definition at line 485 of file absInternal.c.
{
FREE(unit);
} /* End of AbsStatsFree */
Here is the caller graph for this function:
| AbsStats_t* AbsStatsInitialize | ( | void | ) |
Function********************************************************************
Synopsis [Allocate the data structure storing the different statistics measurements collected by the algorithms]
SideEffects []
SeeAlso [AbsStats]
Definition at line 443 of file absInternal.c.
{
AbsStats_t *result;
result = ALLOC(AbsStats_t, 1);
AbsStatsSetNumReorderings(result, 0);
AbsStatsSetEvalFixedPoint(result, 0);
AbsStatsSetEvalAnd(result, 0);
AbsStatsSetEvalNot(result, 0);
AbsStatsSetEvalPreImage(result, 0);
AbsStatsSetEvalIdentifier(result, 0);
AbsStatsSetEvalVariable(result, 0);
AbsStatsSetRefineFixedPoint(result, 0);
AbsStatsSetRefineAnd(result, 0);
AbsStatsSetRefineNot(result, 0);
AbsStatsSetRefinePreImage(result, 0);
AbsStatsSetRefineIdentifier(result, 0);
AbsStatsSetRefineVariable(result, 0);
AbsStatsSetExactPreImage(result, 0);
AbsStatsSetApproxPreImage(result, 0);
AbsStatsSetExactImage(result, 0);
AbsStatsSetPreImageCacheEntries(result, 0);
AbsStatsSetImageCacheEntries(result, 0);
AbsStatsSetImageCpuTime(result, 0);
AbsStatsSetPreImageCpuTime(result, 0);
AbsStatsSetAppPreCpuTime(result, 0);
return result;
} /* End of AbsStatsInitialize */
Here is the caller graph for this function:
| void AbsVerificationFlushCache | ( | Abs_VerificationInfo_t * | absInfo | ) |
Function********************************************************************
Synopsis [Delete all the entries in the evaluation cache]
SideEffects []
SeeAlso [AbsEvalCacheEntry]
Definition at line 641 of file absInternal.c.
{
AbsEvalCacheEntry_t *value;
st_table *table;
bdd_node *key;
st_generator *stgen;
table = AbsVerificationInfoReadImageCache(absInfo);
if (table == NIL(st_table)) {
return;
}
st_foreach_item(table, stgen, &key, &value) {
AbsCacheEntryFree(value);
}
st_free_table(table);
AbsVerificationInfoSetImageCache(absInfo, NIL(st_table));
return;
} /* End of AbsVerificationFlushCache */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsVerificationInfoFree | ( | Abs_VerificationInfo_t * | v | ) |
Function********************************************************************
Synopsis [Free the structure storing the verification info.]
Description [Some of the fields in this structure are owned by this package and some others are simply pointers to a data structure that is owned by some other package. Refer to the definition of Abs_VerificationInfo_t to know which fields are onwed and which are not.]
SideEffects []
SeeAlso [AbsVerificationInfo AbsVertexInfo]
Definition at line 329 of file absInternal.c.
{
if (AbsVerificationInfoReadStateVars(v) != NIL(st_table)) {
st_free_table(AbsVerificationInfoReadStateVars(v));
}
if (AbsVerificationInfoReadQuantifyVars(v) != NIL(st_table)) {
st_free_table(AbsVerificationInfoReadQuantifyVars(v));
}
if (AbsVerificationInfoReadImageCache(v) != NIL(st_table)) {
AbsEvalCacheEntry_t *value;
bdd_node *key;
st_generator *stgen;
st_foreach_item(AbsVerificationInfoReadImageCache(v), stgen,
&key, &value) {
AbsCacheEntryFree(value);
}
st_free_table(AbsVerificationInfoReadImageCache(v));
}
if (AbsVerificationInfoReadCareSet(v) != NIL(mdd_t)) {
mdd_free(AbsVerificationInfoReadCareSet(v));
}
if (AbsVerificationInfoReadTmpCareSet(v) != NIL(mdd_t)) {
mdd_free(AbsVerificationInfoReadTmpCareSet(v));
}
if (AbsVerificationInfoReadCatalog(v) != NIL(AbsVertexCatalog_t)) {
AbsVertexCatalogFree(AbsVerificationInfoReadCatalog(v));
}
AbsStatsFree(AbsVerificationInfoReadStats(v));
FREE(v);
/*
* The options field is not freed since it is assumed that it has been
* allocated outside the AbsVerificationInitialize procedure
*/
return;
} /* End of AbsVerificationInfoFree */
Here is the call graph for this function:
Here is the caller graph for this function:
| Abs_VerificationInfo_t* AbsVerificationInfoInitialize | ( | void | ) |
Function********************************************************************
Synopsis [Allocates the data structure to store information about the general verification process.]
SideEffects []
SeeAlso [AbsVerificationInfo AbsVertexInfo]
Definition at line 289 of file absInternal.c.
{
Abs_VerificationInfo_t *result;
result = ALLOC(Abs_VerificationInfo_t, 1);
AbsVerificationInfoSetNetwork(result, NIL(Ntk_Network_t));
AbsVerificationInfoSetPartition(result, NIL(graph_t));
AbsVerificationInfoSetFsm(result, NIL(Fsm_Fsm_t));
AbsVerificationInfoSetNumStateVars(result, 0);
AbsVerificationInfoSetApproxFsm(result, NIL(Fsm_Fsm_t));
AbsVerificationInfoSetStateVars(result, NIL(st_table));
AbsVerificationInfoSetQuantifyVars(result, NIL(st_table));
AbsVerificationInfoSetCareSet(result, NIL(mdd_t));
AbsVerificationInfoSetTmpCareSet(result, NIL(mdd_t));
AbsVerificationInfoSetImageCache(result, NIL(st_table));
AbsVerificationInfoSetMddManager(result, NIL(mdd_manager));
AbsVerificationInfoSetCatalog(result, NIL(AbsVertexCatalog_t));
AbsVerificationInfoSetStats(result, AbsStatsInitialize());
AbsVerificationInfoSetOptions(result, NIL(AbsOptions_t));
return result;
} /* End of AbsVerificationInfoInitialize */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsVertexFlushCache | ( | AbsVertexInfo_t * | vertexPtr | ) |
Function********************************************************************
Synopsis [Delete all the entries stored in the local evaluation cache that a given vertex has attached to it]
SideEffects []
SeeAlso [AbsVertexInfo]
Definition at line 676 of file absInternal.c.
{
if (AbsVertexReadType(vertexPtr) == preImage_c) {
if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
AbsEvalCacheEntry_t *value;
bdd_node *key;
st_generator *stgen;
st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key,
&value) {
AbsCacheEntryFree(value);
}
st_free_table(AbsVertexReadSolutions(vertexPtr));
AbsVertexSetSolutions(vertexPtr, NIL(st_table));
}
}
if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
AbsVertexFlushCache(AbsVertexReadLeftKid(vertexPtr));
}
if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
AbsVertexFlushCache(AbsVertexReadRightKid(vertexPtr));
}
return;
} /* End of AbsVertexFlushCache */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsVertexFree | ( | AbsVertexCatalog_t * | catalog, |
| AbsVertexInfo_t * | v, | ||
| AbsVertexInfo_t * | fromVertex | ||
| ) |
Function********************************************************************
Synopsis [Free a structure of type AbsVertexInfo.]
Description [optional]
SideEffects []
SeeAlso [AbsVertexInfo_t]
Definition at line 171 of file absInternal.c.
{
/* Decrement the number of references */
AbsVertexReadRefs(v)--;
/* Remove the pointer from its parent to itself */
if (fromVertex != NIL(AbsVertexInfo_t)) {
AbsVertexInfo_t *result;
lsGen listGen;
lsHandle item, toDelete;
lsGeneric userData;
listGen = lsStart(AbsVertexReadParent(v));
toDelete = (lsHandle) 0;
while(toDelete == (lsHandle) 0 &&
lsNext(listGen, &result, &item) == LS_OK) {
if (result == fromVertex) {
toDelete = item;
}
}
lsFinish(listGen);
if (toDelete != (lsHandle)0) {
lsRemoveItem(toDelete, &userData);
}
}
/* If it is not the last reference we are done */
if (AbsVertexReadRefs(v) != 0) {
return;
}
/* Vertices that need recursion over the leftKid */
if (AbsVertexReadType(v) == fixedPoint_c ||
AbsVertexReadType(v) == and_c ||
AbsVertexReadType(v) == xor_c ||
AbsVertexReadType(v) == xnor_c ||
AbsVertexReadType(v) == not_c ||
AbsVertexReadType(v) == preImage_c) {
AbsVertexFree(catalog, AbsVertexReadLeftKid(v), v);
}
/* Vertices that need recursion over the rightKid */
if (AbsVertexReadType(v) == and_c ||
AbsVertexReadType(v) == xor_c ||
AbsVertexReadType(v) == xnor_c) {
AbsVertexFree(catalog, AbsVertexReadRightKid(v), v);
}
/* Remove the vertex from the catalog */
AbsCatalogDelete(catalog, v);
/* The variable vertex does not reference the sat set */
if (AbsVertexReadType(v) != variable_c &&
AbsVertexReadSat(v) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(v));
}
if (AbsVertexReadType(v) == variable_c &&
AbsVertexReadGoalSet(v) != NIL(mdd_t)) {
mdd_free(AbsVertexReadGoalSet(v));
}
lsDestroy(AbsVertexReadParent(v), (void (*)(lsGeneric))0);
/* Free the union fields depending on the type of vertex */
if (AbsVertexReadType(v) == preImage_c) {
if (AbsVertexReadSolutions(v) != NIL(st_table)) {
AbsEvalCacheEntry_t *value;
bdd_node *key;
st_generator *stgen;
st_foreach_item(AbsVertexReadSolutions(v), stgen, &key, &value) {
AbsCacheEntryFree(value);
}
st_free_table(AbsVertexReadSolutions(v));
}
}
else if (AbsVertexReadType(v) == fixedPoint_c) {
if (AbsVertexReadRings(v) != NIL(array_t)) {
mdd_t *unit;
int i;
arrayForEachItem(mdd_t *, AbsVertexReadRings(v), i, unit) {
mdd_free(unit);
}
array_free(AbsVertexReadRings(v));
}
if (AbsVertexReadRingApprox(v) != NIL(array_t)) {
array_free(AbsVertexReadRingApprox(v));
}
if (AbsVertexReadSubApprox(v) != NIL(array_t)) {
array_free(AbsVertexReadSubApprox(v));
}
}
else if (AbsVertexReadType(v) == identifier_c) {
FREE(AbsVertexReadName(v));
FREE(AbsVertexReadValue(v));
}
/* Deallocate the memory for the structure itself */
FREE(v);
} /* End of AbsVertexFree */
Here is the call graph for this function:
Here is the caller graph for this function:
| AbsVertexInfo_t* AbsVertexInitialize | ( | void | ) |
Function********************************************************************
Synopsis [Create a new structure of type VertexInfo and initialize all its fields.]
SideEffects []
SeeAlso [AbsVertexInfo_t]
Definition at line 122 of file absInternal.c.
{
AbsVertexInfo_t *result;
result = ALLOC(AbsVertexInfo_t, 1);
AbsVertexSetType(result, false_c);
AbsVertexSetId(result, vertexCounter++);
AbsVertexSetSat(result, NIL(mdd_t));
AbsVertexSetRefs(result, 1);
AbsVertexSetServed(result, 0);
AbsVertexSetPolarity(result, FALSE);
AbsVertexSetDepth(result, -1);
AbsVertexSetLocalApprox(result, FALSE);
AbsVertexSetGlobalApprox(result, FALSE);
AbsVertexSetConstant(result, FALSE);
AbsVertexSetTrueRefine(result, FALSE);
AbsVertexSetLeftKid(result, NIL(AbsVertexInfo_t));
AbsVertexSetRightKid(result, NIL(AbsVertexInfo_t));
result->parent = lsCreate();
/* Not all of these need to be initialized, but to be sure... */
AbsVertexSetSolutions(result, NIL(st_table));
AbsVertexSetVarId(result, 0);
AbsVertexSetFpVar(result, NIL(AbsVertexInfo_t));
AbsVertexSetVarId(result, 0);
AbsVertexSetGoalSet(result, NIL(mdd_t));
AbsVertexSetRings(result, NIL(array_t));
AbsVertexSetRingApprox(result, NIL(array_t));
AbsVertexSetSubApprox(result, NIL(array_t));
AbsVertexSetUseExtraCareSet(result, FALSE);
AbsVertexSetName(result, NIL(char));
AbsVertexSetValue(result, NIL(char));
return result;
} /* End of AbsVertexInitialize */
Here is the caller graph for this function:
| static mdd_t * ComputeEGtrue | ( | Abs_VerificationInfo_t * | absInfo, |
| mdd_t * | careStates | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Compute the verification of the formula EG(true)]
Description [This is provided as an option. The computation of this formula might reduce the state space to be explored. Specifically, it gets rid of states that do not have any successor as well as any other states leading to them. The benefit of this computation is unclear, specially because some tools that read verilog and produce blif-mv might produce a self loop in every state for which no transition is specified. If that is so, there will never be a state without a successor.]
SideEffects []
Definition at line 1250 of file absInternal.c.
{
AbsOptions_t *options;
AbsVertexInfo_t *vertex;
Ctlp_Formula_t *egFormula;
Ctlp_Formula_t *trueFormula;
mdd_manager *mddManager;
array_t *inputTranslation;
array_t *outputTranslation;
mdd_t *envelope;
long cpuTime;
cpuTime = util_cpu_time();
options = AbsVerificationInfoReadOptions(absInfo);
mddManager = AbsVerificationInfoReadMddManager(absInfo);
/* Compute the EG(true) fixed point */
trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void));
egFormula = Ctlp_FormulaCreate(Ctlp_EG_c, trueFormula, NIL(void));
/* Translate into the graph representation */
inputTranslation = array_alloc(Ctlp_Formula_t *, 1);
array_insert(Ctlp_Formula_t *, inputTranslation, 0, egFormula);
outputTranslation = AbsCtlFormulaArrayTranslate(absInfo, inputTranslation,
NIL(array_t));
vertex = array_fetch(AbsVertexInfo_t *, outputTranslation, 0);
array_free(inputTranslation);
array_free(outputTranslation);
/* Evaluate the formula */
AbsSubFormulaVerify(absInfo, vertex);
envelope = mdd_dup(AbsVertexReadSat(vertex));
/* Clean up */
Ctlp_FormulaFree(egFormula);
AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), vertex,
NIL(AbsVertexInfo_t));
/* Print the number of envelope states */
if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
array_t *sVars;
mdd_t *states;
sVars = Fsm_FsmReadPresentStateVars(AbsVerificationInfoReadFsm(absInfo));
states = mdd_and(envelope, careStates, 1, 1);
(void) fprintf(vis_stdout, "ABS: Envelope with %.0f care states.\n",
mdd_count_onset(mddManager, states, sVars));
mdd_free(states);
}
if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
(void) fprintf(vis_stdout, "ABS: %7.1f secs computing EG(TRUE)\n",
(util_cpu_time() - cpuTime)/1000.0);
}
return envelope;
} /* End of ComputeEGtrue */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void SelectIdentifierVertices | ( | AbsVertexInfo_t * | vertexPtr, |
| array_t * | result, | ||
| st_table * | visited | ||
| ) | [static] |
Function********************************************************************
Synopsis [Given a graph, select the set of vertices that represent identifiers]
SideEffects []
Definition at line 1320 of file absInternal.c.
{
assert(result != NIL(array_t));
if (vertexPtr == NIL(AbsVertexInfo_t)) {
return;
}
if (st_is_member(visited, (char *)vertexPtr)) {
return;
}
if (AbsVertexReadType(vertexPtr) == identifier_c) {
array_insert_last(AbsVertexInfo_t *, result, vertexPtr);
st_insert(visited, (char *)vertexPtr, NIL(char));
return;
}
else {
SelectIdentifierVertices(AbsVertexReadLeftKid(vertexPtr), result, visited);
SelectIdentifierVertices(AbsVertexReadRightKid(vertexPtr), result, visited);
}
st_insert(visited, (char *)vertexPtr, NIL(char));
return;
} /* End of SelectIdentifierVertices */
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: absInternal.c,v 1.30 2005/04/16 04:22:21 fabio Exp $" [static] |
CFile***********************************************************************
FileName [absInternal.c]
PackageName [abs]
Synopsis [Miscelaneous functions to handle caches, don't care conditions, initialization and deallocation of structures, etc]
Author [Abelardo Pardo <abel@vlsi.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.]
Definition at line 19 of file absInternal.c.
int vertexCounter = 0 [static] |
Definition at line 29 of file absInternal.c.
