/**CFile**************************************************************** FileName [giaMini.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Reader/writer for MiniAIG.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaMini.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" #include "opt/dau/dau.h" #include "base/main/mainInt.h" #include "misc/util/utilTruth.h" #include "aig/miniaig/miniaig.h" #include "aig/miniaig/minilut.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Converts MiniAIG into GIA.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ObjFromMiniFanin0Copy( Gia_Man_t * pGia, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id ) { int Lit = Mini_AigNodeFanin0( p, Id ); return Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); } int Gia_ObjFromMiniFanin1Copy( Gia_Man_t * pGia, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id ) { int Lit = Mini_AigNodeFanin1( p, Id ); return Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); } Gia_Man_t * Gia_ManFromMiniAig( Mini_Aig_t * p, Vec_Int_t ** pvCopies ) { Gia_Man_t * pGia, * pTemp; Vec_Int_t * vCopies; int i, iGiaLit = 0, nNodes; // get the number of nodes nNodes = Mini_AigNodeNum(p); // create ABC network pGia = Gia_ManStart( nNodes ); pGia->pName = Abc_UtilStrsav( "MiniAig" ); // create mapping from MiniAIG objects into ABC objects vCopies = Vec_IntAlloc( nNodes ); Vec_IntPush( vCopies, 0 ); // iterate through the objects Gia_ManHashAlloc( pGia ); for ( i = 1; i < nNodes; i++ ) { if ( Mini_AigNodeIsPi( p, i ) ) iGiaLit = Gia_ManAppendCi(pGia); else if ( Mini_AigNodeIsPo( p, i ) ) iGiaLit = Gia_ManAppendCo(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i)); else if ( Mini_AigNodeIsAnd( p, i ) ) iGiaLit = Gia_ManHashAnd(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i), Gia_ObjFromMiniFanin1Copy(pGia, vCopies, p, i)); else assert( 0 ); Vec_IntPush( vCopies, iGiaLit ); } Gia_ManHashStop( pGia ); assert( Vec_IntSize(vCopies) == nNodes ); if ( pvCopies ) *pvCopies = vCopies; else Vec_IntFree( vCopies ); Gia_ManSetRegNum( pGia, Mini_AigRegNum(p) ); pGia = Gia_ManCleanup( pTemp = pGia ); if ( pvCopies ) Gia_ManDupRemapLiterals( *pvCopies, pTemp ); Gia_ManStop( pTemp ); return pGia; } /**Function************************************************************* Synopsis [Converts GIA into MiniAIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Mini_Aig_t * Gia_ManToMiniAig( Gia_Man_t * pGia ) { Mini_Aig_t * p; Gia_Obj_t * pObj; int i; // create the manager p = Mini_AigStart(); Gia_ManConst0(pGia)->Value = Mini_AigLitConst0(); // create primary inputs Gia_ManForEachCi( pGia, pObj, i ) pObj->Value = Mini_AigCreatePi(p); // create internal nodes Gia_ManForEachAnd( pGia, pObj, i ) pObj->Value = Mini_AigAnd( p, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); // create primary outputs Gia_ManForEachCo( pGia, pObj, i ) pObj->Value = Mini_AigCreatePo( p, Gia_ObjFanin0Copy(pObj) ); // set registers Mini_AigSetRegNum( p, Gia_ManRegNum(pGia) ); return p; } /**Function************************************************************* Synopsis [Procedures to input/output MiniAIG into/from internal GIA.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p ) { Gia_Man_t * pGia; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); Gia_ManStopP( &pAbc->pGiaMiniAig ); Vec_IntFreeP( &pAbc->vCopyMiniAig ); pGia = Gia_ManFromMiniAig( (Mini_Aig_t *)p, &pAbc->vCopyMiniAig ); Abc_FrameUpdateGia( pAbc, pGia ); pAbc->pGiaMiniAig = Gia_ManDup( pGia ); // Gia_ManDelete( pGia ); } void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc ) { Gia_Man_t * pGia; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); pGia = Abc_FrameReadGia( pAbc ); if ( pGia == NULL ) printf( "Current network in ABC framework is not defined.\n" ); return Gia_ManToMiniAig( pGia ); } /**Function************************************************************* Synopsis [Procedures to read/write GIA to/from MiniAIG file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManReadMiniAig( char * pFileName ) { Mini_Aig_t * p = Mini_AigLoad( pFileName ); Gia_Man_t * pGia = Gia_ManFromMiniAig( p, NULL ); ABC_FREE( pGia->pName ); pGia->pName = Extra_FileNameGeneric( pFileName ); Mini_AigStop( p ); return pGia; } void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName ) { Mini_Aig_t * p = Gia_ManToMiniAig( pGia ); Mini_AigDump( p, pFileName ); //Mini_AigDumpVerilog( "test_miniaig.v", "top", p ); Mini_AigStop( p ); } /**Function************************************************************* Synopsis [Converts MiniLUT into GIA.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p, Vec_Int_t ** pvCopies ) { Gia_Man_t * pGia, * pTemp; Vec_Int_t * vCopies; Vec_Int_t * vCover = Vec_IntAlloc( 1000 ); Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int i, k, Fan, iGiaLit, nNodes; int LutSize = Abc_MaxInt( 2, Mini_LutSize(p) ); // get the number of nodes nNodes = Mini_LutNodeNum(p); // create ABC network pGia = Gia_ManStart( 3 * nNodes ); pGia->pName = Abc_UtilStrsav( "MiniLut" ); // create mapping from MiniLUT objects into ABC objects vCopies = Vec_IntAlloc( nNodes ); Vec_IntPush( vCopies, 0 ); Vec_IntPush( vCopies, 1 ); // iterate through the objects Gia_ManHashAlloc( pGia ); for ( i = 2; i < nNodes; i++ ) { if ( Mini_LutNodeIsPi( p, i ) ) iGiaLit = Gia_ManAppendCi(pGia); else if ( Mini_LutNodeIsPo( p, i ) ) iGiaLit = Gia_ManAppendCo(pGia, Vec_IntEntry(vCopies, Mini_LutNodeFanin(p, i, 0))); else if ( Mini_LutNodeIsNode( p, i ) ) { unsigned * puTruth = Mini_LutNodeTruth( p, i ); word Truth = ((word)*puTruth << 32) | (word)*puTruth; word * pTruth = LutSize < 6 ? &Truth : (word *)puTruth; Vec_IntClear( vLits ); Mini_LutForEachFanin( p, i, Fan, k ) Vec_IntPush( vLits, Vec_IntEntry(vCopies, Fan) ); iGiaLit = Dsm_ManTruthToGia( pGia, pTruth, vLits, vCover ); } else assert( 0 ); Vec_IntPush( vCopies, iGiaLit ); } Vec_IntFree( vCover ); Vec_IntFree( vLits ); Gia_ManHashStop( pGia ); assert( Vec_IntSize(vCopies) == nNodes ); if ( pvCopies ) *pvCopies = vCopies; else Vec_IntFree( vCopies ); Gia_ManSetRegNum( pGia, Mini_LutRegNum(p) ); pGia = Gia_ManCleanup( pTemp = pGia ); if ( pvCopies ) Gia_ManDupRemapLiterals( *pvCopies, pTemp ); Gia_ManStop( pTemp ); return pGia; } /**Function************************************************************* Synopsis [Marks LUTs that should be complemented.] Description [These are LUTs whose all PO fanouts require them in negative polarity. Other fanouts may require them in positive polarity.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Bit_t * Gia_ManFindComplLuts( Gia_Man_t * pGia ) { Gia_Obj_t * pObj; int i; // mark objects pointed by COs in negative polarity Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(pGia) ); Gia_ManForEachCo( pGia, pObj, i ) if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj) ) Vec_BitWriteEntry( vMarks, Gia_ObjFaninId0p(pGia, pObj), 1 ); // unmark objects pointed by COs in positive polarity Gia_ManForEachCo( pGia, pObj, i ) if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) ) Vec_BitWriteEntry( vMarks, Gia_ObjFaninId0p(pGia, pObj), 0 ); return vMarks; } /**Function************************************************************* Synopsis [Converts GIA into MiniLUT.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia ) { Mini_Lut_t * p; Vec_Bit_t * vMarks; Gia_Obj_t * pObj, * pFanin; Vec_Int_t * vLeaves = Vec_IntAlloc( 16 ); Vec_Int_t * vInvMap = Vec_IntStart( Gia_ManObjNum(pGia) ); int i, k, iFanin, LutSize, nWords, Count = 0, pVars[16]; word * pTruth; assert( Gia_ManHasMapping(pGia) ); LutSize = Gia_ManLutSizeMax( pGia ); LutSize = Abc_MaxInt( LutSize, 2 ); nWords = Abc_Truth6WordNum( LutSize ); assert( LutSize >= 2 ); // create the manager p = Mini_LutStart( LutSize ); // create primary inputs Gia_ManFillValue( pGia ); Gia_ManForEachCi( pGia, pObj, i ) pObj->Value = Mini_LutCreatePi(p); // create internal nodes vMarks = Gia_ManFindComplLuts( pGia ); Gia_ObjComputeTruthTableStart( pGia, LutSize ); Gia_ManForEachLut( pGia, i ) { Vec_IntClear( vLeaves ); Gia_LutForEachFanin( pGia, i, iFanin, k ) Vec_IntPush( vLeaves, iFanin ); if ( Vec_IntSize(vLeaves) > 6 ) { int Extra = Vec_IntSize(vLeaves) - 7; for ( k = Extra; k >= 0; k-- ) Vec_IntPush( vLeaves, Vec_IntEntry(vLeaves, k) ); for ( k = Extra; k >= 0; k-- ) Vec_IntDrop( vLeaves, k ); assert( Vec_IntSize(vLeaves) == Gia_ObjLutSize(pGia, i) ); } Gia_ManForEachObjVec( vLeaves, pGia, pFanin, k ) pVars[k] = pFanin->Value; pObj = Gia_ManObj( pGia, i ); pTruth = Gia_ObjComputeTruthTableCut( pGia, pObj, vLeaves ); if ( Vec_BitEntry(vMarks, i) ) Abc_TtNot( pTruth, nWords ); Vec_IntForEachEntry( vLeaves, iFanin, k ) if ( Vec_BitEntry(vMarks, iFanin) ) Abc_TtFlip( pTruth, nWords, k ); pObj->Value = Mini_LutCreateNode( p, Gia_ObjLutSize(pGia, i), pVars, (unsigned *)pTruth ); } Vec_IntFree( vLeaves ); // create inverter truth table Vec_WrdClear( pGia->vTtMemory ); for ( i = 0; i < nWords; i++ ) Vec_WrdPush( pGia->vTtMemory, ABC_CONST(0x5555555555555555) ); pTruth = Vec_WrdArray( pGia->vTtMemory ); // create primary outputs Gia_ManForEachCo( pGia, pObj, i ) { if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(pGia) ) pObj->Value = Mini_LutCreatePo( p, Gia_ObjFaninC0(pObj) ); else if ( Gia_ObjFaninC0(pObj) == Vec_BitEntry(vMarks, Gia_ObjFaninId0p(pGia, pObj)) ) pObj->Value = Mini_LutCreatePo( p, Gia_ObjFanin0(pObj)->Value ); else // add inverter LUT { int LutInv, Fanin = Gia_ObjFanin0(pObj)->Value; if ( (LutInv = Vec_IntEntry(vInvMap, Fanin)) == 0 ) { LutInv = Mini_LutCreateNode( p, 1, &Fanin, (unsigned *)pTruth ); Vec_IntWriteEntry( vInvMap, Fanin, LutInv ); Count++; } pObj->Value = Mini_LutCreatePo( p, LutInv ); } } Vec_IntFree( vInvMap ); Vec_BitFree( vMarks ); Gia_ObjComputeTruthTableStop( pGia ); // set registers Mini_LutSetRegNum( p, Gia_ManRegNum(pGia) ); //Mini_LutPrintStats( p ); //printf( "Added %d inverters.\n", Count ); return p; } char * Gia_ManToMiniLutAttr( Gia_Man_t * pGia, void * pMiniLut ) { Mini_Lut_t * p = (Mini_Lut_t *)pMiniLut; int i; char * pAttrs = ABC_CALLOC( char, Mini_LutNodeNum(p) ); Gia_ManForEachLut( pGia, i ) if ( Gia_ObjLutIsMux(pGia, i) ) pAttrs[Gia_ManObj(pGia, i)->Value] = 1; return pAttrs; } /**Function************************************************************* Synopsis [Procedures to input/output MiniAIG into/from internal GIA.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * p ) { Gia_Man_t * pGia; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); pGia = Gia_ManFromMiniLut( (Mini_Lut_t *)p, NULL ); Abc_FrameUpdateGia( pAbc, pGia ); // Gia_ManDelete( pGia ); } void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc ) { Mini_Lut_t * pRes = NULL; Gia_Man_t * pGia; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); Gia_ManStopP( &pAbc->pGiaMiniLut ); Vec_IntFreeP( &pAbc->vCopyMiniLut ); pGia = Abc_FrameReadGia( pAbc ); if ( pGia == NULL ) printf( "Current network in ABC framework is not defined.\n" ); pRes = Gia_ManToMiniLut( pGia ); pAbc->pGiaMiniLut = Gia_ManFromMiniLut( pRes, &pAbc->vCopyMiniLut ); return pRes; } char * Abc_FrameGiaOutputMiniLutAttr( Abc_Frame_t * pAbc, void * pMiniLut ) { Gia_Man_t * pGia; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); pGia = Abc_FrameReadGia( pAbc ); if ( pGia == NULL ) printf( "Current network in ABC framework is not defined.\n" ); return Gia_ManToMiniLutAttr( pGia, pMiniLut ); } /**Function************************************************************* Synopsis [Procedures to read/write GIA to/from MiniAIG file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManReadMiniLut( char * pFileName ) { Mini_Lut_t * p = Mini_LutLoad( pFileName ); Gia_Man_t * pGia = Gia_ManFromMiniLut( p, NULL ); ABC_FREE( pGia->pName ); pGia->pName = Extra_FileNameGeneric( pFileName ); Mini_LutStop( p ); return pGia; } void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName ) { Mini_Lut_t * p = Gia_ManToMiniLut( pGia ); Mini_LutDump( p, pFileName ); Mini_LutStop( p ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int * Gia_ManMapMiniLut2MiniAig( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 ) { int * pRes = ABC_FALLOC( int, Vec_IntSize(vMap2) ); Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry, iRepr, fCompl, iLit; Gia_Obj_t * pObj; Gia_ManSetPhase( p1 ); Gia_ManSetPhase( p2 ); Vec_IntForEachEntry( vMap1, Entry, i ) { if ( Entry == -1 ) continue; pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); if ( ~pObj->Value == 0 ) continue; fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; iRepr = Gia_ObjReprSelf(p, Abc_Lit2Var(pObj->Value)); Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit(i, fCompl) ); } Vec_IntForEachEntry( vMap2, Entry, i ) { if ( Entry == -1 ) continue; pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); if ( ~pObj->Value == 0 ) continue; fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; iRepr = Gia_ObjReprSelf(p, Abc_Lit2Var(pObj->Value)); if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 ) continue; pRes[i] = Abc_LitNotCond( iLit, fCompl ); } Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 ); Vec_IntForEachEntry( vMap1, Entry, i ) { if ( Entry == -1 ) continue; pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); if ( !Gia_ObjIsCo(pObj) ) continue; Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i ); } Vec_IntForEachEntry( vMap2, Entry, i ) { if ( Entry == -1 ) continue; pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); if ( !Gia_ObjIsCo(pObj) ) continue; assert( pRes[i] == -1 ); pRes[i] = Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 ); assert( pRes[i] != -1 ); } Vec_IntFree( vMap ); return pRes; } void Gia_ManNameMapVerify( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2, int * pMap ) { int iLut, iObj1, iObj2, nSize = Vec_IntSize(vMap2); Gia_Obj_t * pObjAig, * pObjLut; Gia_ManSetPhase( p1 ); Gia_ManSetPhase( p2 ); for ( iLut = 0; iLut < nSize; iLut++ ) if ( pMap[iLut] >= 0 ) { int iObj = Abc_Lit2Var( pMap[iLut] ); int fCompl = Abc_LitIsCompl( pMap[iLut] ); int iLitAig = Vec_IntEntry( vMap1, iObj ); int iLitLut = Vec_IntEntry( vMap2, iLut ); pObjAig = Gia_ManObj( p1, Abc_Lit2Var(iLitAig) ); if ( Gia_ObjIsCo(pObjAig) ) continue; if ( ~pObjAig->Value == 0 ) continue; pObjLut = Gia_ManObj( p2, Abc_Lit2Var(iLitLut) ); if ( ~pObjLut->Value == 0 ) continue; iObj1 = Gia_ObjReprSelf(p, Abc_Lit2Var(pObjAig->Value)); iObj2 = Gia_ObjReprSelf(p, Abc_Lit2Var(pObjLut->Value)); if ( iObj1 != iObj2 ) printf( "Found functional mismatch for LutId %d and AigId %d.\n", iLut, iObj ); if ( (pObjLut->fPhase ^ Abc_LitIsCompl(iLitLut)) != (pObjAig->fPhase ^ Abc_LitIsCompl(iLitAig) ^ fCompl) ) printf( "Found phase mismatch for LutId %d and AigId %d.\n", iLut, iObj ); } } int * Abc_FrameReadMiniLutNameMapping( Abc_Frame_t * pAbc ) { int fVerbose = 0; int nConfs = 1000; Gia_Man_t * pGia, * pTemp; int * pRes = NULL; if ( pAbc->pGiaMiniAig == NULL ) printf( "GIA derived from MiniAig is not available.\n" ); if ( pAbc->pGiaMiniLut == NULL ) printf( "GIA derived from MiniLut is not available.\n" ); if ( pAbc->pGiaMiniAig == NULL || pAbc->pGiaMiniLut == NULL ) return NULL; pGia = Gia_ManDup2( pAbc->pGiaMiniAig, pAbc->pGiaMiniLut ); //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0, 0 ); // compute equivalences in this AIG pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose ); Gia_ManStop( pTemp ); //if ( fVerbose ) // Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk ); //if ( fVerbose ) // Gia_ManPrintStats( pGia, NULL ); //Vec_IntPrint( pAbc->vCopyMiniAig ); //Vec_IntPrint( pAbc->vCopyMiniLut ); pRes = Gia_ManMapMiniLut2MiniAig( pGia, pAbc->pGiaMiniAig, pAbc->pGiaMiniLut, pAbc->vCopyMiniAig, pAbc->vCopyMiniLut ); //Gia_ManNameMapVerify( pGia, pAbc->pGiaMiniAig, pAbc->pGiaMiniLut, pAbc->vCopyMiniAig, pAbc->vCopyMiniLut, pRes ); Gia_ManStop( pGia ); return pRes; } /**Function************************************************************* Synopsis [Returns equivalences of MiniAig nodes.] Description [The resulting array contains as many entries as there are objects in the initial MiniAIG. If the i-th entry of the array is equal to -1, it means that the i-th MiniAIG object is not equivalent to any other object. Otherwise, the i-th entry contains the literal of the representative of the equivalence class of objects, to which the i-th object belongs. The representative is defined as the first object belonging to the equivalence class in the current topological order. It can be the constant 0 node, a flop output or an internal node. It is the user's responsibility to free the resulting array when it is not needed.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap ) { Vec_Int_t * vRes = Vec_IntStartFull( Vec_IntSize(vMap) ); Vec_Int_t * vGia2Mini = Vec_IntStartFull( Gia_ManObjNum(p) ); Gia_Obj_t * pObj, * pRepr; int i, iObjLit, iReprLit, fCompl, iReprGia, iReprMini; Vec_IntForEachEntry( vMap, iObjLit, i ) { if ( iObjLit == -1 ) continue; iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) ); iReprMini = Vec_IntEntry( vGia2Mini, iReprGia ); if ( iReprMini == -1 ) { Vec_IntWriteEntry( vGia2Mini, iReprGia, i ); continue; } if ( iReprMini == i ) continue; assert( iReprMini < i ); Vec_IntWriteEntry( vRes, i, iReprMini ); } Vec_IntFree( vGia2Mini ); Gia_ManSetPhase( p ); Vec_IntForEachEntry( vRes, iReprMini, i ) { if ( iReprMini == -1 ) continue; iObjLit = Vec_IntEntry(vMap, i); iReprLit = Vec_IntEntry(vMap, iReprMini); pObj = Gia_ManObj( p, Abc_Lit2Var(iObjLit) ); pRepr = Gia_ManObj( p, Abc_Lit2Var(iReprLit) ); fCompl = Abc_LitIsCompl(iObjLit) ^ Abc_LitIsCompl(iReprLit) ^ pObj->fPhase ^ pRepr->fPhase; Vec_IntWriteEntry( vRes, i, Abc_Var2Lit(iReprMini, fCompl) ); } return vRes; } int * Abc_FrameReadMiniAigEquivClasses( Abc_Frame_t * pAbc ) { Vec_Int_t * vRes; int * pRes; if ( pAbc->pGiaMiniAig == NULL ) printf( "GIA derived from MiniAig is not available.\n" ); if ( pAbc->vCopyMiniAig == NULL ) printf( "Mapping of MiniAig nodes is not available.\n" ); if ( pAbc->pGia2 == NULL ) printf( "Internal GIA with equivalence classes is not available.\n" ); if ( pAbc->pGia2->pReprs == NULL ) printf( "Equivalence classes of internal GIA are not available.\n" ); if ( Gia_ManObjNum(pAbc->pGia2) != Gia_ManObjNum(pAbc->pGiaMiniAig) ) printf( "Internal GIA with equivalence classes is not directly derived from MiniAig.\n" ); // derive the set of equivalent node pairs vRes = Gia_ManMapEquivAfterScorr( pAbc->pGia2, pAbc->vCopyMiniAig ); pRes = Vec_IntReleaseArray( vRes ); Vec_IntFree( vRes ); return pRes; } /**Function************************************************************* Synopsis [Verifies equivalences of MiniAig nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_MiniAigReduce( Mini_Aig_t * p, int * pEquivs ) { Gia_Man_t * pGia, * pTemp; Vec_Int_t * vCopies; int i, iGiaLit = 0, nNodes; // get the number of nodes nNodes = Mini_AigNodeNum(p); // create ABC network pGia = Gia_ManStart( nNodes ); pGia->pName = Abc_UtilStrsav( "MiniAig" ); // create mapping from MiniAIG objects into ABC objects vCopies = Vec_IntAlloc( nNodes ); Vec_IntPush( vCopies, 0 ); // iterate through the objects Gia_ManHashAlloc( pGia ); for ( i = 1; i < nNodes; i++ ) { if ( Mini_AigNodeIsPi( p, i ) ) iGiaLit = Gia_ManAppendCi(pGia); else if ( Mini_AigNodeIsPo( p, i ) ) iGiaLit = Gia_ManAppendCo(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i)); else if ( Mini_AigNodeIsAnd( p, i ) ) iGiaLit = Gia_ManHashAnd(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i), Gia_ObjFromMiniFanin1Copy(pGia, vCopies, p, i)); else assert( 0 ); if ( pEquivs[i] != -1 ) iGiaLit = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(pEquivs[i])), Abc_LitIsCompl(pEquivs[i]) ); Vec_IntPush( vCopies, iGiaLit ); } Gia_ManHashStop( pGia ); assert( Vec_IntSize(vCopies) == nNodes ); Vec_IntFree( vCopies ); Gia_ManSetRegNum( pGia, Mini_AigRegNum(p) ); pGia = Gia_ManSeqCleanup( pTemp = pGia ); Gia_ManStop( pTemp ); return pGia; } Gia_Man_t * Gia_MiniAigMiter( Mini_Aig_t * p, int * pEquivs ) { Gia_Man_t * pGia, * pTemp; Vec_Int_t * vCopies; int i, iGiaLit = 0, iGiaLit2, nNodes, iPos = 0, nPos = 0, Temp; // get the number of nodes nNodes = Mini_AigNodeNum(p); // create ABC network pGia = Gia_ManStart( 2 * nNodes ); pGia->pName = Abc_UtilStrsav( "MiniAig" ); // create mapping from MiniAIG objects into ABC objects vCopies = Vec_IntAlloc( nNodes ); Vec_IntPush( vCopies, 0 ); // iterate through the objects Gia_ManHashAlloc( pGia ); for ( i = 1; i < nNodes; i++ ) { if ( Mini_AigNodeIsPi( p, i ) ) iGiaLit = Gia_ManAppendCi(pGia); else if ( Mini_AigNodeIsPo( p, i ) ) { nPos++; Vec_IntPush( vCopies, -1 ); continue; } else if ( Mini_AigNodeIsAnd( p, i ) ) iGiaLit = Gia_ManHashAnd(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i), Gia_ObjFromMiniFanin1Copy(pGia, vCopies, p, i)); else assert( 0 ); Vec_IntPush( vCopies, iGiaLit ); } assert( Vec_IntSize(vCopies) == nNodes ); assert( nPos > Mini_AigRegNum(p) ); // create miters for each equiv class for ( i = 1; i < nNodes; i++ ) { if ( pEquivs[i] == -1 ) continue; iGiaLit = Vec_IntEntry(vCopies, i); iGiaLit2 = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(pEquivs[i])), Abc_LitIsCompl(pEquivs[i]) ); Gia_ManAppendCo( pGia, Gia_ManHashXor(pGia, iGiaLit, iGiaLit2) ); } // create flop inputs Temp = Gia_ManCoNum(pGia); for ( i = 1; i < nNodes; i++ ) { if ( !Mini_AigNodeIsPo( p, i ) ) continue; if ( iPos++ >= nPos - Mini_AigRegNum(p) ) Gia_ManAppendCo(pGia, Gia_ObjFromMiniFanin0Copy(pGia, vCopies, p, i)); } assert( iPos == nPos ); assert( Mini_AigRegNum(p) == Gia_ManCoNum(pGia) - Temp ); Gia_ManSetRegNum( pGia, Mini_AigRegNum(p) ); Gia_ManHashStop( pGia ); Vec_IntFree( vCopies ); pGia = Gia_ManCleanup( pTemp = pGia ); Gia_ManStop( pTemp ); return pGia; } void Gia_MiniAigVerify( Abc_Frame_t * pAbc, char * pFileName ) { int * pEquivs; Gia_Man_t * pGia; char * pFileMiter = "mini_aig_miter.aig"; char * pFileReduced = "mini_aig_reduced.aig"; Mini_Aig_t * p = Mini_AigLoad( pFileName ); Abc_FrameGiaInputMiniAig( pAbc, p ); Cmd_CommandExecute( pAbc, "&ps; &scorr; &ps" ); pEquivs = Abc_FrameReadMiniAigEquivClasses( pAbc ); // dump miter for verification pGia = Gia_MiniAigMiter( p, pEquivs ); Gia_AigerWrite( pGia, pFileMiter, 0, 0, 0 ); printf( "Dumped miter AIG in file \"%s\".\n", pFileMiter ); Gia_ManStop( pGia ); // dump reduced AIG pGia = Gia_MiniAigReduce( p, pEquivs ); Gia_AigerWrite( pGia, pFileReduced, 0, 0, 0 ); printf( "Dumped reduced AIG in file \"%s\".\n", pFileReduced ); Gia_ManStop( pGia ); // cleanup ABC_FREE( pEquivs ); Mini_AigStop( p ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END