/**CFile*********************************************************************** FileName [puresatUtil.c] PackageName [puresat] Synopsis [Abstraction refinement for large scale invariant checking.] Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts: * Localization-reduction base Abstraction * K-induction or interpolation to prove the truth of a property * Bounded Model Checking to find bugs * Incremental concretization based methods to verify abstract bugs * Incremental SAT solver to improve efficiency * UNSAT proof based method to obtain refinement * AROSAT to bring in only necessary latches into unsat proofs * Bridge abstraction to get compact coarse refinement * Refinement minization to guarrantee minimal refinements * Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test * Refinement prediction to decrease the number of refinement iterations * Dynamic switching to redistribute computional resources to improve efficiency For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"] Author [Bing Li] 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 "puresatInt.h" #include "sat.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static array_t *RCArray; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [time out function] Description [time out function] SideEffects [] SeeAlso [] *******************************************************************************/ static int DfsLevel = 0; static array_t *NumInCone; static array_t *NumInAbs; static array_t *DfsArray; /*static array_t *RCArray;*/ /**Function******************************************************************** Synopsis [Allocate a puresat manager] Description [Allocate a puresat manager] SideEffects [] SeeAlso [] ******************************************************************************/ PureSat_Manager_t * PureSatManagerAlloc(void) { PureSat_Manager_t * pm = ALLOC(PureSat_Manager_t,1); memset(pm,0,sizeof(PureSat_Manager_t)); pm->incre = TRUE; pm->ltlFileName = ALLOC(char,200); pm->timeOutPeriod = 10000000; pm->Arosat = TRUE;; pm->CoreRefMin = TRUE; pm->RefPredict = TRUE; pm->Switch = TRUE; return pm; } /**Function******************************************************************** Synopsis [Free a puresat manager] Description [Free a puresat manager] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatManagerFree(PureSat_Manager_t * pm){ if(pm->latchToTableBaigNodes) st_free_table(pm->latchToTableBaigNodes); if(pm->ClsidxToLatchTable) st_free_table(pm->ClsidxToLatchTable); if(pm->CoiTable) st_free_table(pm->CoiTable); if(pm->AbsTable) st_free_table(pm->AbsTable); if(pm->vertexTable) st_free_table(pm->vertexTable); if(pm->SufAbsTable) st_free_table(pm->SufAbsTable);; if(pm->supportTable) st_free_table(pm->supportTable); if(pm->node2dfsTable) st_free_table(pm->node2dfsTable); if(pm->result!=NIL(array_t)) array_free(pm->result); FREE(pm->ltlFileName); FREE(pm); } /**Function******************************************************************** Synopsis [Allocate a puresat incremental SAT manager] Description [Allocate a puresat incremental SAT manager] SideEffects [] SeeAlso [] ******************************************************************************/ PureSat_IncreSATManager_t * PureSatIncreSATManagerAlloc(PureSat_Manager_t * pm) { PureSat_IncreSATManager_t * pism = ALLOC(PureSat_IncreSATManager_t,1); pism->beginPosition = 0; pism->Length = 0; pism->oldLength = 0; pism->propertyPos = 0; memset(pism,0,sizeof(PureSat_IncreSATManager_t)); if(pm->sss){ pism->cnfClauses = BmcCnfClausesAlloc(); pism->cm = sat_InitManager(0); pism->cm->comment = ALLOC(char, 2); pism->cm->comment[0] = ' '; pism->cm->comment[1] = '\0'; pism->cm->maxNodesArraySize = 1; pism->cm->nodesArray = ALLOC(long, pism->cm->maxNodesArraySize ); pism->cm->nodesArraySize = satNodeSize; pism->cm->stdErr = vis_stderr; pism->cm->stdOut = vis_stdout; pism->cm->unitLits = sat_ArrayAlloc(16); pism->cm->pureLits = sat_ArrayAlloc(16); pism->cm->each = sat_InitStatistics(); pism->cm->option = sat_InitOption(); pism->cm->option->ForceFinish = 1; pism->cm->option->incTraceObjective = 1; pism->cm->option->includeLevelZeroLiteral = 1; pism->cm->option->minimizeConflictClause = 0; pism->cm->option->SSS = 1; } return pism; } /**Function******************************************************************** Synopsis [Free a puresat incremental SAT manager] Description [Free a puresat incremental SAT manager] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatIncreSATManagerFree(PureSat_Manager_t *pm, PureSat_IncreSATManager_t * pism) { if(pm->sss){ BmcCnfClausesFree(pism->cnfClauses); FREE(pism->cm->nodesArray); sat_ArrayFree(pism->cm->unitLits); sat_ArrayFree(pism->cm->pureLits); sat_FreeStatistics(pism->cm->each); sat_FreeOption(pism->cm->option); FREE(pism->cm); } FREE(pism); } /**Function******************************************************************** Synopsis [Get the cone of influence for a network node] Description [Get the cone of influence for a network node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForNtkNode( Ntk_Node_t *node, st_table *CoiTable, st_table *visited) { int i, j; Ntk_Node_t *faninNode; if(node == NIL(Ntk_Node_t)){ return; } if(Ntk_NodeTestIsLatch(node)){ DfsLevel++; if (st_lookup_int(CoiTable, node, &j)&&j<=DfsLevel){ DfsLevel--; return; } } if (st_lookup_int(visited, node, &j)&&j<=DfsLevel){ if(Ntk_NodeTestIsLatch(node)) DfsLevel--; return; } st_insert(visited, node, (char *)(long)DfsLevel); if (Ntk_NodeTestIsLatch(node)){ st_insert(CoiTable, node, (char *)(long)DfsLevel); } if(Ntk_NodeTestIsInput(node)) { return; } Ntk_NodeForEachFanin(node, i, faninNode) { PureSatBmcGetCoiForNtkNode(faninNode, CoiTable, visited); } if(Ntk_NodeTestIsLatch(node)) DfsLevel--; return; } /**Function******************************************************************** Synopsis [Get the cone of influence for a ltl formula] Description [Get the cone of influence for a ltl formula] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForLtlFormulaRecursive( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited) { if (formula == NIL(Ctlsp_Formula_t)) { return; } /* leaf node */ if (formula->type == Ctlsp_ID_c){ char *name = Ctlsp_FormulaReadVariableName(formula); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name); int tmp; if (st_lookup_int(visited, node, &tmp)){ /* Node already visited */ return; } PureSatBmcGetCoiForNtkNode(node, ltlCoiTable, visited); return; } PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->left, ltlCoiTable, visited); PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited); return; } /**Function******************************************************************** Synopsis [Get the color of a node] Description [Get the color of a node] SideEffects [] SeeAlso [] ******************************************************************************/ DfsColor PureSatNodeReadColor( Ntk_Node_t * node) { return ((DfsColor) (long) Ntk_NodeReadUndef(node)); } /**Function******************************************************************** Synopsis [Set the color of a node] Description [Set the color of a node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatNodeSetColor( Ntk_Node_t * node, DfsColor color) { Ntk_NodeSetUndef(node, (void *) (long) color); } /**Function******************************************************************** Synopsis [Recursively compute the transitive fan in nodes of a node] Description [Recursively compute the transitive fan in nodes of a node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( Ntk_Node_t *node, int * NumofSupports, boolean stopAtLatches) { int i; Ntk_Node_t * fanin; /* test if we have already started processing this node */ if ( PureSatNodeReadColor( node ) == dfsBlack_c ) { return; } PureSatNodeSetColor( node, dfsBlack_c ); /* if ( Ntk_NodeTestIsCombInput( node ) ) { st_insert( resultTable, (char *) node, (char *) 0 ); }*/ (*NumofSupports)++; if ( Ntk_NodeTestIsInput(node) || ((stopAtLatches == TRUE)&&(Ntk_NodeTestIsLatch(node))) ) { return; } Ntk_NodeForEachFanin( node, i, fanin ) { PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( fanin, NumofSupports, stopAtLatches ); } } /**Function******************************************************************** Synopsis [Get the number of combination support of a node] Description [Get the number of combination support of a node] SideEffects [] SeeAlso [] ******************************************************************************/ int PureSatNodeComputeCombinationalSupport_AllNodes( Ntk_Network_t *network, array_t * nodeArray, boolean stopAtLatches ) { lsGen gen; int i, NumofSupports=0; Ntk_Node_t *node; Ntk_NetworkForEachNode( network, gen, node ) { PureSatNodeSetColor( node, dfsWhite_c ); } /* for each lacthes(node) in the nodeArray, compute the number of gates in the cone of this latch, put the number in NumofSupports*/ arrayForEachItem( Ntk_Node_t *, nodeArray, i, node ) { NumofSupports = 0; PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( node, &NumofSupports, stopAtLatches ); } return NumofSupports; } /**Function******************************************************************** Synopsis [Build a support table,each value associated with a latch is the number of gates in its cone of influence ] Description [Build a support table,each value associated with a latch is the number of gates in its cone of influence ] SideEffects [] SeeAlso [] ******************************************************************************/ /*build a supportTable, each value associated with a latch is NumofGatesInCone*/ void PureSatGenerateSupportTable( Ntk_Network_t *network, PureSat_Manager_t *pm) { array_t *roots = array_alloc(Ntk_Node_t *,0); /*supports;*/ st_generator *stgen; Ntk_Node_t *node,*DataNode=(Ntk_Node_t *)0; int count, NumofSupports; st_foreach_item_int(pm->CoiTable, stgen, &node, &count) { if (Ntk_NodeTestIsLatch(node)) DataNode = Ntk_LatchReadDataInput(node); array_insert(Ntk_Node_t *, roots, 0, DataNode); NumofSupports = PureSatNodeComputeCombinationalSupport_AllNodes(network, roots,FALSE); st_insert(pm->supportTable,node, (char *)(long)NumofSupports); } array_free(roots); } /**Function******************************************************************** Synopsis [Compute the cone of influence for a ltl formula] Description [Compute the cone of influence for a ltl formula] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForLtlFormula( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) { st_table *visited = st_init_table(st_ptrcmp, st_ptrhash); PureSatBmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited); st_free_table(visited); return; } /**Function******************************************************************** Synopsis [] Description [recursively compute the nodes in a ltl formula and put them in an array] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGetFormulaNodes( Ntk_Network_t *network, Ctlsp_Formula_t *F, array_t *formulaNodes) { if (F == NIL(Ctlsp_Formula_t)) return; if (Ctlsp_FormulaReadType(F) == Ctlsp_ID_c) { char *nodeNameString = Ctlsp_FormulaReadVariableName(F); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString); assert(node); array_insert_last(Ntk_Node_t *, formulaNodes, node); return; } PureSatGetFormulaNodes(network, Ctlsp_FormulaReadRightChild(F), formulaNodes); PureSatGetFormulaNodes(network, Ctlsp_FormulaReadLeftChild(F), formulaNodes); } /**Function******************************************************************** Synopsis [Get direct fan in latches for a node] Description [Get direct fan in latches for a node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGetFaninLatches( Ntk_Node_t *node, st_table *visited, st_table *vertexTable) { if (st_is_member(visited, node)) return; st_insert(visited, node, (char *)0); if (Ntk_NodeTestIsLatch(node)) st_insert(vertexTable, Ntk_NodeReadName(node), (char *)0); else { int i; Ntk_Node_t *fanin; Ntk_NodeForEachFanin(node, i, fanin) { PureSatGetFaninLatches(fanin, visited, vertexTable); } } } /**Function******************************************************************** Synopsis [Build a vertex table which stores all the latches in the beginning abstract model] Description [The table contains only those immediate fanin latches of the given formula.] SideEffects [] SeeAlso [] ******************************************************************************/ st_table * PureSatCreateInitialAbstraction( Ntk_Network_t *network, Ctlsp_Formula_t *invFormula, int * Num, PureSat_Manager_t *pm) { array_t *formulaNodes = array_alloc(Ntk_Node_t *, 0); Ntk_Node_t *node; int i; st_table *vertexTable = st_init_table(strcmp, st_strhash); st_table *visited = st_init_table(st_ptrcmp, st_ptrhash); *Num=0; PureSatGetFormulaNodes(network, invFormula, formulaNodes); arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) { PureSatGetFaninLatches(node, visited, vertexTable); } st_free_table(visited); array_free(formulaNodes); if (1) { st_generator *stgen; char *nodeNameString; if(pm->verbosity>=1) fprintf(vis_stdout, "\n Create_InitialAbstraction() =\n"); st_foreach_item(vertexTable, stgen, &nodeNameString, 0) { if(pm->verbosity>=1) fprintf(vis_stdout, "%s\n", nodeNameString); (*Num)++; } if(pm->verbosity>=1){ fprintf(vis_stdout, "\n"); fflush(vis_stdout); } } return vertexTable; } /**Function******************************************************************** Synopsis [Recursively get direct fan in gates of a node] Description [Recursively get direct fan in gates of a node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatRecursivelyComputeTableForLatch(Ntk_Network_t * network, st_table *Table, Ntk_Node_t * node) { int i; Ntk_Node_t * fanin; //want input to be in the Table if(Ntk_NodeTestIsLatch(node)) return; if(!st_lookup(Table,node,NIL(char *))) st_insert(Table,node, (char *)0); else return; if ( Ntk_NodeTestIsCombInput(node)) { return; } Ntk_NodeForEachFanin( node,i,fanin) PureSatRecursivelyComputeTableForLatch(network,Table,fanin); } /**Function******************************************************************** Synopsis [Get direct fan in gates of a node] Description [Get direct fan in gates of a node] SideEffects [] SeeAlso [] ******************************************************************************/ /* put all the gates of Abs model to the Table */ void PureSatComputeTableForLatch(Ntk_Network_t * network, st_table * Table, Ntk_Node_t * Latch) { Ntk_Node_t * fanin; int i; if(!Ntk_NodeTestIsLatch(Latch)) { char * name = Ntk_NodeReadName(Latch); fprintf(vis_stdout,"%s is not a latch!\n",name); exit (0); } if(!st_lookup(Table,Latch,NIL(char *))) { st_insert(Table,Latch, (char *)0); Ntk_NodeForEachFanin(Latch,i,fanin) PureSatRecursivelyComputeTableForLatch(network,Table,fanin); } } /**Function******************************************************************** Synopsis [Take latches in visibleArray as the first level compute the DFS level of each latch in ltlCoiTable] Description [Take latches in visibleArray as the first level compute the DFS level of each latch in ltlCoiTable] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGetCoiForVisibleArray_Ring( Ntk_Network_t *network, array_t *visibleArray, int position, st_table *ltlCoiTable) { int i; char * name; Ntk_Node_t * node; st_table *visited = st_init_table(st_ptrcmp, st_ptrhash); for(i=position;i f) return -1; if( e < f) return 1; return 0; } /**Function******************************************************************** Synopsis [Compare function for quick sort] Description [Compare function for quick sort] SideEffects [] SeeAlso [] ******************************************************************************/ int NumInConeCompare_Ring(int *ptrX, int *ptrY) { int a,b; double c,d; double e,f; a = array_fetch(int,DfsArray,(int)*ptrX); b = array_fetch(int,DfsArray,(int)*ptrY); c = array_fetch(double,RCArray,(int)*ptrX); d = array_fetch(double,RCArray,(int)*ptrY); e = (double)((a)*1000000)-c; f = (double)((b)*1000000)-d; if(e > f) return 1; if( e < f) return -1; return 0; } /**Function******************************************************************** Synopsis [Recursively compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"] Description [Recursively compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatRecursivelyComputeCorrelationforLatch(Ntk_Network_t *network, st_table *AbsTable, st_table * visited, Ntk_Node_t *node, int *count) { Ntk_Node_t * fanin; int i; if(!st_lookup(visited,node,NIL(char *))) { st_insert(visited,node,(char *)0); if(st_lookup(AbsTable,node,NIL(char *))) { (*count)++; } } else return; if(Ntk_NodeTestIsCombInput(node)) return; Ntk_NodeForEachFanin(node,i,fanin) PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,count); } /**Function******************************************************************** Synopsis [Compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"] Description [Compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"] SideEffects [] SeeAlso [] ******************************************************************************/ int PureSatComputeCorrelationforLatch(Ntk_Network_t * network, st_table * AbsTable, Ntk_Node_t *Latch) { int count =0,i; Ntk_Node_t * fanin; st_table *visited = st_init_table(st_ptrcmp,st_ptrhash); Ntk_NodeForEachFanin(Latch,i,fanin) PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,&count); st_free_table(visited); return count*10000; } /**Function******************************************************************** Synopsis [Generating the ring information needed for the computation of the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure] Description [Generating the ring information needed for the computation of the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatGenerateRingFromAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int * NumInSecondLevel) { st_table *CoiTable = pm->CoiTable; st_table *supportTable = pm->supportTable; st_table *AbsTable= pm->AbsTable; array_t * arrayRC = array_alloc(char *,array_n(invisibleArray)),* NumInConeArray = array_alloc(int,0),* NumInAbsArray = array_alloc(int,0); array_t * tmpNumInCone = array_alloc(int,0),* tmpNumInAbs = array_alloc(int,0); array_t * tmpDfsArray = array_alloc(int,0), *tmpRCArray = array_alloc(double,0); array_t * tmpDfsArray1 = array_alloc(int,0), *tmpRCArray1 = array_alloc(double,0); int numincone,i,j,dfs; char *name; double d1; (*NumInSecondLevel) = 0; for(i=0;iverbosity>=2){ int i1; double d1,d2; i1 = array_fetch(int,tmpDfsArray1,i)*1000000; d1 = array_fetch(double,tmpRCArray1,i); d2 = (double)array_fetch(int,tmpDfsArray1,i)*1000000 - d1; if(pm->verbosity>=1) fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,i1,d1,d2); /* fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,array_fetch(int,tmpDfsArray1,i)*1000000,array_fetch(double,tmpRCArray1,i), (double)array_fetch(int,tmpDfsArray1,i)*1000000-(double)array_fetch(double,tmpRCArray1,i));*/ } } FREE(tay); } array_free(NumInConeArray); array_free(NumInAbsArray); array_free(tmpNumInCone); array_free(tmpNumInAbs); array_free(tmpDfsArray); array_free(tmpRCArray); array_free(tmpDfsArray1); array_free(tmpRCArray1); return arrayRC; } /**Function******************************************************************** Synopsis [Clean the SAT solver after a SAT solving procedure is done] Description [Clean the SAT solver after a SAT solving procedure is done] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCleanSat(satManager_t * cm) { int i; satVariable_t *var; satLevel_t *d; cm->nodesArraySize = satNodeSize; sat_ArrayFree(cm->unitLits); sat_ArrayFree(cm->pureLits); cm->unitLits = sat_ArrayAlloc(16); cm->pureLits = sat_ArrayAlloc(16); memset(cm->each,0,sizeof(satStatistics_t)); cm->literals->last = cm->literals->begin+1; cm->literals->initialSize = cm->literals->last; cm->status = 0; cm->currentVarPos = 0; cm->currentTopConflict = 0; cm->lowestBacktrackLevel = 0; cm->implicatedSoFar = 0; /*cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);*/ memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize); /* FREE(cm->variableArray); cm->variableArray = 0;*/ if(cm->variableArray) { for(i=0; i<=cm->initNumVariables; i++) { var = &(cm->variableArray[i]); if(var->wl[0]) { sat_ArrayFree(var->wl[0]); var->wl[0] = 0; } if(var->wl[1]) { sat_ArrayFree(var->wl[1]); var->wl[1] = 0; } } free(cm->variableArray); cm->variableArray = 0; } if(cm->decisionHead) { for(i=0; idecisionHeadSize; i++) { d = &(cm->decisionHead[i]); if(d->implied) sat_ArrayFree(d->implied); if(d->satisfied) sat_ArrayFree(d->satisfied); } free(cm->decisionHead); cm->decisionHead = 0; cm->decisionHeadSize = 0; } sat_FreeQueue(cm->queue); cm->queue = 0; sat_FreeQueue(cm->BDDQueue); cm->BDDQueue = 0; sat_FreeQueue(cm->unusedAigQueue); cm->unusedAigQueue = 0; sat_ArrayFree(cm->auxArray); sat_ArrayFree(cm->nonobjUnitLitArray); sat_ArrayFree(cm->objUnitLitArray); } /**Function******************************************************************** Synopsis [Read clauses from a puresat incremental SAT manager to the CirCUs SAT solver] Description [Read clauses from a puresat incremental SAT manager to the CirCUs SAT solver] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatReadClauses(PureSat_IncreSATManager_t * pism, PureSat_Manager_t * pm) { int i,node,nVar = pism->cnfClauses->cnfGlobalIndex - 1; satManager_t * cm = pism->cm; satArray_t * clauseArray; cm->option->verbose = pm->verbosity; cm->initNumVariables = nVar; cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1); memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1)); if(cm->maxNodesArraySize <= (cm->initNumVariables+2)*satNodeSize){ cm->nodesArray = ALLOC(long, (cm->initNumVariables+2)*satNodeSize); cm->maxNodesArraySize = (cm->initNumVariables+2)*satNodeSize; } if(pism->cm->option->coreGeneration){ pism->cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash); /*the tables stroes entry of (var_node_idx,cls_idx);*/ pism->cm->anteTable = st_init_table(st_numcmp, st_numhash); } sat_AllocLiteralsDB(cm); for(i=1;i<=nVar;i++){ node = sat_CreateNode(cm,2,2); SATflags(node) |= CoiMask; SATvalue(node) = 2; /*SATfanout(node) = 0;*/ cm->nodesArray[node+satFanout] = 0; SATnFanout(node) = 0; } clauseArray = sat_ArrayAlloc(4096); for(i=0; icnfClauses->nextIndex;i++){ int k, cls_idx,v; k = array_fetch(int,pism->cnfClauses->clauseArray,i); if(k!=0){ int sign = 1; if(k<0){ sign = 0; k = -k; } v = k*satNodeSize + sign; sat_ArrayInsert(clauseArray, v); } else{ if(clauseArray->num == 1) { v = clauseArray->space[0]; sat_ArrayInsert(cm->unitLits, SATnot(v)); cls_idx = sat_AddUnitClause(cm, clauseArray); if(pism->cm->option->coreGeneration){ v = SATnormalNode(v); st_insert(pism->cm->anteTable,(char *)(long)v,(char *)(long)cls_idx); } } else{ cls_idx = sat_AddClause(cm, clauseArray); } cm->initNumClauses++; cm->initNumLiterals += clauseArray->num; if(i>pism->propertyPos) SATflags(cls_idx) |= ObjMask; clauseArray->num = 0; } } sat_ArrayFree(clauseArray); } /**Function******************************************************************** Synopsis [Get immediate latch supports for latches in latchNameArray] Description [Get immediate latch supports for latches in latchNameArray] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatGetImmediateSupportLatches( Ntk_Network_t *network, int beginPosition, array_t *latchNameArray) { /* old support, form 0 to 'beginPosition'-1*/ array_t *dataInputs, *supports; /* new support, from 'beginPosition' to array_n(latchNameArray)-1*/ array_t *dataInputs2, *supports2, *supportLatches2; /* The result should be {new support}-{old support}*/ st_table *oldSupportTable; Ntk_Node_t *latch, *dataInput; int i; char *latchName; dataInputs = array_alloc(Ntk_Node_t *, 0); dataInputs2 = array_alloc(Ntk_Node_t *, 0); arrayForEachItem(char *, latchNameArray, i, latchName) { latch = Ntk_NetworkFindNodeByName(network, latchName); assert(latch); assert(Ntk_NodeTestIsLatch(latch)); dataInput = Ntk_LatchReadDataInput(latch); if (i < beginPosition) array_insert_last(Ntk_Node_t *, dataInputs, dataInput); else array_insert_last(Ntk_Node_t *, dataInputs2, dataInput); } supports = Ntk_NodeComputeCombinationalSupport(network, dataInputs, 1); supports2 = Ntk_NodeComputeCombinationalSupport(network, dataInputs2, 1); array_free(dataInputs); array_free(dataInputs2); oldSupportTable = st_init_table(st_ptrcmp, st_ptrhash); arrayForEachItem(Ntk_Node_t *, supports, i, latch) { st_insert(oldSupportTable, latch, NIL(char)); } array_free(supports); supportLatches2 = array_alloc(char *, 0); arrayForEachItem(Ntk_Node_t *, supports2, i, latch) { if (Ntk_NodeTestIsLatch(latch) && !st_is_member(oldSupportTable,latch)) array_insert_last(char *, supportLatches2, Ntk_NodeReadName(latch)); } array_free(supports2); arrayForEachItem(char *, latchNameArray, i, latchName) { if (i < beginPosition) continue; latch = Ntk_NetworkFindNodeByName(network, latchName); if (!st_is_member(oldSupportTable, latch)) array_insert_last(char *, supportLatches2, latchName); } st_free_table(oldSupportTable); return supportLatches2; } /**Function******************************************************************** Synopsis [Dump out clauses to a file] Description [Dump out clauses to a file] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatWriteClausesToFile(PureSat_IncreSATManager_t * pism, mAig_Manager_t *maigManager, char *coreFile) { BmcCnfClauses_t *cnfClauses = pism->cnfClauses; st_generator *stGen; char *name; int cnfIndex, i, k; FILE *cnfFile; coreFile = BmcCreateTmpFile(); cnfFile = fopen(coreFile,"w"); fprintf(vis_stdout, "coreFile is %s\n", coreFile); fprintf(vis_stdout, "Number of Variables = %d Number of Clauses = %d\n", cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) { fprintf(cnfFile, "c %s %d\n",name, cnfIndex); } (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); if (cnfClauses->clauseArray != NIL(array_t)) { for (i = 0; i < cnfClauses->nextIndex; i++) { k = array_fetch(int, cnfClauses->clauseArray, i); (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' '); } } fclose(cnfFile); FREE(coreFile); return; } /**Function******************************************************************** Synopsis [Dump out all the clauses, including conflict clauses, to a file] Description [Dump out all the clauses, including conflict clauses, to a file] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatWriteAllClausesToFile(PureSat_IncreSATManager_t * pism, char *coreFile) { satManager_t *cm = pism->cm; char *tmpallcnfFile = BmcCreateTmpFile(); FILE *fp1 = fopen(coreFile,"r"); FILE *fp2 = fopen(tmpallcnfFile,"w"); char buffer[1024], buffer1[1024]; long *space; int i, numOfConCls=0, numOfVar, sign,var; satArray_t *saved = cm->savedConflictClauses; for(i=0, space=saved->space; inum; i++,space++){ if(*space<0) numOfConCls++; } if(numOfConCls%2!=0){ fprintf(vis_stdout,"should be times of 2\n"); exit(0); } numOfConCls/=2; numOfConCls += cm->initNumClauses; numOfVar = cm->initNumVariables; i=0; /*sprintf(buffer,"p cnf %d %d 0\n", numOfConCls, numOfVar); fputs(buffer, fp2);*/ while(fgets(buffer,1024,fp1)){ if(strncmp(buffer,"c ",2)!=0){ if(strncmp(buffer,"p cnf ",6)==0){ sprintf(buffer1,"p cnf %d %d 0\n", numOfVar, numOfConCls); fputs(buffer1, fp2); } else fputs(buffer, fp2); } } saved = cm->savedConflictClauses; for(i=0, space=saved->space; inum; i++){ if(*space<0){ space++; i++; while(*space>0){ sign = !SATisInverted(*space); var = SATnormalNode(*space); if(sign == 0) var = -var; fprintf(fp2,"%d ",var); space++; i++; } fprintf(fp2,"0\n"); space++; i++; } } fclose(fp1); fclose(fp2); FREE(tmpallcnfFile); } /**Function******************************************************************** Synopsis [Generate refinement latches from UNSAT proof] Description [Generate refinement latches from UNSAT proof] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatGetLatchFromTable(Ntk_Network_t *network, PureSat_Manager_t * pm, char *coreFile) { FILE *fp; char buffer[1024],*nodeName; int idx; st_table * localTable = st_init_table(strcmp,st_strhash); array_t * refinement = array_alloc(char *,0); st_table *ClsidxToLatchTable = pm->ClsidxToLatchTable; st_table *vertexTable = pm->vertexTable; fp = fopen(coreFile,"r"); while(fgets(buffer,1024,fp)){ if(strncmp(buffer,"#clause index:",14)==0){ sscanf(buffer,"#clause index:%d\n",&idx); if(st_lookup(ClsidxToLatchTable,(char *)(long)idx,&nodeName)) if(!st_lookup(vertexTable,nodeName,NIL(char *))&&!st_lookup(localTable,nodeName,NIL(char *))) { st_insert(localTable,nodeName,(char *)0); array_insert_last(char *,refinement,nodeName); } } } st_free_table(localTable); return refinement; } /**Function******************************************************************** Synopsis [remove the ith member of a certain array] Description [remove the ith member of a certain array] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatRemove_char(array_t * array1, int i) { int j; char * str; array_t * array2=array_alloc(char *,0); assert(iAbsTable,node,NIL(char*))) (*ct)++; if(Ntk_NodeTestIsCombInput(node)) return; Ntk_NodeForEachFanin(node,i,fanin){ if(!st_lookup(visited,(char *)fanin,NIL(char *))&& !Ntk_NodeTestIsLatch(fanin)) PureSatComputeNumGatesInAbsForNode(network,pm,fanin,visited,ct,ct1); } return; } /**Function******************************************************************** Synopsis [For nodes in one array: count number of gates and how many of them are already in abstraction] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatComputeNumGatesInAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t * invisibleArray) { int i,ct,ct1,j; char * name; Ntk_Node_t * node,*fanin; st_table * visited; arrayForEachItem(char*,invisibleArray,i,name){ node = Ntk_NetworkFindNodeByName(network,name); ct = 0; ct1 = 0; visited = st_init_table(st_ptrcmp,st_ptrhash); st_insert(visited,node,(char *)0); ct1++; Ntk_NodeForEachFanin(node,j,fanin){ if(!st_lookup(visited,(char *)fanin,NIL(char *))&& !Ntk_NodeTestIsLatch(fanin)) PureSatComputeNumGatesInAbsForNode(network,pm, fanin,visited,&ct,&ct1); } st_insert(pm->niaTable,name,(char*)(long)ct); st_free_table(visited); } return; } /**Function******************************************************************** Synopsis [For one node: count how many nodes are in its cone] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatComputeNumGatesInConeForNode(Ntk_Network_t * network, PureSat_Manager_t * pm, Ntk_Node_t * node, st_table * visited, int * ct) { int i; Ntk_Node_t *fanin; st_insert(visited,node,(char *)0); (*ct)++; if(Ntk_NodeTestIsCombInput(node)) return; Ntk_NodeForEachFanin(node,i,fanin){ if(!st_lookup(visited,(char *)fanin,NIL(char *))&& !Ntk_NodeTestIsLatch(fanin)) PureSatComputeNumGatesInConeForNode(network,pm,fanin,visited,ct); } return; } /**Function******************************************************************** Synopsis [For each node in one array: count how many nodes are in its cone] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatComputeNumGatesInCone(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t * latchArray) { int i,ct,j; char * name; Ntk_Node_t * node,* fanin; st_table * visited; arrayForEachItem(char*,latchArray,i,name){ node = Ntk_NetworkFindNodeByName(network,name); ct = 0; visited = st_init_table(st_ptrcmp,st_ptrhash); st_insert(visited,node,(char *)0); ct++; Ntk_NodeForEachFanin(node,j,fanin){ if(!st_lookup(visited,(char *)fanin,NIL(char *))&& !Ntk_NodeTestIsLatch(fanin)) PureSatComputeNumGatesInConeForNode(network,pm ,fanin,visited,&ct); } st_insert(pm->nicTable,name,(char*)(long)ct); st_free_table(visited); } return; } /**Function******************************************************************** Synopsis [Generate latch candidate array based on BFS ring and RC information] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatGenerateRCArray_2(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int *NumInSecondLevel) { array_t * tmpRCArray = array_alloc(double,0); array_t * tmpDfsArray = array_alloc(int,0); array_t * arrayRC = array_alloc(char*,array_n(invisibleArray)); int i,j; char * name; if(pm->RefPredict) pm->latchArray = array_alloc(char *,0); PureSatComputeNumGatesInAbs(network,pm,invisibleArray); for(i=0;inode2dfsTable,name,&dfs); assert(retVal); array_insert_last(int,tmpDfsArray,dfs); retVal = st_lookup(pm->nicTable,name,&nic); assert(retVal); retVal = st_lookup(pm->niaTable,name,&nia); assert(retVal); array_insert_last(double,tmpRCArray, (double)nia/(double)nic); } DfsArray = tmpDfsArray; RCArray = tmpRCArray; *NumInSecondLevel = 0; { int tmpvalue; double rcvalue; int nn = array_n(invisibleArray); int *tay=ALLOC(int,nn); for(j=0;jverbosity>=1) fprintf(vis_stdout,"arrayRC %s: %f-%f = %f\n",name, (double)tmpvalue*1000000,rcvalue,(double)tmpvalue*1000000-rcvalue); if(pm->RefPredict){ if(rcvalue>=0.87&&tmpvalue==2){ array_insert_last(char*,pm->latchArray,name); if(pm->verbosity>=1) fprintf(vis_stdout,"add %s into pm->latchArray\n",name); } } } FREE(tay); } array_free(DfsArray); array_free(RCArray); return arrayRC; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/