src/grab/grabUtil.c File Reference
#include "grabInt.h"
Include dependency graph for grabUtil.c:
Go to the source code of this file.
Functions | |
| static void | GetFormulaNodes (Ntk_Network_t *network, Ctlp_Formula_t *F, array_t *formulaNodes) |
| static void | GetFaninLatches (Ntk_Node_t *node, st_table *visited, st_table *absVarTable) |
| static void | NodeTableAddCtlFormulaNodes (Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table *nodesTable) |
| st_table * | GrabComputeCOIAbstraction (Ntk_Network_t *network, Ctlp_Formula_t *invFormula) |
| st_table * | GrabComputeInitialAbstraction (Ntk_Network_t *network, Ctlp_Formula_t *invFormula) |
| void | GrabUpdateAbstractPartition (Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag) |
| Fsm_Fsm_t * | GrabCreateAbstractFsm (Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag, int independentFlag) |
| mdd_t * | GrabComputeInitialStates (Ntk_Network_t *network, array_t *psVars) |
| mdd_t * | GrabFsmComputeReachableStates (Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *invStatesArray, int verbose) |
| mdd_t * | GrabFsmComputeConstrainedReachableStates (Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *SORs, int verbose) |
| array_t * | GrabFsmComputeSynchronousOnionRings (Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, mdd_t *inv_states, int cexType, int verbose) |
| array_t * | GrabGetVisibleVarMddIds (Fsm_Fsm_t *absFsm, st_table *absVarTable) |
| array_t * | GrabGetInvisibleVarMddIds (Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable) |
| int | GrabTestRefinementSetSufficient (Ntk_Network_t *network, array_t *SORs, st_table *absVarTable, int verbose) |
| int | GrabTestRefinementBnvSetSufficient (Ntk_Network_t *network, st_table *coiBnvTable, array_t *SORs, st_table *absVarTable, st_table *absBnvTable, int verbose) |
| void | GrabMinimizeLatchRefinementSet (Ntk_Network_t *network, st_table **absVarTable, st_table **absBnvTable, array_t *newlyAddedLatches, array_t **newlyAddedBnvs, array_t *SORs, int verbose) |
| void | GrabMinimizeBnvRefinementSet (Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table **absBnvTable, array_t *newlyAddedBnvs, array_t *SORs, int verbose) |
| void | GrabNtkClearAllMddIds (Ntk_Network_t *network) |
| void | GrabPrintNodeArray (char *caption, array_t *theArray) |
| void | GrabPrintMddIdArray (Ntk_Network_t *network, char *caption, array_t *mddIdArray) |
| void | GrabPrintNodeList (char *caption, lsList theList) |
| void | GrabPrintNodeHashTable (char *caption, st_table *theTable) |
Function Documentation
| static void GetFaninLatches | ( | Ntk_Node_t * | node, |
| st_table * | visited, | ||
| st_table * | absVarTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Get the fan-in latches of those already in the table.]
Description [Get the fan-in latches of those already in the table.]
SideEffects []
Definition at line 1200 of file grabUtil.c.
{
if (st_is_member(visited, node))
return;
st_insert(visited, node, (char *)0);
if (Ntk_NodeTestIsLatch(node))
st_insert(absVarTable, node, (char *)0);
else {
int i;
Ntk_Node_t *fanin;
Ntk_NodeForEachFanin(node, i, fanin) {
GetFaninLatches(fanin, visited, absVarTable);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void GetFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | F, | ||
| array_t * | formulaNodes | ||
| ) | [static] |
CFile***********************************************************************
FileName [grabUtil.c]
PackageName [grab]
Synopsis [The utility functions for abstraction refinement.]
Description [This file contains the functions to check invariant properties by the GRAB abstraction refinement algorithm. GRAB stands for "Generational Refinement of Ariadne's Bundle," in which the automatic refinement is guided by all shortest abstract counter-examples. For more information, please check the ICCAD'03 paper of Wang et al., "Improving Ariadne's Bundle by Following Multiple Counter-Examples in Abstraction Refinement." ]
Author [Chao Wang]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart
Function********************************************************************
Synopsis [Get network nodes that are mentioned by the formula.]
Description [Get network nodes that are mentioned by the formula.]
SideEffects []
Definition at line 1168 of file grabUtil.c.
{
if (F == NIL(Ctlp_Formula_t))
return;
if (Ctlp_FormulaReadType(F) == Ctlp_ID_c) {
char *nodeNameString = Ctlp_FormulaReadVariableName(F);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
assert(node);
array_insert_last(Ntk_Node_t *, formulaNodes, node);
return;
}
GetFormulaNodes(network, Ctlp_FormulaReadRightChild(F), formulaNodes);
GetFormulaNodes(network, Ctlp_FormulaReadLeftChild(F), formulaNodes);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* GrabComputeCOIAbstraction | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | invFormula | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Compute the Cone-Of-Influence abstract model.]
Description [Compute the Cone-Of-Influence abstraction, which consists of latches in the transitive supprot of the property.]
SideEffects []
Definition at line 79 of file grabUtil.c.
{
st_table *formulaNodes;
array_t *formulaCombNodes;
Ntk_Node_t *node;
array_t *nodeArray;
int i;
st_generator *stGen;
st_table *absVarTable;
/* find network nodes in the immediate support of the property */
formulaNodes = st_init_table(st_ptrcmp, st_ptrhash);
NodeTableAddCtlFormulaNodes(network, invFormula, formulaNodes);
/* find network nodes in the transitive fan-in */
nodeArray = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(formulaNodes, stGen, & node, NIL(char *)) {
array_insert_last( Ntk_Node_t *, nodeArray, node);
}
st_free_table(formulaNodes);
formulaCombNodes = Ntk_NodeComputeTransitiveFaninNodes(network, nodeArray,
FALSE, TRUE);
array_free(nodeArray);
/* extract all the latches */
absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(Ntk_Node_t *, formulaCombNodes, i, node) {
if (Ntk_NodeTestIsLatch(node) == TRUE) {
st_insert(absVarTable, node, (char *)0);
}
}
array_free(formulaCombNodes);
return absVarTable;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* GrabComputeInitialAbstraction | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | invFormula | ||
| ) |
Function********************************************************************
Synopsis [Compute the initial abstract model.]
Description [Compute the he initial abstraction, which consists of latches in the immediate supprot of the property.]
SideEffects []
Definition at line 128 of file grabUtil.c.
{
array_t *formulaNodes = array_alloc(Ntk_Node_t *, 0);
Ntk_Node_t *node;
int i;
st_table *absVarTable, *visited;
GetFormulaNodes(network, invFormula, formulaNodes);
absVarTable = st_init_table(st_ptrcmp, st_ptrhash);
visited = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) {
GetFaninLatches(node, visited, absVarTable);
}
st_free_table(visited);
array_free(formulaNodes);
return absVarTable;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* GrabComputeInitialStates | ( | Ntk_Network_t * | network, |
| array_t * | psVars | ||
| ) |
Function********************************************************************
Synopsis [Computes the set of initial states of set of latches.]
Description [Computes the set of initial states of a set of latches. The nodes driving the initial inputs of the latches, called the initial nodes, must not have latches in their support. If an initial node is found that has a latch in its transitive fanin, then a NULL MDD is returned, and a message is written to the error_string.
The initial states are computed as follows. For each latch i, the relation (x_i = g_i(u)) is built, where x_i is the present state variable of latch i, and g_i(u) is the multi-valued initialization function of latch i, in terms of the input variables u. These relations are then conjuncted, and the input variables are existentially quantified from the result (i.e. init_states(x) = u \[ (x_i = g_i(u))\]).]
SideEffects [The result of the initial state computation is stored with the FSM.]
SeeAlso [Fsm_FsmComputeReachableStates]
Definition at line 347 of file grabUtil.c.
{
int i = 0;
mdd_t *initStates;
Ntk_Node_t *node;
array_t *initRelnArray;
array_t *initMvfs;
array_t *initNodes;
array_t *initVertices;
array_t *latchMddIds;
array_t *inputVars = array_alloc(int, 0);
array_t *combArray;
st_table *supportNodes;
st_table *supportVertices;
mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
graph_t *partition =
(graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY);
int numLatches;
Img_MethodType imageMethod;
numLatches = array_n(psVars);
/* Get the array of initial nodes, both as network nodes and as
* partition vertices.
*/
initNodes = array_alloc(Ntk_Node_t *, numLatches);
initVertices = array_alloc(vertex_t *, numLatches);
latchMddIds = array_alloc(int, numLatches);
for (i=0; i<numLatches; i++){
int latchMddId = array_fetch(int, psVars, i);
Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
Ntk_Node_t *initNode = Ntk_LatchReadInitialInput(latch);
vertex_t *initVertex = Part_PartitionFindVertexByName(partition,
Ntk_NodeReadName(initNode));
array_insert(Ntk_Node_t *, initNodes, i, initNode);
array_insert(vertex_t *, initVertices, i, initVertex);
array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
}
/* Get the table of legal support nodes, both as network nodes and
* as partition vertices. Inputs (both primary and pseudo) and
* constants constitute the legal support nodes.
*/
supportNodes = st_init_table(st_ptrcmp, st_ptrhash);
supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
combArray = Ntk_NodeComputeTransitiveFaninNodes(network, initNodes, TRUE,
TRUE);
arrayForEachItem(Ntk_Node_t *, combArray, i, node) {
vertex_t *vertex = Part_PartitionFindVertexByName(partition,
Ntk_NodeReadName(node));
if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
st_insert(supportNodes, node, NIL(char));
st_insert(supportVertices, vertex, NIL(char));
}
if (Ntk_NodeTestIsInput(node)) {
assert(Ntk_NodeReadMddId(node) != -1);
array_insert_last(int, inputVars, Ntk_NodeReadMddId(node));
}
}
array_free(combArray);
array_free(initNodes);
st_free_table(supportNodes);
/* Compute the initial states
*/
initMvfs = Part_PartitionCollapse(partition, initVertices,
supportVertices, NIL(mdd_t));
array_free(initVertices);
st_free_table(supportVertices);
/* Compute the relation (x_i = g_i(u)) for each latch. */
initRelnArray = array_alloc(mdd_t*, numLatches);
for (i = 0; i < numLatches; i++) {
int latchMddId = array_fetch(int, latchMddIds, i);
Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
latchMddId);
array_insert(mdd_t *, initRelnArray, i, initLatchReln);
}
array_free(latchMddIds);
Mvf_FunctionArrayFree(initMvfs);
imageMethod = Img_UserSpecifiedMethod();
if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c)
imageMethod = Img_Iwls95_c;
initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray,
inputVars, psVars,
imageMethod, Img_Forward_c);
mdd_array_free(initRelnArray);
array_free(inputVars);
return (initStates);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Fsm_Fsm_t* GrabCreateAbstractFsm | ( | Ntk_Network_t * | network, |
| st_table * | coiBnvTable, | ||
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| int | partitionFlag, | ||
| int | independentFlag | ||
| ) |
Function********************************************************************
Synopsis [Create the abstract FSM.]
Description [Create the abstract FSM. Table 'coiBnvTable' contains all the BNVs (i.e. intermediate variables), while Table 'absBnvTable' contains all the visible BNVs. BNVs not in absBnvTable should be treated as inputs.
When absBnvTable is NULL (e.g. fine-grain abstraction is disabled), no BNV is treated as input.
If independentFlag is TRUE, invisible latches are regarded as inputs; otherwise, they are regarded as latches.]
SideEffects []
Definition at line 230 of file grabUtil.c.
{
Fsm_Fsm_t *fsm;
array_t *absLatches = array_alloc(Ntk_Node_t *, 0);
array_t *invisibleVars = array_alloc(Ntk_Node_t *, 0);
array_t *absInputs = array_alloc(Ntk_Node_t *, 0);
array_t *rootNodesArray = array_alloc(Ntk_Node_t *, 0);
st_table *rawLeafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
lsList topologicalNodeList;
lsGen lsgen;
st_generator *stgen;
Ntk_Node_t *node;
GrabUpdateAbstractPartition(network, coiBnvTable, absVarTable, absBnvTable,
partitionFlag);
/* first, compute the absLatches, invisibleVars, and absInputs:
* absLatches includes all the visible latch variables;
* invisibleVars includes all the invisible latches variables;
* absInputs includes all the primary and pseudo inputs.
*/
st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
array_insert_last(Ntk_Node_t *, absLatches, node);
array_insert_last(Ntk_Node_t *, rootNodesArray,
Ntk_LatchReadDataInput(node));
array_insert_last(Ntk_Node_t *, rootNodesArray,
Ntk_LatchReadInitialInput(node));
}
Ntk_NetworkForEachCombInput(network, lsgen, node) {
st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
}
st_foreach_item(coiBnvTable, stgen, &node, NIL(char *)) {
/* unless it blongs to the current Abstract Model */
if (absBnvTable && !st_is_member(absBnvTable, node))
st_insert(rawLeafNodesTable, node, (char *) (long) (-1) );
}
topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
rootNodesArray,
rawLeafNodesTable);
lsForEachItem(topologicalNodeList, lsgen, node){
if (st_is_member(rawLeafNodesTable, node) &&
!st_is_member(absVarTable, node) ) {
/*if (Ntk_NodeTestIsLatch(node) ||
coiBnvTable && st_is_member(coiBnvTable, node))*/
if (Ntk_NodeTestIsLatch(node) ||
(coiBnvTable && st_is_member(coiBnvTable, node)))
array_insert_last(Ntk_Node_t *, invisibleVars, node);
else
array_insert_last(Ntk_Node_t *, absInputs, node);
}
}
lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
st_free_table(rawLeafNodesTable);
array_free(rootNodesArray);
/* now, create the abstract Fsm according to the value of
* independentFlag when independentFlag is TRUE, the present state
* varaibles are absLatches; otherwise, they contain both absLatches
* and invisibleVars (with such a FSM, preimages may contain
* invisible vars in their supports)
*/
fsm = Fsm_FsmCreateAbstractFsm(network, NIL(graph_t),
absLatches, invisibleVars, absInputs,
NIL(array_t), independentFlag);
#if 0
/* for debugging */
if (partitionFlag == GRAB_PARTITION_NOCHANGE) {
GrabPrintNodeArray("absLatches", absLatches);
GrabPrintNodeArray("invisibleVars", invisibleVars);
GrabPrintNodeArray("absInputs", absInputs);
}
#endif
array_free(invisibleVars);
array_free(absInputs);
array_free(absLatches);
return fsm;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* GrabFsmComputeConstrainedReachableStates | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| array_t * | SORs, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Compute the reachable states inside the SORs.]
Description [Compute the reachable states inside the SORs.]
SideEffects []
Definition at line 516 of file grabUtil.c.
{
mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
Img_ImageInfo_t *imageInfo;
array_t *rchOnionRings;
mdd_t *mdd1, *mdd2, *mdd3, *mdd4;
mdd_t *mddOne, *initStates, *rchStates;
int i;
assert (SORs != NIL(array_t));
imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);
rchOnionRings = array_alloc(mdd_t *, 0);
mddOne = mdd_one(mddManager);
/* the new initial states */
mdd2 = array_fetch(mdd_t *, SORs, 0);
mdd1 = Fsm_FsmComputeInitialStates(absFsm);
initStates = mdd_and(mdd1, mdd2, 1, 1);
mdd_free(mdd1);
array_insert(mdd_t *, rchOnionRings, 0, initStates);
/* compute the reachable states inside the previous SORs */
rchStates = mdd_dup(initStates);
for (i=0; i<array_n(SORs)-1; i++) {
mdd1 = array_fetch(mdd_t *, rchOnionRings, i);
mdd2 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
mdd1,
rchStates,
mddOne);
mdd3 = array_fetch(mdd_t *, SORs, i+1);
mdd4 = mdd_and(mdd2, mdd3, 1, 1);
mdd_free(mdd2);
/* if this happens, the last ring is no longer reachable */
if (mdd_is_tautology(mdd4, 0)) {
mdd_free(mdd4);
break;
}
array_insert(mdd_t *, rchOnionRings, i+1, mdd4);
mdd1 = rchStates;
rchStates = mdd_or(rchStates, mdd4, 1, 1);
mdd_free(mdd1);
}
mdd_free(mddOne);
FsmSetReachabilityOnionRings(absFsm, rchOnionRings);
return rchStates;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* GrabFsmComputeReachableStates | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| array_t * | invStatesArray, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Compute the reachable states of the abstract model.]
Description [Compute the reachable states of the abstract model.]
SideEffects []
Definition at line 457 of file grabUtil.c.
{
mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
Img_ImageInfo_t *imageInfo;
array_t *fwdOnionRings;
mdd_t *initStates, *mdd1, *mddOne, *rchStates, *frontier;
imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 0, 1);
fwdOnionRings = array_alloc(mdd_t *, 0);
mddOne = mdd_one(mddManager);
initStates = Fsm_FsmComputeInitialStates(absFsm);
array_insert_last(mdd_t *, fwdOnionRings, initStates);
rchStates = mdd_dup(initStates);
frontier = initStates;
while(TRUE) {
mdd1 = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, frontier,
rchStates, mddOne);
frontier = mdd_and(mdd1, rchStates, 1, 0);
mdd_free(mdd1);
mdd1 = rchStates;
rchStates = mdd_or(rchStates, frontier, 1, 1);
mdd_free(mdd1);
if (mdd_is_tautology(frontier, 0)) {
mdd_free(frontier);
break;
}
array_insert_last(mdd_t *, fwdOnionRings, frontier);
/* if this happens, the invariant is voilated */
if (!mdd_lequal_array(frontier, invStatesArray, 1, 1))
break;
}
mdd_free(mddOne);
FsmSetReachabilityOnionRings(absFsm, fwdOnionRings);
return rchStates;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* GrabFsmComputeSynchronousOnionRings | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| array_t * | oldRings, | ||
| mdd_t * | inv_states, | ||
| int | cexType, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Compute the Synchronous Onion Rings (SORs).]
Description [Compute the Synchronous Onion Rings (SORs) with backward reachability analysis. The SORs capture all the shortest counter-examples to an invariant property. If the forward reachability onion rings is not provided (as oldRings), it will be retrived from absFsm.
cexType controls the type of the counter-example envelope: GRAB_CEX_MINTERM, a single-state path, GRAB_CEX_CUBE, a cube-states path, GRAB_CEX_SOR, the SORs. ]
SideEffects []
Definition at line 596 of file grabUtil.c.
{
mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
Img_ImageInfo_t *imageInfo;
array_t *onionRings, *synOnionRings;
array_t *allPSVars;
mdd_t *mddOne, *ring;
mdd_t *mdd1, *mdd2, *mdd3, *mdd4;
int j;
imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0);
/* get the forward reachability onion rings */
onionRings = oldRings;
if (onionRings == NIL(array_t))
onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
assert(onionRings);
synOnionRings = array_alloc(mdd_t *, array_n(onionRings));
mddOne = mdd_one(mddManager);
allPSVars = Fsm_FsmReadPresentStateVars(absFsm);
/* the last ring */
mdd2 = array_fetch_last(mdd_t *, onionRings);
mdd1 = mdd_and(mdd2, inv_states, 1, 0);
if (cexType == GRAB_CEX_MINTERM)
ring = Mc_ComputeAMinterm(mdd1, allPSVars, mddManager);
else if (cexType == GRAB_CEX_CUBE) {
array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd1);
int nvars = array_n(bddIds);
array_free(bddIds);
ring = bdd_approx_remap_ua(mdd1, (bdd_approx_dir_t)BDD_UNDER_APPROX,
nvars, 1024, 1);
if (ring == NIL(mdd_t))
ring = mdd_dup(mdd1);
}else
ring = mdd_dup(mdd1);
mdd_free(mdd1);
array_insert(mdd_t *, synOnionRings, array_n(onionRings)-1, ring);
/* the rest rings */
for (j=array_n(onionRings)-2; j>=0; j--) {
mdd1 = array_fetch(mdd_t *, synOnionRings, j+1);
mdd2 = Img_ImageInfoComputeBwdWithDomainVars(imageInfo,
mdd1,
mdd1,
mddOne);
mdd3 = array_fetch(mdd_t *, onionRings, j);
mdd4 = mdd_and(mdd2, mdd3, 1, 1);
mdd_free(mdd2);
if (cexType == GRAB_CEX_MINTERM)
ring = Mc_ComputeAMinterm(mdd4, allPSVars, mddManager);
else if (cexType == GRAB_CEX_CUBE) {
array_t *bddIds = mdd_get_bdd_support_ids(mddManager, mdd4);
int nvars = array_n(bddIds);
array_free(bddIds);
ring = bdd_approx_remap_ua(mdd4, (bdd_approx_dir_t)BDD_UNDER_APPROX,
nvars, 1024, 1);
if (ring == NIL(mdd_t))
ring = mdd_dup(mdd4);
}else
ring = mdd_dup(mdd4);
mdd_free(mdd4);
array_insert(mdd_t *, synOnionRings, j, ring);
}
mdd_free(mddOne);
return synOnionRings;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* GrabGetInvisibleVarMddIds | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable, | ||
| st_table * | absBnvTable | ||
| ) |
Function********************************************************************
Synopsis [Get the invisible variable mddIds of the current abstraction.]
Description [Get the invisible variable mddIds of the current abstraction. Note that they include both state variables and boolean network variables.]
SideEffects []
Definition at line 718 of file grabUtil.c.
{
Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
array_t *inputVars = Fsm_FsmReadInputVars(absFsm);
array_t *invisibleVarMddIds = array_alloc(int, 0);
Ntk_Node_t *node;
int i, mddId;
arrayForEachItem(int, inputVars, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
if ( !Ntk_NodeTestIsInput(node) &&
!st_is_member(absVarTable, node) ) {
if (absBnvTable != NIL(st_table)) {
if (!st_is_member(absBnvTable, node)) {
array_insert_last(int, invisibleVarMddIds, mddId);
}
}else
array_insert_last(int, invisibleVarMddIds, mddId);
}
}
return invisibleVarMddIds;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* GrabGetVisibleVarMddIds | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable | ||
| ) |
Function********************************************************************
Synopsis [Get the visible variable mddIds of the current abstraction.]
Description [Get the visible variable mddIds of the current abstraction. Note that they are the state variables.]
SideEffects []
Definition at line 688 of file grabUtil.c.
{
array_t *visibleVarMddIds = array_alloc(int, 0);
st_generator *stgen;
Ntk_Node_t *node;
int mddId;
st_foreach_item(absVarTable, stgen, &node, NIL(char *)) {
mddId = Ntk_NodeReadMddId(node);
array_insert_last(int, visibleVarMddIds, mddId);
}
return visibleVarMddIds;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabMinimizeBnvRefinementSet | ( | Ntk_Network_t * | network, |
| st_table * | coiBnvTable, | ||
| st_table * | absVarTable, | ||
| st_table ** | absBnvTable, | ||
| array_t * | newlyAddedBnvs, | ||
| array_t * | SORs, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Minimize the refinement set of latch variable.]
Description [Minimize the refinement set of latch variable. After that, also prune away the boolean network variables that are no longer in the transitive fan-in.]
SideEffects []
Definition at line 923 of file grabUtil.c.
{
st_table *newBnvTable;
Ntk_Node_t *node;
int i, flag, n_size, mddId;
n_size = array_n(newlyAddedBnvs);
if (verbose >= 3)
fprintf(vis_stdout,
"-- grab: minimize bnv refinement set: previous size is %d\n",
n_size);
arrayForEachItem(int, newlyAddedBnvs, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
/* first, try to drop it */
newBnvTable = st_copy(*absBnvTable);
flag = st_delete(newBnvTable, &node, NIL(char *));
assert(flag);
/* if the counter-example does not come back, drop it officially */
flag = Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
coiBnvTable,
SORs,
absVarTable,
newBnvTable);
if (!flag) {
st_free_table(*absBnvTable);
*absBnvTable = newBnvTable;
n_size--;
}else {
st_free_table(newBnvTable);
if (verbose >= 3)
fprintf(vis_stdout," add back %s (BNV)\n",
Ntk_NodeReadName(node));
}
}
if (verbose >= 3)
fprintf(vis_stdout,
"-- grab: minimize bnv refinement set: current size is %d\n",
n_size);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabMinimizeLatchRefinementSet | ( | Ntk_Network_t * | network, |
| st_table ** | absVarTable, | ||
| st_table ** | absBnvTable, | ||
| array_t * | newlyAddedLatches, | ||
| array_t ** | newlyAddedBnvs, | ||
| array_t * | SORs, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Minimize the refinement set of latch variable.]
Description [Minimize the refinement set of latch variable. After that, also prune away the boolean network variables that are no longer in the transitive fan-in.]
SideEffects []
Definition at line 813 of file grabUtil.c.
{
st_table *newVertexTable, *oldBnvTable, *transFaninTable;
array_t *rootArray, *transFanins, *oldNewlyAddedBnvs;
st_generator *stgen;
Ntk_Node_t *node;
int i, flag, n_size, mddId;
n_size = array_n(newlyAddedLatches);
if (verbose >= 3)
fprintf(vis_stdout,
"-- grab: minimize latch refinement set: previous size is %d\n",
n_size);
arrayForEachItem(int, newlyAddedLatches, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
/* first, try to drop it */
newVertexTable = st_copy(*absVarTable);
flag = st_delete(newVertexTable, &node, NIL(char *));
assert(flag);
/* if the counter-example does not come back, drop it officially */
flag = Bmc_AbstractCheckAbstractTraces(network,SORs,
newVertexTable, 0, 0, 0);
if (!flag) {
st_free_table(*absVarTable);
*absVarTable = newVertexTable;
n_size--;
}else {
st_free_table(newVertexTable);
if (verbose >= 3)
fprintf(vis_stdout," add back %s (latch)\n",
Ntk_NodeReadName(node));
}
}
if (verbose >= 3)
fprintf(vis_stdout,
"-- grab: minimize latch refinement set: current size is %d\n",
n_size);
/* prune away irrelevant BNVs */
if (*absBnvTable != NIL(st_table) && st_count(*absBnvTable)>0) {
rootArray = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(*absVarTable, stgen, &node, NIL(char *)) {
array_insert_last(Ntk_Node_t *, rootArray, Ntk_LatchReadDataInput(node));
array_insert_last(Ntk_Node_t *, rootArray,
Ntk_LatchReadInitialInput(node));
}
transFanins = Ntk_NodeComputeTransitiveFaninNodes(network, rootArray,
TRUE, /*stopAtLatch*/
FALSE /*combInputsOnly*/
);
array_free(rootArray);
transFaninTable = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(Ntk_Node_t *, transFanins, i, node) {
st_insert(transFaninTable, node, NIL(char));
}
array_free(transFanins);
oldBnvTable = *absBnvTable;
oldNewlyAddedBnvs = *newlyAddedBnvs;
*absBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
*newlyAddedBnvs = array_alloc(int, 0);
st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
if (st_is_member(transFaninTable, node))
st_insert(*absBnvTable, node, NIL(char));
}
arrayForEachItem(int, oldNewlyAddedBnvs, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
if (st_is_member(transFaninTable, node))
array_insert_last(int, *newlyAddedBnvs, mddId);
}
st_free_table(transFaninTable);
if (verbose >= 5) {
st_foreach_item(oldBnvTable, stgen, &node, NIL(char *)) {
if (!st_is_member(*absBnvTable, node))
fprintf(vis_stdout, " prune away BNV %s\n", Ntk_NodeReadName(node));
}
}
array_free(oldNewlyAddedBnvs);
st_free_table(oldBnvTable);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabNtkClearAllMddIds | ( | Ntk_Network_t * | network | ) |
Function********************************************************************
Synopsis [Clear the fields of mddId for all network nodes.]
Description [Clear the fields of mddId for all network nodes.]
SideEffects []
Definition at line 983 of file grabUtil.c.
{
#ifndef NDEBUG
mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
#endif
Ntk_Node_t *node;
lsGen lsgen;
assert(mddManager == NIL(mdd_manager));
Ntk_NetworkForEachNode(network, lsgen, node) {
Ntk_NodeSetMddId(node, NTK_UNASSIGNED_MDD_ID);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabPrintMddIdArray | ( | Ntk_Network_t * | network, |
| char * | caption, | ||
| array_t * | mddIdArray | ||
| ) |
Function********************************************************************
Synopsis [Print an array of network nodes.]
Description [Print an array of network nodes.]
SideEffects []
Definition at line 1049 of file grabUtil.c.
{
Ntk_Node_t *node;
array_t *theArray = array_alloc(Ntk_Node_t *, array_n(mddIdArray));
int i, mddId;
arrayForEachItem(int, mddIdArray, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
array_insert(Ntk_Node_t *, theArray, i, node);
}
GrabPrintNodeArray(caption, theArray);
array_free(theArray);
}
Here is the call graph for this function:
| void GrabPrintNodeArray | ( | char * | caption, |
| array_t * | theArray | ||
| ) |
Function********************************************************************
Synopsis [Print an array of network nodes.]
Description [Print an array of network nodes.]
SideEffects []
Definition at line 1009 of file grabUtil.c.
{
Ntk_Node_t *node;
char string[32];
int i;
fprintf(vis_stdout, "\n%s[%d] =\n", caption, theArray?array_n(theArray):0);
if (!theArray) return;
arrayForEachItem(Ntk_Node_t *, theArray, i, node) {
if (Ntk_NodeTestIsLatch(node))
strcpy(string, "latch");
else if (Ntk_NodeTestIsInput(node))
strcpy(string, "input");
else if (Ntk_NodeTestIsLatchDataInput(node))
strcpy(string, "latchDataIn");
else if (Ntk_NodeTestIsLatchInitialInput(node))
strcpy(string, "latchInitIn");
else if (Ntk_NodeTestIsConstant(node))
strcpy(string, "const");
else
strcpy(string, "BNV");
fprintf(vis_stdout, "%s\t(%s)\n", Ntk_NodeReadName(node), string);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabPrintNodeHashTable | ( | char * | caption, |
| st_table * | theTable | ||
| ) |
Function********************************************************************
Synopsis [Print a hash table of network nodes.]
Description [Print a hash table of network nodes.]
SideEffects []
Definition at line 1119 of file grabUtil.c.
{
Ntk_Node_t *node;
char string[32];
long value;
st_generator *stgen;
fprintf(vis_stdout, "\n%s[%d] =\n", caption, theTable?st_count(theTable):0);
if (!theTable) return;
st_foreach_item(theTable, stgen, &node, &value) {
if (Ntk_NodeTestIsLatch(node))
strcpy(string, "latch");
else if (Ntk_NodeTestIsInput(node))
strcpy(string, "input");
else if (Ntk_NodeTestIsLatchDataInput(node))
strcpy(string, "latchDataIn");
else if (Ntk_NodeTestIsLatchInitialInput(node))
strcpy(string, "latchInitIn");
else if (Ntk_NodeTestIsConstant(node))
strcpy(string, "const");
else
strcpy(string, "BNV");
if (value != 0)
fprintf(vis_stdout, " %s\t %s\t %ld\n", string, Ntk_NodeReadName(node),
value);
else
fprintf(vis_stdout, " %s\t %s \n", string, Ntk_NodeReadName(node));
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabPrintNodeList | ( | char * | caption, |
| lsList | theList | ||
| ) |
Function********************************************************************
Synopsis [Print a list of network nodes.]
Description [Print a list of network nodes.]
SideEffects []
Definition at line 1079 of file grabUtil.c.
{
Ntk_Node_t *node;
char string[32];
lsGen lsgen;
fprintf(vis_stdout, "\n%s[%d] =\n", caption, theList?lsLength(theList):0);
if (!theList) return;
lsForEachItem(theList, lsgen, node) {
if (Ntk_NodeTestIsLatch(node))
strcpy(string, "latch");
else if (Ntk_NodeTestIsInput(node))
strcpy(string, "input");
else if (Ntk_NodeTestIsLatchDataInput(node))
strcpy(string, "latchDataIn");
else if (Ntk_NodeTestIsLatchInitialInput(node))
strcpy(string, "latchInitIn");
else if (Ntk_NodeTestIsConstant(node))
strcpy(string, "const");
else
strcpy(string, "BNV");
fprintf(vis_stdout, " %s\t %s\n", string, Ntk_NodeReadName(node));
}
}
Here is the call graph for this function:
| int GrabTestRefinementBnvSetSufficient | ( | Ntk_Network_t * | network, |
| st_table * | coiBnvTable, | ||
| array_t * | SORs, | ||
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Test whether the refinement set of BNVs is sufficient.]
Description [Test whether the refinement set of BNVs is sufficient.]
SideEffects []
Definition at line 780 of file grabUtil.c.
{
int is_sufficient;
assert(absBnvTable && coiBnvTable);
is_sufficient =
!Bmc_AbstractCheckAbstractTracesWithFineGrain(network,
coiBnvTable,
SORs,
absVarTable,
absBnvTable);
return is_sufficient;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int GrabTestRefinementSetSufficient | ( | Ntk_Network_t * | network, |
| array_t * | SORs, | ||
| st_table * | absVarTable, | ||
| int | verbose | ||
| ) |
Function********************************************************************
Synopsis [Test whether the refinement set of latches is sufficient.]
Description [Test whether the refinement set of latches is sufficient.]
SideEffects []
Definition at line 755 of file grabUtil.c.
{
int is_sufficient;
is_sufficient = !Bmc_AbstractCheckAbstractTraces(network,
SORs,
absVarTable,
0, 0, 0);
return is_sufficient;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabUpdateAbstractPartition | ( | Ntk_Network_t * | network, |
| st_table * | coiBnvTable, | ||
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| int | partitionFlag | ||
| ) |
Function********************************************************************
Synopsis [Build or update partition for the current abstract model.]
Description [Build or update partition for the current abstract model. It is a two-phase process, in which the first phase generated the Bnvs---intermediate variables that should be created; while the second phase actually create the BDDs.
When a non-empty hash table 'absBnvTable' is given, BNVs not in this table should be treated as inputs---they should not appear in the partition either.
When 'absBnvTable' is not provided (e.g. when fine-grain abstraction is disabled), all relevant BNVs should appear in the partition.]
SideEffects []
Definition at line 171 of file grabUtil.c.
{
graph_t *newPart;
st_table *useAbsBnvTable = absBnvTable? absBnvTable:coiBnvTable;
if (partitionFlag == GRAB_PARTITION_BUILD) {
/* free the existing partition */
Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY);
/* insert bnvs whenever necessary. Note that when the current
* partition is not available, this function will create new bnvs
* and put them into the coiBnvTable. Otherwise, it retrieves
* existing bnvs from the current partiton */
Part_PartitionReadOrCreateBnvs(network, absVarTable, coiBnvTable);
/* create the new partition */
newPart = g_alloc();
newPart->user_data = (gGeneric)PartPartitionInfoCreate("default",
Ntk_NetworkReadMddManager(network),
Part_Frontier_c);
Part_PartitionWithExistingBnvs(network, newPart, coiBnvTable,
absVarTable, useAbsBnvTable);
Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
(void *) newPart);
}else if (partitionFlag == GRAB_PARTITION_UPDATE) {
fprintf(vis_stdout,
"\n ** grab error: GRAB_PARTITION_UPDATE not implemented\n");
assert(0);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NodeTableAddCtlFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula, | ||
| st_table * | nodesTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Add nodes for wires referred to in formula to nodesTable.]
SideEffects []
Definition at line 1229 of file grabUtil.c.
{
if (formula == NIL(Ctlp_Formula_t))
return;
if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
if( node )
st_insert( nodesTable, ( char *) node, NIL(char) );
return;
}
NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );
}
Here is the call graph for this function:
Here is the caller graph for this function:
