From 066e8d1b173d11aeb837ffda56a8ba1bb7ddb214 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 23 Jan 2018 19:45:17 -0800 Subject: Experiments with SAT-based simulation. --- src/aig/gia/gia.h | 10 ++++ src/aig/gia/giaMan.c | 2 + src/aig/gia/giaSim.c | 113 ++++++++++++++++++++++++++++++++++++++++++-- src/proof/cec/cecSat.c | 19 +++++++- src/sat/satoko/solver_api.c | 8 +++- 5 files changed, 146 insertions(+), 6 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 039628bf..fcdb3941 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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 ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 7d0ef288..bc270168 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -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 ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 192184c8..228f6fb4 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index 0f4bf2bb..1d2ebd1d 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -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 ); diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index adf30cef..79d48c3b 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -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; -- cgit v1.2.3