/**CFile*********************************************************************** FileName [puresatIPUtil.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" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ /**Function******************************************************************** Synopsis [Comparison function for sorting] Description [Comparison function for sorting] SideEffects [] SeeAlso [] ******************************************************************************/ static int NodeIndexCompare(const void *x, const void *y) { int n1, n2; n1 = *(int *)x; n2 = *(int *)y; return(n1 > n2); } /**Function******************************************************************** Synopsis [] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int StringCheckIsInteger( char *string, int *value) { char *ptr; long l; l = strtol (string, &ptr, 0) ; if(*ptr != '\0') return 0; if ((l > MAXINT) || (l < -1 - MAXINT)) return 1 ; *value = (int) l; return 2 ; } /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Create a node for resolution tree] Description [Create a node for resolution tree] SideEffects [] SeeAlso [] ******************************************************************************/ RTnode_t RTCreateNode(RTManager_t * rm) { RTnode_t node; if(rm->nArray==0){ rm->nArray = ALLOC(long, RTnodeSize*RT_BLOCK); rm->maxSize = RTnodeSize*RT_BLOCK; rm->aSize = 0; } if(rm->maxSize<=rm->aSize+RTnodeSize){ rm->nArray = REALLOC(long, rm->nArray,rm->maxSize+RTnodeSize*RT_BLOCK); if(rm->nArray == 0){ fprintf(vis_stdout,"memout when alloc %ld bytes\n", (rm->maxSize+RTnodeSize*RT_BLOCK)*4); exit(0); } rm->maxSize = rm->maxSize+RTnodeSize*1000; } rm->aSize += RTnodeSize; node = rm->aSize; RT_fSize(node) = 0; RT_formula(node) = 0; RT_oriClsIdx(node) = 0; RT_pivot(node) = 0; RT_flag(node) = 0; RT_IPnode(node) = -1; RT_left(node) = 0; RT_right(node) = 0; if(rm->fArray==0){ rm->fArray = ALLOC(long,FORMULA_BLOCK); rm->cpos = 0; rm->maxpos = FORMULA_BLOCK; } return node; } /**Function******************************************************************** Synopsis [Allocate an interpolation manager] Description [Allocate an interpolation manager] SideEffects [] SeeAlso [] ******************************************************************************/ IP_Manager_t * IPManagerAlloc() { IP_Manager_t * ipm = ALLOC(IP_Manager_t, 1); memset(ipm,0,sizeof(IP_Manager_t)); return ipm; } /**Function******************************************************************** Synopsis [Free an interpolation manager] Description [Free an interpolation manager] SideEffects [] SeeAlso [] ******************************************************************************/ void IPManagerFree(IP_Manager_t *ipm) { FREE(ipm); } /**Function******************************************************************** Synopsis [Find the type of conflict, return the value to caller] Description [ 0 1 1 1 1 1 | | | | | | 20---33,49--- 9,13--- 17 --- 5 --- 1--- / \ / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 0 0 Bing note: For case 1, maybe solving conflict with both childern is better, but in sat package, only conflict with left child is solved ] SideEffects [] SeeAlso [] ******************************************************************************/ int PureSat_IdentifyConflict( satManager_t *cm, long left, bAigEdge_t right, bAigEdge_t node) { int result; /*1:left 2:right 3:both*/ int value = SATgetValue(left,right,node); switch(value){ case 1: case 5: case 9: case 13: result = 1; break; case 17: case 33: case 49: result = 2; break; case 20: result = 3; break; default: fprintf(vis_stdout,"can't identify the conflict, exit\n"); exit(0); } return result; } /**Function******************************************************************** Synopsis [Get COI for a network node] Description [Get COI for a network node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForNtkNode_New( Ntk_Node_t *node, st_table *CoiTable, st_table *visited) { int i; Ntk_Node_t *faninNode; if(node == NIL(Ntk_Node_t)){ return; } if (st_lookup_int(visited, (char *) node, NIL(int))){ return; } st_insert(visited, (char *) node, (char *) 0); if(Ntk_NodeTestIsInput(node)) return; if (Ntk_NodeTestIsLatch(node)){ st_insert(CoiTable, (char *) node, (char *)0); } Ntk_NodeForEachFanin(node, i, faninNode) { PureSatBmcGetCoiForNtkNode_New(faninNode, CoiTable, visited); } return; } /**Function******************************************************************** Synopsis [Recursively get COI nodes for a LTL formula] Description [Recursively get COI nodes for a LTL formula] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForLtlFormulaRecursive_New( 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, (char *) node, &tmp)){ /* Node already visited */ return; } PureSatBmcGetCoiForNtkNode_New(node, ltlCoiTable, visited); return; } PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->left, ltlCoiTable, visited); PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->right, ltlCoiTable, visited); return; } /**Function******************************************************************** Synopsis [Get COI nodes for a LTL formula] Description [Get COI nodes for a LTL formula] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatBmcGetCoiForLtlFormula_New( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) { st_table *visited = st_init_table(st_ptrcmp, st_ptrhash); PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula, ltlCoiTable, visited); st_free_table(visited); return; } /* BmcGetCoiForLtlFormula() */ /**Function******************************************************************** Synopsis [Mark transitive fanin for an aig node] Description [Mark transitive fanin for an aig node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForNode( satManager_t *cm, bAigEdge_t v, unsigned int mask) { if(v == bAig_NULL) return; v = SATnormalNode(v); if(SATflags(v) & mask) return; SATflags(v) |= mask; if(SATflags(v) & Visited3Mask) return; PureSat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask); PureSat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask); } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForArray( satManager_t *cm, satArray_t *arr, unsigned int mask) { int i, size; bAigEdge_t v; if(arr == 0) return; size = arr->num; for(i=0; ispace[i]; PureSat_MarkTransitiveFaninForNode(cm, v, mask); } } /**Function******************************************************************** Synopsis [Mark transitive fanin for an aig node] Description [Mark transitive fanin for an aig node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForNode2( mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask) { if(v == bAig_NULL) return; v = SATnormalNode(v); if(flags(v) & mask) return; flags(v) |= mask; if(flags(v) & Visited3Mask) return; PureSat_MarkTransitiveFaninForNode2(manager, leftChild(v), mask); PureSat_MarkTransitiveFaninForNode2(manager, rightChild(v), mask); } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForArray2( mAig_Manager_t *manager, satArray_t *arr, unsigned int mask) { bAigEdge_t v; int i, size; if(arr == 0) return; size = arr->num; for(i=0; ispace[i]; PureSat_MarkTransitiveFaninForNode2(manager, v, mask); } } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForNode3( mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask) { if(v == 2) return; v = SATnormalNode(v); if(flags(v) & mask) return; flags(v) |= mask; PureSat_MarkTransitiveFaninForNode3(manager, leftChild(v), mask); PureSat_MarkTransitiveFaninForNode3(manager, rightChild(v), mask); } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForArray3( mAig_Manager_t *manager, satArray_t *arr, unsigned int mask) { bAigEdge_t v; int i, size; if(arr == 0) return; size = arr->num; for(i=0; ispace[i]; PureSat_MarkTransitiveFaninForNode3(manager, v, mask); } } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForNode4( mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask, int bound) { if(v == bAig_NULL) return; v = SATnormalNode(v); if(flags(v) & mask) return; flags(v) |= mask; if((flags(v)&StateBitMask)&& !(flags(v)&VisibleVarMask)&& (bAig_Class(v)>0)){ return; } PureSat_MarkTransitiveFaninForNode4(manager, leftChild(v), mask,bound); PureSat_MarkTransitiveFaninForNode4(manager, rightChild(v), mask,bound); } /**Function******************************************************************** Synopsis [Mark transitive fanin for an array of aig nodes] Description [Mark transitive fanin for an array of aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkTransitiveFaninForArray4( mAig_Manager_t *manager, satArray_t *arr, unsigned int mask, int bound) { bAigEdge_t v; int i, size; if(arr == 0) return; size = arr->num; for(i=0; ispace[i]; v = SATnormalNode(v); PureSat_MarkTransitiveFaninForNode4(manager,v,mask,bound); } } /**Function******************************************************************** Synopsis [clean a certain mask for all the aig nodes] Description [clean a certain mask for all the aig nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_CleanMask(mAig_Manager_t *manager, unsigned int mask) { bAigEdge_t i; for(i=bAigNodeSize; inodesArraySize;i+=bAigNodeSize) flags(i)&=mask; } /**Function******************************************************************** Synopsis [Set COI mask for SAT solver] Description [Set COI mask for SAT solver] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_SetCOI(satManager_t *cm) { PureSat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask); PureSat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask); PureSat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask); } /**Function******************************************************************** Synopsis [Reset COI mask for all nodes] Description [Reset COI mask for all nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_ResetCoi(satManager_t *cm) { bAigEdge_t i; for(i=satNodeSize;inodesArraySize;i+=satNodeSize){ if(SATflags(i) & CoiMask) SATflags(i) &= ResetCoiMask; } } /**Function******************************************************************** Synopsis [Set COI for latch nodes] Description [Set COI for latch nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatSetLatchCOI(Ntk_Network_t * network, PureSat_Manager_t *pm, satManager_t * cm, /*deletable*/ st_table * AbsTable, int from, int to) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t *tf = manager->timeframeWOI; int i,j; bAigEdge_t *L0,*L1,*bL0,*bL1; satArray_t * assert; int nLatches = tf->nLatches, nbLatches = tf->nbLatches; if(from>=to) return; PureSat_ResetCoi(cm); assert = sat_ArrayAlloc(1); sat_ArrayInsert(assert,manager->InitState); PureSat_MarkTransitiveFaninForArray3(manager,assert,CoiMask); sat_ArrayFree(assert); for(i=from; ilatchInputs[i]; L1 = tf->latchInputs[i+1]; bL0 = tf->blatchInputs[i]; bL1 = tf->blatchInputs[i+1]; for(j=0;jassertArray,CoiMask,bound); sat_ArrayFree(assert); } /**Function******************************************************************** Synopsis [Set COI for form the SAT problem] Description [Set COI for form the SAT problem] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatSetCOI(Ntk_Network_t * network, PureSat_Manager_t *pm, satManager_t * cm, st_table * AbsTable, int from, int to, int bound) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); bAigEdge_t property; if(cm->obj->num>0){ property = cm->obj->space[0]; PureSatSetLatchCOI2(network,pm,cm,property,bound); } else{ PureSatSetLatchCOI(network,pm,cm,AbsTable,from,to); PureSat_CleanMask(manager,ResetVisited3Mask); } } /**Function******************************************************************** Synopsis [Build abstraction from concrete model] Description [Build abstraction from concrete model] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatAbstractLatch(bAig_Manager_t *manager, bAigEdge_t v, st_table * tmpTable) { bAigEdge_t nv; /*fanin: set left and right to bAig_NULL*/ nv = bAig_NonInvertedEdge(v); if(leftChild(nv)!=bAig_NULL){ if(!(flags(leftChild(nv))&CoiMask)) flags(leftChild(nv)) |= Visited3Mask; manager->NodesArray[nv+bAigLeft]=bAig_NULL; } if(rightChild(nv)!=bAig_NULL){ if(!(flags(rightChild(nv))&CoiMask)) flags(rightChild(nv)) |= Visited3Mask; manager->NodesArray[nv+bAigRight]=bAig_NULL; } } /**Function******************************************************************** Synopsis [Kill all pseudo global variables for one node for interpolation computation] Description [Kill all pseudo global variables for one node for interpolation computation] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatKillPseudoGVNode(bAig_Manager_t *manager, bAigEdge_t v, st_table * tmpTable) { long size = nFanout(v),i,inv=0; bAigEdge_t v1,v2,nv; bAigEdge_t * fan = (bAigEdge_t *)fanout(v),left; /*fanin: set left and right to bAig_NULL*/ nv = bAig_NonInvertedEdge(v); flags(nv) |= PGVMask; if(leftChild(nv)!=bAig_NULL){ if(!(flags(leftChild(nv))&CoiMask)) flags(leftChild(nv)) |= Visited3Mask; manager->NodesArray[nv+bAigLeft]=bAig_NULL; } if(rightChild(nv)!=bAig_NULL){ if(!(flags(rightChild(nv))&CoiMask)) flags(rightChild(nv)) |= Visited3Mask; manager->NodesArray[nv+bAigRight]=bAig_NULL; } manager->class_ = 2; /*fanout: connection to vars in next tf is disconnected, and a new pseudo var is created, and used as a replacement*/ for(i=0;i>1); if(!(flags(v1)&CoiMask)) continue; if(bAig_Class(v1)>1){ /*igonre invSV since its left and right will be processed to 2*/ if(!(flags(v1)&VisibleVarMask)&&(flags(v1)&StateBitMask)) continue; /*if nonSV, create new Node as replacement*/ if(!st_lookup(tmpTable,(char*)nv,&v2)){ v2 = bAig_CreateNode(manager,bAig_NULL, bAig_NULL); flags(v2) |= DummyMask; st_insert(tmpTable,(char*)nv,(char*)v2); } left = 1; if(bAig_IsInverted(fan[i])) left = 0; inv = bAig_IsInverted(fan[i]>>1)?1:0; v2 = inv ? bAig_Not(v2) : v2; if(left){ #if DBG assert(manager->NodesArray[v1+bAigLeft] != v2); #endif manager->NodesArray[v1+bAigLeft] = v2; PureSat_connectOutput(manager, v2, v1,0); flags(v2) |= CoiMask; } else{ #if DBG assert(manager->NodesArray[v1+bAigRight] != v2); #endif manager->NodesArray[v1+bAigRight] = v2; PureSat_connectOutput(manager, v2, v1,1); flags(v2) |= CoiMask; } } } } /**Function******************************************************************** Synopsis [Kill all pseudo global variables for interpolation computation] Description [Kill all pseudo global variables for interpolation computation] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatKillPseudoGV(Ntk_Network_t * network, PureSat_Manager_t *pm, st_table * AbsTable, int from, int to) { bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t *tf = manager->timeframeWOI; array_t *bVarList,*mVarList; bAigEdge_t * li, *bli,node; int i,j; st_table * tmpTable, *DoneTable; pm->oldPos = manager->nodesArraySize-bAigNodeSize; bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); if(from < 1) from = 1; if(to>pm->Length) to=pm->Length; li = tf->latchInputs[1]; bli = tf->blatchInputs[1]; for(j=0;jnLatches;j++) flags(li[j])&=ResetPGVMask; for(j=0;jnbLatches;j++) flags(bli[j])&=ResetPGVMask; for(i=from;i<=to;i++){ li = tf->latchInputs[i]; bli = tf->blatchInputs[i]; manager->class_ = i; tmpTable = st_init_table(st_numcmp,st_numhash); DoneTable = st_init_table(st_numcmp,st_numhash); for(j=0; jnLatches; j++){ node = bAig_NonInvertedEdge(li[j]); if(st_lookup(DoneTable,(char*)node,NIL(char*))) continue; st_insert(DoneTable,(char*)node,(char*)0); if((flags(node)&StateBitMask)&& !(flags(node)&VisibleVarMask)&& (flags(node)&CoiMask)){ if(i==1) PureSatKillPseudoGVNode(manager,node,tmpTable); else PureSatAbstractLatch(manager,node,tmpTable); } } for(j=0; jnbLatches; j++){ node = bAig_NonInvertedEdge(bli[j]); if(st_lookup(DoneTable,(char*)node,NIL(char*))) continue; st_insert(DoneTable,(char*)node,(char*)0); if((flags(node)&StateBitMask)&& !(flags(node)&VisibleVarMask)&& (flags(node)&CoiMask)){ if(i==1) PureSatKillPseudoGVNode(manager,node,tmpTable); else PureSatAbstractLatch(manager,node,tmpTable); } } st_free_table(tmpTable); st_free_table(DoneTable); } } /**Function******************************************************************** Synopsis [Count number of nodes in COI] Description [Count number of nodes in COI] SideEffects [] SeeAlso [] ******************************************************************************/ int PureSat_CountNodesInCoi(satManager_t* cm) { int ct=0; bAigEdge_t i; for(i=satNodeSize;inodesArraySize;i+=satNodeSize){ if(SATflags(i) & CoiMask){ ct++; } } /*fprintf(vis_stdout,"There are %d node in COI\n",ct);*/ return ct; } /**Function******************************************************************** Synopsis [Sanity check for one node for abstraction processsing] Description [Sanity check for one node for abstraction processsing] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_Check(bAig_Manager_t *manager, bAigEdge_t v) { bAigEdge_t *fan,*fan1,nfan1; bAigEdge_t nfan,cur,child,tmpchild,v1,other,cur1; int size,i,j,find=0,inver,left,left1; nfan = nFanout(v); fan = (bAigEdge_t *)fanout(v); if(fan == 0){ assert(nfan==0); return; } size = 0; for(i=0; fan[i]!=0; i++){ size++; cur = fan[i]; left = 1; inver = 0; if(SATisInverted(cur)) left = 0; cur >>= 1; if(SATisInverted(cur)) inver = 1; cur = SATnormalNode(cur); child = inver? SATnormalNode(v)+1:SATnormalNode(v); if(left) tmpchild = leftChild(cur); else tmpchild = rightChild(cur); assert(tmpchild == child); /*check the other child*/ find = 0; other = left?rightChild(cur):leftChild(cur); assert(other!=bAig_NULL); v1 = SATnormalNode(other); nfan1 = nFanout(v1); fan1 = (bAigEdge_t *)fanout(v1); assert(nfan1!=0&&fan1!=0); for(j=0; fan1[j]!=0; j++){ cur1 = fan1[j]; left1 = 1; if(SATisInverted(cur1)) left1 = 0; assert(j>1)==cur)&&(left1!=left)){ find = 1; break; } } assert(find); } assert(nfan==size); } /**Function******************************************************************** Synopsis [Sanity check for abstraction processsing] Description [Sanity check for abstraction processsing] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_CheckFanoutFanin(bAig_Manager_t *manager) { bAigEdge_t i,v; for(i=bAigNodeSize;inodesArraySize;i+=bAigNodeSize){ v = i; if((flags(v) & IsCNFMask)) continue; PureSat_Check(manager,v); } } /**Function******************************************************************** Synopsis [Reset a sat manager] Description [Reset a sat manager] SideEffects [] SeeAlso [] ******************************************************************************/ /*1. eliminate concls, 2. free variableArray 3. adjust nodeArray(size and new nodes)*/ void PureSat_ResetManager(mAig_Manager_t *manager, satManager_t *cm, int clean) { int i; satVariable_t var; satLevel_t *d; if(cm->variableArray) { for(i=0; iinitNumVariables; 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; cm->currentDecision = 0; } if(cm->literals){ sat_FreeLiteralsDB(cm->literals); cm->literals=0; sat_AllocLiteralsDB(cm); } if(cm->each){ FREE(cm->each); cm->each = sat_InitStatistics(); } if(cm->queue) sat_FreeQueue(cm->queue); if(cm->BDDQueue) sat_FreeQueue(cm->BDDQueue); if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue); cm->queue = 0; cm->BDDQueue = 0; cm->unusedAigQueue = 0; if(cm->nonobjUnitLitArray) sat_ArrayFree(cm->nonobjUnitLitArray); if(cm->objUnitLitArray) sat_ArrayFree(cm->objUnitLitArray); if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray); if(cm->dormantConflictArray) sat_ArrayFree(cm->dormantConflictArray); if(cm->shrinkArray) sat_ArrayFree(cm->shrinkArray); cm->nonobjUnitLitArray = 0; cm->objUnitLitArray = 0; cm->orderedVariableArray = 0; cm->dormantConflictArray = 0; cm->shrinkArray = 0; /*change initNumVariable after cm->variableArray has been freed, otherwise, initNumVariable may change*/ cm->nodesArray = manager->NodesArray; cm->nodesArraySize = manager->nodesArraySize; cm->initNodesArraySize = manager->nodesArraySize; cm->maxNodesArraySize = manager->maxNodesArraySize; cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1; cm->initNumClauses = 0; cm->initNumLiterals = 0; cm->ipm = manager->ipm; cm->assertArray = manager->assertArray; cm->assertArray2 = manager->assertArray2; cm->InitState = manager->InitState; cm->CoiAssertArray = manager->CoiAssertArray; cm->EqArray = manager->EqArray; cm->currentVarPos = 0; cm->currentTopConflict = 0; cm->currentTopConflictCount = 0; cm->lowestBacktrackLevel = 0; cm->implicatedSoFar = 0; //cm->status = 0; if(clean){ for(i=bAigNodeSize;inodesArraySize;i+=bAigNodeSize) cm->nodesArray[i] = 2; } } /**Function******************************************************************** Synopsis [Restore AIG to get rid of Dummy nodes] Description [Restore AIG to get rid of Dummy nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_RestoreAigForDummyNode(mAig_Manager_t *manager, int oldPosition) { bAigEdge_t i; for(i=manager->nodesArraySize-bAigNodeSize; i>oldPosition;i=i-bAigNodeSize){ #if DBG assert(leftChild(i)==bAig_NULL&& rightChild(i)==bAig_NULL); assert(flags(i)&DummyMask); #endif FREE(fanout(i)); } manager->nodesArraySize = oldPosition+bAigNodeSize; return; } /**Function******************************************************************** Synopsis [Process fanout nodes to generate abstraction] Description [Process fanout nodes to generate abstraction] SideEffects [] SeeAlso [] ******************************************************************************/ /*after this funct, all nodes' fanout, either COI or not are in COI, not InvSV, and if this node is InvSV, not to a node in the next tf*/ void PureSatProcessFanout(satManager_t * cm) { long bufSize, bufIndex; bAigEdge_t *buf,left,right,*fan,v,cur; int i, j; long size, tsize; int InvStateVar,l; bufSize = 1024; bufIndex = 0; buf = malloc(sizeof(bAigEdge_t) * bufSize); for(i=satNodeSize; inodesArraySize; i+=satNodeSize) { v = i; if(!(SATflags(v) & CoiMask)) continue; InvStateVar = 0; if((SATflags(v)&StateBitMask)&& !(SATflags(v)&VisibleVarMask)) InvStateVar = 1; size = SATnFanout(v); if(size >= bufSize) { bufSize <<= 1; if(size >= bufSize) bufSize = size + 1; buf = realloc(buf, sizeof(bAigEdge_t) * bufSize); } bufIndex = 0; for(j=0, fan = SATfanout(v); j>= 1; cur = SATnormalNode(cur); /*Not in COI , pass */ if(!(SATflags(cur) & CoiMask)) continue; /*cur is invisible var*/ left = SATleftChild(cur); right = SATrightChild(cur); if(left==bAig_NULL||right==bAig_NULL){ #if DBG assert(left==bAig_NULL&&right==bAig_NULL); assert((SATflags(cur)&StateBitMask)&& !(SATflags(cur)&VisibleVarMask)); #endif continue; } /*v itself is InvStateVar and cur is not InvSV*/ if(SATflags(v)&PGVMask){ if(SATclass(cur)>=2){ l = SATisInverted(fan[j]) ? 0 : 1; if(l){ #if DBG bAigEdge_t v1 = SATnormalNode(SATleftChild(cur)); assert(v1!=v); assert(SATflags(v1)&DummyMask); #endif } else{ #if DBG bAigEdge_t v1 = SATnormalNode(SATrightChild(cur)); assert(v1!=v); assert(SATflags(v1)&DummyMask); #endif } continue; } } buf[bufIndex++] = fan[j]; } if(bufIndex > 0) { tsize = bufIndex; for(j=0, fan=SATfanout(v); j>= 1; cur = SATnormalNode(cur); if(!(SATflags(cur) & CoiMask)) { buf[bufIndex++] = fan[j]; continue; } left = SATleftChild(cur); right = SATrightChild(cur); if(left==bAig_NULL||right==bAig_NULL){ buf[bufIndex++] = fan[j]; continue; } if(SATflags(v)&PGVMask){ if(SATclass(cur)>=2){ buf[bufIndex++] = fan[j]; continue; } } }/*for(j=0, fan=SATfanout(v); jnodesArraySize; i+=satNodeSize) { v = i; if(!(SATflags(v) & CoiMask)) continue; fan = SATfanout(v); size = SATnFanout(v); qsort(fan, size, sizeof(bAigEdge_t), NodeIndexCompare); } } /**Function******************************************************************** Synopsis [Recover from abstractions] Description [Recover from abstractions] SideEffects [] SeeAlso [] ******************************************************************************/ long PureSatRecoverFanoutNode(satManager_t * cm, bAigEdge_t v) { bAigEdge_t *fan,nfan,child,cur; long i; int left,inver; int InvStateVar = 0; if(!(SATflags(v)&VisibleVarMask)&&(SATflags(v)&StateBitMask)) InvStateVar = 1; nfan = SATnFanout(v); fan = SATfanout(v); if(fan == 0) return(0); /*recover left and right children for latch nodes*/ for(i=nfan; fan[i]!=0; i++){ cur = fan[i]; if(!(SATflags(SATnormalNode(cur>>1))&CoiMask)) continue; /*cur is InvSV*/ if((SATleftChild(SATnormalNode(cur>>1))==bAig_NULL)|| (SATrightChild(SATnormalNode(cur>>1))==bAig_NULL)){ #if DBG assert((SATflags(SATnormalNode(cur>>1))&StateBitMask)&& !(SATflags(SATnormalNode(cur>>1))&VisibleVarMask)); #endif left = 1; inver = 0; if(SATisInverted(cur)) left = 0; cur >>= 1; if(SATisInverted(cur)) inver = 1; cur = SATnormalNode(cur); child = inver? SATnormalNode(v)+1:SATnormalNode(v); if(left) SATleftChild(cur)=child; else SATrightChild(cur)=child; continue; } /*v is InvSV, cur is not InvSV*/ if(SATflags(v)&PGVMask){ if(SATclass(SATnormalNode(cur>>1))>=2){ left = 1; inver = 0; if(SATisInverted(cur)) left = 0; cur >>= 1; if(SATisInverted(cur)) inver = 1; cur = SATnormalNode(cur); child = inver? SATnormalNode(v)+1:SATnormalNode(v); if(left) SATleftChild(cur)=child; else SATrightChild(cur)=child; } } } //recover all fanout return(i); } /**Function******************************************************************** Synopsis [Recover invisible state variable node] Description [Recover invisible state variable node] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatRecoverISVNode(satManager_t *cm, bAigEdge_t v) { bAigEdge_t size = SATnFanout(v),cur,node,child; bAigEdge_t * fan = SATfanout(v); int inv,i,left; for(i=0;i>1; node = SATnormalNode(cur); /*not in coi*/ if(!(SATflags(node)&CoiMask)) continue; /*not invisible var*/ if(!((SATflags(node)&StateBitMask)&& !(SATflags(node)&VisibleVarMask))) continue; left=SATisInverted(fan[i])?0:1; inv=SATisInverted(cur)?1:0; child = inv?SATnormalNode(v)+1:SATnormalNode(v); if(left) SATleftChild(node) = child; else SATrightChild(node) = child; } } /**Function******************************************************************** Synopsis [Recover fanout of nodes] Description [Recover fanout of nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatRecoverFanout(satManager_t * cm, PureSat_Manager_t *pm) { bAigEdge_t i, v; /*dummy node can't be recovered*/ for(i=satNodeSize; i<=pm->oldPos; i+=satNodeSize) { v = i; if(SATflags(v) & IsCNFMask) continue; if((SATflags(v)&CoiMask)){ SATnFanout(v) = PureSatRecoverFanoutNode(cm, v); continue; } /*for some node not in coi, but a child of one coi(ISV) node*/ if(SATflags(v)&Visited3Mask){ PureSatRecoverISVNode(cm,v); continue; } } } /**Function******************************************************************** Synopsis [sanity check for one node for abstraction processing] Description [sanity check for one node for abstraction processing] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCheckCoiNode(bAig_Manager_t * manager, bAigEdge_t node) { int i; long *fan; long nfan,child, cur; int left,inv; nfan = nFanout(node); fan = (bAigEdge_t*)fanout(node); if(fan==0) return; /*check child*/ assert((leftChild(node)==bAig_NULL)|| (flags(leftChild(node))&CoiMask)); assert((rightChild(node)==bAig_NULL)|| (flags(rightChild(node))&CoiMask)); if((leftChild(node)==bAig_NULL)||(rightChild(node)==bAig_NULL)) assert((leftChild(node)==bAig_NULL)&&(rightChild(node)==bAig_NULL)); /*check fanout*/ for(i=0; i>1; assert(flags(cur)&CoiMask); left=SATisInverted(fan[i])?0:1; inv=SATisInverted(cur)?1:0; child = inv?SATnormalNode(node)+1:SATnormalNode(node); if(left){ assert(child==leftChild(cur)); } else{ assert(child==rightChild(cur)); } } } /**Function******************************************************************** Synopsis [sanity check for abstraction processing] Description [sanity check for abstraction processing] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCheckCoi(bAig_Manager_t *manager) { long i; for(i=bAigNodeSize;inodesArraySize;i+=bAigNodeSize){ if(flags(i) & IsCNFMask) continue; if(!(flags(i) & CoiMask)) continue; PureSatCheckCoiNode(manager,i); } } /**Function******************************************************************** Synopsis [Preprocess to form SAT instances] Description [Preprocess to form SAT instances] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatPreprocess(Ntk_Network_t * network, satManager_t *cm, PureSat_Manager_t *pm, st_table *vertexTable, int Length) { bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); PureSatSetCOI(network,pm,cm,vertexTable,0, Length,Length); /*for interpolation*/ PureSatKillPseudoGV(network,pm,vertexTable,1,Length); PureSat_ResetManager(manager,cm,0); /*for abstraction*/ PureSatProcessFanout(cm); } /**Function******************************************************************** Synopsis [Recovery step after SAT solving] Description [Recovery step after SAT solving] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatPostprocess(bAig_Manager_t *manager, satManager_t *cm, PureSat_Manager_t *pm) { PureSatRecoverFanout(cm,pm); PureSat_RestoreAigForDummyNode(manager,pm->oldPos); PureSat_CleanMask(manager,ResetVisited3Mask); } /**Function******************************************************************** Synopsis [Convergence test for flat interpolation algorithm] Description [Convergence test for flat interpolation algorithm] SideEffects [] SeeAlso [] ******************************************************************************/ /*test if state1 contains state2*/ int PureSat_TestConvergeForIP(mAig_Manager_t *manager, PureSat_Manager_t *pm, satManager_t *cm, bAigEdge_t state1, bAigEdge_t state2) { satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7; int status, nodes_in_coi = 0; if(state2 == bAig_Zero) return 1; if(state1 == bAig_One) return 1; if(state1 == bAig_Zero && state2 != bAig_Zero) return 0; if(state1 != bAig_One && state2 == bAig_One) return 0; if(pm->verbosity>=1) fprintf(vis_stdout,"Test convergence:\n"); PureSat_ResetCoi(cm); if(pm->verbosity>=1){ fprintf(vis_stdout,"after reset COI\n"); nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } tmp1 = cm->obj; tmp2 = cm->auxObj; tmp3 = cm->assertion; tmp4 = cm->assertArray; //Bing: tmp5 = cm->unitLits; tmp6 = cm->pureLits; tmp7 = cm->nonobjUnitLitArray; cm->obj = 0; cm->auxObj = 0; cm->assertion = 0; //cm->assertArray2 = 0; cm->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(cm->assertArray,SATnot(state1)); sat_ArrayInsert(cm->assertArray,state2); sat_SetConeOfInfluence(cm); if(pm->verbosity>=1){ fprintf(vis_stdout,"after add new init states:\n"); nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } cm->option->coreGeneration = 0; //cm->option->effIP = 0; cm->option->IP = 0; cm->status = 0; sat_Main(cm); if(manager->NodesArray!=cm->nodesArray) /*cm->nodesArray may be reallocated*/ manager->NodesArray = cm->nodesArray; cm->obj = tmp1; cm->auxObj = tmp2; cm->assertion = tmp3; sat_ArrayFree(cm->assertArray); cm->assertArray = tmp4; cm->unitLits = tmp5; cm->pureLits = tmp6; cm->nonobjUnitLitArray = tmp7; cm->option->coreGeneration = 1; cm->option->IP = 1; status = cm->status; #if DBG assert(cm->currentDecision>=-1); #endif if(cm->currentDecision!=-1) sat_Backtrack(cm,-1); cm->status = 0; if(status == SAT_UNSAT) /*state2 contains state1, reach convergence*/ return 1; else return 0; } /**Function******************************************************************** Synopsis [Convergence test for interpolation algorithm with abstraction refinement ] Description [Convergence test for flat interpolation algorithmwith abstraction refinement ] SideEffects [] SeeAlso [] ******************************************************************************/ /*test if state1 contains state2 for abstract refinement*/ int PureSat_TestConvergeForIP_AbRf(Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, array_t * CoiArray, bAigEdge_t state1, bAigEdge_t state2) { satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7; int status, nodes_in_coi = 0; mAig_Manager_t * manager; if(state2 == bAig_Zero) return 1; if(state1 == bAig_One) return 1; if(state1 == bAig_Zero && state2 != bAig_Zero) return 0; if(state1 != bAig_One && state2 == bAig_One) return 0; manager = Ntk_NetworkReadMAigManager(network); if(pm->verbosity>=1) fprintf(vis_stdout,"Test convergence:\n"); PureSat_ResetCoi(cm); if(pm->verbosity>=1){ fprintf(vis_stdout,"after reset COI\n"); nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } tmp1 = cm->obj; tmp2 = cm->auxObj; tmp3 = cm->assertion; tmp4 = cm->assertArray; tmp5 = cm->unitLits; tmp6 = cm->pureLits; tmp7 = cm->nonobjUnitLitArray; cm->obj = 0; cm->auxObj = 0; cm->assertion = 0; cm->unitLits = 0; cm->pureLits = 0; cm->nonobjUnitLitArray = 0; cm->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(cm->assertArray,SATnot(state1)); sat_ArrayInsert(cm->assertArray,state2); sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask); if(pm->verbosity>=1){ fprintf(vis_stdout,"after add new init states:\n"); nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } cm->option->coreGeneration = 0; cm->status = 0; cm->option->AbRf = 0; sat_Main(cm); cm->option->AbRf = 1; if(manager->NodesArray!=cm->nodesArray) /*cm->nodesArray may be reallocated*/ manager->NodesArray = cm->nodesArray; sat_ArrayFree(cm->assertArray); manager->assertArray = tmp4; cm->obj = tmp1; cm->auxObj = tmp2; cm->assertion = tmp3; cm->assertArray = tmp4; cm->unitLits = tmp5; cm->pureLits = tmp6; cm->nonobjUnitLitArray = tmp7; cm->option->coreGeneration = 1; status = cm->status; if(cm->currentDecision!=-1) sat_Backtrack(cm,-1); cm->status = 0; if(status == SAT_UNSAT) /*state2 contains state1, reach convergence*/ return 1; else return 0; } /**Function******************************************************************** Synopsis [Allocate a PureSAT Manager] Description [Allocate a PureSAT Manager] SideEffects [] SeeAlso [] ******************************************************************************/ satManager_t * PureSat_SatManagerAlloc(bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray) { satManager_t * cm; satOption_t *option; int i,size; bAigEdge_t tv; cm = ALLOC(satManager_t, 1); memset(cm, 0, sizeof(satManager_t)); cm->nodesArraySize = manager->nodesArraySize; cm->initNodesArraySize = manager->nodesArraySize; cm->maxNodesArraySize = manager->maxNodesArraySize; cm->nodesArray = manager->NodesArray; cm->HashTable = manager->HashTable; cm->literals = manager->literals; cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1; cm->initNumClauses = 0; cm->initNumLiterals = 0; cm->comment = ALLOC(char, 2); cm->comment[0] = ' '; cm->comment[1] = '\0'; cm->stdErr = vis_stderr; cm->stdOut = vis_stdout; cm->status = 0; cm->orderedVariableArray = 0; cm->unitLits = sat_ArrayAlloc(16); cm->pureLits = sat_ArrayAlloc(16); cm->option = 0; cm->each = 0; cm->decisionHead = 0; cm->variableArray = 0; cm->queue = 0; cm->BDDQueue = 0; cm->unusedAigQueue = 0; cm->ipm = manager->ipm; cm->assertArray = manager->assertArray; cm->assertArray2 = manager->assertArray2; cm->InitState = manager->InitState; cm->CoiAssertArray = manager->CoiAssertArray; cm->EqArray = manager->EqArray; if(auxObjectArray) { cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1); size = auxObjectArray->num; for(i=0; istatus = SAT_UNSAT; break; } sat_ArrayInsert(cm->auxObj, tv); } } if(object == 0) cm->status = SAT_UNSAT; else if(object == 1) cm->status = SAT_SAT; if(cm->status == 0) { if(object!=-1){ cm->obj = sat_ArrayAlloc(1); sat_ArrayInsert(cm->obj, object); } /* initialize option*/ option = sat_InitOption(); option->coreGeneration = 1; option->ForceFinish = 1; option->clauseDeletionHeuristic = 0; option->includeLevelZeroLiteral = 1; option->minimizeConflictClause = 0; option->IP = 1; option->RT = 1; option->verbose = pm->verbosity; cm->anteTable = st_init_table(st_numcmp,st_numhash); cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash); cm->option = option; cm->each = sat_InitStatistics(); BmcRestoreAssertion(manager,cm); /* value reset..*/ sat_CleanDatabase(cm); /* set cone of influence*/ sat_SetConeOfInfluence(cm); sat_AllocLiteralsDB(cm); } return cm; } /**Function******************************************************************** Synopsis [Allocate a PureSAT Manager without setting COI] Description [Allocate a PureSAT Manager without setting COI] SideEffects [] SeeAlso [] ******************************************************************************/ satManager_t * PureSat_SatManagerAlloc_WOCOI(mAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray) { satManager_t * cm; satOption_t *option; int i,size; bAigEdge_t tv; cm = ALLOC(satManager_t, 1); memset(cm, 0, sizeof(satManager_t)); cm->nodesArraySize = manager->nodesArraySize; cm->initNodesArraySize = manager->nodesArraySize; cm->maxNodesArraySize = manager->maxNodesArraySize; cm->nodesArray = manager->NodesArray; cm->HashTable = manager->HashTable; cm->literals = manager->literals; cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1; cm->initNumClauses = 0; cm->initNumLiterals = 0; cm->comment = ALLOC(char, 2); cm->comment[0] = ' '; cm->comment[1] = '\0'; cm->stdErr = vis_stderr; cm->stdOut = vis_stdout; cm->status = 0; cm->orderedVariableArray = 0; cm->unitLits = sat_ArrayAlloc(16); cm->pureLits = sat_ArrayAlloc(16); cm->option = 0; cm->each = 0; cm->decisionHead = 0; cm->variableArray = 0; cm->queue = 0; cm->BDDQueue = 0; cm->unusedAigQueue = 0; cm->ipm = manager->ipm; cm->assertArray = manager->assertArray; cm->assertArray2 = manager->assertArray2; cm->InitState = manager->InitState; cm->CoiAssertArray = manager->CoiAssertArray; cm->EqArray = manager->EqArray; if(auxObjectArray) { cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1); size = auxObjectArray->num; for(i=0; istatus = SAT_UNSAT; break; } sat_ArrayInsert(cm->auxObj, tv); } } if(object == 0) cm->status = SAT_UNSAT; else if(object == 1) cm->status = SAT_SAT; if(cm->status == 0) { if(object!=-1){ cm->obj = sat_ArrayAlloc(1); sat_ArrayInsert(cm->obj, object); } option = sat_InitOption(); option->ForceFinish = 1; option->coreGeneration = 1; option->clauseDeletionHeuristic = 0; option->includeLevelZeroLiteral = 1; option->minimizeConflictClause = 0; option->IP = 0; option->RT = 1; option->verbose = pm->verbosity; cm->anteTable = st_init_table(st_numcmp,st_numhash); cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash); cm->option = option; cm->each = sat_InitStatistics(); BmcRestoreAssertion(manager,cm); sat_CleanDatabase(cm); /* WOCOI: NO set cone of influence*/ sat_AllocLiteralsDB(cm); } return cm; } /**Function******************************************************************** Synopsis [Free a PureSAT manager] Description [Free a PureSAT manager] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_SatFreeManager(satManager_t*cm) { satVariable_t var; satLevel_t *d; int i; if(cm->option->coreGeneration){ st_free_table(cm->anteTable); st_free_table(cm->RTreeTable); cm->anteTable=0; cm->RTreeTable=0; } /*timeframe, timeframeWOI,HashTable can't be freed*/ if(cm->option) sat_FreeOption(cm->option); if(cm->total) sat_FreeStatistics(cm->total); if(cm->each) sat_FreeStatistics(cm->each); if(cm->literals) sat_FreeLiteralsDB(cm->literals); cm->option=0; cm->total=0; cm->each=0; cm->literals=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; } if(cm->queue) sat_FreeQueue(cm->queue); if(cm->BDDQueue) sat_FreeQueue(cm->BDDQueue); if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue); cm->queue = 0; cm->BDDQueue = 0; cm->unusedAigQueue = 0; if(cm->auxObj) sat_ArrayFree(cm->auxObj); if(cm->obj) sat_ArrayFree(cm->obj); if(cm->unitLits) sat_ArrayFree(cm->unitLits); if(cm->pureLits) sat_ArrayFree(cm->pureLits); if(cm->assertion) sat_ArrayFree(cm->assertion); if(cm->auxArray) sat_ArrayFree(cm->auxArray); if(cm->nonobjUnitLitArray) sat_ArrayFree(cm->nonobjUnitLitArray); if(cm->objUnitLitArray) sat_ArrayFree(cm->objUnitLitArray); if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray); if(cm->savedConflictClauses) sat_ArrayFree(cm->savedConflictClauses); cm->auxObj = 0; cm->obj = 0; cm->unitLits = 0; cm->pureLits = 0; cm->assertion = 0; cm->auxArray = 0; cm->nonobjUnitLitArray = 0; cm->objUnitLitArray = 0; cm->orderedVariableArray = 0; if(cm->variableArray) { for(i=0; iinitNumVariables; 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->comment) free(cm->comment); cm->comment=0; FREE(cm); } /**Function******************************************************************** Synopsis [Print the status of AIG] Description [Print the status of AIG] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_PrintAigStatus(mAig_Manager_t *manager) { (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n", manager->maxNodesArraySize/bAigNodeSize); (void) fprintf(vis_stdout,"Current number of nodes: %ld\n", manager->nodesArraySize/bAigNodeSize); fprintf(vis_stdout,"Current Max Node Index: %ld\n\n", manager->nodesArraySize); } /**Function******************************************************************** Synopsis [Mark global variables] Description [Mark global variables] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkGlobalVar(bAig_Manager_t *manager, int length) { bAigTimeFrame_t * tf = manager->timeframeWOI; bAigEdge_t * li,* bli,node; int i; li = tf->latchInputs[length]; bli = tf->blatchInputs[length]; for(i=0; inLatches; i++){ node = bAig_NonInvertedEdge(li[i]); manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask; } for(i=0; inbLatches; i++){ node = bAig_NonInvertedEdge(bli[i]); manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask; } } /**Function******************************************************************** Synopsis [UnMark global variables] Description [UnMark global variables] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_UnMarkGlobalVar(bAig_Manager_t *manager, int length) { bAigTimeFrame_t * tf = manager->timeframeWOI; bAigEdge_t * li,* bli,node; int i; li = tf->latchInputs[length]; bli = tf->blatchInputs[length]; for(i=0; inLatches; i++){ node = bAig_NonInvertedEdge(li[i]); manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask; } for(i=0; inbLatches; i++){ node = bAig_NonInvertedEdge(bli[i]); manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask; } } /**Function******************************************************************** Synopsis [Makr global variable for abstraction refinement] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_MarkGlobalVar_AbRf(bAig_Manager_t *manager, int length) { bAigTimeFrame_t * tf = manager->timeframeWOI; bAigEdge_t * li,* bli,node; int i; li = tf->latchInputs[length]; bli = tf->blatchInputs[length]; for(i=0; inLatches; i++){ node = bAig_NonInvertedEdge(li[i]); if(flags(node)&VisibleVarMask) manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask; } for(i=0; inbLatches; i++){ node = bAig_NonInvertedEdge(bli[i]); if(flags(node)&VisibleVarMask) manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask; } } /**Function******************************************************************** Synopsis [Mark visible variable and also mark visible pseudo global variable] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PuresatMarkVisibleVarWithVPGV(Ntk_Network_t *network, array_t * visibleArray, PureSat_Manager_t *pm, int from, int to) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); MvfAig_Function_t *mvfAig; bAigTimeFrame_t * tf = manager->timeframeWOI; mAigMvar_t lmVar; mAigBvar_t bVar; array_t *bVarList,*mVarList; int i,j,k,lmAigId,index,index1; char * name; Ntk_Node_t * latch; bAigEdge_t node,v, *li, *bli; bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); /*Although some SV in tf 0 are not marked as visiblevar, //they actually visible since all SV of tf 0 are visible*/ if(from<0) from=0; if(to>pm->Length+1) to=pm->Length+1; /*clean VPGV mask*/ li = tf->latchInputs[1]; bli = tf->blatchInputs[1]; for(j=0;jnLatches;j++) flags(li[j])&=ResetVPGVMask; for(j=0;jnbLatches;j++) flags(bli[j])&=ResetVPGVMask; for(i=from;i<=to;i++){ li = tf->latchInputs[i]; bli = tf->blatchInputs[i]; arrayForEachItem(char *,visibleArray,k,name){ int retVal; latch = Ntk_NetworkFindNodeByName(network,name); st_lookup(node2MvfAigTable,latch,&mvfAig); for(j=0;jnum;j++){ v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j)); if(v==bAig_Zero||v==bAig_One) continue; retVal = st_lookup(tf->li2index,(char*)v,&index); assert(retVal); if(li[index]==bAig_Zero||li[index]==bAig_One) continue; node = bAig_NonInvertedEdge(li[index]); manager->NodesArray[node+bAigFlags] |= VisibleVarMask; /*marking PGV*/ if(i==1){ if(!st_lookup(pm->vertexTable,name,NIL(char*))){ flags(node) |= VPGVMask; } } } lmAigId = Ntk_NodeReadMAigId(latch); lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId); for(j=0,index1=lmVar.bVars;jbli2index,(char*)bVar.node,&index); assert(retVal); if(bli[index]==bAig_Zero||bli[index]==bAig_One) continue; node = bAig_NonInvertedEdge(bli[index]); manager->NodesArray[node+bAigFlags] |= VisibleVarMask; /*marking PGV*/ if(i==1){ if(!st_lookup(pm->vertexTable,name,NIL(char*))) flags(node) |= VPGVMask; } } } } return; } /**Function******************************************************************** Synopsis [Mark visible latch variables] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PuresatMarkVisibleVar(Ntk_Network_t *network, array_t * visibleArray, PureSat_Manager_t *pm, int from, int to) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); MvfAig_Function_t *mvfAig; bAigTimeFrame_t * tf = manager->timeframeWOI; mAigMvar_t lmVar; mAigBvar_t bVar; array_t *bVarList,*mVarList; int i,j,k,lmAigId,index,index1; char * name; Ntk_Node_t * latch; bAigEdge_t node,v, *li, *bli; bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); if(from<0) from=0; if(to>pm->Length+1) to=pm->Length+1; for(i=from;i<=to;i++){ li = tf->latchInputs[i]; bli = tf->blatchInputs[i]; arrayForEachItem(char *,visibleArray,k,name){ latch = Ntk_NetworkFindNodeByName(network,name); st_lookup(node2MvfAigTable,latch,&mvfAig); /*multi val var*/ for(j=0;jnum;j++){ int retVal; v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j)); if(v==bAig_Zero||v==bAig_One) continue; retVal = st_lookup(tf->li2index,(char*)v,&index); assert(retVal); if(li[index]==bAig_Zero||li[index]==bAig_One) continue; node = bAig_NonInvertedEdge(li[index]); manager->NodesArray[node+bAigFlags] |= VisibleVarMask; } /*binary var*/ lmAigId = Ntk_NodeReadMAigId(latch); lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId); for(j=0,index1=lmVar.bVars;jbli2index,(char*)bVar.node,&index); assert(retVal); if(bli[index]==bAig_Zero||bli[index]==bAig_One) continue; node = bAig_NonInvertedEdge(bli[index]); manager->NodesArray[node+bAigFlags] |= VisibleVarMask; } }// arrayForEachItem(char *,visibleArray,k,name) } return; } /**Function******************************************************************** Synopsis [Recursively mapping interpolant from a timeframe to another timeframe] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t PureSat_MapIPRecur(mAig_Manager_t *manager, bAigEdge_t node, st_table * tmpTable) { bAigEdge_t v,result,left,right; int isInverted; #if DBG assert(node!=bAig_NULL); #endif if(node == bAig_One || node == bAig_Zero){ return node; } if(st_lookup(tmpTable,(char *)bAig_NonInvertedEdge(node),&v)){ if(bAig_IsInverted(node)) result = bAig_Not(v); else result = v; return result; } left = PureSat_MapIPRecur(manager,leftChild(node),tmpTable); right = PureSat_MapIPRecur(manager,rightChild(node),tmpTable); v = PureSat_And(manager,left,right); isInverted = bAig_IsInverted(node); result = isInverted ? bAig_Not(v) : v; st_insert(tmpTable,(char *)bAig_NonInvertedEdge(node),(char *)v); //fprintf(vis_stdout,"return %d->%d\n",node,result); return result; } /**Function******************************************************************** Synopsis [Maping interpolant from a timeframe to another timeframe] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t PureSat_MapIP(mAig_Manager_t *manager, bAigEdge_t node, int from, int to) { bAigTimeFrame_t *tf = manager->timeframeWOI; st_table *tmpTable = st_init_table(st_numcmp,st_numhash); bAigEdge_t * L1,*L0,result,v1,v0; int i; if(node==bAig_One||node==bAig_Zero) return node; L1 = tf->latchInputs[from]; L0 = tf->latchInputs[to]; for(i=0;inLatches;i++){ v1 = L1[i]; v0 = L0[i]; if(SATisInverted(v1)){ v1 = SATnot(v1); v0 = SATnot(v0); } st_insert(tmpTable,(char*)v1,(char*)v0); } L1 = tf->blatchInputs[from]; L0 = tf->blatchInputs[to]; for(i=0;inbLatches;i++){ v1 = L1[i]; v0 = L0[i]; if(SATisInverted(v1)){ v1 = SATnot(v1); v0 = SATnot(v0); } st_insert(tmpTable,(char*)v1,(char*)v0); } manager->class_ = to; result = PureSat_MapIPRecur(manager,node,tmpTable); st_free_table(tmpTable); return result; } /**Function******************************************************************** Synopsis [process dummy nodes] Description [In UNSAT core, there may be dummy nodes, but in manager, they don't exist any more. This funct is to mark them] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatProcessDummy(bAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode) { int i; bAigEdge_t *lp,node; RTManager_t *rm = cm->rm; if(RT_flag(RTnode)&RT_VisitedMask){ return; } RT_flag(RTnode) |= RT_VisitedMask; if(RT_pivot(RTnode)==0){ /*leaf*/ #if DBG assert(RT_oriClsIdx(RTnode)==0); #endif if(RT_oriClsIdx(RTnode)) lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode)); else lp = RT_formula(RTnode) + cm->rm->fArray; for(i=0;i0);/* not processed yet*/ if(RT_oriClsIdx(RTnode))/*is CNF*/ node = SATgetNode(*lp); else /*is AIG*/ node = *lp; node = SATnormalNode(node); if(node>=manager->nodesArraySize){ #if DBG assert(flags(node)&DummyMask); #endif *lp = DUMMY; } } } /*leaf*/ /*not leaf*/ else{ if(RT_pivot(RTnode)>=manager->nodesArraySize){ int class_ = bAig_Class(RT_pivot(RTnode)); RT_pivot(RTnode) = DUMMY+class_; } PureSatProcessDummy(manager,cm,RT_left(RTnode)); PureSatProcessDummy(manager,cm,RT_right(RTnode)); } return ; } /**Function******************************************************************** Synopsis [Find an aig node from its name] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t PureSat_FindNodeByName( bAig_Manager_t *manager, nameType_t *name, int bound) { bAigEdge_t node; if (!st_lookup(manager->SymbolTableArray[bound], name, &node)){ node = bAig_NULL; } return bAig_GetCanonical(manager, node); } /**Function******************************************************************** Synopsis [Create Aig for a ltl formula] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t PureSatCreatebAigOfPropFormula( Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState) { int index; bAigEdge_t result, left, right, *li; bAigTimeFrame_t *timeframe; if (ltl == NIL(Ctlsp_Formula_t)) return bAig_NULL; if (ltl->type == Ctlsp_TRUE_c) return bAig_One; if (ltl->type == Ctlsp_FALSE_c) return bAig_Zero; assert(Ctlsp_isPropositionalFormula(ltl)); if(withInitialState) timeframe = manager->timeframe; else timeframe = manager->timeframeWOI; if (ltl->type == Ctlsp_ID_c){ char *nodeNameString = Ctlsp_FormulaReadVariableName(ltl); char *nodeValueString = Ctlsp_FormulaReadValueName(ltl); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString); Var_Variable_t *nodeVar; int nodeValue; MvfAig_Function_t *tmpMvfAig; st_table *nodeToMvfAigTable; /* maps each node to its mvfAig */ if (node == NIL(Ntk_Node_t)) { char *nameKey; char tmpName[100]; sprintf(tmpName, "%s_%d", nodeNameString, bound); nameKey = util_strsav(tmpName); result = PureSat_FindNodeByName(manager, nameKey,bound); if(result == bAig_NULL){ result = PureSat_CreateVarNode(manager, nameKey); } else { FREE(nameKey); } return result; } nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); assert(nodeToMvfAigTable != NIL(st_table)); tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); if (tmpMvfAig == NIL(MvfAig_Function_t)){ tmpMvfAig = Bmc_NodeBuildMVF(network, node); array_free(tmpMvfAig); tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); } nodeVar = Ntk_NodeReadVariable(node); if (Var_VariableTestIsSymbolic(nodeVar)) { nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString); if ( nodeValue == -1 ) { (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n"); (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString); return bAig_NULL; } } else { int check; check = StringCheckIsInteger(nodeValueString, &nodeValue); if( check == 0 ) { (void) fprintf(vis_stderr,"Illegal value in the RHS\n"); (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString); return bAig_NULL; } if( check == 1 ) { (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n"); (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString); return bAig_NULL; } if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) { (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n"); (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString); return bAig_NULL; } } result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue); result = bAig_GetCanonical(manager, result); if(st_lookup(timeframe->li2index, (char *)result, &index)) { li = timeframe->latchInputs[bound]; result = bAig_GetCanonical(manager, li[index]); } else if(st_lookup(timeframe->o2index, (char *)result, &index)) { li = timeframe->outputs[bound]; result = bAig_GetCanonical(manager, li[index]); } else if(st_lookup(timeframe->i2index, (char *)result, &index)) { li = timeframe->internals[bound]; result = bAig_GetCanonical(manager, li[index]); } return result; } left = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState); if (left == bAig_NULL){ return bAig_NULL; } right = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState); if (right == bAig_NULL && ltl->type ==Ctlsp_NOT_c ){ return bAig_Not(left); } else if(right == bAig_NULL) { return bAig_NULL; } switch(ltl->type) { case Ctlsp_OR_c: result = PureSat_Or(manager, left, right); break; case Ctlsp_AND_c: result = PureSat_And(manager, left, right); break; case Ctlsp_THEN_c: result = PureSat_Then(manager, left, right); break; case Ctlsp_EQ_c: result = PureSat_Eq(manager, left, right); break; case Ctlsp_XOR_c: result = PureSat_Xor(manager, left, right); break; default: fail("Unexpected type"); } return result; } /* BmcCirCUsCreatebAigOfPropFormula */ /**Function******************************************************************** Synopsis [Mark all node between from and to with obj mask] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatMarkObj(bAig_Manager_t * manager, long from, long to) { long v; for(v=from;v<=to;v+=bAigNodeSize) flags(v)|=ObjMask; } /**Function******************************************************************** Synopsis [procedure of concretization] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ boolean PureSat_ConcretTest(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, int Con, int satStat, int inc) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); int status,i,nodes_in_coi=0; satManager_t *cm; char *name; double t1,t2; satArray_t *saved; st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash); bAigEdge_t from,*lp; arrayForEachItem(char *,sufArray,i,name){ st_insert(SufAbsNameTable,name,(char*)0); } manager->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(manager->assertArray,manager->InitState); cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray); cm->option->coreGeneration = 0; cm->option->RT = 0; cm->option->AbRf = 1; if(inc){ cm->option->incTraceObjective = 1; cm->savedConflictClauses = pm->savedConCls; pm->savedConCls = 0; } t1 = util_cpu_ctime(); PureSat_CleanMask(manager,ResetVisibleVarMask); PuresatMarkVisibleVar(network,sufArray,pm,0,pm->Length+1); if(!Con){ from = manager->nodesArraySize; PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length); PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length); if(inc){ PureSatMarkObj(manager,from,manager->nodesArraySize-bAigNodeSize); } PureSat_ResetManager(manager,cm,0); PureSatProcessFanout(cm); } else{ sat_MarkTransitiveFaninForNode(cm,property,CoiMask); sat_MarkTransitiveFaninForNode(cm,manager->InitState,CoiMask); cm->option->AbRf = 0; } t2 = util_cpu_ctime(); pm->tPro += t2-t1; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t2-t1)/1000.0),pm->tPro/1000); if(pm->verbosity>=1){ nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } st_free_table(SufAbsNameTable); manager->assertArray2 = cm->assertArray2; sat_Main(cm); if(satStat) sat_ReportStatistics(cm,cm->each); cm->option->AbRf = 1; manager->NodesArray = cm->nodesArray; t1 = util_cpu_ctime(); if(!Con){ PureSatRecoverFanout(cm,pm); PureSat_RestoreAigForDummyNode(manager,pm->oldPos); PureSat_CleanMask(manager,ResetVisited3Mask); } /*record conflict*/ if(inc && cm->savedConflictClauses ){ if(!Con){ int num=0; saved = cm->savedConflictClauses; pm->savedConCls = sat_ArrayAlloc(1); for(i=0, lp=saved->space; inum; i++, lp++){ sat_ArrayInsert(pm->savedConCls,*lp); if(*lp<0) num++; } assert(num%2==0); if(pm->verbosity>=2) fprintf(vis_stdout,"record %d ConCls for incremental concretization\n",num/2); } else pm->savedConCls = 0; sat_ArrayFree(cm->savedConflictClauses); cm->savedConflictClauses = 0; } t2 = util_cpu_ctime(); pm->tPro += t2-t1; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t2-t1)/1000.0),pm->tPro/1000); sat_ArrayFree(manager->assertArray); status = cm->status; cm->option->coreGeneration = 1; PureSat_SatFreeManager(cm); if(status == SAT_SAT){ if(pm->verbosity>=1) fprintf(vis_stdout,"CEX exist\n"); return FALSE; /* cex exists*/ } else{ if(pm->verbosity>=1) fprintf(vis_stdout,"no CEX\n"); return TRUE; /* no cex*/ } } /**Function******************************************************************** Synopsis [Concretization procedure for unsat proof-based refinement minimization] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ boolean PureSat_ConcretTest_Core(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, st_table * junkTable) { mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); int status,i,nodes_in_coi=0; satManager_t *cm; char *name; double t1,t2; st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash); array_t * tmpRef1; st_table *refTable = st_init_table(strcmp,st_strhash); arrayForEachItem(char *,sufArray,i,name){ st_insert(SufAbsNameTable,name,(char*)0); } manager->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(manager->assertArray,manager->InitState); cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray); cm->option->coreGeneration = 1; cm->option->AbRf = 1; cm->option->IP = 1; t1 = util_cpu_ctime(); PureSat_CleanMask(manager,ResetVisibleVarMask); PuresatMarkVisibleVarWithVPGV(network,sufArray,pm,0,pm->Length+1); PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length); PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length); PureSat_ResetManager(manager,cm,0); PureSatProcessFanout(cm); t2 = util_cpu_ctime(); pm->tPro += t2-t1; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t2-t1)/1000.0),pm->tPro/1000); if(pm->verbosity>=1){ nodes_in_coi = PureSat_CountNodesInCoi(cm); fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi); } manager->assertArray2 = cm->assertArray2; sat_Main(cm); manager->NodesArray = cm->nodesArray; t1 = util_cpu_ctime(); PureSatRecoverFanout(cm,pm); PureSat_RestoreAigForDummyNode(manager,pm->oldPos); PureSat_CleanMask(manager,ResetVisited3Mask); if(cm->status==SAT_UNSAT){ PureSatProcessDummy(manager,cm,cm->rm->root); ResetRTree(cm->rm); } t2 = util_cpu_ctime(); pm->tPro += t2-t1; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t2-t1)/1000.0),pm->tPro/1000); if(cm->status==SAT_UNSAT){ tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable); arrayForEachItem(char*,tmpRef1,i,name) st_insert(refTable,name,(char*)0); arrayForEachItem(char*,sufArray,i,name){ if(!st_lookup(refTable,name,NIL(char*))&& !st_lookup(pm->vertexTable,name,NIL(char*))){ if(pm->verbosity>=2) fprintf(vis_stdout,"%s can be gotten rid of\n",name); st_insert(junkTable,name,(char*)0); } } array_free(tmpRef1); } st_free_table(SufAbsNameTable); st_free_table(refTable); RT_Free(cm->rm); sat_ArrayFree(manager->assertArray); status = cm->status; cm->option->coreGeneration = 1; PureSat_SatFreeManager(cm); if(status == SAT_SAT){ if(pm->verbosity>=1) fprintf(vis_stdout,"CEX exist\n"); return FALSE; // cex exists } else{ if(pm->verbosity>=1) fprintf(vis_stdout,"no CEX\n"); return TRUE; // no cex } } /**Function******************************************************************** Synopsis [Generate BFS ring for a network node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGenerateRingForNode(Ntk_Network_t *network, PureSat_Manager_t *pm, Ntk_Node_t * node1, array_t * ringArray, int *dfs) { Ntk_Node_t *node; char *name; int i; if(PureSatNodeReadColor(node1) == dfsBlack_c) return; PureSatNodeSetColor(node1,dfsBlack_c); if(Ntk_NodeTestIsLatch(node1)){ name = Ntk_NodeReadName(node1); st_insert(pm->node2dfsTable,name,(char*)(long)(*dfs)); array_insert_last(char *,ringArray,name); return; } Ntk_NodeForEachFanin(node1,i,node){ PureSatGenerateRingForNode(network,pm,node,ringArray, dfs); } return; } /**Function******************************************************************** Synopsis [Generate BFS ring for one array] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatGenerateRing(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t * coreArray, int * dfs) { array_t * ringArray = array_alloc(char *,0); int i,j; char *name; Ntk_Node_t *node1,*node; arrayForEachItem(char *,coreArray,i,name){ node1 = Ntk_NetworkFindNodeByName(network,name); Ntk_NodeForEachFanin(node1,j,node){ PureSatGenerateRingForNode(network,pm,node, ringArray,dfs); } } return ringArray; } /**Function******************************************************************** Synopsis [Generate the ring information for the whole circuit] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGenerateDfs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t * vertexArray) { int dfs = 1,i,ct=0; char *name; Ntk_Node_t *node; array_t * ringArray = array_alloc(char *,0); array_t * coreArray; lsGen gen; st_generator * stgen; Ntk_NetworkForEachNode( network, gen, node ) { PureSatNodeSetColor( node, dfsWhite_c ); } arrayForEachItem(char *,vertexArray,i,name){ st_insert(pm->node2dfsTable,name,(char*)(long)dfs); node = Ntk_NetworkFindNodeByName(network,name); PureSatNodeSetColor(node,dfsBlack_c); ct++; } coreArray = array_dup(vertexArray); while(coreArray->num>0){ dfs++; ringArray = PureSatGenerateRing(network,pm,coreArray, &dfs); arrayForEachItem(char*,ringArray,i,name){ st_insert(pm->node2dfsTable,name,(char*)(long)dfs); ct++; } array_free(coreArray); coreArray = ringArray; } st_foreach_item(pm->CoiTable,stgen,&node,NIL(char*)){ name = Ntk_NodeReadName(node); if(!st_lookup(pm->node2dfsTable,name,NIL(char*))){ st_insert(pm->node2dfsTable,name,(char*)LARGEDFS); if(pm->verbosity>=2) fprintf(vis_stdout,"%s LARGEDFS is inserted into node2dfsTable\n",name); } } return; } /**Function******************************************************************** Synopsis [Sort latch candidate based on BFS ring and RC information] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSatComputeOrder_2(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t * vertexArray, array_t * invisibleArray, int * sccArray, int * NumInSecondLevel) { array_t * RCArray; PureSatGenerateDfs(network,pm,vertexArray); RCArray = PureSatGenerateRCArray_2(network,pm,invisibleArray, NumInSecondLevel); return RCArray; } /**Function******************************************************************** Synopsis [Some latches have the same aig node, add them all to abstractions once one is added. ] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatAddIdenLatchToAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *nameArray) { int i; st_generator * stgen; st_table* table; char *name,*name1; st_table *table1 = st_init_table(st_ptrcmp,st_ptrhash); array_t * tmpArray = array_alloc(char*,0); st_foreach_item(pm->vertexTable,stgen,&name,NIL(char*)) st_insert(table1,name,(char*)0); arrayForEachItem(char*,nameArray,i,name) st_insert(table1,name,(char*)0); arrayForEachItem(char*,nameArray,i,name){ if(st_lookup(pm->IdenLatchTable,name,&table)){ st_foreach_item(table,stgen,&name1,NIL(char*)){ if(!st_lookup(table1,name1,NIL(char*))){ st_insert(table1,name1,(char*)0); array_insert_last(char*,tmpArray,name1); } } } } arrayForEachItem(char*,tmpArray,i,name){ array_insert_last(char*,nameArray,name); if(pm->verbosity>=2) fprintf(vis_stdout,"add %s to refineArray\n",name); } array_free(tmpArray); st_free_table(table1); } /**Function******************************************************************** Synopsis [Create initial abstraction from aig] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatCreateInitAbsByAIG(bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, st_table * tmpTable) { bAigTimeFrame_t * tf = manager->timeframeWOI; char * name; st_table * table; st_generator * stgen; if(node==bAig_NULL) return; node = bAig_NonInvertedEdge(node); if(flags(node)&VisitedMask) return; flags(node) |= VisitedMask; if(flags(node)&StateBitMask){ if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){ int retVal = st_lookup(tf->idx2name,(char*)node,&name); assert(retVal); if(!st_lookup(tmpTable,name,NIL(char*))){ st_insert(tmpTable,name,(char*)0); } } else{ st_foreach_item(table,stgen,&name,NIL(char*)){ if(!st_lookup(tmpTable,name,NIL(char*))){ st_insert(tmpTable,name,(char*)0); } } } } if(flags(node)&StateBitMask) return; PureSatCreateInitAbsByAIG(manager,pm,leftChild(node),tmpTable); PureSatCreateInitAbsByAIG(manager,pm,rightChild(node),tmpTable); } /**Function******************************************************************** Synopsis [Get support latches for one aig node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSat_GetLatchForNode(bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, array_t * nameArray, st_table *tmpTable, int cut) { bAigTimeFrame_t * tf = manager->timeframeWOI; char * name; st_table * table; st_generator * stgen; if(node==bAig_NULL) return; node = bAig_NonInvertedEdge(node); if(flags(node)&VisitedMask) return; flags(node) |= VisitedMask; if(flags(node)&StateBitMask){ if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){ int retVal = st_lookup(tf->idx2name,(char*)node,&name); assert(retVal); if(!st_lookup(tmpTable,name,NIL(char*))){ st_insert(tmpTable,name,(char*)0); array_insert_last(char *,nameArray,name); if(pm->verbosity>=2) fprintf(vis_stdout,"insert %s\n",name); } } else{ st_foreach_item(table,stgen,&name,NIL(char*)){ if(!st_lookup(tmpTable,name,NIL(char*))){ st_insert(tmpTable,name,(char*)0); array_insert_last(char *,nameArray,name); if(pm->verbosity>=2) fprintf(vis_stdout,"insert %s\n",name); } } } } if(cut==2){ if(flags(node)&Visited2Mask) return; } else{ if(cut==1){ if(flags(node)&Visited3Mask) return; } else{ fprintf(vis_stdout,"wrong cut\n"); exit(0); } } PureSat_GetLatchForNode(manager,pm,leftChild(node),nameArray,tmpTable,cut); PureSat_GetLatchForNode(manager,pm,rightChild(node),nameArray,tmpTable,cut); } /**Function******************************************************************** Synopsis [Get COI reduction based on aig, not ntk] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ st_table * PureSatGetAigCoi(Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property) { bAig_Manager_t *manager; st_table * node2MvfAigTable,*tmpTable; array_t * nameArray,*nameArray1; bAigTimeFrame_t *tf; char * name; Ntk_Node_t *latch; MvfAig_Function_t *mvfAig; mAigMvar_t lmVar; mAigBvar_t bVar; array_t *bVarList,*mVarList; int i,j,lmAigId; long index,index1; bAigEdge_t v, *li, *bli; manager = Ntk_NetworkReadMAigManager(network); if (manager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n"); exit(0);; } node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); tf = manager->timeframeWOI; bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); assert(manager->timeframeWOI->currentTimeframe>=2); PureSat_CleanMask(manager,ResetVisitedMask); PureSat_CleanMask(manager,ResetVisited2Mask); PureSat_CleanMask(manager,ResetVisited3Mask); li = tf->latchInputs[1]; for(i=0;inLatches;i++) flags(li[i])|=Visited3Mask; li = tf->blatchInputs[1]; for(i=0;inbLatches;i++) flags(li[i])|=Visited3Mask; li = tf->latchInputs[2]; for(i=0;inLatches;i++) flags(li[i])|=Visited2Mask; li = tf->blatchInputs[2]; for(i=0;inbLatches;i++) flags(li[i])|=Visited2Mask; nameArray = array_alloc(char *,0); tmpTable = st_init_table(st_ptrcmp,st_ptrhash); PureSat_GetLatchForNode(manager,pm,property,nameArray,tmpTable,2); PureSat_CleanMask(manager,ResetVisitedMask); li = tf->latchInputs[2]; bli = tf->blatchInputs[2]; while(nameArray->num>0){ nameArray1 = nameArray; nameArray = array_alloc(char *,0); arrayForEachItem(char*,nameArray1,i,name){ latch = Ntk_NetworkFindNodeByName(network,name); st_lookup(node2MvfAigTable,latch,&mvfAig); for(j=0;jnum;j++){ int retVal; v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j)); if(v==bAig_Zero||v==bAig_One) continue; retVal = st_lookup(tf->li2index,(char*)v,&index); assert(retVal); if(li[index]==bAig_Zero||li[index]==bAig_One) continue; PureSat_GetLatchForNode(manager,pm,li[index],nameArray,tmpTable,1); } lmAigId = Ntk_NodeReadMAigId(latch); lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId); for(j=0,index1=lmVar.bVars;jbli2index,(char*)bVar.node,&index); assert(retVal); if(bli[index]==bAig_Zero||bli[index]==bAig_One) continue; PureSat_GetLatchForNode(manager,pm,bli[index],nameArray,tmpTable,1); } } array_free(nameArray1); } array_free(nameArray); PureSat_CleanMask(manager,ResetVisitedMask); PureSat_CleanMask(manager,ResetVisited2Mask); PureSat_CleanMask(manager,ResetVisited3Mask); return tmpTable; } /**Function******************************************************************** Synopsis [There are some latches whose DI is empty, put them into abstraction will not add any burden to model checker] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatPreProcLatch(Ntk_Network_t *network, PureSat_Manager_t *pm) { st_generator * stgen; bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); bAigTimeFrame_t * tf = manager->timeframeWOI; mAigMvar_t lmVar; mAigBvar_t bVar; array_t *bVarList,*mVarList; int j,lmAigId,id,index1; char * name; Ntk_Node_t * latch; bAigEdge_t v, **li, **bli; MvfAig_Function_t *mvfAig; bVarList = mAigReadBinVarList(manager); mVarList = mAigReadMulVarList(manager); li = tf->latchInputs; bli = tf->blatchInputs; st_foreach_item(pm->CoiTable,stgen,&latch,NIL(char*)){ int checkbin=1; st_lookup(node2MvfAigTable,latch,&mvfAig); for(j=0;jnum;j++){ int retVal; v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j)); if(v==bAig_Zero||v==bAig_One) continue; retVal = st_lookup(tf->li2index,(char*)v,&id); assert(retVal); if(li[0][id]==li[1][id]&&li[1][id]==li[2][id]){ name = Ntk_NodeReadName(latch); st_insert(pm->vertexTable,name,(char*)0); if(pm->verbosity>=2) fprintf(vis_stdout,"preproc: add %s to abs\n",name); checkbin = 0; break; } } if(checkbin){ lmAigId = Ntk_NodeReadMAigId(latch); lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId); for(j=0,index1=lmVar.bVars;jbli2index,(char*)bVar.node,&id); assert(retVal); if(bli[0][id]==bli[1][id]&&bli[1][id]==bli[2][id]){ name = Ntk_NodeReadName(latch); st_insert(pm->vertexTable,name,(char*)0); if(pm->verbosity>=2) fprintf(vis_stdout,"preproc BINARY: add %s to abs\n",name); break; } } } } } /**Function******************************************************************** Synopsis [Generate identical latch clusters] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void PureSatGetIndenticalLatch(Ntk_Network_t *network, PureSat_Manager_t *pm) { bAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t * tf = manager->timeframeWOI; bAigEdge_t *li=tf->latchInputs[2],*bli = tf->blatchInputs[2]; int i; bAigEdge_t v; st_table *table; st_generator *stgen,*stgen1; char *name,*name1; st_table *table2,*table1=st_init_table(st_ptrcmp,st_ptrhash); pm->IdenLatchTable = st_init_table(st_ptrcmp,st_ptrhash); for(i=0;inLatches;i++){ v=bAig_NonInvertedEdge(li[i]); if(!st_lookup(table1,(char*)v,NIL(char*))){ if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){ int init=0; st_foreach_item(table,stgen,&name,NIL(char*)){ if(!st_lookup(pm->IdenLatchTable,name,&table2)){ st_insert(pm->IdenLatchTable,name,table); if(pm->verbosity>=2) fprintf(vis_stdout,"%s and ",name); init = 1; } /*insert everything in table 2 into table name is already in another group, put everything of current group into that group*/ else{ st_foreach_item(table,stgen1,&name1,NIL(char*)){ st_insert(table2,name1,(char*)0); st_insert(pm->IdenLatchTable,name1,table2); if(pm->verbosity>=2) fprintf(vis_stdout,"%s and ",name1); } if(pm->verbosity>=2) fprintf(vis_stdout,"are the same\n"); break; } } if(init){ if(pm->verbosity>=2) fprintf(vis_stdout,"are the same\n"); } } st_insert(table1,(char*)v,(char*)0); } } for(i=0;inbLatches;i++){ v=bAig_NonInvertedEdge(bli[i]); if(!st_lookup(table1,(char*)v,NIL(char*))){ if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){ int init=0; st_foreach_item(table,stgen,&name,NIL(char*)){ if(!st_lookup(pm->IdenLatchTable,name,table2)){ st_insert(pm->IdenLatchTable,name,table); if(pm->verbosity>=2) fprintf(vis_stdout,"%s and ",name); init = 1; } /*insert everything in table 2 into table name is already in another group, put everything of current group into that group*/ else{ st_foreach_item(table,stgen1,&name1,NIL(char*)){ st_insert(table2,name1,(char*)0); st_insert(pm->IdenLatchTable,name1,table2); if(pm->verbosity>=2) fprintf(vis_stdout,"%s and ",name1); } if(pm->verbosity>=2) fprintf(vis_stdout,"are the same\n"); break; } } if(init){ if(pm->verbosity>=2) fprintf(vis_stdout,"are the same\n"); } } st_insert(table1,(char*)v,(char*)0); } } st_free_table(table1); }