Skip to content

A
abc
Commit 22ae2e45 by Alan Mishchenko
Options

Gate level abstraction.

parent 564a3553
Showing with 591 additions and 73 deletions
src/aig/gia/giaAbsVta.c
...@@ -23,6 +23,7 @@ ...@@ -23,6 +23,7 @@
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
#define VTA_LARGE 0xFFFFFF
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -34,14 +35,10 @@ struct Vta_Obj_t_ ...@@ -34,14 +35,10 @@ struct Vta_Obj_t_
int iObj; int iObj;
int iFrame; int iFrame;
int iNext; int iNext;
unsigned Prio : 24; unsigned Prio : 24; // related to VTA_LARGE
unsigned Value : 2; unsigned Value : 2;
unsigned fAdded : 1; unsigned fAdded : 1;
unsigned fNew : 1; unsigned fNew : 1;
// unsigned fPi : 1;
// unsigned fConst : 1;
// int fFlop : 1;
// int fAnd : 1;
}; };
typedef struct Vta_Man_t_ Vta_Man_t; // manager typedef struct Vta_Man_t_ Vta_Man_t; // manager
...@@ -54,24 +51,50 @@ struct Vta_Man_t_ ...@@ -54,24 +51,50 @@ struct Vta_Man_t_
int nTimeMax; // runtime limit int nTimeMax; // runtime limit
int fVerbose; // verbose flag int fVerbose; // verbose flag
// internal data // internal data
int iFrame; // current frame
int nObjs; // the number of objects int nObjs; // the number of objects
int nObjsAlloc; // the number of objects allocated int nObjsAlloc; // the number of objects allocated
int nBins; // number of hash table entries int nBins; // number of hash table entries
int * pBins; // hash table bins int * pBins; // hash table bins
Vta_Obj_t * pObjs; // hash table bins Vta_Obj_t * pObjs; // hash table bins
Vec_Int_t * vOrder; // objects in DPS order
// abstraction // abstraction
int nWords; // the number of sim words for abs int nWords; // the number of sim words for abs
int nFrames; // the number of copmleted frames int nFramesS; // the number of copmleted frames
Vec_Int_t * vAbs; // abstraction Vec_Int_t * vAbs; // starting abstraction
Vec_Int_t * vAbsNew; // computed abstraction
Vec_Int_t * vAbsAll; // abstraction of all timeframes
// other data // other data
Vec_Int_t * vCla2Var; // map clauses into variables Vec_Int_t * vCla2Var; // map clauses into variables
Vec_Ptr_t * vCores; // unsat core for each frame
sat_solver2 * pSat; // incremental SAT solver sat_solver2 * pSat; // incremental SAT solver
}; };
#define VTA_VAR0 1
#define VTA_VAR1 2
#define VTA_VARX 3
static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
{
return (pThis->Value == VTA_VAR0 && !fCompl) || (pThis->Value == VTA_VAR1 && fCompl);
}
static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
{
return (pThis->Value == VTA_VAR1 && !fCompl) || (pThis->Value == VTA_VAR0 && fCompl);
}
static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
static inline unsigned * Vta_ObjAbs( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbs, i*p->nWords ); } static inline unsigned * Vta_ObjAbsOld( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbs, i*p->nWords ); }
static inline unsigned * Vta_ObjAbsNew( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return (unsigned *)Vec_IntEntryP( p->vAbsNew, i*p->nWords ); }
#define Vta_ManForEachObj( p, pObj, i ) \
for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
#define Vta_ManForEachObjVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -112,6 +135,35 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords ) ...@@ -112,6 +135,35 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Detects how many frames are completed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vta_ManDeriveAbsAll( Vec_Int_t * p, int nWords )
{
Vec_Int_t * vRes;
unsigned * pThis;
int i, w, nObjs = Vec_IntSize(p) / nWords;
assert( Vec_IntSize(p) % nWords == 0 );
vRes = Vec_IntAlloc( nObjs );
for ( i = 0; i < nObjs; i++ )
{
pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
for ( w = 0; w < nWords; w++ )
if ( pThis[w] )
break;
Vec_IntPush( vRes, (int)(w < nWords) );
}
return vRes;
}
/**Function*************************************************************
Synopsis [] Synopsis []
Description [] Description []
...@@ -137,14 +189,18 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in ...@@ -137,14 +189,18 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in
p->nObjs = 1; p->nObjs = 1;
p->nBins = Gia_PrimeCudd( p->nObjsAlloc/2 ); p->nBins = Gia_PrimeCudd( p->nObjsAlloc/2 );
p->pBins = ABC_CALLOC( int, p->nBins ); p->pBins = ABC_CALLOC( int, p->nBins );
p->vOrder = Vec_IntAlloc( 1013 );
// abstraction // abstraction
p->nWords = vAbs ? Vec_IntSize(vAbs) / Gia_ManObjNum(p->pGia) : 1; p->nWords = vAbs ? Vec_IntSize(vAbs) / Gia_ManObjNum(p->pGia) : 1;
p->nFrames = vAbs ? Vta_ManReadFrameStart( vAbs, p->nWords ) : 0; p->nFramesS = vAbs ? Vta_ManReadFrameStart( vAbs, p->nWords ) : Abc_MinInt( p->nFramesMax, 10 );
p->vAbs = vAbs ? vAbs : Vec_IntStart( Gia_ManObjNum(p->pGia) * p->nWords ); p->vAbs = vAbs ? Vec_IntDup(vAbs) : Vec_IntStartFull( Gia_ManObjNum(p->pGia) * p->nWords );
p->vAbsNew = Vec_IntStart( Gia_ManObjNum(p->pGia) * p->nWords );
p->vAbsAll = Vta_ManDeriveAbsAll( vAbs, p->nWords );
// other data // other data
p->vCla2Var = Vec_IntAlloc( 1000 ); p->vCla2Var = Vec_IntAlloc( 1000 );
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new(); p->pSat = sat_solver2_new();
assert( nFramesMax == 0 || p->nFrames < nFramesMax ); assert( nFramesMax == 0 || p->nFramesS <= nFramesMax );
return p; return p;
} }
...@@ -162,6 +218,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in ...@@ -162,6 +218,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Vec_Int_t * vAbs, int nFramesMax, in
void Vga_ManStop( Vta_Man_t * p ) void Vga_ManStop( Vta_Man_t * p )
{ {
assert( p->vAbs == NULL ); assert( p->vAbs == NULL );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_IntFreeP( &p->vAbs );
Vec_IntFreeP( &p->vAbsAll );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vCla2Var ); Vec_IntFreeP( &p->vCla2Var );
sat_solver2_delete( p->pSat ); sat_solver2_delete( p->pSat );
ABC_FREE( p->pBins ); ABC_FREE( p->pBins );
...@@ -255,14 +315,11 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) ...@@ -255,14 +315,11 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Vga_ManAddClauses( Vta_Man_t * p, int iObjStart ) void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis )
{ {
Vta_Obj_t * pThis, * pThis0, * pThis1; Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i; int i = Vta_ObjId( p, pThis );
for ( i = iObjStart; i < p->nObjs; i++ )
{
pThis = Vta_ManObj( p, i );
assert( !pThis->fAdded && !pThis->fNew ); assert( !pThis->fAdded && !pThis->fNew );
pObj = Gia_ManObj( p->pGia, pThis->iObj ); pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
...@@ -312,53 +369,6 @@ void Vga_ManAddClauses( Vta_Man_t * p, int iObjStart ) ...@@ -312,53 +369,6 @@ void Vga_ManAddClauses( Vta_Man_t * p, int iObjStart )
} }
else if ( !Gia_ObjIsPi(p->pGia, pObj) ) else if ( !Gia_ObjIsPi(p->pGia, pObj) )
assert( 0 ); assert( 0 );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame )
{
Gia_Obj_t * pObj;
Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
assert( !Gia_ObjIsCo(pObj) );
if ( !pThis->fNew )
return;
pThis->fNew = 0;
pObj = Gia_ManObj( p->pGia, iObj );
if ( Gia_ObjIsAnd(pObj) )
{
Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
Vga_ManUnroll_rec( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( iFrame == 0 )
{
pThis = Vga_ManFindOrAdd( p, iObj, -1 );
assert( pThis->fNew );
pThis->fNew = 0;
}
else
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
}
}
else if ( Gia_ObjIsPi(p->pGia, pObj) )
{}
else if ( Gia_ObjIsConst0(pObj) )
{}
else assert( 0 );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -372,10 +382,11 @@ static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame ) ...@@ -372,10 +382,11 @@ static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Vta_ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) Vec_Int_t * Vta_ManUnsatCore( Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
{ {
Vec_Int_t * vPres;
Vec_Int_t * vCore; Vec_Int_t * vCore;
int RetValue, clk = clock(); int k, i, Entry, RetValue, clk = clock();
if ( piRetValue ) if ( piRetValue )
*piRetValue = -1; *piRetValue = -1;
// solve the problem // solve the problem
...@@ -409,9 +420,359 @@ Vec_Int_t * Vta_ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, in ...@@ -409,9 +420,359 @@ Vec_Int_t * Vta_ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, in
printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
// remap core into variables
vPres = Vec_IntStart( sat_solver2_nvars(pSat) );
k = 0;
Vec_IntForEachEntry( vCore, Entry, i )
{
Entry = Vec_IntEntry(vCla2Var, Entry);
if ( Vec_IntEntry(vPres, Entry) )
continue;
Vec_IntWriteEntry( vPres, Entry, 1 );
Vec_IntWriteEntry( vCore, k++, Entry );
}
Vec_IntShrink( vCore, k );
Vec_IntFree( vPres );
if ( fVerbose )
{
printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore; return vCore;
} }
/**Function*************************************************************
Synopsis [Compares two objects by their distance.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 )
{
int Diff = (*pp1)->Prio - (*pp2)->Prio;
if ( Diff < 0 )
return -1;
if ( Diff > 0 )
return 1;
Diff = (*pp1) - (*pp2);
if ( Diff < 0 )
return -1;
if ( Diff > 0 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Refines abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
{
Abc_Cex_t * pCex = NULL;
Vec_Ptr_t * vTermsUsed, * vTermsUnused;
Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
Gia_Obj_t * pObj;
int i, Counter;
assert( Vec_IntSize(p->vOrder) == p->nObjs - 1 );
// clean depth field
Vta_ManForEachObj( p, pThis, i )
{
pThis->Prio = VTA_LARGE;
pThis->Value = sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0;
}
// set the last node
pThis = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
pThis->Prio = 1;
// consider nodes in the reverse order
vTermsUsed = Vec_PtrAlloc( 1015 );
vTermsUnused = Vec_PtrAlloc( 1016 );
Vta_ManForEachObjVecReverse( p->vOrder, p, pThis, i )
{
// skip unreachable ones
if ( pThis->Prio == VTA_LARGE )
continue;
// skip contants and PIs
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
{
pThis->Prio = 0;
continue;
}
// collect useful terminals
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( !pThis->fAdded )
{
assert( pThis->Prio > 0 || pThis->Prio < VTA_LARGE );
if ( Vec_IntEntry(p->vAbsAll, pThis->iObj) )
Vec_PtrPush( vTermsUsed, pThis );
else
Vec_PtrPush( vTermsUnused, pThis );
continue;
}
// propagate
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame == 0 )
pThis->Prio = 0;
else
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
}
}
else assert( 0 );
}
// objects with equal distance should receive priority based on number
// those objects whose prototypes have been added in other timeframes
// should have higher priority than the current object
Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease );
Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
// assign the priority based on these orders
Counter = 1;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
pThis->Prio = Counter++;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
pThis->Prio = Counter++;
// propagate in the direct order
Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
{
assert( pThis->fNew == 0 );
// skip unreachable ones
if ( pThis->Prio == VTA_LARGE )
continue;
// skip terminal objects
if ( !pThis->fAdded )
continue;
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
pObj = Gia_ManObj( p->pGia, pThis->iObj );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( pThis->Value == VTA_VAR1 )
{
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
}
else if ( pThis->Value == VTA_VAR0 )
{
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio );
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Prio = pThis0->Prio;
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Prio = pThis1->Prio;
else assert( 0 );
}
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
pThis->Prio = pThis0->Prio;
}
}
}
Vec_PtrClear( vTermsUsed );
// select important values
pTop = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
pTop->fNew = 1;
Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
{
if ( pThis->fNew == 0 )
continue;
pThis->fNew = 0;
assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
// skip terminal objects
if ( !pThis->fAdded )
{
Vec_PtrPush( vTermsUsed, pThis );
continue;
}
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
pObj = Gia_ManObj( p->pGia, pThis->iObj );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( pThis->Value == VTA_VAR1 )
{
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
pThis0->fNew = 1;
pThis1->fNew = 1;
}
else if ( pThis->Value == VTA_VAR0 )
{
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
assert( pThis0->Prio <= pThis->Prio );
assert( pThis1->Prio <= pThis->Prio );
if ( pThis0->Prio <= pThis1->Prio )
pThis0->fNew = 1;
else
pThis1->fNew = 1;
}
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
pThis0->fNew = 1;
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis1->fNew = 1;
else assert( 0 );
}
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
pThis0->fNew = 1;
}
}
}
// verify
Vta_ManForEachObj( p, pThis, i )
pThis->Value = VTA_VARX;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
// simulate
Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
{
assert( pThis->fNew == 0 );
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR1;
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR0;
else
pThis->Value = VTA_VARX;
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
assert( pThis0 );
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Value = VTA_VAR0;
else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
pThis->Value = VTA_VAR1;
else
pThis->Value = VTA_VARX;
}
}
// double check the solver
if ( pThis->Value != VTA_VARX )
assert( (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
}
// check the output
if ( pTop->Value != VTA_VAR1 )
printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
// produce true counter-example
if ( pTop->Prio == 0 )
{
pCex = NULL;
pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->iFrame+1 );
pCex->iPo = 0;
pCex->iFrame = p->iFrame;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 );
pObj = Gia_ManObj( p->pGia, pThis->iObj );
assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsCi(pObj) );
if ( Gia_ObjIsRo(p->pGia, pObj) )
assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 )
Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
}
}
// perform refinement
else
{
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
assert( !pThis->fAdded );
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsAnd(pObj) )
{
Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( pThis->iFrame > 0 )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
}
}
else assert( 0 );
}
// add clauses
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
Vga_ManAddClausesOne( p, pThis );
}
Vec_PtrFree( vTermsUsed );
Vec_PtrFree( vTermsUnused );
return pCex;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.] Synopsis [Collect nodes/flops involved in different timeframes.]
...@@ -439,6 +800,112 @@ void Vec_IntDoubleWidth( Vec_Int_t * p, int nWords ) ...@@ -439,6 +800,112 @@ void Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prints the results.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vta_ManAbsPrint( Vta_Man_t * p, int fThis )
{
Vec_Ptr_t * vInfos;
Vec_Int_t * vPres;
unsigned * pInfo;
int CountAll, CountUni;
int Entry, i, w, f;
// collected used nodes
vInfos = Vec_PtrAlloc( 1000 );
Vec_IntForEachEntry( p->vAbsAll, Entry, i )
{
if ( Entry )
Vec_PtrPush( vInfos, Vta_ObjAbsNew(p, i) );
pInfo = Vta_ObjAbsNew(p, i);
for ( w = 0; w < p->nWords; w++ )
if ( pInfo[w] )
break;
assert( Entry == (int)(w < p->nWords) );
}
printf( "%d", Vec_PtrSize(vInfos) );
// print results for used nodes
vPres = Vec_IntStart( Vec_PtrSize(vInfos) );
for ( f = 0; f <= fThis; f++ )
{
CountAll = CountUni = 0;
Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i )
{
if ( !Gia_InfoHasBit(pInfo, f) )
continue;
CountAll++;
if ( Vec_IntEntry(vPres, i) )
continue;
CountUni++;
Vec_IntWriteEntry( vPres, i, 1 );
}
printf( " %d(%d)", CountAll, CountUni );
}
printf( "\n" );
Vec_PtrFree( vInfos );
Vec_IntFree( vPres );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vga_ManUnroll_rec( Vta_Man_t * p, int iObj, int iFrame )
{
int iVar;
Gia_Obj_t * pObj;
Vta_Obj_t * pThis;
if ( !Gia_InfoHasBit( Vta_ObjAbsOld(p, iObj), iFrame ) )
return;
pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
if ( !pThis->fNew )
return;
pThis->fNew = 0;
iVar = Vta_ObjId( p, pThis );
pObj = Gia_ManObj( p->pGia, iObj );
assert( !Gia_ObjIsCo(pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
Vga_ManUnroll_rec( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( iFrame == 0 )
{
pThis = Vga_ManFindOrAdd( p, iObj, -1 );
assert( pThis->fNew );
pThis->fNew = 0;
}
else
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
}
}
else if ( Gia_ObjIsPi(p->pGia, pObj) )
{}
else if ( Gia_ObjIsConst0(pObj) )
{}
else assert( 0 );
Vec_IntPush( p->vOrder, iVar );
}
/**Function*************************************************************
Synopsis [Collect nodes/flops involved in different timeframes.] Synopsis [Collect nodes/flops involved in different timeframes.]
Description [] Description []
...@@ -452,6 +919,7 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, ...@@ -452,6 +919,7 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax,
{ {
Vta_Man_t * p; Vta_Man_t * p;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Abc_Cex_t * pCex;
Vec_Int_t * vCore; Vec_Int_t * vCore;
Vec_Int_t * vAbs = NULL; Vec_Int_t * vAbs = NULL;
int f, i, iObjPrev, RetValue, Entry; int f, i, iObjPrev, RetValue, Entry;
...@@ -460,8 +928,9 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, ...@@ -460,8 +928,9 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax,
// start the manager // start the manager
p = Vga_ManStart( pAig, vAbs, nFramesMax, nConfMax, nTimeMax, fVerbose ); p = Vga_ManStart( pAig, vAbs, nFramesMax, nConfMax, nTimeMax, fVerbose );
// iteragte though time frames // iteragte though time frames
for ( f = p->nFrames; f < nFramesMax; f++ ) for ( f = 0; f < nFramesMax; f++ )
{ {
p->iFrame = f;
if ( fVerbose ) if ( fVerbose )
printf( "Frame %4d : ", f ); printf( "Frame %4d : ", f );
if ( p->nWords * 32 == f ) if ( p->nWords * 32 == f )
...@@ -469,19 +938,68 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax, ...@@ -469,19 +938,68 @@ void Gia_VtaTest( Gia_Man_t * pAig, int nFramesMax, int nConfMax, int nTimeMax,
Vec_IntDoubleWidth( vAbs, p->nWords ); Vec_IntDoubleWidth( vAbs, p->nWords );
p->nWords *= 2; p->nWords *= 2;
} }
if ( f < p->nFramesS )
{
// unroll and create clauses
iObjPrev = p->nObjs; iObjPrev = p->nObjs;
assert( Gia_InfoHasBit( Vta_ObjAbsOld(p, Gia_ObjFaninId0p(p->pGia, pObj)), f ) );
Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); Vga_ManUnroll_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
Vga_ManAddClauses( p, iObjPrev ); for ( i = iObjPrev; i < p->nObjs; i++ )
Vga_ManAddClausesOne( p, Vta_ManObj(p, i) );
// run SAT solver // run SAT solver
vCore = Vta_ManUnsatCore( p->pSat, nConfMax, fVerbose, &RetValue ); vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue );
if ( vCore == NULL ) if ( vCore == NULL && RetValue == 0 )
pCex = NULL;
}
else
{
// consider the last p->nFramesS/2 cores
// add them for the last time frame
// iterate as long as there are counter-examples
while ( 1 )
{
vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, nConfMax, fVerbose, &RetValue );
if ( vCore != NULL )
{
// unroll the solver, add the core
// return and dobule check
break; break;
}
pCex = Vta_ManRefineAbstraction( p );
if ( pCex != NULL )
break;
}
}
if ( pCex != NULL )
{
// the problem is SAT
}
if ( vCore == NULL )
{
// resource limit is reached
}
// add core to storage // add core to storage
Vec_IntForEachEntry( vCore, Entry, i ) Vec_IntForEachEntry( vCore, Entry, i )
Gia_InfoSetBit( Vta_ObjAbs(p, Vec_IntEntry(p->vCla2Var, Entry)), f ); {
Vec_IntFree( vCore ); Vta_Obj_t * pThis = Vta_ManObj( p, Entry );
unsigned * pInfo = Vta_ObjAbsNew( p, pThis->iObj );
Vec_IntWriteEntry( p->vAbsAll, pThis->iObj, 1 );
Gia_InfoSetBit( pInfo, pThis->iFrame );
} }
vAbs = p->vAbs; p->vAbs = NULL; // Vec_IntFree( vCore );
Vec_PtrPush( p->vCores, vCore );
// print the result
if ( fVerbose )
Vta_ManAbsPrint( p, f );
}
vAbs = p->vAbsNew; p->vAbsNew = NULL;
Vga_ManStop( p ); Vga_ManStop( p );
// print statistics about the core // print statistics about the core
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment