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

874 lines
30 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [saigAbsCba.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [CEX-based abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// local manager
typedef struct Saig_ManCba_t_ Saig_ManCba_t;
struct Saig_ManCba_t_
{
// user data
Aig_Man_t * pAig; // user's AIG
Abc_Cex_t * pCex; // user's CEX
int nInputs; // the number of first inputs to skip
int fVerbose; // verbose flag
// unrolling
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs
// additional information
Vec_Vec_t * vReg2Frame; // register to frame mapping
Vec_Vec_t * vReg2Value; // register to value mapping
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Selects the best flops from the given array.]
Description [Selects the best 'nFfsToSelect' flops among the array
'vAbsFfsToAdd' of flops that should be added to the abstraction.
To this end, this procedure simulates the original AIG (pAig) using
the given CEX (pAbsCex), which was detected for the abstraction.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
int i, k, f, Entry, iBit, * pPerm;
assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
// map previously abstracted flops into their original numbers
vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry == 0 )
Vec_IntPush( vMapEntries, i );
// simulate one frame at a time
assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
// initialize the flops
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = 0;
for ( f = 0; f < pAbsCex->iFrame; f++ )
{
// override the flop values according to the cex
iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
Vec_IntForEachEntry( vMapEntries, Entry, k )
Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k);
// simulate
Aig_ManForEachNode( pAig, pObj, k )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachCo( pAig, pObj, k )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
// transfer
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
pObjRo->fMarkB = pObjRi->fMarkB;
// compare
iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
Vec_IntForEachEntry( vMapEntries, Entry, k )
if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) )
Vec_IntAddToEntry( vFlopCosts, k, 1 );
}
// Vec_IntForEachEntry( vFlopCosts, Entry, i )
// printf( "%d ", Entry );
// printf( "\n" );
// remap the cost
vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
// sort the flops
pPerm = Abc_MergeSortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
// shrink the array
vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
for ( i = 0; i < nFfsToSelect; i++ )
{
// printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
}
// printf( "\n" );
// cleanup
ABC_FREE( pPerm );
Vec_IntFree( vMapEntries );
Vec_IntFree( vFlopCosts );
Vec_IntFree( vFlopAddCosts );
Aig_ManCleanMarkB(pAig);
// return the computed flops
return vFfsToAddBest;
}
/**Function*************************************************************
Synopsis [Duplicate with literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
{
Vec_Int_t * vLevel;
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pMiter;
int i, k, Lit;
assert( pAig->nConstrs == 0 );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) );
pAigNew->pName = Abc_UtilStrsav( pAig->pName );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
Aig_ManForEachCi( pAig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pAigNew );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs for cubes
Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
{
pMiter = Aig_ManConst1( pAigNew );
Vec_IntForEachEntry( vLevel, Lit, k )
{
pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
}
Aig_ObjCreateCo( pAigNew, pMiter );
}
// transfer to register outputs
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
// finalize
Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
return pAigNew;
}
/**Function*************************************************************
Synopsis [Maps array of frame PI IDs into array of additional PI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaReason2Inputs( Saig_ManCba_t * p, Vec_Int_t * vReasons )
{
Vec_Int_t * vOriginal, * vVisited;
int i, Entry;
vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) );
vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
Vec_IntForEachEntry( vReasons, Entry, i )
{
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
assert( iInput >= p->nInputs && iInput < Aig_ManCiNum(p->pAig) );
if ( Vec_IntEntry(vVisited, iInput) == 0 )
Vec_IntPush( vOriginal, iInput - p->nInputs );
Vec_IntAddToEntry( vVisited, iInput, 1 );
}
Vec_IntFree( vVisited );
return vOriginal;
}
/**Function*************************************************************
Synopsis [Creates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons )
{
Abc_Cex_t * pCare;
int i, Entry, iInput, iFrame;
pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
Vec_IntForEachEntry( vReasons, Entry, i )
{
assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
}
/*
for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ )
{
int Count = 0;
for ( i = 0; i < pCare->nPis; i++ )
Count += Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i);
printf( "%d ", Count );
}
printf( "\n" );
*/
return pCare;
}
/**Function*************************************************************
Synopsis [Returns reasons for the property to fail.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsConst1(pObj) )
return;
if ( Aig_ObjIsCi(pObj) )
{
Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
return;
}
assert( Aig_ObjIsNode(pObj) );
if ( pObj->fPhase )
{
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
}
else
{
int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
assert( !fPhase0 || !fPhase1 );
if ( !fPhase0 && fPhase1 )
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
else if ( fPhase0 && !fPhase1 )
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
else
{
int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
if ( iPrio0 <= iPrio1 )
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
else
Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
}
}
}
/**Function*************************************************************
Synopsis [Returns reasons for the property to fail.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
{
Aig_Obj_t * pObj;
Vec_Int_t * vPrios, * vReasons;
int i;
// set PI values according to CEX
vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
Aig_ManConst1(p->pFrames)->fPhase = 1;
Aig_ManForEachCi( p->pFrames, pObj, i )
{
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
}
// traverse and set the priority
Aig_ManForEachNode( p->pFrames, pObj, i )
{
int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
pObj->fPhase = fPhase0 && fPhase1;
if ( fPhase0 && fPhase1 ) // both are one
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
else if ( !fPhase0 && fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
else if ( fPhase0 && !fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
else // both are zero
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
}
// check the property output
pObj = Aig_ManCo( p->pFrames, 0 );
pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
assert( !pObj->fPhase );
// select the reason
vReasons = Vec_IntAlloc( 100 );
Aig_ManIncrementTravId( p->pFrames );
Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
Vec_IntFree( vPrios );
// assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
return vReasons;
}
/**Function*************************************************************
Synopsis [Collect nodes in the unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsCo(pObj) )
Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
else if ( Aig_ObjIsNode(pObj) )
{
Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
}
if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
Vec_IntPush( vObjs, Aig_ObjId(pObj) );
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A, Vec_Vec_t ** pvReg2Frame )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
Vec_Vec_t * vFrameObjs; // the list of objects per frame
Vec_Int_t * vRoots, * vObjs;
Aig_Obj_t * pObj;
int i, f;
// sanity checks
assert( Saig_ManPiNum(pAig) == pCex->nPis );
// assert( Saig_ManRegNum(pAig) == pCex->nRegs );
assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
// map PIs of the unrolled frames into PIs of the original design
*pvMapPiF2A = Vec_IntAlloc( 1000 );
// collect COs and Objs visited in each frame
vFrameCos = Vec_VecStart( pCex->iFrame+1 );
vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
// initialized the topmost frame
pObj = Aig_ManCo( pAig, pCex->iPo );
Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
for ( f = pCex->iFrame; f >= 0; f-- )
{
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
vRoots = Vec_VecEntryInt( vFrameCos, f );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManCbaUnrollCollect_rec( pAig, pObj,
Vec_VecEntryInt(vFrameObjs, f),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
}
// derive unrolled timeframes
pFrames = Aig_ManStart( 10000 );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// initialize the flops
if ( Saig_ManRegNum(pAig) == pCex->nRegs )
{
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
}
else // this is the case when synthesis was applied, assume all-0 init state
{
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), 1 );
}
// iterate through the frames
for ( f = 0; f <= pCex->iFrame; f++ )
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else if ( Aig_ObjIsCo(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pFrames);
else if ( Saig_ObjIsPi(pAig, pObj) )
{
if ( Aig_ObjCioId(pObj) < nInputs )
{
int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
}
else
{
pObj->pData = Aig_ObjCreateCi( pFrames );
Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
Vec_IntPush( *pvMapPiF2A, f );
}
}
}
if ( f == pCex->iFrame )
break;
// transfer
vRoots = Vec_VecEntryInt( vFrameCos, f );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
{
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
if ( *pvReg2Frame )
{
Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) ); // record LO
Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjToLit((Aig_Obj_t *)pObj->pData) ); // record its literal
}
}
}
// create output
pObj = Aig_ManCo( pAig, pCex->iPo );
Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
Aig_ManSetRegNum( pFrames, 0 );
// cleanup
Vec_VecFree( vFrameCos );
Vec_VecFree( vFrameObjs );
// finallize
Aig_ManCleanup( pFrames );
// return
return pFrames;
}
/**Function*************************************************************
Synopsis [Creates refinement manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
Saig_ManCba_t * p;
p = ABC_CALLOC( Saig_ManCba_t, 1 );
p->pAig = pAig;
p->pCex = pCex;
p->nInputs = nInputs;
p->fVerbose = fVerbose;
return p;
}
/**Function*************************************************************
Synopsis [Destroys refinement manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCbaStop( Saig_ManCba_t * p )
{
Vec_VecFreeP( &p->vReg2Frame );
Vec_VecFreeP( &p->vReg2Value );
Aig_ManStopP( &p->pFrames );
Vec_IntFreeP( &p->vMapPiF2A );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Destroys refinement manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManCbaShrink( Saig_ManCba_t * p )
{
Aig_Man_t * pManNew;
Aig_Obj_t * pObjLi, * pObjFrame;
Vec_Int_t * vLevel, * vLevel2;
int f, k, ObjId, Lit;
// assuming that important objects are labeled in Saig_ManCbaFindReason()
Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f )
{
Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k )
{
pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) );
if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) )
continue;
pObjLi = Aig_ManObj( p->pAig, ObjId );
assert( Saig_ObjIsLi(p->pAig, pObjLi) );
Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
}
}
// print statistics
Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k )
{
vLevel2 = Vec_VecEntryInt( p->vReg2Value, k );
printf( "Level = %4d StateBits = %4d (%6.2f %%) CareBits = %4d (%6.2f %%)\n", k,
Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig),
Vec_IntSize(vLevel2), 100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) );
}
// try reducing the frames
pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
// Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
Aig_ManStop( pManNew );
}
static inline void Saig_ObjCexMinSet0( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 0; }
static inline void Saig_ObjCexMinSet1( Aig_Obj_t * pObj ) { pObj->fMarkA = 0; pObj->fMarkB = 1; }
static inline void Saig_ObjCexMinSetX( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 1; }
static inline int Saig_ObjCexMinGet0( Aig_Obj_t * pObj ) { return pObj->fMarkA && !pObj->fMarkB; }
static inline int Saig_ObjCexMinGet1( Aig_Obj_t * pObj ) { return !pObj->fMarkA && pObj->fMarkB; }
static inline int Saig_ObjCexMinGetX( Aig_Obj_t * pObj ) { return pObj->fMarkA && pObj->fMarkB; }
static inline int Saig_ObjCexMinGet0Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }
static inline int Saig_ObjCexMinGet1Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }
static inline int Saig_ObjCexMinGet0Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }
static inline int Saig_ObjCexMinGet1Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }
static inline void Saig_ObjCexMinSim( Aig_Obj_t * pObj )
{
if ( Aig_ObjIsAnd(pObj) )
{
if ( Saig_ObjCexMinGet0Fanin0(pObj) || Saig_ObjCexMinGet0Fanin1(pObj) )
Saig_ObjCexMinSet0( pObj );
else if ( Saig_ObjCexMinGet1Fanin0(pObj) && Saig_ObjCexMinGet1Fanin1(pObj) )
Saig_ObjCexMinSet1( pObj );
else
Saig_ObjCexMinSetX( pObj );
}
else if ( Aig_ObjIsCo(pObj) )
{
if ( Saig_ObjCexMinGet0Fanin0(pObj) )
Saig_ObjCexMinSet0( pObj );
else if ( Saig_ObjCexMinGet1Fanin0(pObj) )
Saig_ObjCexMinSet1( pObj );
else
Saig_ObjCexMinSetX( pObj );
}
else assert( 0 );
}
static inline void Saig_ObjCexMinPrint( Aig_Obj_t * pObj )
{
if ( Saig_ObjCexMinGet0(pObj) )
printf( "0" );
else if ( Saig_ObjCexMinGet1(pObj) )
printf( "1" );
else if ( Saig_ObjCexMinGetX(pObj) )
printf( "X" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManCexVerifyUsingTernary( Aig_Man_t * pAig, Abc_Cex_t * pCex, Abc_Cex_t * pCare )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int i, f, iBit = 0;
assert( pCex->iFrame == pCare->iFrame );
assert( pCex->nBits == pCare->nBits );
assert( pCex->iPo < Saig_ManPoNum(pAig) );
Saig_ObjCexMinSet1( Aig_ManConst1(pAig) );
// set flops to the init state
Saig_ManForEachLo( pAig, pObj, i )
{
assert( !Abc_InfoHasBit(pCex->pData, iBit) );
assert( !Abc_InfoHasBit(pCare->pData, iBit) );
// if ( Abc_InfoHasBit(pCare->pData, iBit++) )
Saig_ObjCexMinSet0( pObj );
// else
// Saig_ObjCexMinSetX( pObj );
}
iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ )
{
// init inputs
Saig_ManForEachPi( pAig, pObj, i )
{
if ( Abc_InfoHasBit(pCare->pData, iBit++) )
{
if ( Abc_InfoHasBit(pCex->pData, iBit-1) )
Saig_ObjCexMinSet1( pObj );
else
Saig_ObjCexMinSet0( pObj );
}
else
Saig_ObjCexMinSetX( pObj );
}
// simulate internal nodes
Aig_ManForEachNode( pAig, pObj, i )
Saig_ObjCexMinSim( pObj );
// simulate COs
Aig_ManForEachCo( pAig, pObj, i )
Saig_ObjCexMinSim( pObj );
/*
Aig_ManForEachObj( pAig, pObj, i )
{
Aig_ObjPrint(pAig, pObj);
printf( " Value = " );
Saig_ObjCexMinPrint( pObj );
printf( "\n" );
}
*/
// transfer
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
pObjRo->fMarkA = pObjRi->fMarkA,
pObjRo->fMarkB = pObjRi->fMarkB;
}
assert( iBit == pCex->nBits );
return Saig_ObjCexMinGet1( Aig_ManCo( pAig, pCex->iPo ) );
}
/**Function*************************************************************
Synopsis [SAT-based refinement of the counter-example.]
Description [The first parameter (nInputs) indicates how many first
primary inputs to skip without considering as care candidates.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
Saig_ManCba_t * p;
Vec_Int_t * vReasons;
Abc_Cex_t * pCare;
abctime clk = Abc_Clock();
clk = Abc_Clock();
p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
// p->vReg2Frame = Vec_VecStart( pCex->iFrame );
// p->vReg2Value = Vec_VecStart( pCex->iFrame );
p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
vReasons = Saig_ManCbaFindReason( p );
if ( p->vReg2Frame )
Saig_ManCbaShrink( p );
//if ( fVerbose )
//Aig_ManPrintStats( p->pFrames );
if ( fVerbose )
{
Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons );
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
Vec_IntFree( vRes );
ABC_PRT( "Time", Abc_Clock() - clk );
}
pCare = Saig_ManCbaReason2Cex( p, vReasons );
Vec_IntFree( vReasons );
Saig_ManCbaStop( p );
if ( fVerbose )
{
printf( "Real " );
Abc_CexPrintStats( pCex );
}
if ( fVerbose )
{
printf( "Care " );
Abc_CexPrintStats( pCare );
}
/*
// verify the reduced counter-example using ternary simulation
if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
else if ( fVerbose )
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
*/
Aig_ManCleanMarkAB( pAig );
return pCare;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
{
Saig_ManCba_t * p;
Vec_Int_t * vRes, * vReasons;
abctime clk;
if ( Saig_ManPiNum(pAig) != pCex->nPis )
{
printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n",
Aig_ManCiNum(pAig), pCex->nPis );
return NULL;
}
clk = Abc_Clock();
p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
vReasons = Saig_ManCbaFindReason( p );
vRes = Saig_ManCbaReason2Inputs( p, vReasons );
if ( fVerbose )
{
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", Abc_Clock() - clk );
}
Vec_IntFree( vReasons );
Saig_ManCbaStop( p );
return vRes;
}
/**Function*************************************************************
Synopsis [Checks the abstracted model for a counter-example.]
Description [Returns the array of abstracted flops that should be added
to the abstraction.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
{
Vec_Int_t * vAbsFfsToAdd;
int RetValue;
abctime clk = Abc_Clock();
// assert( pAbs->nRegs > 0 );
// perform BMC
RetValue = Saig_ManBmcScalable( pAbs, pPars );
if ( RetValue == -1 ) // time out - nothing to add
{
printf( "Resource limit is reached during BMC.\n" );
assert( pAbs->pSeqModel == NULL );
return Vec_IntAlloc( 0 );
}
if ( pAbs->pSeqModel == NULL )
{
printf( "BMC did not detect a CEX with the given depth.\n" );
return Vec_IntAlloc( 0 );
}
if ( pPars->fVerbose )
Abc_CexPrintStats( pAbs->pSeqModel );
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
{
Vec_IntFree( vAbsFfsToAdd );
return NULL;
}
if ( pPars->fVerbose )
{
printf( "Adding %d registers to the abstraction (total = %d). ",
Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return vAbsFfsToAdd;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink