/**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.] ******************************************************************************/ #include "grabInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ st_table * GrabComputeCOIAbstraction( Ntk_Network_t *network, Ctlp_Formula_t *invFormula) { 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; } /**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 [] ******************************************************************************/ st_table * GrabComputeInitialAbstraction( Ntk_Network_t *network, Ctlp_Formula_t *invFormula) { 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; } /**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 [] ******************************************************************************/ void GrabUpdateAbstractPartition( Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag) { 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); } } /**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 [] ******************************************************************************/ Fsm_Fsm_t * GrabCreateAbstractFsm( Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag, int independentFlag) { 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; } /**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) = \exists u \[\prod (x_i = g_i(u))\]).] SideEffects [The result of the initial state computation is stored with the FSM.] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ mdd_t * GrabComputeInitialStates( Ntk_Network_t *network, array_t *psVars) { 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=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; } /**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 [] ******************************************************************************/ array_t * GrabGetVisibleVarMddIds ( Fsm_Fsm_t *absFsm, st_table *absVarTable) { 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; } /**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 [] ******************************************************************************/ array_t * GrabGetInvisibleVarMddIds( Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable) { 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; } /**Function******************************************************************** Synopsis [Test whether the refinement set of latches is sufficient.] Description [Test whether the refinement set of latches is sufficient.] SideEffects [] ******************************************************************************/ int GrabTestRefinementSetSufficient( Ntk_Network_t *network, array_t *SORs, st_table *absVarTable, int verbose) { int is_sufficient; is_sufficient = !Bmc_AbstractCheckAbstractTraces(network, SORs, absVarTable, 0, 0, 0); return is_sufficient; } /**Function******************************************************************** Synopsis [Test whether the refinement set of BNVs is sufficient.] Description [Test whether the refinement set of BNVs is sufficient.] SideEffects [] ******************************************************************************/ int GrabTestRefinementBnvSetSufficient( Ntk_Network_t *network, st_table *coiBnvTable, array_t *SORs, st_table *absVarTable, st_table *absBnvTable, int verbose) { int is_sufficient; assert(absBnvTable && coiBnvTable); is_sufficient = !Bmc_AbstractCheckAbstractTracesWithFineGrain(network, coiBnvTable, SORs, absVarTable, absBnvTable); return is_sufficient; } /**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 [] ******************************************************************************/ void GrabMinimizeLatchRefinementSet( Ntk_Network_t *network, st_table **absVarTable, st_table **absBnvTable, array_t *newlyAddedLatches, array_t **newlyAddedBnvs, array_t *SORs, int verbose) { 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); } } /**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 [] ******************************************************************************/ void GrabMinimizeBnvRefinementSet( Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table **absBnvTable, array_t *newlyAddedBnvs, array_t *SORs, int verbose) { 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); } /**Function******************************************************************** Synopsis [Clear the fields of mddId for all network nodes.] Description [Clear the fields of mddId for all network nodes.] SideEffects [] ******************************************************************************/ void GrabNtkClearAllMddIds( Ntk_Network_t *network) { #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); } } /**Function******************************************************************** Synopsis [Print an array of network nodes.] Description [Print an array of network nodes.] SideEffects [] ******************************************************************************/ void GrabPrintNodeArray( char *caption, array_t *theArray) { 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); } } /**Function******************************************************************** Synopsis [Print an array of network nodes.] Description [Print an array of network nodes.] SideEffects [] ******************************************************************************/ void GrabPrintMddIdArray( Ntk_Network_t *network, char *caption, array_t *mddIdArray) { 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); } /**Function******************************************************************** Synopsis [Print a list of network nodes.] Description [Print a list of network nodes.] SideEffects [] ******************************************************************************/ void GrabPrintNodeList( char *caption, lsList theList) { 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)); } } /**Function******************************************************************** Synopsis [Print a hash table of network nodes.] Description [Print a hash table of network nodes.] SideEffects [] ******************************************************************************/ void GrabPrintNodeHashTable( char *caption, st_table *theTable) { 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)); } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Get network nodes that are mentioned by the formula.] Description [Get network nodes that are mentioned by the formula.] SideEffects [] ******************************************************************************/ static void GetFormulaNodes( Ntk_Network_t *network, Ctlp_Formula_t *F, array_t *formulaNodes) { 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); } /**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 [] ******************************************************************************/ static void GetFaninLatches( Ntk_Node_t *node, st_table *visited, st_table *absVarTable) { 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); } } } /**Function******************************************************************** Synopsis [Add nodes for wires referred to in formula to nodesTable.] SideEffects [] ******************************************************************************/ static void NodeTableAddCtlFormulaNodes( Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable ) { 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 ); }