src/aig/ivy/ivyFraig.c File Reference
#include "satSolver.h"#include "extra.h"#include "ivy.h"#include "cuddInt.h"
Include dependency graph for ivyFraig.c:
Go to the source code of this file.
Define Documentation
| #define Ivy_FraigForEachBinNode | ( | pBin, | |||
| pEnt | ) |
Value:
for ( pEnt = pBin; \ pEnt; \ pEnt = Ivy_ObjNodeHashNext(pEnt) )
Definition at line 177 of file ivyFraig.c.
| #define Ivy_FraigForEachClassNode | ( | pClass, | |||
| pEnt | ) |
Value:
for ( pEnt = pClass; \ pEnt; \ pEnt = Ivy_ObjClassNodeNext(pEnt) )
Definition at line 172 of file ivyFraig.c.
| #define Ivy_FraigForEachEquivClass | ( | pList, | |||
| pEnt | ) |
Value:
for ( pEnt = pList; \ pEnt; \ pEnt = Ivy_ObjEquivListNext(pEnt) )
Definition at line 161 of file ivyFraig.c.
| #define Ivy_FraigForEachEquivClassSafe | ( | pList, | |||
| pEnt, | |||||
| pEnt2 | ) |
Value:
for ( pEnt = pList, \ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \ pEnt; \ pEnt = pEnt2, \ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
Definition at line 165 of file ivyFraig.c.
Typedef Documentation
| typedef struct Ivy_FraigList_t_ Ivy_FraigList_t |
Definition at line 31 of file ivyFraig.c.
| typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t |
CFile****************************************************************
FileName [ivyFraig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Functional reduction of AIGs]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS ///
Definition at line 29 of file ivyFraig.c.
| typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t |
Definition at line 30 of file ivyFraig.c.
| typedef struct Prove_ParamsStruct_t_ Prove_Params_t |
Definition at line 104 of file ivyFraig.c.
Function Documentation
| void Ivy_FraigAddClass | ( | Ivy_FraigList_t * | pList, | |
| Ivy_Obj_t * | pClass | |||
| ) |
Function*************************************************************
Synopsis [Adds equivalence class to the list of classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 1056 of file ivyFraig.c.
01057 { 01058 if ( pList->pHead == NULL ) 01059 { 01060 pList->pHead = pClass; 01061 pList->pTail = pClass; 01062 Ivy_ObjSetEquivListPrev( pClass, NULL ); 01063 Ivy_ObjSetEquivListNext( pClass, NULL ); 01064 } 01065 else 01066 { 01067 Ivy_ObjSetEquivListNext( pList->pTail, pClass ); 01068 Ivy_ObjSetEquivListPrev( pClass, pList->pTail ); 01069 Ivy_ObjSetEquivListNext( pClass, NULL ); 01070 pList->pTail = pClass; 01071 } 01072 pList->nItems++; 01073 }
| void Ivy_FraigAddClausesMux | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pNode | |||
| ) |
Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
Definition at line 2297 of file ivyFraig.c.
02298 { 02299 Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE; 02300 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; 02301 02302 assert( !Ivy_IsComplement( pNode ) ); 02303 assert( Ivy_ObjIsMuxType( pNode ) ); 02304 // get nodes (I = if, T = then, E = else) 02305 pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); 02306 // get the variable numbers 02307 VarF = Ivy_ObjSatNum(pNode); 02308 VarI = Ivy_ObjSatNum(pNodeI); 02309 VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT)); 02310 VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE)); 02311 // get the complementation flags 02312 fCompT = Ivy_IsComplement(pNodeT); 02313 fCompE = Ivy_IsComplement(pNodeE); 02314 02315 // f = ITE(i, t, e) 02316 02317 // i' + t' + f 02318 // i' + t + f' 02319 // i + e' + f 02320 // i + e + f' 02321 02322 // create four clauses 02323 pLits[0] = toLitCond(VarI, 1); 02324 pLits[1] = toLitCond(VarT, 1^fCompT); 02325 pLits[2] = toLitCond(VarF, 0); 02326 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02327 assert( RetValue ); 02328 pLits[0] = toLitCond(VarI, 1); 02329 pLits[1] = toLitCond(VarT, 0^fCompT); 02330 pLits[2] = toLitCond(VarF, 1); 02331 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02332 assert( RetValue ); 02333 pLits[0] = toLitCond(VarI, 0); 02334 pLits[1] = toLitCond(VarE, 1^fCompE); 02335 pLits[2] = toLitCond(VarF, 0); 02336 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02337 assert( RetValue ); 02338 pLits[0] = toLitCond(VarI, 0); 02339 pLits[1] = toLitCond(VarE, 0^fCompE); 02340 pLits[2] = toLitCond(VarF, 1); 02341 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02342 assert( RetValue ); 02343 02344 // two additional clauses 02345 // t' & e' -> f' 02346 // t & e -> f 02347 02348 // t + e + f' 02349 // t' + e' + f 02350 02351 if ( VarT == VarE ) 02352 { 02353 // assert( fCompT == !fCompE ); 02354 return; 02355 } 02356 02357 pLits[0] = toLitCond(VarT, 0^fCompT); 02358 pLits[1] = toLitCond(VarE, 0^fCompE); 02359 pLits[2] = toLitCond(VarF, 1); 02360 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02361 assert( RetValue ); 02362 pLits[0] = toLitCond(VarT, 1^fCompT); 02363 pLits[1] = toLitCond(VarE, 1^fCompE); 02364 pLits[2] = toLitCond(VarF, 0); 02365 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); 02366 assert( RetValue ); 02367 }
| void Ivy_FraigAddClausesSuper | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pNode, | |||
| Vec_Ptr_t * | vSuper | |||
| ) |
Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
Definition at line 2380 of file ivyFraig.c.
02381 { 02382 Ivy_Obj_t * pFanin; 02383 int * pLits, nLits, RetValue, i; 02384 assert( !Ivy_IsComplement(pNode) ); 02385 assert( Ivy_ObjIsNode( pNode ) ); 02386 // create storage for literals 02387 nLits = Vec_PtrSize(vSuper) + 1; 02388 pLits = ALLOC( int, nLits ); 02389 // suppose AND-gate is A & B = C 02390 // add !A => !C or A + !C 02391 Vec_PtrForEachEntry( vSuper, pFanin, i ) 02392 { 02393 pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin)); 02394 pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1); 02395 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 02396 assert( RetValue ); 02397 } 02398 // add A & B => C or !A + !B + C 02399 Vec_PtrForEachEntry( vSuper, pFanin, i ) 02400 pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin)); 02401 pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0); 02402 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); 02403 assert( RetValue ); 02404 free( pLits ); 02405 }
| void Ivy_FraigAddToPatScores | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pClass, | |||
| Ivy_Obj_t * | pClassNew | |||
| ) | [static] |
Function*************************************************************
Synopsis [Adds to pattern scores.]
Description []
SideEffects []
SeeAlso []
Definition at line 1666 of file ivyFraig.c.
01667 { 01668 Ivy_FraigSim_t * pSims0, * pSims1; 01669 unsigned uDiff; 01670 int i, w; 01671 // get hold of the simulation information 01672 pSims0 = Ivy_ObjSim(pClass); 01673 pSims1 = Ivy_ObjSim(pClassNew); 01674 // iterate through the differences and record the score 01675 for ( w = 0; w < p->nSimWords; w++ ) 01676 { 01677 uDiff = pSims0->pData[w] ^ pSims1->pData[w]; 01678 if ( uDiff == 0 ) 01679 continue; 01680 for ( i = 0; i < 32; i++ ) 01681 if ( uDiff & ( 1 << i ) ) 01682 p->pPatScores[w*32+i]++; 01683 } 01684 }
| Ivy_Obj_t * Ivy_FraigAnd | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObjOld | |||
| ) | [static] |
Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
Definition at line 2001 of file ivyFraig.c.
02002 { 02003 Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew; 02004 int RetValue; 02005 // get the fraiged fanins 02006 pFanin0New = Ivy_ObjChild0Equiv(pObjOld); 02007 pFanin1New = Ivy_ObjChild1Equiv(pObjOld); 02008 // get the candidate fraig node 02009 pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New ); 02010 // get representative of this class 02011 if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node 02012 (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node 02013 { 02014 assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) ); 02015 assert( pObjNew != Ivy_Regular(pFanin0New) ); 02016 assert( pObjNew != Ivy_Regular(pFanin1New) ); 02017 return pObjNew; 02018 } 02019 // get the fraiged representative 02020 pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld)); 02021 // if the fraiged nodes are the same return 02022 if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) ) 02023 return pObjNew; 02024 assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) ); 02025 // printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id ); 02026 02027 // they are different (the counter-example is in p->pPatWords) 02028 RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) ); 02029 if ( RetValue == 1 ) // proved equivalent 02030 { 02031 // mark the class as proved 02032 if ( Ivy_ObjClassNodeNext(pObjOld) == NULL ) 02033 Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1; 02034 return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase ); 02035 } 02036 if ( RetValue == -1 ) // failed 02037 return pObjNew; 02038 // simulate the counter-example and return the new node 02039 Ivy_FraigResimulate( p ); 02040 return pObjNew; 02041 }
| void Ivy_FraigAssignDist1 | ( | Ivy_FraigMan_t * | p, | |
| unsigned * | pPat | |||
| ) |
Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
Definition at line 731 of file ivyFraig.c.
00732 { 00733 Ivy_Obj_t * pObj; 00734 int i, Limit; 00735 Ivy_ManForEachPi( p->pManAig, pObj, i ) 00736 { 00737 Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) ); 00738 // printf( "%d", Ivy_InfoHasBit(pPat, i) ); 00739 } 00740 // printf( "\n" ); 00741 00742 Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); 00743 for ( i = 0; i < Limit; i++ ) 00744 Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 ); 00745 }
| void Ivy_FraigAssignRandom | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
Definition at line 712 of file ivyFraig.c.
00713 { 00714 Ivy_Obj_t * pObj; 00715 int i; 00716 Ivy_ManForEachPi( p->pManAig, pObj, i ) 00717 Ivy_NodeAssignRandom( p, pObj ); 00718 }
| int Ivy_FraigCheckOutputSims | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Returns 1 if the one of the output is already non-constant 0.]
Description []
SideEffects []
SeeAlso []
Definition at line 1338 of file ivyFraig.c.
01339 { 01340 Ivy_Obj_t * pObj; 01341 int i; 01342 // make sure the reference simulation pattern does not detect the bug 01343 pObj = Ivy_ManPo( p->pManAig, 0 ); 01344 assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0 01345 Ivy_ManForEachPo( p->pManAig, pObj, i ) 01346 { 01347 // complement simulation info 01348 // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) 01349 // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) ); 01350 // check 01351 if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) ) 01352 { 01353 // create the counter-example from this pattern 01354 Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) ); 01355 return 1; 01356 } 01357 // complement simulation info 01358 // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) 01359 // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) ); 01360 } 01361 return 0; 01362 }
| void Ivy_FraigCheckOutputSimsSavePattern | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Creates the counter-example from the successful pattern.]
Description []
SideEffects []
SeeAlso []
Definition at line 1296 of file ivyFraig.c.
01297 { 01298 Ivy_FraigSim_t * pSims; 01299 int i, k, BestPat, * pModel; 01300 // find the word of the pattern 01301 pSims = Ivy_ObjSim(pObj); 01302 for ( i = 0; i < p->nSimWords; i++ ) 01303 if ( pSims->pData[i] ) 01304 break; 01305 assert( i < p->nSimWords ); 01306 // find the bit of the pattern 01307 for ( k = 0; k < 32; k++ ) 01308 if ( pSims->pData[i] & (1 << k) ) 01309 break; 01310 assert( k < 32 ); 01311 // determine the best pattern 01312 BestPat = i * 32 + k; 01313 // fill in the counter-example data 01314 pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); 01315 Ivy_ManForEachPi( p->pManAig, pObj, i ) 01316 { 01317 pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat); 01318 // printf( "%d", pModel[i] ); 01319 } 01320 // printf( "\n" ); 01321 // set the model 01322 assert( p->pManFraig->pData == NULL ); 01323 p->pManFraig->pData = pModel; 01324 return; 01325 }
| void Ivy_FraigCleanPatScores | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Cleans pattern scores.]
Description []
SideEffects []
SeeAlso []
Definition at line 1648 of file ivyFraig.c.
01649 { 01650 int i, nLimit = p->nSimWords * 32; 01651 for ( i = 0; i < nLimit; i++ ) 01652 p->pPatScores[i] = 0; 01653 }
Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
Definition at line 2443 of file ivyFraig.c.
02444 { 02445 Vec_Ptr_t * vSuper; 02446 assert( !Ivy_IsComplement(pObj) ); 02447 assert( !Ivy_ObjIsPi(pObj) ); 02448 vSuper = Vec_PtrAlloc( 4 ); 02449 Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); 02450 return vSuper; 02451 }
Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
Definition at line 2418 of file ivyFraig.c.
02419 { 02420 // if the new node is complemented or a PI, another gate begins 02421 if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || 02422 (fUseMuxes && Ivy_ObjIsMuxType(pObj)) ) 02423 { 02424 Vec_PtrPushUnique( vSuper, pObj ); 02425 return; 02426 } 02427 // go through the branches 02428 Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes ); 02429 Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes ); 02430 }
| int Ivy_FraigCountClassNodes | ( | Ivy_Obj_t * | pClass | ) |
Function*************************************************************
Synopsis [Count the number of elements in the class.]
Description []
SideEffects []
SeeAlso []
Definition at line 1434 of file ivyFraig.c.
01435 { 01436 Ivy_Obj_t * pObj; 01437 int Counter = 0; 01438 Ivy_FraigForEachClassNode( pClass, pObj ) 01439 Counter++; 01440 return Counter; 01441 }
| int Ivy_FraigCountPairsClasses | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
SideEffects []
SeeAlso []
Definition at line 1136 of file ivyFraig.c.
01137 { 01138 Ivy_Obj_t * pClass, * pNode; 01139 int nPairs = 0, nNodes; 01140 return nPairs; 01141 01142 Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) 01143 { 01144 nNodes = 0; 01145 Ivy_FraigForEachClassNode( pClass, pNode ) 01146 nNodes++; 01147 nPairs += nNodes * (nNodes - 1) / 2; 01148 } 01149 return nPairs; 01150 }
| void Ivy_FraigCreateClasses | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
SideEffects []
SeeAlso []
Definition at line 1163 of file ivyFraig.c.
01164 { 01165 Ivy_Obj_t ** pTable; 01166 Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry; 01167 int i, nTableSize; 01168 unsigned Hash; 01169 pConst1 = Ivy_ManConst1(p->pManAig); 01170 // allocate the table 01171 nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13; 01172 pTable = ALLOC( Ivy_Obj_t *, nTableSize ); 01173 memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize ); 01174 // collect nodes into the table 01175 Ivy_ManForEachObj( p->pManAig, pObj, i ) 01176 { 01177 if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) 01178 continue; 01179 Hash = Ivy_NodeHash( p, pObj ); 01180 if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) ) 01181 { 01182 Ivy_NodeAddToClass( pConst1, pObj ); 01183 continue; 01184 } 01185 // add the node to the table 01186 pBin = pTable[Hash % nTableSize]; 01187 Ivy_FraigForEachBinNode( pBin, pEntry ) 01188 if ( Ivy_NodeCompareSims( p, pEntry, pObj ) ) 01189 { 01190 Ivy_NodeAddToClass( pEntry, pObj ); 01191 break; 01192 } 01193 // check if the entry was added 01194 if ( pEntry ) 01195 continue; 01196 Ivy_ObjSetNodeHashNext( pObj, pBin ); 01197 pTable[Hash % nTableSize] = pObj; 01198 } 01199 // collect non-trivial classes 01200 assert( p->lClasses.pHead == NULL ); 01201 Ivy_ManForEachObj( p->pManAig, pObj, i ) 01202 { 01203 if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) 01204 continue; 01205 Ivy_ObjSetNodeHashNext( pObj, NULL ); 01206 if ( Ivy_ObjClassNodeRepr(pObj) == NULL ) 01207 { 01208 assert( Ivy_ObjClassNodeNext(pObj) == NULL ); 01209 continue; 01210 } 01211 // recognize the head of the class 01212 if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL ) 01213 continue; 01214 // clean the class representative and add it to the list 01215 Ivy_ObjSetClassNodeRepr( pObj, NULL ); 01216 Ivy_FraigAddClass( &p->lClasses, pObj ); 01217 } 01218 // free the table 01219 free( pTable ); 01220 }
| int * Ivy_FraigCreateModel | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Generates the counter-example satisfying the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 1508 of file ivyFraig.c.
01509 { 01510 int * pModel; 01511 Ivy_Obj_t * pObj; 01512 int i; 01513 pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); 01514 Ivy_ManForEachPi( p->pManFraig, pObj, i ) 01515 pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ); 01516 return pModel; 01517 }
| void Ivy_FraigInsertClass | ( | Ivy_FraigList_t * | pList, | |
| Ivy_Obj_t * | pBase, | |||
| Ivy_Obj_t * | pClass | |||
| ) |
Function*************************************************************
Synopsis [Updates the list of classes after base class has split.]
Description []
SideEffects []
SeeAlso []
Definition at line 1086 of file ivyFraig.c.
01087 { 01088 Ivy_ObjSetEquivListPrev( pClass, pBase ); 01089 Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); 01090 if ( Ivy_ObjEquivListNext(pBase) ) 01091 Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass ); 01092 Ivy_ObjSetEquivListNext( pBase, pClass ); 01093 if ( pList->pTail == pBase ) 01094 pList->pTail = pClass; 01095 pList->nItems++; 01096 }
| Ivy_Man_t* Ivy_FraigMiter | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) |
Function*************************************************************
Synopsis [Applies brute-force SAT to the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 471 of file ivyFraig.c.
00472 { 00473 Ivy_FraigMan_t * p; 00474 Ivy_Man_t * pManAigNew; 00475 Ivy_Obj_t * pObj; 00476 int i, clk; 00477 clk = clock(); 00478 assert( Ivy_ManLatchNum(pManAig) == 0 ); 00479 p = Ivy_FraigStartSimple( pManAig, pParams ); 00480 // set global limits 00481 p->nBTLimitGlobal = s_nBTLimitGlobal; 00482 p->nInsLimitGlobal = s_nInsLimitGlobal; 00483 // duplicate internal nodes 00484 Ivy_ManForEachNode( p->pManAig, pObj, i ) 00485 pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); 00486 // try to prove each output of the miter 00487 Ivy_FraigMiterProve( p ); 00488 // add the POs 00489 Ivy_ManForEachPo( p->pManAig, pObj, i ) 00490 Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); 00491 // clean the new manager 00492 Ivy_ManForEachObj( p->pManFraig, pObj, i ) 00493 { 00494 if ( Ivy_ObjFaninVec(pObj) ) 00495 Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); 00496 pObj->pNextFan0 = pObj->pNextFan1 = NULL; 00497 } 00498 // remove dangling nodes 00499 Ivy_ManCleanup( p->pManFraig ); 00500 pManAigNew = p->pManFraig; 00501 p->timeTotal = clock() - clk; 00502 00503 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) ); 00504 //PRT( "Time", p->timeTotal ); 00505 Ivy_FraigStop( p ); 00506 return pManAigNew; 00507 }
| void Ivy_FraigMiterPrint | ( | Ivy_Man_t * | pNtk, | |
| char * | pString, | |||
| int | clk, | |||
| int | fVerbose | |||
| ) | [static] |
Function*************************************************************
Synopsis [Prints the status of the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 1780 of file ivyFraig.c.
01781 { 01782 if ( !fVerbose ) 01783 return; 01784 printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) ); 01785 PRT( pString, clock() - clk ); 01786 }
| void Ivy_FraigMiterProve | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Tries to prove each output of the miter until encountering a sat output.]
Description []
SideEffects []
SeeAlso []
Definition at line 1856 of file ivyFraig.c.
01857 { 01858 Ivy_Obj_t * pObj, * pObjNew; 01859 int i, RetValue, clk = clock(); 01860 int fVerbose = 0; 01861 Ivy_ManForEachPo( p->pManAig, pObj, i ) 01862 { 01863 if ( i && fVerbose ) 01864 { 01865 PRT( "Time", clock() -clk ); 01866 } 01867 pObjNew = Ivy_ObjChild0Equiv(pObj); 01868 // check if the output is constant 1 01869 if ( pObjNew == p->pManFraig->pConst1 ) 01870 { 01871 if ( fVerbose ) 01872 printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) ); 01873 // assing constant 0 model 01874 p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); 01875 memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) ); 01876 break; 01877 } 01878 // check if the output is constant 0 01879 if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) ) 01880 { 01881 if ( fVerbose ) 01882 printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); 01883 continue; 01884 } 01885 // check if the output can be constant 0 01886 if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) 01887 { 01888 if ( fVerbose ) 01889 printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); 01890 // assing constant 0 model 01891 p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); 01892 memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) ); 01893 break; 01894 } 01895 /* 01896 // check the representative of this node 01897 pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj)); 01898 if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 ) 01899 printf( "Representative is not constant 1.\n" ); 01900 else 01901 printf( "Representative is constant 1.\n" ); 01902 */ 01903 // try to prove the output constant 0 01904 RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) ); 01905 if ( RetValue == 1 ) // proved equivalent 01906 { 01907 if ( fVerbose ) 01908 printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); 01909 // set the constant miter 01910 Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) ); 01911 continue; 01912 } 01913 if ( RetValue == -1 ) // failed 01914 { 01915 if ( fVerbose ) 01916 printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter ); 01917 continue; 01918 } 01919 // proved satisfiable 01920 if ( fVerbose ) 01921 printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); 01922 // create the model 01923 p->pManFraig->pData = Ivy_FraigCreateModel(p); 01924 break; 01925 } 01926 if ( fVerbose ) 01927 { 01928 PRT( "Time", clock() -clk ); 01929 } 01930 }
| int Ivy_FraigMiterStatus | ( | Ivy_Man_t * | pMan | ) | [static] |
Function*************************************************************
Synopsis [Reports the status of the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 1799 of file ivyFraig.c.
01800 { 01801 Ivy_Obj_t * pObj, * pObjNew; 01802 int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; 01803 if ( pMan->pData ) 01804 return 0; 01805 Ivy_ManForEachPo( pMan, pObj, i ) 01806 { 01807 pObjNew = Ivy_ObjChild0(pObj); 01808 // check if the output is constant 1 01809 if ( pObjNew == pMan->pConst1 ) 01810 { 01811 CountNonConst0++; 01812 continue; 01813 } 01814 // check if the output is constant 0 01815 if ( pObjNew == Ivy_Not(pMan->pConst1) ) 01816 { 01817 CountConst0++; 01818 continue; 01819 } 01820 // check if the output can be constant 0 01821 if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) 01822 { 01823 CountNonConst0++; 01824 continue; 01825 } 01826 CountUndecided++; 01827 } 01828 /* 01829 if ( p->pParams->fVerbose ) 01830 { 01831 printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) ); 01832 printf( "Const0 = %d. ", CountConst0 ); 01833 printf( "NonConst0 = %d. ", CountNonConst0 ); 01834 printf( "Undecided = %d. ", CountUndecided ); 01835 printf( "\n" ); 01836 } 01837 */ 01838 if ( CountNonConst0 ) 01839 return 0; 01840 if ( CountUndecided ) 01841 return -1; 01842 return 1; 01843 }
| void Ivy_FraigNodeAddToSolver | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pOld, | |||
| Ivy_Obj_t * | pNew | |||
| ) | [static] |
Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
Definition at line 2490 of file ivyFraig.c.
02491 { 02492 Vec_Ptr_t * vFrontier, * vFanins; 02493 Ivy_Obj_t * pNode, * pFanin; 02494 int i, k, fUseMuxes = 1; 02495 assert( pOld || pNew ); 02496 // quit if CNF is ready 02497 if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) ) 02498 return; 02499 // start the frontier 02500 vFrontier = Vec_PtrAlloc( 100 ); 02501 if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier ); 02502 if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier ); 02503 // explore nodes in the frontier 02504 Vec_PtrForEachEntry( vFrontier, pNode, i ) 02505 { 02506 // create the supergate 02507 assert( Ivy_ObjSatNum(pNode) ); 02508 assert( Ivy_ObjFaninVec(pNode) == NULL ); 02509 if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) ) 02510 { 02511 vFanins = Vec_PtrAlloc( 4 ); 02512 Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) ); 02513 Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) ); 02514 Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) ); 02515 Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) ); 02516 Vec_PtrForEachEntry( vFanins, pFanin, k ) 02517 Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); 02518 Ivy_FraigAddClausesMux( p, pNode ); 02519 } 02520 else 02521 { 02522 vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes ); 02523 Vec_PtrForEachEntry( vFanins, pFanin, k ) 02524 Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); 02525 Ivy_FraigAddClausesSuper( p, pNode, vFanins ); 02526 } 02527 assert( Vec_PtrSize(vFanins) > 1 ); 02528 Ivy_ObjSetFaninVec( pNode, vFanins ); 02529 } 02530 Vec_PtrFree( vFrontier ); 02531 }
| int Ivy_FraigNodeIsConst | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pNew | |||
| ) | [static] |
Function*************************************************************
Synopsis [Runs equivalence test for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
Definition at line 2222 of file ivyFraig.c.
02223 { 02224 int pLits[2], RetValue1, RetValue, clk; 02225 02226 // make sure the nodes are not complemented 02227 assert( !Ivy_IsComplement(pNew) ); 02228 assert( pNew != p->pManFraig->pConst1 ); 02229 p->nSatCalls++; 02230 02231 // make sure the solver is allocated and has enough variables 02232 if ( p->pSat == NULL ) 02233 { 02234 p->pSat = sat_solver_new(); 02235 p->nSatVars = 1; 02236 sat_solver_setnvars( p->pSat, 1000 ); 02237 // var 0 is reserved for const1 node - add the clause 02238 // pLits[0] = toLit( 0 ); 02239 // sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 02240 } 02241 02242 // if the nodes do not have SAT variables, allocate them 02243 Ivy_FraigNodeAddToSolver( p, NULL, pNew ); 02244 02245 // prepare variable activity 02246 Ivy_FraigSetActivityFactors( p, NULL, pNew ); 02247 02248 // solve under assumptions 02249 clk = clock(); 02250 pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase ); 02251 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 02252 (sint64)p->pParams->nBTLimitMiter, (sint64)0, 02253 p->nBTLimitGlobal, p->nInsLimitGlobal ); 02254 p->timeSat += clock() - clk; 02255 if ( RetValue1 == l_False ) 02256 { 02257 p->timeSatUnsat += clock() - clk; 02258 pLits[0] = lit_neg( pLits[0] ); 02259 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 02260 assert( RetValue ); 02261 // continue solving the other implication 02262 p->nSatCallsUnsat++; 02263 } 02264 else if ( RetValue1 == l_True ) 02265 { 02266 p->timeSatSat += clock() - clk; 02267 if ( p->pPatWords ) 02268 Ivy_FraigSavePattern( p ); 02269 p->nSatCallsSat++; 02270 return 0; 02271 } 02272 else // if ( RetValue1 == l_Undef ) 02273 { 02274 p->timeSatFail += clock() - clk; 02275 // mark the node as the failed node 02276 pNew->fFailTfo = 1; 02277 p->nSatFailsReal++; 02278 return -1; 02279 } 02280 02281 // return SAT proof 02282 p->nSatProof++; 02283 return 1; 02284 }
| int Ivy_FraigNodesAreEquiv | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pOld, | |||
| Ivy_Obj_t * | pNew | |||
| ) | [static] |
Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 2073 of file ivyFraig.c.
02074 { 02075 int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); 02076 02077 // make sure the nodes are not complemented 02078 assert( !Ivy_IsComplement(pNew) ); 02079 assert( !Ivy_IsComplement(pOld) ); 02080 assert( pNew != pOld ); 02081 02082 // if at least one of the nodes is a failed node, perform adjustments: 02083 // if the backtrack limit is small, simply skip this node 02084 // if the backtrack limit is > 10, take the quare root of the limit 02085 nBTLimit = p->pParams->nBTLimitNode; 02086 if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) 02087 { 02088 p->nSatFails++; 02089 // fail immediately 02090 // return -1; 02091 if ( nBTLimit <= 10 ) 02092 return -1; 02093 nBTLimit = (int)pow(nBTLimit, 0.7); 02094 } 02095 p->nSatCalls++; 02096 02097 // make sure the solver is allocated and has enough variables 02098 if ( p->pSat == NULL ) 02099 { 02100 p->pSat = sat_solver_new(); 02101 p->nSatVars = 1; 02102 sat_solver_setnvars( p->pSat, 1000 ); 02103 // var 0 is reserved for const1 node - add the clause 02104 // pLits[0] = toLit( 0 ); 02105 // sat_solver_addclause( p->pSat, pLits, pLits + 1 ); 02106 } 02107 02108 // if the nodes do not have SAT variables, allocate them 02109 Ivy_FraigNodeAddToSolver( p, pOld, pNew ); 02110 02111 // prepare variable activity 02112 Ivy_FraigSetActivityFactors( p, pOld, pNew ); 02113 02114 // solve under assumptions 02115 // A = 1; B = 0 OR A = 1; B = 1 02116 clk = clock(); 02117 pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 ); 02118 pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); 02119 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); 02120 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 02121 (sint64)nBTLimit, (sint64)0, 02122 p->nBTLimitGlobal, p->nInsLimitGlobal ); 02123 p->timeSat += clock() - clk; 02124 if ( RetValue1 == l_False ) 02125 { 02126 p->timeSatUnsat += clock() - clk; 02127 pLits[0] = lit_neg( pLits[0] ); 02128 pLits[1] = lit_neg( pLits[1] ); 02129 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 02130 assert( RetValue ); 02131 // continue solving the other implication 02132 p->nSatCallsUnsat++; 02133 } 02134 else if ( RetValue1 == l_True ) 02135 { 02136 p->timeSatSat += clock() - clk; 02137 Ivy_FraigSavePattern( p ); 02138 p->nSatCallsSat++; 02139 return 0; 02140 } 02141 else // if ( RetValue1 == l_Undef ) 02142 { 02143 p->timeSatFail += clock() - clk; 02144 // mark the node as the failed node 02145 if ( pOld != p->pManFraig->pConst1 ) 02146 pOld->fFailTfo = 1; 02147 pNew->fFailTfo = 1; 02148 p->nSatFailsReal++; 02149 return -1; 02150 } 02151 02152 // if the old node was constant 0, we already know the answer 02153 if ( pOld == p->pManFraig->pConst1 ) 02154 { 02155 p->nSatProof++; 02156 return 1; 02157 } 02158 02159 // solve under assumptions 02160 // A = 0; B = 1 OR A = 0; B = 0 02161 clk = clock(); 02162 pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 ); 02163 pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase ); 02164 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 02165 (sint64)nBTLimit, (sint64)0, 02166 p->nBTLimitGlobal, p->nInsLimitGlobal ); 02167 p->timeSat += clock() - clk; 02168 if ( RetValue1 == l_False ) 02169 { 02170 p->timeSatUnsat += clock() - clk; 02171 pLits[0] = lit_neg( pLits[0] ); 02172 pLits[1] = lit_neg( pLits[1] ); 02173 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); 02174 assert( RetValue ); 02175 p->nSatCallsUnsat++; 02176 } 02177 else if ( RetValue1 == l_True ) 02178 { 02179 p->timeSatSat += clock() - clk; 02180 Ivy_FraigSavePattern( p ); 02181 p->nSatCallsSat++; 02182 return 0; 02183 } 02184 else // if ( RetValue1 == l_Undef ) 02185 { 02186 p->timeSatFail += clock() - clk; 02187 // mark the node as the failed node 02188 pOld->fFailTfo = 1; 02189 pNew->fFailTfo = 1; 02190 p->nSatFailsReal++; 02191 return -1; 02192 } 02193 /* 02194 // check BDD proof 02195 { 02196 int RetVal; 02197 PRT( "Sat", clock() - clk2 ); 02198 clk2 = clock(); 02199 RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew ); 02200 // printf( "%d ", RetVal ); 02201 assert( RetVal ); 02202 PRT( "Bdd", clock() - clk2 ); 02203 printf( "\n" ); 02204 } 02205 */ 02206 // return SAT proof 02207 p->nSatProof++; 02208 return 1; 02209 }
Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
Definition at line 2709 of file ivyFraig.c.
02710 { 02711 static DdManager * dd = NULL; 02712 DdNode * bFunc, * bTemp; 02713 Vec_Ptr_t * vFront; 02714 Ivy_Obj_t * pObj; 02715 int i, RetValue, Iter, Level; 02716 // start the manager 02717 if ( dd == NULL ) 02718 dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); 02719 // create front 02720 vFront = Vec_PtrAlloc( 100 ); 02721 Vec_PtrPush( vFront, pObj1 ); 02722 Vec_PtrPush( vFront, pObj2 ); 02723 // get the function 02724 bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) ); Cudd_Ref( bFunc ); 02725 bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase ); 02726 // try running BDDs 02727 for ( Iter = 0; ; Iter++ ) 02728 { 02729 // find max level 02730 Level = 0; 02731 Vec_PtrForEachEntry( vFront, pObj, i ) 02732 if ( Level < (int)pObj->Level ) 02733 Level = (int)pObj->Level; 02734 if ( Level == 0 ) 02735 break; 02736 bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc ); 02737 Cudd_RecursiveDeref( dd, bTemp ); 02738 if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved 02739 {printf( "%d", Iter ); break;} 02740 if ( Cudd_DagSize(bFunc) > 1000 ) 02741 {printf( "b" ); break;} 02742 if ( dd->size > 120 ) 02743 {printf( "s" ); break;} 02744 if ( Iter > 50 ) 02745 {printf( "i" ); break;} 02746 } 02747 if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat 02748 RetValue = 1; 02749 else if ( Level == 0 ) // sat 02750 RetValue = 0; 02751 else 02752 RetValue = -1; // spaceout/timeout 02753 Cudd_RecursiveDeref( dd, bFunc ); 02754 Vec_PtrFree( vFront ); 02755 return RetValue; 02756 }
| DdNode* Ivy_FraigNodesAreEquivBdd_int | ( | DdManager * | dd, | |
| DdNode * | bFunc, | |||
| Vec_Ptr_t * | vFront, | |||
| int | Level | |||
| ) |
Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
Definition at line 2618 of file ivyFraig.c.
02619 { 02620 DdNode ** pFuncs; 02621 DdNode * bFuncNew; 02622 Vec_Ptr_t * vTemp; 02623 Ivy_Obj_t * pObj, * pFanin; 02624 int i, NewSize; 02625 // create new frontier 02626 vTemp = Vec_PtrAlloc( 100 ); 02627 Vec_PtrForEachEntry( vFront, pObj, i ) 02628 { 02629 if ( (int)pObj->Level != Level ) 02630 { 02631 pObj->fMarkB = 1; 02632 pObj->TravId = Vec_PtrSize(vTemp); 02633 Vec_PtrPush( vTemp, pObj ); 02634 continue; 02635 } 02636 02637 pFanin = Ivy_ObjFanin0(pObj); 02638 if ( pFanin->fMarkB == 0 ) 02639 { 02640 pFanin->fMarkB = 1; 02641 pFanin->TravId = Vec_PtrSize(vTemp); 02642 Vec_PtrPush( vTemp, pFanin ); 02643 } 02644 02645 pFanin = Ivy_ObjFanin1(pObj); 02646 if ( pFanin->fMarkB == 0 ) 02647 { 02648 pFanin->fMarkB = 1; 02649 pFanin->TravId = Vec_PtrSize(vTemp); 02650 Vec_PtrPush( vTemp, pFanin ); 02651 } 02652 } 02653 // collect the permutation 02654 NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp)); 02655 pFuncs = ALLOC( DdNode *, NewSize ); 02656 Vec_PtrForEachEntry( vFront, pObj, i ) 02657 { 02658 if ( (int)pObj->Level != Level ) 02659 pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId ); 02660 else 02661 pFuncs[i] = Cudd_bddAnd( dd, 02662 Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ), 02663 Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) ); 02664 Cudd_Ref( pFuncs[i] ); 02665 } 02666 // add the remaining vars 02667 assert( NewSize == dd->size ); 02668 for ( i = Vec_PtrSize(vFront); i < dd->size; i++ ) 02669 { 02670 pFuncs[i] = Cudd_bddIthVar( dd, i ); 02671 Cudd_Ref( pFuncs[i] ); 02672 } 02673 02674 // create new 02675 bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew ); 02676 // clean trav Id 02677 Vec_PtrForEachEntry( vTemp, pObj, i ) 02678 { 02679 pObj->fMarkB = 0; 02680 pObj->TravId = 0; 02681 } 02682 // deref 02683 for ( i = 0; i < dd->size; i++ ) 02684 Cudd_RecursiveDeref( dd, pFuncs[i] ); 02685 free( pFuncs ); 02686 02687 free( vFront->pArray ); 02688 *vFront = *vTemp; 02689 02690 vTemp->nCap = vTemp->nSize = 0; 02691 vTemp->pArray = NULL; 02692 Vec_PtrFree( vTemp ); 02693 02694 Cudd_Deref( bFuncNew ); 02695 return bFuncNew; 02696 }
| void Ivy_FraigObjAddToFrontier | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| Vec_Ptr_t * | vFrontier | |||
| ) |
Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
Definition at line 2464 of file ivyFraig.c.
02465 { 02466 assert( !Ivy_IsComplement(pObj) ); 02467 if ( Ivy_ObjSatNum(pObj) ) 02468 return; 02469 assert( Ivy_ObjSatNum(pObj) == 0 ); 02470 assert( Ivy_ObjFaninVec(pObj) == NULL ); 02471 if ( Ivy_ObjIsConst1(pObj) ) 02472 return; 02473 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars ); 02474 Ivy_ObjSetSatNum( pObj, p->nSatVars++ ); 02475 if ( Ivy_ObjIsNode(pObj) ) 02476 Vec_PtrPush( vFrontier, pObj ); 02477 }
| void Ivy_FraigParamsDefault | ( | Ivy_FraigParams_t * | pParams | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
Definition at line 220 of file ivyFraig.c.
00221 { 00222 memset( pParams, 0, sizeof(Ivy_FraigParams_t) ); 00223 pParams->nSimWords = 32; // the number of words in the simulation info 00224 pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached 00225 pParams->fPatScores = 0; // enables simulation pattern scoring 00226 pParams->MaxScore = 25; // max score after which resimulation is used 00227 pParams->fDoSparse = 1; // skips sparse functions 00228 // pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped 00229 // pParams->dActConeBumpMax = 5.0; // the largest bump of activity 00230 pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped 00231 pParams->dActConeBumpMax = 10.0; // the largest bump of activity 00232 00233 pParams->nBTLimitNode = 100; // conflict limit at a node 00234 pParams->nBTLimitMiter = 500000; // conflict limit at an output 00235 // pParams->nBTLimitGlobal = 0; // conflict limit global 00236 // pParams->nInsLimitGlobal = 0; // inspection limit global 00237 }
| Ivy_Man_t* Ivy_FraigPerform | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) |
Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 442 of file ivyFraig.c.
00443 { 00444 Ivy_FraigMan_t * p; 00445 Ivy_Man_t * pManAigNew; 00446 int clk; 00447 if ( Ivy_ManNodeNum(pManAig) == 0 ) 00448 return Ivy_ManDup(pManAig); 00449 clk = clock(); 00450 assert( Ivy_ManLatchNum(pManAig) == 0 ); 00451 p = Ivy_FraigStart( pManAig, pParams ); 00452 Ivy_FraigSimulate( p ); 00453 Ivy_FraigSweep( p ); 00454 pManAigNew = p->pManFraig; 00455 p->timeTotal = clock() - clk; 00456 Ivy_FraigStop( p ); 00457 return pManAigNew; 00458 }
| Ivy_Man_t * Ivy_FraigPerform_int | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams, | |||
| sint64 | nBTLimitGlobal, | |||
| sint64 | nInsLimitGlobal, | |||
| sint64 * | pnSatConfs, | |||
| sint64 * | pnSatInspects | |||
| ) | [static] |
Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 405 of file ivyFraig.c.
00406 { 00407 Ivy_FraigMan_t * p; 00408 Ivy_Man_t * pManAigNew; 00409 int clk; 00410 if ( Ivy_ManNodeNum(pManAig) == 0 ) 00411 return Ivy_ManDup(pManAig); 00412 clk = clock(); 00413 assert( Ivy_ManLatchNum(pManAig) == 0 ); 00414 p = Ivy_FraigStart( pManAig, pParams ); 00415 // set global limits 00416 p->nBTLimitGlobal = nBTLimitGlobal; 00417 p->nInsLimitGlobal = nInsLimitGlobal; 00418 00419 Ivy_FraigSimulate( p ); 00420 Ivy_FraigSweep( p ); 00421 pManAigNew = p->pManFraig; 00422 p->timeTotal = clock() - clk; 00423 if ( pnSatConfs ) 00424 *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0; 00425 if ( pnSatInspects ) 00426 *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0; 00427 Ivy_FraigStop( p ); 00428 return pManAigNew; 00429 }
| void Ivy_FraigPrint | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Prints stats for the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 634 of file ivyFraig.c.
00635 { 00636 double nMemory; 00637 nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20); 00638 printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory ); 00639 printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); 00640 printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter ); 00641 printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 00642 p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); 00643 printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 00644 Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); 00645 if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); 00646 PRT( "AIG simulation ", p->timeSim ); 00647 PRT( "AIG traversal ", p->timeTrav ); 00648 PRT( "SAT solving ", p->timeSat ); 00649 PRT( " Unsat ", p->timeSatUnsat ); 00650 PRT( " Sat ", p->timeSatSat ); 00651 PRT( " Fail ", p->timeSatFail ); 00652 PRT( "Class refining ", p->timeRef ); 00653 PRT( "TOTAL RUNTIME ", p->timeTotal ); 00654 if ( p->time1 ) { PRT( "time1 ", p->time1 ); } 00655 }
| void Ivy_FraigPrintActivity | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Prints variable activity.]
Description []
SideEffects []
SeeAlso []
Definition at line 2054 of file ivyFraig.c.
| void Ivy_FraigPrintClass | ( | Ivy_Obj_t * | pClass | ) |
Function*************************************************************
Synopsis [Print the class.]
Description []
SideEffects []
SeeAlso []
Definition at line 1414 of file ivyFraig.c.
01415 { 01416 Ivy_Obj_t * pObj; 01417 printf( "Class {" ); 01418 Ivy_FraigForEachClassNode( pClass, pObj ) 01419 printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' ); 01420 printf( " }\n" ); 01421 }
| void Ivy_FraigPrintSimClasses | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 1454 of file ivyFraig.c.
01455 { 01456 Ivy_Obj_t * pClass; 01457 Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) 01458 { 01459 // Ivy_FraigPrintClass( pClass ); 01460 printf( "%d ", Ivy_FraigCountClassNodes( pClass ) ); 01461 } 01462 // printf( "\n" ); 01463 }
| int Ivy_FraigProve | ( | Ivy_Man_t ** | ppManAig, | |
| void * | pPars | |||
| ) |
Function*************************************************************
Synopsis [Performs combinational equivalence checking for the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 250 of file ivyFraig.c.
00251 { 00252 Prove_Params_t * pParams = pPars; 00253 Ivy_FraigParams_t Params, * pIvyParams = &Params; 00254 Ivy_Man_t * pManAig, * pManTemp; 00255 int RetValue, nIter, clk, timeStart = clock();//, Counter; 00256 sint64 nSatConfs, nSatInspects; 00257 00258 // start the network and parameters 00259 pManAig = *ppManAig; 00260 Ivy_FraigParamsDefault( pIvyParams ); 00261 pIvyParams->fVerbose = pParams->fVerbose; 00262 pIvyParams->fProve = 1; 00263 00264 if ( pParams->fVerbose ) 00265 { 00266 printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n", 00267 pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" ); 00268 printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n", 00269 pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti, 00270 pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti, 00271 pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti ); 00272 printf( "Mitering last = %d.\n", 00273 pParams->nMiteringLimitLast ); 00274 } 00275 00276 // if SAT only, solve without iteration 00277 if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) 00278 { 00279 clk = clock(); 00280 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); 00281 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00282 RetValue = Ivy_FraigMiterStatus( pManAig ); 00283 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00284 *ppManAig = pManAig; 00285 return RetValue; 00286 } 00287 00288 if ( Ivy_ManNodeNum(pManAig) < 500 ) 00289 { 00290 // run the first mitering 00291 clk = clock(); 00292 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig); 00293 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00294 RetValue = Ivy_FraigMiterStatus( pManAig ); 00295 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00296 if ( RetValue >= 0 ) 00297 { 00298 *ppManAig = pManAig; 00299 return RetValue; 00300 } 00301 } 00302 00303 // check the current resource limits 00304 RetValue = -1; 00305 for ( nIter = 0; nIter < pParams->nItersMax; nIter++ ) 00306 { 00307 if ( pParams->fVerbose ) 00308 { 00309 printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 00310 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 00311 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) ); 00312 fflush( stdout ); 00313 } 00314 00315 // try rewriting 00316 if ( pParams->fUseRewriting ) 00317 { // bug in Ivy_NodeFindCutsAll() when leaves are identical! 00318 /* 00319 clk = clock(); 00320 Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); 00321 pManAig = Ivy_ManRwsat( pManAig, 0 ); 00322 RetValue = Ivy_FraigMiterStatus( pManAig ); 00323 Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose ); 00324 */ 00325 } 00326 if ( RetValue >= 0 ) 00327 break; 00328 00329 // try fraiging followed by mitering 00330 if ( pParams->fUseFraiging ) 00331 { 00332 clk = clock(); 00333 pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)); 00334 pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig); 00335 pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp ); 00336 RetValue = Ivy_FraigMiterStatus( pManAig ); 00337 Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose ); 00338 } 00339 if ( RetValue >= 0 ) 00340 break; 00341 00342 // add to the number of backtracks and inspects 00343 pParams->nTotalBacktracksMade += nSatConfs; 00344 pParams->nTotalInspectsMade += nSatInspects; 00345 // check if global resource limit is reached 00346 if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) || 00347 (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) ) 00348 { 00349 printf( "Reached global limit on conflicts/inspects. Quitting.\n" ); 00350 *ppManAig = pManAig; 00351 return -1; 00352 } 00353 } 00354 00355 if ( RetValue < 0 ) 00356 { 00357 if ( pParams->fVerbose ) 00358 { 00359 printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast ); 00360 fflush( stdout ); 00361 } 00362 clk = clock(); 00363 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); 00364 if ( pParams->nTotalBacktrackLimit ) 00365 s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade; 00366 if ( pParams->nTotalInspectLimit ) 00367 s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade; 00368 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00369 s_nBTLimitGlobal = 0; 00370 s_nInsLimitGlobal = 0; 00371 RetValue = Ivy_FraigMiterStatus( pManAig ); 00372 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00373 // make sure that the sover never returns "undecided" when infinite resource limits are set 00374 if( RetValue == -1 && pParams->nTotalInspectLimit == 0 && 00375 pParams->nTotalBacktrackLimit == 0 ) 00376 { 00377 extern void Prove_ParamsPrint( Prove_Params_t * pParams ); 00378 Prove_ParamsPrint( pParams ); 00379 printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n"); 00380 exit(1); 00381 } 00382 } 00383 00384 // assign the model if it was proved by rewriting (const 1 miter) 00385 if ( RetValue == 0 && pManAig->pData == NULL ) 00386 { 00387 pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) ); 00388 memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) ); 00389 } 00390 *ppManAig = pManAig; 00391 return RetValue; 00392 }
| int Ivy_FraigRefineClass_rec | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pClass | |||
| ) |
Function*************************************************************
Synopsis [Recursively refines the class after simulation.]
Description [Returns 1 if the class has changed.]
SideEffects []
SeeAlso []
Definition at line 1233 of file ivyFraig.c.
01234 { 01235 Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode; 01236 int RetValue = 0; 01237 // check if there is refinement 01238 pListOld = pClass; 01239 Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew ) 01240 { 01241 if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) ) 01242 { 01243 if ( p->pParams->fPatScores ) 01244 Ivy_FraigAddToPatScores( p, pClass, pClassNew ); 01245 break; 01246 } 01247 pListOld = pClassNew; 01248 } 01249 if ( pClassNew == NULL ) 01250 return 0; 01251 // set representative of the new class 01252 Ivy_ObjSetClassNodeRepr( pClassNew, NULL ); 01253 // start the new list 01254 pListNew = pClassNew; 01255 // go through the remaining nodes and sort them into two groups: 01256 // (1) matches of the old node; (2) non-matches of the old node 01257 Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode ) 01258 if ( Ivy_NodeCompareSims( p, pClass, pNode ) ) 01259 { 01260 Ivy_ObjSetClassNodeNext( pListOld, pNode ); 01261 pListOld = pNode; 01262 } 01263 else 01264 { 01265 Ivy_ObjSetClassNodeNext( pListNew, pNode ); 01266 Ivy_ObjSetClassNodeRepr( pNode, pClassNew ); 01267 pListNew = pNode; 01268 } 01269 // finish both lists 01270 Ivy_ObjSetClassNodeNext( pListNew, NULL ); 01271 Ivy_ObjSetClassNodeNext( pListOld, NULL ); 01272 // update the list of classes 01273 Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew ); 01274 // if the old class is trivial, remove it 01275 if ( Ivy_ObjClassNodeNext(pClass) == NULL ) 01276 Ivy_FraigRemoveClass( &p->lClasses, pClass ); 01277 // if the new class is trivial, remove it; otherwise, try to refine it 01278 if ( Ivy_ObjClassNodeNext(pClassNew) == NULL ) 01279 Ivy_FraigRemoveClass( &p->lClasses, pClassNew ); 01280 else 01281 RetValue = Ivy_FraigRefineClass_rec( p, pClassNew ); 01282 return RetValue + 1; 01283 }
| int Ivy_FraigRefineClasses | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description [Assumes that simulation info is assigned. Returns the number of classes refined.]
SideEffects [Large equivalence class of constant 0 may cause problems.]
SeeAlso []
Definition at line 1376 of file ivyFraig.c.
01377 { 01378 Ivy_Obj_t * pClass, * pClass2; 01379 int clk, RetValue, Counter = 0; 01380 // check if some outputs already became non-constant 01381 // this is a special case when computation can be stopped!!! 01382 if ( p->pParams->fProve ) 01383 Ivy_FraigCheckOutputSims( p ); 01384 if ( p->pManFraig->pData ) 01385 return 0; 01386 // refine the classed 01387 clk = clock(); 01388 Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 ) 01389 { 01390 if ( pClass->fMarkA ) 01391 continue; 01392 RetValue = Ivy_FraigRefineClass_rec( p, pClass ); 01393 Counter += ( RetValue > 0 ); 01394 //if ( Ivy_ObjIsConst1(pClass) ) 01395 //printf( "%d ", RetValue ); 01396 //if ( Ivy_ObjIsConst1(pClass) ) 01397 // p->time1 += clock() - clk; 01398 } 01399 p->timeRef += clock() - clk; 01400 return Counter; 01401 }
| void Ivy_FraigRemoveClass | ( | Ivy_FraigList_t * | pList, | |
| Ivy_Obj_t * | pClass | |||
| ) |
Function*************************************************************
Synopsis [Removes equivalence class from the list of classes.]
Description []
SideEffects []
SeeAlso []
Definition at line 1109 of file ivyFraig.c.
01110 { 01111 if ( pList->pHead == pClass ) 01112 pList->pHead = Ivy_ObjEquivListNext(pClass); 01113 if ( pList->pTail == pClass ) 01114 pList->pTail = Ivy_ObjEquivListPrev(pClass); 01115 if ( Ivy_ObjEquivListPrev(pClass) ) 01116 Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); 01117 if ( Ivy_ObjEquivListNext(pClass) ) 01118 Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) ); 01119 Ivy_ObjSetEquivListNext( pClass, NULL ); 01120 Ivy_ObjSetEquivListPrev( pClass, NULL ); 01121 pClass->fMarkA = 0; 01122 pList->nItems--; 01123 }
| void Ivy_FraigResimulate | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Resimulates fraiging manager after finding a counter-example.]
Description []
SideEffects []
SeeAlso []
Definition at line 1736 of file ivyFraig.c.
01737 { 01738 int nChanges; 01739 Ivy_FraigAssignDist1( p, p->pPatWords ); 01740 Ivy_FraigSimulateOne( p ); 01741 if ( p->pParams->fPatScores ) 01742 Ivy_FraigCleanPatScores( p ); 01743 nChanges = Ivy_FraigRefineClasses( p ); 01744 if ( p->pManFraig->pData ) 01745 return; 01746 if ( nChanges < 1 ) 01747 printf( "Error: A counter-example did not refine classes!\n" ); 01748 assert( nChanges >= 1 ); 01749 //printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges ); 01750 if ( !p->pParams->fPatScores ) 01751 return; 01752 01753 // perform additional simulation using dist1 patterns derived from successful patterns 01754 while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore ) 01755 { 01756 Ivy_FraigAssignDist1( p, p->pPatWords ); 01757 Ivy_FraigSimulateOne( p ); 01758 Ivy_FraigCleanPatScores( p ); 01759 nChanges = Ivy_FraigRefineClasses( p ); 01760 if ( p->pManFraig->pData ) 01761 return; 01762 //printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); 01763 if ( nChanges == 0 ) 01764 break; 01765 } 01766 }
| void Ivy_FraigSavePattern | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
Definition at line 1530 of file ivyFraig.c.
01531 { 01532 Ivy_Obj_t * pObj; 01533 int i; 01534 memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); 01535 Ivy_ManForEachPi( p->pManFraig, pObj, i ) 01536 // Vec_PtrForEachEntry( p->vPiVars, pObj, i ) 01537 if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) 01538 Ivy_InfoSetBit( p->pPatWords, i ); 01539 // Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); 01540 }
| void Ivy_FraigSavePattern0 | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Generated const 0 pattern.]
Description []
SideEffects []
SeeAlso []
Definition at line 1476 of file ivyFraig.c.
| void Ivy_FraigSavePattern1 | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [[Generated const 1 pattern.]
Description []
SideEffects []
SeeAlso []
Definition at line 1492 of file ivyFraig.c.
| void Ivy_FraigSavePattern2 | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
Definition at line 1553 of file ivyFraig.c.
01554 { 01555 Ivy_Obj_t * pObj; 01556 int i; 01557 memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); 01558 // Ivy_ManForEachPi( p->pManFraig, pObj, i ) 01559 Vec_PtrForEachEntry( p->vPiVars, pObj, i ) 01560 if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) 01561 // Ivy_InfoSetBit( p->pPatWords, i ); 01562 Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); 01563 }
| void Ivy_FraigSavePattern3 | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
Definition at line 1576 of file ivyFraig.c.
01577 { 01578 Ivy_Obj_t * pObj; 01579 int i; 01580 for ( i = 0; i < p->nPatWords; i++ ) 01581 p->pPatWords[i] = Ivy_ObjRandomSim(); 01582 Vec_PtrForEachEntry( p->vPiVars, pObj, i ) 01583 if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) ) 01584 Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 ); 01585 }
| int Ivy_FraigSelectBestPat | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Selects the best pattern.]
Description [Returns 1 if such pattern is found.]
SideEffects []
SeeAlso []
Definition at line 1697 of file ivyFraig.c.
01698 { 01699 Ivy_FraigSim_t * pSims; 01700 Ivy_Obj_t * pObj; 01701 int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1; 01702 for ( i = 1; i < nLimit; i++ ) 01703 { 01704 if ( MaxScore < p->pPatScores[i] ) 01705 { 01706 MaxScore = p->pPatScores[i]; 01707 BestPat = i; 01708 } 01709 } 01710 if ( MaxScore == 0 ) 01711 return 0; 01712 // if ( MaxScore > p->pParams->MaxScore ) 01713 // printf( "Max score is %3d. ", MaxScore ); 01714 // copy the best pattern into the selected pattern 01715 memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); 01716 Ivy_ManForEachPi( p->pManAig, pObj, i ) 01717 { 01718 pSims = Ivy_ObjSim(pObj); 01719 if ( Ivy_InfoHasBit(pSims->pData, BestPat) ) 01720 Ivy_InfoSetBit(p->pPatWords, i); 01721 } 01722 return MaxScore; 01723 }
| int Ivy_FraigSetActivityFactors | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pOld, | |||
| Ivy_Obj_t * | pNew | |||
| ) | [static] |
Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
Definition at line 2580 of file ivyFraig.c.
02581 { 02582 int clk, LevelMin, LevelMax; 02583 assert( pOld || pNew ); 02584 clk = clock(); 02585 // reset the active variables 02586 veci_resize(&p->pSat->act_vars, 0); 02587 // prepare for traversal 02588 Ivy_ManIncrementTravId( p->pManFraig ); 02589 // determine the min and max level to visit 02590 assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 ); 02591 LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); 02592 LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio)); 02593 // traverse 02594 if ( pOld && !Ivy_ObjIsConst1(pOld) ) 02595 Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax ); 02596 if ( pNew && !Ivy_ObjIsConst1(pNew) ) 02597 Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax ); 02598 //Ivy_FraigPrintActivity( p ); 02599 p->timeTrav += clock() - clk; 02600 return 1; 02601 }
| int Ivy_FraigSetActivityFactors_rec | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| int | LevelMin, | |||
| int | LevelMax | |||
| ) |
Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
Definition at line 2544 of file ivyFraig.c.
02545 { 02546 Vec_Ptr_t * vFanins; 02547 Ivy_Obj_t * pFanin; 02548 int i, Counter = 0; 02549 assert( !Ivy_IsComplement(pObj) ); 02550 assert( Ivy_ObjSatNum(pObj) ); 02551 // skip visited variables 02552 if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) ) 02553 return 0; 02554 Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj); 02555 // add the PI to the list 02556 if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) ) 02557 return 0; 02558 // set the factor of this variable 02559 // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump 02560 p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin); 02561 veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj)); 02562 // explore the fanins 02563 vFanins = Ivy_ObjFaninVec( pObj ); 02564 Vec_PtrForEachEntry( vFanins, pFanin, i ) 02565 Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax ); 02566 return 1 + Counter; 02567 }
| void Ivy_FraigSimulate | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Performs simulation of the manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 1599 of file ivyFraig.c.
01600 { 01601 int nChanges, nClasses; 01602 // start the classes 01603 Ivy_FraigAssignRandom( p ); 01604 Ivy_FraigSimulateOne( p ); 01605 Ivy_FraigCreateClasses( p ); 01606 //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) ); 01607 // refine classes by walking 0/1 patterns 01608 Ivy_FraigSavePattern0( p ); 01609 Ivy_FraigAssignDist1( p, p->pPatWords ); 01610 Ivy_FraigSimulateOne( p ); 01611 nChanges = Ivy_FraigRefineClasses( p ); 01612 if ( p->pManFraig->pData ) 01613 return; 01614 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); 01615 Ivy_FraigSavePattern1( p ); 01616 Ivy_FraigAssignDist1( p, p->pPatWords ); 01617 Ivy_FraigSimulateOne( p ); 01618 nChanges = Ivy_FraigRefineClasses( p ); 01619 if ( p->pManFraig->pData ) 01620 return; 01621 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); 01622 // refine classes by random simulation 01623 do { 01624 Ivy_FraigAssignRandom( p ); 01625 Ivy_FraigSimulateOne( p ); 01626 nClasses = p->lClasses.nItems; 01627 nChanges = Ivy_FraigRefineClasses( p ); 01628 if ( p->pManFraig->pData ) 01629 return; 01630 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); 01631 } while ( (double)nChanges / nClasses > p->pParams->dSimSatur ); 01632 // Ivy_FraigPrintSimClasses( p ); 01633 }
| void Ivy_FraigSimulateOne | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
Definition at line 980 of file ivyFraig.c.
00981 { 00982 Ivy_Obj_t * pObj; 00983 int i, clk; 00984 clk = clock(); 00985 Ivy_ManForEachNode( p->pManAig, pObj, i ) 00986 { 00987 Ivy_NodeSimulate( p, pObj ); 00988 /* 00989 if ( Ivy_ObjFraig(pObj) == NULL ) 00990 printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase ); 00991 else 00992 printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase ); 00993 Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 ); 00994 printf( "\n" ); 00995 */ 00996 } 00997 p->timeSim += clock() - clk; 00998 p->nSimRounds++; 00999 }
| void Ivy_FraigSimulateOneSim | ( | Ivy_FraigMan_t * | p | ) |
Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
Definition at line 1012 of file ivyFraig.c.
01013 { 01014 Ivy_FraigSim_t * pSims; 01015 int clk; 01016 clk = clock(); 01017 for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext ) 01018 Ivy_NodeSimulateSim( p, pSims ); 01019 p->timeSim += clock() - clk; 01020 p->nSimRounds++; 01021 }
| Ivy_FraigMan_t * Ivy_FraigStart | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) | [static] |
Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 544 of file ivyFraig.c.
00545 { 00546 Ivy_FraigMan_t * p; 00547 Ivy_FraigSim_t * pSims; 00548 Ivy_Obj_t * pObj; 00549 int i, k, EntrySize; 00550 // clean the fanout representation 00551 Ivy_ManForEachObj( pManAig, pObj, i ) 00552 // pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; 00553 assert( !pObj->pEquiv && !pObj->pFanout ); 00554 // allocat the fraiging manager 00555 p = ALLOC( Ivy_FraigMan_t, 1 ); 00556 memset( p, 0, sizeof(Ivy_FraigMan_t) ); 00557 p->pParams = pParams; 00558 p->pManAig = pManAig; 00559 p->pManFraig = Ivy_ManStartFrom( pManAig ); 00560 // allocate simulation info 00561 p->nSimWords = pParams->nSimWords; 00562 // p->pSimWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 00563 EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords; 00564 p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize ); 00565 memset( p->pSimWords, 0, EntrySize ); 00566 k = 0; 00567 Ivy_ManForEachObj( pManAig, pObj, i ) 00568 { 00569 pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++); 00570 pSims->pNext = NULL; 00571 if ( Ivy_ObjIsNode(pObj) ) 00572 { 00573 if ( p->pSimStart == NULL ) 00574 p->pSimStart = pSims; 00575 else 00576 ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims; 00577 pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) ); 00578 pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) ); 00579 pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase; 00580 } 00581 else 00582 { 00583 pSims->pFanin0 = NULL; 00584 pSims->pFanin1 = NULL; 00585 pSims->Type = 0; 00586 } 00587 Ivy_ObjSetSim( pObj, pSims ); 00588 } 00589 assert( k == Ivy_ManObjNum(pManAig) ); 00590 // allocate storage for sim pattern 00591 p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); 00592 p->pPatWords = ALLOC( unsigned, p->nPatWords ); 00593 p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 00594 p->vPiVars = Vec_PtrAlloc( 100 ); 00595 // set random number generator 00596 srand( 0xABCABC ); 00597 return p; 00598 }
| Ivy_FraigMan_t * Ivy_FraigStartSimple | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) | [static] |
Function*************************************************************
Synopsis [Starts the fraiging manager without simulation info.]
Description []
SideEffects []
SeeAlso []
Definition at line 520 of file ivyFraig.c.
00521 { 00522 Ivy_FraigMan_t * p; 00523 // allocat the fraiging manager 00524 p = ALLOC( Ivy_FraigMan_t, 1 ); 00525 memset( p, 0, sizeof(Ivy_FraigMan_t) ); 00526 p->pParams = pParams; 00527 p->pManAig = pManAig; 00528 p->pManFraig = Ivy_ManStartFrom( pManAig ); 00529 p->vPiVars = Vec_PtrAlloc( 100 ); 00530 return p; 00531 }
| void Ivy_FraigStop | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 611 of file ivyFraig.c.
00612 { 00613 if ( p->pParams->fVerbose ) 00614 Ivy_FraigPrint( p ); 00615 if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); 00616 if ( p->pSat ) sat_solver_delete( p->pSat ); 00617 FREE( p->pPatScores ); 00618 FREE( p->pPatWords ); 00619 FREE( p->pSimWords ); 00620 free( p ); 00621 }
| void Ivy_FraigSweep | ( | Ivy_FraigMan_t * | p | ) | [static] |
Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 1943 of file ivyFraig.c.
01944 { 01945 Ivy_Obj_t * pObj;//, * pTemp; 01946 int i, k = 0; 01947 p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0; 01948 p->nClassesBeg = p->lClasses.nItems; 01949 // duplicate internal nodes 01950 p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) ); 01951 Ivy_ManForEachNode( p->pManAig, pObj, i ) 01952 { 01953 Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); 01954 // default to simple strashing if simulation detected a counter-example for a PO 01955 if ( p->pManFraig->pData ) 01956 pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); 01957 else 01958 pObj->pEquiv = Ivy_FraigAnd( p, pObj ); 01959 assert( pObj->pEquiv != NULL ); 01960 // pTemp = Ivy_Regular(pObj->pEquiv); 01961 // assert( Ivy_Regular(pObj->pEquiv)->Type ); 01962 } 01963 Extra_ProgressBarStop( p->pProgress ); 01964 p->nClassesEnd = p->lClasses.nItems; 01965 // try to prove the outputs of the miter 01966 p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig); 01967 // Ivy_FraigMiterStatus( p->pManFraig ); 01968 if ( p->pParams->fProve && p->pManFraig->pData == NULL ) 01969 Ivy_FraigMiterProve( p ); 01970 // add the POs 01971 Ivy_ManForEachPo( p->pManAig, pObj, i ) 01972 Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); 01973 // clean the old manager 01974 Ivy_ManForEachObj( p->pManAig, pObj, i ) 01975 pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; 01976 // clean the new manager 01977 Ivy_ManForEachObj( p->pManFraig, pObj, i ) 01978 { 01979 if ( Ivy_ObjFaninVec(pObj) ) 01980 Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); 01981 pObj->pNextFan0 = pObj->pNextFan1 = NULL; 01982 } 01983 // remove dangling nodes 01984 Ivy_ManCleanup( p->pManFraig ); 01985 // clean up the class marks 01986 Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj ) 01987 pObj->fMarkA = 0; 01988 }
Function*************************************************************
Synopsis [Adds one node to the equivalence class.]
Description []
SideEffects []
SeeAlso []
Definition at line 1034 of file ivyFraig.c.
01035 { 01036 if ( Ivy_ObjClassNodeNext(pClass) == NULL ) 01037 Ivy_ObjSetClassNodeNext( pClass, pObj ); 01038 else 01039 Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj ); 01040 Ivy_ObjSetClassNodeLast( pClass, pObj ); 01041 Ivy_ObjSetClassNodeRepr( pObj, pClass ); 01042 Ivy_ObjSetClassNodeNext( pObj, NULL ); 01043 }
| void Ivy_NodeAssignConst | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| int | fConst1 | |||
| ) |
Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
Definition at line 691 of file ivyFraig.c.
00692 { 00693 Ivy_FraigSim_t * pSims; 00694 int i; 00695 assert( Ivy_ObjIsPi(pObj) ); 00696 pSims = Ivy_ObjSim(pObj); 00697 for ( i = 0; i < p->nSimWords; i++ ) 00698 pSims->pData[i] = fConst1? ~(unsigned)0 : 0; 00699 }
| void Ivy_NodeAssignRandom | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
Definition at line 670 of file ivyFraig.c.
00671 { 00672 Ivy_FraigSim_t * pSims; 00673 int i; 00674 assert( Ivy_ObjIsPi(pObj) ); 00675 pSims = Ivy_ObjSim(pObj); 00676 for ( i = 0; i < p->nSimWords; i++ ) 00677 pSims->pData[i] = Ivy_ObjRandomSim(); 00678 }
| int Ivy_NodeCompareSims | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj0, | |||
| Ivy_Obj_t * | pObj1 | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
Definition at line 800 of file ivyFraig.c.
00801 { 00802 Ivy_FraigSim_t * pSims0, * pSims1; 00803 int i; 00804 pSims0 = Ivy_ObjSim(pObj0); 00805 pSims1 = Ivy_ObjSim(pObj1); 00806 for ( i = 0; i < p->nSimWords; i++ ) 00807 if ( pSims0->pData[i] != pSims1->pData[i] ) 00808 return 0; 00809 return 1; 00810 }
| void Ivy_NodeComplementSim | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
Definition at line 780 of file ivyFraig.c.
00781 { 00782 Ivy_FraigSim_t * pSims; 00783 int i; 00784 pSims = Ivy_ObjSim(pObj); 00785 for ( i = 0; i < p->nSimWords; i++ ) 00786 pSims->pData[i] = ~pSims->pData[i]; 00787 }
| unsigned Ivy_NodeHash | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Computes hash value using simulation info.]
Description []
SideEffects []
SeeAlso []
Definition at line 941 of file ivyFraig.c.
00942 { 00943 static int s_FPrimes[128] = { 00944 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 00945 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 00946 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 00947 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 00948 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 00949 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 00950 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 00951 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 00952 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 00953 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 00954 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 00955 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 00956 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 00957 }; 00958 Ivy_FraigSim_t * pSims; 00959 unsigned uHash; 00960 int i; 00961 assert( p->nSimWords <= 128 ); 00962 uHash = 0; 00963 pSims = Ivy_ObjSim(pObj); 00964 for ( i = 0; i < p->nSimWords; i++ ) 00965 uHash ^= pSims->pData[i] * s_FPrimes[i]; 00966 return uHash; 00967 }
| int Ivy_NodeHasZeroSim | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
Definition at line 758 of file ivyFraig.c.
00759 { 00760 Ivy_FraigSim_t * pSims; 00761 int i; 00762 pSims = Ivy_ObjSim(pObj); 00763 for ( i = 0; i < p->nSimWords; i++ ) 00764 if ( pSims->pData[i] ) 00765 return 0; 00766 return 1; 00767 }
| void Ivy_NodeSimulate | ( | Ivy_FraigMan_t * | p, | |
| Ivy_Obj_t * | pObj | |||
| ) |
Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 878 of file ivyFraig.c.
00879 { 00880 Ivy_FraigSim_t * pSims, * pSims0, * pSims1; 00881 int fCompl, fCompl0, fCompl1, i; 00882 assert( !Ivy_IsComplement(pObj) ); 00883 // get hold of the simulation information 00884 pSims = Ivy_ObjSim(pObj); 00885 pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj)); 00886 pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj)); 00887 // get complemented attributes of the children using their random info 00888 fCompl = pObj->fPhase; 00889 fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)); 00890 fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)); 00891 // simulate 00892 if ( fCompl0 && fCompl1 ) 00893 { 00894 if ( fCompl ) 00895 for ( i = 0; i < p->nSimWords; i++ ) 00896 pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]); 00897 else 00898 for ( i = 0; i < p->nSimWords; i++ ) 00899 pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]); 00900 } 00901 else if ( fCompl0 && !fCompl1 ) 00902 { 00903 if ( fCompl ) 00904 for ( i = 0; i < p->nSimWords; i++ ) 00905 pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]); 00906 else 00907 for ( i = 0; i < p->nSimWords; i++ ) 00908 pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]); 00909 } 00910 else if ( !fCompl0 && fCompl1 ) 00911 { 00912 if ( fCompl ) 00913 for ( i = 0; i < p->nSimWords; i++ ) 00914 pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]); 00915 else 00916 for ( i = 0; i < p->nSimWords; i++ ) 00917 pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]); 00918 } 00919 else // if ( !fCompl0 && !fCompl1 ) 00920 { 00921 if ( fCompl ) 00922 for ( i = 0; i < p->nSimWords; i++ ) 00923 pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]); 00924 else 00925 for ( i = 0; i < p->nSimWords; i++ ) 00926 pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]); 00927 } 00928 }
| void Ivy_NodeSimulateSim | ( | Ivy_FraigMan_t * | p, | |
| Ivy_FraigSim_t * | pSims | |||
| ) |
Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 823 of file ivyFraig.c.
00824 { 00825 unsigned * pData, * pData0, * pData1; 00826 int i; 00827 pData = pSims->pData; 00828 pData0 = pSims->pFanin0->pData; 00829 pData1 = pSims->pFanin1->pData; 00830 switch( pSims->Type ) 00831 { 00832 case 0: 00833 for ( i = 0; i < p->nSimWords; i++ ) 00834 pData[i] = (pData0[i] & pData1[i]); 00835 break; 00836 case 1: 00837 for ( i = 0; i < p->nSimWords; i++ ) 00838 pData[i] = ~(pData0[i] & pData1[i]); 00839 break; 00840 case 2: 00841 for ( i = 0; i < p->nSimWords; i++ ) 00842 pData[i] = (pData0[i] & ~pData1[i]); 00843 break; 00844 case 3: 00845 for ( i = 0; i < p->nSimWords; i++ ) 00846 pData[i] = (~pData0[i] | pData1[i]); 00847 break; 00848 case 4: 00849 for ( i = 0; i < p->nSimWords; i++ ) 00850 pData[i] = (~pData0[i] & pData1[i]); 00851 break; 00852 case 5: 00853 for ( i = 0; i < p->nSimWords; i++ ) 00854 pData[i] = (pData0[i] | ~pData1[i]); 00855 break; 00856 case 6: 00857 for ( i = 0; i < p->nSimWords; i++ ) 00858 pData[i] = ~(pData0[i] | pData1[i]); 00859 break; 00860 case 7: 00861 for ( i = 0; i < p->nSimWords; i++ ) 00862 pData[i] = (pData0[i] | pData1[i]); 00863 break; 00864 } 00865 }
Definition at line 137 of file ivyFraig.c.
00137 { return pObj->pNextFan0; }
Definition at line 139 of file ivyFraig.c.
00139 { return pObj->pNextFan1; }
Definition at line 138 of file ivyFraig.c.
00138 { return pObj->pNextFan0; }
Definition at line 141 of file ivyFraig.c.
00141 { return pObj->pPrevFan0; }
Definition at line 142 of file ivyFraig.c.
00142 { return pObj->pPrevFan1; }
Definition at line 145 of file ivyFraig.c.
Definition at line 143 of file ivyFraig.c.
00143 { return pObj->pEquiv; }
Definition at line 140 of file ivyFraig.c.
00140 { return pObj->pPrevFan0; }
| static unsigned Ivy_ObjRandomSim | ( | ) | [inline, static] |
Definition at line 158 of file ivyFraig.c.
| static int Ivy_ObjSatNum | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 144 of file ivyFraig.c.
00144 { return (int)pObj->pNextFan0; }
Definition at line 148 of file ivyFraig.c.
00148 { pObj->pNextFan0 = pLast; }
Definition at line 150 of file ivyFraig.c.
00150 { pObj->pNextFan1 = pNext; }
Definition at line 149 of file ivyFraig.c.
00149 { pObj->pNextFan0 = pRepr; }
Definition at line 152 of file ivyFraig.c.
00152 { pObj->pPrevFan0 = pNext; }
Definition at line 153 of file ivyFraig.c.
00153 { pObj->pPrevFan1 = pPrev; }
Definition at line 156 of file ivyFraig.c.
Definition at line 154 of file ivyFraig.c.
00154 { pObj->pEquiv = pNode; }
Definition at line 151 of file ivyFraig.c.
00151 { pObj->pPrevFan0 = pNext; }
| static void Ivy_ObjSetSatNum | ( | Ivy_Obj_t * | pObj, | |
| int | Num | |||
| ) | [inline, static] |
Definition at line 155 of file ivyFraig.c.
| static void Ivy_ObjSetSim | ( | Ivy_Obj_t * | pObj, | |
| Ivy_FraigSim_t * | pSim | |||
| ) | [inline, static] |
Definition at line 147 of file ivyFraig.c.
| static Ivy_FraigSim_t* Ivy_ObjSim | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 136 of file ivyFraig.c.
00136 { return (Ivy_FraigSim_t *)pObj->pFanout; }
Variable Documentation
sint64 s_nBTLimitGlobal = 0 [static] |
Definition at line 202 of file ivyFraig.c.
sint64 s_nInsLimitGlobal = 0 [static] |
Definition at line 203 of file ivyFraig.c.
