luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/proof/cec/cecCorr.c

1138 lines
39 KiB
C
Raw Blame History

/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// 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 = Abc_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 = Abc_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 = Abc_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 = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_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, Abc_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 = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_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, Abc_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 = Abc_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 );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "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 = Abc_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 = Abc_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 );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "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 )
{
unsigned * pInfo;
int k, w, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = (unsigned *)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 = (unsigned *)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) );
// Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) );
// transfer info from the representative
pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
for ( w = 0; w < nWords; w++ )
pInfoObj[w] = pInfoRepr[w];
}
// Abc_Print( 1, "\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) );
// Abc_Print( 1, "%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 )
{
unsigned * pInfoObj, * pInfoRepr;
int w, i, iObj, iRepr, nWords;
nWords = Vec_PtrReadWordsSimInfo( vInfo );
Vec_IntForEachEntry( vPairs, iRepr, i )
{
iObj = Vec_IntEntry( vPairs, ++i );
pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj );
pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr );
for ( w = 0; w < nWords; w++ )
{
assert( 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 = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
if ( Abc_InfoHasBit( pPres, iBit ) &&
Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
Abc_InfoSetBit( pPres, iBit );
if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
Abc_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, kMax = 0;//, iBit = 1;
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_MaxInt( 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++ );
// Abc_Print( 1, "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 = (unsigned *)Vec_PtrEntry( vInfo, Abc_Lit2Var(iLit) );
if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(iLit) )
Abc_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
}
// Abc_Print( 1, "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 )
{
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->nFrames = 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) );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
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->nFrames = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, 0 );
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) )
// Abc_Print( 1, "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 ) )
// Abc_Print( 1, "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 )
// Abc_Print( 1, "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 = Abc_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 = Abc_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 )
Abc_Print( 1, "BMC : " );
else
Abc_Print( 1, "%3d : ", iIter );
Abc_Print( 1, "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++;
}
Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
Abc_PrintTime( 1, "T", Time );
}
/**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->nFrames = 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 = Tas_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 []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
int fRunBmcFirst = 1;
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;
int r, RetValue, clkTotal = clock();
int clkSat = 0, clkSim = 0, clkSrm = 0;
int clk2, clk = clock();
if ( Gia_ManRegNum(pAig) == 0 )
{
Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return 0;
}
Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nFrames = pPars->nFrames;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fConstCorr = pPars->fConstCorr;
pParsSim->fSeqSimulate = 1;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim );
if ( pAig->pReprs == NULL )
{
Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax );
Cec_ManSimClassesRefine( pSim );
}
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
Abc_Print( 1, "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 );
}
// check the base case
if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
if ( pPars->pFunc )
{
((int (*)(void *))pPars->pFunc)( pPars->pData );
((int (*)(void *))pPars->pFunc)( pPars->pData );
}
if ( pPars->nStepsMax == 0 )
{
Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
Cec_ManSimStop( pSim );
return 1;
}
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
if ( pPars->nStepsMax == r )
{
Cec_ManSimStop( pSim );
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
return 1;
}
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 );
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 );
if ( pPars->pFunc )
((int (*)(void *))pPars->pFunc)( pPars->pData );
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
// check the overflow
if ( r == nIterMax )
Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
// check the base case
if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
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_PrintTime( 1, "TOTAL", clkTotal );
}
return 1;
}
/**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 );
// Abc_Print( 1, "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, Abc_BitWordNum(Gia_ManRegNum(pAig)) );
Gia_ManForEachRo( pAig, pObj, i )
{
if ( pObj->fMark1 )
Abc_InfoSetBit( pInitState, i );
// Abc_Print( 1, "%d", pObj->fMark1 );
}
// Abc_Print( 1, "\n" );
Gia_ManCleanMark1( pAig );
return pInitState;
}
/**Function*************************************************************
Synopsis [Prints flop equivalences.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pRepr;
int i;
assert( p->vNamesIn != NULL );
Gia_ManForEachRo( p, pObj, i )
{
if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjIsCi(pRepr) )
Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ),
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
else
Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
}
}
}
/**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;
unsigned * pInitState;
int RetValue;
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, (int *)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_MaxInt( 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 )
{
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 )
{
Abc_Print( 1, "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) );
}
if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
// print verbose info about equivalences
if ( pPars->fVerboseFlops )
{
if ( pAig->vNamesIn == NULL )
Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" );
else
Cec_ManPrintFlopEquivs( pAig );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink