diff options
Diffstat (limited to 'src')
35 files changed, 2184 insertions, 164 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 2e409312..0cdd5b1a 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -328,6 +328,8 @@ static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj- static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; } static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild0Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pNext, Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pNext, Aig_ObjFaninC1(pObj)) : NULL; } static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); } static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; } @@ -637,6 +639,7 @@ extern void Aig_ManCleanMarkB( Aig_Man_t * p ); extern void Aig_ManCleanMarkAB( Aig_Man_t * p ); extern void Aig_ManCleanData( Aig_Man_t * p ); extern void Aig_ObjCleanData_rec( Aig_Obj_t * pObj ); +extern void Aig_ManCleanNext( Aig_Man_t * p ); extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper ); extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj ); extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 ); diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index e5b4d2c7..2668bbb2 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -206,6 +206,25 @@ void Aig_ManCleanData( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Cleans the data pointers for the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCleanNext( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + pObj->pNext = NULL; +} + +/**Function************************************************************* + Synopsis [Recursively cleans the data pointers in the cone of the node.] Description [Applicable to small AIGs only because no caching is performed.] diff --git a/src/aig/cgt/cgt.h b/src/aig/cgt/cgt.h new file mode 100644 index 00000000..b9997d56 --- /dev/null +++ b/src/aig/cgt/cgt.h @@ -0,0 +1,81 @@ +/**CFile**************************************************************** + + FileName [cgt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CGT_H__ +#define __CGT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +/* + The algorithm implemented in this package is based on the paper: + A. Hurst. "Automatic synthesis of clock gating logic with controlled + netlist perturbation", DAC 2008. +*/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cgt_Par_t_ Cgt_Par_t; +struct Cgt_Par_t_ +{ + int nLevelMax; // the max number of levels to look for clock-gates + int nCandMax; // the max number of candidates at each node + int nOdcMax; // the max number of ODC levels to consider + int nConfMax; // the max number of conflicts at a node + int nVarsMin; // the min number of variables to recycle the SAT solver + int nFlopsMin; // the min number of flops needed to recycle the SAT solver + int fVerbose; // verbosity flag + +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cgtCore.c ==========================================================*/ +extern void Cgt_SetDefaultParams( Cgt_Par_t * p ); +extern Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ); +extern Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cgt/cgtAig.c b/src/aig/cgt/cgtAig.c new file mode 100644 index 00000000..b30d3f16 --- /dev/null +++ b/src/aig/cgt/cgtAig.c @@ -0,0 +1,311 @@ +/**CFile**************************************************************** + + FileName [cgtAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [Creates AIG to compute clock-gating.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cgtInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes transitive fanout cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManDetectCandidates_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsNode(pObj) ) + { + Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin0(pObj), nLevelMax, vCands ); + Cgt_ManDetectCandidates_rec( pAig, Aig_ObjFanin1(pObj), nLevelMax, vCands ); + } + if ( Aig_ObjLevel(pObj) <= nLevelMax ) + Vec_PtrPush( vCands, pObj ); +} + +/**Function************************************************************* + + Synopsis [Computes transitive fanout cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands ) +{ + Vec_PtrClear( vCands ); + if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) ) + return; + Aig_ManIncrementTravId( pAig ); + Cgt_ManDetectCandidates_rec( pAig, pObj, nLevelMax, vCands ); +} + +/**Function************************************************************* + + Synopsis [Computes transitive fanout cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManDetectFanout_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout ) +{ + Aig_Obj_t * pFanout; + int f, iFanout; + if ( Aig_ObjIsPo(pObj) || Aig_ObjLevel(pObj) > nOdcMax ) + return; + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + Vec_PtrPush( vFanout, pObj ); + Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f ) + Cgt_ManDetectFanout_rec( pAig, pFanout, nOdcMax, vFanout ); +} + +/**Function************************************************************* + + Synopsis [Computes transitive fanout cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout ) +{ + Aig_Obj_t * pFanout; + int i, k, f, iFanout; + // collect visited nodes + Vec_PtrClear( vFanout ); + Aig_ManIncrementTravId( pAig ); + Cgt_ManDetectFanout_rec( pAig, pObj, nOdcMax, vFanout ); + // remove those nodes whose fanout is included + k = 0; + Vec_PtrForEachEntry( vFanout, pObj, i ) + { + // go through the fanouts of this node + Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, f ) + if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) ) + break; + if ( f == Aig_ObjRefs(pObj) ) // all fanouts are included + continue; + Vec_PtrWriteEntry( vFanout, k++, pObj ); + } + Vec_PtrShrink( vFanout, k ); + Vec_PtrSort( vFanout, Aig_ObjCompareIdIncrease ); + assert( Vec_PtrSize(vFanout) > 0 ); +} + +/**Function************************************************************* + + Synopsis [Derives miter for clock-gating.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cgt_ManConstructMiter( Cgt_Man_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObjLo ) +{ + Aig_Obj_t * pMiter, * pRoot; + int i; + assert( Aig_ObjIsPi(pObjLo) ); + pMiter = Aig_ManConst0( pNew ); + Cgt_ManDetectFanout( p->pAig, pObjLo, p->pPars->nOdcMax, p->vFanout ); + Vec_PtrForEachEntry( p->vFanout, pRoot, i ) + pMiter = Aig_Or( pNew, pMiter, Aig_Exor(pNew, pRoot->pData, pRoot->pNext) ); + return pMiter; +} + +/**Function************************************************************* + + Synopsis [Derives AIG for clock-gating.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i; + assert( Aig_ManRegNum(p->pAig) ); + Aig_ManCleanNext( p->pAig ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p->pAig) ); + // build the first frame + Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p->pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +// Saig_ManForEachPo( p->pAig, pObj, i ) +// pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // build the second frame + Aig_ManConst1(p->pAig)->pNext = Aig_ManConst1(pNew); + Saig_ManForEachPi( p->pAig, pObj, i ) + pObj->pNext = Aig_ObjCreatePi( pNew ); + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + pObjLo->pNext = Aig_ObjChild0Copy(pObjLi); + Aig_ManForEachNode( p->pAig, pObj, i ) + if ( Aig_ObjLevel(pObj) <= p->pPars->nOdcMax ) + pObj->pNext = Aig_And( pNew, Aig_ObjChild0Next(pObj), Aig_ObjChild1Next(pObj) ); + // construct clock-gating miters for each register input + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + pObjLi->pData = Aig_ObjCreatePo( pNew, Cgt_ManConstructMiter(p, pNew, pObjLo) ); + Aig_ManCleanNext( p->pAig ); + Aig_ManSetPioNumbers( p->pAig ); + Aig_ManCleanup( pNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Cgt_ManDupPartition_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsPi(pObj) ) + return pObj->pData = Aig_ObjCreatePi( pNew ); + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Duplicates register outputs starting from the given one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(pAig) == 0 ); + pNew = Aig_ManStart( nVarsMin ); + Aig_ManIncrementTravId( pAig ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew); + Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); + for ( i = iStart; i < iStart + nFlopsMin && i < Aig_ManPoNum(pAig); i++ ) + { + pObj = Aig_ManPo( pAig, i ); + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + for ( ; Aig_ManObjNum(pNew) < nVarsMin && i < Aig_ManPoNum(pAig); i++ ) + { + pObj = Aig_ManPo( pAig, i ); + Cgt_ManDupPartition_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + assert( nFlopsMin >= Aig_ManPoNum(pAig) || Aig_ManPoNum(pNew) >= nFlopsMin ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derives AIG after clock-gating.] + + Description [The array contains, for each flop, its gate if present.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo, * pGate, * pGateNew; + int i; + assert( Aig_ManRegNum(pAig) ); + pNew = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Saig_ManForEachPo( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pGate = Vec_PtrEntry( vGates, i ); + if ( pGate == NULL ) + pObjNew = Aig_ObjChild0Copy(pObjLi); + else + { + pGateNew = Aig_NotCond( Aig_Regular(pGate)->pData, Aig_IsComplement(pGate) ); + pObjNew = Aig_Mux( pNew, pGateNew, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); + } + pObjLi->pData = Aig_ObjCreatePo( pNew, pObjNew ); + } + Aig_ManCleanup( pNew ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cgt/cgtCore.c b/src/aig/cgt/cgtCore.c new file mode 100644 index 00000000..a06820b4 --- /dev/null +++ b/src/aig/cgt/cgtCore.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [cgtCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cgtInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_SetDefaultParams( Cgt_Par_t * p ) +{ + memset( p, 0, sizeof(Cgt_Par_t) ); + p->nLevelMax = 1000; // the max number of levels to look for clock-gates + p->nCandMax = 1000; // the max number of candidates at each node + p->nOdcMax = 0; // the max number of ODC levels to consider + p->nConfMax = 1000; // the max number of conflicts at a node + p->nVarsMin = 5000; // the min number of vars to recycle the SAT solver + p->nFlopsMin = 25; // the min number of flops to recycle the SAT solver + p->fVerbose = 0; // verbosity flag +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation does not filter out this candidate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cgt_SimulationFilter( Cgt_Man_t * p, Aig_Obj_t * pCandFrame, Aig_Obj_t * pMiterFrame ) +{ + unsigned * pInfoCand, * pInfoMiter; + int w, nWords = Aig_BitWordNum( p->nPatts ); + pInfoCand = Vec_PtrEntry( p->vPatts, Aig_ObjId(Aig_Regular(pCandFrame)) ); + pInfoMiter = Vec_PtrEntry( p->vPatts, Aig_ObjId(pMiterFrame) ); + // C => !M -- true is the same as C & M -- false + if ( !Aig_IsComplement(pCandFrame) ) + { + for ( w = 0; w < nWords; w++ ) + if ( pInfoCand[w] & pInfoMiter[w] ) + return 0; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pInfoCand[w] & pInfoMiter[w] ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Saves one simulation pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_SimulationRecord( Cgt_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p->pPart, pObj, i ) + if ( sat_solver_var_value( p->pSat, p->pCnf->pVarNums[i] ) ) + Aig_InfoSetBit( Vec_PtrEntry(p->vPatts, i), p->nPatts ); + p->nPatts++; + if ( p->nPatts == 32 * p->nPattWords ) + { + Vec_PtrReallocSimInfo( p->vPatts ); + p->nPattWords *= 2; + } +} + +/**Function************************************************************* + + Synopsis [Performs clock-gating for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart ) +{ + Vec_Ptr_t * vNodes = p->vFanout; + Aig_Obj_t * pMiter, * pCand, * pMiterFrame, * pCandFrame, * pMiterPart, * pCandPart; + int i, k, RetValue; + assert( Vec_VecSize(p->vGatesAll) == Aig_ManPoNum(p->pFrame) ); + // go through all the registers inputs of this range + for ( i = iStart; i < iStart + Aig_ManPoNum(p->pPart); i++ ) + { + pMiter = Saig_ManLi( p->pAig, i ); + Cgt_ManDetectCandidates( p->pAig, Aig_ObjFanin0(pMiter), p->pPars->nLevelMax, vNodes ); + // go through the candidates of this PO + Vec_PtrForEachEntry( vNodes, pCand, k ) + { + // get the corresponding nodes from the frames + pCandFrame = pCand->pData; + pMiterFrame = pMiter->pData; + // get the corresponding nodes from the part + pCandPart = pCandFrame->pData; + pMiterPart = pMiterFrame->pData; + // try direct polarity + if ( Cgt_SimulationFilter( p, pCandPart, pMiterPart ) ) + { + RetValue = Cgt_CheckImplication( p, pCandPart, pMiterPart ); + if ( RetValue == 1 ) + { + Vec_VecPush( p->vGatesAll, i, pCand ); + continue; + } + if ( RetValue == 0 ) + Cgt_SimulationRecord( p ); + } + // try reverse polarity + if ( Cgt_SimulationFilter( p, Aig_Not(pCandPart), pMiterPart ) ) + { + RetValue = Cgt_CheckImplication( p, Aig_Not(pCandPart), pMiterPart ); + if ( RetValue == 1 ) + { + Vec_VecPush( p->vGatesAll, i, Aig_Not(pCand) ); + continue; + } + if ( RetValue == 0 ) + Cgt_SimulationRecord( p ); + } + } + } +} + +/**Function************************************************************* + + Synopsis [Performs clock-gating for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart ) +{ + int iStop; + p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart ); + p->pCnf = Cnf_DeriveSimple( p->pPart, Aig_ManPoNum(p->pPart) ); + p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + sat_solver_compress( p->pSat ); + p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), 16 ); + Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords ); + Cgt_ClockGatingRangeCheck( p, iStart ); + iStop = iStart + Aig_ManPoNum(p->pPart); + Cgt_ManClean( p ); + return iStop; +} + +/**Function************************************************************* + + Synopsis [Performs clock-gating for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ) +{ + Cgt_Par_t Pars; + Cgt_Man_t * p; + Vec_Vec_t * vGatesAll; + int iStart; + if ( pPars == NULL ) + Cgt_SetDefaultParams( pPars = &Pars ); + p = Cgt_ManCreate( pAig, pCare, pPars ); + p->pFrame = Cgt_ManDeriveAigForGating( p ); + assert( Aig_ManPoNum(p->pFrame) == Saig_ManRegNum(p->pAig) ); + for ( iStart = 0; iStart < Aig_ManPoNum(p->pFrame); ) + iStart = Cgt_ClockGatingRange( p, iStart ); + vGatesAll = p->vGatesAll; + return vGatesAll; +} + +/**Function************************************************************* + + Synopsis [Performs clock-gating for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ) +{ + Aig_Man_t * pGated; + Vec_Vec_t * vGatesAll; + Vec_Ptr_t * vGates; + vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars ); + vGates = Cgt_ManDecideSimple( pAig, vGatesAll ); + pGated = Cgt_ManDeriveGatedAig( pAig, vGates ); + Vec_PtrFree( vGates ); + Vec_VecFree( vGatesAll ); + return pGated; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cgt/cgtDecide.c b/src/aig/cgt/cgtDecide.c new file mode 100644 index 00000000..8f57bd4a --- /dev/null +++ b/src/aig/cgt/cgtDecide.c @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [cgtMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [Decide what gate to use for what flop.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cgtInt.h" +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ); +extern int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Chooses what clock-gate to use for each register.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) +{ + Vec_Ptr_t * vGates; + vGates = Vec_PtrStart( Saig_ManRegNum(pAig) ); + return vGates; +} + +/**Function************************************************************* + + Synopsis [Chooses what clock-gate to use for this register.] + + Description [Currently uses the naive approach: For each register, + choose the clock gate, which covers most of the transitions.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ) +{ + Ssw_Sml_t * pSml; + Vec_Ptr_t * vGates, * vCands; + Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest; + int i, k, nHitsCur, nHitsMax; + vGates = Vec_PtrStart( Saig_ManRegNum(pAig) ); + pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 1 ); + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + nHitsMax = 0; + pCandBest = NULL; + vCands = Vec_VecEntry( vGatesAll, i ); + Vec_PtrForEachEntry( vCands, pCand, k ) + { + // check if this is indeed a clock-gate + if ( !Ssw_SmlCheckXorImplication( pSml, pObjLi, pObjLo, pCand ) ) + printf( "Clock gate candidate is invalid!\n" ); + // find its characteristic number + nHitsCur = Ssw_SmlCountXorImplication( pSml, pObjLi, pObjLo, pCand ); + if ( nHitsMax < nHitsCur ) + { + nHitsMax = nHitsCur; + pCandBest = pCand; + } + } + if ( pCandBest != NULL ) + Vec_PtrWriteEntry( vGates, i, pCandBest ); + } + Ssw_SmlStop( pSml ); + return vGates; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cgt/cgtInt.h b/src/aig/cgt/cgtInt.h new file mode 100644 index 00000000..7b4b6e63 --- /dev/null +++ b/src/aig/cgt/cgtInt.h @@ -0,0 +1,107 @@ +/**CFile**************************************************************** + + FileName [cgtInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CGT_INT_H__ +#define __CGT_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "saig.h" +#include "satSolver.h" +#include "cnf.h" +#include "cgt.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cgt_Man_t_ Cgt_Man_t; +struct Cgt_Man_t_ +{ + // user's data + Cgt_Par_t * pPars; // user's parameters + Aig_Man_t * pAig; // user's AIG manager + Aig_Man_t * pCare; // user's constraints + Vec_Vec_t * vGatesAll; // the computed clock-gates + Vec_Ptr_t * vGates; // the selected clock-gates + // internal data + Aig_Man_t * pFrame; // clock gate AIG manager + Vec_Ptr_t * vFanout; // temporary storage for fanouts + // SAT solving + Aig_Man_t * pPart; // partition + Cnf_Dat_t * pCnf; // CNF of the partition + sat_solver * pSat; // SAT solver + Vec_Ptr_t * vPatts; // simulation patterns + int nPatts; // the number of patterns accumulated + int nPattWords; // the number of pattern words + // statistics + int nCalls; // total calls + int nCallsSat; // satisfiable calls + int nCallsUnsat; // unsatisfiable calls + int nCallsUndec; // undecided calls + int timeSat; // total runtime + int timeSatSat; // satisfiable runtime + int timeSatUnsat; // unsatisfiable runtime + int timeSatUndec; // undecided runtime +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cgtAig.c ==========================================================*/ +extern void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax, Vec_Ptr_t * vCands ); +extern Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ); +extern Aig_Man_t * Cgt_ManDupPartition( Aig_Man_t * pAig, int nVarsMin, int nFlopsMin, int iStart ); +extern Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Ptr_t * vGates ); +/*=== cgtDecide.c ==========================================================*/ +extern Vec_Ptr_t * Cgt_ManDecide( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ); +extern Vec_Ptr_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll ); +/*=== cgtMan.c ==========================================================*/ +extern Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ); +extern void Cgt_ManClean( Cgt_Man_t * p ); +extern void Cgt_ManStop( Cgt_Man_t * p ); +/*=== cgtSat.c ==========================================================*/ +extern int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pFlop ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c new file mode 100644 index 00000000..9615d2e6 --- /dev/null +++ b/src/aig/cgt/cgtMan.c @@ -0,0 +1,168 @@ +/**CFile**************************************************************** + + FileName [cgtMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [Manipulation of clock gating manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cgtInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPars ) +{ + Cgt_Man_t * p; + // prepare the sequential AIG + assert( Saig_ManRegNum(pAig) > 0 ); + Aig_ManFanoutStart( pAig ); + Aig_ManSetPioNumbers( pAig ); + // create interpolation manager + p = ALLOC( Cgt_Man_t, 1 ); + memset( p, 0, sizeof(Cgt_Man_t) ); + p->pPars = pPars; + p->pAig = pAig; + p->vGatesAll = Vec_VecStart( Saig_ManRegNum(pAig) ); + p->vFanout = Vec_PtrAlloc( 1000 ); + p->nPattWords = 16; + return p; +} + +/**Function************************************************************* + + Synopsis [Creates the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManClean( Cgt_Man_t * p ) +{ + if ( p->pPart ) + { + Aig_ManStop( p->pPart ); + p->pPart = NULL; + } + if ( p->pCnf ) + { + Cnf_DataFree( p->pCnf ); + p->pCnf = NULL; + } + if ( p->pSat ) + { + sat_solver_delete( p->pSat ); + p->pSat = NULL; + } + if ( p->vPatts ) + { + Vec_PtrFree( p->vPatts ); + p->vPatts = NULL; + } +} + + +/**Function************************************************************* + + Synopsis [Prints stats of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManPrintStats( Cgt_Man_t * p ) +{ +/* + double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); + + printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), + 0/p->pPars->nIters ); + printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Cgt_ManCountEquivs(p) ); + printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", + p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds ); + 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->nNodesBeg:1), + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); + + p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; + PRTP( "BMC ", p->timeBmc, p->timeTotal ); + PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); + PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); + PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); + PRTP( " undecided", p->timeSatUndec, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); +*/ +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cgt_ManStop( Cgt_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Cgt_ManPrintStats( p ); + if ( p->pFrame ) + Aig_ManStop( p->pFrame ); + Cgt_ManClean( p ); + Vec_PtrFree( p->vFanout ); + Vec_PtrFree( p->vGates ); + Vec_VecFree( p->vGatesAll ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cgt/cgtSat.c b/src/aig/cgt/cgtSat.c new file mode 100644 index 00000000..094fb47d --- /dev/null +++ b/src/aig/cgt/cgtSat.c @@ -0,0 +1,92 @@ +/**CFile**************************************************************** + + FileName [cgtSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Clock gating package.] + + Synopsis [Checking implications using SAT.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cgtSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cgtInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Runs equivalence test for the two nodes.] + + Description [Both nodes should be regular and different from each other.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter ) +{ + int nBTLimit = p->pPars->nConfMax; + int pLits[2], RetValue, clk; + p->nCalls++; + + // sanity checks + assert( p->pSat && p->pCnf ); + assert( !Aig_IsComplement(pMiter) ); + assert( Aig_Regular(pGate) != pMiter ); + + // solve under assumptions + // G => !M -- true G & M -- false + pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) ); + pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 ); + +clk = clock(); + RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + sat_solver_compress( p->pSat ); + p->nCallsUnsat++; + return 1; + } + else if ( RetValue == l_True ) + { +p->timeSatSat += clock() - clk; + p->nCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nCallsUndec++; + return -1; + } + return -2; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cgt/module.make b/src/aig/cgt/module.make new file mode 100644 index 00000000..911d8d1f --- /dev/null +++ b/src/aig/cgt/module.make @@ -0,0 +1,5 @@ +SRC += src/aig/cgt/cgtAig.c \ + src/aig/cgt/cgtCore.c \ + src/aig/cgt/cgtDecide.c \ + src/aig/cgt/cgtMan.c \ + src/aig/cgt/cgtSat.c diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 190281c9..2cdf203d 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -174,7 +174,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) } RetValue = Fra_FraigMiterStatus( pAig ); // assert( RetValue == -1 ); - if ( RetValue >= 0 ) + if ( RetValue == 0 ) { pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) ); memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index cae37f85..ca73b17d 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -348,7 +348,12 @@ clk = clock(); } Aig_ManSetRegNum( pNew, pNew->nRegs ); - pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); +// pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); + if ( Aig_ManRegNum(pNew) > 0 ) + pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); + else + pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); + if ( pNew == NULL ) { pNew = pTemp; diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index a0fca09d..101cf2eb 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -140,6 +140,17 @@ struct Kit_DsdMan_t_ Vec_Int_t * vNodes; // temporary array for BDD nodes }; +#ifdef WIN32 +#define DLLEXPORT __declspec(dllexport) +#define DLLIMPORT __declspec(dllimport) +#else /* defined(WIN32) */ +#define DLLIMPORT +#endif /* defined(WIN32) */ + +#ifndef ABC_DLL +#define ABC_DLL DLLIMPORT +#endif + static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; } static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; } @@ -558,7 +569,7 @@ extern char * Kit_PlaStart( void * p, int nCubes, int nVars ); extern char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover ); extern void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover ); extern char * Kit_PlaStoreSop( void * p, char * pSop ); -extern char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover ); +extern ABC_DLL char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover ); /*=== kitSop.c ==========================================================*/ extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory ); extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory ); diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index a82157c0..54db901f 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: ntl.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $] + Revision [$Id: ntl.h,v 1.3 2008/10/24 14:18:44 mjarvin Exp $] ***********************************************************************/ @@ -308,6 +308,7 @@ extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); extern ABC_DLL Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ); extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ); +extern ABC_DLL Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); /*=== ntlInsert.c ==========================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); extern ABC_DLL Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ); @@ -323,7 +324,6 @@ extern ABC_DLL void Ntl_ManCleanup( Ntl_Man_t * p ); extern ABC_DLL Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p ); extern ABC_DLL Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManFree( Ntl_Man_t * p ); -extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p ); extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p ); @@ -351,16 +351,17 @@ extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFile /*=== ntlSweep.c ==========================================================*/ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ -extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); -extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); +extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName ); +extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName ); +extern ABC_DLL Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName ); extern ABC_DLL void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p ); -extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ); +extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber ); extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelCountNets( Ntl_Mod_t * p ); extern ABC_DLL int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ); -extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); +extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, const char * pName ); /*=== ntlTime.c ==========================================================*/ extern ABC_DLL Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); /*=== ntlReadBlif.c ==========================================================*/ diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index 03e9e898..47f14525 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: ntlCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: ntlCheck.c,v 1.1 2008/10/10 14:09:29 mjarvin Exp $] ***********************************************************************/ @@ -312,10 +312,11 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) Vec_PtrPush( vNets, pNet ); } +#if 0 // sjang // print the warning if ( Vec_PtrSize(vNets) > 0 ) { - printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pModel->pName ); + printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\": ", Vec_PtrSize(vNets), pModel->pName ); Vec_PtrForEachEntry( vNets, pNet, i ) { printf( "%s%s", (i? ", ": ""), pNet->pName ); @@ -328,6 +329,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) } printf( "\n" ); } +#endif Vec_PtrFree( vNets ); } diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 800b711c..d1a1b99d 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - January 8, 2007.] - Revision [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $] + Revision [$Id: ntlReadBlif.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $] ***********************************************************************/ diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c index 991d701a..fc95415d 100644 --- a/src/aig/ntl/ntlSweep.c +++ b/src/aig/ntl/ntlSweep.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: ntlSweep.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $] ***********************************************************************/ @@ -154,8 +154,10 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) // print detailed statistics of sweeping - if ( fVerbose ) + if ( fVerbose && Counter > 0) { + int numLutBox = 0; + printf( "Swept away:" ); printf( " Node = %d (%4.1f %%)", nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE], @@ -175,8 +177,21 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) printf( "Sweep removed %d boxed of %d types (out of %d types):\n", nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], ModelCounter, Vec_PtrSize(p->vModels)-1 ); Ntl_ManForEachModel( p, pMod, i ) - if ( i ) - printf( "Model %3d : %-40s Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems ); + { + if ( i && (pMod->nRems + pMod->nUsed-pMod->nRems) > 0) + { + + if (strncmp(pMod->pName, "LUT", 3) != 0) + { + //printf( "( M%d: %s, S=%d, L=%d ) ", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems ); + //printf( "Model %3d : %-40s Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems ); + } else + { + numLutBox++; + } + } + } + printf("\nLUTboxType =%d\n", numLutBox); } } if ( !Ntl_ManCheck( p ) ) diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index 208b4491..aa122900 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: ntlTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: ntlTable.c,v 1.3 2008/10/24 14:18:44 mjarvin Exp $] ***********************************************************************/ @@ -25,7 +25,7 @@ //////////////////////////////////////////////////////////////////////// // hashing for strings -static unsigned Ntl_HashString( char * pName, int TableSize ) +static unsigned Ntl_HashString( const char * pName, int TableSize ) { static int s_Primes[10] = { 1291, 1699, 2357, 4177, 5147, @@ -52,7 +52,7 @@ static unsigned Ntl_HashString( char * pName, int TableSize ) SeeAlso [] ***********************************************************************/ -Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, char * pName ) +Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, const char * pName ) { Ntl_Net_t * pNet; pNet = (Ntl_Net_t *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, sizeof(Ntl_Net_t) + strlen(pName) + 1 ); @@ -113,7 +113,7 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ) +Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName ) { Ntl_Net_t * pEnt; unsigned Key = Ntl_HashString( pName, p->nTableSize ); @@ -163,7 +163,7 @@ void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet ) SeeAlso [] ***********************************************************************/ -Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) +Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName ) { Ntl_Net_t * pEnt; unsigned Key = Ntl_HashString( pName, p->nTableSize ); @@ -178,6 +178,18 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) return pEnt; } +Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName ) +{ + Ntl_Net_t * pEnt; + unsigned Key = Ntl_HashString( pName, p->nTableSize ); + pEnt = Ntl_ModelCreateNet( p, pName ); + pEnt->pNext = p->pTable[Key]; + p->pTable[Key] = pEnt; + if ( ++p->nEntries > 2 * p->nTableSize ) + Ntl_ModelTableResize( p ); + return pEnt; +} + /**Function************************************************************* Synopsis [Assigns numbers to PIs and POs.] @@ -210,7 +222,7 @@ void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p ) SeeAlso [] ***********************************************************************/ -int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) +int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber ) { Ntl_Net_t * pNet; Ntl_Obj_t * pObj; @@ -273,7 +285,7 @@ int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * SeeAlso [] ***********************************************************************/ -int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) +int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, const char * pName, int * pNumber ) { Ntl_Net_t * pNet; Ntl_Obj_t * pTerm; @@ -461,7 +473,7 @@ int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ) SeeAlso [] ***********************************************************************/ -Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) +Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, const char * pName ) { Ntl_Mod_t * pEnt; unsigned Key = Ntl_HashString( pName, p->nModTableSize ); diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index 252546e8..55cdf42b 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: nwkMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: nwkMan.c,v 1.1 2008/10/10 14:09:30 mjarvin Exp $] ***********************************************************************/ @@ -154,7 +154,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) ParsBest.nPis = ParsNew.nPis; ParsBest.nPos = ParsNew.nPos; // write the network - Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" ); +// Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" ); // Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL ); return 1; } diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 02db900b..d96996cf 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -78,6 +78,8 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== sswAbs.c ==========================================================*/ +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index cfbba7e1..8498f59a 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -28,12 +28,315 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { return Vec_StrGetEntry( p, nObjs*i+pObj->Id ); } +static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 ); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose ) +{ + Vec_Int_t * vCore; + void * pSatCnf; + Intp_Man_t * pManProof; + int RetValue, clk = clock(); + // solve the problem + RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_Undef ) + { + printf( "Conflict limit is reached.\n" ); + return NULL; + } + if ( RetValue == l_True ) + { + printf( "The BMC problem is SAT.\n" ); + return NULL; + } + if ( fVerbose ) + { + printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts ); + PRT( "Time", clock() - clk ); + } + assert( RetValue == l_False ); + pSatCnf = sat_solver_store_release( pSat ); + // derive the UNSAT core + clk = clock(); + pManProof = Intp_ManAlloc(); + vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 ); + Intp_ManFree( pManProof ); + Sto_ManFree( pSatCnf ); + if ( fVerbose ) + { + printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses ); + PRT( "Time", clock() - clk ); + } + return vCore; +} + + +/**Function************************************************************* + + Synopsis [Mark visited nodes recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i ) +{ + if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) ) + return 1; + Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ); + if ( Saig_ObjIsPi( p, pObj ) ) + return 1; + if ( Saig_ObjIsLo( p, pObj ) ) + return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 ); + if ( Aig_ObjIsPo( pObj ) ) + return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); + Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); + Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Mark visited nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax ) +{ + Vec_Str_t * vObj2Visit; + Aig_Obj_t * pObj; + int i, f; + vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax ); + Saig_ManForEachLo( p, pObj, i ) + Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); + for ( f = 0; f < nFramesMax; f++ ) + { + Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f ); + Saig_ManForEachPo( p, pObj, i ) + Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f ); + } + return vObj2Visit; +} + +/**Function************************************************************* + + Synopsis [Performs the actual construction of the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return pObj->pData; + assert( Aig_ObjIsNode(pObj) ); + Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); + Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives a vector of AIG managers, one for each frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) +{ + Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs; + Vec_Str_t * vObj2Visit; + Aig_Man_t * pFrame; + Aig_Obj_t * pObj; + int f, i; + vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax ); + vFrames = Vec_PtrAlloc( nFramesMax ); + vLoObjs = Vec_PtrAlloc( 100 ); + vLiObjs = Vec_PtrAlloc( 100 ); + for ( f = 0; f < nFramesMax; f++ ) + { + Aig_ManCleanData( p ); + pFrame = Aig_ManStart( 1000 ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame); + // create PIs + Vec_PtrClear( vLoObjs ); + Vec_PtrClear( vLiObjs ); + Aig_ManForEachPi( p, pObj, i ) + { + if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) + { + pObj->pData = Aig_ObjCreatePi(pFrame); + if ( i >= Saig_ManPiNum(p) ) + Vec_PtrPush( vLoObjs, pObj ); + } + } + // remember the number of (implicit) registers in this frame + pFrame->nAsserts = Vec_PtrSize(vLoObjs); + // create POs + Aig_ManForEachPo( p, pObj, i ) + if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) + { + Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); + pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) ); + if ( i >= Saig_ManPoNum(p) ) + Vec_PtrPush( vLiObjs, pObj ); + } + Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) ); + // set the new PIs to point to the recorresponding registers + Aig_ManCleanData( pFrame ); + Vec_PtrForEachEntry( vLoObjs, pObj, i ) + ((Aig_Obj_t *)pObj->pData)->pData = pObj; + Vec_PtrForEachEntry( vLiObjs, pObj, i ) + ((Aig_Obj_t *)pObj->pData)->pData = pObj; + if ( fVerbose ) + printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n", + f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) ); + } + Vec_PtrFree( vLoObjs ); + Vec_PtrFree( vLiObjs ); + Vec_StrFree( vObj2Visit ); + return vFrames; +} + +/**Function************************************************************* + + Synopsis [Derives a vector of AIG managers, one for each frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnf, * pCnfPrev; + Vec_Int_t * vPoLits; + Aig_Obj_t * pObjPo, * pObjLi, * pObjLo; + int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters; + // start array of output literals + vPoLits = Vec_IntAlloc( 100 ); + // count the number of CNF variables + nSatVars = 0; + Vec_PtrForEachEntry( vFrames, pCnf, f ) + nSatVars += pCnf->nVars; + + // create the SAT solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, nSatVars ); + + // add clauses for the timeframes + nSatVars = 0; +// Vec_PtrForEachEntryReverse( vFrames, pCnf, f ) + Vec_PtrForEachEntry( vFrames, pCnf, f ) + { + // lift clauses of this CNF + Cnf_DataLift( pCnf, nSatVars ); + nSatVars += pCnf->nVars; + // copy clauses into the manager + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + { + printf( "The BMC problem is trivially UNSAT.\n" ); + sat_solver_delete( pSat ); + Vec_IntFree( vPoLits ); + return NULL; + } + } + // remember output literal + Aig_ManForEachPo( pCnf->pMan, pObjPo, i ) + { + if ( i == Saig_ManPoNum(p) ) + break; + Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) ); + } + } + + // add auxiliary clauses (output, connectors, initial) + // add output clause + if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) + assert( 0 ); + Vec_IntFree( vPoLits ); + + // add connecting clauses + pCnfPrev = Vec_PtrEntry( vFrames, 0 ); + Vec_PtrForEachEntryStart( vFrames, pCnf, f, 1 ) + { + nRegisters = pCnf->pMan->nAsserts; + assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) ); + assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) ); + for ( i = 0; i < nRegisters; i++ ) + { + pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i ); + pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); + // get variable numbers + iVarOld = pCnfPrev->pVarNums[pObjLi->Id]; + iVarNew = pCnf->pVarNums[pObjLo->Id]; + // add clauses connecting existing variables + Lits[0] = toLitCond( iVarOld, 0 ); + Lits[1] = toLitCond( iVarNew, 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( iVarOld, 1 ); + Lits[1] = toLitCond( iVarNew, 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + pCnfPrev = pCnf; + } + // add unit clauses + pCnf = Vec_PtrEntry( vFrames, 0 ); + nRegisters = pCnf->pMan->nAsserts; + for ( i = 0; i < nRegisters; i++ ) + { + pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); + assert( pCnf->pVarNums[pObjLo->Id] >= 0 ); + Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + assert( 0 ); + } + sat_solver_store_mark_roots( pSat ); + return pSat; +} + + +/**Function************************************************************* + Synopsis [Creates SAT solver for BMC.] Description [] @@ -123,7 +426,7 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames ) /**Function************************************************************* - Synopsis [Finds the set of clauses involved in the UNSAT core.] + Synopsis [Performs proof-based abstraction using BMC of the given depth.] Description [] @@ -132,37 +435,78 @@ sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose ) +Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore ) { - Vec_Int_t * vCore; - void * pSatCnf; - Intp_Man_t * pManProof; - int RetValue; - // solve the problem - RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); - if ( RetValue == l_Undef ) + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + Vec_Int_t * vFlops; + int * pVars, * pFlops; + int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses; + // count the number of CNF variables + nSatVars = 0; + Vec_PtrForEachEntry( vFrames, pCnf, f ) + nSatVars += pCnf->nVars; + // mark register variables + pVars = ALLOC( int, nSatVars ); + for ( i = 0; i < nSatVars; i++ ) + pVars[i] = -1; + Vec_PtrForEachEntry( vFrames, pCnf, f ) { - printf( "Conflict limit is reached.\n" ); - return NULL; + Aig_ManForEachPi( pCnf->pMan, pObj, i ) + { + assert( pCnf->pVarNums[pObj->Id] >= 0 ); + assert( pCnf->pVarNums[pObj->Id] < nSatVars ); + if ( pObj->pData == NULL ) + continue; + iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPiNum(p); + assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); + pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; + } + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + { + assert( pCnf->pVarNums[pObj->Id] >= 0 ); + assert( pCnf->pVarNums[pObj->Id] < nSatVars ); + if ( pObj->pData == NULL ) + continue; + iReg = Aig_ObjPioNum(pObj->pData) - Saig_ManPoNum(p); + assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); + pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; + } } - if ( RetValue == l_True ) + // mark used registers + pFlops = CALLOC( int, Aig_ManRegNum(p) ); + Vec_IntForEachEntry( vCore, iClause, i ) { - printf( "The BMC problem is SAT.\n" ); - return NULL; + nSatClauses = 0; + Vec_PtrForEachEntry( vFrames, pCnf, f ) + { + if ( iClause < nSatClauses + pCnf->nClauses ) + break; + nSatClauses += pCnf->nClauses; + } + if ( f == Vec_PtrSize(vFrames) ) + continue; + iClause = iClause - nSatClauses; + assert( iClause >= 0 ); + assert( iClause < pCnf->nClauses ); + // consider the clause + for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ ) + { + iReg = pVars[ lit_var(*piLit) ]; + if ( iReg >= 0 ) + pFlops[iReg] = 1; + } } - if ( fVerbose ) - printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts ); - assert( RetValue == l_False ); - pSatCnf = sat_solver_store_release( pSat ); - // derive the UNSAT core - pManProof = Intp_ManAlloc(); - vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose ); - Intp_ManFree( pManProof ); - Sto_ManFree( pSatCnf ); - return vCore; + // collect registers + vFlops = Vec_IntAlloc( Aig_ManRegNum(p) ); + for ( i = 0; i < Aig_ManRegNum(p); i++ ) + if ( pFlops[i] ) + Vec_IntPush( vFlops, i ); + free( pFlops ); + free( pVars ); + return vFlops; } - /**Function************************************************************* Synopsis [Performs proof-based abstraction using BMC of the given depth.] @@ -225,39 +569,139 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ) +void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames ) +{ + Cnf_Dat_t * pCnf; + int i; + Vec_PtrForEachEntry( vFrames, pCnf, i ) + { + Aig_ManStop( pCnf->pMan ); + Cnf_DataFree( pCnf ); + } + Vec_PtrFree( vFrames ); +} + +/**Function************************************************************* + + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) +{ + Vec_Ptr_t * vFlopPtrs, * vSupp; + Aig_Obj_t * pObj; + int i, Entry; + // collect latch inputs + vFlopPtrs = Vec_PtrAlloc( 1000 ); + Vec_IntForEachEntry( vFlops, Entry, i ) + { + Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) ); + pObj = Saig_ManLo(p, Entry); + pObj->fMarkA = 1; + } + // collect latch outputs + vSupp = Vec_PtrAlloc( 1000 ); + Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp ); + Vec_PtrFree( vFlopPtrs ); + // mark influencing flops + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->fMarkA = 1; + Vec_PtrFree( vSupp ); + // reload flops + Vec_IntClear( vFlops ); + Aig_ManForEachPi( p, pObj, i ) + { + if ( pObj->fMarkA == 0 ) + continue; + pObj->fMarkA = 0; + if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 ) + Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); + } +} + +/**Function************************************************************* + + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fVerbose ) { Aig_Man_t * pResult; Cnf_Dat_t * pCnf; + Vec_Ptr_t * vFrames; sat_solver * pSat; Vec_Int_t * vCore; Vec_Int_t * vFlops; - int clk = clock(); + int clk = clock(), clk2 = clock(); assert( Aig_ManRegNum(p) > 0 ); Aig_ManSetPioNumbers( p ); if ( fVerbose ) printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); - // create CNF for the AIG - pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); - // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + if ( fDynamic ) + { + // create CNF for the frames + vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose ); + // create dynamic solver + pSat = Saig_AbsCreateSolverDyn( p, vFrames ); + } + else + { + // create CNF for the AIG + pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); + // create SAT solver for the unrolled AIG + pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + } + if ( fVerbose ) + { + printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); + PRT( "Time", clock() - clk2 ); + } // compute UNSAT core vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); sat_solver_delete( pSat ); if ( vCore == NULL ) { - Cnf_DataFree( pCnf ); + Saig_AbsFreeCnfs( vFrames ); return NULL; } // collect registers - vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); - Cnf_DataFree( pCnf ); + if ( fDynamic ) + { + vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); + Saig_AbsFreeCnfs( vFrames ); + } + else + { + vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); + Cnf_DataFree( pCnf ); + } Vec_IntFree( vCore ); if ( fVerbose ) { - printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); + printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); PRT( "Time", clock() - clk ); } + // extend the abstraction + if ( fExtend ) + { + if ( fVerbose ) + printf( "Support extended from %d flops to", Vec_IntSize(vFlops) ); + Saig_AbsExtendOneStep( p, vFlops ); + if ( fVerbose ) + printf( " %d flops.\n", Vec_IntSize(vFlops) ); + } // create the resulting AIG pResult = Saig_ManAbstraction( p, vFlops ); Vec_IntFree( vFlops ); @@ -265,6 +709,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 2248fb37..a5235042 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -51,6 +51,7 @@ struct Saig_Bmc_t_ Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables // subproblems Vec_Ptr_t * vTargets; // targets to be solved in this interval + int iFramePrev; // previous frame int iFrameLast; // last frame int iOutputLast; // last output int iFrameFail; // failed frame @@ -251,6 +252,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) // int i; int nNodes = Aig_ManObjNum( p->pFrm ); Vec_PtrClear( p->vTargets ); + p->iFramePrev = p->iFrameLast; for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 ) { if ( p->iOutputLast == 0 ) @@ -573,7 +575,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->iOutputFail, p->iFrameFail ); else // if ( RetValue == l_False || RetValue == l_Undef ) - printf( "No output was asserted in %d frames. ", p->iFrameLast ); + printf( "No output was asserted in %d frames. ", p->iFramePrev-1 ); PRT( "Time", clock() - clk ); if ( RetValue != l_True ) { diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index cc71f371..84c8a4fe 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -635,7 +635,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames ) { Aig_Man_t * pFrames0, * pFrames1, * pMiter; - assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) ); +// assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) ); pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames ); pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames ); pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 ); @@ -790,9 +790,9 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ) { Aig_ManPrintStats( pPart0 ); Aig_ManPrintStats( pPart1 ); -// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); -// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); -// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); + Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); + Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); + printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); } RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose ); Aig_ManStop( pPart0 ); diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 4bb2356a..5d70812d 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -90,8 +90,6 @@ struct Ssw_Cex_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); /*=== sswBmc.c ==========================================================*/ extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ); /*=== sswCore.c ==========================================================*/ diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 3dfee28b..771fd530 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -482,75 +482,34 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Creates initial simulation classes.] + Synopsis [Takes the set of const1 cands and rehashes them using sim info.] - Description [Assumes that simulation info is assigned.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ) +int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) { -// int nFrames = 4; -// int nWords = 1; -// int nIters = 16; - -// int nFrames = 32; -// int nWords = 4; -// int nIters = 0; - - int nFrames = 4; - int nWords = 2; - int nIters = 16; - Ssw_Cla_t * p; - Ssw_Sml_t * pSml; + Aig_Man_t * pAig = p->pAig; Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; Aig_Obj_t * pObj, * pTemp, * pRepr; - int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2, RetValue; - int clk; - - // start the classes - p = Ssw_ClassesStart( pAig ); - - // perform sequential simulation -clk = clock(); - pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); -if ( fVerbose ) -{ - printf( "Allocated %.2f Mb for simulation information.\n", - 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) ); - printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords ); - PRT( "Time", clock() - clk ); -} - - // set comparison procedures -clk = clock(); - Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2; // allocate the hash table hashing simulation info into nodes - nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); + nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 ); ppTable = CALLOC( Aig_Obj_t *, nTableSize ); ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); - // add all the nodes to the hash table + // sort through the candidates nEntries = 0; - Aig_ManForEachObj( p->pAig, pObj, i ) + p->nCands1 = 0; + Vec_PtrForEachEntry( vCands, pObj, i ) { - if ( fLatchCorr ) - { - if ( !Saig_ObjIsLo(p->pAig, pObj) ) - continue; - } - else - { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) - continue; - // skip the node with more that the given number of levels - if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) - continue; - } + assert( p->pClassSizes[pObj->Id] == 0 ); + Aig_ObjSetRepr( p->pAig, pObj, NULL ); // check if the node belongs to the class of constant 1 if ( p->pFuncNodeIsConst( p->pManData, pObj ) ) { @@ -562,7 +521,9 @@ clk = clock(); iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize; // add the node to the class if ( ppTable[iEntry] == NULL ) + { ppTable[iEntry] = pObj; + } else { // set the representative of this node @@ -581,24 +542,18 @@ clk = clock(); nEntries++; } } - - // allocate room for classes - p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 ); - p->pMemClassesFree = p->pMemClasses + nEntries; // copy the entries into storage in the topological order nEntries2 = 0; - Aig_ManForEachObj( p->pAig, pObj, i ) + Vec_PtrForEachEntry( vCands, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) - continue; nNodes = p->pClassSizes[pObj->Id]; // skip the nodes that are not representatives of non-trivial classes if ( nNodes == 0 ) continue; assert( nNodes > 1 ); // add the nodes to the class in the topological order - ppClassNew = p->pMemClasses + nEntries2; + ppClassNew = p->pMemClassesFree + nEntries2; ppClassNew[0] = pObj; for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp; pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ ) @@ -611,12 +566,88 @@ clk = clock(); // increment the number of entries nEntries2 += nNodes; } + p->pMemClassesFree += nEntries2; assert( nEntries == nEntries2 ); free( ppTable ); free( ppNexts ); + // now it is time to refine the classes + return Ssw_ClassesRefine( p, 1 ); +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ) +{ +// int nFrames = 4; +// int nWords = 1; +// int nIters = 16; + +// int nFrames = 32; +// int nWords = 4; +// int nIters = 0; + + int nFrames = 4; + int nWords = 2; + int nIters = 16; + Ssw_Cla_t * p; + Ssw_Sml_t * pSml; + Vec_Ptr_t * vCands; + Aig_Obj_t * pObj; + int i, k, RetValue, clk; + + // start the classes + p = Ssw_ClassesStart( pAig ); + + // perform sequential simulation +clk = clock(); + pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); +if ( fVerbose ) +{ + printf( "Allocated %.2f Mb to store simulation information.\n", + 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) ); + printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords ); + PRT( "Time", clock() - clk ); +} + + // set comparison procedures +clk = clock(); + Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + + // collect nodes to be considered as candidates + vCands = Vec_PtrAlloc( 1000 ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Saig_ObjIsLo(p->pAig, pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) + continue; + } + Vec_PtrPush( vCands, pObj ); + } + + // allocate room for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) ); + p->pMemClassesFree = p->pMemClasses; // now it is time to refine the classes - Ssw_ClassesRefine( p, 1 ); + Ssw_ClassesPrepareRehash( p, vCands ); if ( fVerbose ) { printf( "Collecting candidate equivalence classes. " ); @@ -625,27 +656,30 @@ PRT( "Time", clock() - clk ); clk = clock(); // perform iterative refinement using simulation - k = 0; for ( i = 1; i < nIters; i++ ) { + // collect const1 candidates + Vec_PtrClear( vCands ); + Aig_ManForEachObj( p->pAig, pObj, k ) + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + Vec_PtrPush( vCands, pObj ); + assert( Vec_PtrSize(vCands) == p->nCands1 ); + // perform new round of simulation Ssw_SmlResimulateSeq( pSml ); - // simulate internal nodes - Ssw_SmlSimulateOne( pSml ); // check equivalence classes - RetValue = Ssw_ClassesRefineConst1( p, 1 ); - RetValue += Ssw_ClassesRefine( p, 1 ); - k++; + RetValue = Ssw_ClassesPrepareRehash( p, vCands ); if ( RetValue == 0 ) break; } - Ssw_ClassesCheck( p ); Ssw_SmlStop( pSml ); + Vec_PtrFree( vCands ); if ( fVerbose ) { printf( "Simulation of %d frames with %d words (%2d rounds). ", - nFrames, nWords, k ); + nFrames, nWords, i-1 ); PRT( "Time", clock() - clk ); } + Ssw_ClassesCheck( p ); // Ssw_ClassesPrint( p, 0 ); return p; } @@ -848,7 +882,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi { Aig_Obj_t ** pClassOld, ** pClassNew; Aig_Obj_t * pObj, * pReprNew; - int i; + int i; // split the class Vec_PtrClear( p->vClassOld ); diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6db8cc3a..68c00a0e 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -150,7 +150,7 @@ clk = clock(); RetValue = Ssw_ManSweepLatch( p ); if ( p->pPars->fVerbose ) { - printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ", + printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); @@ -174,11 +174,13 @@ clk = clock(); else if ( p->pPars->fDynamic ) { printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); - printf( "R =%3d. ", p->nRecycles-nRecycles ); + printf( "R =%4d. ", p->nRecycles-nRecycles ); } - printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal ); + printf( "F =%5d. ", p->nSatFailsReal-nSatFailsReal ); PRT( "T", clock() - clk ); } +// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) +// p->pPars->nBTLimit = 10000; } nSatProof = p->nSatProof; nSatCallsSat = p->nSatCallsSat; diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 91f6e713..913f7518 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -61,6 +61,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // other p->vNewLos = Vec_PtrAlloc( 100 ); p->vNewPos = Vec_IntAlloc( 100 ); + +// p->pPars->fVerbose = 1; return p; } diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index ce6ca38c..836b75e3 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -187,6 +187,70 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right ) /**Function************************************************************* + Synopsis [Checks implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ) +{ + unsigned * pSimLi, * pSimLo, * pSimCand; + int k; + pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id ); + pSimLi = Ssw_ObjSim( p, pObjLi->Id ); + pSimLo = Ssw_ObjSim( p, pObjLo->Id ); + if ( !Aig_IsComplement(pCand) ) + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) ) + return 0; + } + else + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in the implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ) +{ + unsigned * pSimLi, * pSimLo, * pSimCand; + int k, Counter = 0; + pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id ); + pSimLi = Ssw_ObjSim( p, pObjLi->Id ); + pSimLo = Ssw_ObjSim( p, pObjLo->Id ); + if ( !Aig_IsComplement(pCand) ) + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k])); + } + else + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k])); + } + return Counter; +} + +/**Function************************************************************* + Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ac417d14..2ad8dc75 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37,6 +37,7 @@ #include "int.h" #include "dch.h" #include "ssw.h" +#include "cgt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -200,6 +201,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -470,6 +472,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 ); @@ -7941,7 +7944,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ - +/* pNtkRes = Abc_NtkDarTestNtk( pNtk ); if ( pNtkRes == NULL ) { @@ -7950,9 +7953,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ - -// Abc_NtkDarTest( pNtk ); + Abc_NtkDarTest( pNtk ); return 0; usage: @@ -14634,6 +14637,162 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Cgt_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtkRes, * pNtk, * pNtkCare; + int c; + + extern Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Cgt_SetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "LNDCVKvh" ) ) != EOF ) + { + switch ( c ) + { + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLevelMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLevelMax <= 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nCandMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nCandMax <= 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nOdcMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nOdcMax <= 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfMax <= 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nVarsMin = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nVarsMin <= 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFlopsMin = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFlopsMin <= 0 ) + goto usage; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( argc == globalUtilOptind + 1 ) + { + pNtkCare = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 ); + if ( pNtkCare == NULL ) + { + printf( "Reading care network has failed.\n" ); + return 1; + } + // modify the current network + pNtkRes = Abc_NtkDarClockGate( pNtk, pNtkCare, pPars ); + Abc_NtkDelete( pNtkCare ); + } + else if ( argc == globalUtilOptind ) + { + pNtkRes = Abc_NtkDarClockGate( pNtk, NULL, pPars ); + } + else + { + fprintf( pErr, "Wrong number of arguments.\n" ); + return 0; + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Clock gating has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: clockgate [-LNDCVK <num>] [-vh] <file>\n" ); + fprintf( pErr, "\t sequential clock gating with observability don't-cares\n" ); + fprintf( pErr, "\t-L num : max level number of a clock gate [default = %d]\n", pPars->nLevelMax ); + fprintf( pErr, "\t-N num : max number of candidates for a flop [default = %d]\n", pPars->nCandMax ); + fprintf( pErr, "\t-D num : max number of ODC levels to consider [default = %d]\n", pPars->nOdcMax ); + fprintf( pErr, "\t-C num : max number of conflicts at a node [default = %d]\n", pPars->nConfMax ); + fprintf( pErr, "\t-V num : min number of vars to recycle SAT solver [default = %d]\n", pPars->nVarsMin ); + fprintf( pErr, "\t-K num : min number of flops to recycle SAT solver [default = %d]\n", pPars->nFlopsMin ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tfile : (optional) constraints for primary inputs and register outputs\n"); + return 1; +} /**Function************************************************************* @@ -16239,11 +16398,11 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 1000; + nFrames = 2000; nSizeMax = 200000; - nBTLimit = 10000; - nBTLimitAll = 10000000; - nNodeDelta = 1000; + nBTLimit = 2000; + nBTLimitAll = 2000000; + nNodeDelta = 2000; fRewrite = 0; fNewAlgo = 0; fVerbose = 0; @@ -16896,9 +17055,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int nFramesMax; int nConfMax; + int fDynamic; + int fExtend; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -16907,9 +17068,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFramesMax = 10; nConfMax = 10000; - fVerbose = 1; + fDynamic = 1; + fExtend = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF ) { switch ( c ) { @@ -16935,6 +17098,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfMax < 0 ) goto usage; break; + case 'd': + fDynamic ^= 1; + break; + case 'e': + fExtend ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -16961,7 +17130,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Target enlargement has failed.\n" ); @@ -16971,10 +17140,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: abs [-FC num] [-vh]\n" ); + fprintf( pErr, "usage: abs [-FC num] [-devh]\n" ); fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" ); fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); + fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); + fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "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; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 22f4b45c..dcc7f4c1 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -28,6 +28,7 @@ #include "int.h" #include "dch.h" #include "ssw.h" +#include "cgt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -2189,10 +2190,8 @@ PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose ) { - Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); - Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); @@ -2201,7 +2200,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf return NULL; Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fVerbose ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose ); Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; @@ -2563,6 +2562,44 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan1, * pMan2 = NULL, * pMan; + pMan1 = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan1 == NULL ) + return NULL; + if ( pCare ) + { + pMan2 = Abc_NtkToDar( pCare, 0, 0 ); + if ( pMan2 == NULL ) + { + Aig_ManStop( pMan1 ); + return NULL; + } + } + pMan = Cgt_ClockGating( pMan1, pMan2, pPars ); + Aig_ManStop( pMan1 ); + if ( pMan2 ) + Aig_ManStop( pMan2 ); + if ( pMan == NULL ) + return NULL; + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Performs phase abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose ) { Abc_Ntk_t * pNtkAig; @@ -2677,7 +2714,7 @@ Aig_ManPrintStats( pMan ); pTemp = Ssw_SignalCorrespondeceTestPairs( pMan ); Aig_ManStop( pTemp ); */ - Ssw_SecSpecialMiter( pMan, 0 ); + Ssw_SecSpecialMiter( pMan, 1 ); Aig_ManStop( pMan ); } @@ -2708,6 +2745,8 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) Aig_ManSetRegNum( pMan, pMan->nRegs ); pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan ); Aig_ManStop( pTemp ); + if ( pMan == NULL ) + return NULL; pNtkAig = Abc_NtkFromAigPhase( pMan ); pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); @@ -2715,8 +2754,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) Aig_ManStop( pMan ); return pNtkAig; */ - Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); - Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); @@ -2725,7 +2762,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) return NULL; Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 1 ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 1 ); Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index b03a00fa..becbfd6b 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -79,6 +79,10 @@ struct Abc_Frame_t_ void * pAbc8Nwk; // the current mapped network void * pAbc8Aig; // the current AIG void * pAbc8Lib; // the current LUT library + + // the addition to keep the best Ntl that can be used to restore + void * pAbc8NtlBestDelay; // the best delay, Ntl + void * pAbc8NtlBestArea; // the best area }; //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 59322cad..20521805 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -212,6 +212,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * pPinPerm[i] = pPinPerm[best_i]; pPinPerm[best_i] = temp; } +/* // verify assert( pPinPerm[0] < (int)pCut->nLeaves ); for ( i = 1; i < (int)pCut->nLeaves; i++ ) @@ -219,6 +220,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * assert( pPinPerm[i] < (int)pCut->nLeaves ); assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] ); } +*/ } /**Function************************************************************* diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h index 71c77321..3fdb7ffb 100644 --- a/src/misc/util/util_hack.h +++ b/src/misc/util/util_hack.h @@ -32,7 +32,9 @@ extern "C" { #include <time.h> #include <math.h> -#define EXTERN extern +#ifndef EXTERN +#define EXTERN extern +#endif #define NIL(type) ((type *) 0) #define random rand #define srandom srand diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 863be8bb..a00aaa68 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -336,13 +336,72 @@ static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin ) SeeAlso [] ***********************************************************************/ -static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry ) +static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Fill ) { int i; Vec_StrGrow( p, nSize ); p->nSize = nSize; for ( i = 0; i < p->nSize; i++ ) - p->pArray[i] = Entry; + p->pArray[i] = Fill; +} + +/**Function************************************************************* + + Synopsis [Fills the vector with given number of entries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_StrFillExtra( Vec_Str_t * p, int nSize, char Fill ) +{ + int i; + if ( p->nSize >= nSize ) + return; + if ( 2 * p->nSize > nSize ) + Vec_StrGrow( p, 2 * nSize ); + else + Vec_StrGrow( p, nSize ); + for ( i = p->nSize; i < nSize; i++ ) + p->pArray[i] = Fill; + p->nSize = nSize; +} + +/**Function************************************************************* + + Synopsis [Returns the entry even if the place not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline char Vec_StrGetEntry( Vec_Str_t * p, int i ) +{ + Vec_StrFillExtra( p, i + 1, 0 ); + return Vec_StrEntry( p, i ); +} + +/**Function************************************************************* + + Synopsis [Inserts the entry even if the place does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_StrSetEntry( Vec_Str_t * p, int i, char Entry ) +{ + Vec_StrFillExtra( p, i + 1, 0 ); + Vec_StrWriteEntry( p, i, Entry ); } /**Function************************************************************* diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 00ac60ca..7bb4bd6c 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -210,5 +210,13 @@ static void sat_solver_act_var_clear(sat_solver* s) s->activity[i] = 0.0; s->var_inc = 1.0; } +static void sat_solver_compress(sat_solver* s) +{ + if ( s->qtail != s->qhead ) + { + int RetValue = sat_solver_simplify(s); + assert( RetValue != 0 ); + } +} #endif |