/**CFile****************************************************************
FileName [absOut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [Abstraction refinement outside of abstraction engines.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
{
Abc_Cex_t * pCex;
int i, f, iPiNum;
assert( pCexAbs->iPo == 0 );
// start the counter-example
pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
for ( f = 0; f <= pCexAbs->iFrame; f++ )
for ( i = 0; i < Vec_IntSize(vPis); i++ )
{
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
{
iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
}
}
// verify the counter example
if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
{
Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
else
{
Abc_Print( 1, "Counter-example verification is successful.\n" );
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
}
return pCex;
}
/**Function*************************************************************
Synopsis [Refines gate-level abstraction using the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
{
extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
int fAddOneLayer = 1;
Abc_Cex_t * pCexNew = NULL;
Gia_Man_t * pAbs;
Aig_Man_t * pAig;
Abc_Cex_t * pCare;
Vec_Int_t * vPis, * vPPis;
int f, i, iObjId;
abctime clk = Abc_Clock();
int nOnes = 0, Counter = 0;
if ( p->vGateClasses == NULL )
{
Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
return -1;
}
// derive abstraction
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
Gia_ManStop( pAbs );
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
if ( Gia_ManPiNum(pAbs) != pCex->nPis )
{
Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
Gia_ManStop( pAbs );
return -1;
}
if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
{
Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
// Gia_ManStop( pAbs );
// return -1;
}
// else
// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
// get inputs
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
// add missing logic
if ( fAddOneLayer )
{
Gia_Obj_t * pObj;
// check if this is a real counter-example
Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Gia_ManForEachPi( pAbs, pObj, i )
{
if ( i >= Vec_IntSize(vPis) ) // PPIs
Gia_ObjTerSimSetX( pObj );
else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachRo( pAbs, pObj, i )
{
if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( pAbs, pObj );
}
Gia_ManForEachAnd( pAbs, pObj, i )
Gia_ObjTerSimAnd( pObj );
Gia_ManForEachCo( pAbs, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( pAbs, 0 );
if ( Gia_ObjTerSimGet1(pObj) )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
// else
// Abc_Print( 1, "CEX is not real.\n" );
Gia_ManForEachObj( pAbs, pObj, i )
Gia_ObjTerSimSetC( pObj );
if ( pCexNew == NULL )
{
// grow one layer
Vec_IntForEachEntry( vPPis, iObjId, i )
{
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
}
if ( fVerbose )
{
Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
}
else
{
// minimize the CEX
pAig = Gia_ManToAigSimple( pAbs );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
Aig_ManStop( pAig );
if ( pCare == NULL )
Abc_Print( 1, "Counter-example minimization has failed.\n" );
// add new objects to the map
iObjId = -1;
for ( f = 0; f <= pCare->iFrame; f++ )
for ( i = 0; i < pCare->nPis; i++ )
if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
{
nOnes++;
assert( i >= Vec_IntSize(vPis) );
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
continue;
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
// Abc_Print( 1, "Adding object %d.\n", iObjId );
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
Counter++;
}
Abc_CexFree( pCare );
if ( fVerbose )
{
Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// consider the case of SAT
if ( iObjId == -1 )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
}
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Gia_ManStop( pAbs );
if ( pCexNew )
{
ABC_FREE( p->pCexSeq );
p->pCexSeq = pCexNew;
return 0;
}
// extract abstraction to include min-cut
if ( fMinCut )
Nwk_ManDeriveMinCut( p, fVerbose );
return -1;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example and returns flop values.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManGetStateAndCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
{
Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) );
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
assert( iFrame >= 0 && iFrame <= p->iFrame );
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ )
{
if ( i == iFrame )
{
Gia_ManForEachRo( pAig, pObjRo, k )
Vec_IntPush( vInit, pObjRo->fMark0 );
}
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
if ( RetValue != 1 )
Vec_IntFreeP( &vInit );
Gia_ManCleanMark0(pAig);
return vInit;
}
/**Function*************************************************************
Synopsis [Verify counter-example starting in the given timeframe.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
assert( iFrame >= 0 && iFrame <= p->iFrame );
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
Gia_ManCleanMark0(pAig);
if ( RetValue == 1 )
printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" );
else
printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vInit )
{
Vec_Bit_t * vInitNew;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, iFlopId;
assert( Vec_IntSize(vInit) == Vec_IntSize(vFlops) );
vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
Gia_ManForEachObjVec( vFlops, p, pObj, i )
{
assert( Gia_ObjIsRo(p, pObj) );
if ( Vec_IntEntry(vInit, i) == 0 )
continue;
iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) );
Vec_BitWriteEntry( vInitNew, iFlopId, 1 );
}
pNew = Gia_ManDupFlip( p, Vec_BitArray(vInitNew) );
Vec_BitFree( vInitNew );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose )
{
Gia_Man_t * pAbs, * pNew;
Vec_Int_t * vFlops, * vInit;
Vec_Int_t * vCopy;
// abctime clk = Abc_Clock();
int RetValue;
ABC_FREE( p->pCexSeq );
if ( p->vGateClasses == NULL )
{
Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" );
return -1;
}
vCopy = Vec_IntDup( p->vGateClasses );
Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra );
// derive abstraction
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
Gia_ManStop( pAbs );
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
if ( Gia_ManPiNum(pAbs) != pCex->nPis )
{
Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" );
Gia_ManStop( pAbs );
Vec_IntFree( vCopy );
return -1;
}
// get the state in frame iFrameStart
vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart );
if ( vInit == NULL )
{
Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" );
Gia_ManStop( pAbs );
Vec_IntFree( vCopy );
return -1;
}
if ( fVerbose )
Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" );
// get inputs
Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL );
// assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
Gia_ManStop( pAbs );
//Vec_IntPrint( vFlops );
//Vec_IntPrint( vInit );
// transform the manager to have new init state
pNew = Gia_ManTransformFlops( p, vFlops, vInit );
Vec_IntFree( vFlops );
Vec_IntFree( vInit );
// verify abstraction
{
Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses );
Gia_ManCheckCex( pAbs, pCex, iFrameStart );
Gia_ManStop( pAbs );
}
// transfer abstraction
assert( pNew->vGateClasses == NULL );
pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
// perform abstraction for the new AIG
{
Abs_Par_t Pars, * pPars = &Pars;
Abs_ParSetDefaults( pPars );
pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra;
pPars->fVerbose = fVerbose;
RetValue = Gia_ManPerformGla( pNew, pPars );
if ( RetValue == 0 ) // spurious SAT
{
Vec_IntFreeP( &pNew->vGateClasses );
pNew->vGateClasses = Vec_IntDup( vCopy );
}
}
// move the abstraction map
Vec_IntFreeP( &p->vGateClasses );
p->vGateClasses = pNew->vGateClasses;
pNew->vGateClasses = NULL;
// cleanup
Gia_ManStop( pNew );
Vec_IntFree( vCopy );
return -1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END