diff options
Diffstat (limited to 'src')
31 files changed, 995 insertions, 493 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 6987412d..5861bc36 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -150,6 +150,8 @@ struct Aig_Man_t_ void * pSeqModel; Aig_Man_t * pManExdc; Vec_Ptr_t * vOnehots; + Aig_Man_t * pManHaig; + int fCreatePios; // timing statistics int time1; int time2; @@ -322,7 +324,8 @@ static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; } -static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; } +static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } +static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -469,11 +472,12 @@ extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ); extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ); /*=== aigDup.c ==========================================================*/ -extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ); -extern Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder ); +extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ); extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p ); @@ -487,15 +491,15 @@ extern void Aig_ManFanoutStart( Aig_Man_t * p ); extern void Aig_ManFanoutStop( Aig_Man_t * p ); /*=== aigFrames.c ==========================================================*/ extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap ); -/*=== aigHaig.c ==========================================================*/ -extern void Aig_ManHaigRecord( Aig_Man_t * p ); /*=== aigMan.c ==========================================================*/ extern Aig_Man_t * Aig_ManStart( int nNodesMax ); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ); extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); +extern int Aig_ManAntiCleanup( Aig_Man_t * p ); extern int Aig_ManPiCleanup( Aig_Man_t * p ); +extern int Aig_ManPoCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew ); extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs ); @@ -517,9 +521,9 @@ extern void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_ extern void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop ); -extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew ); -extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ); extern void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ); +extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew ); +extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel ); /*=== aigOper.c =========================================================*/ extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i ); extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index fc01e7f0..1ec92968 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -40,11 +40,13 @@ SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDup( Aig_Man_t * p ) +Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p ) { Aig_Man_t * pNew; Aig_Obj_t * pObj, * pObjNew; int i; + assert( p->pManTime == NULL ); + assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); @@ -88,12 +90,109 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p ) pObj->pData = pObjNew; } assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); - // duplicate the timing manager - if ( p->pManTime ) - pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; + p->pManHaig = NULL; + } // check the resulting network if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDup(): The check has failed.\n" ); + printf( "Aig_ManDupSimple(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return pObj->pData; + Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) ); + if ( Aig_ObjIsBuf(pObj) ) + return pObj->pData = Aig_ObjChild0Copy(pObj); + Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObj->pData)->pHaig = pObj->pHaig; + return pObj->pData; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager.] + + Description [Orders nodes as follows: PIs, ANDs, POs.] + + SideEffects [This procedure assumes that buffers are not used during + HAIG recording. This way, each HAIG node is in one-to-one correspondence + with old HAIG node. There is no need to create new nodes, just reassign + the pointers. If it were not the case, we would need to create HAIG nodes + for each new node duplicated. ] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i; + assert( p->pManTime == NULL ); + assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->nRegs = p->nRegs; + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = p->nTruePos; + pNew->nAsserts = p->nAsserts; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; + Aig_ManForEachPi( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePi( pNew ); + pObjNew->pHaig = pObj->pHaig; + pObjNew->Level = pObj->Level; + pObj->pData = pObjNew; + } + // duplicate internal nodes + Aig_ManForEachObj( p, pObj, i ) + if ( !Aig_ObjIsPo(pObj) ) + { + Aig_ManDupSimpleDfs_rec( pNew, p, pObj ); + assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level ); + } + // add the POs + Aig_ManForEachPo( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + pObjNew->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } + assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; + p->pManHaig = NULL; + } + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDupSimple(): The check has failed.\n" ); return pNew; } @@ -160,6 +259,12 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ) // duplicate the timing manager if ( p->pManTime ) pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; + p->pManHaig = NULL; + } // check the resulting network if ( !Aig_ManCheck(pNew) ) printf( "Aig_ManDupOrdered(): The check has failed.\n" ); @@ -255,7 +360,9 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj return pObj->pData = Aig_ObjChild0Copy(pObj); Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) ); pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) ); - if ( pObj->pHaig ) + if ( p->pManHaig != NULL ) + Aig_Regular(pObjNew)->pHaig = Aig_NotCond( pObj->pHaig, Aig_IsComplement(pObjNew) ); + else if ( pObj->pHaig ) Aig_Regular(pObjNew)->pHaig = pObj->pHaig; if ( pEquivNew ) { @@ -313,7 +420,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ) { pObjNew = Aig_ObjCreatePi( pNew ); pObjNew->Level = pObj->Level; - Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + pObjNew->pHaig = pObj->pHaig; pObj->pData = pObjNew; } else if ( Aig_ObjIsPo(pObj) ) @@ -321,7 +428,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ) Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) ); // assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level ); pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + pObjNew->pHaig = pObj->pHaig; pObj->pData = pObjNew; } } @@ -331,6 +438,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ) // duplicate the timing manager if ( p->pManTime ) pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; + p->pManHaig = NULL; + } // check the resulting network if ( !Aig_ManCheck(pNew) ) printf( "Aig_ManDupDfs(): The check has failed.\n" ); @@ -379,7 +492,7 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pObjNew, * pEquivNew = NULL; if ( pObj->pData ) @@ -387,12 +500,12 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * if ( Aig_ObjIsPi(pObj) ) return NULL; if ( p->pEquivs && Aig_ObjEquiv(p, pObj) ) - pEquivNew = Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjEquiv(p, pObj) ); - if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) ) ) + pEquivNew = Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjEquiv(p, pObj) ); + if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) ) ) return NULL; if ( Aig_ObjIsBuf(pObj) ) return pObj->pData = Aig_ObjChild0Copy(pObj); - if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin1(pObj) ) ) + if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) ) return NULL; pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) ); if ( pObj->pHaig ) @@ -418,7 +531,7 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder ) +Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ) { Vec_Ptr_t * vPios; Aig_Man_t * pNew; @@ -448,7 +561,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder ) // duplicate internal nodes Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; - vPios = Aig_ManOrderPios( p, pOrder ); + vPios = Aig_ManOrderPios( p, pGuide ); Vec_PtrForEachEntry( vPios, pObj, i ) { if ( Aig_ObjIsPi(pObj) ) @@ -460,7 +573,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder ) } else if ( Aig_ObjIsPo(pObj) ) { - Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) ); + Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) ); // assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level ); pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); Aig_Regular(pObjNew)->pHaig = pObj->pHaig; diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c deleted file mode 100644 index 491a09a3..00000000 --- a/src/aig/aig/aigHaig.c +++ /dev/null @@ -1,271 +0,0 @@ -/**CFile**************************************************************** - - FileName [aigHaig.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [AIG package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "aig.h" -#include "satSolver.h" -#include "cnf.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline Aig_Obj_t * Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f ) { return ppMap[nFrames*pObj->Id + f]; } -static inline void Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; } -static inline Aig_Obj_t * Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } -static inline Aig_Obj_t * Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs speculative reduction for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame ) -{ - Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; - // skip nodes without representative - pObjRepr = pObj->pHaig; - if ( pObjRepr == NULL ) - return; - assert( !Aig_IsComplement(pObjRepr) ); - assert( pObjRepr->Id < pObj->Id ); - // get the new node - pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame ); - // get the new node of the representative - pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame ); - // if this is the same node, no need to add constraints - if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) - return; - // these are different nodes - perform speculative reduction - pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); - // set the new node - Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 ); - // add the constraint - pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); - pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); - pMiter = Aig_Not( pMiter ); - Aig_ObjCreatePo( pFrames, pMiter ); -} - -/**Function************************************************************* - - Synopsis [Prepares the inductive case with speculative reduction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; - Aig_Obj_t ** ppMap; - int i, k, f; - assert( nFrames >= 2 ); - assert( Aig_ManRegNum(pHaig) > 0 ); - assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) ); - - // create node mapping - ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames ); - memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames ); - - // start the frames - pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pHaig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec ); - pFrames->nRegs = pHaig->nRegs; - - // create PI nodes for the frames - for ( f = 0; f < nFrames; f++ ) - Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) ); - for ( f = 0; f < nFrames; f++ ) - Aig_ManForEachPiSeq( pHaig, pObj, i ) - Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) ); - // create latches for the first frame - Aig_ManForEachLoSeq( pHaig, pObj, i ) - Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) ); - - // add timeframes - for ( f = 0; f < nFrames; f++ ) - { - // mark the asserts - if ( f == nFrames - 1 ) - pFrames->nAsserts = Aig_ManPoNum(pFrames); - // constrain latch outputs and internal nodes - Aig_ManForEachObj( pHaig, pObj, i ) - { - if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL ) - { - Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); - } - else if ( Aig_ObjIsNode(pObj) ) - { - pObjNew = Aig_And( pFrames, - Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), - Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) ); - Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew ); - Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); - } - } - -/* - // set the constraints on the latch outputs - Aig_ManForEachLoSeq( pHaig, pObj, i ) - Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); - // add internal nodes of this frame - Aig_ManForEachNode( pHaig, pObj, i ) - { - pObjNew = Aig_And( pFrames, - Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), - Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) ); - Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew ); - Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f ); - } -*/ - // transfer latch inputs to the latch outputs - Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k ) - { - pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f); - Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew ); - } - } - - // remove dangling nodes - Aig_ManCleanup( pFrames ); - free( ppMap ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManHaigVerify( Aig_Man_t * pHaig ) -{ - int nBTLimit = 0; - Aig_Man_t * pFrames; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - Aig_Obj_t * pObj; - int i, Lit, RetValue, Counter; - int clk = clock(); - - // create time frames with speculative reduction and convert them into CNF -clk = clock(); - pFrames = Aig_ManHaigFrames( pHaig, 2 ); - pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); -// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); -//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); - // create the SAT solver to be used for this problem - pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - - printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n", - Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) ); - printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n", - Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames), - pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); - -PRT( "Preparation", clock() - clk ); - if ( pSat == NULL ) - { - printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); - return -1; - } - - // solve each output -clk = clock(); - Counter = 0; - Aig_ManForEachPo( pFrames, pObj, i ) - { - if ( i < pFrames->nAsserts ) - continue; - Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase ); - RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( RetValue != l_False ) - Counter++; - } -PRT( "Solving ", clock() - clk ); - if ( Counter ) - printf( "Verification failed for %d classes.\n", Counter ); - else - printf( "Verification is successful.\n" ); - - // clean up - Aig_ManStop( pFrames ); - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManHaigRecord( Aig_Man_t * p ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj; - int i; - // start the HAIG - p->pManHaig = Aig_ManDupOrdered( p ); - // set the pointers to the HAIG nodes - Aig_ManForEachObj( p, pObj, i ) - pObj->pHaig = pObj->pData; - // remove structural hashing table - Aig_TableClear( p->pManHaig ); - // perform a sequence of synthesis steps - pNew = Aig_ManRetimeFrontier( p, 10000 ); - // use the haig for verification - Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif", NULL, NULL ); - Aig_ManHaigVerify( pNew->pManHaig ); - Aig_ManStop( pNew ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 669691f4..9877fdae 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -163,7 +163,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * Aig_ObjCreatePo( pNew, pObj ); // check the resulting network if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDup(): The check has failed.\n" ); + printf( "Aig_ManExtractMiter(): The check has failed.\n" ); return pNew; } @@ -235,8 +235,7 @@ int Aig_ManCleanup( Aig_Man_t * p ) { Vec_Ptr_t * vObjs; Aig_Obj_t * pNode; - int i, nNodesOld; - nNodesOld = Aig_ManNodeNum(p); + int i, nNodesOld = Aig_ManNodeNum(p); // collect roots of dangling nodes vObjs = Vec_PtrAlloc( 100 ); Aig_ManForEachObj( p, pNode, i ) @@ -251,6 +250,27 @@ int Aig_ManCleanup( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Adds POs for the nodes that otherwise would be dangling.] + + Description [Returns the number of POs added.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManAntiCleanup( Aig_Man_t * p ) +{ + Aig_Obj_t * pNode; + int i, nNodesOld = Aig_ManPoNum(p); + Aig_ManForEachObj( p, pNode, i ) + if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 ) + Aig_ObjCreatePo( p, pNode ); + return nNodesOld - Aig_ManPoNum(p); +} + +/**Function************************************************************* + Synopsis [Removes PIs without fanouts.] Description [Returns the number of PIs removed.] @@ -282,6 +302,40 @@ int Aig_ManPiCleanup( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Removes POs with constant input.] + + Description [Returns the number of POs removed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManPoCleanup( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, k = 0, nPosOld = Aig_ManPoNum(p); + Vec_PtrForEachEntry( p->vPos, pObj, i ) + { + if ( i >= Aig_ManPoNum(p) - Aig_ManRegNum(p) ) + Vec_PtrWriteEntry( p->vPos, k++, pObj ); + else if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) || !Aig_ObjFaninC0(pObj) ) // non-const or const1 + Vec_PtrWriteEntry( p->vPos, k++, pObj ); + else + { + Aig_ObjDisconnect( p, pObj ); + Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); + } + } + Vec_PtrShrink( p->vPos, k ); + p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + if ( Aig_ManRegNum(p) ) + p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); + return nPosOld - Aig_ManPoNum(p); +} + +/**Function************************************************************* + Synopsis [Performs one iteration of AIG rewriting.] Description [] diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 73b15caf..b5a404ab 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -46,6 +46,12 @@ Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p ) pObj->Type = AIG_OBJ_PI; Vec_PtrPush( p->vPis, pObj ); p->nObjs[AIG_OBJ_PI]++; + if ( p->pManHaig && p->fCreatePios ) + { + p->pManHaig->nRegs++; + pObj->pHaig = Aig_ObjCreatePi( p->pManHaig ); +// printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id ); + } return pObj; } @@ -68,6 +74,11 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver ) Vec_PtrPush( p->vPos, pObj ); Aig_ObjConnect( p, pObj, pDriver, NULL ); p->nObjs[AIG_OBJ_PO]++; + if ( p->pManHaig && p->fCreatePios ) + { + pObj->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( pDriver ) ); +// printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id ); + } return pObj; } @@ -88,7 +99,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) Aig_Obj_t * pObj; assert( !Aig_IsComplement(pGhost) ); assert( Aig_ObjIsHash(pGhost) ); - assert( pGhost == &p->Ghost ); +// assert( pGhost == &p->Ghost ); // get memory for the new object pObj = Aig_ManFetchMemory( p ); pObj->Type = pGhost->Type; @@ -97,6 +108,14 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) // update node counters of the manager p->nObjs[Aig_ObjType(pObj)]++; assert( pObj->pData == NULL ); + if ( p->pManHaig ) + { + pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 ); + pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 ); + pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost ); + assert( !Aig_IsComplement(pObj->pHaig) ); +// printf( "Creating HAIG node %d equivalent to node %d.\n", pObj->pHaig->Id, pObj->Id ); + } return pObj; } @@ -137,7 +156,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj pObj->Level = Aig_ObjLevelNew( pObj ); pObj->fPhase = Aig_ObjPhaseReal(pFan0) & Aig_ObjPhaseReal(pFan1); // add the node to the structural hash table - if ( Aig_ObjIsHash(pObj) ) + if ( p->pTable && Aig_ObjIsHash(pObj) ) Aig_TableInsert( p, pObj ); // add the node to the dynamically updated topological order // if ( p->pOrderData && Aig_ObjIsNode(pObj) ) @@ -173,7 +192,7 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj ) Aig_ObjDeref(Aig_ObjFanin1(pObj)); } // remove the node from the structural hash table - if ( Aig_ObjIsHash(pObj) ) + if ( p->pTable && Aig_ObjIsHash(pObj) ) Aig_TableDelete( p, pObj ); // add the first fanin pObj->pFanin0 = NULL; @@ -271,6 +290,81 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew /**Function************************************************************* + Synopsis [Verbose printing of the AIG node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int fHaig = 0; + int fShowFanouts = 0; + Aig_Obj_t * pTemp; + assert( !Aig_IsComplement(pObj) ); + printf( "Node %4d : ", Aig_ObjId(pObj) ); + if ( Aig_ObjIsConst1(pObj) ) + printf( "constant 1" ); + else if ( Aig_ObjIsPi(pObj) ) + printf( "PI" ); + else if ( Aig_ObjIsPo(pObj) ) + printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); + else if ( Aig_ObjIsBuf(pObj) ) + printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); + else + printf( "AND( %4d%s, %4d%s )", + Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), + Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") ); + printf( " (refs = %3d)", Aig_ObjRefs(pObj) ); + if ( fShowFanouts && p->pFanData ) + { + Aig_Obj_t * pFanout; + int i, iFan; + printf( "\nFanouts:\n" ); + Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) + { + printf( " " ); + printf( "Node %4d : ", Aig_ObjId(pFanout) ); + if ( Aig_ObjIsPo(pFanout) ) + printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); + else if ( Aig_ObjIsBuf(pFanout) ) + printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); + else + printf( "AND( %4d%s, %4d%s )", + Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), + Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") ); + printf( "\n" ); + } + return; + } + if ( fHaig ) + { + if ( pObj->pHaig == NULL ) + printf( " HAIG node not given" ); + else + printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") ); + return; + } + // there are choices + if ( p->pEquivs && p->pEquivs[pObj->Id] ) + { + // print equivalence class + printf( " { %4d ", pObj->Id ); + for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] ) + printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " ); + printf( " }" ); + return; + } + // this is a secondary node + if ( p->pReprs && p->pReprs[pObj->Id] ) + printf( " class of %d", pObj->Id ); +} + +/**Function************************************************************* + Synopsis [Replaces node with a buffer fanin by a node without them.] Description [] @@ -280,7 +374,7 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew SeeAlso [] ***********************************************************************/ -void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel ) +void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fUpdateLevel ) { Aig_Obj_t * pFanReal0, * pFanReal1, * pResult; p->nBufFixes++; @@ -305,7 +399,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i else assert( 0 ); // replace the node with buffer by the node without buffer - Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel ); + Aig_ObjReplace( p, pObj, pResult, fUpdateLevel ); } /**Function************************************************************* @@ -319,7 +413,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i SeeAlso [] ***********************************************************************/ -int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel ) +int Aig_ManPropagateBuffers( Aig_Man_t * p, int fUpdateLevel ) { Aig_Obj_t * pObj; int nSteps; @@ -329,7 +423,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel ) // get the node with a buffer fanin for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) ); // replace this node by a node without buffer - Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel ); + Aig_NodeFixBufferFanins( p, pObj, fUpdateLevel ); // stop if a cycle occured if ( nSteps > 1000000 ) { @@ -354,15 +448,13 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel ) SeeAlso [] ***********************************************************************/ -void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ) +void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel ) { Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); - Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig; // the object to be replaced cannot be complemented assert( !Aig_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal -// assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) ); - assert( !Aig_ObjIsPo(pObjOld) ); + assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) ); // the object to be used cannot be a buffer or a PO assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) ); // the object cannot be the same @@ -375,14 +467,25 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in printf( "Aig_ObjReplace(): Internal error!\n" ); exit(1); } + // map the HAIG nodes + if ( p->pManHaig != NULL ) + { +// printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n", +// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL ); + assert( pObjNewR->pHaig != NULL ); +// assert( pObjNewR->pHaig->pHaig == NULL ); + assert( !Aig_IsComplement(pObjNewR->pHaig) ); + pObjNewR->pHaig->pHaig = pObjOld->pHaig; + } + else + pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig; // recursively delete the old node - but leave the object there pObjNewR->nRefs++; - if ( !Aig_ObjIsPi(pObjOld) ) - Aig_ObjDelete_rec( p, pObjOld, 0 ); + Aig_ObjDelete_rec( p, pObjOld, 0 ); pObjNewR->nRefs--; // if the new object is complemented or already used, create a buffer p->nObjs[pObjOld->Type]--; - if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Aig_ObjIsNode(pObjNew)) ) + if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || !Aig_ObjIsNode(pObjNew) ) { pObjOld->Type = AIG_OBJ_BUF; Aig_ObjConnect( p, pObjOld, pObjNew, NULL ); @@ -396,8 +499,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in pObjOld->Type = pObjNew->Type; Aig_ObjDisconnect( p, pObjNew ); Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 ); - // update the haig node - pObjOld->pHaig = pObjNew->pHaig; // delete the new object Aig_ObjDelete( p, pObjNew ); // update levels @@ -418,84 +519,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in { Vec_PtrPush( p->vBufs, pObjOld ); p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) ); - Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel ); + Aig_ManPropagateBuffers( p, fUpdateLevel ); } - pObjOld->pHaig = pHaig; -} - -/**Function************************************************************* - - Synopsis [Verbose printing of the AIG node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ) -{ - int fHaig = 0; - int fShowFanouts = 0; - Aig_Obj_t * pTemp; - assert( !Aig_IsComplement(pObj) ); - printf( "Node %4d : ", Aig_ObjId(pObj) ); - if ( Aig_ObjIsConst1(pObj) ) - printf( "constant 1" ); - else if ( Aig_ObjIsPi(pObj) ) - printf( "PI" ); - else if ( Aig_ObjIsPo(pObj) ) - printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); - else if ( Aig_ObjIsBuf(pObj) ) - printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); - else - printf( "AND( %4d%s, %4d%s )", - Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), - Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") ); - printf( " (refs = %3d)", Aig_ObjRefs(pObj) ); - if ( fShowFanouts && p->pFanData ) - { - Aig_Obj_t * pFanout; - int i, iFan; - printf( "\nFanouts:\n" ); - Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) - { - printf( " " ); - printf( "Node %4d : ", Aig_ObjId(pFanout) ); - if ( Aig_ObjIsPo(pFanout) ) - printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); - else if ( Aig_ObjIsBuf(pFanout) ) - printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") ); - else - printf( "AND( %4d%s, %4d%s )", - Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), - Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") ); - printf( "\n" ); - } - return; - } - if ( fHaig ) - { - if ( pObj->pHaig == NULL ) - printf( " HAIG node not given" ); - else - printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") ); - return; - } - // there are choices - if ( p->pEquivs && p->pEquivs[pObj->Id] ) - { - // print equivalence class - printf( " { %4d ", pObj->Id ); - for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] ) - printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " ); - printf( " }" ); - return; - } - // this is a secondary node - if ( p->pReprs && p->pReprs[pObj->Id] ) - printf( " class of %d", pObj->Id ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index cec92c11..392de03e 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1323,7 +1323,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon // create the equivalent nodes lists Aig_ManMarkValidChoices( pAig ); // reconstruct the network - pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry(vAigs,0) ); + pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) ); Aig_ManStop( pTemp ); // duplicate the timing manager pTemp = Vec_PtrEntry( vAigs, 0 ); @@ -1566,7 +1566,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) // create the equivalent nodes lists Aig_ManMarkValidChoices( pNew ); // reconstruct the network - pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) ); + pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) ); Aig_ManStop( pTemp ); // duplicate the timing manager pTemp = Vec_PtrEntry( vAigs, 0 ); diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index c2d08350..1474fcd5 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -103,7 +103,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) ); // check the resulting network if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDup(): The check has failed.\n" ); + printf( "Aig_ManRemap(): The check has failed.\n" ); return pNew; } @@ -598,7 +598,7 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int // store the original AIG assert( pAig->vFlopNums == NULL ); pAigInit = pAig; - pAig = Aig_ManDup( pAig ); + pAig = Aig_ManDupSimple( pAig ); // create storage for latch numbers pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs ); pAig->vFlopReprs = Vec_IntAlloc( 100 ); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index 9cfbf5f2..68efbba6 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -68,6 +68,7 @@ void Aig_TableResize( Aig_Man_t * p ) Aig_Obj_t * pEntry, * pNext; Aig_Obj_t ** pTableOld, ** ppPlace; int nTableSizeOld, Counter, i, clk; + assert( p->pTable != NULL ); clk = clock(); // save the old table pTableOld = p->pTable; @@ -115,7 +116,7 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ) assert( Aig_ObjIsNode(pGhost) ); assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) ); assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id ); - if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) ) + if ( p->pTable == NULL || !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) ) return NULL; for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext ) { diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 5556ac2e..3656aae3 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -333,7 +333,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) Synopsis [Derives a simple CNF for the AIG.] - Description [The last argument shows the number of last outputs + Description [The last argument lists the number of last outputs of the manager, which will not be converted into clauses. New variables will be introduced for these outputs.] diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 6dd308f9..49ca963b 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -353,7 +353,18 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * // make sure the balanced node is not assigned // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); assert( pObjOld->pData == NULL ); - Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; + if ( pNew->pManHaig != NULL ) + { + Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); +// printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n", +// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL ); + assert( pObjNewR->pHaig != NULL ); +// assert( pObjNewR->pHaig->pHaig == NULL ); + assert( !Aig_IsComplement(pObjNewR->pHaig) ); + pObjNewR->pHaig->pHaig = pObjOld->pHaig; + } + else + Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; return pObjOld->pData = pObjNew; } @@ -383,6 +394,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); + // pass the HAIG manager + if ( p->pManHaig != NULL ) + { + pNew->pManHaig = p->pManHaig; p->pManHaig = NULL; + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig); + } // map the PI nodes Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -401,6 +418,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) // copy the PI pObjNew = Aig_ObjCreatePi(pNew); pObj->pData = pObjNew; + pObjNew->pHaig = pObj->pHaig; // set the arrival time of the new PI arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) ); pObjNew->Level = (int)arrTime; @@ -411,10 +429,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); - Aig_ObjCreatePo( pNew, pObjNew ); // save arrival time of the output arrTime = (float)Aig_Regular(pObjNew)->Level; Tim_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime ); + // create PO + pObjNew = Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew->pHaig = pObj->pHaig; } else assert( 0 ); @@ -429,13 +449,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pObjNew = Aig_ObjCreatePi(pNew); pObjNew->Level = pObj->Level; pObj->pData = pObjNew; + pObjNew->pHaig = pObj->pHaig; } Aig_ManForEachPo( p, pObj, i ) { pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); - Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew = Aig_ObjCreatePo( pNew, pObjNew ); + pObjNew->pHaig = pObj->pHaig; } } Vec_VecFree( vStore ); diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index b13c7313..e82cce22 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -133,7 +133,7 @@ p->timeCuts += clock() - clk; // remove the old cuts Dar_ObjSetCuts( pObj, NULL ); // replace the node - Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); + Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel ); continue; } @@ -156,7 +156,7 @@ p->timeCuts += clock() - clk; pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase ); assert( (int)Aig_Regular(pObjNew)->Level <= Required ); // replace the node - Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); + Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel ); // compare the gains nNodeAfter = Aig_ManNodeNum( pAig ); assert( p->GainBest <= nNodeBefore - nNodeAfter ); diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index 09b9b3a4..d19d48e4 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -582,7 +582,7 @@ p->timeEval += clock() - clk; pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest ); assert( (int)Aig_Regular(pObjNew)->Level <= Required ); // replace the node - Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); + Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel ); // compare the gains nNodeAfter = Aig_ManNodeNum( pAig ); assert( p->GainBest <= nNodeBefore - nNodeAfter ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 3be0e3f6..df92792a 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -105,9 +105,9 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p // set the new node Fra_ObjSetFraig( pObj, iFrame, pObjNew2 ); // add the constraint - pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); - pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); - pMiter = Aig_Not( pMiter ); + pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew ); + pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) ); + assert( Aig_ObjPhaseReal(pMiter) == 1 ); Aig_ObjCreatePo( pManFraig, pMiter ); } diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index b8f93f57..ec6b7795 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -82,7 +82,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) float TimeLeft = 0.0; // try the miter before solving - pNew = Aig_ManDup( p ); + pNew = Aig_ManDupSimple( p ); RetValue = Fra_FraigMiterStatus( pNew ); if ( RetValue >= 0 ) goto finish; @@ -144,7 +144,7 @@ clk = clock(); PRT( "Time", clock() - clk ); } } - + // run latch correspondence clk = clock(); if ( pNew->nRegs ) @@ -165,22 +165,27 @@ clk = clock(); } } pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); + p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + Aig_ManStop( pTemp ); if ( pNew == NULL ) { + if ( p->pSeqModel ) + { + RetValue = 0; + printf( "Networks are NOT EQUIVALENT after simulation. " ); +PRT( "Time", clock() - clkTotal ); + if ( pParSec->fReportSolution && !pParSec->fRecursive ) + { + printf( "SOLUTION: FAIL " ); +PRT( "Time", clock() - clkTotal ); + } + return RetValue; + } pNew = pTemp; RetValue = -1; TimeOut = 1; goto finish; } - p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; - Aig_ManStop( pTemp ); - if ( pNew == NULL ) - { - RetValue = 0; - printf( "Networks are NOT EQUIVALENT after simulation. " ); -PRT( "Time", clock() - clkTotal ); - return RetValue; - } if ( pParSec->fVerbose ) { @@ -354,6 +359,11 @@ PRT( "Time", clock() - clk ); RetValue = 0; printf( "Networks are NOT EQUIVALENT after simulation. " ); PRT( "Time", clock() - clkTotal ); + if ( pParSec->fReportSolution && !pParSec->fRecursive ) + { + printf( "SOLUTION: FAIL " ); +PRT( "Time", clock() - clkTotal ); + } return RetValue; } Fra_SmlStop( pSml ); diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip Binary files differnew file mode 100644 index 00000000..0adf10df --- /dev/null +++ b/src/aig/fra/fraSec80516.zip diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index b14dd5bd..a8de5e37 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -994,7 +994,7 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) } return pCex; } - + /**Function************************************************************* Synopsis [Generates seq counter-example from the combinational one.] diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c index faae32d2..c6e80e75 100644 --- a/src/aig/ntl/ntlMap.c +++ b/src/aig/ntl/ntlMap.c @@ -129,7 +129,7 @@ void Ntl_ManSetIfParsDefault( If_Par_t * pPars ) pPars->nFlowIters = 1; pPars->nAreaIters = 2; pPars->DelayTarget = -1; - pPars->Epsilon = (float)0.001; + pPars->Epsilon = (float)0.005; pPars->fPreprocess = 1; pPars->fArea = 0; pPars->fFancy = 0; diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index 6c78ca87..f74f44f3 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -29,8 +29,6 @@ extern "C" { /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#pragma warning( disable : 4273 ) - #include "aig.h" #include "hop.h" #include "tim.h" @@ -119,6 +117,9 @@ struct Nwk_Obj_t_ //////////////////////////////////////////////////////////////////////// /// INLINED FUNCTIONS /// //////////////////////////////////////////////////////////////////////// + +//#pragma warning( disable : 4273 ) + #ifdef WIN32 #define DLLEXPORT __declspec(dllexport) #define DLLIMPORT __declspec(dllimport) diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index ea122bbf..50d6db49 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,5 +1,6 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigCone.c \ + src/aig/saig/saigHaig.c \ src/aig/saig/saigInter.c \ src/aig/saig/saigIoa.c \ src/aig/saig/saigPhase.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index c8efab40..8ec680b8 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -79,6 +79,8 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); +/*=== saigHaig.c ==========================================================*/ +extern void Saig_ManHaigRecord( Aig_Man_t * p ); /*=== saigIoa.c ==========================================================*/ extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 952094ce..2d5af2d3 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -145,11 +145,11 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax { pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); - if ( Counter >= nSizeMax ) - { - Aig_ManCleanup( pFrames ); - return pFrames; - } + } + if ( Counter >= nSizeMax ) + { + Aig_ManCleanup( pFrames ); + return pFrames; } if ( f == nFrames - 1 ) break; @@ -201,6 +201,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); PRT( "Time", clock() - clk ); + fflush( stdout ); } // rewrite the timeframes if ( fRewrite ) @@ -214,6 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); PRT( "Time", clock() - clk ); + fflush( stdout ); } } // create the SAT solver @@ -230,15 +232,20 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim { printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); PRT( "Time", clock() - clk ); + fflush( stdout ); } status = sat_solver_simplify(pSat); if ( status == 0 ) { if ( fVerbose ) + { printf( "The BMC problem is trivially UNSAT\n" ); + fflush( stdout ); + } } else { + int clkPart = clock(); Aig_ManForEachPo( pFrames, pObj, i ) { Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); @@ -247,12 +254,14 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); clk = clock(); status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( fVerbose ) + if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) { - printf( "Solved output %2d of frame %3d. ", - i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + printf( "Solved %2d outputs of frame %3d. ", + Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); - PRT( "Time", clock() - clk ); + PRT( "Time", clock() - clkPart ); + clkPart = clock(); + fflush( stdout ); } if ( status == l_False ) { @@ -272,7 +281,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else { - *piFrame = i; + *piFrame = i / Saig_ManPoNum(pAig); RetValue = -1; break; } diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c new file mode 100644 index 00000000..64f4e943 --- /dev/null +++ b/src/aig/saig/saigHaig.c @@ -0,0 +1,472 @@ +/**CFile**************************************************************** + + FileName [saigHaig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Experiments with history AIG recording.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "satSolver.h" +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; + // skip nodes without representative + pObjRepr = pObj->pHaig; + if ( pObjRepr == NULL ) + return; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = pObj->pData; + // get the new node of the representative + pObjReprNew = pObjRepr->pData; + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + // these are different nodes - perform speculative reduction + pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node + pObj->pData = pObjNew2; + // add the constraint + pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew ); + pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) ); + assert( Aig_ObjPhaseReal(pMiter) == 1 ); + Aig_ObjCreatePo( pFrames, pMiter ); +} + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f, nAssumptions = 0; + assert( nFrames == 1 || nFrames == 2 ); + assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 ); + // start AIG manager for timeframes + pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames ); + pFrames->pName = Aig_UtilStrsav( pHaig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec ); + // map the constant node + Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pHaig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add timeframes + Aig_ManSetPioNumbers( pHaig ); + for ( f = 0; f < nFrames; f++ ) + { + Aig_ManForEachObj( pHaig, pObj, i ) + { + if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) ) + continue; + if ( Saig_ObjIsPi(pHaig, pObj) ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + continue; + } + if ( Saig_ObjIsLo(pHaig, pObj) ) + { + Aig_ManHaigSpeculate( pFrames, pObj ); + continue; + } + if ( Aig_ObjIsNode(pObj) ) + { + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_ManHaigSpeculate( pFrames, pObj ); + continue; + } + assert( 0 ); + } + if ( f == nFrames - 2 ) + nAssumptions = Aig_ManPoNum(pFrames); + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pHaig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pHaig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions; + Aig_ManSetRegNum( pFrames, 0 ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) +{ + int nBTLimit = 0; + Aig_Man_t * pFrames; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + int i, Lit, RetValue, Counter; + int clk = clock(); + + // create time frames with speculative reduction and convert them into CNF +clk = clock(); + pFrames = Aig_ManHaigFrames( pHaig, nFrames ); +Aig_ManShow( pFrames, 0, NULL ); + + printf( "AIG: " ); + Aig_ManPrintStats( pAig ); + printf( "HAIG: " ); + Aig_ManPrintStats( pHaig ); + printf( "Frames: " ); + Aig_ManPrintStats( pFrames ); + printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n", + Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts ); + pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts ); +PRT( "Preparation", clock() - clk ); + +// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); +//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); + Saig_ManDumpBlif( pHaig, "haig_temp.blif" ); + Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" ); + // create the SAT solver to be used for this problem + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); + return -1; + } + + // solve each output +clk = clock(); + if ( pFrames->nAsserts == 0 ) + { + RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + printf( "SAT solver is wrong\n" ); + } + else + { + Counter = 0; + Aig_ManForEachPo( pFrames, pObj, i ) + { + if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts ) + continue; + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); + RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + } +PRT( "Solving ", clock() - clk ); + if ( Counter ) + printf( "Verification failed for %d classes.\n", Counter ); + else + printf( "Verification is successful.\n" ); + } + + // clean up + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) +{ + int nBTLimit = 0; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj, * pRepr; + int i, RetValue, Counter, Lits[2]; + int nClasses = 0; + int clk = clock(); + + assert( nFrames == 1 || nFrames == 2 ); + +clk = clock(); + pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) ); + // create the SAT solver to be used for this problem + pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 ); + if ( pSat == NULL ) + { + printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" ); + return -1; + } + + if ( nFrames == 2 ) + { + // add clauses for the first frame + Aig_ManForEachObj( pHaig, pObj, i ) + { + pRepr = pObj->pHaig; + if ( pRepr == NULL ) + continue; + if ( pRepr->fPhase ^ pObj->fPhase ) + { + Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return 0; + } + Lits[0]++; + Lits[1]++; + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return 0; + } + } + else + { + Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return 0; + } + Lits[0]++; + Lits[1]--; + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + { + sat_solver_delete( pSat ); + return 0; + } + } + } + + // add clauses for the next timeframe + { + int nLitsAll = 2 * pCnf->nVars; + int * pLits = pCnf->pClauses[0]; + for ( i = 0; i < pCnf->nLiterals; i++ ) + pLits[i] += nLitsAll; + } + } +PRT( "Preparation", clock() - clk ); + + + // check in the second timeframe +clk = clock(); + Counter = 0; + nClasses = 0; + Aig_ManForEachObj( pHaig, pObj, i ) + { + pRepr = pObj->pHaig; + if ( pRepr == NULL ) + continue; + nClasses++; + if ( pRepr->fPhase ^ pObj->fPhase ) + { + Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 ); + + RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + + Lits[0]++; + Lits[1]++; + + RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + } + else + { + Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 ); + + RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + + Lits[0]++; + Lits[1]--; + + RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_False ) + Counter++; + } + } +PRT( "Solving ", clock() - clk ); + if ( Counter ) + printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses ); + else + printf( "Verification is successful for all %d classes.\n", nClasses ); + + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManHaigRecord( Aig_Man_t * p ) +{ + extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ); + int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 ); + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Aig_Man_t * pNew, * pTemp; + Aig_Obj_t * pObj; + int i; + Dar_ManDefaultRwrParams( pParsRwr ); + // duplicate this manager + pNew = Aig_ManDupSimple( p ); + + // create its history AIG + pNew->pManHaig = Aig_ManDupSimple( pNew ); + Aig_ManForEachObj( pNew, pObj, i ) + pObj->pHaig = pObj->pData; + // remove structural hashing table + Aig_TableClear( pNew->pManHaig ); + + // perform retiming + if ( fUseRetiming ) + { +/* + // perform balancing + pNew = Dar_ManBalance( pTemp = pNew, 0 ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); + + // perform rewriting + Dar_ManRewrite( pNew, pParsRwr ); + pNew = Aig_ManDupDfs( pTemp = pNew ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); +*/ + // perform retiming + Saig_ManRetimeSteps( pNew, 1000, 1 ); + pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); + + // perform balancing + pNew = Dar_ManBalance( pTemp = pNew, 0 ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); + + // perform rewriting + Dar_ManRewrite( pNew, pParsRwr ); + pNew = Aig_ManDupDfs( pTemp = pNew ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); + } + else + { + // perform balancing + pNew = Dar_ManBalance( pTemp = pNew, 0 ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); +/* + // perform rewriting + Dar_ManRewrite( pNew, pParsRwr ); + pNew = Aig_ManDupDfs( pTemp = pNew ); + assert( pNew->pManHaig != NULL ); + assert( pTemp->pManHaig == NULL ); + Aig_ManStop( pTemp ); +*/ + } + + // use the haig for verification + Aig_ManAntiCleanup( pNew->pManHaig ); + Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs ); +//Aig_ManShow( pNew->pManHaig, 0, NULL ); + + printf( "AIG: " ); + Aig_ManPrintStats( pNew ); + printf( "HAIG: " ); + Aig_ManPrintStats( pNew->pManHaig ); + + if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) ) + printf( "Constructing SAT solver has failed.\n" ); + + // cleanup + Aig_ManStop( pNew->pManHaig ); + pNew->pManHaig = NULL; + Aig_ManStop( pNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index f19a27b6..323a230f 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -885,7 +885,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose ); Saig_TsiStop( pTsi ); if ( pNew == NULL ) - pNew = Aig_ManDup( p ); + pNew = Aig_ManDupSimple( p ); return pNew; } diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index 3935db6c..0ad6c314 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -622,7 +622,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl Vec_Ptr_t * vCut; Aig_Man_t * pNew, * pTemp, * pCopy; int i, fChanges; - pNew = Aig_ManDup( p ); + pNew = Aig_ManDupSimple( p ); // perform several iterations of forward retiming fChanges = 0; if ( !fBackwardOnly ) @@ -672,7 +672,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl { if ( Saig_ManRegNum(pNew) == 0 ) break; - pCopy = Aig_ManDup( pNew ); + pCopy = Aig_ManDupSimple( pNew ); pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose ); Aig_ManStop( pCopy ); if ( pTemp == NULL ) diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c index e7ec3c08..f7c27a93 100644 --- a/src/aig/saig/saigRetStep.c +++ b/src/aig/saig/saigRetStep.c @@ -44,6 +44,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj ) Aig_Obj_t * pFanin0, * pFanin1; Aig_Obj_t * pInput0, * pInput1; Aig_Obj_t * pObjNew, * pObjLi, * pObjLo; + int fCompl; assert( Saig_ManRegNum(p) > 0 ); assert( Aig_ObjIsNode(pObj) ); @@ -68,22 +69,26 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj ) pInput1 = Aig_ObjChild0( pInput1 ); pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) ); pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) ); + // get the condition when the register should be complemetned + fCompl = Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj); // create new node pObjNew = Aig_And( p, pInput0, pInput1 ); // create new register input - pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) ); + pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) ); pObjLi->PioNum = Aig_ManPoNum(p) - 1; - assert( pObjLi->fPhase == 0 ); // create new register output pObjLo = Aig_ObjCreatePi( p ); pObjLo->PioNum = Aig_ManPiNum(p) - 1; p->nRegs++; +//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", +// pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl ); + // return register output - return Aig_NotCond( pObjLo, pObjNew->fPhase ); + return Aig_NotCond( pObjLo, fCompl ); } /**Function************************************************************* @@ -163,6 +168,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ) int RetValue, s, i; Aig_ManSetPioNumbers( p ); Aig_ManFanoutStart( p ); + p->fCreatePios = 1; if ( fForward ) { for ( s = 0; s < nSteps; s++ ) @@ -172,7 +178,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ) pObjNew = Saig_ManRetimeNodeFwd( p, pObj ); if ( pObjNew == NULL ) continue; - Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); + Aig_ObjReplace( p, pObj, pObjNew, 0 ); break; } } @@ -186,13 +192,16 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ) pObjNew = Saig_ManRetimeNodeBwd( p, pObj ); if ( pObjNew == NULL ) continue; - Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); + Aig_ObjReplace( p, pObj, pObjNew, 0 ); break; } } } + p->fCreatePios = 0; + Aig_ManFanoutStop( p ); RetValue = Aig_ManCleanup( p ); assert( RetValue == 0 ); + Aig_ManSetRegNum( p, p->nRegs ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 0cafa314..8f0c7210 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -29,8 +29,6 @@ extern "C" { /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#pragma warning( disable : 4273 ) - #include <stdio.h> #include <stdlib.h> #include <string.h> @@ -226,6 +224,8 @@ struct Abc_Lib_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +//#pragma warning( disable : 4273 ) + #ifdef WIN32 #define DLLEXPORT __declspec(dllexport) #define DLLIMPORT __declspec(dllimport) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9b5ebddb..8d27c0d2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2762,19 +2762,36 @@ usage: int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtk, * pNtkRes; int c; + int fCleanupPis; + int fCleanupPos; + int fVerbose; + + extern Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fCleanupPis = 1; + fCleanupPos = 1; + fVerbose = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "iovh" ) ) != EOF ) { switch ( c ) { + case 'i': + fCleanupPis ^= 1; + break; + case 'o': + fCleanupPos ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -2789,16 +2806,35 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" ); + if ( !fCleanupPos && !fCleanupPos ) + { + printf( "Cleanup for PIs and POs is not enabled.\n" ); + pNtkRes = Abc_NtkDup( pNtk ); + } + else + pNtkRes = Abc_NtkDarCleanupAig( pNtk, fCleanupPis, fCleanupPos, fVerbose ); + } + else + { + Abc_NtkCleanup( pNtk, fVerbose ); + pNtkRes = Abc_NtkDup( pNtk ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Cleanup has failed.\n" ); return 1; } - // modify the current network - Abc_NtkCleanup( pNtk, 1 ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: cleanup [-h]\n" ); - fprintf( pErr, "\t removes dangling nodes\n" ); + fprintf( pErr, "usage: cleanup [-iovh]\n" ); + fprintf( pErr, "\t for logic networks, removes dangling combinatinal logic\n" ); + fprintf( pErr, "\t for AIGs, removes PIs w/o fanout and POs driven by const-0\n" ); + fprintf( pErr, "\t-i : toggles removing PIs without fanout [default = %s]\n", fCleanupPis? "yes": "no" ); + fprintf( pErr, "\t-o : toggles removing POs with const-0 drivers [default = %s]\n", fCleanupPos? "yes": "no" ); + fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -7469,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); // extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); -// extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); + extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern void Abc_NtkDarTestBlif( char * pFileName ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose ); @@ -7661,7 +7697,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ // Abc_NtkDarPartition( pNtk ); -Abc_NtkDarTest( pNtk ); +//Abc_NtkDarTest( pNtk ); + + +Abc_NtkDarHaigRecord( pNtk ); return 0; pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ca54e4e1..f369918e 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -94,16 +94,6 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ) pMan->fCatchExor = fExors; pMan->pName = Extra_UtilStrsav( pNtk->pName ); - // save the number of registers - if ( fRegisters ) - { - pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); -// pMan->vFlopNums = NULL; -// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk ); - if ( pNtk->vOnehots ) - pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots ); - } // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) @@ -134,6 +124,16 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ) if ( !fExors && nNodes ) printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes ); //Aig_ManDumpVerilog( pMan, "test.v" ); + // save the number of registers + if ( fRegisters ) + { + Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) ); + pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); +// pMan->vFlopNums = NULL; +// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk ); + if ( pNtk->vOnehots ) + pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots ); + } if ( !Aig_ManCheck( pMan ) ) { printf( "Abc_NtkToDar: AIG check has failed.\n" ); @@ -1220,8 +1220,6 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in return RetValue; } assert( pMan->nRegs > 0 ); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); // perform verification if ( fNewAlgo ) { @@ -1282,8 +1280,6 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra return -1; } assert( pMan->nRegs > 0 ); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); @@ -1593,9 +1589,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbo Vec_IntFree( pMan->vFlopNums ); pMan->vFlopNums = NULL; - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); - pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose ); Aig_ManStop( pTemp ); @@ -1630,9 +1623,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa Vec_IntFree( pMan->vFlopNums ); pMan->vFlopNums = NULL; - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); - pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose ); Aig_ManStop( pTemp ); @@ -1664,11 +1654,8 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ) Vec_IntFree( pMan->vFlopNums ); pMan->vFlopNums = NULL; - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); - Aig_ManPrintStats(pMan); - Saig_ManRetimeSteps( pMan, 1, 0 ); + Saig_ManRetimeSteps( pMan, 1000, 1 ); Aig_ManPrintStats(pMan); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); @@ -1689,18 +1676,16 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ) ***********************************************************************/ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ) { -/* Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; -// Aig_ManReduceLachesCount( pMan ); if ( pMan->vFlopNums ) Vec_IntFree( pMan->vFlopNums ); pMan->vFlopNums = NULL; - Aig_ManHaigRecord( pMan ); + + Saig_ManHaigRecord( pMan ); Aig_ManStop( pMan ); -*/ } /**Function************************************************************* @@ -2006,8 +1991,6 @@ void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk ) if ( pMan == NULL ) return; assert( Aig_ManRegNum(pMan) > 0 ); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); Saig_ManPrintCones( pMan ); Aig_ManStop( pMan ); } @@ -2063,10 +2046,7 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in Vec_Int_t * vInits; Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk, 0, 0 ); - pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return NULL; vInits = Abc_NtkGetLatchValues(pNtk); @@ -2097,10 +2077,7 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk, 0, 0 ); - pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return NULL; pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose ); @@ -2116,6 +2093,43 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI /**Function************************************************************* + Synopsis [Performs phase abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + if ( fCleanupPis ) + { + int Temp = Aig_ManPiCleanup( pMan ); + if ( fVerbose ) + printf( "Cleanup removed %d primary inputs without fanout.\n", Temp ); + } + if ( fCleanupPos ) + { + int Temp = Aig_ManPoCleanup( pMan ); + if ( fVerbose ) + printf( "Cleanup removed %d primary outputs driven by const-0.\n", Temp ); + } + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + Synopsis [Performs BDD-based reachability analysis.] Description [] @@ -2129,10 +2143,7 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio { extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); Aig_Man_t * pMan; - pMan = Abc_NtkToDar( pNtk, 0, 0 ); - pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); @@ -2156,9 +2167,6 @@ void Abc_NtkDarTest( Abc_Ntk_t * pNtk ) Aig_Man_t * pMan; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 1 ); - pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); - pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); if ( pMan == NULL ) return; diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c index a6ec6981..f74cbee8 100644 --- a/src/base/abci/abcRec.c +++ b/src/base/abci/abcRec.c @@ -523,6 +523,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk ) pPars->nFlowIters = 0; pPars->nAreaIters = 0; pPars->DelayTarget = -1; + pPars->Epsilon = (float)0.005; pPars->fPreprocess = 0; pPars->fArea = 1; pPars->fFancy = 0; diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 8e8e8719..f2861204 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -74,6 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF pPars->nFlowIters = nFlowIters; pPars->nAreaIters = nAreaIters; pPars->DelayTarget = -1; + pPars->Epsilon = (float)0.005; pPars->fPreprocess = 1; pPars->fArea = fArea; pPars->fFancy = 0; diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index 80080d50..4eb64aa2 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -53,6 +53,7 @@ void Lpk_IfManStart( Lpk_Man_t * p ) pPars->nFlowIters = 0; // 1 pPars->nAreaIters = 0; // 1 pPars->DelayTarget = -1; + pPars->Epsilon = (float)0.005; pPars->fPreprocess = 0; pPars->fArea = 1; pPars->fFancy = 0; |