diff options
33 files changed, 2220 insertions, 560 deletions
@@ -2586,6 +2586,10 @@ SOURCE=.\src\aig\fra\fraInd.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraLcr.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraMan.c # End Source File # Begin Source File @@ -2794,6 +2798,10 @@ SOURCE=.\src\aig\aig\aigRet.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigScl.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigSeq.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 1ee62ad6..a6428e65 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -128,6 +128,8 @@ struct Aig_Man_t_ int fCatchExor; // enables EXOR nodes int fAddStrash; // performs additional strashing Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes + void (*pImpFunc) (void*, void*); // implication checking precedure + void * pImpData; // implication checking data // timing statistics int time1; int time2; @@ -298,6 +300,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) // iterator over the primary outputs #define Aig_ManForEachPo( p, pObj, i ) \ Vec_PtrForEachEntry( p->vPos, pObj, i ) +// iterator over the assertions +#define Aig_ManForEachAssert( p, pObj, i ) \ + Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts ) // iterator over all objects, including those currently not used #define Aig_ManForEachObj( p, pObj, i ) \ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else @@ -373,15 +378,12 @@ extern void Aig_ManFanoutStop( 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_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ); extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ); -extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ); 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_ManCountMergeRegs( Aig_Man_t * p ); -extern int Aig_ManSeqCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); -extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); /*=== aigMem.c ==========================================================*/ extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p ); @@ -436,6 +438,11 @@ 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_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ); +/*=== aigScl.c ==========================================================*/ +extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ); +extern int Aig_ManSeqCleanup( Aig_Man_t * p ); +extern int Aig_ManCountMergeRegs( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); /*=== aigShow.c ========================================================*/ diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 122daaa4..076cc420 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -172,54 +172,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) /**Function************************************************************* - Synopsis [Remaps the manager.] - - Description [Map in the array specifies for each CI nodes the node that - should be used after remapping.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjMapped; - int i; - // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); - pNew->nRegs = p->nRegs; - pNew->nAsserts = p->nAsserts; - // create the PIs - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); - // implement the mapping - Aig_ManForEachPi( p, pObj, i ) - { - pObjMapped = Vec_PtrEntry( vMap, i ); - pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); - } - // duplicate internal nodes - Aig_ManForEachObj( p, pObj, i ) - if ( Aig_ObjIsBuf(pObj) ) - pObj->pData = Aig_ObjChild0Copy(pObj); - else if ( Aig_ObjIsNode(pObj) ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // add the POs - Aig_ManForEachPo( p, pObj, i ) - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) ); - // check the resulting network - if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDup(): The check has failed.\n" ); - return pNew; -} - -/**Function************************************************************* - Synopsis [Extracts the miter composed of XOR of the two nodes.] Description [] @@ -306,110 +258,6 @@ void Aig_ManStop( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) -{ - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - return; - Aig_ObjSetTravIdCurrent(p, pObj); - // collect latch input corresponding to unmarked PI (latch output) - if ( Aig_ObjIsPi(pObj) ) - { - Vec_PtrPush( vNodes, pObj->pNext ); - return; - } - if ( Aig_ObjIsPo(pObj) ) - { - Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); - return; - } - assert( Aig_ObjIsNode(pObj) ); - Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); - Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes ); -} - -/**Function************************************************************* - - Synopsis [Returns the number of dangling nodes removed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManSeqCleanup( Aig_Man_t * p ) -{ - Vec_Ptr_t * vNodes, * vCis, * vCos; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, nTruePis, nTruePos; - assert( Aig_ManBufNum(p) == 0 ); - - // mark the PIs - Aig_ManIncrementTravId( p ); - Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); - Aig_ManForEachPiSeq( p, pObj, i ) - Aig_ObjSetTravIdCurrent( p, pObj ); - - // prepare to collect nodes reachable from POs - vNodes = Vec_PtrAlloc( 100 ); - Aig_ManForEachPoSeq( p, pObj, i ) - Vec_PtrPush( vNodes, pObj ); - - // remember latch inputs in latch outputs - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - pObjLo->pNext = pObjLi; - // mark the nodes reachable from these nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - Aig_ManSeqCleanup_rec( p, pObj, vNodes ); - assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) ); - // clean latch output pointers - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - pObjLo->pNext = NULL; - - // if some latches are removed, update PIs/POs - if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) ) - { - // collect new CIs/COs - vCis = Vec_PtrAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPi( p, pObj, i ) - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - Vec_PtrPush( vCis, pObj ); - vCos = Vec_PtrAlloc( Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - Vec_PtrPush( vCos, pObj ); - else - Aig_ObjDisconnect( p, pObj ); - // remember the number of true PIs/POs - nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); - nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); - // set the new number of registers - p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes); - // create new PIs/POs - assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs ); - assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs ); - Vec_PtrFree( p->vPis ); p->vPis = vCis; - Vec_PtrFree( p->vPos ); p->vPos = vCos; - p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); - p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); - } - Vec_PtrFree( vNodes ); - // remove dangling nodes - return Aig_ManCleanup( p ); -} - -/**Function************************************************************* - - Synopsis [Returns the number of dangling nodes removed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Aig_ManCleanup( Aig_Man_t * p ) { Vec_Ptr_t * vObjs; @@ -430,42 +278,6 @@ int Aig_ManCleanup( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Returns the number of dangling nodes removed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManCountMergeRegs( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj, * pFanin; - int i, Counter = 0, Const0 = 0, Const1 = 0; - Aig_ManIncrementTravId( p ); - Aig_ManForEachLiSeq( p, pObj, i ) - { - pFanin = Aig_ObjFanin0(pObj); - if ( Aig_ObjIsConst1(pFanin) ) - { - if ( Aig_ObjFaninC0(pObj) ) - Const0++; - else - Const1++; - } - if ( Aig_ObjIsTravIdCurrent(p, pFanin) ) - continue; - Aig_ObjSetTravIdCurrent(p, pFanin); - Counter++; - } - printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", - Aig_ManRegNum(p), Counter, Const0, Const1 ); - return 0; -} - -/**Function************************************************************* - Synopsis [Stops the AIG manager.] Description [] @@ -491,149 +303,6 @@ void Aig_ManPrintStats( Aig_Man_t * p ) printf( "\n" ); } -/**Function************************************************************* - - Synopsis [Checks how many latches can be reduced.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManReduceLachesCount( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj, * pFanin; - int i, Counter = 0; - assert( Aig_ManRegNum(p) > 0 ); - Aig_ManForEachObj( p, pObj, i ) - assert( !pObj->fMarkA && !pObj->fMarkB ); - Aig_ManForEachLiSeq( p, pObj, i ) - { - pFanin = Aig_ObjFanin0(pObj); - if ( Aig_ObjFaninC0(pObj) ) - { - if ( pFanin->fMarkB ) - Counter++; - else - pFanin->fMarkB = 1; - } - else - { - if ( pFanin->fMarkA ) - Counter++; - else - pFanin->fMarkA = 1; - } - } - Aig_ManForEachLiSeq( p, pObj, i ) - { - pFanin = Aig_ObjFanin0(pObj); - pFanin->fMarkA = pFanin->fMarkB = 0; - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [Reduces the latches.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p ) -{ - Vec_Ptr_t * vMap; - Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin; - int * pMapping, i; - // start mapping by adding the true PIs - vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPiSeq( p, pObj, i ) - Vec_PtrPush( vMap, pObj ); - // create mapping of fanin nodes into the corresponding latch outputs - pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) ); - Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - { - pFanin = Aig_ObjFanin0(pObjLi); - if ( Aig_ObjFaninC0(pObjLi) ) - { - if ( pFanin->fMarkB ) - { - Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) ); - } - else - { - pFanin->fMarkB = 1; - pMapping[2*pFanin->Id + 1] = i; - Vec_PtrPush( vMap, pObjLo ); - } - } - else - { - if ( pFanin->fMarkA ) - { - Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) ); - } - else - { - pFanin->fMarkA = 1; - pMapping[2*pFanin->Id] = i; - Vec_PtrPush( vMap, pObjLo ); - } - } - } - free( pMapping ); - Aig_ManForEachLiSeq( p, pObj, i ) - { - pFanin = Aig_ObjFanin0(pObj); - pFanin->fMarkA = pFanin->fMarkB = 0; - } - return vMap; -} - -/**Function************************************************************* - - Synopsis [Reduces the latches.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) -{ - Aig_Man_t * pTemp; - Vec_Ptr_t * vMap; - int nSaved, nCur; - for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur ) - { - if ( fVerbose ) - { - printf( "Saved = %5d. ", nCur ); - printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); - } - vMap = Aig_ManReduceLachesOnce( p ); - p = Aig_ManRemap( pTemp = p, vMap ); - Aig_ManStop( pTemp ); - Vec_PtrFree( vMap ); - Aig_ManSeqCleanup( p ); - if ( fVerbose ) - { - printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); - printf( "\n" ); - } - } - return p; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index f616bc25..d230f0d9 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -321,7 +321,7 @@ Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan ) } assert( 0 ); } -printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) ); +//printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) ); Part_ManStop( p ); // sort supports by size Vec_VecSort( vSupps, 1 ); diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 3e588979..cea3c438 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -253,7 +253,7 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb ***********************************************************************/ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) { - int fOrdered = 1; + int fOrdered = 0; Aig_Man_t * pNew; Aig_Obj_t * pObj; int i; diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c new file mode 100644 index 00000000..f8989446 --- /dev/null +++ b/src/aig/aig/aigScl.c @@ -0,0 +1,370 @@ +/**CFile**************************************************************** + + FileName [aigScl.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Sequential cleanup.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigScl.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Remaps the manager.] + + Description [Map in the array specifies for each CI nodes the node that + should be used after remapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjMapped; + int i; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // implement the mapping + Aig_ManForEachPi( p, pObj, i ) + { + pObjMapped = Vec_PtrEntry( vMap, i ); + pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); + } + // duplicate internal nodes + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add the POs + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDup(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + // collect latch input corresponding to unmarked PI (latch output) + if ( Aig_ObjIsPi(pObj) ) + { + Vec_PtrPush( vNodes, pObj->pNext ); + return; + } + if ( Aig_ObjIsPo(pObj) ) + { + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManSeqCleanup( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes, * vCis, * vCos; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, nTruePis, nTruePos; + assert( Aig_ManBufNum(p) == 0 ); + + // mark the PIs + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + + // prepare to collect nodes reachable from POs + vNodes = Vec_PtrAlloc( 100 ); + Aig_ManForEachPoSeq( p, pObj, i ) + Vec_PtrPush( vNodes, pObj ); + + // remember latch inputs in latch outputs + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + pObjLo->pNext = pObjLi; + // mark the nodes reachable from these nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + Aig_ManSeqCleanup_rec( p, pObj, vNodes ); + assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) ); + // clean latch output pointers + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + pObjLo->pNext = NULL; + + // if some latches are removed, update PIs/POs + if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) ) + { + // collect new CIs/COs + vCis = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + Vec_PtrPush( vCis, pObj ); + vCos = Vec_PtrAlloc( Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + Vec_PtrPush( vCos, pObj ); + else + Aig_ObjDisconnect( p, pObj ); + // remember the number of true PIs/POs + nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); + nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); + // set the new number of registers + p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes); + // create new PIs/POs + assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs ); + assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs ); + Vec_PtrFree( p->vPis ); p->vPis = vCis; + Vec_PtrFree( p->vPos ); p->vPos = vCos; + p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); + p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + } + Vec_PtrFree( vNodes ); + // remove dangling nodes + return Aig_ManCleanup( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCountMergeRegs( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0, Const0 = 0, Const1 = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsConst1(pFanin) ) + { + if ( Aig_ObjFaninC0(pObj) ) + Const0++; + else + Const1++; + } + if ( Aig_ObjIsTravIdCurrent(p, pFanin) ) + continue; + Aig_ObjSetTravIdCurrent(p, pFanin); + Counter++; + } + printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", + Aig_ManRegNum(p), Counter, Const0, Const1 ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Checks how many latches can be reduced.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManReduceLachesCount( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0, Diffs = 0; + assert( Aig_ManRegNum(p) > 0 ); + Aig_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjFaninC0(pObj) ) + { + if ( pFanin->fMarkB ) + Counter++; + else + pFanin->fMarkB = 1; + } + else + { + if ( pFanin->fMarkA ) + Counter++; + else + pFanin->fMarkA = 1; + } + } + // count fanins that have both attributes + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + Diffs += pFanin->fMarkA && pFanin->fMarkB; + pFanin->fMarkA = pFanin->fMarkB = 0; + } +// printf( "Diffs = %d.\n", Diffs ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Reduces the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p ) +{ + Vec_Ptr_t * vMap; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin; + int * pMapping, i; + // start mapping by adding the true PIs + vMap = Vec_PtrAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPiSeq( p, pObj, i ) + Vec_PtrPush( vMap, pObj ); + // create mapping of fanin nodes into the corresponding latch outputs + pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + pFanin = Aig_ObjFanin0(pObjLi); + if ( Aig_ObjFaninC0(pObjLi) ) + { + if ( pFanin->fMarkB ) + { + Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) ); + } + else + { + pFanin->fMarkB = 1; + pMapping[2*pFanin->Id + 1] = i; + Vec_PtrPush( vMap, pObjLo ); + } + } + else + { + if ( pFanin->fMarkA ) + { + Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) ); + } + else + { + pFanin->fMarkA = 1; + pMapping[2*pFanin->Id] = i; + Vec_PtrPush( vMap, pObjLo ); + } + } + } + free( pMapping ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + pFanin->fMarkA = pFanin->fMarkB = 0; + } + return vMap; +} + +/**Function************************************************************* + + Synopsis [Reduces the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pTemp; + Vec_Ptr_t * vMap; + int nSaved, nCur; + for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur ) + { + if ( fVerbose ) + { + printf( "Saved = %5d. ", nCur ); + printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + } + vMap = Aig_ManReduceLachesOnce( p ); + p = Aig_ManRemap( pTemp = p, vMap ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vMap ); + Aig_ManSeqCleanup( p ); + if ( fVerbose ) + { + printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); + printf( "\n" ); + } + } + return p; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c index b8296cb2..e5b96879 100644 --- a/src/aig/aig/aigTsim.c +++ b/src/aig/aig/aigTsim.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define TSI_MAX_ROUNDS 10000 +#define TSI_MAX_ROUNDS 1000 #define AIG_XVS0 1 #define AIG_XVS1 2 @@ -340,7 +340,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) } if ( f == TSI_MAX_ROUNDS ) { - printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS ); + printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS ); Aig_TsiStop( pTsi ); return NULL; } diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index cdf1fdf7..4d99e254 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -662,7 +662,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) { FILE * pFile; Vec_Ptr_t * vNodes; - Aig_Obj_t * pObj, * pConst1 = NULL; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL; int i, nDigits, Counter = 0; if ( Aig_ManPoNum(p) == 0 ) { @@ -687,14 +687,22 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) fprintf( pFile, ".model test\n" ); // write PIs fprintf( pFile, ".inputs" ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachPiSeq( p, pObj, i ) fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); fprintf( pFile, "\n" ); // write POs fprintf( pFile, ".outputs" ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachPoSeq( p, pObj, i ) fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); fprintf( pFile, "\n" ); + // write latches + if ( Aig_ManRegNum(p) ) + { + fprintf( pFile, "\n" ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData ); + fprintf( pFile, "\n" ); + } // write nodes Vec_PtrForEachEntry( vNodes, pObj, i ) { diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index 45ed62ee..d1b1cd3b 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -9,6 +9,8 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigOrder.c \ src/aig/aig/aigPart.c \ src/aig/aig/aigRepr.c \ + src/aig/aig/aigRet.c \ + src/aig/aig/aigScl.c \ src/aig/aig/aigSeq.c \ src/aig/aig/aigTable.c \ src/aig/aig/aigTiming.c \ diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 217d1fba..931e0930 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -77,6 +77,7 @@ struct Fra_Par_t_ int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only int fUseImps; // use implications + int fWriteImps; // record implications }; // FRAIG equivalence classes @@ -148,7 +149,6 @@ struct Fra_Man_t_ // statistics int nSimRounds; int nNodesMiter; - int nLitsZero; int nLitsBeg; int nLitsEnd; int nNodesBeg; @@ -202,6 +202,10 @@ static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pN static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } +static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; } +static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; } +static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -222,7 +226,7 @@ extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFai extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); -extern int Fra_ClassesRefine1( Fra_Cla_t * p ); +extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ); extern int Fra_ClassesCountLits( Fra_Cla_t * p ); extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); @@ -233,18 +237,24 @@ 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 ========================================================*/ -extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); -extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig ); extern int Fra_FraigMiterStatus( Aig_Man_t * p ); +extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); +extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); +extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ); /*=== fraImp.c ========================================================*/ extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ); extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos ); extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ); extern void Fra_ImpCompactArray( Vec_Int_t * vImps ); +extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ); +extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ); +extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ); /*=== fraInd.c ========================================================*/ -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 ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ); +/*=== fraLcr.c ========================================================*/ +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -259,7 +269,7 @@ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, A extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index 45c162af..648d08c4 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -31,6 +31,8 @@ struct Fra_Bmc_t_ int nPref; // the size of the prefix int nDepth; // the depth of the frames int nFramesAll; // the total number of timeframes + // implications to be filtered + Vec_Int_t * vImps; // AIG managers Aig_Man_t * pAig; // the original AIG manager Aig_Man_t * pAigFrames; // initialized timeframes @@ -67,7 +69,6 @@ static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { Fra_Man_t * p = pObj0->pData; -// Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig; Aig_Obj_t * pObjFrames0, * pObjFrames1; Aig_Obj_t * pObjFraig0, * pObjFraig1; int i; @@ -102,6 +103,69 @@ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ) return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) ); } +/**Function************************************************************* + + Synopsis [Refines implications using BMC.] + + Description [The input is the combinational FRAIG manager, + which is used to FRAIG the timeframes. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc ) +{ + Aig_Obj_t * pLeft, * pRight; + Aig_Obj_t * pLeftT, * pRightT; + Aig_Obj_t * pLeftF, * pRightF; + int i, f, Imp, Left, Right; + int fComplL, fComplR; + assert( p->nFramesAll == 1 ); + assert( p->pManAig == pBmc->pAigFrames ); + Vec_IntForEachEntry( pBmc->vImps, Imp, i ) + { + if ( Imp == 0 ) + continue; + Left = Fra_ImpLeft(Imp); + Right = Fra_ImpRight(Imp); + // get the corresponding nodes + pLeft = Aig_ManObj( pBmc->pAig, Left ); + pRight = Aig_ManObj( pBmc->pAig, Right ); + // iterate through the timeframes + for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ ) + { + // get timeframes nodes + pLeftT = Bmc_ObjFrames( pLeft, f ); + pRightT = Bmc_ObjFrames( pRight, f ); + // get the corresponding FRAIG nodes + pLeftF = Fra_ObjFraig( Aig_Regular(pLeftT), 0 ); + pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 ); + // get the complemented attributes + fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT); + fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT); + // check equality + if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) + { + if ( fComplL != fComplR ) + Vec_IntWriteEntry( pBmc->vImps, i, 0 ); + break; + } + // check the implication + // - if true, a clause is added + // - if false, a cex is simulated + // make sure the implication is refined + if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 ) + { + Vec_IntWriteEntry( pBmc->vImps, i, 0 ); + break; + } + } + } + Fra_ImpCompactArray( pBmc->vImps ); +} + /**Function************************************************************* @@ -125,8 +189,6 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth ) p->nFramesAll = nPref + nDepth; p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); -// p->pObjToFraig = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); -// memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); return p; } @@ -215,34 +277,6 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p ) /**Function************************************************************* - Synopsis [Constructs FRAIG manager for the initialized timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p ) -{ - Aig_Man_t * pFraig; - Fra_Par_t Pars, * pPars = &Pars; - Fra_ParamsDefault( pPars ); - pPars->nBTLimitNode = 100000; - pPars->fVerbose = 0; - pPars->fProve = 0; - pPars->fDoSparse = 1; - pPars->fSpeculate = 0; - pPars->fChoicing = 0; - pFraig = Fra_FraigPerform( p->pAigFrames, pPars ); - p->pObjToFraig = p->pAigFrames->pObjCopies; - p->pAigFrames->pObjCopies = NULL; - return pFraig; -} - -/**Function************************************************************* - Synopsis [Performs BMC for the given AIG.] Description [] @@ -255,12 +289,22 @@ Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p ) void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) { Aig_Obj_t * pObj; - int i, clk = clock(); + int i, nImpsOld, clk = clock(); assert( p->pBmc == NULL ); // derive and fraig the frames p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth ); p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc ); - p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc ); + // if implications are present, configure the AIG manager to check them + if ( p->pCla->vImps ) + { + p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications; + p->pBmc->pAigFrames->pImpData = p->pBmc; + p->pBmc->vImps = p->pCla->vImps; + nImpsOld = Vec_IntSize(p->pCla->vImps); + } + p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 ); + p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies; + p->pBmc->pAigFrames->pObjCopies = NULL; // annotate frames nodes with pointers to the manager Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i ) pObj->pData = p; @@ -271,19 +315,31 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) ); PRT( "Time", clock() - clk ); - printf( "Before BMC: " ); Fra_ClassesPrint( p->pCla, 0 ); + printf( "Before BMC: " ); +// Fra_ClassesPrint( p->pCla, 0 ); + printf( "Const = %5d. Class = %5d. Lit = %5d. ", + Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); + if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 ) + printf( "Imp = %5d. ", nImpsOld ); + printf( "\n" ); } // refine the classes p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst; p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual; Fra_ClassesRefine( p->pCla ); - Fra_ClassesRefine1( p->pCla ); + Fra_ClassesRefine1( p->pCla, 1, NULL ); p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst; p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual; // report the results if ( p->pPars->fVerbose ) { - printf( "After BMC: " ); Fra_ClassesPrint( p->pCla, 0 ); + printf( "After BMC: " ); +// Fra_ClassesPrint( p->pCla, 0 ); + printf( "Const = %5d. Class = %5d. Lit = %5d. ", + Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); + if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 ) + printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) ); + printf( "\n" ); } // free the BMC manager Fra_BmcStop( p->pBmc ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index d6db125b..3e3392c7 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -520,10 +520,10 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) SeeAlso [] ***********************************************************************/ -int Fra_ClassesRefine1( Fra_Cla_t * p ) +int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped ) { Aig_Obj_t * pObj, ** ppClass; - int i, k, nRefis; + int i, k, nRefis = 1; // check if there is anything to refine if ( Vec_PtrSize(p->vClasses1) == 0 ) return 0; @@ -565,7 +565,10 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) assert( ppClass[0] != NULL ); Vec_PtrPush( p->vClasses, ppClass ); // iteratively refine this class - nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses ); + if ( fRefineNewClass ) + nRefis += Fra_RefineClassLastIter( p, p->vClasses ); + else if ( pSkipped ) + (*pSkipped)++; return nRefis; } diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 9adbb7a9..94beb61a 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -246,7 +246,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPush( p->vTimeouts, pObj ); // verify that the counter-example satisfies all the constraints // if ( p->vCex ) -// Fra_FraigVerifyCounterEx( p, p->vCex ); +// Fra_FraigVerifyCounterEx( p, p->vCex ); // simulate the counter-example and return the Fraig node Fra_SmlResimulate( p ); if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr ) @@ -334,12 +334,15 @@ clk = clock(); if ( p->pPars->fChoicing ) Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); // collect initial states - p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); p->nRegsBeg = Aig_ManRegNum(pManAig); // perform fraig sweep Fra_FraigSweep( p ); + // call back the procedure to check implications + if ( pManAig->pImpFunc ) + pManAig->pImpFunc( p, pManAig->pImpData ); + // finalize the fraiged manager Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) { @@ -397,6 +400,32 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ) pPars->fChoicing = 1; return Fra_FraigPerform( pManAig, pPars ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ) +{ + Aig_Man_t * pFraig; + Fra_Par_t Pars, * pPars = &Pars; + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = nConfMax; + pPars->fVerbose = 0; + pPars->fProve = 0; + pPars->fDoSparse = 1; + pPars->fSpeculate = 0; + pPars->fChoicing = 0; + pFraig = Fra_FraigPerform( pManAig, pPars ); + return pFraig; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index 8af11b78..5e4b8c28 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -24,10 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Sml_ImpLeft( int Imp ) { return Imp & 0xFFFF; } -static inline int Sml_ImpRight( int Imp ) { return Imp >> 16; } -static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -43,19 +39,35 @@ static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) SeeAlso [] ***********************************************************************/ +static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node ) +{ + unsigned * pSim; + int k, Counter = 0; + pSim = Fra_ObjSim( p, Node ); + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes( pSim[k] ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in each siminfo of each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) { Aig_Obj_t * pObj; - unsigned * pSim; - int i, k, * pnBits; + int i, * pnBits; pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 ); memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) ); Aig_ManForEachObj( p->pAig, pObj, i ) - { - pSim = Fra_ObjSim( p, i ); - for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) - pnBits[i] += Aig_WordCountOnes( pSim[k] ); - } + pnBits[i] = Fra_SmlCountOnesOne( p, i ); return pnBits; } @@ -106,6 +118,27 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) /**Function************************************************************* + Synopsis [Counts the number of 1s in the reverse implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult ) +{ + unsigned * pSimL, * pSimR; + int k; + pSimL = Fra_ObjSim( p, Left ); + pSimR = Fra_ObjSim( p, Right ); + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + pResult[k] |= pSimL[k] & ~pSimR[k]; +} + +/**Function************************************************************* + Synopsis [Returns the array of nodes sorted by the number of 1s.] Description [] @@ -284,7 +317,6 @@ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 ) ***********************************************************************/ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ) { -// Aig_Obj_t * pObj; int nSimWords = 64; Fra_Sml_t * pSeq, * pComb; Vec_Int_t * vImps, * vTemp; @@ -293,21 +325,13 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; int CostMin = AIG_INFINITY, CostMax = 0; int i, k, Imp, CostRange, clk = clock(); + assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) ); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 ); // get the nodes sorted by the number of 1s vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr ); -/* -Aig_ManForEachObj( p->pManAig, pObj, i ) -{ - printf( "%6s", Aig_ObjIsPi(pObj)? "pi" : (Aig_ObjIsNode(pObj)? "node" : "other" ) ); - printf( "%d (%d) :\n", i, pObj->fPhase ); - Extra_PrintBinary( stdout, Fra_ObjSim( pComb, i ), 64 ); printf( "\n" ); - Extra_PrintBinary( stdout, Fra_ObjSim( pSeq, i ), 64 ); printf( "\n" ); -} -*/ // count the total number of implications for ( k = nSimWords * 32; k > 0; k-- ) for ( i = k - 1; i > 0; i-- ) @@ -335,10 +359,8 @@ Aig_ManForEachObj( p->pManAig, pObj, i ) nImpsComb++; continue; } -// printf( "d=%d c=%d ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) ); - nImpsCollected++; - Imp = Sml_ImpCreate( *pNodesI, *pNodesK ); + Imp = Fra_ImpCreate( *pNodesI, *pNodesK ); pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK); CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] ); CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] ); @@ -368,13 +390,16 @@ 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 < %d] ", - nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax ); +printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", + nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected ); +printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ", + CostMin, CostRange, CostMax ); PRT( "Time", clock() - clk ); } return vImps; } + // the following three procedures are called to // - add implications to the SAT solver // - check implications using the SAT solver @@ -401,8 +426,8 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ) Vec_IntForEachEntry( vImps, Imp, i ) { // get the corresponding nodes - pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) ); - pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) ); + pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); + pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); // check if all the nodes are present for ( f = 0; f < p->pPars->nFramesK; f++ ) { @@ -431,7 +456,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ) // get the complemented attributes fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF); fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF); - // get the constaint + // get the constraint // L => R L' v R (complement = L & R') pLits[0] = 2 * Left + !fComplL; pLits[1] = 2 * Right + fComplR; @@ -476,8 +501,8 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in { if ( Imp == 0 ) continue; - Left = Sml_ImpLeft(Imp); - Right = Sml_ImpRight(Imp); + Left = Fra_ImpLeft(Imp); + Right = Fra_ImpRight(Imp); Max = AIG_MAX( Left, Right ); assert( Max >= pNode->Id ); if ( Max > pNode->Id ) @@ -494,9 +519,6 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in // check equality if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) { -// assert( fComplL == fComplR ); -// if ( fComplL != fComplR ) -// printf( "Fra_ImpCheckForNode(): Unexpected situation!\n" ); if ( fComplL != fComplR ) Vec_IntWriteEntry( vImps, i, 0 ); continue; @@ -507,6 +529,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in // make sure the implication is refined if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 ) { + p->pCla->fRefinement = 1; Fra_SmlResimulate( p ); if ( Vec_IntEntry(vImps, i) != 0 ) printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" ); @@ -536,8 +559,8 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ) if ( Imp == 0 ) continue; // get the corresponding nodes - pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) ); - pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) ); + pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); + pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); // check if implication holds using this simulation info if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) ) { @@ -569,6 +592,113 @@ void Fra_ImpCompactArray( Vec_Int_t * vImps ) Vec_IntShrink( vImps, k ); } +/**Function************************************************************* + + Synopsis [Determines the ratio of the state space by computed implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ) +{ + int nSimWords = 64; + Fra_Sml_t * pComb; + unsigned * pResult; + double Ratio = 0.0; + int Left, Right, Imp, i; + if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) + return Ratio; + // simulate the AIG manager with combinational patterns + pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); + // go through the implications and collect where they do not hold + pResult = Fra_ObjSim( pComb, 0 ); + assert( pResult[0] == 0 ); + Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) + { + Left = Fra_ImpLeft(Imp); + Right = Fra_ImpRight(Imp); + Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult ); + } + // count the number of ones in this area + Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref)); + Fra_SmlStop( pComb ); + return Ratio; +} + +/**Function************************************************************* + + Synopsis [Returns the number of failed implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ) +{ + int nSimWords = 2000; + Fra_Sml_t * pSeq; + char * pfFails; + int Left, Right, Imp, i, Counter; + if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) + return 0; + // simulate the AIG manager with combinational patterns + pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 ); + // go through the implications and check how many of them do not hold + pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) ); + memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) ); + Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) + { + Left = Fra_ImpLeft(Imp); + Right = Fra_ImpRight(Imp); + pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right ); + } + // count how many has failed + Counter = 0; + for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ ) + Counter += pfFails[i]; + free( pfFails ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Record proven implications in the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) +{ + Aig_Obj_t * pLeft, * pRight, * pMiter; + int nPosOld, Imp, i; + if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) + return; + // go through the implication + nPosOld = Aig_ManPoNum(pNew); + Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) + { + pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); + pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); + // record the implication: L' + R + pMiter = Aig_Or( pNew, + Aig_NotCond(pLeft->pData, !pLeft->fPhase), + Aig_NotCond(pRight->pData, pRight->fPhase) ); + Aig_ObjCreatePo( pNew, pMiter ); + } + pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 6d8305c0..53dbdbb6 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -177,6 +177,61 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) /**Function************************************************************* + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) +{ + Aig_Obj_t * pObj, ** pLatches; + int i, k, f, nNodesOld; + // set copy pointer of each object to point to itself + Aig_ManForEachObj( p, pObj, i ) + pObj->pData = pObj; + // iterate and add objects + nNodesOld = Aig_ManObjIdMax(p); + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) ); + for ( f = 0; f < nFrames; f++ ) + { + // clean latch inputs and outputs + Aig_ManForEachLiSeq( p, pObj, i ) + pObj->pData = NULL; + Aig_ManForEachLoSeq( p, pObj, i ) + pObj->pData = NULL; + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p, pObj, i ) + { + if ( Aig_ObjFanin0(pObj)->pData ) + pLatches[k++] = Aig_ObjChild0Copy(pObj); + else + pLatches[k++] = NULL; + } + // insert them as the latch output values + k = 0; + Aig_ManForEachLoSeq( p, pObj, i ) + pObj->pData = pLatches[k++]; + // create the next time frame of nodes + Aig_ManForEachNode( p, pObj, i ) + { + if ( i > nNodesOld ) + break; + if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData ) + pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else + pObj->pData = NULL; + } + } + free( pLatches ); +} + +/**Function************************************************************* + Synopsis [Performs choicing of the AIG.] Description [] @@ -186,7 +241,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 nMaxImps, 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 fWriteImps, int fVerbose, int * pnIter ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -201,8 +256,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Aig_Man_t * pManAigNew; -// Vec_Int_t * vImps; + int nNodesBeg, nRegsBeg, Temp; int nIter, i, clk = clock(), clk2; + if ( Aig_ManNodeNum(pManAig) == 0 ) { if ( pnIter ) *pnIter = 0; @@ -212,6 +268,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, assert( Aig_ManRegNum(pManAig) > 0 ); assert( nFramesK > 0 ); //Aig_ManShow( pManAig, 0, NULL ); + + nNodesBeg = Aig_ManNodeNum(pManAig); + nRegsBeg = Aig_ManRegNum(pManAig); + + // enhance the AIG by adding timeframes +// Fra_FramesAddMore( pManAig, 3 ); // get parameters Fra_ParamsDefaultSeq( pPars ); @@ -222,6 +284,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, pPars->fRewrite = fRewrite; pPars->fLatchCorr = fLatchCorr; pPars->fUseImps = fUseImps; + pPars->fWriteImps = fWriteImps; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); @@ -255,19 +318,19 @@ PRT( "Time", clock() - clk ); p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); } - // 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, pPars->nMaxImps, pPars->fLatchCorr ); - - p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); + + // perform BMC (for the min number of frames) + Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement +//Fra_ClassesPrint( p->pCla, 1 ); +// if ( p->vCex == NULL ) +// p->vCex = Vec_IntAlloc( 1000 ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); - p->nNodesBeg = Aig_ManNodeNum(pManAig); - p->nRegsBeg = Aig_ManRegNum(pManAig); + p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig); + p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig); // dump AIG of the timeframes // pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK ); @@ -279,6 +342,8 @@ PRT( "Time", clock() - clk ); p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) { + int nLitsOld = Fra_ClassesCountLits(p->pCla); + int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes @@ -325,13 +390,13 @@ PRT( "Time", clock() - clk ); // report the intermediate results if ( fVerbose ) { - printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. %s = %6d. NR = %6d.\n", + printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ", nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), - Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, - p->pCla->vImps? "I" : "N", - p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig), - Aig_ManNodeNum(p->pManFraig) ); - } + Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); + if ( p->pCla->vImps ) + printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) ); + printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) ); + } // perform sweeping p->nSatCallsRecent = 0; @@ -341,18 +406,40 @@ PRT( "Time", clock() - clk ); assert( p->vTimeouts == NULL ); if ( p->vTimeouts ) printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); - // cleanup Fra_ManClean( p ); -// if ( nIter == 3 ) -// break; + // check if refinement has happened +// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla)); + if ( p->pCla->fRefinement && + nLitsOld == Fra_ClassesCountLits(p->pCla) && + nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) ) + { + printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" ); + break; + } } -// Fra_ClassesPrint( p->pCla, 1 ); -// Fra_ClassesSelectRepr( p->pCla ); + // check implications using simulation + if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) + { + int clk = clock(); + if ( Temp = Fra_ImpVerifyUsingSimulation( p ) ) + printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) ); + else + printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) ); + PRT( "Time", clock() - clk ); + } + + // move the classes into representatives and reduce AIG clk2 = clock(); +// Fra_ClassesPrint( p->pCla, 1 ); + Fra_ClassesSelectRepr( p->pCla ); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); pManAigNew = Aig_ManDupRepr( pManAig ); + // add implications to the manager + if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) + Fra_ImpRecordInManager( p, pManAigNew ); + // cleanup the new manager Aig_ManSeqCleanup( pManAigNew ); // Aig_ManCountMergeRegs( pManAigNew ); p->timeTrav += clock() - clk2; diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c new file mode 100644 index 00000000..c3b5504e --- /dev/null +++ b/src/aig/fra/fraLcr.c @@ -0,0 +1,644 @@ +/**CFile**************************************************************** + + FileName [fraLcorr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Latch correspondence computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Fra_Lcr_t_ Fra_Lcr_t; +struct Fra_Lcr_t_ +{ + // original AIG + Aig_Man_t * pAig; + // equivalence class representation + Fra_Cla_t * pCla; + // partitioning information + Vec_Ptr_t * vParts; // output partitions + int * pInToOutPart; // mapping of PI num into PO partition num + int * pInToOutNum; // mapping of PI num into the num of this PO in the partition + // AIGs for the partitions + Vec_Ptr_t * vFraigs; + // other variables + int fRefining; + // parameters + int nFramesP; + int fVerbose; + // statistics + int nIters; + int nLitsBeg; + int nLitsEnd; + int nNodesBeg; + int nNodesEnd; + int nRegsBeg; + int nRegsEnd; + // runtime + int timeSim; + int timePart; + int timeTrav; + int timeFraig; + int timeUpdate; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the retiming manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig ) +{ + Fra_Lcr_t * p; + p = ALLOC( Fra_Lcr_t, 1 ); + memset( p, 0, sizeof(Fra_Lcr_t) ); + p->pAig = pAig; + p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) ); + memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) ); + p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) ); + memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) ); + p->vFraigs = Vec_PtrAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prints stats for the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lcr_ManPrint( Fra_Lcr_t * p ) +{ + printf( "Iterations = %d. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", + p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); + PRT( "AIG simulation ", p->timeSim ); + PRT( "AIG partitioning", p->timePart ); + PRT( "AIG rebuiding ", p->timeTrav ); + PRT( "FRAIGing ", p->timeFraig ); + PRT( "AIG updating ", p->timeUpdate ); + PRT( "TOTAL RUNTIME ", p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Deallocates the retiming manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lcr_ManFree( Fra_Lcr_t * p ) +{ + Aig_Obj_t * pObj; + int i; + if ( p->fVerbose ) + Lcr_ManPrint( p ); + Aig_ManForEachPi( p->pAig, pObj, i ) + pObj->pNext = NULL; + Vec_PtrFree( p->vFraigs ); + if ( p->pCla ) Fra_ClassesStop( p->pCla ); + if ( p->vParts ) Vec_VecFree( (Vec_Vec_t *)p->vParts ); + free( p->pInToOutPart ); + free( p->pInToOutNum ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prepare the AIG for class computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig ) +{ + Fra_Man_t * p; + Aig_Obj_t * pObj; + int i; + p = ALLOC( Fra_Man_t, 1 ); + memset( p, 0, sizeof(Fra_Man_t) ); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = p; + return p; +} + +/**Function************************************************************* + + Synopsis [Prepare the AIG for class computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = p; +} + +/**Function************************************************************* + + Synopsis [Compares two nodes for equivalence after partitioned fraiging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + Fra_Man_t * pTemp = pObj0->pData; + Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc; + Aig_Man_t * pFraig; + Aig_Obj_t * pOut0, * pOut1; + int nPart0, nPart1; + assert( Aig_ObjIsPi(pObj0) ); + assert( Aig_ObjIsPi(pObj1) ); + // find the partition to which these nodes belong + nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext]; + nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext]; + // if this is the result of refinement of the class created const-1 nodes + // the nodes may end up in different partions - we assume them equivalent + if ( nPart0 != nPart1 ) + { + assert( 0 ); + return 1; + } + assert( nPart0 == nPart1 ); + pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 ); + // get the fraig outputs + pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] ); + pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] ); + return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1); +} + +/**Function************************************************************* + + Synopsis [Compares the node with a constant after partioned fraiging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_LcrNodeIsConst( Aig_Obj_t * pObj ) +{ + Fra_Man_t * pTemp = pObj->pData; + Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc; + Aig_Man_t * pFraig; + Aig_Obj_t * pOut; + int nPart; + assert( Aig_ObjIsPi(pObj) ); + // find the partition to which these nodes belong + nPart = pLcr->pInToOutPart[(int)pObj->pNext]; + pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart ); + // get the fraig outputs + pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] ); + return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig); +} + +/**Function************************************************************* + + Synopsis [Give the AIG and classes, reduces AIG for partitioning.] + + Description [Ignores registers that are not in the classes. + Places candidate equivalent classes of registers into single outputs + (for ease of partitioning). The resulting combinational AIG contains + outputs in the same order as equivalence classes of registers, + followed by constant-1 registers. Preserves the set of all inputs. + Complemented attributes of the outputs do not matter because we need + then only for collecting the structural info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter; + int i, c, Offset; + // remember the numbers of the inputs of the original AIG + Aig_ManForEachPi( pLcr->pAig, pObj, i ) + { + pObj->pData = pLcr; + pObj->pNext = (Aig_Obj_t *)i; + } + // compute the LO/LI offset + Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig); + // create the PIs + Aig_ManCleanData( pLcr->pAig ); + pNew = Aig_ManStartFrom( pLcr->pAig ); + // go over the equivalence classes + Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i ) + { + pMiter = Aig_ManConst0(pNew); + for ( c = 0; ppClass[c]; c++ ) + { + assert( Aig_ObjIsPi(ppClass[c]) ); + pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext ); + pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); + pMiter = Aig_Exor( pNew, pMiter, pObjNew ); + } + Aig_ObjCreatePo( pNew, pMiter ); + } + // go over the constant candidates + Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i ) + { + assert( Aig_ObjIsPi(pObj) ); + pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext ); + pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); + Aig_ObjCreatePo( pNew, pMiter ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Remaps partitions into the inputs of original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum ) +{ + Vec_Int_t * vOne, * vOneNew; + Aig_Obj_t ** ppClass, * pObjPi; + int Out, Offset, i, k, c; + // compute the LO/LI offset + Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig); + Vec_PtrForEachEntry( vParts, vOne, i ) + { + vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) ); + Vec_IntForEachEntry( vOne, Out, k ) + { + if ( Out < Vec_PtrSize(pCla->vClasses) ) + { + ppClass = Vec_PtrEntry( pCla->vClasses, Out ); + for ( c = 0; ppClass[c]; c++ ) + { + pInToOutPart[(int)ppClass[c]->pNext] = i; + pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew); + Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext ); + } + } + else + { + pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) ); + pInToOutPart[(int)pObjPi->pNext] = i; + pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew); + Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext ); + } + } + // replace the class + Vec_PtrWriteEntry( vParts, i, vOneNew ); + Vec_IntFree( vOne ); + } +} + +/**Function************************************************************* + + Synopsis [Creates AIG of one partition with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsPi(pObj) ) + { +// Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj); + Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id]; + if ( pRepr == NULL ) + pObj->pData = Aig_ObjCreatePi( pNew ); + else + { + pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr ); + pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase ); + } + return pObj->pData; + } + Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) ); + Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Creates AIG of one partition with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int Out, i; + // create new AIG for this partition + pNew = Aig_ManStartFrom( p->pAig ); + Aig_ManIncrementTravId( p->pAig ); + Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); + Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); + Vec_IntForEachEntry( vPart, Out, i ) + { + pObj = Aig_ManPo( p->pAig, Out ); + if ( pObj->fMarkA ) + { + pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ); + } + else + pObjNew = Aig_ManConst1( pNew ); + Aig_ObjCreatePo( pNew, pObjNew ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Marks the nodes belonging to the equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassNodesMark( Fra_Lcr_t * p ) +{ + Aig_Obj_t * pObj, ** ppClass; + int i, c, Offset; + // compute the LO/LI offset + Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); + // mark the nodes remaining in the classes + Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + { + pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext ); + pObj->fMarkA = 1; + } + Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + { + for ( c = 0; ppClass[c]; c++ ) + { + pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext ); + pObj->fMarkA = 1; + } + } +} + +/**Function************************************************************* + + Synopsis [Unmarks the nodes belonging to the equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) +{ + Aig_Obj_t * pObj, ** ppClass; + int i, c, Offset; + // compute the LO/LI offset + Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); + // mark the nodes remaining in the classes + Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + { + pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext ); + pObj->fMarkA = 0; + } + Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + { + for ( c = 0; ppClass[c]; c++ ) + { + pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext ); + pObj->fMarkA = 0; + } + } +} + +/**Function************************************************************* + + Synopsis [Performs choicing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter ) +{ + int nPartSize = 200; + int fReprSelect = 0; + + Fra_Lcr_t * p; + Fra_Man_t * pTemp; + Aig_Man_t * pAigPart, * pAigNew = NULL; + Vec_Int_t * vPart; + Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078); + int i, nIter, clk = clock(), clk2, clk3; + if ( Aig_ManNodeNum(pAig) == 0 ) + { + if ( pnIter ) *pnIter = 0; + return Aig_ManDup(pAig, 1); + } + assert( Aig_ManLatchNum(pAig) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + + // start the manager + p = Lcr_ManAlloc( pAig ); + p->nFramesP = nFramesP; + p->fVerbose = fVerbose; + + // simulate the AIG +clk2 = clock(); +if ( fVerbose ) +printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 ); + pTemp = Fra_LcrAigPrepare( p->pAig ); + pTemp->pBmc = (Fra_Bmc_t *)p; + pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 ); +if ( fVerbose ) +{ +PRT( "Time", clock() - clk2 ); +p->timeSim += clock() - clk2; +} + // get preliminary info about equivalence classes + pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig ); + Fra_ClassesPrepare( p->pCla, 1 ); + p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst; + p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual; + Fra_SmlStop( pTemp->pSml ); + + // partition the AIG for latch correspondence computation +clk2 = clock(); +if ( fVerbose ) +printf( "Partitioning AIG ... " ); + pAigPart = Fra_LcrDeriveAigForPartitioning( p ); + p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL ); + Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum ); + Aig_ManStop( pAigPart ); +if ( fVerbose ) +{ +PRT( "Time", clock() - clk2 ); +p->timePart += clock() - clk2; +} + + // get the initial stats + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nNodesBeg = Aig_ManNodeNum(p->pAig); + p->nRegsBeg = Aig_ManRegNum(p->pAig); + + // perforn interative reduction of the partitions + p->fRefining = 1; + for ( nIter = 0; p->fRefining; nIter++ ) + { + p->fRefining = 0; + clk3 = clock(); + // derive AIGs for each partition + Fra_ClassNodesMark( p ); + Vec_PtrClear( p->vFraigs ); + Vec_PtrForEachEntry( p->vParts, vPart, i ) + { +clk2 = clock(); + pAigPart = Fra_LcrCreatePart( p, vPart ); +p->timeTrav += clock() - clk2; +clk2 = clock(); + pAigNew = Fra_FraigEquivence( pAigPart, nConfMax ); +p->timeFraig += clock() - clk2; + Vec_PtrPush( p->vFraigs, pAigNew ); + Aig_ManStop( pAigPart ); + } + Fra_ClassNodesUnmark( p ); + // report the intermediate results + if ( fVerbose ) + { + printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ", + nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), + Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) ); + PRT( "T", clock() - clk3 ); + } + // refine the classes + Fra_LcrAigPrepareTwo( p->pAig, pTemp ); + if ( Fra_ClassesRefine( p->pCla ) ) + p->fRefining = 1; + if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) ) + p->fRefining = 1; + // clean the fraigs + Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) + Aig_ManStop( pAigPart ); + + // repartition if needed + if ( 1 ) + { +clk2 = clock(); + Vec_VecFree( (Vec_Vec_t *)p->vParts ); + pAigPart = Fra_LcrDeriveAigForPartitioning( p ); + p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL ); + Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum ); + Aig_ManStop( pAigPart ); +p->timePart += clock() - clk2; + } + } + free( pTemp ); + p->nIters = nIter; + + // move the classes into representatives and reduce AIG +clk2 = clock(); +// Fra_ClassesPrint( p->pCla, 1 ); + if ( fReprSelect ) + Fra_ClassesSelectRepr( p->pCla ); + Fra_ClassesCopyReprs( p->pCla, NULL ); + pAigNew = Aig_ManDupRepr( p->pAig ); + Aig_ManSeqCleanup( pAigNew ); +// Aig_ManCountMergeRegs( pAigNew ); +p->timeUpdate += clock() - clk2; +p->timeTotal = clock() - clk; + // get the final stats + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nNodesEnd = Aig_ManNodeNum(pAigNew); + p->nRegsEnd = Aig_ManRegNum(pAigNew); + Lcr_ManFree( p ); + if ( pnIter ) *pnIter = nIter; + return pAigNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 0116bbc4..97282e98 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -181,6 +181,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) assert( p->pManFraig == NULL ); // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 ); + pManFraig->nRegs = p->pManAig->nRegs; + pManFraig->nAsserts = p->pManAig->nAsserts; // set the pointers to the available fraig nodes Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) ); Aig_ManForEachPi( p->pManAig, pObj, i ) @@ -271,9 +273,9 @@ void Fra_ManPrint( Fra_Man_t * p ) { double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", - p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg ); - printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", - p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars ); + p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) ); + printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", + p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) ); printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 8b9258cb..88c552dc 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose ) { Aig_Man_t * pNew; int nFrames, RetValue, nIter, clk, clkTotal = clock(); @@ -48,7 +48,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); } else { @@ -56,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, fLatchCorr, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { @@ -89,6 +89,136 @@ PRT( "Time", clock() - clkTotal ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +{ + Aig_Man_t * pNew, * pTemp; + int nFrames, RetValue, nIter, clk, clkTotal = clock(); + int fLatchCorr = 0; + + pNew = Aig_ManDup( p, 1 ); + if ( fVerbose ) + { + printf( "Original miter: Latches = %5d. Nodes = %6d.\n", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); + } +//Aig_ManDumpBlif( pNew, "after.blif" ); + + // perform sequential cleanup +clk = clock(); + pNew = Aig_ManReduceLaches( pNew, 0 ); + pNew = Aig_ManConstReduce( pNew, 0 ); + if ( fVerbose ) + { + printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + + // perform forward retiming + if ( fRetimeFirst ) + { +clk = clock(); + pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + } + + // run latch correspondence +clk = clock(); + pNew = Aig_ManDup( pTemp = pNew, 1 ); + Aig_ManStop( pTemp ); + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ", + nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + + // perform fraiging +clk = clock(); + pNew = Fra_FraigEquivence( pTemp = pNew, 1000 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Fraiging: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + + // perform seq sweeping while increasing the number of frames + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue == -1 ) + for ( nFrames = 1; ; nFrames *= 2 ) + { +clk = clock(); + pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + Aig_ManStop( pTemp ); + RetValue = Fra_FraigMiterStatus( pNew ); + if ( fVerbose ) + { + printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", + nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + if ( RetValue != -1 ) + break; + // perform rewriting +clk = clock(); + pNew = Aig_ManDup( pTemp = pNew, 1 ); + Aig_ManStop( pTemp ); + pNew = Dar_ManRewriteDefault( pTemp = pNew ); + if ( fVerbose ) + { + printf( "Rewriting: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + // perform retiming +clk = clock(); + pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + Aig_ManStop( pTemp ); + pNew = Aig_ManDup( pTemp = pNew, 1 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + } + // get the miter status + RetValue = Fra_FraigMiterStatus( pNew ); + Aig_ManStop( pNew ); + + // report the miter + if ( RetValue == 1 ) + printf( "Networks are equivalent. " ); + else if ( RetValue == 0 ) + printf( "Networks are NOT EQUIVALENT. " ); + else + printf( "Networks are UNDECIDED. " ); +PRT( "Time", clock() - clkTotal ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 3463ee0d..0b93fb73 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -199,7 +199,7 @@ 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 ); @@ -208,7 +208,6 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) 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: " ); @@ -608,7 +607,7 @@ void Fra_SmlResimulate( Fra_Man_t * p ) return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); - nChanges += Fra_ClassesRefine1( p->pCla ); + nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); if ( p->pCla->vImps ) nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); p->timeRef += clock() - clk; @@ -652,7 +651,7 @@ printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); - nChanges += Fra_ClassesRefine1( p->pCla ); + nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); p->timeRef += clock() - clk; if ( fVerbose ) printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); @@ -663,7 +662,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); - nChanges += Fra_ClassesRefine1( p->pCla ); + nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); p->timeRef += clock() - clk; if ( fVerbose ) @@ -677,7 +676,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( return; clk = clock(); nChanges = Fra_ClassesRefine( p->pCla ); - nChanges += Fra_ClassesRefine1( p->pCla ); + nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); p->timeRef += clock() - clk; if ( fVerbose ) printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) ); @@ -704,7 +703,6 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) { Fra_Sml_t * p; - assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) ); p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame ); memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); p->pAig = pAig; diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index bd8a20be..e7264fdc 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -5,6 +5,7 @@ SRC += src/aig/fra/fraBmc.c \ src/aig/fra/fraCore.c \ src/aig/fra/fraImp.c \ src/aig/fra/fraInd.c \ + src/aig/fra/fraLcr.c \ src/aig/fra/fraMan.c \ src/aig/fra/fraSat.c \ src/aig/fra/fraSec.c \ diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index bda8781c..42820550 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -869,6 +869,7 @@ extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFree extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ); extern void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk ); +extern int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index bb1ae2ed..b4a97223 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -148,6 +148,33 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Reads the number of cubes of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, nCubes, nCubePairs = 0; + assert( Abc_NtkHasSop(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + assert( pNode->pData ); + nCubes = Abc_SopGetCubeNum( pNode->pData ); + nCubePairs += nCubes * (nCubes - 1) / 2; + } + return nCubePairs; +} + +/**Function************************************************************* + Synopsis [Reads the number of literals in the SOPs of the nodes.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 78519d40..3902830d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -123,6 +123,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -166,6 +167,7 @@ static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -326,12 +328,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); -// Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); -// Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 ); @@ -339,6 +340,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); @@ -2588,22 +2590,34 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) p = ALLOC( Fxu_Data_t, 1 ); memset( p, 0, sizeof(Fxu_Data_t) ); // set the defaults - p->nPairsMax = 30000; - p->nNodesExt = 10000; - p->fOnlyS = 0; - p->fOnlyD = 0; - p->fUse0 = 0; - p->fUseCompl = 1; - p->fVerbose = 0; + p->nSingleMax = 20000; + p->nPairsMax = 30000; + p->nNodesExt = 10000; + p->fOnlyS = 0; + p->fOnlyD = 0; + p->fUse0 = 0; + p->fUseCompl = 1; + p->fVerbose = 0; Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "SDNsdzcvh")) != EOF ) { switch (c) { - case 'L': + case 'S': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + p->nSingleMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( p->nSingleMax < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } p->nPairsMax = atoi(argv[globalUtilOptind]); @@ -2643,7 +2657,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) default: goto usage; } - } + } if ( pNtk == NULL ) { @@ -2673,10 +2687,11 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n"); + fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n"); fprintf( pErr, "\t performs unate fast extract on the current network\n"); + fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); + fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt ); - fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax ); fprintf( pErr, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" ); fprintf( pErr, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); fprintf( pErr, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); @@ -6175,7 +6190,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nLevels = 128; + nLevels = 1000; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) { @@ -6293,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 ); + pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -8674,7 +8689,7 @@ int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 1; + fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { @@ -10975,12 +10990,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFramesP; int nFramesK; int nMaxImps; - int fExdc; int fUseImps; int fRewrite; int fLatchCorr; + int fWriteImps; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10990,13 +11005,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) nFramesP = 0; nFramesK = 1; nMaxImps = 5000; - fExdc = 1; fUseImps = 0; fRewrite = 0; fLatchCorr = 0; + fWriteImps = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PFIirlevh" ) ) != EOF ) { switch ( c ) { @@ -11033,9 +11048,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nMaxImps <= 0 ) goto usage; break; - case 'e': - fExdc ^= 1; - break; case 'i': fUseImps ^= 1; break; @@ -11045,6 +11057,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': fLatchCorr ^= 1; break; + case 'e': + fWriteImps ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11069,12 +11084,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Sequential sweep works only for structurally hashed networks (run \"strash\").\n" ); - return 1; + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; } // get the new network - pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -11085,15 +11100,120 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" ); + fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps ); -// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); + fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int nFramesP; + int nConfMax; + int fVerbose; + extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFramesP = 0; + nConfMax = 10000; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF ) + { + switch ( c ) + { + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nFramesP = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFramesP < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfMax < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } + + // get the new network + pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Sequential sweeping has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" ); + fprintf( pErr, "\t computes latch correspondence using 1-step induction\n" ); + fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); + fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -11113,12 +11233,12 @@ usage: int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes, * pTemp; + Abc_Ntk_t * pNtk, * pNtkRes; int c; int fLatchSweep; int fAutoSweep; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11153,23 +11273,13 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - if ( !Abc_NtkIsLogic(pNtk) ) + if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Only works for logic networks.\n" ); + fprintf( pErr, "Only works for structrally hashed networks.\n" ); return 1; } // modify the current network - - // get the new network - pNtkRes = Abc_NtkDup( pNtk ); - Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose ); - if ( fLatchSweep ) - { - pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 ); - Abc_NtkDelete( pTemp ); - pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose ); - Abc_NtkDelete( pTemp ); - } + pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential cleanup has failed.\n" ); @@ -11180,14 +11290,14 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: scleanup [-lavh]\n" ); + fprintf( pErr, "usage: scleanup [-lvh]\n" ); fprintf( pErr, "\t performs sequential cleanup\n" ); fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); - fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); +// fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); fprintf( pErr, "\t (the latter may change sequential behaviour)\n" ); fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); - fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); +// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -11291,9 +11401,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int nFrames; - int fInputs; + int fXInputs; + int fXState; int fVerbose; - extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose ); + extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11301,10 +11412,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFrames = 10; - fInputs = 0; + fXInputs = 0; + fXState = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Fisvh" ) ) != EOF ) { switch ( c ) { @@ -11320,7 +11432,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; break; case 'i': - fInputs ^= 1; + fXInputs ^= 1; + break; + case 's': + fXState ^= 1; break; case 'v': fVerbose ^= 1; @@ -11343,14 +11458,15 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose ); + Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose ); return 0; usage: - fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" ); + fprintf( pErr, "usage: xsim [-F num] [-isvh]\n" ); fprintf( pErr, "\t performs X-valued simulation of the AIG\n" ); fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); - fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" ); + fprintf( pErr, "\t-i : toggle X-valued representation of inputs [default = %s]\n", fXInputs? "yes": "no" ); + fprintf( pErr, "\t-s : toggle X-valued representation of state [default = %s]\n", fXState? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -11674,11 +11790,12 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) char ** pArgvNew; int nArgcNew; int c; + int fRetimeFirst; int fVerbose; int fVeryVerbose; int nFrames; - extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11686,10 +11803,11 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFrames = 0; // if 0, iterates through frames - fVerbose = 1; + fRetimeFirst = 1; + fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) { switch ( c ) { @@ -11704,6 +11822,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFrames <= 0 ) goto usage; break; + case 'r': + fRetimeFirst ^= 1; + break; case 'w': fVeryVerbose ^= 1; break; @@ -11727,18 +11848,19 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform verification - Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose ); + Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: - fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" ); + fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); - fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); @@ -11746,6 +11868,95 @@ usage: fprintf( pErr, "\t if one file is given, uses the current network and the file\n"); return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fRetimeFirst; + int fVerbose; + int fVeryVerbose; + int nFrames; + + extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 0; // if 0, iterates through frames + fRetimeFirst = 1; + fVerbose = 0; + fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames <= 0 ) + goto usage; + break; + case 'r': + fRetimeFirst ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + printf( "The network has no latches. Used combinational command \"iprove\".\n" ); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } + + // perform verification + Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" ); + fprintf( pErr, "\t performs SEC on the sequential miter\n" ); + fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ce783c95..40a52ce8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -122,6 +122,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew; Aig_Obj_t * pObj; int i; assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); @@ -141,7 +142,19 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Vec_PtrFree( vNodes ); // connect the PO nodes Aig_ManForEachPo( pMan, pObj, i ) + { + if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) + break; Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + // if there are assertions, add them + if ( pMan->nAsserts > 0 ) + Aig_ManForEachAssert( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreateAssert(pNtkNew); + Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); + Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); return pNtkNew; @@ -194,7 +207,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Vec_PtrFree( vNodes ); // connect the PO nodes Aig_ManForEachPo( pMan, pObj, i ) + { + if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) + break; Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } + // if there are assertions, add them + if ( pMan->nAsserts > 0 ) + Aig_ManForEachAssert( pMan, pObj, i ) + { + pObjNew = Abc_NtkCreateAssert(pNtkNew); + Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); + Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + } if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); return pNtkNew; @@ -892,7 +917,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -916,7 +941,7 @@ PRT( "Initial fraiging time", clock() - clk ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -929,6 +954,34 @@ PRT( "Initial fraiging time", clock() - clk ); /**Function************************************************************* + Synopsis [Computes latch correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL ); + Aig_ManStop( pTemp ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + Synopsis [Gives the current ABC network to AIG manager for processing.] Description [] @@ -938,11 +991,40 @@ PRT( "Initial fraiging time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) { - Fraig_Params_t Params; Aig_Man_t * pMan; - Abc_Ntk_t * pMiter, * pTemp; + int RetValue; + // derive the AIG manager + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + // perform verification + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +{ +// Fraig_Params_t Params; + Aig_Man_t * pMan; + Abc_Ntk_t * pMiter;//, * pTemp; int RetValue; // get the miter of the two networks @@ -971,6 +1053,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo return 1; } + // commented out because something became non-inductive +/* // preprocess the miter by fraiging it // (note that for each functional class, fraiging leaves one representative; // so fraiging does not reduce the number of functions represented by nodes @@ -978,7 +1062,25 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo Params.nBTLimit = 100000; pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 ); Abc_NtkDelete( pTemp ); - + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } +*/ // derive the AIG manager pMan = Abc_NtkToDar( pMiter, 1 ); Abc_NtkDelete( pMiter ); @@ -990,7 +1092,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose ); Aig_ManStop( pMan ); return RetValue; } @@ -1006,15 +1108,19 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; - pMan = Aig_ManReduceLaches( pMan, fVerbose ); - pMan = Aig_ManConstReduce( pMan, fVerbose ); + Aig_ManSeqCleanup( pMan ); + if ( fLatchSweep ) + { + pMan = Aig_ManReduceLaches( pMan, fVerbose ); + pMan = Aig_ManConstReduce( pMan, fVerbose ); + } pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; @@ -1038,6 +1144,8 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; +// Aig_ManReduceLachesCount( pMan ); + pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 ); Aig_ManStop( pTemp ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 004d1f39..f9b053ba 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -213,6 +213,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) printf( "Total nodes = %6d %6.2f Mb Changes = %6d.\n", s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges ); */ + +// if ( Abc_NtkHasSop(pNtk) ) +// printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) ); } /**Function************************************************************* diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 4fdb7cbc..69373597 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -233,7 +233,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) // perform strashing nNewCis = 0; Abc_NtkCleanCopy( pNtk2 ); - Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1); + if ( Abc_NtkIsStrash(pNtk2) ) + Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1); Abc_NtkForEachCi( pNtk2, pObj, i ) { pName = Abc_ObjName(pObj); diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index c05823da..5d9e4634 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -103,7 +103,7 @@ static inline void Abc_XsimPrint( FILE * pFile, int Value ) SeeAlso [] ***********************************************************************/ -void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose ) +void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose ) { Abc_Obj_t * pObj; int i, f; @@ -111,20 +111,26 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer srand( 0x12341234 ); // start simulation Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 ); - if ( fInputs ) + if ( fXInputs ) { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, XVSX ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) ); } else { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + } + if ( fXState ) + { Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX ); } + else + { + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) ); + } // simulate and print the result fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" ); for ( f = 0; f < nFrames; f++ ) @@ -147,14 +153,24 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer fprintf( stdout, " : " ); Abc_NtkForEachPo( pNtk, pObj, i ) Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); + if ( Abc_NtkAssertNum(pNtk) ) + { + fprintf( stdout, " : " ); + Abc_NtkForEachAssert( pNtk, pObj, i ) + Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); + } fprintf( stdout, "\n" ); // assign input values - if ( fInputs ) + if ( fXInputs ) + { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, XVSX ); + } else + { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + } // transfer the latch values Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) ); diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index a92ef934..d11fd793 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Fxu_Single * pSingle; Fxu_Double * pDouble; int Weight1, Weight2, Weight3; + int Counter = 0; s_MemoryTotal = 0; s_MemoryPeak = 0; @@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) { Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ); if ( pData->fVerbose ) - printf( "Best single = %3d.\n", Weight1 ); + printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 ); if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 ) Fxu_UpdateSingle( p ); else @@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) { Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d.\n", Weight2 ); + printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 ); if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 ) Fxu_UpdateDouble( p ); else @@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 ); + printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 ); //Fxu_Select( p, &pSingle, &pDouble ); if ( Weight1 >= Weight2 ) @@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) // select the best single and double Weight3 = Fxu_Select( p, &pSingle, &pDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", - Weight2, Weight1, Weight3 ); + printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", + Counter++, Weight2, Weight1, Weight3 ); if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 ) Fxu_Update( p, pSingle, pDouble ); @@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) } if ( pData->fVerbose ) - printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 ); + printf( "Total single = %3d. Total double = %3d. Total compl = %3d. \n", + p->nDivs1, p->nDivs2, p->nDivs3 ); // create the new covers if ( pData->nNodesNew ) diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index 7025d019..e6d0b69e 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -55,7 +55,8 @@ struct FxuDataStruct bool fUseCompl; // set to 1 to have complement taken into account bool fVerbose; // set to 1 to have verbose output int nNodesExt; // the number of divisors to extract - int nPairsMax; // the maximum number of cube pairs to consider + int nSingleMax; // the max number of single-cube divisors to consider + int nPairsMax; // the max number of double-cube divisors to consider // the input information Vec_Ptr_t * vSops; // the SOPs for each node in the network Vec_Ptr_t * vFanins; // the fanins of each node in the network diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c index 99942a88..e3300df9 100644 --- a/src/opt/fxu/fxuCreate.c +++ b/src/opt/fxu/fxuCreate.c @@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) // consider the case when cube pairs should be preprocessed // before adding them to the set of divisors +// if ( pData->fVerbose ) +// printf( "The total number of cube pairs is %d.\n", nPairsTotal ); + if ( nPairsTotal > 10000000 ) + { + printf( "The total number of cube pairs of the network is more than 10,000,000.\n" ); + printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" ); + printf( "that the user changes the network by reducing the size of logic node and\n" ); + printf( "consequently the number of cube pairs to be processed by this command.\n" ); + printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" ); + printf( "as a proprocessing step, while selecting <num> as approapriate.\n" ); + return NULL; + } if ( nPairsTotal > pData->nPairsMax ) if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) ) return NULL; +// if ( pData->fVerbose ) +// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax ); // add the var pairs to the heap - Fxu_MatrixComputeSingles( p ); + Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax ); // print stats if ( pData->fVerbose ) @@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) p->lVars.nItems, p->lCubes.nItems ); fprintf( stdout, "Lits = %d Density = %.5f%%\n", p->nEntries, Density ); - fprintf( stdout, "1-cube divisors = %6d. ", p->lSingles.nItems ); - fprintf( stdout, "2-cube divisors = %6d. ", p->nDivsTotal ); - fprintf( stdout, "Cube pairs = %6d.", nPairsTotal ); + fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal ); + fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal ); fprintf( stdout, "\n" ); } // Fxu_MatrixPrint( stdout, p ); diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h index 0ae1d79e..ea85cb79 100644 --- a/src/opt/fxu/fxuInt.h +++ b/src/opt/fxu/fxuInt.h @@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words // the single cube divisors Fxu_ListSingle lSingles; // the linked list of single cube divisors Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix + int nWeightLimit;// the limit on weight of single cube divisors collected + int nSingleTotal;// the total number of single cube divisors // storage for cube pairs Fxu_Pair *** pppPairs; Fxu_Pair ** ppPairs; @@ -459,7 +461,7 @@ extern void Fxu_PairClearStorage( Fxu_Cube * pCube ); extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 ); extern void Fxu_PairAdd( Fxu_Pair * pPair ); /*===== fxuSingle.c ====================================================*/ -extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p ); +extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax ); extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ); extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 ); /*===== fxuMatrix.c ====================================================*/ diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c index be90e159..73d9a76c 100644 --- a/src/opt/fxu/fxuSingle.c +++ b/src/opt/fxu/fxuSingle.c @@ -17,11 +17,14 @@ ***********************************************************************/ #include "fxuInt.h" +#include "vec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -38,12 +41,130 @@ SeeAlso [] ***********************************************************************/ -void Fxu_MatrixComputeSingles( Fxu_Matrix * p ) +void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax ) { Fxu_Var * pVar; - // iterate through the columns in the matrix + Vec_Ptr_t * vSingles; + int i, k; + // set the weight limit + p->nWeightLimit = 1 - fUse0; + // iterate through columns in the matrix and collect single-cube divisors + vSingles = Vec_PtrAlloc( 10000 ); Fxu_MatrixForEachVariable( p, pVar ) - Fxu_MatrixComputeSinglesOne( p, pVar ); + Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles ); + p->nSingleTotal = Vec_PtrSize(vSingles) / 3; + // check if divisors should be filtered + if ( Vec_PtrSize(vSingles) > nSingleMax ) + { + int * pWeigtCounts, nDivCount, Weight, i, c;; + assert( Vec_PtrSize(vSingles) % 3 == 0 ); + // count how many divisors have the given weight + pWeigtCounts = ALLOC( int, 1000 ); + memset( pWeigtCounts, 0, sizeof(int) * 1000 ); + for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 ) + { + Weight = (int)Vec_PtrEntry(vSingles, i); + if ( Weight >= 999 ) + pWeigtCounts[999]++; + else + pWeigtCounts[Weight]++; + } + // select the bound on the weight (above this bound, singles will be included) + nDivCount = 0; + for ( c = 999; c >= 0; c-- ) + { + nDivCount += pWeigtCounts[c]; + if ( nDivCount >= nSingleMax ) + break; + } + free( pWeigtCounts ); + // collect singles with the given costs + k = 0; + for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 ) + { + Weight = (int)Vec_PtrEntry(vSingles, i); + if ( Weight < c ) + continue; + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) ); + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) ); + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) ); + if ( k/3 == nSingleMax ) + break; + } + Vec_PtrShrink( vSingles, k ); + // adjust the weight limit + p->nWeightLimit = c; + } + // collect the selected divisors + assert( Vec_PtrSize(vSingles) % 3 == 0 ); + for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 ) + { + Fxu_MatrixAddSingle( p, + Vec_PtrEntry(vSingles,i), + Vec_PtrEntry(vSingles,i+1), + (int)Vec_PtrEntry(vSingles,i+2) ); + } + Vec_PtrFree( vSingles ); +} + +/**Function************************************************************* + + Synopsis [Adds the single-cube divisors associated with a new column.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles ) +{ + Fxu_Lit * pLitV, * pLitH; + Fxu_Var * pVar2; + int Coin; + int WeightCur; + + // start collecting the affected vars + Fxu_MatrixRingVarsStart( p ); + // go through all the literals of this variable + for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext ) + // for this literal, go through all the horizontal literals + for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev ) + { + // get another variable + pVar2 = pLitH->pVar; + // skip the var if it is already used + if ( pVar2->pOrder ) + continue; + // skip the var if it belongs to the same node +// if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] ) +// continue; + // collect the var + Fxu_MatrixRingVarsAdd( p, pVar2 ); + } + // stop collecting the selected vars + Fxu_MatrixRingVarsStop( p ); + + // iterate through the selected vars + Fxu_MatrixForEachVarInRing( p, pVar2 ) + { + // count the coincidence + Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar ); + assert( Coin > 0 ); + // get the new weight + WeightCur = Coin - 2; + // peformance fix (August 24, 2007) + if ( WeightCur >= p->nWeightLimit ) + { + Vec_PtrPush( vSingles, pVar2 ); + Vec_PtrPush( vSingles, pVar ); + Vec_PtrPush( vSingles, (void *)WeightCur ); + } + } + + // unmark the vars + Fxu_MatrixRingVarsUnmark( p ); } /**Function************************************************************* @@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p ) ***********************************************************************/ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) { -// int * pValue2Node = p->pValue2Node; Fxu_Lit * pLitV, * pLitH; Fxu_Var * pVar2; int Coin; -// int CounterAll; -// int CounterTest; int WeightCur; // start collecting the affected vars @@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) { // get another variable pVar2 = pLitH->pVar; -// CounterAll++; // skip the var if it is already used if ( pVar2->pOrder ) continue; @@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) // iterate through the selected vars Fxu_MatrixForEachVarInRing( p, pVar2 ) { -// CounterTest++; // count the coincidence Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar ); assert( Coin > 0 ); // get the new weight WeightCur = Coin - 2; - if ( WeightCur >= 0 ) + // peformance fix (August 24, 2007) +// if ( WeightCur >= 0 ) +// Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur ); + if ( WeightCur >= p->nWeightLimit ) Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur ); } - // unmark the vars Fxu_MatrixRingVarsUnmark( p ); } diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c index a430b9c1..274f79f6 100644 --- a/src/opt/fxu/fxuUpdate.c +++ b/src/opt/fxu/fxuUpdate.c @@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p ) { Fxu_Single * pSingle, * pSingle2; int WeightNew; + int Counter = 0; Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 ) { // if at least one of the variables is marked, recalculate if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder ) { + Counter++; // get the new weight WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 ); if ( WeightNew >= 0 ) @@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p ) } } } +// printf( "Called procedure %d times.\n", Counter ); } /**Function************************************************************* |