From ddc6d1c1682a18e293399b7d6c9f4a9018c30c70 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 28 Aug 2007 08:01:00 -0700 Subject: Version abc70828 --- src/aig/aig/aig.h | 15 +- src/aig/aig/aigMan.c | 331 ------------------------- src/aig/aig/aigPart.c | 2 +- src/aig/aig/aigRepr.c | 2 +- src/aig/aig/aigScl.c | 370 ++++++++++++++++++++++++++++ src/aig/aig/aigTsim.c | 4 +- src/aig/aig/aigUtil.c | 14 +- src/aig/aig/module.make | 2 + src/aig/fra/fra.h | 22 +- src/aig/fra/fraBmc.c | 128 +++++++--- src/aig/fra/fraClass.c | 9 +- src/aig/fra/fraCore.c | 33 ++- src/aig/fra/fraImp.c | 202 ++++++++++++--- src/aig/fra/fraInd.c | 131 ++++++++-- src/aig/fra/fraLcr.c | 644 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/fra/fraMan.c | 8 +- src/aig/fra/fraSec.c | 136 +++++++++- src/aig/fra/fraSim.c | 12 +- src/aig/fra/module.make | 1 + 19 files changed, 1606 insertions(+), 460 deletions(-) create mode 100644 src/aig/aig/aigScl.c create mode 100644 src/aig/fra/fraLcr.c (limited to 'src/aig') 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 @@ -170,54 +170,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) return pNew; } -/**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.] @@ -295,110 +247,6 @@ void Aig_ManStop( Aig_Man_t * p ) free( p ); } -/**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.] @@ -428,42 +276,6 @@ int Aig_ManCleanup( Aig_Man_t * p ) return nNodesOld - Aig_ManNodeNum(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.] @@ -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; } @@ -213,34 +275,6 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p ) return pAigFrames; } -/**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.] @@ -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,14 +24,31 @@ /// 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 /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Counts the number of 1s in each siminfo of each node.] + + Description [] + + SideEffects [] + + 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.] @@ -46,16 +63,11 @@ static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) 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; } @@ -104,6 +116,27 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) return Counter; } +/**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.] @@ -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 @@ -175,6 +175,61 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) return pManFraig; } +/**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.] @@ -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 \ -- cgit v1.2.3