diff options
33 files changed, 2092 insertions, 122 deletions
@@ -2959,6 +2959,10 @@ SOURCE=.\src\aig\aig\aigDup.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigFact.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigFanout.c # End Source File # Begin Source File diff --git a/src/aig/aig/aigFact.c b/src/aig/aig/aigFact.c new file mode 100644 index 00000000..7004618a --- /dev/null +++ b/src/aig/aig/aigFact.c @@ -0,0 +1,272 @@ +/**CFile**************************************************************** + + FileName [aigFactor.c] + + SystemName [] + + PackageName [] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [] + + Date [Ver. 1.0. Started - April 17, 2009.] + + Revision [$Id: aigFactor.c,v 1.00 2009/04/17 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detects multi-input AND gate rooted at this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFindImplications_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vImplics ) +{ + if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ) + { + Vec_PtrPushUnique( vImplics, pObj ); + return; + } + Aig_ManFindImplications_rec( Aig_ObjChild0(pObj), vImplics ); + Aig_ManFindImplications_rec( Aig_ObjChild1(pObj), vImplics ); +} + +/**Function************************************************************* + + Synopsis [Returns the nodes whose values are implied by pNode.] + + Description [Attention! Both pNode and results can be complemented! + Also important: Currently, this procedure only does backward propagation. + In general, it may find more implications if forward propagation is enabled.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManFindImplications( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + Vec_Ptr_t * vImplics; + vImplics = Vec_PtrAlloc( 100 ); + Aig_ManFindImplications_rec( pNode, vImplics ); + return vImplics; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cone of the node overlaps with the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManFindConeOverlap_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + if ( Aig_ObjIsTravIdPrevious( p, pNode ) ) + return 1; + if ( Aig_ObjIsTravIdCurrent( p, pNode ) ) + return 0; + Aig_ObjSetTravIdCurrent( p, pNode ); + if ( Aig_ObjIsPi(pNode) ) + return 0; + if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin0(pNode) ) ) + return 1; + if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin1(pNode) ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cone of the node overlaps with the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pTemp; + int i; + assert( !Aig_IsComplement(pNode) ); + assert( !Aig_ObjIsConst1(pNode) ); + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vImplics, pTemp, i ) + Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) ); + Aig_ManIncrementTravId( p ); + return Aig_ManFindConeOverlap_rec( p, pNode ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cone of the node overlaps with the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDeriveNewCone_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + if ( Aig_ObjIsTravIdCurrent( p, pNode ) ) + return pNode->pData; + Aig_ObjSetTravIdCurrent( p, pNode ); + if ( Aig_ObjIsPi(pNode) ) + return pNode->pData = pNode; + Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin0(pNode) ); + Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin1(pNode) ); + return pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cone of the node overlaps with the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDeriveNewCone( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pTemp; + int i; + assert( !Aig_IsComplement(pNode) ); + assert( !Aig_ObjIsConst1(pNode) ); + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vImplics, pTemp, i ) + { + Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) ); + Aig_Regular(pTemp)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pTemp) ); + } + return Aig_ManDeriveNewCone_rec( p, pNode ); +} + +/**Function************************************************************* + + Synopsis [Returns algebraic factoring of B in terms of A.] + + Description [Returns internal node C (an AND gate) that is equal to B + under assignment A = 'Value', or NULL if there is no such node C. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManFactorAlgebraic_int( Aig_Man_t * p, Aig_Obj_t * pPoA, Aig_Obj_t * pPoB, int Value ) +{ + Aig_Obj_t * pNodeA, * pNodeC; + Vec_Ptr_t * vImplics; + int RetValue; + if ( Aig_ObjIsConst1(Aig_ObjFanin0(pPoA)) || Aig_ObjIsConst1(Aig_ObjFanin0(pPoB)) ) + return NULL; + if ( Aig_ObjIsPi(Aig_ObjFanin0(pPoB)) ) + return NULL; + // get the internal node representing function of A under assignment A = 'Value' + pNodeA = Aig_ObjChild0( pPoA ); + pNodeA = Aig_NotCond( pNodeA, Value==0 ); + // find implications of this signal (nodes whose value is fixed under assignment A = 'Value') + vImplics = Aig_ManFindImplications( p, pNodeA ); + // check if the TFI cone of B overlaps with the implied nodes + RetValue = Aig_ManFindConeOverlap( p, vImplics, Aig_ObjFanin0(pPoB) ); + if ( RetValue == 0 ) // no overlap + { + Vec_PtrFree( vImplics ); + return NULL; + } + // there is overlap - derive node representing value of B under assignment A = 'Value' + pNodeC = Aig_ManDeriveNewCone( p, vImplics, Aig_ObjFanin0(pPoB) ); + pNodeC = Aig_NotCond( pNodeC, Aig_ObjFaninC0(pPoB) ); + Vec_PtrFree( vImplics ); + return pNodeC; +} + +/**Function************************************************************* + + Synopsis [Returns algebraic factoring of B in terms of A.] + + Description [Returns internal node C (an AND gate) that is equal to B + under assignment A = 'Value', or NULL if there is no such node C. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManFactorAlgebraic( Aig_Man_t * p, int iPoA, int iPoB, int Value ) +{ + assert( iPoA >= 0 && iPoA < Aig_ManPoNum(p) ); + assert( iPoB >= 0 && iPoB < Aig_ManPoNum(p) ); + assert( Value == 0 || Value == 1 ); + return Aig_ManFactorAlgebraic_int( p, Aig_ManPo(p, iPoA), Aig_ManPo(p, iPoB), Value ); +} + +/**Function************************************************************* + + Synopsis [Testing procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFactorAlgebraicTest( Aig_Man_t * p ) +{ + int iPoA = 0; + int iPoB = 1; + int Value = 0; + Aig_Obj_t * pRes; +// Aig_Obj_t * pObj; +// int i; + pRes = Aig_ManFactorAlgebraic( p, iPoA, iPoB, Value ); + Aig_ManShow( p, 0, NULL ); + Aig_ObjPrint( p, pRes ); + printf( "\n" ); +/* + printf( "Results:\n" ); + Aig_ManForEachObj( p, pObj, i ) + { + printf( "Object = %d.\n", i ); + Aig_ObjPrint( p, pObj ); + printf( "\n" ); + Aig_ObjPrint( p, pObj->pData ); + printf( "\n" ); + } +*/ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 8d243419..9034f272 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -313,6 +313,16 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj ) int fHaig = 0; int fShowFanouts = 0; Aig_Obj_t * pTemp; + if ( pObj == NULL ) + { + printf( "Object is NULL." ); + return; + } + if ( Aig_IsComplement(pObj) ) + { + printf( "Compl " ); + pObj = Aig_Not(pObj); + } assert( !Aig_IsComplement(pObj) ); printf( "Node %4d : ", Aig_ObjId(pObj) ); if ( Aig_ObjIsConst1(pObj) ) diff --git a/src/aig/bbl/bblif.h b/src/aig/bbl/bblif.h index db3eb2f5..89c58f93 100644 --- a/src/aig/bbl/bblif.h +++ b/src/aig/bbl/bblif.h @@ -36,6 +36,14 @@ (3) read a binary BLIF file with a mapped network produced by ABC (4) return the mapped network to the caller through a set of APIs + It should be noted that the BBLIF interface can be used to pass + the network from the calling application into ABC without writing it + into a file. In this case, ABC should be compiled as a library and + linked to the calling application. The BBLIF manager can be given + directly to the procedure Bbl_ManToAbc() to convert it into an AIG. + Similarly, the resulting mapped network can be converted into + BBLIF manager and passed back after the call to Bbl_ManFromAbc(). + Here these steps are described in more detail: (1) The BBLIF manager is allocated by calling Bbl_ManStart() and diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index 5cb8d345..8e14d2ef 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -122,6 +122,7 @@ struct Cec_ParCor_t_ int nWords; // the number of simulation words int nRounds; // the number of simulation rounds int nFrames; // the number of time frames + int nPrefix; // the number of time frames in the prefix int nBTLimit; // conflict limit at a node int fLatchCorr; // consider only latch outputs int fUseRings; // use rings diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 7ec3dad4..111cc8a8 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -236,6 +236,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) return RetValue; } +/**Function************************************************************* + + Synopsis [Implementation of new signal correspodence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) +{ + extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); + Gia_Man_t * pGia; + Cec_ParCor_t CorPars, * pCorPars = &CorPars; + Cec_ManCorSetDefaultParams( pCorPars ); + pCorPars->fUseCSat = fUseCSat; + pCorPars->nBTLimit = nConfs; + pGia = Gia_ManFromAigSimple( pAig ); + Cec_ManLSCorrespondenceClasses( pGia, pCorPars ); + Gia_ManReprToAigRepr( pAig, pGia ); + Gia_ManStop( pGia ); + return Aig_ManDupSimple( pAig ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index cd3ce7b9..fd723f30 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -712,6 +712,8 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) ); +// printf( "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) ); + if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 8e97e207..b4076916 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ); +static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -41,12 +41,12 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ SeeAlso [] ***********************************************************************/ -static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ) +static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) { if ( Gia_ObjIsAnd(pObj) ) { - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f ); - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f ); + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix ); + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix ); return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); } if ( f == 0 ) @@ -56,7 +56,7 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ } assert( f && Gia_ObjIsRo(p, pObj) ); pObj = Gia_ObjRoToRi( p, pObj ); - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 ); + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix ); return Gia_ObjFanin0CopyF( p, f-1, pObj ); } @@ -71,21 +71,21 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ SeeAlso [] ***********************************************************************/ -void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f ) +void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) { Gia_Obj_t * pRepr; int iLitNew; if ( ~Gia_ObjCopyF(p, f, pObj) ) return; - if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { - Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f ); + Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix ); iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); Gia_ObjSetCopyF( p, f, pObj, iLitNew ); return; } assert( Gia_ObjIsCand(pObj) ); - iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); + iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); Gia_ObjSetCopyF( p, f, pObj, iLitNew ); } @@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I { if ( Gia_ObjIsConst( p, i ) ) { - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); if ( iObjNew != 0 ) { @@ -148,8 +148,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I iPrev = i; Gia_ClassForEachObj1( p, i, iObj ) { - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) @@ -161,8 +161,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I iPrev = iObj; } iObj = i; - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames ); + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) @@ -181,8 +181,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) continue; - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames ); + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); if ( iPrevNew != iObjNew ) { @@ -216,18 +216,18 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) +Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pRepr; Vec_Int_t * vXorLits; int f, i, iPrevNew, iObjNew; - assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) ); + assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); assert( Gia_ManRegNum(p) > 0 ); assert( p->pReprs != NULL ); - p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); + p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) ); Gia_ManSetPhase( p ); - pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) @@ -235,7 +235,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V Gia_ManAppendCi(pNew); Gia_ObjSetCopyF( p, 0, pObj, 0 ); } - for ( f = 0; f < nFrames+fScorr; f++ ) + for ( f = 0; f < nFrames+nPrefix+fScorr; f++ ) { Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ManForEachPi( p, pObj, i ) @@ -243,15 +243,15 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V } *pvOutputs = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 ); - for ( f = 0; f < nFrames; f++ ) + for ( f = nPrefix; f < nFrames+nPrefix; f++ ) { Gia_ManForEachObj1( p, pObj, i ) { pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) continue; - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); if ( iPrevNew != iObjNew ) { @@ -752,6 +752,74 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte /**Function************************************************************* + Synopsis [Runs BMC for the equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs ) +{ + Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Vec_Str_t * vStatus; + Vec_Int_t * vOutputs; + Vec_Int_t * vCexStore; + Cec_ManSim_t * pSim; + Gia_Man_t * pSrm; + int fChanges, RetValue; + // prepare simulation manager + Cec_ManSimSetDefaultParams( pParsSim ); + pParsSim->nWords = pPars->nWords; + pParsSim->nRounds = pPars->nRounds; + pParsSim->fVerbose = pPars->fVerbose; + pParsSim->fLatchCorr = pPars->fLatchCorr; + pParsSim->fSeqSimulate = 1; + pSim = Cec_ManSimStart( pAig, pParsSim ); + // prepare SAT solving + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->nBTLimit = pPars->nBTLimit; + pParsSat->fVerbose = pPars->fVerbose; + fChanges = 1; + while ( fChanges ) + { + int clkBmc = clock(); + fChanges = 0; + pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( Gia_ManPoNum(pSrm) == 0 ) + { + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + break; + } + pParsSat->nBTLimit *= 10; + if ( pPars->fUseCSat ) + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + else + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + // refine classes with these counter-examples + if ( Vec_IntSize(vCexStore) ) + { + RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs ); + Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + fChanges = 1; + } + if ( pPars->fVerbose ) + Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); + // recycle + Vec_IntFree( vCexStore ); + Vec_StrFree( vStatus ); + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + } + Cec_ManSimStop( pSim ); +} + +/**Function************************************************************* + Synopsis [Internal procedure for register correspondence.] Description [] @@ -775,8 +843,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) int r, RetValue, clkTotal = clock(); int clkSat = 0, clkSim = 0, clkSrm = 0; int clk2, clk = clock(); - ABC_FREE( pAig->pReprs ); - ABC_FREE( pAig->pNexts ); if ( Gia_ManRegNum(pAig) == 0 ) { printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); @@ -792,8 +858,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pParsSim->fSeqSimulate = 1; // create equivalence classes of registers pSim = Cec_ManSimStart( pAig, pParsSim ); - Cec_ManSimClassesPrepare( pSim ); - Cec_ManSimClassesRefine( pSim ); + if ( pAig->pReprs == NULL ) + { + Cec_ManSimClassesPrepare( pSim ); + Cec_ManSimClassesRefine( pSim ); + } // prepare SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; @@ -805,6 +874,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); } + // check the base case + if ( !pPars->fLatchCorr || pPars->nFrames > 1 ) + Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) { @@ -848,49 +920,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); } - // check the base case - if ( !pPars->fLatchCorr || pPars->nFrames > 1 ) - { - int fChanges = 1; - while ( fChanges ) - { - int clkBmc = clock(); - fChanges = 0; - pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); - if ( Gia_ManPoNum(pSrm) == 0 ) - { - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - break; - } - pParsSat->nBTLimit *= 10; - if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - // refine classes with these counter-examples - if ( Vec_IntSize(vCexStore) ) - { - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - fChanges = 1; - } - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); - // recycle - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - } - } - else - { - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); - } + if ( pPars->fVerbose ) + Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); // check the overflow if ( r == nIterMax ) printf( "The refinement was not finished. The result may be incorrect.\n" ); @@ -910,6 +941,51 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) /**Function************************************************************* + Synopsis [Computes new initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) +{ + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + unsigned * pInitState; + int i, f; + Gia_ManRandom( 1 ); +// printf( "Simulating %d timeframes.\n", nFrames ); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark1 = 0; + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManConst0(pAig)->fMark1 = 0; + Gia_ManForEachPi( pAig, pObj, i ) + pObj->fMark1 = Gia_ManRandom(0) & 1; + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachRi( pAig, pObj, i ) + pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i ) + pObjRo->fMark1 = pObjRi->fMark1; + } + pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) ); + Gia_ManForEachRo( pAig, pObj, i ) + { + if ( pObj->fMark1 ) + Gia_InfoSetBit( pInitState, i ); +// printf( "%d", pObj->fMark1 ); + } +// printf( "\n" ); + Gia_ManCleanMark1( pAig ); + return pInitState; +} + +/**Function************************************************************* + Synopsis [Top-level procedure for register correspondence.] Description [] @@ -922,8 +998,39 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { Gia_Man_t * pNew, * pTemp; + unsigned * pInitState; int RetValue; - RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); + ABC_FREE( pAig->pReprs ); + ABC_FREE( pAig->pNexts ); + if ( pPars->nPrefix == 0 ) + RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); + else + { + // compute the cycles AIG + pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix ); + pTemp = Gia_ManDupFlip( pAig, pInitState ); + ABC_FREE( pInitState ); + // compute classes of this AIG + RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars ); + // transfer the class info + pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL; + pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL; + // perform additional BMC + pPars->fUseCSat = 0; + pPars->nBTLimit = ABC_MAX( pPars->nBTLimit, 1000 ); + Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix ); +/* + // transfer the class info back + pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL; + pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL; + // continue refining + RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars ); + // transfer the class info + pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL; + pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL; +*/ + Gia_ManStop( pTemp ); + } // derive reduced AIG if ( pPars->fMakeChoices ) { @@ -932,7 +1039,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) } else { - Gia_ManEquivImprove( pAig ); +// Gia_ManEquivImprove( pAig ); pNew = Gia_ManCorrReduce( pAig ); pNew = Gia_ManSeqCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); @@ -947,6 +1054,8 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); } + if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) ) + printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix ); return pNew; } diff --git a/src/aig/cec/cecCorr_updated.c b/src/aig/cec/cecCorr_updated.c new file mode 100644 index 00000000..dbe81d81 --- /dev/null +++ b/src/aig/cec/cecCorr_updated.c @@ -0,0 +1,1022 @@ +/**CFile**************************************************************** + + FileName [cecCorr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Latch/signal correspondence computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the real value of the literal w/o spec reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) +{ + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix ); + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix ); + return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); + } + if ( f == 0 ) + { + assert( Gia_ObjIsRo(p, pObj) ); + return Gia_ObjCopyF(p, f, pObj); + } + assert( f && Gia_ObjIsRo(p, pObj) ); + pObj = Gia_ObjRoToRi( p, pObj ); + Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix ); + return Gia_ObjFanin0CopyF( p, f-1, pObj ); +} + +/**Function************************************************************* + + Synopsis [Recursively performs speculative reduction for the object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) +{ + Gia_Obj_t * pRepr; + int iLitNew; + if ( ~Gia_ObjCopyF(p, f, pObj) ) + return; + if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + { + Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix ); + iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + Gia_ObjSetCopyF( p, f, pObj, iLitNew ); + return; + } + assert( Gia_ObjIsCand(pObj) ); + iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); + Gia_ObjSetCopyF( p, f, pObj, iLitNew ); +} + +/**Function************************************************************* + + Synopsis [Derives SRM for signal correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrev, iObj, iPrevNew, iObjNew; + assert( nFrames > 0 ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) ); + Gia_ManForEachRo( p, pObj, i ) + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) ); + for ( f = 0; f < nFrames+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + if ( fRings ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsConst( p, i ) ) + { + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); + if ( iObjNew != 0 ) + { + Vec_IntPush( *pvOutputs, 0 ); + Vec_IntPush( *pvOutputs, i ); + Vec_IntPush( vXorLits, iObjNew ); + } + } + else if ( Gia_ObjIsHead( p, i ) ) + { + iPrev = i; + Gia_ClassForEachObj1( p, i, iObj ) + { + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) + { + Vec_IntPush( *pvOutputs, iPrev ); + Vec_IntPush( *pvOutputs, iObj ); + Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); + } + iPrev = iObj; + } + iObj = i; + iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); + iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); + if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) + { + Vec_IntPush( *pvOutputs, iPrev ); + Vec_IntPush( *pvOutputs, iObj ); + Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); + } + } + } + } + else + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + ABC_FREE( p->pCopies ); +//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); +//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Derives SRM for signal correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrevNew, iObjNew; + assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + { + Gia_ManAppendCi(pNew); + Gia_ObjSetCopyF( p, 0, pObj, 0 ); + } + for ( f = 0; f < nFrames+nPrefix+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + for ( f = nPrefix; f < nFrames+nPrefix; f++ ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + ABC_FREE( p->pCopies ); +//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); +//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState ) +{ + unsigned * pInfo; + int k, w, nWords; + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + assert( nFlops <= Vec_PtrSize(vInfo) ); + for ( k = 0; k < nFlops; k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + if ( pInitState && Gia_InfoHasBit(pInitState, k) ) + { + for ( w = 0; w < nWords; w++ ) + pInfo[w] = ~0; +// pInfo[0] <<= 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + pInfo[w] = 0; + } + } + for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Gia_ManRandom( 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Remaps simulation info from SRM to the original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo ) +{ + Gia_Obj_t * pObj, * pRepr; + unsigned * pInfoObj, * pInfoRepr; + int i, w, nWords; + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + Gia_ManForEachRo( p, pObj, i ) + { + // skip ROs without representatives + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) + continue; + pInfoObj = Vec_PtrEntry( vInfo, i ); + for ( w = 0; w < nWords; w++ ) + assert( pInfoObj[w] == 0 ); + // skip ROs with constant representatives + if ( Gia_ObjIsConst0(pRepr) ) + continue; + assert( Gia_ObjIsRo(p, pRepr) ); +// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) ); + // transfer info from the representative + pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); + for ( w = 0; w < nWords; w++ ) + pInfoObj[w] = pInfoRepr[w]; + } +// printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Collects information about remapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ) +{ + Vec_Int_t * vPairs; + Gia_Obj_t * pObj, * pRepr; + int i; + vPairs = Vec_IntAlloc( 100 ); + Gia_ManForEachRo( p, pObj, i ) + { + // skip ROs without representatives + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) +// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) ) + continue; + assert( Gia_ObjIsRo(p, pRepr) ); +// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); + // remember the pair + Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); + Vec_IntPush( vPairs, i ); + } + return vPairs; +} + +/**Function************************************************************* + + Synopsis [Remaps simulation info from SRM to the original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState ) +{ + unsigned * pInfoObj, * pInfoRepr; + int w, i, iObj, iRepr, nWords; + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + Vec_IntForEachEntry( vPairs, iRepr, i ) + { + iObj = Vec_IntEntry( vPairs, ++i ); + pInfoObj = Vec_PtrEntry( vInfo, iObj ); + pInfoRepr = Vec_PtrEntry( vInfo, iRepr ); + for ( w = 0; w < nWords; w++ ) + { + assert( pInitState || pInfoObj[w] == 0 ); + pInfoObj[w] = pInfoRepr[w]; + } + } +} + +/**Function************************************************************* + + Synopsis [Packs one counter-examples into the array of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +*************************************`**********************************/ +int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits ) +{ + unsigned * pInfo, * pPres; + int i; + for ( i = 0; i < nLits; i++ ) + { + pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + return 0; + } + for ( i = 0; i < nLits; i++ ) + { + pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_InfoXorBit( pInfo, iBit ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs bitpacking of counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) +{ + Vec_Int_t * vPat; + Vec_Ptr_t * vPres; + int nWords = Vec_PtrReadWordsSimInfo(vInfo); + int nBits = 32 * nWords; + int k, nSize, iBit = 1, kMax = 0; + vPat = Vec_IntAlloc( 100 ); + vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords ); + Vec_PtrCleanSimInfo( vPres, 0, nWords ); + while ( iStart < Vec_IntSize(vCexStore) ) + { + // skip the output number + iStart++; + // get the number of items + nSize = Vec_IntEntry( vCexStore, iStart++ ); + if ( nSize <= 0 ) + continue; + // extract pattern + Vec_IntClear( vPat ); + for ( k = 0; k < nSize; k++ ) + Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); + // add pattern to storage + for ( k = 1; k < nBits; k++ ) + if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) + break; + kMax = ABC_MAX( kMax, k ); + if ( k == nBits-1 ) + break; + } + Vec_PtrFree( vPres ); + Vec_IntFree( vPat ); + return iStart; +} + +/**Function************************************************************* + + Synopsis [Performs bitpacking of counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) +{ + unsigned * pInfo; + int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo); + int k, iLit, nLits, Out, iBit = 1; + while ( iStart < Vec_IntSize(vCexStore) ) + { + // skip the output number +// iStart++; + Out = Vec_IntEntry( vCexStore, iStart++ ); +// printf( "iBit = %d. Out = %d.\n", iBit, Out ); + // get the number of items + nLits = Vec_IntEntry( vCexStore, iStart++ ); + if ( nLits <= 0 ) + continue; + // add pattern to storage + for ( k = 0; k < nLits; k++ ) + { + iLit = Vec_IntEntry( vCexStore, iStart++ ); + pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) + Gia_InfoXorBit( pInfo, iBit ); + } + if ( ++iBit == nBits ) + break; + } +// printf( "added %d bits\n", iBit-1 ); + return iStart; +} + +/**Function************************************************************* + + Synopsis [Resimulates counter-examples derived by the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState ) +{ + Vec_Int_t * vPairs; + Vec_Ptr_t * vSimInfo; + int RetValue = 0, iStart = 0; + vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); + Gia_ManSetRefs( pSim->pAig ); +// pSim->pPars->nWords = 63; + pSim->pPars->nRounds = nFrames; + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); + while ( iStart < Vec_IntSize(vCexStore) ) + { + Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState ); + iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); +// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); +// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); + Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState ); + RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); +// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL ); + } +//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); + assert( iStart == Vec_IntSize(vCexStore) ); + Vec_PtrFree( vSimInfo ); + Vec_IntFree( vPairs ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates counter-examples derived by the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ) +{ + Vec_Ptr_t * vSimInfo; + int RetValue = 0, iStart = 0; + Gia_ManSetRefs( pSim->pAig ); + pSim->pPars->nRounds = 1; + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); + while ( iStart < Vec_IntSize(vCexStore) ) + { + Cec_ManStartSimInfo( vSimInfo, 0, NULL ); + iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); + RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); + } + assert( iStart == Vec_IntSize(vCexStore) ); + Vec_PtrFree( vSimInfo ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Updates equivalence classes by marking those that timed out.] + + Description [Returns 1 if all ndoes are proved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings ) +{ + int i, status, iRepr, iObj; + int Counter = 0; + assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) ); + Vec_StrForEachEntry( vStatus, status, i ) + { + iRepr = Vec_IntEntry( vOutputs, 2*i ); + iObj = Vec_IntEntry( vOutputs, 2*i+1 ); + if ( status == 1 ) + continue; + if ( status == 0 ) + { + if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) + Counter++; +// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) +// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); +// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) +// Cec_ManSimClassRemoveOne( pSim, iObj ); + continue; + } + if ( status == -1 ) + { +// if ( !Gia_ObjFailed( p, iObj ) ) +// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); +// Gia_ObjSetFailed( p, iRepr ); +// Gia_ObjSetFailed( p, iObj ); +// if ( fRings ) +// Cec_ManSimClassRemoveOne( pSim, iRepr ); + Cec_ManSimClassRemoveOne( pSim, iObj ); + continue; + } + } +// if ( Counter ) +// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pRepr; + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + { + Gia_ManCorrReduce_rec( pNew, p, pRepr ); + pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return; + } + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Reduces AIG using equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Prints statistics during solving.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ) +{ + int nLits, CounterX = 0, Counter0 = 0, Counter = 0; + int i, Entry, nProve = 0, nDispr = 0, nFail = 0; + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + { + if ( Gia_ObjIsNone(p, i) ) + CounterX++; + else if ( Gia_ObjIsConst(p, i) ) + Counter0++; + else if ( Gia_ObjIsHead(p, i) ) + Counter++; + } + CounterX -= Gia_ManCoNum(p); + nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; + if ( iIter == -1 ) + printf( "BMC : " ); + else + printf( "%3d : ", iIter ); + printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); + if ( vStatus ) + Vec_StrForEachEntry( vStatus, Entry, i ) + { + if ( Entry == 1 ) + nProve++; + else if ( Entry == 0 ) + nDispr++; + else if ( Entry == -1 ) + nFail++; + } + printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); + ABC_PRT( "T", Time ); +} + +/**Function************************************************************* + + Synopsis [Computes new initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) +{ + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + unsigned * pInitState; + int i, f; + printf( "Simulating %d timeframes.\n", nFrames ); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark1 = 0; + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManConst0(pAig)->fMark1 = 0; + Gia_ManForEachPi( pAig, pObj, i ) + pObj->fMark1 = Gia_ManRandom(0) & 1; +// pObj->fMark1 = 1; + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachRi( pAig, pObj, i ) + pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i ) + pObjRo->fMark1 = pObjRi->fMark1; + } + pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) ); + Gia_ManForEachRo( pAig, pObj, i ) + { + if ( pObj->fMark1 ) + Gia_InfoSetBit( pInitState, i ); +// printf( "%d", pObj->fMark1 ); + } +// printf( "\n" ); + Gia_ManCleanMark1( pAig ); + return pInitState; +} + +/**Function************************************************************* + + Synopsis [Internal procedure for register correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) +{ + int nIterMax = 100000; + int nAddFrames = 1; // additional timeframes to simulate + Vec_Str_t * vStatus; + Vec_Int_t * vOutputs; + Vec_Int_t * vCexStore; + Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Cec_ManSim_t * pSim; + Gia_Man_t * pSrm; + unsigned * pInitState = NULL; + int r, RetValue, clkTotal = clock(); + int clkSat = 0, clkSim = 0, clkSrm = 0; + int clk2, clk = clock(); + ABC_FREE( pAig->pReprs ); + ABC_FREE( pAig->pNexts ); + if ( Gia_ManRegNum(pAig) == 0 ) + { + printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); + return 0; + } + Gia_ManRandom( 1 ); + // derive initial state for resimulation + if ( pPars->nPrefix ) +// pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) ); + pInitState = Cec_ManComputeInitState( pAig, 100 ); + // prepare simulation manager + Cec_ManSimSetDefaultParams( pParsSim ); + pParsSim->nWords = pPars->nWords; + pParsSim->nRounds = pPars->nRounds; + pParsSim->fVerbose = pPars->fVerbose; + pParsSim->fLatchCorr = pPars->fLatchCorr; + pParsSim->fSeqSimulate = 1; + // create equivalence classes of registers + pSim = Cec_ManSimStart( pAig, pParsSim, pInitState ); + Cec_ManSimClassesPrepare( pSim ); + Cec_ManSimClassesRefine( pSim ); + // prepare SAT solving + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->nBTLimit = pPars->nBTLimit; + pParsSat->fVerbose = pPars->fVerbose; + if ( pPars->fVerbose ) + { + printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", + Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), + pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); + Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); + } + // perform refinement of equivalence classes + for ( r = 0; r < nIterMax; r++ ) + { + clk = clock(); + // perform speculative reduction + clk2 = clock(); + pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) ); + clkSrm += clock() - clk2; + if ( Gia_ManCoNum(pSrm) == 0 ) + { + Vec_IntFree( vOutputs ); + Gia_ManStop( pSrm ); + break; + } +//Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); + // found counter-examples to speculation + clk2 = clock(); + if ( pPars->fUseCSat ) + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + else + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + Gia_ManStop( pSrm ); + clkSat += clock() - clk2; + if ( Vec_IntSize(vCexStore) == 0 ) + { + Vec_IntFree( vCexStore ); + Vec_StrFree( vStatus ); + Vec_IntFree( vOutputs ); + break; + } + // refine classes with these counter-examples + clk2 = clock(); + RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState ); + Vec_IntFree( vCexStore ); + clkSim += clock() - clk2; + Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + if ( pPars->fVerbose ) + Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); + Vec_StrFree( vStatus ); + Vec_IntFree( vOutputs ); +//Gia_ManEquivPrintClasses( pAig, 1, 0 ); + } + ABC_FREE( pInitState ); + // check the base case + if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix ) + { + int fChanges = 1; + while ( fChanges ) + { + int clkBmc = clock(); + fChanges = 0; + pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( Gia_ManPoNum(pSrm) == 0 ) + { + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + break; + } + pParsSat->nBTLimit *= 10; + if ( pPars->nPrefix ) + { + pParsSat->nBTLimit = 10000; + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + } + else if ( pPars->fUseCSat ) + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + else + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + // refine classes with these counter-examples + if ( Vec_IntSize(vCexStore) ) + { + clk2 = clock(); + RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL ); + clkSim += clock() - clk2; + Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + fChanges = 1; + } + if ( pPars->fVerbose ) + Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); + // recycle + Vec_IntFree( vCexStore ); + Vec_StrFree( vStatus ); + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + } + } + else + { + if ( pPars->fVerbose ) + Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); + } + // check the overflow + if ( r == nIterMax ) + printf( "The refinement was not finished. The result may be incorrect.\n" ); + Cec_ManSimStop( pSim ); + clkTotal = clock() - clkTotal; + // report the results + if ( pPars->fVerbose ) + { + ABC_PRTP( "Srm ", clkSrm, clkTotal ); + ABC_PRTP( "Sat ", clkSat, clkTotal ); + ABC_PRTP( "Sim ", clkSim, clkTotal ); + ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); + ABC_PRT( "TOTAL", clkTotal ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Top-level procedure for register correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) +{ + Gia_Man_t * pNew, * pTemp; + int RetValue; + RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); + // derive reduced AIG + if ( pPars->fMakeChoices ) + { + pNew = Gia_ManEquivToChoices( pAig, 1 ); + Gia_ManHasChoices( pNew ); + } + else + { + Gia_ManEquivImprove( pAig ); + pNew = Gia_ManCorrReduce( pAig ); + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); + } + // report the results + if ( pPars->fVerbose ) + { + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), + 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), + Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), + 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); + } + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index 5f032b59..3a8d8588 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -823,13 +823,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St { if ( Gia_ObjFaninC0(pObj) ) { - printf( "Constant 1 output of SRM!!!\n" ); +// printf( "Constant 1 output of SRM!!!\n" ); Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example Vec_StrPush( vStatus, 0 ); } else { - printf( "Constant 0 output of SRM!!!\n" ); +// printf( "Constant 0 output of SRM!!!\n" ); Vec_StrPush( vStatus, 1 ); } continue; diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c index 1e1e4edb..7f7b1b4c 100644 --- a/src/aig/dar/darCut.c +++ b/src/aig/dar/darCut.c @@ -627,6 +627,7 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot ) { Aig_Obj_t * pObj; int i; + Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL ); Vec_PtrForEachEntry( p->vCutNodes, pObj, i ) if ( !Aig_ObjIsNone(pObj) ) Dar_ObjSetCuts( pObj, NULL ); @@ -653,7 +654,7 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ) Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0); Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1); Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut; - int i, k, RetValue; + int i, k, RetValue; assert( !Aig_IsComplement(pObj) ); assert( Aig_ObjIsNode(pObj) ); diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index 7b23aa33..7f9188e0 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -813,6 +813,12 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) pData->Level = Aig_Regular(pData->pFunc)->Level; // mark the node if it is part of MFFC pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc)); + // assign the probability + if ( p->pPars->fPower ) + { + float Prob = Aig_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) ); + pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob; + } } } } @@ -830,22 +836,30 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) ***********************************************************************/ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower ) { - float Power0, Power1; Dar_LibDat_t * pData; + float Power0, Power1; int Area; if ( pPower ) *pPower = (float)0.0; + pData = s_DarLib->pDatas + pObj->Num; + if ( pData->TravId == Out ) + return 0; + pData->TravId = Out; if ( pObj->fTerm ) + { + if ( pPower ) + *pPower = pData->dProb; return 0; + } assert( pObj->Num > 3 ); - pData = s_DarLib->pDatas + pObj->Num; if ( pData->Level > Required ) return 0xff; if ( pData->pFunc && !pData->fMffc ) + { + if ( pPower ) + *pPower = pData->dProb; return 0; - if ( pData->TravId == Out ) - return 0; - pData->TravId = Out; + } // this is a new node - get a bound on the area of its branches nNodesSaved--; Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1, pPower? &Power0 : NULL ); diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 2d633d5c..571a6ef8 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -513,6 +513,7 @@ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index a4f1ab44..4b3692e4 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -105,6 +105,46 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ) +{ + Gia_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + // create the new manager + pNew = Gia_ManStart( Aig_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsAnd(pObj) ) + pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) ); + else if ( Aig_ObjIsPi(pObj) ) + pObj->iData = Gia_ManAppendCi( pNew ); + else if ( Aig_ObjIsPo(pObj) ) + pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) ); + else if ( Aig_ObjIsConst1(pObj) ) + pObj->iData = 1; + else + assert( 0 ); + } + Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + if ( pNew->pNexts ) + Gia_ManDeriveReprs( pNew ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Handles choices as additional combinational outputs.] Description [] @@ -243,6 +283,43 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) return pMan; } + +/**Function************************************************************* + + Synopsis [Transfers representatives from pGia to pAig.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ) +{ + Aig_Obj_t * pObj; + Gia_Obj_t * pGiaObj, * pGiaRepr; + int i; + assert( p->pReprs == NULL ); + assert( pGia->pReprs != NULL ); + // move pointers from AIG to GIA + Aig_ManForEachObj( p, pObj, i ) + { + assert( i == 0 || !Gia_LitIsCompl(pObj->iData) ); + pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) ); + pGiaObj->Value = i; + } + // set the pointers to the nodes in AIG + Aig_ManReprStart( p, Aig_ManObjNumMax(p) ); + Gia_ManForEachObj( pGia, pGiaObj, i ) + { + pGiaRepr = Gia_ObjReprObj( pGia, i ); + if ( pGiaRepr == NULL ) + continue; + Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) ); + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 0c0ee598..507e5143 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -47,8 +47,10 @@ /*=== giaAig.c =============================================================*/ extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); +extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); +extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ); #ifdef __cplusplus } diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index f53a3d33..e005dfc2 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -473,6 +473,8 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) Vec_IntShrink( p->vLevReas, 3*iBound ); } +int s_Counter = 0; + /**Function************************************************************* Synopsis [Assigns the variables a value.] @@ -498,6 +500,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 ); Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 ); assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail ); + s_Counter++; } @@ -925,6 +928,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) { int RetValue = 0; + s_Counter = 0; assert( !p->pProp.iHead && !p->pProp.iTail ); assert( !p->pJust.iHead && !p->pJust.iTail ); assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 ); @@ -941,6 +945,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Cbs_ManCheckLimits( p ) ) RetValue = -1; + +// printf( "%d ", s_Counter ); return RetValue; } @@ -1019,7 +1025,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt { if ( Gia_ObjFaninC0(pRoot) ) { - printf( "Constant 1 output of SRM!!!\n" ); +// printf( "Constant 1 output of SRM!!!\n" ); Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example Vec_StrPush( vStatus, 0 ); } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 63748403..cde19a22 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -246,6 +246,47 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while complementing the flops.] + + Description [The array of initial state contains the init state + for each state bit of the flops in the design.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) ) + pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + pObj->Value = Gia_ObjFanin0Copy(pObj); + if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) ) + pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) ); + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + } + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} /**Function************************************************************* diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 0a44d2dc..c8d38331 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -162,9 +162,10 @@ struct Ntl_Net_t_ int iTemp; // other data }; Ntl_Obj_t * pDriver; // driver of the net - int NetId; // unique ID of the net - char nVisits; // the number of times the net is visited - char fMark; // temporary mark + unsigned NetId : 28; // unique ID of the net + unsigned nVisits : 2; // the number of times the net is visted + unsigned fMark : 1; // temporary mark + unsigned fFixed : 1; // the fixed net char pName[0]; // the name of this net }; @@ -392,6 +393,7 @@ extern ABC_DLL int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ); extern ABC_DLL int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ); extern ABC_DLL int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); extern ABC_DLL void Ntl_ModelClearNets( Ntl_Mod_t * pModel ); +extern ABC_DLL void Ntl_ManRemoveUselessNets( Ntl_Man_t * p ); #ifdef __cplusplus } diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 405ec83f..70f97d89 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -422,6 +422,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe // collapse the AIG pAig = Ntl_ManExtract( p ); +//Ntl_ManPrintStats( p ); +//Aig_ManPrintStats( pAig ); pNew = Ntl_ManInsertAig( p, pAig ); pAigCol = Ntl_ManCollapseSeq( pNew, 0 ); if ( pAigCol == NULL ) @@ -429,6 +431,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe Aig_ManStop( pAig ); return pNew; } +//Ntl_ManPrintStats( pNew ); +//Aig_ManPrintStats( pAigCol ); // perform SCL for the given design pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 21f2d246..eb967bdc 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -245,6 +245,42 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) /**Function************************************************************* + Synopsis [Find drivers of the given net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pNode; + Ntl_Net_t * pNet, * pNetThis; + int i, k; + pRoot = Ntl_ManRootModel( p ); + pNetThis = Ntl_ModelFindNet( pRoot, pName ); + printf( "\n*** Net %d \"%s\":\n", pNetThis->NetId, pName ); + // mark from the nodes + Ntl_ModelForEachPo( pRoot, pNode, i ) + if ( pNetThis == Ntl_ObjFanin0(pNode) ) + printf( "driven by PO %d\n", i ); + Ntl_ModelForEachNode( pRoot, pNode, i ) + Ntl_ObjForEachFanin( pNode, pNet, k ) + if ( pNetThis == pNet ) + printf( "driven by node %d with %d fanins and %d fanouts\n (%s)\n", + pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName ); + Ntl_ModelForEachBox( pRoot, pNode, i ) + Ntl_ObjForEachFanin( pNode, pNet, k ) + if ( pNetThis == pNet ) + printf( "driven by box %d with %d fanins and %d fanouts\n (%s)\n", + pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName ); +} + +/**Function************************************************************* + Synopsis [Inserts the given mapping into the netlist.] Description [] diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index 552d5c15..4c9bb311 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -460,6 +460,8 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) } else pNet->pCopy = NULL; + if ( pNet->pCopy ) + ((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed; } Ntl_ModelForEachObj( pModelOld, pObj, i ) { @@ -511,6 +513,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_ModelForEachNet( pModelOld, pNet, i ) { pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); + ((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed; if ( pNet->pDriver == NULL ) { assert( !pModelOld->attrWhite ); diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 9c3d4e42..6d1b6c83 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -657,6 +657,68 @@ void Ntl_ModelClearNets( Ntl_Mod_t * pModel ) } } +/**Function************************************************************* + + Synopsis [Removes nets without fanins and fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManRemoveUselessNets( Ntl_Man_t * p ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pNode; + Ntl_Net_t * pNet; + int i, k, Counter; + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachNet( pRoot, pNet, i ) + pNet->fMark = 0; + Ntl_ModelForEachPi( pRoot, pNode, i ) + { + pNet = Ntl_ObjFanout0(pNode); + pNet->fMark = 1; + } + Ntl_ModelForEachPo( pRoot, pNode, i ) + { + pNet = Ntl_ObjFanin0(pNode); + pNet->fMark = 1; + } + Ntl_ModelForEachNode( pRoot, pNode, i ) + { + Ntl_ObjForEachFanin( pNode, pNet, k ) + pNet->fMark = 1; + Ntl_ObjForEachFanout( pNode, pNet, k ) + pNet->fMark = 1; + } + Ntl_ModelForEachBox( pRoot, pNode, i ) + { + Ntl_ObjForEachFanin( pNode, pNet, k ) + pNet->fMark = 1; + Ntl_ObjForEachFanout( pNode, pNet, k ) + pNet->fMark = 1; + } + Counter = 0; + Ntl_ModelForEachNet( pRoot, pNet, i ) + { + if ( pNet->fMark ) + { + pNet->fMark = 0; + continue; + } + if ( pNet->fFixed ) + continue; + Ntl_ModelDeleteNet( pRoot, pNet ); + Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL ); + Counter++; + } + if ( Counter ) + printf( "Deleted %d nets without fanins/fanouts.\n", Counter ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index 10b7b462..12a72e2f 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -518,9 +518,21 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) Vec_Int_t * vTruth; Nwk_Obj_t * pObj; int i, Counter = 0; + Nwk_Obj_t * pNodeThis = pNtk->vObjs->pArray[72688]; + vTruth = Vec_IntAlloc( 1 << 16 ); Nwk_ManForEachNode( pNtk, pObj, i ) + { + if ( i == 641386 ) + { + int x = 0; + } Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose ); + if ( pNodeThis->nFanouts != 15 ) + { + int s = 0; + } + } if ( fVerbose && Counter ) printf( "Support minimization reduced support of %d nodes.\n", Counter ); Vec_IntFree( vTruth ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 5ddef829..c7109e26 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); 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 a2a915f7..f6845acd 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -869,9 +869,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Aig_ManPrintStats( pResult ); else printf( " -----------------------------------------------------\n" ); + if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) + { + printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio ); + break; + } } } - Vec_IntFree( vFlops ); return pResult; } diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index adb98401..c2a33ee4 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -61,6 +61,8 @@ struct Ssw_Pars_t_ int fLocalSim; // enable local simulation simulation int fPartSigCorr; // uses partial signal correspondence int nIsleDist; // extends islands by the given distance + int fScorrGia; // new signal correspondence implementation + int fUseCSat; // new SAT solver using when fScorrGia is selected int fVerbose; // verbose stats int fFlopVerbose; // verbose printout of redundant flops // optimized latch correspondence diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 56b37fbe..41123ca4 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -277,6 +277,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) return Ssw_SignalCorrespondencePart( pAig, pPars ); } + + if ( pPars->fScorrGia ) + { + extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); + return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); + } + // start the induction manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 3e233d90..6973bb64 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1185,6 +1185,81 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches ) fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" ); } +/**Function************************************************************* + + Synopsis [Converts the network to sequential.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd ) +{ + Abc_Obj_t * pObjLi, * pObjLo, * pObj; + int i; + assert( Abc_NtkBoxNum(pNtk) == 0 ); + if ( !Abc_NtkIsComb(pNtk) ) + { + printf( "The network is a not a combinational one.\n" ); + return; + } + if ( nLatchesToAdd >= Abc_NtkPiNum(pNtk) ) + { + printf( "The number of latches is more or equal than the number of PIs.\n" ); + return; + } + if ( nLatchesToAdd >= Abc_NtkPoNum(pNtk) ) + { + printf( "The number of latches is more or equal than the number of POs.\n" ); + return; + } + + // move the last PIs to become CIs + Vec_PtrClear( pNtk->vPis ); + Abc_NtkForEachCi( pNtk, pObj, i ) + { + if ( i < Abc_NtkCiNum(pNtk) - nLatchesToAdd ) + { + Vec_PtrPush( pNtk->vPis, pObj ); + continue; + } + pObj->Type = ABC_OBJ_BO; + pNtk->nObjCounts[ABC_OBJ_PI]--; + pNtk->nObjCounts[ABC_OBJ_BO]++; + } + + // move the last POs to become COs + Vec_PtrClear( pNtk->vPos ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( i < Abc_NtkCoNum(pNtk) - nLatchesToAdd ) + { + Vec_PtrPush( pNtk->vPos, pObj ); + continue; + } + pObj->Type = ABC_OBJ_BI; + pNtk->nObjCounts[ABC_OBJ_PO]--; + pNtk->nObjCounts[ABC_OBJ_BI]++; + } + + // create latches + for ( i = 0; i < nLatchesToAdd; i++ ) + { + pObjLo = Abc_NtkCi( pNtk, Abc_NtkCiNum(pNtk) - nLatchesToAdd + i ); + pObjLi = Abc_NtkCo( pNtk, Abc_NtkCoNum(pNtk) - nLatchesToAdd + i ); + pObj = Abc_NtkCreateLatch( pNtk ); + Abc_ObjAddFanin( pObj, pObjLi ); + Abc_ObjAddFanin( pObjLo, pObj ); + Abc_LatchSetInit0( pObj ); + } + + if ( !Abc_NtkCheck( pNtk ) ) + fprintf( stdout, "Abc_NtkMakeSeq(): Network check has failed.\n" ); +} + /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6beaf144..f8815321 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -261,6 +261,7 @@ static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Insert ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -578,6 +579,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*merge", Abc_CommandAbc8Merge, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*insert", Abc_CommandAbc8Insert, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 ); @@ -5281,6 +5283,8 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; int fRemoveLatches; + int nLatchesToAdd; + extern void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5288,11 +5292,23 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fRemoveLatches = 0; + nLatchesToAdd = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Llh" ) ) != EOF ) { switch ( c ) { + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nLatchesToAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLatchesToAdd < 0 ) + goto usage; + break; case 'l': fRemoveLatches ^= 1; break; @@ -5308,7 +5324,12 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - if ( Abc_NtkIsComb(pNtk) ) + if ( Abc_NtkIsComb(pNtk) && nLatchesToAdd == 0 ) + { + fprintf( pErr, "The network is already combinational.\n" ); + return 0; + } + if ( !Abc_NtkIsComb(pNtk) && nLatchesToAdd != 0 ) { fprintf( pErr, "The network is already combinational.\n" ); return 0; @@ -5316,15 +5337,19 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network pNtkRes = Abc_NtkDup( pNtk ); - Abc_NtkMakeComb( pNtkRes, fRemoveLatches ); + if ( nLatchesToAdd ) + Abc_NtkMakeSeq( pNtkRes, nLatchesToAdd ); + else + Abc_NtkMakeComb( pNtkRes, fRemoveLatches ); // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: comb [-lh]\n" ); - fprintf( pErr, "\t makes the current network combinational by replacing latches by PI/PO pairs\n" ); - fprintf( pErr, "\t-l : toggle removing latches [default = %s]\n", fRemoveLatches? "yes": "no" ); + fprintf( pErr, "usage: comb [-L num] [-lh]\n" ); + fprintf( pErr, "\t converts comb network into seq, and vice versa\n" ); + fprintf( pErr, "\t-L : number of latches to add to comb network (0 = do not add) [default = %d]\n", nLatchesToAdd ); + fprintf( pErr, "\t-l : toggle converting latches to PIs/POs or removing them [default = %s]\n", fRemoveLatches? "remove": "convert" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -8449,7 +8474,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_NtkDarTest( pNtk ); - Bbl_ManTest( pNtk ); +// Bbl_ManTest( pNtk ); + + { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern void Aig_ManFactorAlgebraicTest( Aig_Man_t * p ); + Aig_Man_t * pAig; + pAig = Abc_NtkToDar( pNtk, 0, 0 ); + Aig_ManFactorAlgebraicTest( pAig ); + Aig_ManStop( pAig ); + } + // Bbl_ManSimpleDemo(); return 0; usage: @@ -9576,7 +9611,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; @@ -18480,9 +18515,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSkipProof; int nFramesBmc; int nConfMaxBmc; + int nRatio; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -18496,9 +18532,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fSkipProof = 0; nFramesBmc = 2000; nConfMaxBmc = 5000; + nRatio = 10; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesvh" ) ) != EOF ) { switch ( c ) { @@ -18546,6 +18583,17 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfMaxBmc < 0 ) goto usage; break; + case 'R': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRatio = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRatio < 0 ) + goto usage; + break; case 'd': fDynamic ^= 1; break; @@ -18579,9 +18627,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); return 0; } + if ( !(0 <= nRatio && nRatio <= 100) ) + { + fprintf( stdout, "Wrong value of parameter \"-R <num>\".\n" ); + return 0; + } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose ); if ( pNtkRes == NULL ) { if ( pNtk->pSeqModel == NULL ) @@ -18592,13 +18645,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" ); + fprintf( pErr, "usage: abs [-FCGDR num] [-desvh]\n" ); fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax ); fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc ); fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc ); + fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", nRatio ); 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-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); @@ -18806,7 +18860,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) // Ioa_WriteBlif( pTemp, "test_boxes.blif" ); Ntl_ManFree( pTemp ); } - return 0; + return 0; } Abc_FrameClearDesign(); @@ -18960,7 +19014,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv ) fCollapsed = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "abch" ) ) != EOF ) - { + { switch ( c ) { case 'a': @@ -19392,7 +19446,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( pAbc->pAbc8Lib == NULL ) { - printf( "LUT library is not given. Using default 6-LUT library.\n" ); + printf( "LUT library is not given. Using default LUT library.\n" ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); } printf( "MAPPED: " ); @@ -19480,7 +19534,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pAbc8Lib == NULL ) { - printf( "LUT library is not given. Using default 6-LUT library.\n" ); + printf( "LUT library is not given. Using default LUT library.\n" ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); } @@ -20460,8 +20514,6 @@ usage: return 1; } - - /**Function************************************************************* Synopsis [] @@ -20606,6 +20658,56 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc8Insert( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void * Ntl_ManInsertNtk( void * p, void * pNtk ); + void * pNtlNew; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAbc8Ntl == NULL ) + { + printf( "Abc_CommandAbc8Insert(): There is no design.\n" ); + return 1; + } + if ( pAbc->pAbc8Nwk == NULL ) + { + printf( "Abc_CommandAbc8Insert(): There is no network to insert.\n" ); + return 1; + } + pNtlNew = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk ); + Abc_FrameClearDesign(); + pAbc->pAbc8Ntl = pNtlNew; + return 0; + +usage: + fprintf( stdout, "usage: *insert [-h]\n" ); + fprintf( stdout, "\t inserts the mapped network into the netlist\n" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { void * pNtlNew; @@ -21148,7 +21250,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsncvh" ) ) != EOF ) { switch ( c ) { @@ -21274,6 +21376,12 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': pPars->fLocalSim ^= 1; break; + case 'n': + pPars->fScorrGia ^= 1; + break; + case 'c': + pPars->fUseCSat ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -21327,7 +21435,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsvh]\n" ); + fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsncvh]\n" ); fprintf( stdout, "\t performs sequential sweep using K-step induction\n" ); fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -21343,6 +21451,8 @@ usage: fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( stdout, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" ); fprintf( stdout, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" ); + fprintf( stdout, "\t-n : toggle using new AIG package [default = %s]\n", pPars->fScorrGia? "yes": "no" ); + fprintf( stdout, "\t-c : toggle using new AIG package and SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -21414,7 +21524,7 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameClearDesign(); pAbc->pAbc8Ntl = pNtlTemp; } - + // sweep the current design Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose ); if ( Counter == 0 ) @@ -23389,7 +23499,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManCorSetDefaultParams( pPars ); pPars->fLatchCorr = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrcvh" ) ) != EOF ) { switch ( c ) { @@ -23415,6 +23525,17 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPrefix = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPrefix < 0 ) + goto usage; + break; case 'f': pPars->fFirstStop ^= 1; break; @@ -23447,10 +23568,11 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &lcorr [-FC num] [-frcvh]\n" ); + fprintf( stdout, "usage: &lcorr [-FCP num] [-frcvh]\n" ); fprintf( stdout, "\t performs latch correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); @@ -23477,7 +23599,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManCorSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrecvh" ) ) != EOF ) { switch ( c ) { @@ -23503,6 +23625,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPrefix = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPrefix < 0 ) + goto usage; + break; case 'f': pPars->fFirstStop ^= 1; break; @@ -23538,10 +23671,11 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" ); + fprintf( stdout, "usage: &scorr [-FCP num] [-frecvh]\n" ); fprintf( stdout, "\t performs signal correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); @@ -24297,7 +24431,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars ); if ( pAbc->pAbc8Lib == NULL ) { - printf( "LUT library is not given. Using default 6-LUT library.\n" ); + printf( "LUT library is not given. Using default LUT library.\n" ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); } // set defaults diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index a5973153..ab47d797 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1743,6 +1743,18 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) RetValue = Abc_NtkIvyProve( &pNtkComb, pParams ); // transfer model if given // pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL; + if ( RetValue == 0 && (Abc_NtkLatchNum(pNtk) == 0) ) + { + pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL; + printf( "Networks are not equivalent.\n" ); + ABC_PRT( "Time", clock() - clk ); + if ( pSecPar->fReportSolution ) + { + printf( "SOLUTION: FAIL " ); + ABC_PRT( "Time", clock() - clkTotal ); + } + return RetValue; + } Abc_NtkDelete( pNtkComb ); // return the result, if solved if ( RetValue == 1 ) @@ -2570,7 +2582,7 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; @@ -2580,7 +2592,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, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose ); if ( pTemp->pSeqModel ) { ABC_FREE( pNtk->pModel ); @@ -2710,7 +2722,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation // consider the case of one output if ( Abc_NtkCoNum(pNtkOn) == 1 ) return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose ); - // start the new newtork + // start the new network pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName); Abc_NtkForEachPi( pNtkOn, pObj, i ) @@ -3393,7 +3405,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) return NULL; /* Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, 1 ); Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 114288ba..bf082456 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -103,6 +103,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) Abc_Ntk_t * pNtkAig; Abc_Obj_t * pObj; int i, nNodes;//, RetValue; + int Counter = 0; assert( Abc_NtkIsStrash(pNtk) ); //timeRetime = clock(); // print warning about choice nodes @@ -112,8 +113,14 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); // complement the 1-values registers Abc_NtkForEachLatch( pNtk, pObj, i ) - if ( Abc_LatchIsInit1(pObj) ) + { + if ( Abc_LatchIsInitDc(pObj) ) + Counter++; + else if ( Abc_LatchIsInit1(pObj) ) Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); + } + if ( Counter ) + printf( "Converting %d flops from don't-care to zero initial value.\n", Counter ); // restrash the nodes (assuming a topological order of the old network) Abc_NtkForEachNode( pNtk, pObj, i ) pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index 76a82b51..5e9093e7 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -204,6 +204,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() ); +// Abc_ObjSetXsim( pObj, ABC_INIT_ONE ); Abc_AigForEachAnd( pNtk, pObj, i ) Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) ); Abc_NtkForEachCo( pNtk, pObj, i ) @@ -213,7 +214,11 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe } // set the final values Abc_NtkForEachLatch( pNtk, pObj, i ) + { pObj->pData = (void *)(ABC_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj)); +// printf( "%d", Abc_LatchIsInit1(pObj) ); + } +// printf( "\n" ); } /////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.c b/src/base/io/io.c index 46d61583..75419e0f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1823,13 +1823,18 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) char * pFileName; int c; int fNames; + int forceSeq; fNames = 0; + forceSeq = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snh" ) ) != EOF ) { switch ( c ) { + case 's': + forceSeq ^= 1; + break; case 'n': fNames ^= 1; break; @@ -1912,8 +1917,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) } if ( fNames ) { + char *cycle_ctr = forceSeq?"@0":""; Abc_NtkForEachPi( pNtk, pObj, i ) - fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); +// fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); + fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) ); } else { @@ -1927,9 +1934,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" ); + fprintf( pAbc->Err, "usage: write_counter [-snh] <file>\n" ); fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" ); fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" ); + fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" ); fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); |