/**CFile**************************************************************** FileName [aigUtil.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [AIG package.] Synopsis [Various procedures.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] Revision [$Id: aigUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ #include "aig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Increments the current traversal ID of the network.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManIncrementTravId( Aig_Man_t * p ) { if ( p->nTravIds >= (1<<30)-1 ) Aig_ManCleanData( p ); p->nTravIds++; } /**Function************************************************************* Synopsis [Returns the time stamp.] Description [The file should be closed.] SideEffects [] SeeAlso [] ***********************************************************************/ char * Aig_TimeStamp() { static char Buffer[100]; char * TimeStamp; time_t ltime; // get the current time time( <ime ); TimeStamp = asctime( localtime( <ime ) ); TimeStamp[ strlen(TimeStamp) - 1 ] = 0; strcpy( Buffer, TimeStamp ); return Buffer; } /**Function************************************************************* Synopsis [Make sure AIG has not gaps in the numeric order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ManHasNoGaps( Aig_Man_t * p ) { return (int)(Aig_ManObjNum(p) == Aig_ManCiNum(p) + Aig_ManCoNum(p) + Aig_ManNodeNum(p) + 1); } /**Function************************************************************* Synopsis [Collect the latches.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ManLevels( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i, LevelMax = 0; Aig_ManForEachCo( p, pObj, i ) LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level ); return LevelMax; } /**Function************************************************************* Synopsis [Reset reference counters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManResetRefs( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->nRefs = 0; Aig_ManForEachObj( p, pObj, i ) { if ( Aig_ObjFanin0(pObj) ) Aig_ObjFanin0(pObj)->nRefs++; if ( Aig_ObjFanin1(pObj) ) Aig_ObjFanin1(pObj)->nRefs++; } } /**Function************************************************************* Synopsis [Cleans fMarkA.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanMarkA( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->fMarkA = 0; } /**Function************************************************************* Synopsis [Cleans fMarkB.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanMarkB( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->fMarkB = 0; } /**Function************************************************************* Synopsis [Cleans fMarkB.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanMarkAB( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->fMarkA = pObj->fMarkB = 0; } /**Function************************************************************* Synopsis [Cleans the data pointers for the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanData( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->pData = NULL; } /**Function************************************************************* Synopsis [Cleans the data pointers for the nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanNext( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) pObj->pNext = NULL; } /**Function************************************************************* Synopsis [Recursively cleans the data pointers in the cone of the node.] Description [Applicable to small AIGs only because no caching is performed.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjCleanData_rec( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); assert( !Aig_ObjIsCo(pObj) ); if ( Aig_ObjIsAnd(pObj) ) { Aig_ObjCleanData_rec( Aig_ObjFanin0(pObj) ); Aig_ObjCleanData_rec( Aig_ObjFanin1(pObj) ); } pObj->pData = NULL; } /**Function************************************************************* Synopsis [Detects multi-input gate rooted at this node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) { if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) ) { Vec_PtrPushUnique(vSuper, pObj); return; } Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper ); Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper ); } /**Function************************************************************* Synopsis [Detects multi-input gate rooted at this node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper ) { assert( !Aig_IsComplement(pRoot) ); Vec_PtrClear( vSuper ); Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper ); } /**Function************************************************************* Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ObjIsMuxType( Aig_Obj_t * pNode ) { Aig_Obj_t * pNode0, * pNode1; // check that the node is regular assert( !Aig_IsComplement(pNode) ); // if the node is not AND, this is not MUX if ( !Aig_ObjIsAnd(pNode) ) return 0; // if the children are not complemented, this is not MUX if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) ) return 0; // get children pNode0 = Aig_ObjFanin0(pNode); pNode1 = Aig_ObjFanin1(pNode); // if the children are not ANDs, this is not MUX if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) ) return 0; // otherwise the node is MUX iff it has a pair of equal grandchildren return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) || (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) || (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) || (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1))); } /**Function************************************************************* Synopsis [Recognizes what nodes are inputs of the EXOR.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 ) { Aig_Obj_t * p0, * p1; assert( !Aig_IsComplement(pObj) ); if ( !Aig_ObjIsNode(pObj) ) return 0; if ( Aig_ObjIsExor(pObj) ) { *ppFan0 = Aig_ObjChild0(pObj); *ppFan1 = Aig_ObjChild1(pObj); return 1; } assert( Aig_ObjIsAnd(pObj) ); p0 = Aig_ObjChild0(pObj); p1 = Aig_ObjChild1(pObj); if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) ) return 0; p0 = Aig_Regular(p0); p1 = Aig_Regular(p1); if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) ) return 0; if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) ) return 0; if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) ) return 0; *ppFan0 = Aig_ObjChild0(p0); *ppFan1 = Aig_ObjChild1(p0); return 1; } /**Function************************************************************* Synopsis [Recognizes what nodes are control and data inputs of a MUX.] Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Obj_t ** ppNodeE ) { Aig_Obj_t * pNode0, * pNode1; assert( !Aig_IsComplement(pNode) ); assert( Aig_ObjIsMuxType(pNode) ); // get children pNode0 = Aig_ObjFanin0(pNode); pNode1 = Aig_ObjFanin1(pNode); // find the control variable if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) ) { // if ( Fraig_IsComplement(pNode1->p2) ) if ( Aig_ObjFaninC1(pNode0) ) { // pNode2->p2 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1); *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1); return Aig_ObjChild1(pNode1);//pNode2->p2; } else { // pNode1->p2 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1); *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1); return Aig_ObjChild1(pNode0);//pNode1->p2; } } else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) ) { // if ( Fraig_IsComplement(pNode1->p1) ) if ( Aig_ObjFaninC0(pNode0) ) { // pNode2->p1 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2); *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2); return Aig_ObjChild0(pNode1);//pNode2->p1; } else { // pNode1->p1 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2); *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2); return Aig_ObjChild0(pNode0);//pNode1->p1; } } else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) ) { // if ( Fraig_IsComplement(pNode1->p1) ) if ( Aig_ObjFaninC0(pNode0) ) { // pNode2->p2 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1); *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2); return Aig_ObjChild1(pNode1);//pNode2->p2; } else { // pNode1->p1 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2); *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1); return Aig_ObjChild0(pNode0);//pNode1->p1; } } else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) ) { // if ( Fraig_IsComplement(pNode1->p2) ) if ( Aig_ObjFaninC1(pNode0) ) { // pNode2->p1 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2); *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1); return Aig_ObjChild0(pNode1);//pNode2->p1; } else { // pNode1->p2 is positive phase of C *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1); *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2); return Aig_ObjChild1(pNode0);//pNode1->p2; } } assert( 0 ); // this is not MUX return NULL; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj ) { Aig_Obj_t * pObjNew, * pObjR = Aig_Regular(pObj); if ( !Aig_ObjIsBuf(pObjR) ) return pObj; pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObjR) ); return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) ); } /**Function************************************************************* Synopsis [Procedure used for sorting the nodes in increasing order of IDs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) { int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2); if ( Diff < 0 ) return -1; if ( Diff > 0 ) return 1; return 0; } /**Function************************************************************* Synopsis [Prints Eqn formula for the AIG rooted at this node.] Description [The formula is in terms of PIs, which should have their names assigned in pObj->pData fields.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ) { Vec_Ptr_t * vSuper; Aig_Obj_t * pFanin; int fCompl, i; // store the complemented attribute fCompl = Aig_IsComplement(pObj); pObj = Aig_Regular(pObj); // constant case if ( Aig_ObjIsConst1(pObj) ) { fprintf( pFile, "%d", !fCompl ); return; } // PI case if ( Aig_ObjIsCi(pObj) ) { fprintf( pFile, "%s%s", fCompl? "!" : "", (char*)pObj->pData ); return; } // AND case Vec_VecExpand( vLevels, Level ); vSuper = Vec_VecEntry(vLevels, Level); Aig_ObjCollectMulti( pObj, vSuper ); fprintf( pFile, "%s", (Level==0? "" : "(") ); Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 ); if ( i < Vec_PtrSize(vSuper) - 1 ) fprintf( pFile, " %s ", fCompl? "+" : "*" ); } fprintf( pFile, "%s", (Level==0? "" : ")") ); return; } /**Function************************************************************* Synopsis [Prints Verilog formula for the AIG rooted at this node.] Description [The formula is in terms of PIs, which should have their names assigned in pObj->pData fields.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ) { Vec_Ptr_t * vSuper; Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC; int fCompl, i; // store the complemented attribute fCompl = Aig_IsComplement(pObj); pObj = Aig_Regular(pObj); // constant case if ( Aig_ObjIsConst1(pObj) ) { fprintf( pFile, "1\'b%d", !fCompl ); return; } // PI case if ( Aig_ObjIsCi(pObj) ) { fprintf( pFile, "%s%s", fCompl? "~" : "", (char*)pObj->pData ); return; } // EXOR case if ( Aig_ObjIsExor(pObj) ) { Vec_VecExpand( vLevels, Level ); vSuper = Vec_VecEntry( vLevels, Level ); Aig_ObjCollectMulti( pObj, vSuper ); fprintf( pFile, "%s", (Level==0? "" : "(") ); Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 ); if ( i < Vec_PtrSize(vSuper) - 1 ) fprintf( pFile, " ^ " ); } fprintf( pFile, "%s", (Level==0? "" : ")") ); return; } // MUX case if ( Aig_ObjIsMuxType(pObj) ) { if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) ) { fprintf( pFile, "%s", (Level==0? "" : "(") ); Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 ); fprintf( pFile, " ^ " ); Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 ); fprintf( pFile, "%s", (Level==0? "" : ")") ); } else { pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 ); fprintf( pFile, "%s", (Level==0? "" : "(") ); Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 ); fprintf( pFile, " ? " ); Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 ); fprintf( pFile, " : " ); Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 ); fprintf( pFile, "%s", (Level==0? "" : ")") ); } return; } // AND case Vec_VecExpand( vLevels, Level ); vSuper = Vec_VecEntry(vLevels, Level); Aig_ObjCollectMulti( pObj, vSuper ); fprintf( pFile, "%s", (Level==0? "" : "(") ); Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i ) { Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 ); if ( i < Vec_PtrSize(vSuper) - 1 ) fprintf( pFile, " %s ", fCompl? "|" : "&" ); } fprintf( pFile, "%s", (Level==0? "" : ")") ); return; } /**Function************************************************************* Synopsis [Prints node in HAIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ) { assert( !Aig_IsComplement(pObj) ); printf( "Node %p : ", pObj ); if ( Aig_ObjIsConst1(pObj) ) printf( "constant 1" ); else if ( Aig_ObjIsCi(pObj) ) printf( "PI" ); else if ( Aig_ObjIsCo(pObj) ) { printf( "PO" ); printf( "%p%s", Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") ); } else printf( "AND( %p%s, %p%s )", Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") ); printf( " (refs = %3d)", Aig_ObjRefs(pObj) ); } /**Function************************************************************* Synopsis [Prints node in HAIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ) { Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; int i; printf( "PIs: " ); Aig_ManForEachCi( p, pObj, i ) printf( " %p", pObj ); printf( "\n" ); vNodes = Aig_ManDfs( p, 0 ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" ); printf( "\n" ); Vec_PtrFree( vNodes ); } /**Function************************************************************* Synopsis [Write speculative miter for one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManDump( Aig_Man_t * p ) { static int Counter = 0; char FileName[20]; // dump the logic into a file sprintf( FileName, "aigbug\\%03d.blif", ++Counter ); Aig_ManDumpBlif( p, FileName, NULL, NULL ); printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName ); } /**Function************************************************************* Synopsis [Writes the AIG into a BLIF file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ) { FILE * pFile; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL; int i, nDigits, Counter = 0; if ( Aig_ManCoNum(p) == 0 ) { printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); return; } // check if constant is used Aig_ManForEachCo( p, pObj, i ) if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) pConst1 = Aig_ManConst1(p); // collect nodes in the DFS order vNodes = Aig_ManDfs( p, 1 ); // assign IDs to objects Aig_ManConst1(p)->iData = Counter++; Aig_ManForEachCi( p, pObj, i ) pObj->iData = Counter++; Aig_ManForEachCo( p, pObj, i ) pObj->iData = Counter++; Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) pObj->iData = Counter++; nDigits = Abc_Base10Log( Counter ); // write the file pFile = fopen( pFileName, "w" ); fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" ); // fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); fprintf( pFile, ".model %s\n", p->pName ); // write PIs fprintf( pFile, ".inputs" ); Aig_ManForEachPiSeq( p, pObj, i ) if ( vPiNames ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) ); else fprintf( pFile, " n%0*d", nDigits, pObj->iData ); fprintf( pFile, "\n" ); // write POs fprintf( pFile, ".outputs" ); Aig_ManForEachPoSeq( p, pObj, i ) if ( vPoNames ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) ); else fprintf( pFile, " n%0*d", nDigits, pObj->iData ); fprintf( pFile, "\n" ); // write latches if ( Aig_ManRegNum(p) ) { fprintf( pFile, "\n" ); Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) { fprintf( pFile, ".latch" ); if ( vPoNames ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) ); else fprintf( pFile, " n%0*d", nDigits, pObjLi->iData ); if ( vPiNames ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) ); else fprintf( pFile, " n%0*d", nDigits, pObjLo->iData ); fprintf( pFile, " 0\n" ); } fprintf( pFile, "\n" ); } // write nodes if ( pConst1 ) fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData ); Aig_ManSetCioIds( p ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { fprintf( pFile, ".names" ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData ); fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) ); } // write POs Aig_ManForEachCo( p, pObj, i ) { fprintf( pFile, ".names" ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); if ( vPoNames ) fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) ); else fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) ); } Aig_ManCleanCioIds( p ); fprintf( pFile, ".end\n\n" ); fclose( pFile ); Vec_PtrFree( vNodes ); } /**Function************************************************************* Synopsis [Writes the AIG into a Verilog file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ) { FILE * pFile; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL; int i, nDigits, Counter = 0; if ( Aig_ManCoNum(p) == 0 ) { printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); return; } // check if constant is used Aig_ManForEachCo( p, pObj, i ) if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) pConst1 = Aig_ManConst1(p); // collect nodes in the DFS order vNodes = Aig_ManDfs( p, 1 ); // assign IDs to objects Aig_ManConst1(p)->iData = Counter++; Aig_ManForEachCi( p, pObj, i ) pObj->iData = Counter++; Aig_ManForEachCo( p, pObj, i ) pObj->iData = Counter++; Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) pObj->iData = Counter++; nDigits = Abc_Base10Log( Counter ); // write the file pFile = fopen( pFileName, "w" ); fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" ); // fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); if ( Aig_ManRegNum(p) ) fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" ); else fprintf( pFile, "module %s (", p->pName? p->pName: "test" ); Aig_ManForEachPiSeq( p, pObj, i ) fprintf( pFile, "%s n%0*d", ((Aig_ManRegNum(p) || i)? ",":""), nDigits, pObj->iData ); Aig_ManForEachPoSeq( p, pObj, i ) fprintf( pFile, ", n%0*d", nDigits, pObj->iData ); fprintf( pFile, " );\n" ); // write PIs if ( Aig_ManRegNum(p) ) fprintf( pFile, "input clock;\n" ); Aig_ManForEachPiSeq( p, pObj, i ) fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData ); // write POs Aig_ManForEachPoSeq( p, pObj, i ) fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData ); // write latches if ( Aig_ManRegNum(p) ) { Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData ); Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData ); } // write nodes Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData ); if ( pConst1 ) fprintf( pFile, "wire n%0*d;\n", nDigits, pConst1->iData ); // write nodes if ( pConst1 ) fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", nDigits, pObj->iData, !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData, !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData ); } // write POs Aig_ManForEachPoSeq( p, pObj, i ) { fprintf( pFile, "assign n%0*d = %sn%0*d;\n", nDigits, pObj->iData, !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData ); } if ( Aig_ManRegNum(p) ) { Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) { fprintf( pFile, "assign n%0*d = %sn%0*d;\n", nDigits, pObjLi->iData, !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData ); } } // write initial state if ( Aig_ManRegNum(p) ) { Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n", nDigits, pObjLo->iData, nDigits, pObjLi->iData ); Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n", nDigits, pObjLo->iData ); } fprintf( pFile, "endmodule\n\n" ); fclose( pFile ); Vec_PtrFree( vNodes ); } /**Function************************************************************* Synopsis [Sets the PI/PO numbers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManSetCioIds( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachCi( p, pObj, i ) pObj->CioId = i; Aig_ManForEachCo( p, pObj, i ) pObj->CioId = i; } /**Function************************************************************* Synopsis [Sets the PI/PO numbers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCleanCioIds( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachCi( p, pObj, i ) pObj->pNext = NULL; Aig_ManForEachCo( p, pObj, i ) pObj->pNext = NULL; } /**Function************************************************************* Synopsis [Sets the PI/PO numbers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ManChoiceNum( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i, Counter = 0; Aig_ManForEachNode( p, pObj, i ) Counter += Aig_ObjIsChoice( p, pObj ); return Counter; } /**Function************************************************************* Synopsis [Prints the fanouts of the control register.] Description [Useful only for Intel MC benchmarks.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManPrintControlFanouts( Aig_Man_t * p ) { Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl; int i; pCtrl = Aig_ManCi( p, Aig_ManCiNum(p) - 1 ); printf( "Control signal:\n" ); Aig_ObjPrint( p, pCtrl ); printf( "\n\n" ); Aig_ManForEachObj( p, pObj, i ) { if ( !Aig_ObjIsNode(pObj) ) continue; assert( pObj != pCtrl ); pFanin0 = Aig_ObjFanin0(pObj); pFanin1 = Aig_ObjFanin1(pObj); if ( pFanin0 == pCtrl && Aig_ObjIsCi(pFanin1) ) { Aig_ObjPrint( p, pObj ); printf( "\n" ); Aig_ObjPrint( p, pFanin1 ); printf( "\n" ); printf( "\n" ); } if ( pFanin1 == pCtrl && Aig_ObjIsCi(pFanin0) ) { Aig_ObjPrint( p, pObj ); printf( "\n" ); Aig_ObjPrint( p, pFanin0 ); printf( "\n" ); printf( "\n" ); } } } /**Function************************************************************* Synopsis [Returns the composite name of the file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix ) { static char Buffer[1000]; char * pDot; strcpy( Buffer, pBase ); if ( (pDot = strrchr( Buffer, '.' )) ) *pDot = 0; strcat( Buffer, pSuffix ); if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) ) return pDot+1; return Buffer; } /**Function************************************************************* Synopsis [Creates a sequence of random numbers.] Description [] SideEffects [] SeeAlso [http://en.wikipedia.org/wiki/LFSR] ***********************************************************************/ void Aig_ManRandomTest2() { FILE * pFile; unsigned int lfsr = 1; unsigned int period = 0; pFile = fopen( "rand.txt", "w" ); do { // lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1 lfsr = 1; // to prevent the warning ++period; fprintf( pFile, "%10d : %10d ", period, lfsr ); // Extra_PrintBinary( pFile, &lfsr, 32 ); fprintf( pFile, "\n" ); if ( period == 20000 ) break; } while(lfsr != 1u); fclose( pFile ); } /**Function************************************************************* Synopsis [Creates a sequence of random numbers.] Description [] SideEffects [] SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx] ***********************************************************************/ void Aig_ManRandomTest1() { FILE * pFile; unsigned int lfsr; unsigned int period = 0; pFile = fopen( "rand.txt", "w" ); do { lfsr = Aig_ManRandom( 0 ); ++period; fprintf( pFile, "%10d : %10d ", period, lfsr ); // Extra_PrintBinary( pFile, &lfsr, 32 ); fprintf( pFile, "\n" ); if ( period == 20000 ) break; } while(lfsr != 1u); fclose( pFile ); } #define NUMBER1 3716960521u #define NUMBER2 2174103536u /**Function************************************************************* Synopsis [Creates a sequence of random numbers.] Description [] SideEffects [] SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx] ***********************************************************************/ unsigned Aig_ManRandom( int fReset ) { static unsigned int m_z = NUMBER1; static unsigned int m_w = NUMBER2; if ( fReset ) { m_z = NUMBER1; m_w = NUMBER2; } m_z = 36969 * (m_z & 65535) + (m_z >> 16); m_w = 18000 * (m_w & 65535) + (m_w >> 16); return (m_z << 16) + m_w; } /**Function************************************************************* Synopsis [Creates a sequence of random numbers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ word Aig_ManRandom64( int fReset ) { word Res = (word)Aig_ManRandom(fReset); return Res | ((word)Aig_ManRandom(0) << 32); } /**Function************************************************************* Synopsis [Creates random info for the primary inputs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ) { unsigned * pInfo; int i, w; Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart ) for ( w = iWordStart; w < iWordStop; w++ ) pInfo[w] = Aig_ManRandom(0); } /**Function************************************************************* Synopsis [Returns the result of merging the two vectors.] Description [Assumes that the vectors are sorted in the increasing order.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) { Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) ); pBeg = (Aig_Obj_t **)vArr->pArray; while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { if ( (*pBeg1)->Id == (*pBeg2)->Id ) *pBeg++ = *pBeg1++, pBeg2++; else if ( (*pBeg1)->Id < (*pBeg2)->Id ) *pBeg++ = *pBeg1++; else *pBeg++ = *pBeg2++; } while ( pBeg1 < pEnd1 ) *pBeg++ = *pBeg1++; while ( pBeg2 < pEnd2 ) *pBeg++ = *pBeg2++; vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; assert( vArr->nSize <= vArr->nCap ); assert( vArr->nSize >= vArr1->nSize ); assert( vArr->nSize >= vArr2->nSize ); } /**Function************************************************************* Synopsis [Returns the result of intersecting the two vectors.] Description [Assumes that the vectors are sorted in the increasing order.] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) { Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) ); pBeg = (Aig_Obj_t **)vArr->pArray; while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { if ( (*pBeg1)->Id == (*pBeg2)->Id ) *pBeg++ = *pBeg1++, pBeg2++; else if ( (*pBeg1)->Id < (*pBeg2)->Id ) // *pBeg++ = *pBeg1++; pBeg1++; else // *pBeg++ = *pBeg2++; pBeg2++; } // while ( pBeg1 < pEnd1 ) // *pBeg++ = *pBeg1++; // while ( pBeg2 < pEnd2 ) // *pBeg++ = *pBeg2++; vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; assert( vArr->nSize <= vArr->nCap ); assert( vArr->nSize <= vArr1->nSize ); assert( vArr->nSize <= vArr2->nSize ); } ABC_NAMESPACE_IMPL_END #include "proof/fra/fra.h" #include "aig/saig/saig.h" ABC_NAMESPACE_IMPL_START extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex ); extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig ); extern int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame ); /**Function************************************************************* Synopsis [Starts the process of retuning values for internal nodes.] Description [Should be called when pCex is available, before probing any object for its value using Aig_ManCounterExampleValueLookup().] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex ) { Aig_Obj_t * pObj, * pObjRi, * pObjRo; int Val0, Val1, nObjs, i, k, iBit = 0; assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak // allocate memory to store simulation bits for internal nodes pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) ); // the register values in the counter-example should be zero Saig_ManForEachLo( pAig, pObj, k ) assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 ); // iterate through the timeframes nObjs = Aig_ManObjNumMax(pAig); for ( i = 0; i <= pCex->iFrame; i++ ) { // set constant 1 node Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 ); // set primary inputs according to the counter-example Saig_ManForEachPi( pAig, pObj, k ) if ( Abc_InfoHasBit(pCex->pData, iBit++) ) Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); // compute values for each node Aig_ManForEachNode( pAig, pObj, k ) { Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) ); Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) ); if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) ) Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); } // derive values for combinational outputs Aig_ManForEachCo( pAig, pObj, k ) { Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) ); if ( Val0 ^ Aig_ObjFaninC0(pObj) ) Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); } if ( i == pCex->iFrame ) continue; // transfer values to the register output of the next frame Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) ) Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) ); } assert( iBit == pCex->nBits ); // check that the counter-example is correct, that is, the corresponding output is asserted assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManCo(pAig, pCex->iPo)) ) ); } /**Function************************************************************* Synopsis [Stops the process of retuning values for internal nodes.] Description [Should be called when probing is no longer needed] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig ) { assert( pAig->pData2 != NULL ); // if this fail, we try to call this procedure more than once free( pAig->pData2 ); pAig->pData2 = NULL; } /**Function************************************************************* Synopsis [Returns the value of the given object in the given timeframe.] Description [Should be called to probe the value of an object with the given ID (iFrame is a 0-based number of a time frame - should not exceed the number of timeframes in the original counter-example).] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame ) { assert( Id >= 0 && Id < Aig_ManObjNumMax(pAig) ); return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNumMax(pAig) * iFrame + Id ); } /**Function************************************************************* Synopsis [Procedure to test the above code.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex ) { Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNumMax(pAig)/2 ); int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 ); printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame ); Aig_ManCounterExampleValueStart( pAig, pCex ); printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame, Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) ); Aig_ManCounterExampleValueStop( pAig ); } /**Function************************************************************* Synopsis [Handle the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManSetPhase( Aig_Man_t * pAig ) { Aig_Obj_t * pObj; int i; // set the PI simulation information Aig_ManConst1( pAig )->fPhase = 1; Aig_ManForEachCi( pAig, pObj, i ) pObj->fPhase = 0; // simulate internal nodes Aig_ManForEachNode( pAig, pObj, i ) pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) ); // simulate PO nodes Aig_ManForEachCo( pAig, pObj, i ) pObj->fPhase = Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj); } /**Function************************************************************* Synopsis [Collects muxes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig ) { Vec_Ptr_t * vMuxes; Aig_Obj_t * pObj; int i; vMuxes = Vec_PtrAlloc( 100 ); Aig_ManForEachNode( pAig, pObj, i ) if ( Aig_ObjIsMuxType(pObj) ) Vec_PtrPush( vMuxes, pObj ); return vMuxes; } /**Function************************************************************* Synopsis [Dereferences muxes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes ) { Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC; int i; Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i ) { if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) ) { pNodeT->nRefs--; pNodeE->nRefs--; } else { pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE ); pNodeC->nRefs--; } } } /**Function************************************************************* Synopsis [References muxes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes ) { Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC; int i; Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i ) { if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) ) { pNodeT->nRefs++; pNodeE->nRefs++; } else { pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE ); pNodeC->nRefs++; } } } /**Function************************************************************* Synopsis [Complements the constraint outputs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_ManInvertConstraints( Aig_Man_t * pAig ) { Aig_Obj_t * pObj; int i; if ( Aig_ManConstrNum(pAig) == 0 ) return; Saig_ManForEachPo( pAig, pObj, i ) { if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) ) Aig_ObjChild0Flip( pObj ); } } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END