diff options
Diffstat (limited to 'abc70930/src/base/abci/abcDar.c')
-rw-r--r-- | abc70930/src/base/abci/abcDar.c | 1212 |
1 files changed, 0 insertions, 1212 deletions
diff --git a/abc70930/src/base/abci/abcDar.c b/abc70930/src/base/abci/abcDar.c deleted file mode 100644 index 90fe35e9..00000000 --- a/abc70930/src/base/abci/abcDar.c +++ /dev/null @@ -1,1212 +0,0 @@ -/**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 ) -{ - sat_solver * pSat; - Aig_Man_t * pMan; - Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); - Vec_Int_t * vCiIds; - - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkLatchNum(pNtk) == 0 ); - assert( Abc_NtkPoNum(pNtk) == 1 ); - - // conver to the manager - pMan = Abc_NtkToDar( pNtk, 0 ); - // derive CNF - pCnf = Cnf_Derive( pMan, 0 ); -// pCnf = Cnf_DeriveSimple( pMan, 0 ); - // convert into the SAT solver - pSat = Cnf_DataWriteIntoSolver( pCnf ); - vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); - Aig_ManStop( pMan ); - Cnf_DataFree( pCnf ); - // solve SAT - if ( pSat == NULL ) - { - Vec_IntFree( vCiIds ); -// printf( "Trivially unsat\n" ); - return 1; - } - - -// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - - // simplify the problem - clk = clock(); - status = sat_solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - if ( status == 0 ) - { - Vec_IntFree( vCiIds ); - sat_solver_delete( pSat ); -// printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 1; - } - - // solve the miter - clk = clock(); - if ( fVerbose ) - pSat->verbosity = 1; - status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 ); - if ( status == l_Undef ) - { -// printf( "The problem timed out.\n" ); - RetValue = -1; - } - else if ( status == l_True ) - { -// printf( "The problem is SATISFIABLE.\n" ); - RetValue = 0; - } - else if ( status == l_False ) - { -// printf( "The problem is UNSATISFIABLE.\n" ); - RetValue = 1; - } - else - assert( 0 ); -// PRT( "SAT sat_solver time", clock() - clk ); -// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); - - // if the problem is SAT, get the counterexample - if ( status == l_True ) - { - pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - } - // free the sat_solver - if ( fVerbose ) - Sat_SolverPrintStats( stdout, pSat ); -//sat_solver_store_write( pSat, "trace.cnf" ); -//sat_solver_store_free( pSat ); - sat_solver_delete( pSat ); - Vec_IntFree( vCiIds ); - 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 /// -//////////////////////////////////////////////////////////////////////// - - |