/**CFile**************************************************************** FileName [abcVanImp.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] Synopsis [Implementation of van Eijk's method for implications.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - October 2, 2005.] Revision [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "abc.h" #include "fraig.h" #include "sim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Van_Man_t_ Van_Man_t; struct Van_Man_t_ { // single frame representation Abc_Ntk_t * pNtkSingle; // single frame Vec_Int_t * vCounters; // the counters of 1s in the simulation info Vec_Ptr_t * vZeros; // the set of constant 0 candidates Vec_Int_t * vImps; // the set of all implications Vec_Int_t * vImpsMis; // the minimum independent set of implications // multiple frame representation Abc_Ntk_t * pNtkMulti; // multiple frame Vec_Ptr_t * vCorresp; // the correspondence between single frame and multiple frames // parameters int nFrames; // the number of timeframes int nWords; // the number of simulation words int nIdMax; // the maximum ID in the single frame int fVerbose; // the verbosiness flag // statistics int nPairsAll; int nImpsAll; int nEquals; int nZeros; // runtime int timeAll; int timeSim; int timeAdd; int timeCheck; int timeInfo; int timeMis; }; static void Abc_NtkVanImpCompute( Van_Man_t * p ); static Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ); static void Abc_NtkVanImpComputeAll( Van_Man_t * p ); static Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ); static void Abc_NtkVanImpManFree( Van_Man_t * p ); static void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); static int Abc_NtkVanImpCountEqual( Van_Man_t * p ); static Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); //////////////////////////////////////////////////////////////////////// /// INLINED FUNCTIONS /// //////////////////////////////////////////////////////////////////////// // returns the correspondence of the node in the frame static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) { return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); } // returns the left node of the implication static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp ) { return Abc_NtkObj( pNtk, Imp >> 16 ); } // returns the right node of the implication static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp ) { return Abc_NtkObj( pNtk, Imp & 0xFFFF ); } // returns the implication static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight ) { return (pLeft->Id << 16) | pRight->Id; } // returns the right node of the implication static inline void Abc_NodeVanPrintImp( unsigned Imp ) { printf( "%d -> %d ", Imp >> 16, Imp & 0xFFFF ); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Derives implications that hold sequentially.] Description [Adds EXDC network to the current network to record the set of computed sequentially equivalence implications, representing a subset of unreachable states.] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkNew; Van_Man_t * p; assert( Abc_NtkIsStrash(pNtk) ); // start the manager p = ALLOC( Van_Man_t, 1 ); memset( p, 0, sizeof(Van_Man_t) ); p->nFrames = nFrames; p->fVerbose = fVerbose; p->vCorresp = Vec_PtrAlloc( 100 ); // FRAIG the network to get rid of combinational equivalences Fraig_ParamsSetDefaultFull( &Params ); p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); p->nIdMax = Abc_NtkObjNumMax( p->pNtkSingle ); Abc_AigSetNodePhases( p->pNtkSingle ); Abc_NtkCleanNext( p->pNtkSingle ); // if ( fVerbose ) // printf( "The number of ANDs in 1 timeframe = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) ); // derive multiple time-frames and node correspondence (to be used in the inductive case) p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 ); // if ( fVerbose ) // printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) ); // get the implications Abc_NtkVanImpCompute( p ); // create the new network with EXDC correspondingn to the computed implications if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) ) { if ( p->pNtkSingle->pExdc ) { printf( "The old EXDC network is thrown away.\n" ); Abc_NtkDelete( p->pNtkSingle->pExdc ); p->pNtkSingle->pExdc = NULL; } pNtkNew = Abc_NtkDup( p->pNtkSingle ); pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis ); } else pNtkNew = Abc_NtkDup( p->pNtkSingle ); // free stuff Abc_NtkVanImpManFree( p ); return pNtkNew; } /**Function************************************************************* Synopsis [Frees the manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanImpManFree( Van_Man_t * p ) { Abc_NtkDelete( p->pNtkMulti ); Abc_NtkDelete( p->pNtkSingle ); Vec_PtrFree( p->vCorresp ); Vec_PtrFree( p->vZeros ); Vec_IntFree( p->vCounters ); Vec_IntFree( p->vImpsMis ); Vec_IntFree( p->vImps ); free( p ); } /**Function************************************************************* Synopsis [Derives the minimum independent set of sequential implications.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanImpCompute( Van_Man_t * p ) { Fraig_Man_t * pFraig; Vec_Ptr_t * vZeros; Vec_Int_t * vImps, * vImpsTemp; int nIters, clk; // compute all implications and count 1s in the simulation info clk = clock(); Abc_NtkVanImpComputeAll( p ); p->timeAll += clock() - clk; // compute the MIS clk = clock(); p->vImpsMis = Abc_NtkVanImpComputeMis( p ); p->timeMis += clock() - clk; if ( p->fVerbose ) { printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n", p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros ); PRT( "Visiting all nodes pairs while preparing for the inductive case", p->timeAll ); printf( "Start : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); } // iterate to perform the iterative filtering of implications for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ ) { // FRAIG the ununitialized frames pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 ); // assuming that zeros and imps hold in the first k-1 frames // check if they hold in the k-th frame vZeros = Vec_PtrAlloc( 100 ); vImps = Vec_IntAlloc( 100 ); Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps ); Fraig_ManFree( pFraig ); clk = clock(); vImpsTemp = p->vImps; p->vImps = vImps; Vec_IntFree( p->vImpsMis ); p->vImpsMis = Abc_NtkVanImpComputeMis( p ); p->vImps = vImpsTemp; p->timeMis += clock() - clk; // report the results if ( p->fVerbose ) printf( "Iter = %2d: Seq = %7d. MIS = %7d. Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) ); // if the fixed point is reaches, quit the loop if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) ) { // no change Vec_PtrFree(vZeros); Vec_IntFree(vImps); break; } // update the sets Vec_PtrFree( p->vZeros ); p->vZeros = vZeros; Vec_IntFree( p->vImps ); p->vImps = vImps; } // compute the MIS clk = clock(); Vec_IntFree( p->vImpsMis ); p->vImpsMis = Abc_NtkVanImpComputeMis( p ); // p->vImpsMis = Vec_IntDup( p->vImps ); p->timeMis += clock() - clk; if ( p->fVerbose ) printf( "Final : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); /* if ( p->fVerbose ) { PRT( "All ", p->timeAll ); PRT( "Sim ", p->timeSim ); PRT( "Add ", p->timeAdd ); PRT( "Check ", p->timeCheck ); PRT( "Mis ", p->timeMis ); } */ /* // print the implications in the MIS if ( p->fVerbose ) { Abc_Obj_t * pNode, * pNode1, * pNode2; unsigned Imp; int i; if ( Vec_PtrSize(p->vZeros) ) { printf( "The const nodes are: " ); Vec_PtrForEachEntry( p->vZeros, pNode, i ) printf( "%d(%d) ", pNode->Id, pNode->fPhase ); printf( "\n" ); } if ( Vec_IntSize(p->vImpsMis) ) { printf( "The implications are: " ); Vec_IntForEachEntry( p->vImpsMis, Imp, i ) { pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); } printf( "\n" ); } } */ } /**Function************************************************************* Synopsis [Filters zeros and implications by performing one inductive step.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) { ProgressBar * pProgress; Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj; Fraig_Node_t * pFNode1, * pFNode2; Fraig_Node_t * ppFNodes[2]; unsigned Imp; int i, f, k, clk; clk = clock(); for ( f = 0; f < p->nFrames; f++ ) { // add new clauses for zeros Vec_PtrForEachEntry( p->vZeros, pNode, i ) { pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f ); pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase ); Fraig_ManAddClause( pFraig, &pFNode1, 1 ); } // add new clauses for imps Vec_IntForEachEntry( p->vImps, Imp, i ) { pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f ); pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f ); pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase ); ppFNodes[1] = Fraig_NotCond( pFNode2, pNode2->fPhase ); // assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) ); Fraig_ManAddClause( pFraig, ppFNodes, 2 ); } } p->timeAdd += clock() - clk; // check the zero nodes clk = clock(); Vec_PtrClear( vZeros ); Vec_PtrForEachEntry( p->vZeros, pNode, i ) { pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames ); pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); pFNode1 = Fraig_Regular(pFNode1); pFNode2 = Fraig_ManReadConst1(pFraig); if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) Vec_PtrPush( vZeros, pNode ); else { // since we disproved this zero, we should add all possible implications to p->vImps // these implications will be checked below and only correct ones will remain Abc_NtkForEachObj( p->pNtkSingle, pObj, k ) { if ( Abc_ObjIsPo(pObj) ) continue; if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 ) Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) ); } } } // check implications pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize ); Vec_IntClear( vImps ); Vec_IntForEachEntry( p->vImps, Imp, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames ); pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames ); pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase ); pFNode2 = Fraig_NotCond( pFNode2, pNode2->fPhase ); if ( pFNode1 == Fraig_Not(pFNode2) ) { Vec_IntPush( vImps, Imp ); continue; } if ( pFNode1 == pFNode2 ) { if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) ) continue; if ( pFNode1 == Fraig_ManReadConst1(pFraig) ) { Vec_IntPush( vImps, Imp ); continue; } pFNode1 = Fraig_Regular(pFNode1); pFNode2 = Fraig_ManReadConst1(pFraig); if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) Vec_IntPush( vImps, Imp ); continue; } if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) ) Vec_IntPush( vImps, Imp ); } Extra_ProgressBarStop( pProgress ); p->timeCheck += clock() - clk; } /**Function************************************************************* Synopsis [Computes all implications.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanImpComputeAll( Van_Man_t * p ) { ProgressBar * pProgress; Fraig_Man_t * pManSingle; Vec_Ptr_t * vInfo; Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1; Fraig_Node_t * pFNode1, * pFNode2; unsigned * pPats1, * pPats2; int nFrames, nUnsigned, RetValue; int clk, i, k, Count1, Count2; // decide how many frames to simulate nFrames = 32; nUnsigned = 32; p->nWords = nFrames * nUnsigned; // simulate randomly the initialized frames clk = clock(); vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned ); // complement the info for those nodes whose phase is 1 Abc_NtkForEachObj( p->pNtkSingle, pObj, i ) if ( pObj->fPhase ) Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords ); // compute the number of ones for each node p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords ); p->timeSim += clock() - clk; // FRAIG the uninitialized frame pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 ); // now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes /* Abc_NtkForEachPi( p->pNtkSingle, pNode1, i ) printf( "PI = %d\n", pNode1->Id ); Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i ) printf( "Latch = %d\n", pNode1->Id ); Abc_NtkForEachPo( p->pNtkSingle, pNode1, i ) printf( "PO = %d\n", pNode1->Id ); */ // go through the pairs of signals in the frames pProgress = Extra_ProgressBarStart( stdout, p->nIdMax ); pConst1 = Abc_NtkConst1( p->pNtkSingle ); p->vImps = Vec_IntAlloc( 100 ); p->vZeros = Vec_PtrAlloc( 100 ); Abc_NtkForEachObj( p->pNtkSingle, pNode1, i ) { if ( Abc_ObjIsPo(pNode1) ) continue; if ( pNode1 == pConst1 ) continue; Extra_ProgressBarUpdate( pProgress, i, NULL ); // get the number of zeros of this node Count1 = Vec_IntEntry( p->vCounters, pNode1->Id ); if ( Count1 == 0 ) { Vec_PtrPush( p->vZeros, pNode1 ); p->nZeros++; continue; } pPats1 = Sim_SimInfoGet(vInfo, pNode1); Abc_NtkForEachObj( p->pNtkSingle, pNode2, k ) { if ( k >= i ) break; if ( Abc_ObjIsPo(pNode2) ) continue; if ( pNode2 == pConst1 ) continue; p->nPairsAll++; // here we have a pair of nodes (pNode1 and pNode2) // such that Id(pNode1) < Id(pNode2) assert( pNode2->Id < pNode1->Id ); // get the number of zeros of this node Count2 = Vec_IntEntry( p->vCounters, pNode2->Id ); if ( Count2 == 0 ) continue; pPats2 = Sim_SimInfoGet(vInfo, pNode2); // check for implications if ( Count1 < Count2 ) { //clk = clock(); RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords ); //p->timeInfo += clock() - clk; if ( !RetValue ) continue; p->nImpsAll++; // pPats1 => pPats2 or pPats1' v pPats2 pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase ); pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); // check if this implication is combinational if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) continue; // otherwise record it Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); } else if ( Count2 < Count1 ) { //clk = clock(); RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords ); //p->timeInfo += clock() - clk; if ( !RetValue ) continue; p->nImpsAll++; // pPats2 => pPats2 or pPats2' v pPats1 pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase ); pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); // check if this implication is combinational if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) continue; // otherwise record it Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); } else { //clk = clock(); RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords); //p->timeInfo += clock() - clk; if ( !RetValue ) continue; p->nEquals++; // get the FRAIG nodes pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); // check if this implication is combinational if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) ) { if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); else assert( 0 ); // impossible for FRAIG } else { Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); } } // printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); } } Fraig_ManFree( pManSingle ); Sim_UtilInfoFree( vInfo ); Extra_ProgressBarStop( pProgress ); } /**Function************************************************************* Synopsis [Sorts the nodes.] Description [Sorts the nodes appearing in the left-hand sides of the implications by the number of 1s in their simulation info.] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ) { Abc_Obj_t * pNode, * pList; Vec_Ptr_t * vSorted; unsigned Imp; int i, nOnes; // start the sorted array vSorted = Vec_PtrStart( p->nWords * 32 ); // go through the implications Abc_NtkIncrementTravId( p->pNtkSingle ); Vec_IntForEachEntry( p->vImps, Imp, i ) { pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); assert( !Abc_ObjIsPo(pNode) ); // if this node is already visited, skip if ( Abc_NodeIsTravIdCurrent( pNode ) ) continue; // mark the node as visited Abc_NodeSetTravIdCurrent( pNode ); // add the node to the list nOnes = Vec_IntEntry( p->vCounters, pNode->Id ); pList = Vec_PtrEntry( vSorted, nOnes ); pNode->pNext = pList; Vec_PtrWriteEntry( vSorted, nOnes, pNode ); } return vSorted; } /**Function************************************************************* Synopsis [Computes the array of beginnings.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p ) { Vec_Int_t * vBegins; unsigned Imp; int i, ItemLast, ItemCur; // sort the implications (by the number of the left-hand-side node) Vec_IntSort( p->vImps, 0 ); // start the array of beginnings vBegins = Vec_IntStart( p->nIdMax + 1 ); // mark the begining of each node's implications ItemLast = 0; Vec_IntForEachEntry( p->vImps, Imp, i ) { ItemCur = (Imp >> 16); if ( ItemCur == ItemLast ) continue; Vec_IntWriteEntry( vBegins, ItemCur, i ); ItemLast = ItemCur; } // fill in the empty spaces ItemLast = Vec_IntSize(p->vImps); Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast ); Vec_IntForEachEntryReverse( vBegins, ItemCur, i ) { if ( ItemCur == 0 ) Vec_IntWriteEntry( vBegins, i, ItemLast ); else ItemLast = ItemCur; } Imp = Vec_IntEntry( p->vImps, 0 ); ItemCur = (Imp >> 16); for ( i = 0; i <= ItemCur; i++ ) Vec_IntWriteEntry( vBegins, i, 0 ); return vBegins; } /**Function************************************************************* Synopsis [Derives the minimum subset of implications.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis ) { Vec_Int_t * vNexts; int i, Next; // if this node is already visited, skip if ( Abc_NodeIsTravIdCurrent( pNode ) ) return; // mark the node as visited Abc_NodeSetTravIdCurrent( pNode ); // mark the children vNexts = Vec_VecEntry( vImpsMis, pNode->Id ); Vec_IntForEachEntry( vNexts, Next, i ) Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis ); } /**Function************************************************************* Synopsis [Derives the minimum subset of implications.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ) { Abc_Obj_t * pNode, * pNext, * pList; Vec_Vec_t * vMatrix; Vec_Ptr_t * vSorted; Vec_Int_t * vBegins; Vec_Int_t * vImpsMis; int i, k, iStart, iStop; void * pEntry; unsigned Imp; if ( Vec_IntSize(p->vImps) == 0 ) return Vec_IntAlloc(0); // compute the sorted list of nodes by the number of 1s Abc_NtkCleanNext( p->pNtkSingle ); vSorted = Abc_NtkVanImpSortByOnes( p ); // compute the array of beginnings vBegins = Abc_NtkVanImpComputeBegs( p ); /* Vec_IntForEachEntry( p->vImps, Imp, i ) { printf( "%d: ", i ); Abc_NodeVanPrintImp( Imp ); } printf( "\n\n" ); Vec_IntForEachEntry( vBegins, Imp, i ) printf( "%d=%d ", i, Imp ); printf( "\n\n" ); */ // compute the MIS by considering nodes in the reverse order of ones vMatrix = Vec_VecStart( p->nIdMax ); Vec_PtrForEachEntryReverse( vSorted, pList, i ) { for ( pNode = pList; pNode; pNode = pNode->pNext ) { // get the starting and stopping implication of this node iStart = Vec_IntEntry( vBegins, pNode->Id ); iStop = Vec_IntEntry( vBegins, pNode->Id + 1 ); if ( iStart == iStop ) continue; assert( iStart < iStop ); // go through all the implications of this node Abc_NtkIncrementTravId( p->pNtkSingle ); Abc_NodeIsTravIdCurrent( pNode ); Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop ) { assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) ); pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp); // if this node is already visited, skip if ( Abc_NodeIsTravIdCurrent( pNext ) ) continue; assert( pNode->Id != pNext->Id ); // add implication Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id ); // recursively mark dependent nodes Abc_NtkVanImpMark_rec( pNext, vMatrix ); } } } Vec_IntFree( vBegins ); Vec_PtrFree( vSorted ); // transfer the MIS into the normal array vImpsMis = Vec_IntAlloc( 100 ); Vec_VecForEachEntry( vMatrix, pEntry, i, k ) { assert( (i << 16) != ((int)pEntry) ); Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) ); } Vec_VecFree( vMatrix ); return vImpsMis; } /**Function************************************************************* Synopsis [Count equal pairs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkVanImpCountEqual( Van_Man_t * p ) { Abc_Obj_t * pNode1, * pNode2, * pNode3; Vec_Int_t * vBegins; int iStart, iStop; unsigned Imp, ImpR; int i, k, Counter; // compute the array of beginnings vBegins = Abc_NtkVanImpComputeBegs( p ); // go through each node and out Counter = 0; Vec_IntForEachEntry( p->vImps, Imp, i ) { pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); if ( pNode1->Id > pNode2->Id ) continue; iStart = Vec_IntEntry( vBegins, pNode2->Id ); iStop = Vec_IntEntry( vBegins, pNode2->Id + 1 ); Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop ) { assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) ); pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR); if ( pNode1 == pNode3 ) { Counter++; break; } } } Vec_IntFree( vBegins ); return Counter; } /**Function************************************************************* Synopsis [Create EXDC from the equivalence classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) { Abc_Ntk_t * pNtkNew; Vec_Ptr_t * vCone; Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew; unsigned Imp; int i, k; assert( Abc_NtkIsStrash(pNtk) ); // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); pNtkNew->pName = Extra_UtilStrsav( "exdc" ); pNtkNew->pSpec = NULL; // map the constant nodes Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); // for each CI, create PI Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); // cannot add latches here because pLatch->pCopy pointers are used // build logic cone for zero nodes pTotal = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); Vec_PtrForEachEntry( vZeros, pNode, i ) { // build the logic cone for the node if ( Abc_ObjFaninNum(pNode) == 2 ) { vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); Vec_PtrForEachEntry( vCone, pObj, k ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); Vec_PtrFree( vCone ); assert( pObj == pNode ); } // complement if there is phase difference pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ); // add it to the EXDC pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy ); } // create logic cones for the implications Vec_IntForEachEntry( vImps, Imp, i ) { pNode1 = Abc_NtkObj(pNtk, Imp >> 16); pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF); // build the logic cone for the first node if ( Abc_ObjFaninNum(pNode1) == 2 ) { vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 ); Vec_PtrForEachEntry( vCone, pObj, k ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); Vec_PtrFree( vCone ); assert( pObj == pNode1 ); } // complement if there is phase difference pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase ); // build the logic cone for the second node if ( Abc_ObjFaninNum(pNode2) == 2 ) { vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 ); Vec_PtrForEachEntry( vCone, pObj, k ) pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); Vec_PtrFree( vCone ); assert( pObj == pNode2 ); } // complement if there is phase difference pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase ); // build the implication and add it to the EXDC pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) ); pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); } /* // create the only PO pObjNew = Abc_NtkCreatePo( pNtkNew ); // add the PO name Abc_NtkLogicStoreName( pObjNew, "DC" ); // add the PO Abc_ObjAddFanin( pObjNew, pTotal ); // quontify the PIs existentially pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); // get the new PO pObjNew = Abc_NtkPo( pNtkNew, 0 ); // remember the miter output pTotal = Abc_ObjChild0( pObjNew ); // remove the PO Abc_NtkDeleteObj( pObjNew ); // make the old network point to the new things Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = Abc_NtkPi( pNtkNew, i ); */ // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") ); // link to the POs of the network Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) Abc_ObjAddFanin( pObj->pCopy, pTotal ); Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_ObjAddFanin( pObj->pCopy, pTotal ); // remove the extra nodes Abc_AigCleanup( pNtkNew->pManFunc ); // check the result if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); return NULL; } return pNtkNew; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////