/**CFile**************************************************************** FileName [abcDetect.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] Synopsis [Detect conditions.] Author [Alan Mishchenko, Dao Ai Quoc] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 7, 2016.] Revision [$Id: abcDetect.c,v 1.00 2016/06/07 00:00:00 alanmi Exp $] ***********************************************************************/ #include "base/abc/abc.h" #include "misc/vec/vecHsh.h" #include "misc/util/utilNam.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "map/mio/mio.h" #include "map/mio/exp.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef enum { ABC_FIN_NONE = -100, // 0: unknown ABC_FIN_SA0, // 1: ABC_FIN_SA1, // 2: ABC_FIN_NEG, // 3: ABC_FIN_RDOB_AND, // 4: ABC_FIN_RDOB_NAND, // 5: ABC_FIN_RDOB_OR, // 6: ABC_FIN_RDOB_NOR, // 7: ABC_FIN_RDOB_XOR, // 8: ABC_FIN_RDOB_NXOR, // 9: ABC_FIN_RDOB_NOT, // 10: ABC_FIN_RDOB_BUFF, // 11: ABC_FIN_RDOB_LAST // 12: } Abc_FinType_t; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Generates fault list for the given mapped network.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt ) { Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; Mio_Gate_t * pGate; Abc_Obj_t * pObj; int i, Count = 1; FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } assert( Abc_NtkIsMappedLogic(pNtk) ); Abc_NtkForEachNode( pNtk, pObj, i ) { Mio_Gate_t * pGateObj = (Mio_Gate_t *)pObj->pData; int nInputs = Mio_GateReadPinNum(pGateObj); // add basic faults (SA0, SA1, NEG) fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA0" ), Count++; fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA1" ), Count++; fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "NEG" ), Count++; if ( fStuckAt ) continue; // add other faults, which correspond to changing the given gate // by another gate with the same support-size from the same library Mio_LibraryForEachGate( pLib, pGate ) if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs ) fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++; } printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d %sfaults.\n", pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1, fStuckAt ? "stuck-at ":"" ); fclose( pFile ); } /**Function************************************************************* Synopsis [Recognize type.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Io_ReadFinTypeMapped( Mio_Library_t * pLib, char * pThis ) { Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pThis, NULL ); if ( pGate == NULL ) { printf( "Cannot find gate \"%s\" in the current library.\n", pThis ); return ABC_FIN_NONE; } return Mio_GateReadCell( pGate ); } int Io_ReadFinType( char * pThis ) { if ( !strcmp(pThis, "SA0") ) return ABC_FIN_SA0; if ( !strcmp(pThis, "SA1") ) return ABC_FIN_SA1; if ( !strcmp(pThis, "NEG") ) return ABC_FIN_NEG; if ( !strcmp(pThis, "RDOB_AND") ) return ABC_FIN_RDOB_AND; if ( !strcmp(pThis, "RDOB_NAND") ) return ABC_FIN_RDOB_NAND; if ( !strcmp(pThis, "RDOB_OR") ) return ABC_FIN_RDOB_OR; if ( !strcmp(pThis, "RDOB_NOR") ) return ABC_FIN_RDOB_NOR; if ( !strcmp(pThis, "RDOB_XOR") ) return ABC_FIN_RDOB_XOR; if ( !strcmp(pThis, "RDOB_NXOR") ) return ABC_FIN_RDOB_NXOR; if ( !strcmp(pThis, "RDOB_NOT") ) return ABC_FIN_RDOB_NOT; if ( !strcmp(pThis, "RDOB_BUFF") ) return ABC_FIN_RDOB_BUFF; return ABC_FIN_NONE; } char * Io_WriteFinType( int Type ) { if ( Type == ABC_FIN_SA0 ) return "SA0"; if ( Type == ABC_FIN_SA1 ) return "SA1"; if ( Type == ABC_FIN_NEG ) return "NEG"; if ( Type == ABC_FIN_RDOB_AND ) return "RDOB_AND" ; if ( Type == ABC_FIN_RDOB_NAND ) return "RDOB_NAND"; if ( Type == ABC_FIN_RDOB_OR ) return "RDOB_OR" ; if ( Type == ABC_FIN_RDOB_NOR ) return "RDOB_NOR" ; if ( Type == ABC_FIN_RDOB_XOR ) return "RDOB_XOR" ; if ( Type == ABC_FIN_RDOB_NXOR ) return "RDOB_NXOR"; if ( Type == ABC_FIN_RDOB_NOT ) return "RDOB_NOT" ; if ( Type == ABC_FIN_RDOB_BUFF ) return "RDOB_BUFF"; return "Unknown"; } /**Function************************************************************* Synopsis [Read information from file.] Description [Returns information as a set of pairs: (ObjId, TypeId). Uses the current network to map ObjName given in the file into ObjId.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose ) { Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; char Buffer[1000]; Abc_Obj_t * pObj; Abc_Nam_t * pNam; Vec_Int_t * vMap; Vec_Int_t * vPairs = NULL; int i, Type, iObj, fFound, nLines = 1; FILE * pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) { printf( "Cannot open input file \"%s\" for reading.\n", pFileName ); return NULL; } // map CI/node names into their IDs pNam = Abc_NamStart( 1000, 10 ); vMap = Vec_IntAlloc( 1000 ); Vec_IntPush( vMap, -1 ); Abc_NtkForEachObj( pNtk, pObj, i ) { if ( !Abc_ObjIsCi(pObj) && !Abc_ObjIsNode(pObj) ) continue; Abc_NamStrFindOrAdd( pNam, Abc_ObjName(pObj), &fFound ); if ( fFound ) { printf( "The same name \"%s\" appears twice among CIs and internal nodes.\n", Abc_ObjName(pObj) ); goto finish; } Vec_IntPush( vMap, Abc_ObjId(pObj) ); } assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) ); // read file lines vPairs = Vec_IntAlloc( 1000 ); Vec_IntPushTwo( vPairs, -1, -1 ); while ( fgets(Buffer, 1000, pFile) != NULL ) { // read line number char * pToken = strtok( Buffer, " \n\r\t" ); if ( pToken == NULL ) break; if ( nLines++ != atoi(pToken) ) { printf( "Line numbers are not consecutive. Quitting.\n" ); Vec_IntFreeP( &vPairs ); goto finish; } // read object name and find its ID pToken = strtok( NULL, " \n\r\t" ); iObj = Abc_NamStrFind( pNam, pToken ); if ( !iObj ) { printf( "Cannot find object with name \"%s\".\n", pToken ); continue; } // read type pToken = strtok( NULL, " \n\r\t" ); if ( Abc_NtkIsMappedLogic(pNtk) ) { if ( !strcmp(pToken, "SA0") || !strcmp(pToken, "SA1") || !strcmp(pToken, "NEG") ) Type = Io_ReadFinType( pToken ); else Type = Io_ReadFinTypeMapped( pLib, pToken ); } else Type = Io_ReadFinType( pToken ); if ( Type == ABC_FIN_NONE ) { printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); continue; } Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type ); } assert( Vec_IntSize(vPairs) == 2 * nLines ); printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName ); // verify the reader by printing the results if ( fVerbose ) Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 ) printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) ); finish: Vec_IntFree( vMap ); Abc_NamDeref( pNam ); fclose( pFile ); return vPairs; } /**Function************************************************************* Synopsis [Extend the network by adding second timeframe.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkFrameExtend( Abc_Ntk_t * pNtk ) { Vec_Ptr_t * vFanins, * vNodes; Abc_Obj_t * pObj, * pFanin, * pReset, * pEnable, * pSignal; Abc_Obj_t * pResetN, * pEnableN, * pAnd0, * pAnd1, * pMux; int i, k, iStartPo, nPisOld = Abc_NtkPiNum(pNtk), nPosOld = Abc_NtkPoNum(pNtk); // skip if there are no flops if ( pNtk->nConstrs == 0 ) return; assert( Abc_NtkPiNum(pNtk) >= pNtk->nConstrs ); assert( Abc_NtkPoNum(pNtk) >= pNtk->nConstrs * 4 ); // collect nodes vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) ); Abc_NtkForEachNode( pNtk, pObj, i ) Vec_PtrPush( vNodes, pObj ); // duplicate PIs vFanins = Vec_PtrAlloc( 2 ); Abc_NtkForEachPi( pNtk, pObj, i ) { if ( i == nPisOld ) break; if ( i < nPisOld - pNtk->nConstrs ) { Abc_NtkDupObj( pNtk, pObj, 0 ); Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" ); continue; } // create flop input iStartPo = nPosOld + 4 * (i - nPisOld); pReset = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 1 ) ); pEnable = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 2 ) ); pSignal = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 3 ) ); pResetN = Abc_NtkCreateNodeInv( pNtk, pReset ); pEnableN = Abc_NtkCreateNodeInv( pNtk, pEnable ); Vec_PtrFillTwo( vFanins, 2, pEnableN, pObj ); pAnd0 = Abc_NtkCreateNodeAnd( pNtk, vFanins ); Vec_PtrFillTwo( vFanins, 2, pEnable, pSignal ); pAnd1 = Abc_NtkCreateNodeAnd( pNtk, vFanins ); Vec_PtrFillTwo( vFanins, 2, pAnd0, pAnd1 ); pMux = Abc_NtkCreateNodeOr( pNtk, vFanins ); Vec_PtrFillTwo( vFanins, 2, pResetN, pMux ); pObj->pCopy = Abc_NtkCreateNodeAnd( pNtk, vFanins ); } // duplicate internal nodes Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) Abc_NtkDupObj( pNtk, pObj, 0 ); // connect objects Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); // create new POs and reconnect flop inputs Abc_NtkForEachPo( pNtk, pObj, i ) { if ( i == nPosOld ) break; if ( i < nPosOld - 4 * pNtk->nConstrs ) { Abc_NtkDupObj( pNtk, pObj, 0 ); Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" ); Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy ); continue; } Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Abc_ObjFanin0(pObj)->pCopy ); } Vec_PtrFree( vFanins ); Vec_PtrFree( vNodes ); } /**Function************************************************************* Synopsis [Detect equivalence classes of nodes in terms of their TFO.] Description [Given is the logic network (pNtk) and the set of objects (primary inputs or internal nodes) to be considered (vObjs), this function returns a set of equivalence classes of these objects in terms of their transitive fanout (TFO). Two objects belong to the same class if the set of COs they feed into are the same.] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkDetectObjClasses_rec( Abc_Obj_t * pObj, Vec_Int_t * vMap, Hsh_VecMan_t * pHash, Vec_Int_t * vTemp ) { Vec_Int_t * vArray, * vSet; Abc_Obj_t * pNext; int i; // get the CO set for this object int Entry = Vec_IntEntry(vMap, Abc_ObjId(pObj)); if ( Entry != -1 ) // the set is already computed return Entry; // compute a new CO set assert( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) ); // if there is no fanouts, the set of COs is empty if ( Abc_ObjFanoutNum(pObj) == 0 ) { Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), 0 ); return 0; } // compute the set for the first fanout Entry = Abc_NtkDetectObjClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp ); if ( Abc_ObjFanoutNum(pObj) == 1 ) { Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry ); return Entry; } vSet = Vec_IntAlloc( 16 ); // initialize the set with that of first fanout vArray = Hsh_VecReadEntry( pHash, Entry ); Vec_IntClear( vSet ); Vec_IntAppend( vSet, vArray ); // iteratively add sets of other fanouts Abc_ObjForEachFanout( pObj, pNext, i ) { if ( i == 0 ) continue; Entry = Abc_NtkDetectObjClasses_rec( pNext, vMap, pHash, vTemp ); vArray = Hsh_VecReadEntry( pHash, Entry ); Vec_IntTwoMerge2( vSet, vArray, vTemp ); ABC_SWAP( Vec_Int_t, *vSet, *vTemp ); } // create or find new set and map the object into it Entry = Hsh_VecManAdd( pHash, vSet ); Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry ); Vec_IntFree( vSet ); return Entry; } Vec_Wec_t * Abc_NtkDetectObjClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs, Vec_Wec_t ** pvCos ) { Vec_Wec_t * vClasses; // classes of equivalence objects from vObjs Vec_Int_t * vClassMap; // mapping of each CO set into its class in vClasses Vec_Int_t * vClass; // one equivalence class Abc_Obj_t * pObj; int i, iObj, SetId, ClassId; // create hash table to hash sets of CO indexes Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000 ); // create elementary sets (each composed of one CO) and map COs into them Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) ); Vec_Int_t * vSet = Vec_IntAlloc( 16 ); assert( Abc_NtkIsLogic(pNtk) ); // compute empty set SetId = Hsh_VecManAdd( pHash, vSet ); assert( SetId == 0 ); Abc_NtkForEachCo( pNtk, pObj, i ) { Vec_IntFill( vSet, 1, Abc_ObjId(pObj) ); SetId = Hsh_VecManAdd( pHash, vSet ); Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), SetId ); } // make sure the array of objects is sorted Vec_IntSort( vObjs, 0 ); // begin from the objects and map their IDs into sets of COs Abc_NtkForEachObjVec( vObjs, pNtk, pObj, i ) Abc_NtkDetectObjClasses_rec( pObj, vMap, pHash, vSet ); Vec_IntFree( vSet ); // create map for mapping CO set its their classes vClassMap = Vec_IntStartFull( Hsh_VecSize(pHash) + 1 ); // collect classes of objects vClasses = Vec_WecAlloc( 1000 ); Vec_IntForEachEntry( vObjs, iObj, i ) { //char * pName = Abc_ObjName( Abc_NtkObj(pNtk, iObj) ); // for a given object (iObj), find the ID of its COs set SetId = Vec_IntEntry( vMap, iObj ); assert( SetId >= 0 ); // for the given CO set, finds its equivalence class ClassId = Vec_IntEntry( vClassMap, SetId ); if ( ClassId == -1 ) // there is no equivalence class { // map this CO set into a new equivalence class Vec_IntWriteEntry( vClassMap, SetId, Vec_WecSize(vClasses) ); vClass = Vec_WecPushLevel( vClasses ); } else // get hold of the equivalence class vClass = Vec_WecEntry( vClasses, ClassId ); // add objects to the class Vec_IntPush( vClass, iObj ); // print the set for this object //printf( "Object %5d : ", iObj ); //Vec_IntPrint( Hsh_VecReadEntry(pHash, SetId) ); } // collect arrays of COs for each class *pvCos = Vec_WecStart( Vec_WecSize(vClasses) ); Vec_WecForEachLevel( vClasses, vClass, i ) { iObj = Vec_IntEntry( vClass, 0 ); // for a given object (iObj), find the ID of its COs set SetId = Vec_IntEntry( vMap, iObj ); assert( SetId >= 0 ); // for the given CO set ID, find the set vSet = Hsh_VecReadEntry( pHash, SetId ); Vec_IntAppend( Vec_WecEntry(*pvCos, i), vSet ); } Hsh_VecManStop( pHash ); Vec_IntFree( vClassMap ); Vec_IntFree( vMap ); return vClasses; } void Abc_NtkDetectClassesTest2( Abc_Ntk_t * pNtk, int fVerbose, int fVeryVerbose ) { Vec_Int_t * vObjs; Vec_Wec_t * vRes, * vCos; // for testing, create the set of object IDs for all combinational inputs (CIs) Abc_Obj_t * pObj; int i; vObjs = Vec_IntAlloc( Abc_NtkCiNum(pNtk) ); Abc_NtkForEachCi( pNtk, pObj, i ) Vec_IntPush( vObjs, Abc_ObjId(pObj) ); // compute equivalence classes of CIs and print them vRes = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCos ); Vec_WecPrint( vRes, 0 ); Vec_WecPrint( vCos, 0 ); // clean up Vec_IntFree( vObjs ); Vec_WecFree( vRes ); Vec_WecFree( vCos ); } /**Function************************************************************* Synopsis [Collecting objects.] Description [Collects combinational inputs (vCIs) and internal nodes (vNodes) reachable from the given set of combinational outputs (vCOs).] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkFinMiterCollect_rec( Abc_Obj_t * pObj, Vec_Int_t * vCis, Vec_Int_t * vNodes ) { if ( Abc_NodeIsTravIdCurrent(pObj) ) return; Abc_NodeSetTravIdCurrent(pObj); if ( Abc_ObjIsCi(pObj) ) Vec_IntPush( vCis, Abc_ObjId(pObj) ); else { Abc_Obj_t * pFanin; int i; assert( Abc_ObjIsNode( pObj ) ); Abc_ObjForEachFanin( pObj, pFanin, i ) Abc_NtkFinMiterCollect_rec( pFanin, vCis, vNodes ); Vec_IntPush( vNodes, Abc_ObjId(pObj) ); } } void Abc_NtkFinMiterCollect( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes ) { Abc_Obj_t * pObj; int i; Vec_IntClear( vCis ); Vec_IntClear( vNodes ); Abc_NtkIncrementTravId( pNtk ); Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) Abc_NtkFinMiterCollect_rec( Abc_ObjFanin0(pObj), vCis, vNodes ); } /**Function************************************************************* Synopsis [Simulates expression using given simulation info.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim ) { int i, w, nVars = Mio_GateReadPinNum(pGate); Vec_Int_t * vExpr = Mio_GateReadExpr( pGate ); assert( nVars <= 6 ); for ( w = 0; w < nWords; w++ ) { word uFanins[6]; for ( i = 0; i < nVars; i++ ) uFanins[i] = ppFaninSims[i][w]; pObjSim[w] = Exp_Truth6( nVars, vExpr, uFanins ); } } /**Function************************************************************* Synopsis [Simulates expression for one simulation pattern.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] ) { int nVars = Mio_GateReadPinNum(pGate); int i, iMint = 0; for ( i = 0; i < nVars; i++ ) if ( iBits[i] ) iMint |= (1 << i); return Abc_InfoHasBit( (unsigned *)Mio_GateReadTruthP(pGate), iMint ); } /**Function************************************************************* Synopsis [Simulated expression with one bit.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits ) { int i, nVars = Mio_GateReadPinNum(pGate); Vec_Int_t * vExpr = Mio_GateReadExpr( pGate ); if ( Exp_IsConst0(vExpr) ) return 0; if ( Exp_IsConst1(vExpr) ) return 1; if ( Exp_IsLit(vExpr) ) { int Index0 = Vec_IntEntry(vExpr,0) >> 1; int fCompl0 = Vec_IntEntry(vExpr,0) & 1; assert( Index0 < nVars ); return Abc_LitNotCond( iLits[Index0], fCompl0 ); } Vec_IntClear( vLits ); for ( i = 0; i < nVars; i++ ) Vec_IntPush( vLits, iLits[i] ); for ( i = 0; i < Exp_NodeNum(vExpr); i++ ) { int Index0 = Vec_IntEntry( vExpr, 2*i+0 ) >> 1; int Index1 = Vec_IntEntry( vExpr, 2*i+1 ) >> 1; int fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1; int fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1; Vec_IntPush( vLits, Gia_ManHashAnd( pGia, Abc_LitNotCond(Vec_IntEntry(vLits, Index0), fCompl0), Abc_LitNotCond(Vec_IntEntry(vLits, Index1), fCompl1) ) ); } return Abc_LitNotCond( Vec_IntEntryLast(vLits), Vec_IntEntryLast(vExpr) & 1 ); } /**Function************************************************************* Synopsis [AIG construction and simulation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Abc_NtkFinSimOneLit( Gia_Man_t * pNew, Abc_Obj_t * pObj, int Type, Vec_Int_t * vMap, int n, Vec_Int_t * vTemp ) { if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 ) { extern int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits ); Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc; int i, Lits[6]; for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) Lits[i] = Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId(pObj, i), n) ); return Mio_LibGateSimulateGia( pNew, Mio_LibraryReadGateById(pLib, Type), Lits, vTemp ); } else { int iLit0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId0(pObj), n) ) : -1; int iLit1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId1(pObj), n) ) : -1; assert( Type != ABC_FIN_NEG ); if ( Type == ABC_FIN_SA0 ) return 0; if ( Type == ABC_FIN_SA1 ) return 1; if ( Type == ABC_FIN_RDOB_BUFF ) return iLit0; if ( Type == ABC_FIN_RDOB_NOT ) return Abc_LitNot( iLit0 ); if ( Type == ABC_FIN_RDOB_AND ) return Gia_ManHashAnd( pNew, iLit0, iLit1 ); if ( Type == ABC_FIN_RDOB_OR ) return Gia_ManHashOr( pNew, iLit0, iLit1 ); if ( Type == ABC_FIN_RDOB_XOR ) return Gia_ManHashXor( pNew, iLit0, iLit1 ); if ( Type == ABC_FIN_RDOB_NAND ) return Abc_LitNot(Gia_ManHashAnd( pNew, iLit0, iLit1 )); if ( Type == ABC_FIN_RDOB_NOR ) return Abc_LitNot(Gia_ManHashOr( pNew, iLit0, iLit1 )); if ( Type == ABC_FIN_RDOB_NXOR ) return Abc_LitNot(Gia_ManHashXor( pNew, iLit0, iLit1 )); assert( 0 ); return -1; } } static inline int Abc_NtkFinSimOneBit( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords, int iBit ) { if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 ) { extern int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] ); Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc; int i, iBits[6]; for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) { word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) ); iBits[i] = Abc_InfoHasBit( (unsigned*)pSim0, iBit ); } return Mio_LibGateSimulateOne( Mio_LibraryReadGateById(pLib, Type), iBits ); } else { word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL; word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL; int iBit0 = Abc_ObjFaninNum(pObj) > 0 ? Abc_InfoHasBit( (unsigned*)pSim0, iBit ) : -1; int iBit1 = Abc_ObjFaninNum(pObj) > 1 ? Abc_InfoHasBit( (unsigned*)pSim1, iBit ) : -1; assert( Type != ABC_FIN_NEG ); if ( Type == ABC_FIN_SA0 ) return 0; if ( Type == ABC_FIN_SA1 ) return 1; if ( Type == ABC_FIN_RDOB_BUFF ) return iBit0; if ( Type == ABC_FIN_RDOB_NOT ) return !iBit0; if ( Type == ABC_FIN_RDOB_AND ) return iBit0 & iBit1; if ( Type == ABC_FIN_RDOB_OR ) return iBit0 | iBit1; if ( Type == ABC_FIN_RDOB_XOR ) return iBit0 ^ iBit1; if ( Type == ABC_FIN_RDOB_NAND ) return !(iBit0 & iBit1); if ( Type == ABC_FIN_RDOB_NOR ) return !(iBit0 | iBit1); if ( Type == ABC_FIN_RDOB_NXOR ) return !(iBit0 ^ iBit1); assert( 0 ); return -1; } } static inline void Abc_NtkFinSimOneWord( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords ) { if ( Abc_NtkIsMappedLogic(pObj->pNtk) ) { extern void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim ); word * ppSims[6]; int i; word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); assert( Type == -1 ); for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ ) ppSims[i] = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) ); Mio_LibGateSimulate( (Mio_Gate_t *)pObj->pData, ppSims, nWords, pSim ); } else { word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); int w; word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL; word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL; assert( Type != ABC_FIN_NEG ); if ( Type == ABC_FIN_SA0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = 0; else if ( Type == ABC_FIN_SA1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~((word)0); else if ( Type == ABC_FIN_RDOB_BUFF ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w]; else if ( Type == ABC_FIN_RDOB_NOT ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w]; else if ( Type == ABC_FIN_RDOB_AND ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w]; else if ( Type == ABC_FIN_RDOB_OR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] | pSim1[w]; else if ( Type == ABC_FIN_RDOB_XOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] ^ pSim1[w]; else if ( Type == ABC_FIN_RDOB_NAND ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] & pSim1[w]); else if ( Type == ABC_FIN_RDOB_NOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]); else if ( Type == ABC_FIN_RDOB_NXOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] ^ pSim1[w]); else assert( 0 ); } } // returns 1 if the functionality with indexes i1 and i2 is the same static inline int Abc_NtkFinCompareSimTwo( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Wrd_t * vSims, int nWords, int i1, int i2 ) { Abc_Obj_t * pObj; int i; assert( i1 != i2 ); Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) { word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ); if ( Abc_InfoHasBit((unsigned*)pSim0, i1) != Abc_InfoHasBit((unsigned*)pSim0, i2) ) return 0; } return 1; } Gia_Man_t * Abc_NtkFinMiterToGia( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, int iObjs[2], int Types[2], Vec_Int_t * vLits ) { Gia_Man_t * pNew = NULL, * pTemp; Abc_Obj_t * pObj; Vec_Int_t * vTemp = Vec_IntAlloc( 100 ); int n, i, Type, iMiter, iLit, * pLits; // create AIG manager pNew = Gia_ManStart( 1000 ); pNew->pName = Abc_UtilStrsav( pNtk->pName ); pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); Gia_ManHashStart( pNew ); // create inputs Abc_NtkForEachObjVec( vCis, pNtk, pObj, i ) { iLit = Gia_ManAppendCi(pNew); for ( n = 0; n < 2; n++ ) { if ( iObjs[n] != (int)Abc_ObjId(pObj) ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), iLit ); else if ( Types[n] != ABC_FIN_NEG ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) ); else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(iLit) ); } } // create internal nodes Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) { Type = Abc_NtkIsMappedLogic(pNtk) ? Mio_GateReadCell((Mio_Gate_t *)pObj->pData) : Vec_IntEntry(vTypes, Abc_ObjId(pObj)); for ( n = 0; n < 2; n++ ) { if ( iObjs[n] != (int)Abc_ObjId(pObj) ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp) ); else if ( Types[n] != ABC_FIN_NEG ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) ); else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG ) Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp)) ); } } // create comparator iMiter = 0; Abc_NtkForEachObjVec( vCos, pNtk, pObj, i ) { pLits = Vec_IntEntryP( vLits, Abc_Var2Lit(Abc_ObjFaninId0(pObj), 0) ); iLit = Gia_ManHashXor( pNew, pLits[0], pLits[1] ); iMiter = Gia_ManHashOr( pNew, iMiter, iLit ); } Gia_ManAppendCo( pNew, iMiter ); // perform cleanup pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); Vec_IntFree( vTemp ); return pNew; } void Abc_NtkFinSimulateOne( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, Vec_Wec_t * vMap2, Vec_Int_t * vPat, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vPairs, Vec_Wec_t * vRes, int iLevel, int iItem ) { Abc_Obj_t * pObj; Vec_Int_t * vClass, * vArray; int i, Counter = 0; int nItems = Vec_WecSizeSize(vRes); assert( nItems == Vec_WecSizeSize(vMap2) ); assert( nItems <= 128 * nWords ); // assign inputs assert( Vec_IntSize(vPat) == Vec_IntSize(vCis) ); Abc_NtkForEachObjVec( vCis, pNtk, pObj, i ) { int w, iObj = Abc_ObjId( pObj ); word Init = Vec_IntEntry(vPat, i) ? ~((word)0) : 0; word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); for ( w = 0; w < nWords; w++ ) pSim[w] = Init; vArray = Vec_WecEntry(vMap2, iObj); if ( Vec_IntSize(vArray) > 0 ) { int k, iFin, Index, iObj, Type; Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) { assert( Index < 64 ); iObj = Vec_IntEntry( vPairs, 2*iFin ); assert( iObj == (int)Abc_ObjId(pObj) ); Type = Vec_IntEntry( vPairs, 2*iFin+1 ); assert( Type == ABC_FIN_NEG || Type == ABC_FIN_SA0 || Type == ABC_FIN_SA1 ); if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) ) Abc_InfoXorBit( (unsigned *)pSim, Index ); Counter++; } } } // simulate internal nodes Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) { int iObj = Abc_ObjId( pObj ); int Type = Abc_NtkIsMappedLogic(pNtk) ? -1 : Vec_IntEntry( vTypes, iObj ); word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); Abc_NtkFinSimOneWord( pObj, Type, vSims, nWords ); vArray = Vec_WecEntry(vMap2, iObj); if ( Vec_IntSize(vArray) > 0 ) { int k, iFin, Index, iObj, Type; Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) { assert( Index < 64 * nWords ); iObj = Vec_IntEntry( vPairs, 2*iFin ); assert( iObj == (int)Abc_ObjId(pObj) ); Type = Vec_IntEntry( vPairs, 2*iFin+1 ); if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) ) Abc_InfoXorBit( (unsigned *)pSim, Index ); Counter++; } } } assert( nItems == 2*Counter ); // confirm no refinement Vec_WecForEachLevelStop( vRes, vClass, i, iLevel+1 ) { int k, iFin, Index, Value; int Index0 = Vec_IntEntry( vClass, 1 ); Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) { if ( i == iLevel && k/2 >= iItem ) break; //printf( "Double-checking pair %d and %d\n", iFin0, iFin ); Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index ); assert( Value ); // the same value } } // check refinement Vec_WecForEachLevelStart( vRes, vClass, i, iLevel ) { int k, iFin, Index, Value, Index0 = Vec_IntEntry(vClass, 1); int j = (i == iLevel) ? 2*iItem : 2; Vec_Int_t * vNewClass = NULL; Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, j ) { Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index ); if ( Value ) // the same value { Vec_IntWriteEntry( vClass, j++, iFin ); Vec_IntWriteEntry( vClass, j++, Index ); continue; } // create new class vNewClass = vNewClass ? vNewClass : Vec_WecPushLevel( vRes ); Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry vClass = Vec_WecEntry( vRes, i ); } Vec_IntShrink( vClass, j ); } } /**Function************************************************************* Synopsis [Check equivalence using SAT solver.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, int iObjs[2], int Types[2], Vec_Int_t * vLits ) { Gia_Man_t * pGia = Abc_NtkFinMiterToGia( pNtk, vTypes, vCos, vCis, vNodes, iObjs, Types, vLits ); if ( Gia_ManAndNum(pGia) == 0 && Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManCo(pGia, 0))) ) { Vec_Int_t * vPat = Gia_ObjFaninC0(Gia_ManCo(pGia, 0)) ? Vec_IntStart(Vec_IntSize(vCis)) : NULL; Gia_ManStop( pGia ); return vPat; } else { Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) { Gia_ManStop( pGia ); Cnf_DataFree( pCnf ); return NULL; } else { int i, nConfLimit = 10000; Vec_Int_t * vPat = NULL; int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0, 0 ); Gia_ManStop( pGia ); Cnf_DataFree( pCnf ); status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); if ( status == l_Undef ) vPat = Vec_IntAlloc(0); else if ( status == l_True ) { vPat = Vec_IntAlloc( Vec_IntSize(vCis) ); for ( i = 0; i < Vec_IntSize(vCis); i++ ) Vec_IntPush( vPat, sat_solver_var_value(pSat, iVarBeg+i) ); } //printf( "%d ", sat_solver_nconflicts(pSat) ); sat_solver_delete( pSat ); return vPat; } } } /**Function************************************************************* Synopsis [Refinement of equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkFinLocalSetup( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Int_t * vResArray ) { int i, iFin; Vec_IntClear( vResArray ); Vec_IntForEachEntry( vList, iFin, i ) { int iObj = Vec_IntEntry( vPairs, 2*iFin ); Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj ); Vec_IntPushTwo( vArray, iFin, i ); Vec_IntPushTwo( vResArray, iFin, i ); } } void Abc_NtkFinLocalSetdown( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2 ) { int i, iFin; Vec_IntForEachEntry( vList, iFin, i ) { int iObj = Vec_IntEntry( vPairs, 2*iFin ); Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj ); Vec_IntClear( vArray ); } } int Abc_NtkFinRefinement( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Wec_t * vResult ) { Vec_Wec_t * vRes = Vec_WecAlloc( 100 ); int nWords = Abc_Bit6WordNum( Vec_IntSize(vList) ); Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Abc_NtkObjNumMax(pNtk) ); // simulation info for each object Vec_Int_t * vLits = Vec_IntStart( 2*Abc_NtkObjNumMax(pNtk) ); // two literals for each object Vec_Int_t * vPat, * vClass, * vArray; int i, k, iFin, Index, nCalls = 0; // prepare vArray = Vec_WecPushLevel( vRes ); Abc_NtkFinLocalSetup( vPairs, vList, vMap2, vArray ); // try all-0/all-1 pattern for ( i = 0; i < 2; i++ ) { vPat = Vec_IntAlloc( Vec_IntSize(vCis) ); Vec_IntFill( vPat, Vec_IntSize(vCis), i ); Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, 0, 1 ); Vec_IntFree( vPat ); } // explore the classes //Vec_WecPrint( vRes, 0 ); Vec_WecForEachLevel( vRes, vClass, i ) { int iFin0 = Vec_IntEntry( vClass, 0 ); Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 ) { int Objs[2] = { Vec_IntEntry(vPairs, 2*iFin0), Vec_IntEntry(vPairs, 2*iFin) }; int Types[2] = { Vec_IntEntry(vPairs, 2*iFin0+1), Vec_IntEntry(vPairs, 2*iFin+1) }; nCalls++; //printf( "Checking pair %d and %d.\n", iFin0, iFin ); vPat = Abc_NtkFinCheckPair( pNtk, vTypes, vCos, vCis, vNodes, Objs, Types, vLits ); if ( vPat == NULL ) // proved continue; assert( Vec_IntEntry(vClass, k) == iFin ); if ( Vec_IntSize(vPat) == 0 ) { Vec_Int_t * vNewClass = Vec_WecPushLevel( vRes ); Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry vClass = Vec_WecEntry( vRes, i ); Vec_IntDrop( vClass, k+1 ); Vec_IntDrop( vClass, k ); } else // resimulate and refine Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, i, k/2 ); Vec_IntFree( vPat ); // make sure refinement happened (k'th entry is now absent or different) vClass = Vec_WecEntry( vRes, i ); assert( Vec_IntSize(vClass) <= k || Vec_IntEntry(vClass, k) != iFin ); k -= 2; //Vec_WecPrint( vRes, 0 ); } } // unprepare Abc_NtkFinLocalSetdown( vPairs, vList, vMap2 ); // reload proved equivs into the final array Vec_WecForEachLevel( vRes, vArray, i ) { assert( Vec_IntSize(vArray) % 2 == 0 ); if ( Vec_IntSize(vArray) <= 2 ) continue; vClass = Vec_WecPushLevel( vResult ); Vec_IntForEachEntryDouble( vArray, iFin, Index, k ) Vec_IntPush( vClass, iFin ); } Vec_WecFree( vRes ); Vec_WrdFree( vSims ); Vec_IntFree( vLits ); return nCalls; } /**Function************************************************************* Synopsis [Detecting classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Abc_ObjFinGateType( Abc_Obj_t * pNode ) { char * pSop = (char *)pNode->pData; if ( !strcmp(pSop, "1 1\n") ) return ABC_FIN_RDOB_BUFF; if ( !strcmp(pSop, "0 1\n") ) return ABC_FIN_RDOB_NOT; if ( !strcmp(pSop, "11 1\n") ) return ABC_FIN_RDOB_AND; if ( !strcmp(pSop, "11 0\n") ) return ABC_FIN_RDOB_NAND; if ( !strcmp(pSop, "00 0\n") ) return ABC_FIN_RDOB_OR; if ( !strcmp(pSop, "00 1\n") ) return ABC_FIN_RDOB_NOR; if ( !strcmp(pSop, "01 1\n10 1\n") ) return ABC_FIN_RDOB_XOR; if ( !strcmp(pSop, "11 1\n00 1\n") ) return ABC_FIN_RDOB_NXOR; return ABC_FIN_NONE; } int Abc_NtkFinCheckTypesOk( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; Abc_NtkForEachNode( pNtk, pObj, i ) if ( Abc_ObjFinGateType(pObj) == ABC_FIN_NONE ) return i; return 0; } int Abc_NtkFinCheckTypesOk2( Abc_Ntk_t * pNtk ) { Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc; int i, iObj, Type; Vec_IntForEachEntryDoubleStart( pNtk->vFins, iObj, Type, i, 2 ) { Abc_Obj_t * pObj = Abc_NtkObj( pNtk, iObj ); Mio_Gate_t * pGateFlt, * pGateObj = (Mio_Gate_t *)pObj->pData; if ( Type < 0 ) // SA0, SA1, NEG continue; pGateFlt = Mio_LibraryReadGateById( pLib, Type ); if ( Mio_GateReadPinNum(pGateFlt) < 1 ) continue; if ( Mio_GateReadPinNum(pGateObj) != Mio_GateReadPinNum(pGateFlt) ) return iObj; } return 0; } Vec_Int_t * Abc_NtkFinComputeTypes( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; Vec_Int_t * vObjs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachNode( pNtk, pObj, i ) Vec_IntWriteEntry( vObjs, Abc_ObjId(pObj), Abc_ObjFinGateType(pObj) ); return vObjs; } Vec_Int_t * Abc_NtkFinComputeObjects( Vec_Int_t * vPairs, Vec_Wec_t ** pvMap, int nObjs ) { int i, iObj, Type; Vec_Int_t * vObjs = Vec_IntAlloc( 100 ); *pvMap = Vec_WecStart( nObjs ); Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 ) { Vec_IntPush( vObjs, iObj ); Vec_WecPush( *pvMap, iObj, i/2 ); } Vec_IntUniqify( vObjs ); return vObjs; } Vec_Int_t * Abc_NtkFinCreateList( Vec_Wec_t * vMap, Vec_Int_t * vClass ) { int i, iObj; Vec_Int_t * vList = Vec_IntAlloc( 100 ); Vec_IntForEachEntry( vClass, iObj, i ) Vec_IntAppend( vList, Vec_WecEntry(vMap, iObj) ); return vList; } int Abc_NtkFinCountPairs( Vec_Wec_t * vClasses ) { int i, Counter = 0; Vec_Int_t * vLevel; Vec_WecForEachLevel( vClasses, vLevel, i ) Counter += Vec_IntSize(vLevel) - 1; return Counter; } Vec_Wec_t * Abc_NtkDetectFinClasses( Abc_Ntk_t * pNtk, int fVerbose ) { Vec_Int_t * vTypes = NULL; // gate types Vec_Int_t * vPairs; // original info as a set of pairs (ObjId, TypeId) Vec_Int_t * vObjs; // all those objects that have some fin Vec_Wec_t * vMap; // for each object, the set of fins Vec_Wec_t * vMap2; // for each local object, the set of pairs (Info, Index) Vec_Wec_t * vClasses; // classes of objects Vec_Wec_t * vCoSets; // corresponding CO sets Vec_Int_t * vClass; // one class Vec_Int_t * vCoSet; // one set of COs Vec_Int_t * vCiSet; // one set of CIs Vec_Int_t * vNodeSet; // one set of nodes Vec_Int_t * vList; // one info list Vec_Wec_t * vResult; // resulting equivalences int i, iObj, nCalls; if ( pNtk->vFins == NULL ) { printf( "Current network does not have the required info.\n" ); return NULL; } assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) ); if ( Abc_NtkIsSopLogic(pNtk) ) { iObj = Abc_NtkFinCheckTypesOk(pNtk); if ( iObj ) { printf( "Current network contains unsupported gate types (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); return NULL; } vTypes = Abc_NtkFinComputeTypes( pNtk ); } else if ( Abc_NtkIsMappedLogic(pNtk) ) { iObj = Abc_NtkFinCheckTypesOk2(pNtk); if ( iObj ) { printf( "Current network has mismatch between mapped gate size and fault gate size (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) ); return NULL; } } else assert( 0 ); //Abc_NtkFrameExtend( pNtk ); // collect data vPairs = pNtk->vFins; vObjs = Abc_NtkFinComputeObjects( vPairs, &vMap, Abc_NtkObjNumMax(pNtk) ); vClasses = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCoSets ); // refine classes vCiSet = Vec_IntAlloc( 1000 ); vNodeSet = Vec_IntAlloc( 1000 ); vMap2 = Vec_WecStart( Abc_NtkObjNumMax(pNtk) ); vResult = Vec_WecAlloc( 1000 ); Vec_WecForEachLevel( vClasses, vClass, i ) { // extract one window vCoSet = Vec_WecEntry( vCoSets, i ); Abc_NtkFinMiterCollect( pNtk, vCoSet, vCiSet, vNodeSet ); // refine one class vList = Abc_NtkFinCreateList( vMap, vClass ); nCalls = Abc_NtkFinRefinement( pNtk, vTypes, vCoSet, vCiSet, vNodeSet, vPairs, vList, vMap2, vResult ); if ( fVerbose ) printf( "Group %4d : Obj =%4d. Fins =%4d. CI =%5d. CO =%5d. Node =%6d. SAT calls =%5d.\n", i, Vec_IntSize(vClass), Vec_IntSize(vList), Vec_IntSize(vCiSet), Vec_IntSize(vCoSet), Vec_IntSize(vNodeSet), nCalls ); Vec_IntFree( vList ); } // sort entries in each array Vec_WecForEachLevel( vResult, vClass, i ) Vec_IntSort( vClass, 0 ); // sort by the index of the first entry Vec_WecSortByFirstInt( vResult, 0 ); // cleanup Vec_IntFreeP( & vTypes ); Vec_IntFree( vObjs ); Vec_WecFree( vClasses ); Vec_WecFree( vMap ); Vec_WecFree( vMap2 ); Vec_WecFree( vCoSets ); Vec_IntFree( vCiSet ); Vec_IntFree( vNodeSet ); return vResult; } /**Function************************************************************* Synopsis [Print results.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkPrintFinResults( Vec_Wec_t * vClasses ) { Vec_Int_t * vClass; int i, k, Entry; Vec_WecForEachLevel( vClasses, vClass, i ) Vec_IntForEachEntryStart( vClass, Entry, k, 1 ) printf( "%d %d\n", Vec_IntEntry(vClass, 0), Entry ); } /**Function************************************************************* Synopsis [Top-level procedure.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose ) { Vec_Wec_t * vResult; abctime clk = Abc_Clock(); if ( fSeq ) Abc_NtkFrameExtend( pNtk ); vResult = Abc_NtkDetectFinClasses( pNtk, fVerbose ); printf( "Computed %d equivalence classes with %d item pairs. ", Vec_WecSize(vResult), Abc_NtkFinCountPairs(vResult) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( fVeryVerbose ) Vec_WecPrint( vResult, 1 ); // if ( fVerbose ) // Abc_NtkPrintFinResults( vResult ); Vec_WecFree( vResult ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END