diff options
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 1245 |
1 files changed, 1245 insertions, 0 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c new file mode 100644 index 00000000..abf79a82 --- /dev/null +++ b/src/base/abci/abcDar.c @@ -0,0 +1,1245 @@ +/**CFile**************************************************************** + + FileName [abcDar.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [DAG-aware rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "aig.h" +#include "dar.h" +#include "cnf.h" +#include "fra.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [Assumes that registers are ordered after PIs/POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) +{ + Aig_Man_t * pMan; + Aig_Obj_t * pObjNew; + Abc_Obj_t * pObj; + int i, nNodes, nDontCares; + // make sure the latches follow PIs/POs + if ( fRegisters ) + { + assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( i < Abc_NtkPiNum(pNtk) ) + assert( Abc_ObjIsPi(pObj) ); + else + assert( Abc_ObjIsBo(pObj) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + if ( i < Abc_NtkPoNum(pNtk) ) + assert( Abc_ObjIsPo(pObj) ); + else + assert( Abc_ObjIsBi(pObj) ); + // print warning about initial values + nDontCares = 0; + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_LatchIsInitDc(pObj) ) + { + Abc_LatchSetInit0(pObj); + nDontCares++; + } + if ( nDontCares ) + { + printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares ); + printf( "The don't-care are assumed to be 0. The result may not verify.\n" ); + printf( "Use command \"print_latch\" to see the init values of registers.\n" ); + printf( "Use command \"init\" to change the values.\n" ); + } + } + // create the manager + pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); + pMan->pName = Extra_UtilStrsav( pNtk->pName ); + // save the number of registers + if ( fRegisters ) + { + pMan->nRegs = Abc_NtkLatchNum(pNtk); + pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); + } + // transfer the pointers to the basic nodes + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan); + // complement the 1-values registers + if ( fRegisters ) + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_LatchIsInit1(pObj) ) + Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); + // perform the conversion of the internal nodes (assumes DFS ordering) +// pMan->fAddStrash = 1; + Abc_NtkForEachNode( pNtk, pObj, i ) + { + pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) ); +// printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id ); + } + pMan->fAddStrash = 0; + // create the POs + Abc_NtkForEachCo( pNtk, pObj, i ) + Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); + // complement the 1-valued registers + if ( fRegisters ) + Aig_ManForEachLiSeq( pMan, pObjNew, i ) + if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) ) + pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0); + // remove dangling nodes + if ( nNodes = Aig_ManCleanup( pMan ) ) + printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes ); +//Aig_ManDumpVerilog( pMan, "test.v" ); + if ( !Aig_ManCheck( pMan ) ) + { + printf( "Abc_NtkToDar: AIG check has failed.\n" ); + Aig_ManStop( pMan ); + return NULL; + } + return pMan; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew; + Aig_Obj_t * pObj; + int i; +// assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + { + if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) + break; + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + // if there are assertions, add them + if ( pMan->nAsserts > 0 ) + Aig_ManForEachAssert( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreateAssert(pNtkNew); + Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); + Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [This procedure should be called after seq sweeping, + which changes the number of registers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pLatch; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i; +// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPiSeq( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // create as many latches as there are registers in the manager + Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) + { + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pObjLi->pData = Abc_NtkCreateBi( pNtkNew ); + pObjLo->pData = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pObjLi->pData ); + Abc_ObjAddFanin( pObjLo->pData, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + } + if ( pMan->vFlopNums == NULL ) + Abc_NtkAddDummyBoxNames( pNtkNew ); + else + { + assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) + { + pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL ); + } + } + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + { + if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) + break; + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + // if there are assertions, add them + if ( pMan->nAsserts > 0 ) + Aig_ManForEachAssert( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreateAssert(pNtkNew); + Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); + Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Aig_Obj_t * pObj, * pTemp; + int i; + assert( pMan->pEquivs != NULL ); + assert( Aig_ManBufNum(pMan) == 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + + // rebuild the AIG + vNodes = Aig_ManDfsChoices( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + if ( pTemp = pMan->pEquivs[pObj->Id] ) + { + Abc_Obj_t * pAbcRepr, * pAbcObj; + assert( pTemp->pData != NULL ); + pAbcRepr = pObj->pData; + pAbcObj = pTemp->pData; + pAbcObj->pData = pAbcRepr->pData; + pAbcRepr->pData = pAbcObj; + } + } +//printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Aig_Obj_t * pObj; + int i; +// assert( Aig_ManLatchNum(pMan) > 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkPi(pNtkNew, i); + // create latches of the new network + Aig_ManForEachObj( pMan, pObj, i ) + { + if ( !Aig_ObjIsLatch(pObj) ) + continue; + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pFaninNew0 = Abc_NtkCreateBi( pNtkNew ); + pFaninNew1 = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + pObj->pData = Abc_ObjFanout0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // add the first fanin + pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + if ( Aig_ObjIsBuf(pObj) ) + continue; + // add the second fanin + pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj); + // create the new node + if ( Aig_ObjIsExor(pObj) ) + pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + else + pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + } + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + { + pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew ); + } + // connect the latches + Aig_ManForEachObj( pMan, pObj, i ) + { + if ( !Aig_ObjIsLatch(pObj) ) + continue; + pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Collect latch values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vInits; + Abc_Obj_t * pLatch; + int i; + vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + assert( Abc_LatchIsInit1(pLatch) == 0 ); + Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) ); + } + return vInits; +} + +/**Function************************************************************* + + Synopsis [Performs verification after retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +{ + int fRemove1, fRemove2; + Aig_Man_t * pMan1, * pMan2; + int * pArray; + + fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0)); + fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0)); + + + pMan1 = Abc_NtkToDar( pNtk1, 0 ); + pMan2 = Abc_NtkToDar( pNtk2, 0 ); + + Aig_ManPrintStats( pMan1 ); + Aig_ManPrintStats( pMan2 ); + +// pArray = Abc_NtkGetLatchValues(pNtk1); + pArray = NULL; + Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray ); + free( pArray ); + +// pArray = Abc_NtkGetLatchValues(pNtk2); + pArray = NULL; + Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray ); + free( pArray ); + + Aig_ManPrintStats( pMan1 ); + Aig_ManPrintStats( pMan2 ); + + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + + + if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); + if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig = NULL; + Aig_Man_t * pMan; + extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ); + + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + + // perform computation +// Fra_ManPartitionTest( pMan, 4 ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + + // make sure everything is okay + if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkDar: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose ) +{ + Fra_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = nConfLimit; + pPars->fChoicing = fChoicing; + pPars->fDoSparse = fDoSparse; + pPars->fSpeculate = fSpeculate; + pPars->fProve = fProve; + pPars->fVerbose = fVerbose; + pMan = Fra_FraigPerform( pTemp = pMan, pPars ); + if ( fChoicing ) + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pTemp ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose ) +{ + extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pTemp ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManPrintStats( pMan ); +/* +// Aig_ManSupports( pMan ); + { + Vec_Vec_t * vParts; + vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL ); + Vec_VecFree( vParts ); + } +*/ + Dar_ManRewrite( pMan, pPars ); +// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); +// Aig_ManStop( pTemp ); + +clk = clock(); + pMan = Aig_ManDup( pTemp = pMan, 0 ); + Aig_ManStop( pTemp ); +//PRT( "time", clock() - clk ); + +// Aig_ManPrintStats( pMan ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManPrintStats( pMan ); + + Dar_ManRefactor( pMan, pPars ); +// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); +// Aig_ManStop( pTemp ); + +clk = clock(); + pMan = Aig_ManDup( pTemp = pMan, 0 ); + Aig_ManStop( pTemp ); +//PRT( "time", clock() - clk ); + +// Aig_ManPrintStats( pMan ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManPrintStats( pMan ); + +clk = clock(); + pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); + Aig_ManStop( pTemp ); +//PRT( "time", clock() - clk ); + +// Aig_ManPrintStats( pMan ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); + Aig_ManStop( pTemp ); + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManPrintStats( pMan ); + +clk = clock(); + pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); + Aig_ManStop( pTemp ); +//PRT( "time", clock() - clk ); + +// Aig_ManPrintStats( pMan ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + Aig_Obj_t * pObj, * pLeaf; + Cnf_Cut_t * pCut; + Vec_Int_t * vCover; + unsigned uTruth; + int i, k, nDupGates; + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // make the mapper point to the new network + Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pNode, i ) + Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy; + // process the nodes in topological order + vCover = Vec_IntAlloc( 1 << 16 ); + Vec_PtrForEachEntry( vMapped, pObj, i ) + { + // create new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add fanins according to the cut + pCut = pObj->pData; + Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) + Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); + // add logic function + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); + } + else + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); + // save the node + pObj->pData = pNodeNew; + } + Vec_IntFree( vCover ); + // add the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pObj = Aig_ManPo(p->pManAig, i); + pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + + // remove the constant node if not used + pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData; + if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) + Abc_NtkDeleteObj( pNodeNew ); + // minimize the node +// Abc_NtkSweep( pNtkNew, 0 ); + // decouple the PO driver nodes to reduce the number of levels + nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); +// if ( nDupGates && If_ManReadVerbose(pIfMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Vec_Ptr_t * vMapped; + Aig_Man_t * pMan; + Cnf_Man_t * pManCnf; + Cnf_Dat_t * pCnf; + Abc_Ntk_t * pNtkNew = NULL; + assert( Abc_NtkIsStrash(pNtk) ); + + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + if ( !Aig_ManCheck( pMan ) ) + { + printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); + Aig_ManStop( pMan ); + return NULL; + } + // perform balance + Aig_ManPrintStats( pMan ); + + // derive CNF + pCnf = Cnf_Derive( pMan, 0 ); + pManCnf = Cnf_ManRead(); + + // write the network for verification + vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 ); + pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped ); + Vec_PtrFree( vMapped ); + + // write CNF into a file + Cnf_DataWriteIntoFile( pCnf, pFileName, 0 ); + Cnf_DataFree( pCnf ); + Cnf_ClearMemory(); + + Aig_ManStop( pMan ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Solves combinational miter using a SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +{ + Aig_Man_t * pMan; + int RetValue;//, clk = clock(); + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + pMan = Abc_NtkToDar( pNtk, 0 ); + RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); + pNtk->pModel = pMan->pData, pMan->pData = NULL; + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose ) +{ + Aig_Man_t * pMan, * pMan1, * pMan2; + Abc_Ntk_t * pMiter; + int RetValue, clkTotal = clock(); + + // cannot partition if it is already a miter + if ( pNtk2 == NULL && fPartition == 1 ) + { + printf( "Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" ); + fPartition = 0; + } + + // if partitioning is selected, call partitioned CEC + if ( fPartition ) + { + pMan1 = Abc_NtkToDar( pNtk1, 0 ); + pMan2 = Abc_NtkToDar( pNtk2, 0 ); + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, fVerbose ); + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + goto finish; + } + + if ( pNtk2 != NULL ) + { + // get the miter of the two networks + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + if ( pMiter == NULL ) + { + printf( "Miter computation has failed.\n" ); + return 0; + } + } + else + { + pMiter = Abc_NtkDup( pNtk1 ); + } + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { +// extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + if ( pNtk2 == NULL ) + pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 ); +// pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); +// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); +// FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } + + // derive the AIG manager + pMan = Abc_NtkToDar( pMiter, 0 ); + Abc_NtkDelete( pMiter ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + // perform verification + RetValue = Fra_FraigCec( &pMan, fVerbose ); + // transfer model if given + if ( pNtk2 == NULL ) + pNtk1->pModel = pMan->pData, pMan->pData = NULL; + Aig_ManStop( pMan ); + +finish: + // report the miter + if ( RetValue == 1 ) + { + printf( "Networks are equivalent. " ); +PRT( "Time", clock() - clkTotal ); + } + else if ( RetValue == 0 ) + { + printf( "Networks are NOT EQUIVALENT. " ); +PRT( "Time", clock() - clkTotal ); + } + else + { + printf( "Networks are UNDECIDED. " ); +PRT( "Time", clock() - clkTotal ); + } + fflush( stdout ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ) +{ + Fraig_Params_t Params; + Abc_Ntk_t * pNtkAig, * pNtkFraig; + Aig_Man_t * pMan, * pTemp; + int clk = clock(); + + // preprocess the miter by fraiging it + // (note that for each functional class, fraiging leaves one representative; + // so fraiging does not reduce the number of functions represented by nodes + Fraig_ParamsSetDefault( &Params ); + Params.nBTLimit = 100000; +// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + pNtkFraig = Abc_NtkDup( pNtk ); +if ( fVerbose ) +{ +PRT( "Initial fraiging time", clock() - clk ); +} + + pMan = Abc_NtkToDar( pNtkFraig, 1 ); + Abc_NtkDelete( pNtkFraig ); + if ( pMan == NULL ) + return NULL; + + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL ); + Aig_ManStop( pTemp ); + + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Computes latch correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL ); + Aig_ManStop( pTemp ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +{ + Aig_Man_t * pMan; + int RetValue; + // derive the AIG manager + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + // perform verification + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +{ +// Fraig_Params_t Params; + Aig_Man_t * pMan; + Abc_Ntk_t * pMiter;//, * pTemp; + int RetValue; + + // get the miter of the two networks + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + if ( pMiter == NULL ) + { + printf( "Miter computation has failed.\n" ); + return 0; + } + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } + + // commented out because something became non-inductive +/* + // preprocess the miter by fraiging it + // (note that for each functional class, fraiging leaves one representative; + // so fraiging does not reduce the number of functions represented by nodes + Fraig_ParamsSetDefault( &Params ); + Params.nBTLimit = 100000; + pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 ); + Abc_NtkDelete( pTemp ); + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } +*/ + // derive the AIG manager + pMan = Abc_NtkToDar( pMiter, 1 ); + Abc_NtkDelete( pMiter ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + + // perform verification + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + Aig_ManSeqCleanup( pMan ); + if ( fLatchSweep ) + { + if ( pMan->nRegs ) + pMan = Aig_ManReduceLaches( pMan, fVerbose ); + if ( pMan->nRegs ) + pMan = Aig_ManConstReduce( pMan, fVerbose ); + } + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; +// Aig_ManReduceLachesCount( pMan ); + + pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 ); + Aig_ManStop( pTemp ); + +// pMan = Aig_ManReduceLaches( pMan, 1 ); +// pMan = Aig_ManConstReduce( pMan, 1 ); + + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |