From 28467823812f63a40f9a322b1fefc7decce4b766 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Aug 2007 08:01:00 -0700 Subject: Version abc70822 --- src/aig/aig/aig.h | 6 +- src/aig/aig/aigDfs.c | 48 +++++ src/aig/aig/aigRepr.c | 50 ++++- src/aig/aig/aigRet.c | 528 ++++++++++++++++++++++++++++++++++++++++++------ src/aig/aig/aigSeq.c | 219 -------------------- src/aig/aig/aigTsim.c | 436 +++++++++++++++++++++++++++++++++++++++ src/aig/aig/module.make | 1 + src/aig/fra/fra.h | 6 +- src/aig/fra/fraClass.c | 172 +++++++++++++++- src/aig/fra/fraCore.c | 104 +++++++--- src/aig/fra/fraImp.c | 16 +- src/aig/fra/fraInd.c | 55 ++--- src/aig/fra/fraMan.c | 1 + src/aig/fra/fraPart.c | 86 ++++++++ src/aig/fra/fraSec.c | 5 +- src/aig/fra/fraSim.c | 13 +- src/aig/ivy/ivyMan.c | 2 +- 17 files changed, 1380 insertions(+), 368 deletions(-) create mode 100644 src/aig/aig/aigTsim.c (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 953d98ac..1ee62ad6 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -359,6 +359,7 @@ extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ); extern int Aig_ManCountLevels( Aig_Man_t * p ); extern int Aig_DagSize( Aig_Obj_t * pObj ); +extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj ); extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars ); extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar ); @@ -434,10 +435,9 @@ extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); extern void Aig_ManCreateChoices( Aig_Man_t * p ); /*=== aigRet.c ========================================================*/ -extern Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ); +extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); -extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ); /*=== aigShow.c ========================================================*/ extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== aigTable.c ========================================================*/ @@ -458,6 +458,8 @@ extern void Aig_ManVerifyLevel( Aig_Man_t * p ); extern void Aig_ManVerifyReverseLevel( Aig_Man_t * p ); /*=== aigTruth.c ========================================================*/ extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore ); +/*=== aigTsim.c ========================================================*/ +extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ); /*=== aigUtil.c =========================================================*/ extern unsigned Aig_PrimeCudd( unsigned p ); extern void Aig_ManIncrementTravId( Aig_Man_t * p ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 5a18c4ac..86509322 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -378,6 +378,54 @@ int Aig_DagSize( Aig_Obj_t * pObj ) return Counter; } +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + (*pCounter)++; + return; + } + assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); + Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter ); + if ( Aig_ObjFanin1(pObj) ) + Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter ); +} + +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int Counter = 0; + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPo(pObj) ); + Aig_ManIncrementTravId( p ); + Aig_SupportSize_rec( p, pObj, &Counter ); + return Counter; +} + /**Function************************************************************* Synopsis [Transfers the AIG from one manager into another.] diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index a862bf97..3e588979 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -130,7 +130,7 @@ static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode ) assert( p->pReprs != NULL ); assert( !Aig_IsComplement(pNode) ); assert( pNode->Id < p->nReprsAlloc ); - assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id ); +// assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id ); return p->pReprs[pNode->Id]; } @@ -210,10 +210,36 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ) assert( pNew->pReprs != NULL ); // go through the nodes which have representatives Aig_ManForEachObj( p, pObj, k ) - if ( pRepr = Aig_ObjFindRepr(p, pObj) ) + if ( (pRepr = Aig_ObjFindRepr(p, pObj)) ) Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr; + if ( pObj->pData ) + return pObj->pData; + if ( (pRepr = Aig_ObjFindRepr(p, pObj)) ) + { + Aig_ManDupRepr_rec( pNew, p, pRepr ); + return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase ); + } + Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) ); + Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); +} + /**Function************************************************************* Synopsis [Duplicates AIG while substituting representatives.] @@ -227,27 +253,29 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ) ***********************************************************************/ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) { + int fOrdered = 1; Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pRepr; + Aig_Obj_t * pObj; int i; // start the HOP package pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); pNew->nRegs = p->nRegs; Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 ); // map the const and primary inputs + Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); // map the internal nodes -//printf( "\n" ); - Aig_ManForEachNode( p, pObj, i ) + if ( fOrdered ) { - pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); - if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class - { -//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id ); - Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); - } + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); + } + else + { + Aig_ManForEachPo( p, pObj, i ) + Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) ); } // transfer the POs Aig_ManForEachPo( p, pObj, i ) diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c index eacf756b..38fcc719 100644 --- a/src/aig/aig/aigRet.c +++ b/src/aig/aig/aigRet.c @@ -40,9 +40,11 @@ struct Rtm_Man_t_ Vec_Ptr_t * vPis; // PIs only Vec_Ptr_t * vPos; // POs only Aig_MmFlex_t * pMem; // the memory manager + // autonomous components after cutting off // storage for overflow latches - unsigned * pExtra; - unsigned * pExtraFree; + unsigned * pExtra; + int nExtraCur; + int nExtraAlloc; }; typedef struct Rtm_Edg_t_ Rtm_Edg_t; @@ -58,32 +60,59 @@ struct Rtm_Obj_t_ void * pCopy; // the copy of this object unsigned long Type : 3; // object type unsigned long fMark : 1; // multipurpose mark + unsigned long fAuto : 1; // this object belongs to an autonomous component unsigned long fCompl0 : 1; // complemented attribute of the first edge unsigned long fCompl1 : 1; // complemented attribute of the second edge unsigned long nFanins : 8; // the number of fanins - unsigned Num : 18; // the retiming number of this node + unsigned Num : 17; // the retiming number of this node int Id; // ID of this object int Temp; // temporary usage int nFanouts; // the number of fanouts void * pFanio[0]; // fanins and their edges (followed by fanouts and pointers to their edges) }; -static Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; } -static Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; } -static Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; } +static inline Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; } +static inline Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; } +static inline Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); } +static inline Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; } + +static inline Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; } +static inline Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; } +static inline Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB ) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; } + +static inline int Rtm_InitWordsNum( int nLats ) { return (nLats >> 4) + ((nLats & 15) > 0); } +static inline int Rtm_InitGetTwo( unsigned * p, int i ) { return (p[i>>4] >> ((i & 15)<<1)) & 3; } +static inline void Rtm_InitSetTwo( unsigned * p, int i, int val ) { p[i>>4] |= (val << ((i & 15)<<1)); } +static inline void Rtm_InitXorTwo( unsigned * p, int i, int val ) { p[i>>4] ^= (val << ((i & 15)<<1)); } + +static inline Rtm_Init_t Rtm_ObjGetFirst1( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; } +static inline Rtm_Init_t Rtm_ObjGetLast1( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; } +static inline Rtm_Init_t Rtm_ObjGetOne1( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (i << 1)) & 3; } +static inline Rtm_Init_t Rtm_ObjRemFirst1( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } +static inline Rtm_Init_t Rtm_ObjRemLast1( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; pEdge->LData ^= Val << ((pEdge->nLats-1)<<1); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } +static inline void Rtm_ObjAddFirst1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData = (pEdge->LData << 2) | Val; pEdge->nLats++; } +static inline void Rtm_ObjAddLast1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData |= Val << (pEdge->nLats<<1); pEdge->nLats++; } + +static inline Rtm_Init_t Rtm_ObjGetFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, 0 ); } +static inline Rtm_Init_t Rtm_ObjGetLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1 ); } +static inline Rtm_Init_t Rtm_ObjGetOne2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, i ); } +static Rtm_Init_t Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ); +static inline Rtm_Init_t Rtm_ObjRemLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Val = Rtm_ObjGetLast2( p, pEdge ); Rtm_InitXorTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1, Val ); pEdge->nLats--; return Val; } +static void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ); +static inline void Rtm_ObjAddLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { Rtm_InitSetTwo( p->pExtra + pEdge->LData, pEdge->nLats, Val ); pEdge->nLats++; } + +static void Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge ); +static void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge ); +static void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge ); + +static inline Rtm_Init_t Rtm_ObjGetFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return pEdge->nLats > 10? Rtm_ObjGetFirst2(p, pEdge) : Rtm_ObjGetFirst1(pEdge); } +static inline Rtm_Init_t Rtm_ObjGetLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return pEdge->nLats > 10? Rtm_ObjGetLast2(p, pEdge) : Rtm_ObjGetLast1(pEdge); } +static inline Rtm_Init_t Rtm_ObjGetOne( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i ) { return pEdge->nLats > 10? Rtm_ObjGetOne2(p, pEdge, i) : Rtm_ObjGetOne1(pEdge, i); } +static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemFirst2(p, pEdge) : Rtm_ObjRemFirst1(pEdge); if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; } +static Rtm_Init_t Rtm_ObjRemLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemLast2(p, pEdge) : Rtm_ObjRemLast1(pEdge); if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; } +static void Rtm_ObjAddFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddFirst2(p, pEdge, Val); else Rtm_ObjAddFirst1(pEdge, Val); } +static void Rtm_ObjAddLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddLast2(p, pEdge, Val); else Rtm_ObjAddLast1(pEdge, Val); } -static Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; } -static Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; } -static Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); } -static Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; } - -static Rtm_Init_t Rtm_ObjGetFirst( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; } -static Rtm_Init_t Rtm_ObjGetLast( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; } -static Rtm_Init_t Rtm_ObjGetOne( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (2 * i)) & 3; } -static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } -static Rtm_Init_t Rtm_ObjRemLast( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; pEdge->LData ^= Val << (2 *(pEdge->nLats-1)); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; } -static void Rtm_ObjAddFirst( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData = (pEdge->LData << 2) | Lat; pEdge->nLats++; } -static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData |= Lat << (2*pEdge->nLats); pEdge->nLats++; } // iterator over the primary inputs #define Rtm_ManForEachPi( p, pObj, i ) \ @@ -111,6 +140,149 @@ static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Transfers from big to small storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) +{ + assert( pEdge->nLats == 10 ); + pEdge->LData = p->pExtra[pEdge->LData]; +} + +/**Function************************************************************* + + Synopsis [Transfers from small to big storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) +{ + assert( pEdge->nLats == 10 ); + if ( p->nExtraCur + 1 > p->nExtraAlloc ) + { + int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 ); + p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew ); + p->nExtraAlloc = nExtraAllocNew; + } + p->pExtra[p->nExtraCur] = pEdge->LData; + pEdge->LData = p->nExtraCur++; +} + +/**Function************************************************************* + + Synopsis [Transfers to bigger storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) +{ + int nWords; + assert( (pEdge->nLats & 15) == 15 ); + nWords = (pEdge->nLats + 1) >> 4; + if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc ) + { + int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 ); + p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew ); + p->nExtraAlloc = nExtraAllocNew; + } + memcpy( p->pExtra + p->nExtraCur, p->pExtra + pEdge->LData, sizeof(unsigned) * nWords ); + p->pExtra[p->nExtraCur + nWords] = 0; + pEdge->LData = p->nExtraCur; + p->nExtraCur += nWords + 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rtm_Init_t Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) +{ + Rtm_Init_t Val = 0, Temp; + unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( pEdge->nLats-- ) - 1; + while ( pE >= pB ) + { + Temp = *pE & 3; + *pE = (*pE >> 2) | (Val << 30); + Val = Temp; + pE--; + } + assert( Val != 0 ); + return Val; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) +{ + unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( ++pEdge->nLats ); + Rtm_Init_t Temp; + assert( Val != 0 ); + while ( pB < pE ) + { + Temp = *pB >> 30; + *pB = (*pB << 2) | Val; + Val = Temp; + pB++; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_PrintEdge( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) +{ + unsigned LData = pEdge->LData; + printf( "%d : ", pEdge->nLats ); + if ( pEdge->nLats > 10 ) + Extra_PrintBinary( stdout, p->pExtra + pEdge->LData, 2*(pEdge->nLats+1) ); + else + Extra_PrintBinary( stdout, &LData, 2*(pEdge->nLats+1) ); + printf( "\n" ); +} + + /**Function************************************************************* Synopsis [Allocates the retiming manager.] @@ -153,6 +325,7 @@ void Rtm_ManFree( Rtm_Man_t * p ) Vec_PtrFree( p->vPis ); Vec_PtrFree( p->vPos ); Aig_MmFlexStop( p->pMem, 0 ); + FREE( p->pExtra ); free( p ); } @@ -171,10 +344,19 @@ int Rtm_ManLatchMax( Rtm_Man_t * p ) { Rtm_Obj_t * pObj; Rtm_Edg_t * pEdge; - int nLatchMax = 0, i, k; + int nLatchMax = 0, i, k;//, c, Val; Rtm_ManForEachObj( p, pObj, i ) Rtm_ObjForEachFaninEdge( pObj, pEdge, k ) + { +/* + for ( c = 0; c < (int)pEdge->nLats; c++ ) + { + Val = Rtm_ObjGetOne( p, pEdge, c ); + assert( Val == 1 || Val == 2 ); + } +*/ nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats ); + } return nLatchMax; } @@ -253,6 +435,27 @@ int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj ) return 1; } +/**Function************************************************************* + + Synopsis [Check the possibility of forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ObjCheckRetimeBwd( Rtm_Obj_t * pObj ) +{ + Rtm_Edg_t * pEdge; + int i; + Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) + if ( pEdge->nLats == 0 ) + return 0; + return 1; +} + /**Function************************************************************* Synopsis [Check the possibility of forward retiming.] @@ -273,6 +476,26 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj ) return Degree + 1; } +/**Function************************************************************* + + Synopsis [Check the possibility of forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj ) +{ + Rtm_Obj_t * pFanout; + int i, Degree = 0; + Rtm_ObjForEachFanout( pObj, pFanout, i ) + Degree = AIG_MAX( Degree, (int)pFanout->Num ); + return Degree + 1; +} + /**Function************************************************************* Synopsis [Performs forward retiming.] @@ -284,7 +507,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj ) +void Rtm_ObjRetimeFwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj ) { Rtm_Init_t ValTotal, ValCur; Rtm_Edg_t * pEdge; @@ -294,17 +517,143 @@ void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj ) ValTotal = RTM_VAL_ONE; Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) { - ValCur = Rtm_ObjRemFirst( pEdge ); + ValCur = Rtm_ObjRemFirst( pRtm, pEdge ); ValCur = Rtm_InitNotCond( ValCur, i? pObj->fCompl1 : pObj->fCompl0 ); ValTotal = Rtm_InitAnd( ValTotal, ValCur ); } // insert the result in the fanout values Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) + Rtm_ObjAddLast( pRtm, pEdge, ValTotal ); +} + +/**Function************************************************************* + + Synopsis [Performs forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjRetimeBwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj ) +{ + Rtm_Edg_t * pEdge; + int i; + assert( Rtm_ObjCheckRetimeBwd(pObj) ); + // extract values and compute the result + Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) + Rtm_ObjRemLast( pRtm, pEdge ); + // insert the result in the fanout values + Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) + Rtm_ObjAddFirst( pRtm, pEdge, RTM_VAL_VOID ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjMarkAutoFwd_rec( Rtm_Obj_t * pObj ) +{ + Rtm_Obj_t * pFanout; + int i; + if ( pObj->fAuto ) + return; + pObj->fAuto = 1; + Rtm_ObjForEachFanout( pObj, pFanout, i ) + Rtm_ObjMarkAutoFwd_rec( pFanout ); +} + +/**Function************************************************************* + + Synopsis [Marks the nodes unreachable from the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ManMarkAutoFwd( Rtm_Man_t * pRtm ) +{ + Rtm_Obj_t * pObjRtm; + int i, Counter = 0; + // mark nodes reachable from the PIs + pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 ); + Rtm_ObjMarkAutoFwd_rec( pObjRtm ); + Rtm_ManForEachPi( pRtm, pObjRtm, i ) + Rtm_ObjMarkAutoFwd_rec( pObjRtm ); + // count the number of autonomous nodes + Rtm_ManForEachObj( pRtm, pObjRtm, i ) { - if ( pEdge->nLats >= 10 ) - printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" ); - Rtm_ObjAddLast( pEdge, ValTotal ); + pObjRtm->fAuto = !pObjRtm->fAuto; + Counter += pObjRtm->fAuto; } + // mark the fanins of the autonomous nodes + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rtm_ObjMarkAutoBwd_rec( Rtm_Obj_t * pObj ) +{ + Rtm_Obj_t * pFanin; + int i; + if ( pObj->fAuto ) + return; + pObj->fAuto = 1; + Rtm_ObjForEachFanin( pObj, pFanin, i ) + Rtm_ObjMarkAutoBwd_rec( pFanin ); +} + +/**Function************************************************************* + + Synopsis [Marks the nodes unreachable from the POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rtm_ManMarkAutoBwd( Rtm_Man_t * pRtm ) +{ + Rtm_Obj_t * pObjRtm; + int i, Counter = 0; + // mark nodes reachable from the PIs + pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 ); + pObjRtm->fAuto = 1; + Rtm_ManForEachPi( pRtm, pObjRtm, i ) + pObjRtm->fAuto = 1; + Rtm_ManForEachPo( pRtm, pObjRtm, i ) + Rtm_ObjMarkAutoBwd_rec( pObjRtm ); + // count the number of autonomous nodes + Rtm_ManForEachObj( pRtm, pObjRtm, i ) + { + pObjRtm->fAuto = !pObjRtm->fAuto; + Counter += pObjRtm->fAuto; + } + // mark the fanins of the autonomous nodes + return Counter; } /**Function************************************************************* @@ -358,9 +707,6 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p ) Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); } - // set registers - Aig_ManForEachLoSeq( p, pObj, i ) - Rtm_ObjAddFirst( Rtm_ObjEdge(pObj->pData, 0), RTM_VAL_ZERO ); return pRtm; } @@ -375,7 +721,7 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches ) +Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Man_t * pRtm, Rtm_Obj_t * pObjRtm, int * pLatches ) { Rtm_Edg_t * pEdge; Aig_Obj_t * pRes, * pFanin; @@ -387,10 +733,10 @@ Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatc Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k ) { if ( pEdge->nLats == 0 ) - pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches ); + pFanin = Rtm_ManToAig_rec( pNew, pRtm, Rtm_ObjFanin(pObjRtm, k), pLatches ); else { - Val = Rtm_ObjGetFirst( pEdge ); + Val = Rtm_ObjGetFirst( pRtm, pEdge ); pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 ); pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE ); } @@ -438,7 +784,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm ) Aig_ObjCreatePi(pNew); // create internal nodes Rtm_ManForEachObj( pRtm, pObjRtm, i ) - Rtm_ManToAig_rec( pNew, pObjRtm, pLatches ); + Rtm_ManToAig_rec( pNew, pRtm, pObjRtm, pLatches ); // create POs Rtm_ManForEachPo( pRtm, pObjRtm, i ) Aig_ObjCreatePo( pNew, pObjRtm->pCopy ); @@ -451,7 +797,8 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm ) pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy; for ( m = 0; m < (int)pEdge->nLats; m++ ) { - Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m ); + Val = Rtm_ObjGetOne( pRtm, pEdge, pEdge->nLats - 1 - m ); + assert( Val == RTM_VAL_ZERO || Val == RTM_VAL_ONE || Val == RTM_VAL_VOID ); pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE ); Aig_ObjCreatePo( pNew, pObjNew ); pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m ); @@ -479,16 +826,33 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ) +Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ) { Vec_Ptr_t * vQueue; Aig_Man_t * pNew; Rtm_Man_t * pRtm; - Rtm_Obj_t * pObj, * pFanout; + Rtm_Obj_t * pObj, * pNext; Aig_Obj_t * pObjAig; - int i, k, Degree, DegreeMax = 0; + int i, k, nAutos, Degree, DegreeMax = 0; + int clk; + // create the retiming manager +clk = clock(); pRtm = Rtm_ManFromAig( p ); + // set registers + Aig_ManForEachLoSeq( p, pObjAig, i ) + Rtm_ObjAddFirst( pRtm, Rtm_ObjEdge(pObjAig->pData, 0), fForward? RTM_VAL_ZERO : RTM_VAL_VOID ); + // detect and mark the autonomous components + if ( fForward ) + nAutos = Rtm_ManMarkAutoFwd( pRtm ); + else + nAutos = Rtm_ManMarkAutoBwd( pRtm ); + if ( fVerbose ) + { + printf( "Detected %d autonomous objects. ", nAutos ); + PRT( "Time", clock() - clk ); + } + // set the current retiming number Rtm_ManForEachObj( pRtm, pObj, i ) { @@ -497,13 +861,30 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ) pObj->Num = 0; } +clk = clock(); // put the LOs on the queue vQueue = Vec_PtrAlloc( 1000 ); - Aig_ManForEachLoSeq( p, pObjAig, i ) + if ( fForward ) + { + Aig_ManForEachLoSeq( p, pObjAig, i ) + { + pObj = pObjAig->pData; + if ( pObj->fAuto ) + continue; + pObj->fMark = 1; + Vec_PtrPush( vQueue, pObj ); + } + } + else { - pObj = pObjAig->pData; - pObj->fMark = 1; - Vec_PtrPush( vQueue, pObj ); + Aig_ManForEachLiSeq( p, pObjAig, i ) + { + pObj = pObjAig->pData; + if ( pObj->fAuto ) + continue; + pObj->fMark = 1; + Vec_PtrPush( vQueue, pObj ); + } } // perform retiming DegreeMax = 0; @@ -511,36 +892,69 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose ) { pObj->fMark = 0; // retime the node - Rtm_ObjRetimeFwd( pObj ); - // check if its fanouts should be retimed - Rtm_ObjForEachFanout( pObj, pFanout, k ) + if ( fForward ) { - if ( pFanout->fMark ) // skip aleady scheduled - continue; - if ( pFanout->Type ) // skip POs - continue; - if ( !Rtm_ObjCheckRetimeFwd( pFanout ) ) // skip non-retimable - continue; - Degree = Rtm_ObjGetDegreeFwd( pFanout ); - DegreeMax = AIG_MAX( DegreeMax, Degree ); - if ( Degree > nStepsMax ) // skip nodes with high degree - continue; - pFanout->fMark = 1; - pFanout->Num = Degree; - Vec_PtrPush( vQueue, pFanout ); + Rtm_ObjRetimeFwd( pRtm, pObj ); + // check if its fanouts should be retimed + Rtm_ObjForEachFanout( pObj, pNext, k ) + { + if ( pNext->fMark ) // skip aleady scheduled + continue; + if ( pNext->Type ) // skip POs + continue; + if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable + continue; + Degree = Rtm_ObjGetDegreeFwd( pNext ); + DegreeMax = AIG_MAX( DegreeMax, Degree ); + if ( Degree > nStepsMax ) // skip nodes with high degree + continue; + pNext->fMark = 1; + pNext->Num = Degree; + Vec_PtrPush( vQueue, pNext ); + } + } + else + { + Rtm_ObjRetimeBwd( pRtm, pObj ); + // check if its fanouts should be retimed + Rtm_ObjForEachFanin( pObj, pNext, k ) + { + if ( pNext->fMark ) // skip aleady scheduled + continue; + if ( pNext->nFanins == 0 ) // skip PIs + continue; + if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable + continue; + Degree = Rtm_ObjGetDegreeBwd( pNext ); + DegreeMax = AIG_MAX( DegreeMax, Degree ); + if ( Degree > nStepsMax ) // skip nodes with high degree + continue; + pNext->fMark = 1; + pNext->Num = Degree; + Vec_PtrPush( vQueue, pNext ); + } } } if ( fVerbose ) - printf( "Performed %d fwd latch moves of max depth %d and max latch count %d.\n", - Vec_PtrSize(vQueue), DegreeMax, Rtm_ManLatchMax(pRtm) ); + { + printf( "Performed %d %s latch moves of max depth %d and max latch count %d.\n", + Vec_PtrSize(vQueue), fForward? "fwd":"bwd", DegreeMax, Rtm_ManLatchMax(pRtm) ); + printf( "Memory usage = %d. ", pRtm->nExtraCur ); + PRT( "Time", clock() - clk ); + } Vec_PtrFree( vQueue ); // get the new manager pNew = Rtm_ManToAig( pRtm ); Rtm_ManFree( pRtm ); // group the registers +clk = clock(); pNew = Aig_ManReduceLaches( pNew, fVerbose ); + if ( fVerbose ) + { + PRT( "Register sharing time", clock() - clk ); + } return pNew; } diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c index 5bd5aaa5..d296d339 100644 --- a/src/aig/aig/aigSeq.c +++ b/src/aig/aig/aigSeq.c @@ -24,70 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define AIG_XVS0 1 -#define AIG_XVS1 2 -#define AIG_XVSX 3 - -static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; } -static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; } -static inline int Aig_XsimInv( int Value ) -{ - if ( Value == AIG_XVS0 ) - return AIG_XVS1; - if ( Value == AIG_XVS1 ) - return AIG_XVS0; - assert( Value == AIG_XVSX ); - return AIG_XVSX; -} -static inline int Aig_XsimAnd( int Value0, int Value1 ) -{ - if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 ) - return AIG_XVS0; - if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX ) - return AIG_XVSX; - assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 ); - return AIG_XVS1; -} -static inline int Aig_XsimRand2() -{ - return (rand() & 1) ? AIG_XVS1 : AIG_XVS0; -} -static inline int Aig_XsimRand3() -{ - int RetValue; - do { - RetValue = rand() & 3; - } while ( RetValue == 0 ); - return RetValue; -} -static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj ) -{ - int RetValue; - RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj)); - return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue; -} -static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj ) -{ - int RetValue; - RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj)); - return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue; -} -static inline void Aig_XsimPrint( FILE * pFile, int Value ) -{ - if ( Value == AIG_XVS0 ) - { - fprintf( pFile, "0" ); - return; - } - if ( Value == AIG_XVS1 ) - { - fprintf( pFile, "1" ); - return; - } - assert( Value == AIG_XVSX ); - fprintf( pFile, "x" ); -} - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -559,161 +495,6 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ) -/**Function************************************************************* - - Synopsis [Cycles the circuit to create a new initial state.] - - Description [Simulates the circuit with random input for the given - number of timeframes to get a better initial state.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) -{ - int nRounds = 1000; // limit on the number of ternary simulation rounds - Vec_Ptr_t * vMap; - Vec_Ptr_t * vStates; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - unsigned * pState, * pPrev; - int i, k, f, fConstants, Value, nWords, nCounter; - // allocate storage for states - nWords = Aig_BitWordNum( 2*Aig_ManRegNum(p) ); - vStates = Vec_PtrAllocSimInfo( nRounds, nWords ); - // initialize the values - Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 ); - Aig_ManForEachPiSeq( p, pObj, i ) - Aig_ObjSetXsim( pObj, AIG_XVSX ); - Aig_ManForEachLoSeq( p, pObj, i ) - Aig_ObjSetXsim( pObj, AIG_XVS0 ); - // simulate for the given number of timeframes - for ( f = 0; f < nRounds; f++ ) - { - // collect this state - pState = Vec_PtrEntry( vStates, f ); - memset( pState, 0, sizeof(unsigned) * nWords ); - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - { - Value = Aig_ObjGetXsim(pObjLo); - if ( Value & 1 ) - Aig_InfoSetBit( pState, 2 * i ); - if ( Value & 2 ) - Aig_InfoSetBit( pState, 2 * i + 1 ); -// Aig_XsimPrint( stdout, Value ); - } -// printf( "\n" ); - // check if this state exists - for ( i = f - 1; i >= 0; i-- ) - { - pPrev = Vec_PtrEntry( vStates, i ); - if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) ) - break; - } - if ( i >= 0 ) - break; - // simulate internal nodes - Aig_ManForEachNode( p, pObj, i ) - Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) ); - // transfer the latch values - Aig_ManForEachLiSeq( p, pObj, i ) - Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) ); - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) ); - } - if ( f == nRounds ) - { - printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" ); - Vec_PtrFree( vStates ); - return NULL; - } - // OR all the states - pState = Vec_PtrEntry( vStates, 0 ); - for ( i = 1; i <= f; i++ ) - { - pPrev = Vec_PtrEntry( vStates, i ); - for ( k = 0; k < nWords; k++ ) - pState[k] |= pPrev[k]; - } - // check if there are constants - fConstants = 0; - if ( 2*Aig_ManRegNum(p) == 32*nWords ) - { - for ( i = 0; i < nWords; i++ ) - if ( pState[i] != ~0 ) - fConstants = 1; - } - else - { - for ( i = 0; i < nWords - 1; i++ ) - if ( pState[i] != ~0 ) - fConstants = 1; - if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) ) - fConstants = 1; - } - if ( fConstants == 0 ) - { - Vec_PtrFree( vStates ); - return NULL; - } - - // start mapping by adding the true PIs - vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPiSeq( p, pObj, i ) - Vec_PtrPush( vMap, pObj ); - // find constant registers - nCounter = 0; - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); - nCounter += (Value == 1 || Value == 2); - if ( Value == 1 ) - Vec_PtrPush( vMap, Aig_ManConst0(p) ); - else if ( Value == 2 ) - Vec_PtrPush( vMap, Aig_ManConst1(p) ); - else if ( Value == 3 ) - Vec_PtrPush( vMap, pObjLo ); - else - assert( 0 ); -// Aig_XsimPrint( stdout, Value ); - } -// printf( "\n" ); - Vec_PtrFree( vStates ); - if ( fVerbose ) - printf( "Detected %d constants after %d iterations.\n", nCounter, f ); - return vMap; -} - -/**Function************************************************************* - - Synopsis [Reduces the circuit using ternary simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ) -{ - Aig_Man_t * pTemp; - Vec_Ptr_t * vMap; - while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) ) - { - if ( fVerbose ) - printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); - p = Aig_ManRemap( pTemp = p, vMap ); - Aig_ManStop( pTemp ); - Vec_PtrFree( vMap ); - Aig_ManSeqCleanup( p ); - if ( fVerbose ) - printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); - } - return p; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c new file mode 100644 index 00000000..b8296cb2 --- /dev/null +++ b/src/aig/aig/aigTsim.c @@ -0,0 +1,436 @@ +/**CFile**************************************************************** + + FileName [aigTsim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Ternary simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigTsim.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define TSI_MAX_ROUNDS 10000 + +#define AIG_XVS0 1 +#define AIG_XVS1 2 +#define AIG_XVSX 3 + +static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; } +static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; } +static inline int Aig_XsimInv( int Value ) +{ + if ( Value == AIG_XVS0 ) + return AIG_XVS1; + if ( Value == AIG_XVS1 ) + return AIG_XVS0; + assert( Value == AIG_XVSX ); + return AIG_XVSX; +} +static inline int Aig_XsimAnd( int Value0, int Value1 ) +{ + if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 ) + return AIG_XVS0; + if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX ) + return AIG_XVSX; + assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 ); + return AIG_XVS1; +} +static inline int Aig_XsimRand2() +{ + return (rand() & 1) ? AIG_XVS1 : AIG_XVS0; +} +static inline int Aig_XsimRand3() +{ + int RetValue; + do { + RetValue = rand() & 3; + } while ( RetValue == 0 ); + return RetValue; +} +static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj)); + return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue; +} +static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj)); + return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue; +} +static inline void Aig_XsimPrint( FILE * pFile, int Value ) +{ + if ( Value == AIG_XVS0 ) + { + fprintf( pFile, "0" ); + return; + } + if ( Value == AIG_XVS1 ) + { + fprintf( pFile, "1" ); + return; + } + assert( Value == AIG_XVSX ); + fprintf( pFile, "x" ); +} + +// simulation manager +typedef struct Aig_Tsi_t_ Aig_Tsi_t; +struct Aig_Tsi_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + // ternary state representation + int nWords; // the number of words in the states + Vec_Ptr_t * vStates; // the collection of ternary states + Aig_MmFixed_t * pMem; // memory for ternary states + // hash table for terminary states + unsigned ** pBins; + int nBins; +}; + +static inline unsigned * Aig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); } +static inline void Aig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig ) +{ + Aig_Tsi_t * p; + p = (Aig_Tsi_t *)malloc( sizeof(Aig_Tsi_t) ); + memset( p, 0, sizeof(Aig_Tsi_t) ); + p->pAig = pAig; + p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) ); + p->vStates = Vec_PtrAlloc( 1000 ); + p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 ); + p->nBins = Aig_PrimeCudd(TSI_MAX_ROUNDS/2); + p->pBins = ALLOC( unsigned *, p->nBins ); + memset( p->pBins, 0, sizeof(unsigned *) * p->nBins ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TsiStop( Aig_Tsi_t * p ) +{ + Aig_MmFixedStop( p->pMem, 0 ); + Vec_PtrFree( p->vStates ); + free( p->pBins ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_TsiStateHash( unsigned * pState, int nWords, int nTableSize ) +{ + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned uHash; + int i; + uHash = 0; + for ( i = 0; i < nWords; i++ ) + uHash ^= pState[i] * s_FPrimes[i & 0x7F]; + return uHash % nTableSize; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_TsiStateLookup( Aig_Tsi_t * p, unsigned * pState, int nWords ) +{ + unsigned * pEntry; + int Hash; + Hash = Aig_TsiStateHash( pState, nWords, p->nBins ); + for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Aig_TsiNext(pEntry, nWords) ) + if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TsiStateInsert( Aig_Tsi_t * p, unsigned * pState, int nWords ) +{ + int Hash = Aig_TsiStateHash( pState, nWords, p->nBins ); + assert( !Aig_TsiStateLookup( p, pState, nWords ) ); + Aig_TsiSetNext( pState, nWords, p->pBins[Hash] ); + p->pBins[Hash] = pState; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Aig_TsiStateNew( Aig_Tsi_t * p ) +{ + unsigned * pState; + pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem ); + memset( pState, 0, sizeof(unsigned) * p->nWords ); + Vec_PtrPush( p->vStates, pState ); + return pState; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState ) +{ + int i, Value, nZeros = 0, nOnes = 0, nDcs = 0; + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + if ( Value == 1 ) + printf( "0" ), nZeros++; + else if ( Value == 2 ) + printf( "1" ), nOnes++; + else if ( Value == 3 ) + printf( "x" ), nDcs++; + else + assert( 0 ); + } + printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs ); +} + + +/**Function************************************************************* + + Synopsis [Cycles the circuit to create a new initial state.] + + Description [Simulates the circuit with random input for the given + number of timeframes to get a better initial state.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) +{ + Aig_Tsi_t * pTsi; + Vec_Ptr_t * vMap; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + unsigned * pState, * pPrev; + int i, k, f, fConstants, Value, nCounter; + // allocate the simulation manager + pTsi = Aig_TsiStart( p ); + // initialize the values + Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 ); + Aig_ManForEachPiSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, AIG_XVSX ); + Aig_ManForEachLoSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, AIG_XVS0 ); + // simulate for the given number of timeframes + for ( f = 0; f < TSI_MAX_ROUNDS; f++ ) + { + // collect this state + pState = Aig_TsiStateNew( pTsi ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + Value = Aig_ObjGetXsim(pObjLo); + if ( Value & 1 ) + Aig_InfoSetBit( pState, 2 * i ); + if ( Value & 2 ) + Aig_InfoSetBit( pState, 2 * i + 1 ); + } +// Aig_TsiStatePrint( pTsi, pState ); + // check if this state exists + if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) ) + break; + // insert this state + Aig_TsiStateInsert( pTsi, pState, pTsi->nWords ); + // simulate internal nodes + Aig_ManForEachNode( p, pObj, i ) + Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) ); + // transfer the latch values + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) ); + } + if ( f == TSI_MAX_ROUNDS ) + { + printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS ); + Aig_TsiStop( pTsi ); + return NULL; + } + // OR all the states + pState = Vec_PtrEntry( pTsi->vStates, 0 ); + Vec_PtrForEachEntry( pTsi->vStates, pPrev, i ) + { + for ( k = 0; k < pTsi->nWords; k++ ) + pState[k] |= pPrev[k]; + } + // check if there are constants + fConstants = 0; + if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords ) + { + for ( i = 0; i < pTsi->nWords; i++ ) + if ( pState[i] != ~0 ) + fConstants = 1; + } + else + { + for ( i = 0; i < pTsi->nWords - 1; i++ ) + if ( pState[i] != ~0 ) + fConstants = 1; + if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) ) + fConstants = 1; + } + if ( fConstants == 0 ) + { + Aig_TsiStop( pTsi ); + return NULL; + } + + // start mapping by adding the true PIs + vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Vec_PtrPush( vMap, pObj ); + // find constant registers + nCounter = 0; + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + nCounter += (Value == 1 || Value == 2); + if ( Value == 1 ) + Vec_PtrPush( vMap, Aig_ManConst0(p) ); + else if ( Value == 2 ) + Vec_PtrPush( vMap, Aig_ManConst1(p) ); + else if ( Value == 3 ) + Vec_PtrPush( vMap, pObjLo ); + else + assert( 0 ); +// Aig_XsimPrint( stdout, Value ); + } +// printf( "\n" ); + Aig_TsiStop( pTsi ); + if ( fVerbose ) + printf( "Detected %d constants after %d iterations of ternary simulation.\n", nCounter, f ); + return vMap; +} + +/**Function************************************************************* + + Synopsis [Reduces the circuit using ternary simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pTemp; + Vec_Ptr_t * vMap; + while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) ) + { + if ( fVerbose ) + printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + p = Aig_ManRemap( pTemp = p, vMap ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vMap ); + Aig_ManSeqCleanup( p ); + if ( fVerbose ) + printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + } + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index 93b25e4a..45ed62ee 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -13,5 +13,6 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigTable.c \ src/aig/aig/aigTiming.c \ src/aig/aig/aigTruth.c \ + src/aig/aig/aigTsim.c \ src/aig/aig/aigUtil.c \ src/aig/aig/aigWin.c \ No newline at end of file diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index c8617d84..217d1fba 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -73,6 +73,7 @@ struct Fra_Par_t_ int nBTLimitMiter; // conflict limit at an output int nFramesP; // the number of timeframes to in the prefix int nFramesK; // the number of timeframes to unroll + int nMaxImps; // the maximum number of implications to consider int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only int fUseImps; // use implications @@ -133,6 +134,7 @@ struct Fra_Man_t_ // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example + Vec_Int_t * vCex; // satisfiability solving sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used @@ -226,6 +228,8 @@ extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); extern void Fra_ClassesLatchCorr( Fra_Man_t * p ); extern void Fra_ClassesPostprocess( Fra_Cla_t * p ); +extern void Fra_ClassesSelectRepr( Fra_Cla_t * p ); +extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ); /*=== fraCnf.c ========================================================*/ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ @@ -240,7 +244,7 @@ extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ); extern void Fra_ImpCompactArray( Vec_Int_t * vImps ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index a9d727da..d6db125b 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) int i; Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->pAig->pReprs[i] != NULL ) + printf( "Classes are not cleared!\n" ); + assert( p->pAig->pReprs[i] == NULL ); + } + } if ( vFailed ) - Vec_PtrForEachEntry( vFailed, pObj, i ) - p->pAig->pReprs[pObj->Id] = NULL; + Vec_PtrForEachEntry( vFailed, pObj, i ) + p->pAig->pReprs[pObj->Id] = NULL; } /**Function************************************************************* @@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass ) assert( Fra_ClassObjRepr(pTemp) == pClass[0] ); printf( "{ " ); for ( i = 0; pTemp = pClass[i]; i++ ) - printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 ); + printf( "%d(%d) ", pTemp->Id, pTemp->Level ); printf( "}\n" ); } @@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) Aig_Obj_t * pObj; int i; - printf( "Const = %5d. Class = %5d. Lit = %5d.\n", + printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); + if ( p->vImps && Vec_IntSize(p->vImps) > 0 ) + printf( "Imp = %5d. ", Vec_IntSize(p->vImps) ); + printf( "\n" ); if ( fVeryVerbose ) { @@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; + // skip the node with more that the given number of levels +// if ( pObj->Level > 3 ) +// continue; } -//printf( "%3d : ", pObj->Id ); -//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); -//printf( "\n" ); // hash the node by its simulation info iEntry = p->pFuncNodeHash( pObj, nTableSize ); // check if the node belongs to the class of constant 1 @@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) vTemp = p->vClassesTemp; p->vClassesTemp = p->vClasses; p->vClasses = vTemp; - p->fRefinement = (nRefis > 0); return nRefis; } @@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) Vec_PtrShrink( p->vClasses1, k ); if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; - p->fRefinement = 1; /* printf( "Refined const-1 class: {" ); Vec_PtrForEachEntry( p->vClassNew, pObj, i ) @@ -675,6 +685,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) free( pWeights ); } +/**Function************************************************************* + + Synopsis [Postprocesses the classes by selecting representative lowest in top order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesSelectRepr( Fra_Cla_t * p ) +{ + Aig_Obj_t ** pClass, * pNodeMin; + int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur; + // reassign representatives in each class + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + // collect support sizes and find the min-support node + pNodeMin = NULL; + nSuppSizeMin = AIG_INFINITY; + for ( c = 0; pClass[c]; c++ ) + { + nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] ); +// nSuppSizeCur = 1; + if ( nSuppSizeMin > nSuppSizeCur || + (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) ) + { + nSuppSizeMin = nSuppSizeCur; + pNodeMin = pClass[c]; + cMinSupp = c; + } + } + // skip the case when the repr did not change + if ( cMinSupp == 0 ) + continue; + // make the new node the representative of the class + pClass[cMinSupp] = pClass[0]; + pClass[0] = pNodeMin; + // set the representative + for ( c = 0; pClass[c]; c++ ) + Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL ); + } +} + + + +static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return ppEquivs[pObj->Id]; } +static inline void Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; } + +static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)); } + +/**Function************************************************************* + + Synopsis [Add the node and its constraints to the new AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs ) +{ + Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2; + // skip nodes without representative + if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) + return; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Fra_ObjEqu( ppEquivs, pObj ); + // get the new node of the representative + pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr ); + // 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 +// Fra_ObjSetEqu( ppEquivs, pObj, 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 ); + Aig_ObjCreatePo( pManFraig, pMiter ); +} + /**Function************************************************************* Synopsis [Derives AIG for the partitioned problem.] @@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) ***********************************************************************/ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) { - + Aig_Man_t * pManFraig; + Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t ** pLatches, ** ppEquivs; + int i, k, f, nFramesAll = nFramesK + 1; + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( nFramesK > 0 ); + // start the fraig package + pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll ); + // allocate place for the node mapping + ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 ); + Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); + // create latches for the first frame + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // add timeframes + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); + for ( f = 0; f < nFramesAll; f++ ) + { + // create PIs for this frame + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) ); + Fra_ObjSetEqu( ppEquivs, pObj, pObjNew ); + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + } + if ( f == nFramesAll - 1 ) + break; + if ( f == nFramesAll - 2 ) + pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p->pAig, pObj, i ) + pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj ); + // insert them to the latch output values + k = 0; + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] ); + } + free( pLatches ); + free( ppEquivs ); + // mark the asserts + assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 ); +printf( "Assert miters = %6d. Output miters = %6d.\n", + pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts ); + // remove dangling nodes + Aig_ManCleanup( pManFraig ); + return pManFraig; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 3c76af03..9adbb7a9 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -24,6 +24,23 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/* + Speculating reduction in the sequential case leads to an interesting + situation when a counter-ex may not refine any classes. This happens + for non-constant equivalence classes. In such cases the representative + of the class (proved by simulation to be non-constant) may be reduced + to a constant during the speculative reduction. The fraig-representative + of this representative node is a constant node, even though this is a + non-constant class. Experiments have shown that this situation happens + very often at the beginning of the refinement iteration when there are + many spurious candidate equivalence classes (especially if heavy-duty + simulatation of BMC was node used at the beginning). As a result, the + SAT solver run may return a counter-ex that distinguishes the given + representative node from the constant-1 node but this counter-ex + does not distinguish the nodes in the non-costant class... This is why + there is no check of refinment after a counter-ex in the sequential case. +*/ + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -115,6 +132,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_ pNode->pData = p; } +/**Function************************************************************* + + Synopsis [Verifies the generated counter-ex.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) +{ + Aig_Obj_t * pObj, ** ppClass; + int i, c; + assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) ); + // make sure the input pattern is not used + Aig_ManForEachObj( p->pManAig, pObj, i ) + assert( !pObj->fMarkB ); + // simulate the cex through the AIG + Aig_ManConst1(p->pManAig)->fMarkB = 1; + Aig_ManForEachPi( p->pManAig, pObj, i ) + pObj->fMarkB = Vec_IntEntry(vCex, i); + Aig_ManForEachNode( p->pManAig, pObj, i ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( p->pManAig, pObj, i ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + // check if the classes hold + Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + { + if ( pObj->fPhase != pObj->fMarkB ) + printf( "The node %d is not constant under cex!\n", pObj->Id ); + } + Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + { + for ( c = 1; ppClass[c]; c++ ) + if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) ) + printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id ); +// for ( c = 0; ppClass[c]; c++ ) +// if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) ) +// printf( "A member of non-constant class has a constant repr!\n" ); + } + // clean the simulation pattern + Aig_ManForEachObj( p->pManAig, pObj, i ) + pObj->fMarkB = 0; +} + /**Function************************************************************* Synopsis [Performs fraiging for one node.] @@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); return; } -//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id ); // disprove the nodes + p->pCla->fRefinement = 1; // if we do not include the node into those disproved, we may end up // merging this node with another representative, for which proof has timed out if ( p->vTimeouts ) Vec_PtrPush( p->vTimeouts, pObj ); + // verify that the counter-example satisfies all the constraints +// if ( p->vCex ) +// Fra_FraigVerifyCounterEx( p, p->vCex ); // simulate the counter-example and return the Fraig node Fra_SmlResimulate( p ); -/* -printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id ); -Fra_ClassesPrint( p->pCla, 1 ); -printf( "%3d : ", 19 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", 27 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", 30 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "\n\n" ); -*/ - if ( Fra_ClassObjRepr(pObj) == pObjRepr ) - { -/* -//Fra_ClassesPrint( p->pCla, 1 ); -//printf( "\n\n" ); -printf( "%3d : ", pObj->Id ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", pObjRepr->Id ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -*/ - if ( Aig_ObjIsPi(pObj) ) - printf( "primary input\n" ); - else - printf( "NOT primary input\n" ); + if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr ) printf( "Fra_FraigNode(): Error in class refinement!\n" ); - } - assert( Fra_ClassObjRepr(pObj) != pObjRepr ); + assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr ); } /**Function************************************************************* diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index 25b34e03..8af11b78 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit ) +Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange ) { Vec_Int_t * vImpsNew; int * pCostCount, nImpCount, Imp, i, c; @@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, break; } free( pCostCount ); + if ( pCostRange ) + *pCostRange = c; return vImpsNew; } @@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in int * pImpCosts, * pNodesI, * pNodesK; int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; int CostMin = AIG_INFINITY, CostMax = 0; - int i, k, Imp, clk = clock(); + int i, k, Imp, CostRange, clk = clock(); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); @@ -350,9 +352,10 @@ finish: Fra_SmlStop( pSeq ); // select implications with the highest cost + CostRange = CostMin; if ( Vec_IntSize(vImps) > nImpUseLimit ) { - vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit ); + vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange ); Vec_IntFree( vTemp ); } @@ -365,8 +368,8 @@ finish: (int (*)(const void *, const void *)) Sml_CompareMaxId ); if ( p->pPars->fVerbose ) { -printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d - %d] ", - nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax ); +printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d < %d < %d] ", + nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax ); PRT( "Time", clock() - clk ); } return vImps; @@ -381,7 +384,7 @@ PRT( "Time", clock() - clk ); Synopsis [Add implication clauses to the SAT solver.] - Description [] + Description [Note that implications should be checked in the first frame!] SideEffects [] @@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ) { Vec_IntWriteEntry( vImps, i, 0 ); RetValue = 1; - p->pCla->fRefinement = 1; } } return RetValue; diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index d754f3ae..6d8305c0 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p ) pTemp = Aig_ManDup( p->pManFraig, 0 ); // pTemp = Dar_ManRwsat( pTemp, 1, 0 ); pTemp = Dar_ManRewriteDefault( pTemp ); - // printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); //Aig_ManDumpBlif( p->pManFraig, "1.blif" ); //Aig_ManDumpBlif( pTemp, "2.blif" ); - // Fra_FramesWriteCone( pTemp ); // Aig_ManStop( pTemp ); // transfer PI/register pointers @@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) { Aig_Man_t * pManFraig; - Aig_Obj_t * pObj, * pObjNew; - Aig_Obj_t ** pLatches; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; int i, k, f; assert( p->pManFraig == NULL ); assert( Aig_ManRegNum(p->pManAig) > 0 ); @@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); // add timeframes - pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) ); for ( f = 0; f < p->nFramesAll - 1; f++ ) { // set the constraints on the latch outputs @@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, f, pObjNew ); Fra_FramesConstrainNode( pManFraig, pObj, f ); } - // save the latch input values - k = 0; - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - pLatches[k++] = Fra_ObjChild0Fra(pObj,f); - assert( k == Aig_ManRegNum(p->pManAig) ); - // insert them to the latch output values - k = 0; - Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, f+1, pLatches[k++] ); - assert( k == Aig_ManRegNum(p->pManAig) ); + // transfer latch input to the latch outputs + Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k ) + Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) ); } - free( pLatches ); // mark the asserts pManFraig->nAsserts = Aig_ManPoNum(pManFraig); - // add the POs for the latch inputs - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) ); + // add the POs for the latch outputs of the last frame + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); // remove dangling nodes Aig_ManCleanup( pManFraig ); @@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, Fra_ParamsDefaultSeq( pPars ); pPars->nFramesP = nFramesP; pPars->nFramesK = nFramesK; + pPars->nMaxImps = nMaxImps; pPars->fVerbose = fVerbose; pPars->fRewrite = fRewrite; pPars->fLatchCorr = fLatchCorr; @@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, } else { + // bug: r iscas/blif/s5378.blif ; st; ssw -v // bug: r iscas/blif/s1238.blif ; st; ssw -v // refine the classes with more simulation rounds - p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 ); // 32, 2 ); +if ( fVerbose ) +printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 ); + p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 ); +if ( fVerbose ) +{ +PRT( "Time", clock() - clk ); +} Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); // Fra_ClassesPostprocess( p->pCla ); // allocate new simulation manager for simulating counter-examples @@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); } - // perform BMC - Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 ); + // perform BMC (for the min number of frames) + Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK ); //Fra_ClassesPrint( p->pCla, 1 ); +// p->vCex = Vec_IntAlloc( 1000 ); // select the most expressive implications if ( pPars->fUseImps ) - p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr ); + p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); p->nRegsBeg = Aig_ManRegNum(pManAig); + // dump AIG of the timeframes +// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK ); +// Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" ); +// Fra_ManPartitionTest2( pManAigNew ); +// Aig_ManStop( pManAigNew ); + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, // cleanup Fra_ManClean( p ); +// if ( nIter == 3 ) +// break; } +// Fra_ClassesPrint( p->pCla, 1 ); +// Fra_ClassesSelectRepr( p->pCla ); // move the classes into representatives and reduce AIG clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 2b8e0a68..0116bbc4 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p ) if ( p->pSat ) sat_solver_delete( p->pSat ); if ( p->pCla ) Fra_ClassesStop( p->pCla ); if ( p->pSml ) Fra_SmlStop( p->pSml ); + if ( p->vCex ) Vec_IntFree( p->vCex ); FREE( p->pMemFraig ); FREE( p->pMemFanins ); FREE( p->pMemSatNums ); diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c index d3fdbcfd..6e593694 100644 --- a/src/aig/fra/fraPart.c +++ b/src/aig/fra/fraPart.c @@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk ); +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ManPartitionTest2( Aig_Man_t * p ) +{ + Vec_Vec_t * vSupps, * vSuppsIn; + Vec_Int_t * vSup, * vSup2, * vSup3; + Aig_Obj_t * pObj; + int Entry, Entry2, Entry3, Counter; + int i, k, m, n, clk; + char * pSupp; + + // compute supports +clk = clock(); + vSupps = Aig_ManSupports( p ); +PRT( "Supports", clock() - clk ); + // remove last entry + Aig_ManForEachPo( p, pObj, i ) + { + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntPop( vSup ); + // remember support +// pObj->pNext = (Aig_Obj_t *)vSup; + } + + // create reverse supports +clk = clock(); + vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + if ( i == p->nAsserts ) + break; + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntForEachEntry( vSup, Entry, k ) + Vec_VecPush( vSuppsIn, Entry, (void *)i ); + } +PRT( "Inverse ", clock() - clk ); + + // create affective supports +clk = clock(); + pSupp = ALLOC( char, Aig_ManPiNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + if ( i % 50 != 0 ) + continue; + vSup = Vec_VecEntry( vSupps, i ); + memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) ); + // go through each input of this output + Vec_IntForEachEntry( vSup, Entry, k ) + { + pSupp[Entry] = 1; + vSup2 = Vec_VecEntry( vSuppsIn, Entry ); + // go though each assert of this input + Vec_IntForEachEntry( vSup2, Entry2, m ) + { + vSup3 = Vec_VecEntry( vSupps, Entry2 ); + // go through each input of this assert + Vec_IntForEachEntry( vSup3, Entry3, n ) + { + pSupp[Entry3] = 1; + } + } + } + // count the entries + Counter = 0; + for ( m = 0; m < Aig_ManPiNum(p); m++ ) + Counter += pSupp[m]; + printf( "%d(%d) ", Vec_IntSize(vSup), Counter ); + } + printf( "\n" ); +PRT( "Extension ", clock() - clk ); + + free( pSupp ); + Vec_VecFree( vSupps ); + Vec_VecFree( vSuppsIn ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 2a0d06b5..8b9258cb 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { Aig_Man_t * pNew; int nFrames, RetValue, nIter, clk, clkTotal = clock(); + int fLatchCorr = 0; if ( nFramesFix ) { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter ); } else { @@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose for ( nFrames = 1; ; nFrames++ ) { clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index b31fcb7f..3463ee0d 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -199,6 +199,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) Aig_ManForEachPi( p->pManFraig, pObj, i ) if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) Aig_InfoSetBit( p->pPatWords, i ); +/* + if ( p->vCex ) + { + Vec_IntClear( p->vCex ); + for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + } +*/ + /* printf( "Pattern: " ); Aig_ManForEachPi( p->pManFraig, pObj, i ) @@ -601,7 +612,7 @@ clk = clock(); if ( p->pCla->vImps ) nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); p->timeRef += clock() - clk; - if ( nChanges < 1 ) + if ( !p->pPars->nFramesK && nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); // assert( nChanges >= 1 ); //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c index 2d99c4f1..07faef85 100644 --- a/src/aig/ivy/ivyMan.c +++ b/src/aig/ivy/ivyMan.c @@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch ) int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) { Ivy_Obj_t * pNode; - int LimitFactor = 10; + int LimitFactor = 100; int NodeBeg = Ivy_ManNodeNum(p); int nSteps; for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) -- cgit v1.2.3