#include "absInt.h"
Include dependency graph for absEvaluate.c:
Go to the source code of this file.
Functions | |
| static void | EvaluateVariable (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static void | EvaluateIdentifier (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static void | EvaluateNot (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static void | EvaluateAnd (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static void | EvaluateFixedPoint (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static void | EvaluatePreImage (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static mdd_t * | OverApproximatePreImageWithSubFSM (Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) |
| static mdd_t * | OverApproximatePreImageWithBddSubsetting (Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) |
| static mdd_t * | UnderApproximatePreImageWithBddSubsetting (Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) |
| void | AbsSubFormulaVerify (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| void | AbsFormulaScheduleEvaluation (AbsVertexInfo_t *current, AbsVertexInfo_t *limit) |
| mdd_t * | AbsComputeOptimalIterate (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *lowerIterate, mdd_t *upperIterate) |
| boolean | AbsFixedPointIterate (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, int iterateIndex) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: absEvaluate.c,v 1.19 2002/09/19 05:25:00 fabio Exp $" |
Function Documentation
| mdd_t* AbsComputeOptimalIterate | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | lowerIterate, | ||
| mdd_t * | upperIterate | ||
| ) |
Function********************************************************************
Synopsis [Function to minimize the size of the BDD representing one iteration of the fix-point]
Description [This function is simply to encapsulate the call to the minimize procedure and have a simple place where to explore the different choices when it comes to select upper and lower bounds for a function. In the case of fix-point evaluation, there are several bounds that can be used to look for a compact representation, this is the function in which that experimenting should be included]
SideEffects []
SeeAlso [AbsFixedPointIterate]
Definition at line 207 of file absEvaluate.c.
{
mdd_t *tmp;
mdd_t *result;
if (AbsOptionsReadMinimizeIterate(AbsVerificationInfoReadOptions(absInfo))
&& AbsVertexReadUseExtraCareSet(vertexPtr)) {
/*
* For this computation we have three ingredients and a handfull of
* choices. The ingredients are the sets newIterate, iterate and
* careSet. The goal is to compute an interval delimited by two boolean
* functions and then call the function bdd_between to try to obtain
* the best bdd in size inside that interval. To compute the extremes
* of the interval there are several choices. For example, the care set
* can be used in the lower bound of the interval or in both
* bounds. The bigger the interval the more choice the function
* bdd_between has to minimize, however, this does not turn into a
* better result.
*
* Current Choice: [newIterate * iterate', newIterate]
*/
tmp = mdd_and(lowerIterate, upperIterate, 0, 1);
result = bdd_between(tmp, upperIterate);
/* This line for debugging purposes, should be removed
(void) fprintf(vis_stdout,
"newIterate : %d, Diff : %d, result %d\n",
mdd_size(upperIterate), mdd_size(tmp),
mdd_size(result)); */
mdd_free(tmp);
}
else {
result = mdd_dup(upperIterate);
}
return result;
} /* End of AbsComputeOptimalIterate */
Here is the caller graph for this function:
| boolean AbsFixedPointIterate | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| int | iterateIndex | ||
| ) |
Function********************************************************************
Synopsis [Function to compute the iteration in a fix-point computation]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 261 of file absEvaluate.c.
{
AbsVertexInfo_t *subFormula;
boolean keepIterating;
boolean globalApprox;
int stepCount;
long verbosity;
mdd_t *iterate;
mdd_t *newIterate;
mdd_t *careSet;
/* Do not allow to iterate from the middle of a fixed point computation */
assert(iterateIndex == array_n(AbsVertexReadRings(vertexPtr)) - 1);
careSet = AbsVerificationInfoReadCareSet(absInfo);
/* Check if the set of iterates has already converged */
if (array_n(AbsVertexReadRings(vertexPtr)) > 1) {
mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateIndex);
mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
return FALSE;
}
iterate = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
}
else {
iterate = AbsVertexFetchRing(vertexPtr, iterateIndex);
}
newIterate = AbsVertexFetchRing(vertexPtr, iterateIndex);
/* Variable initialization */
keepIterating = TRUE;
stepCount = iterateIndex;
verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
subFormula = AbsVertexReadLeftKid(vertexPtr);
globalApprox = AbsVertexFetchSubApprox(vertexPtr, iterateIndex);
/* Main loop for the fixed point computation */
while (keepIterating) {
mdd_t *best;
/*
* Given newIterate, iterate and CareSet, if the use of extra care set is
* enabled, choose the best candidate as the value of the iterate.
*/
best = AbsComputeOptimalIterate(absInfo, vertexPtr, iterate, newIterate);
/* Print the iterates */
if ((verbosity & ABS_VB_PITER) || (verbosity & ABS_VB_ITSIZ)) {
(void) fprintf(vis_stdout, "ABS: New Iterate: ");
if (verbosity & ABS_VB_ITSIZ) {
(void) fprintf(vis_stdout, "%d -> %d\n", mdd_size(newIterate),
mdd_size(best));
}
else {
(void) fprintf(vis_stdout, "\n");
}
if (verbosity & ABS_VB_PITER) {
AbsBddPrintMinterms(newIterate);
}
}
/* Store the value of the variable */
AbsVertexSetSat(AbsVertexReadFpVar(vertexPtr), best);
/* Mark the proper sub-formulas for re-evaluation */
AbsFormulaScheduleEvaluation(AbsVertexReadFpVar(vertexPtr), vertexPtr);
/* Evaluate the sub-formula */
AbsSubFormulaVerify(absInfo, subFormula);
mdd_free(best);
iterate = newIterate;
/*
* Compute the new iterate. Due to the fact that don't cares are being
* used, it might be possible that the new iterate does not contain the
* previous one, in that case the or is taken
*/
newIterate = mdd_or(iterate, AbsVertexReadSat(subFormula), 1, 1);
assert(AbsMddLEqualModCareSet(iterate, newIterate, careSet));
/* Set the rings and the approximation flags */
AbsVertexInsertRing(vertexPtr, newIterate);
AbsVertexInsertRingApprox(vertexPtr, FALSE);
globalApprox = globalApprox || AbsVertexReadGlobalApprox(subFormula);
AbsVertexInsertSubApprox(vertexPtr, globalApprox);
keepIterating = !AbsMddEqualModCareSet(newIterate, iterate, careSet);
stepCount++;
} /* End of main while loop */
return TRUE;
} /* End of AbsFixedPointIterate */
Here is the call graph for this function:
Here is the caller graph for this function:
| void AbsFormulaScheduleEvaluation | ( | AbsVertexInfo_t * | current, |
| AbsVertexInfo_t * | limit | ||
| ) |
Function********************************************************************
Synopsis [Traverse the operational graph and mark formulas for evaluation]
Description [This procedure receives two pointers and marks every formula in between for later evaluation. The marking process is simply setting the field served to 0]
SideEffects []
SeeAlso [AbsFixedPointIterate]
Definition at line 161 of file absEvaluate.c.
{
/* We reached the final case */
if (current == limit) {
return;
}
else {
AbsVertexInfo_t *parentPtr;
lsList parentList;
lsGen gen;
/* Set the re-evaluation flag for the current vertex */
AbsVertexSetServed(current, 0);
/* Recur over the parents */
parentList = AbsVertexReadParent(current);
lsForEachItem(parentList, gen, parentPtr) {
if (parentPtr != NIL(AbsVertexInfo_t)) {
AbsFormulaScheduleEvaluation(parentPtr, limit);
}
}
}
return;
} /* End of AbsFormulaScheduleEvaluation */
Here is the caller graph for this function:
| void AbsSubFormulaVerify | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Procedure to evaluate a sub-formula]
Description [This procedure is simply a switch to call the apropriate evaluation procedures depending on the type of formula]
SideEffects [EvaluateFixedPoint, EvaluateAnd, EvaluateNot, EvaluatePreImage, EvaluateIdentifier, EvaluateVariable]
Definition at line 71 of file absEvaluate.c.
{
AbsStats_t *stats;
mdd_manager *mddManager;
mdd_t *oldTmpCareSet = NIL(mdd_t);
long verbosity;
stats = AbsVerificationInfoReadStats(absInfo);
mddManager = AbsVerificationInfoReadMddManager(absInfo);
/* If the current vertex has more than one parent, the temporary care set
* must be reset (because it depends on the path that led to this vertex */
if (lsLength(vertexPtr->parent) > 1) {
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
}
switch (AbsVertexReadType(vertexPtr)) {
case fixedPoint_c:
EvaluateFixedPoint(absInfo, vertexPtr);
AbsStatsReadEvalFixedPoint(stats)++;
break;
case and_c:
EvaluateAnd(absInfo, vertexPtr);
AbsStatsReadEvalAnd(stats)++;
break;
case not_c:
EvaluateNot(absInfo, vertexPtr);
AbsStatsReadEvalNot(stats)++;
break;
case preImage_c:
EvaluatePreImage(absInfo, vertexPtr);
AbsStatsReadEvalPreImage(stats)++;
break;
case identifier_c:
EvaluateIdentifier(absInfo, vertexPtr);
AbsStatsReadEvalIdentifier(stats)++;
break;
case variable_c:
EvaluateVariable(absInfo, vertexPtr);
AbsStatsReadEvalVariable(stats)++;
break;
default: fail("Encountered unknown type of vertex\n");
}
verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
/* Print the size of the care set */
if (verbosity & ABS_VB_CARESZ) {
(void) fprintf(vis_stdout, "ABS: Size of Care Set: ");
(void) fprintf(vis_stdout, "%d Nodes.\n",
mdd_size(AbsVerificationInfoReadCareSet(absInfo)));
}
/* Print the care set */
if (verbosity & ABS_VB_CARE) {
(void) fprintf(vis_stdout, "ABS: Care Set for Evaluation:\n");
AbsBddPrintMinterms(AbsVerificationInfoReadCareSet(absInfo));
}
/* Print the contents of the vertex */
if (verbosity & ABS_VB_VTXCNT) {
AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
}
if (lsLength(vertexPtr->parent) > 1) {
/* Restore the old temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
}
} /* End of AbsSubFormulaVerify */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateAnd | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Evaluate a conjunction vertex]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 549 of file absEvaluate.c.
{
if (AbsVertexReadServed(vertexPtr) == 0) {
AbsVertexInfo_t *firstFormula;
AbsVertexInfo_t *secondFormula;
mdd_t *oldTmpCareSet;
/* Clean up of previous result */
if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(vertexPtr));
AbsVertexSetSat(vertexPtr, NIL(mdd_t));
}
/* Obtain the subformulas to evaluate */
firstFormula = AbsVertexReadLeftKid(vertexPtr);
secondFormula = AbsVertexReadRightKid(vertexPtr);
/* Recursively evaluate the first sub-formula */
AbsSubFormulaVerify(absInfo, firstFormula);
/* Store the temporary careset and set the new one */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo,
mdd_and(oldTmpCareSet,
AbsVertexReadSat(firstFormula),
1,1));
/* Recursively evaluate the second sub-formula */
AbsSubFormulaVerify(absInfo, secondFormula);
/* Restore the temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
/* Compute result, so far no approximation is required */
AbsVertexSetSat(vertexPtr, mdd_and(AbsVertexReadSat(firstFormula),
AbsVertexReadSat(secondFormula),
1, 1));
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(firstFormula) ||
AbsVertexReadGlobalApprox(secondFormula));
}
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
} /* End of EvaluateAnd */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateFixedPoint | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Evaluate a fix-point vertex]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 613 of file absEvaluate.c.
{
if (AbsVertexReadServed(vertexPtr) == 0) {
mdd_manager *mddManager;
mdd_t *oldTmpCareSet;
mdd_t *newTmpCareSet;
if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) {
mdd_t *ringUnit;
int i;
arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), i, ringUnit) {
mdd_free(ringUnit);
}
array_free(AbsVertexReadRings(vertexPtr));
array_free(AbsVertexReadRingApprox(vertexPtr));
array_free(AbsVertexReadSubApprox(vertexPtr));
mdd_free(AbsVertexReadSat(vertexPtr));
}
/* Re-allocation of the temporary structures */
AbsVertexSetRings(vertexPtr, array_alloc(mdd_t *, 0));
AbsVertexSetRingApprox(vertexPtr, array_alloc(boolean, 0));
AbsVertexSetSubApprox(vertexPtr, array_alloc(boolean, 0));
/* Initial values of the fixed point */
mddManager = AbsVerificationInfoReadMddManager(absInfo);
AbsVertexInsertRing(vertexPtr, mdd_zero(mddManager));
AbsVertexInsertRingApprox(vertexPtr, FALSE);
AbsVertexInsertSubApprox(vertexPtr, FALSE);
/* Reset the temporary careset to the mdd one */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
newTmpCareSet = mdd_one(mddManager);
AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);
/* Effectively iterate the body */
AbsFixedPointIterate(absInfo, vertexPtr, 0);
/* Restore the old temporary careset */
mdd_free(newTmpCareSet);
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
/* Set the last result as the set sat*/
AbsVertexSetSat(vertexPtr,
mdd_dup(AbsVertexFetchRing(vertexPtr,
array_n(AbsVertexReadRings(vertexPtr))
- 1)));
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexFetchSubApprox(vertexPtr,
array_n(AbsVertexReadSubApprox(vertexPtr)) - 1));
}
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateIdentifier | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Evaluate a vertex storing an Id]
Description [This vertex represents a subformula with an atomic proposition. No approximation is done on its evaluation. The assumption is that this operation does not cause blow up in the memory requirements. This situation might change though]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 400 of file absEvaluate.c.
{
if (AbsVertexReadServed(vertexPtr) == 0) {
Ntk_Node_t *node;
Var_Variable_t *nodeVar;
graph_t *partition;
vertex_t *partitionVertex;
Mvf_Function_t *nodeFunction;
mdd_t *result;
char *nodeNameString;
char *nodeValueString;
int nodeValue;
/* Clean up of previous result */
if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(vertexPtr));
AbsVertexSetSat(vertexPtr, NIL(mdd_t));
}
/* Read the partition */
partition = AbsVerificationInfoReadPartition(absInfo);
assert(partition != NIL(graph_t));
/* Obtain the name and the value being used */
nodeNameString = AbsVertexReadName(vertexPtr);
nodeValueString = AbsVertexReadValue(vertexPtr);
/* Obtain the the node in the network and the variable attached to it */
node = Ntk_NetworkFindNodeByName(AbsVerificationInfoReadNetwork(absInfo),
nodeNameString);
nodeVar = Ntk_NodeReadVariable(node);
/* Obtain the real value of the multi-valued vairable */
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar,
nodeValueString);
}
else {
nodeValue = atoi(nodeValueString);
}
/* Read the partition, find the vertex in the partition and its function */
partitionVertex = Part_PartitionFindVertexByName(partition,
nodeNameString);
/* If the vertex is not represented in the partition must be built */
if (partitionVertex == NIL(vertex_t)) {
Ntk_Node_t *tmpNode;
lsGen tmpGen;
array_t *mvfArray;
array_t *tmpRoots;
st_table *tmpLeaves;
/* Initialize the variables */
tmpRoots = array_alloc(Ntk_Node_t *, 0);
tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
/* Insert the parameters in the array and table */
array_insert_last(Ntk_Node_t *, tmpRoots, node);
Ntk_NetworkForEachCombInput(AbsVerificationInfoReadNetwork(absInfo),
tmpGen, tmpNode) {
st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
}
/* Effectively build the mdd for the given vertex */
mvfArray = Ntm_NetworkBuildMvfs(AbsVerificationInfoReadNetwork(absInfo),
tmpRoots, tmpLeaves, NIL(mdd_t));
nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0);
array_free(tmpRoots);
st_free_table(tmpLeaves);
array_free(mvfArray);
/* Store the result in the vertex */
result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
AbsVertexSetSat(vertexPtr, mdd_dup(result));
Mvf_FunctionFree(nodeFunction);
}
else {
/* Store the result in the vertex */
nodeFunction = Part_VertexReadFunction(partitionVertex);
result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
AbsVertexSetSat(vertexPtr, mdd_dup(result));
}
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr, FALSE);
}
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
} /* End of EvaluateIdentifier */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateNot | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Evaluate a negation vertex]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 508 of file absEvaluate.c.
{
if (AbsVertexReadServed(vertexPtr) == 0) {
AbsVertexInfo_t *subFormula;
/* Clean up of previous result */
if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(vertexPtr));
AbsVertexSetSat(vertexPtr, NIL(mdd_t));
}
/* Recursively evaluate the sub-formula */
subFormula = AbsVertexReadLeftKid(vertexPtr);
AbsSubFormulaVerify(absInfo, subFormula);
/* Negate the result of the sub-formula */
AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));
}
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
} /* End of EvaluateNot */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluatePreImage | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Evaluate a pre-image vertex]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 689 of file absEvaluate.c.
{
AbsOptions_t *options;
AbsStats_t *stats;
long verbosity;
/* Variable initialization */
options = AbsVerificationInfoReadOptions(absInfo);
verbosity = AbsOptionsReadVerbosity(options);
stats = AbsVerificationInfoReadStats(absInfo);
if (AbsVertexReadServed(vertexPtr) == 0) {
AbsVertexInfo_t *subFormula;
mdd_manager *mddManager;
mdd_t *result;
mdd_t *careSet;
mdd_t *oldTmpCareSet;
mdd_t *minimizedSet;
/* Variable initialization */
mddManager = AbsVerificationInfoReadMddManager(absInfo);
subFormula = AbsVertexReadLeftKid(vertexPtr);
/*
* Compute the care set as the conjunction of the given one and the
* temporary one
*/
careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);
/* Clean up */
if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(vertexPtr));
AbsVertexSetSat(vertexPtr, NIL(mdd_t));
}
/* Reset the temporary careset to the mdd one */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
/* Evaluate the sub-formula */
AbsSubFormulaVerify(absInfo, subFormula);
/* Restore the old temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
/* Check for trivial cases */
if (mdd_is_tautology(AbsVertexReadSat(subFormula), 0) ||
mdd_is_tautology(AbsVertexReadSat(subFormula), 1)) {
AbsVertexSetSat(vertexPtr, mdd_dup(AbsVertexReadSat(subFormula)));
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(subFormula));
mdd_free(careSet);
return;
}
/* if (AbsOptionsReadMinimizeIterate(options)){ */
if (FALSE){
minimizedSet = bdd_minimize(AbsVertexReadSat(subFormula),
AbsVerificationInfoReadCareSet(absInfo));
}
else {
minimizedSet = mdd_dup(AbsVertexReadSat(subFormula));
}
/* Look up in the cache if the result has been previously computed */
if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
mdd_t *unit;
boolean localFlag;
boolean exactness;
exactness = AbsOptionsReadExact(options);
if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
minimizedSet, careSet, !exactness,
&unit, &localFlag)) {
/* Set the sat */
AbsVertexSetSat(vertexPtr, mdd_dup(unit));
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, localFlag & !exactness);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(subFormula) ||
AbsVertexReadLocalApprox(vertexPtr));
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
mdd_free(careSet);
mdd_free(minimizedSet);
return;
}
}
else {
/* Initialize the cache */
AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
}
/* Effectively compute preImage */
if (!AbsOptionsReadExact(options)) {
if (AbsVertexReadPolarity(vertexPtr)) {
if (AbsOptionsReadPartApprox(options)) {
result = OverApproximatePreImageWithSubFSM(absInfo, minimizedSet,
minimizedSet, careSet);
}
else {
result = OverApproximatePreImageWithBddSubsetting(absInfo,
minimizedSet,
minimizedSet,
careSet);
}
AbsVertexSetLocalApprox(vertexPtr, TRUE);
}
else {
result = UnderApproximatePreImageWithBddSubsetting(absInfo,
minimizedSet,
minimizedSet,
careSet);
AbsVertexSetLocalApprox(vertexPtr, TRUE);
}
AbsStatsReadApproxPreImage(AbsVerificationInfoReadStats(absInfo))++;
}
else {
Fsm_Fsm_t *system;
Img_ImageInfo_t *imageInfo;
long cpuTime;
system = AbsVerificationInfoReadFsm(absInfo);
imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
cpuTime = util_cpu_time();
result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, minimizedSet,
minimizedSet,careSet);
AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;
AbsStatsReadExactPreImage(stats)++;
AbsVertexSetLocalApprox(vertexPtr, FALSE);
}
AbsVertexSetSat(vertexPtr, result);
/* Set the value in the cache */
AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
minimizedSet, AbsVertexReadSat(vertexPtr), careSet,
AbsVertexReadLocalApprox(vertexPtr), FALSE);
AbsStatsReadPreImageCacheEntries(stats)++;
mdd_free(minimizedSet);
/* Set the approximation flags */
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(subFormula) ||
AbsVertexReadLocalApprox(vertexPtr));
/* Print the number of states in the on set of Sat */
if (verbosity & ABS_VB_TSAT) {
Fsm_Fsm_t *globalSystem;
array_t *domainVars;
mdd_t *intersection;
intersection = mdd_and(AbsVertexReadSat(vertexPtr), careSet, 1, 1);
globalSystem = AbsVerificationInfoReadFsm(absInfo);
domainVars = Fsm_FsmReadPresentStateVars(globalSystem);
(void) fprintf(vis_stdout, "ABS: %.0f States satisfy the EX formula.\n",
mdd_count_onset(AbsVerificationInfoReadMddManager(absInfo),
intersection, domainVars));
mdd_free(intersection);
}
mdd_free(careSet);
}
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
} /* End of EvaluatePreImage */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateVariable | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Function to evaluate a sub-formula representing the variable of a fix-point computation]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 375 of file absEvaluate.c.
{
/* Increase the number of times the result has been used */
AbsVertexReadServed(vertexPtr)++;
return;
} /* End of EvaluateVariable */
Here is the caller graph for this function:
| static mdd_t * OverApproximatePreImageWithBddSubsetting | ( | Abs_VerificationInfo_t * | absInfo, |
| mdd_t * | lowerBound, | ||
| mdd_t * | upperBound, | ||
| mdd_t * | careSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [A second procedure to compute an over-approximation of the Preimage]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 921 of file absEvaluate.c.
{
Fsm_Fsm_t *system;
Img_ImageInfo_t *imageInfo;
mdd_t *superSet;
mdd_t *result;
long cpuTime;
/* Initialize some variables */
system = AbsVerificationInfoReadFsm(absInfo);
/* Compute the subset of the restriction set */
superSet = bdd_approx_remap_ua(lowerBound,BDD_OVER_APPROX,
AbsVerificationInfoReadNumStateVars(absInfo),
0,1);
/* Obtain the image info */
imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
cpuTime = util_cpu_time();
result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, superSet,
superSet, careSet);
AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+=
util_cpu_time() - cpuTime;
mdd_free(superSet);
return result;
} /* End of OverApproximatePreImageWithBddSubsetting */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * OverApproximatePreImageWithSubFSM | ( | Abs_VerificationInfo_t * | absInfo, |
| mdd_t * | lowerBound, | ||
| mdd_t * | upperBound, | ||
| mdd_t * | careSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compute an over-approximation of the Preimage]
SideEffects [This overapproximation is computed by just ignoring some FSM components]
SeeAlso [AbsSubFormulaVerify]
Definition at line 879 of file absEvaluate.c.
{
Fsm_Fsm_t *system;
Img_ImageInfo_t *imageInfo;
mdd_t *result;
long cpuTime;
/* Initialize some variables */
system = AbsVerificationInfoReadApproxFsm(absInfo);
if (system == NIL(Fsm_Fsm_t)) {
system = AbsVerificationInfoReadFsm(absInfo);
}
/* Obtain the image info */
imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
cpuTime = util_cpu_time();
result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, lowerBound,
upperBound, careSet);
AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+=
util_cpu_time() - cpuTime;
return result;
} /* End of OverApproximatePreImageWithSubFSM */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * UnderApproximatePreImageWithBddSubsetting | ( | Abs_VerificationInfo_t * | absInfo, |
| mdd_t * | lowerBound, | ||
| mdd_t * | upperBound, | ||
| mdd_t * | careSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compute an under-approximation of the preimage]
SideEffects []
SeeAlso [AbsSubFormulaVerify]
Definition at line 965 of file absEvaluate.c.
{
Fsm_Fsm_t *system;
Img_ImageInfo_t *imageInfo;
mdd_t *subSet;
mdd_t *result;
long cpuTime;
/* Initialize some variables */
system = AbsVerificationInfoReadFsm(absInfo);
/* Compute the subset of the restriction set */
subSet = bdd_approx_remap_ua(lowerBound, BDD_UNDER_APPROX,
AbsVerificationInfoReadNumStateVars(absInfo),
0,1);
/* Obtain the image info */
imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
cpuTime = util_cpu_time();
result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, subSet, subSet,
careSet);
AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+=
util_cpu_time() - cpuTime;
mdd_free(subSet);
return result;
} /* End of UnderApproximatePreImageWithBddSubsetting */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: absEvaluate.c,v 1.19 2002/09/19 05:25:00 fabio Exp $" [static] |
CFile***********************************************************************
FileName [absEvaluate.c]
PackageName [abs]
Synopsis [Evaluation procedures for the abstraction based mu-calculus model checker.]
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 20 of file absEvaluate.c.
