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

Experiments with SAT-based simulation.

This commit is contained in:
Alan Mishchenko 2018-01-23 19:45:17 -08:00
parent 67e820a5eb
commit 066e8d1b17
5 changed files with 146 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/aig/gia/gia.h
View File

@ -150,6 +150,7 @@ struct Gia_Man_t_
Vec_Ptr_t * vSeqModelVec; // sequential counter-examples
Vec_Int_t vCopies; // intermediate copies
Vec_Int_t vCopies2; // intermediate copies
Vec_Int_t * vVar2Obj; // mapping of variables into objects
Vec_Int_t * vTruths; // used for truth table computation
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
Vec_Int_t * vGateClasses; // classes of gates for abstraction
@ -209,6 +210,11 @@ struct Gia_Man_t_
Vec_Wrd_t * vSimsPi;
Vec_Int_t * vClassOld;
Vec_Int_t * vClassNew;
// incremental simulation
int fIncrSim;
int iNextPi;
int iTimeStamp;
Vec_Int_t * vTimeStamps;
// truth table computation for small functions
int nTtVars; // truth table variables
int nTtWords; // truth table words
@ -1518,6 +1524,10 @@ extern int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0
extern void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 );
extern void Gia_ManBuiltInSimResimulate( Gia_Man_t * p );
extern int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat );
extern void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs );
extern void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits );
extern int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 );
extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
/*=== giaSpeedup.c ============================================================*/
extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );

2
src/aig/gia/giaMan.c
View File

@ -92,6 +92,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vClassOld );
Vec_WrdFreeP( &p->vSims );
Vec_WrdFreeP( &p->vSimsPi );
Vec_IntFreeP( &p->vTimeStamps );
Vec_FltFreeP( &p->vTiming );
Vec_VecFreeP( &p->vClockDoms );
Vec_IntFreeP( &p->vCofVars );
@ -118,6 +119,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vTruths );
Vec_IntErase( &p->vCopies );
Vec_IntErase( &p->vCopies2 );
Vec_IntFreeP( &p->vVar2Obj );
Vec_IntErase( &p->vCopiesTwo );
Vec_IntErase( &p->vSuppVars );
Vec_WrdFreeP( &p->vSuppWords );

113
src/aig/gia/giaSim.c
View File

@ -800,7 +800,7 @@ void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj )
word * pInfo = Gia_ManBuiltInData( p, iObj );
word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) );
assert( p->fBuiltInSim );
assert( p->fBuiltInSim || p->fIncrSim );
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
@ -860,7 +860,7 @@ int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
{
word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
assert( p->fBuiltInSim );
assert( p->fBuiltInSim || p->fIncrSim );
// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
@ -903,7 +903,7 @@ int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
{
word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
assert( p->fBuiltInSim );
assert( p->fBuiltInSim || p->fIncrSim );
// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
@ -1113,6 +1113,113 @@ int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vOb
return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs );
}
/**Function*************************************************************
Synopsis [Bit-parallel simulation during AIG construction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManIncrSimUpdate( Gia_Man_t * p )
{
int i, k;
// extend timestamp info
assert( Vec_IntSize(p->vTimeStamps) <= Gia_ManObjNum(p) );
Vec_IntFillExtra( p->vTimeStamps, Gia_ManObjNum(p), 0 );
// extend simulation info
assert( Vec_WrdSize(p->vSims) <= Gia_ManObjNum(p) * p->nSimWords );
Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p) * p->nSimWords, 0 );
// extend PI info
assert( p->iNextPi <= Gia_ManCiNum(p) );
for ( i = p->iNextPi; i < Gia_ManCiNum(p); i++ )
{
word * pSims = Gia_ManBuiltInData( p, Gia_ManCiIdToId(p, i) );
for ( k = 0; k < p->nSimWords; k++ )
pSims[k] = Gia_ManRandomW(0);
}
p->iNextPi = Gia_ManCiNum(p);
}
void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs )
{
assert( !p->fIncrSim );
p->fIncrSim = 1;
p->iPatsPi = 0;
p->nSimWords = nWords;
// init time stamps
p->iTimeStamp = 1;
p->vTimeStamps = Vec_IntAlloc( p->nSimWords );
// init object sim info
p->iNextPi = 0;
p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
Gia_ManRandomW( 1 );
}
void Gia_ManIncrSimStop( Gia_Man_t * p )
{
assert( p->fIncrSim );
p->fIncrSim = 0;
p->iPatsPi = 0;
p->nSimWords = 0;
p->iTimeStamp = 1;
Vec_IntFreeP( &p->vTimeStamps );
Vec_WrdFreeP( &p->vSims );
}
void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits )
{
int i, iLit;
assert( Vec_IntSize(vObjLits) > 0 );
p->iTimeStamp++;
Vec_IntForEachEntry( vObjLits, iLit, i )
{
word * pSims = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit) );
if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
continue;
//assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 );
//Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) )
Abc_TtXorBit(pSims, p->iPatsPi);
}
p->iPatsPi = (p->iPatsPi == p->nSimWords * 64 - 1) ? 0 : p->iPatsPi + 1;
}
void Gia_ManIncrSimCone_rec( Gia_Man_t * p, int iObj )
{
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
if ( Gia_ObjIsCi(pObj) )
return;
if ( Vec_IntEntry(p->vTimeStamps, iObj) == p->iTimeStamp )
return;
assert( Vec_IntEntry(p->vTimeStamps, iObj) < p->iTimeStamp );
Vec_IntWriteEntry( p->vTimeStamps, iObj, p->iTimeStamp );
assert( Gia_ObjIsAnd(pObj) );
Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
Gia_ManBuiltInSimPerformInt( p, iObj );
}
int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
{
assert( iLit0 > 1 && iLit1 > 1 );
Gia_ManIncrSimUpdate( p );
Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 );
}
int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
{
assert( iLit0 > 1 && iLit1 > 1 );
Gia_ManIncrSimUpdate( p );
Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

19
src/proof/cec/cecSat.c
View File

@ -301,12 +301,19 @@ void Cec2_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
}
void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat )
{
int iVar;
assert( !Gia_IsComplement(pObj) );
assert( !Gia_ObjIsConst0(pObj) );
if ( Cec2_ObjSatId(p, pObj) >= 0 )
return;
assert( Cec2_ObjSatId(p, pObj) == -1 );
Cec2_ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) );
iVar = satoko_add_variable(pSat, 0);
if ( p->vVar2Obj )
{
assert( Vec_IntSize(p->vVar2Obj) == iVar );
Vec_IntPush( p->vVar2Obj, Gia_ObjId(p, pObj) );
}
Cec2_ObjSetSatId( p, pObj, iVar );
if ( Gia_ObjIsAnd(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
@ -322,7 +329,15 @@ int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr
return Cec2_ObjSatId(pGia,pObj);
assert( iObj > 0 );
if ( Gia_ObjIsCi(pObj) )
return Cec2_ObjSetSatId( pGia, pObj, satoko_add_variable(pSat, 0) );
{
int iVar = satoko_add_variable(pSat, 0);
if ( pGia->vVar2Obj )
{
assert( Vec_IntSize(pGia->vVar2Obj) == iVar );
Vec_IntPush( pGia->vVar2Obj, iObj );
}
return Cec2_ObjSetSatId( pGia, pObj, iVar );
}
assert( Gia_ObjIsAnd(pObj) );
// start the frontier
Vec_PtrClear( vFrontier );

8
src/sat/satoko/solver_api.c
View File

@ -281,7 +281,13 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF);
return (s->status = (solver_propagate(s) == UNDEF));
}
if ( 0 ) {
for ( i = 0; i < vec_uint_size(s->temp_lits); i++ ) {
int lit = vec_uint_at(s->temp_lits, i);
printf( "%s%d ", lit&1 ? "!":"", lit>>1 );
}
printf( "\n" );
}
cref = solver_clause_create(s, s->temp_lits, 0);
clause_watch(s, cref);
return SATOKO_OK;