From 486eacc542f193231fd7f116f38e2efab753568c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 25 Apr 2013 15:32:30 -0700 Subject: SAT sweeping under constraints. --- src/proof/ssc/module.make | 5 + src/proof/ssc/ssc.h | 76 ++++++++++++ src/proof/ssc/sscClass.c | 245 ++++++++++++++++++++++++++++++++++++++ src/proof/ssc/sscCore.c | 191 ++++++++++++++++++++++++++++++ src/proof/ssc/sscInt.h | 122 +++++++++++++++++++ src/proof/ssc/sscSat.c | 113 ++++++++++++++++++ src/proof/ssc/sscSim.c | 294 ++++++++++++++++++++++++++++++++++++++++++++++ src/proof/ssc/sscUtil.c | 152 ++++++++++++++++++++++++ 8 files changed, 1198 insertions(+) create mode 100644 src/proof/ssc/module.make create mode 100644 src/proof/ssc/ssc.h create mode 100644 src/proof/ssc/sscClass.c create mode 100644 src/proof/ssc/sscCore.c create mode 100644 src/proof/ssc/sscInt.h create mode 100644 src/proof/ssc/sscSat.c create mode 100644 src/proof/ssc/sscSim.c create mode 100644 src/proof/ssc/sscUtil.c (limited to 'src/proof') diff --git a/src/proof/ssc/module.make b/src/proof/ssc/module.make new file mode 100644 index 00000000..55e845f8 --- /dev/null +++ b/src/proof/ssc/module.make @@ -0,0 +1,5 @@ +SRC += src/proof/ssc/sscClass.c \ + src/proof/ssc/sscCore.c \ + src/proof/ssc/sscSat.c \ + src/proof/ssc/sscSim.c \ + src/proof/ssc/sscUtil.c diff --git a/src/proof/ssc/ssc.h b/src/proof/ssc/ssc.h new file mode 100644 index 00000000..de32ffc1 --- /dev/null +++ b/src/proof/ssc/ssc.h @@ -0,0 +1,76 @@ +/**CFile**************************************************************** + + FileName [ssc.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__ssc__ssc_h +#define ABC__aig__ssc__ssc_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// choicing parameters +typedef struct Ssc_Pars_t_ Ssc_Pars_t; +struct Ssc_Pars_t_ +{ + int nWords; // the number of simulation words + int nBTLimit; // conflict limit at a node + int nSatVarMax; // the max number of SAT variables + int nCallsRecycle; // calls to perform before recycling SAT solver + int fVerbose; // verbose stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== sscCore.c ==========================================================*/ +extern void Ssc_ManSetDefaultParams( Ssc_Pars_t * p ); +extern Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ); +extern Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c new file mode 100644 index 00000000..a6d2b5e3 --- /dev/null +++ b/src/proof/ssc/sscClass.c @@ -0,0 +1,245 @@ +/**CFile**************************************************************** + + FileName [sscClass.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [Equivalence classes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sscInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes hash key of the simuation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ssc_GiaSimHashKey( Gia_Man_t * p, int iObj, int nTableSize ) +{ + static int s_Primes[16] = { + 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, + 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; + word * pSim = Gia_ObjSim( p, iObj ); + unsigned uHash = 0; + int i, nWords = Gia_ObjSimWords(p); + if ( pSim[0] & 1 ) + for ( i = 0; i < nWords; i++ ) + uHash ^= ~pSim[i] * s_Primes[i & 0xf]; + else + for ( i = 0; i < nWords; i++ ) + uHash ^= pSim[i] * s_Primes[i & 0xf]; + return (int)(uHash % nTableSize); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if sim patterns are equal up to the complement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ssc_GiaSimIsConst0( Gia_Man_t * p, int iObj0 ) +{ + int w, nWords = Gia_ObjSimWords(p); + word * pSim = Gia_ObjSim( p, iObj0 ); + if ( pSim[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pSim[w] ) + return 0; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pSim[w] ) + return 0; + } + return 1; +} +static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 ) +{ + int w, nWords = Gia_ObjSimWords(p); + word * pSim0 = Gia_ObjSim( p, iObj0 ); + word * pSim1 = Gia_ObjSim( p, iObj1 ); + if ( (pSim0[0] & 1) != (pSim1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( pSim0[w] != ~pSim1[w] ) + return 0; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pSim0[w] != pSim1[w] ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Refines one equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) +{ + int Repr = GIA_VOID, EntPrev = -1, Ent, i; + assert( Vec_IntSize(vClass) > 0 ); + Vec_IntForEachEntry( vClass, Ent, i ) + { + if ( i == 0 ) + { + Repr = Ent; + Gia_ObjSetRepr( p, Ent, GIA_VOID ); + EntPrev = Ent; + } + else + { + assert( Repr < Ent ); + Gia_ObjSetRepr( p, Ent, Repr ); + Gia_ObjSetNext( p, EntPrev, Ent ); + EntPrev = Ent; + } + } + Gia_ObjSetNext( p, EntPrev, 0 ); +} +int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i ) +{ + Gia_Obj_t * pObj; + int Ent; + Vec_IntClear( p->vClassOld ); + Vec_IntClear( p->vClassNew ); + Vec_IntPush( p->vClassOld, i ); + pObj = Gia_ManObj(p, i); + Gia_ClassForEachObj1( p, i, Ent ) + { + if ( Ssc_GiaSimAreEqual( p, i, Ent ) ) + Vec_IntPush( p->vClassOld, Ent ); + else + Vec_IntPush( p->vClassNew, Ent ); + } + if ( Vec_IntSize( p->vClassNew ) == 0 ) + return 0; + Ssc_GiaSimClassCreate( p, p->vClassOld ); + Ssc_GiaSimClassCreate( p, p->vClassNew ); + if ( Vec_IntSize(p->vClassNew) > 1 ) + return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) ); + return 1; +} +void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined ) +{ + int * pTable, nTableSize, i, k, Key; + if ( Vec_IntSize(vRefined) == 0 ) + return; + nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); + pTable = ABC_CALLOC( int, nTableSize ); + Vec_IntForEachEntry( vRefined, i, k ) + { + assert( !Ssc_GiaSimIsConst0( p, i ) ); + Key = Ssc_GiaSimHashKey( p, i, nTableSize ); + if ( pTable[Key] == 0 ) + { + assert( Gia_ObjRepr(p, i) == 0 ); + assert( Gia_ObjNext(p, i) == 0 ); + Gia_ObjSetRepr( p, i, GIA_VOID ); + } + else + { + Gia_ObjSetNext( p, pTable[Key], i ); + Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) ); + if ( Gia_ObjRepr(p, i) == GIA_VOID ) + Gia_ObjSetRepr( p, i, pTable[Key] ); + assert( Gia_ObjRepr(p, i) > 0 ); + } + pTable[Key] = i; + } + Vec_IntForEachEntry( vRefined, i, k ) + if ( Gia_ObjIsHead( p, i ) ) + Ssc_GiaSimClassRefineOne( p, i ); + ABC_FREE( pTable ); +} + +/**Function************************************************************* + + Synopsis [Refines equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssc_GiaClassesRefine( Gia_Man_t * p ) +{ + Vec_Int_t * vRefinedC; + Gia_Obj_t * pObj; + int i; + if ( p->pReprs == NULL ) + { + assert( p->pReprs == NULL ); + p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID ); + if ( p->vClassOld == NULL ) + p->vClassOld = Vec_IntAlloc( 100 ); + if ( p->vClassNew == NULL ) + p->vClassNew = Vec_IntAlloc( 100 ); + } + vRefinedC = Vec_IntAlloc( 100 ); + Gia_ManForEachCand( p, pObj, i ) + if ( Gia_ObjIsTail(p, i) ) + Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) ); + else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) ) + Vec_IntPush( vRefinedC, i ); + Ssc_GiaSimProcessRefined( p, vRefinedC ); + Vec_IntFree( vRefinedC ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c new file mode 100644 index 00000000..f2cd810a --- /dev/null +++ b/src/proof/ssc/sscCore.c @@ -0,0 +1,191 @@ +/**CFile**************************************************************** + + FileName [sscCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [The core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sscInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_ManSetDefaultParams( Ssc_Pars_t * p ) +{ + memset( p, 0, sizeof(Ssc_Pars_t) ); + p->nWords = 4; // the number of simulation words + p->nBTLimit = 1000; // conflict limit at a node + p->nSatVarMax = 5000; // the max number of SAT variables + p->nCallsRecycle = 100; // calls to perform before recycling SAT solver + p->fVerbose = 0; // verbose stats +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_ManStop( Ssc_Man_t * p ) +{ + if ( p->pSat ) + sat_solver_delete( p->pSat ); + Vec_IntFreeP( &p->vSatVars ); + Gia_ManStopP( &p->pFraig ); + Vec_IntFreeP( &p->vPivot ); + ABC_FREE( p ); +} +Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) +{ + Ssc_Man_t * p; + p = ABC_CALLOC( Ssc_Man_t, 1 ); + p->pPars = pPars; + p->pAig = pAig; + p->pCare = pCare; + p->pFraig = Gia_ManDup( p->pCare ); + Gia_ManInvertPos( p->pFraig ); + Ssc_ManStartSolver( p ); + if ( p->pSat == NULL ) + { + printf( "Constraints are UNSAT after propagation.\n" ); + Ssc_ManStop( p ); + return NULL; + } + p->vPivot = Ssc_GiaFindPivotSim( p->pFraig ); +// Vec_IntFreeP( &p->vPivot ); + if ( p->vPivot == NULL ) + p->vPivot = Ssc_ManFindPivotSat( p ); + if ( p->vPivot == NULL ) + { + printf( "Constraints are UNSAT or conflict limit is too low.\n" ); + Ssc_ManStop( p ); + return NULL; + } + Vec_IntPrint( p->vPivot ); + return p; +} + +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) +{ + Ssc_Man_t * p; + Gia_Man_t * pResult; + clock_t clk, clkTotal = clock(); + int i; + assert( Gia_ManRegNum(pCare) == 0 ); + assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) ); + assert( Gia_ManIsNormalized(pAig) ); + assert( Gia_ManIsNormalized(pCare) ); + // reset random numbers + Gia_ManRandom( 1 ); + // sweeping manager + p = Ssc_ManStart( pAig, pCare, pPars ); + if ( p == NULL ) + return Gia_ManDup( pAig ); + // perform simulation +clk = clock(); + for ( i = 0; i < 16; i++ ) + { + Ssc_GiaRandomPiPattern( pAig, 10, NULL ); + Ssc_GiaSimRound( pAig ); + Ssc_GiaClassesRefine( pAig ); + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + } +p->timeSimInit += clock() - clk; + // remember the resulting AIG + pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 ); + if ( pResult == NULL ) + { + printf( "There is no equivalences.\n" ); + pResult = Gia_ManDup( pAig ); + } + Ssc_ManStop( p ); + // count the number of representatives + if ( pPars->fVerbose ) + { + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d. ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + } + return pResult; +} +Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) +{ + Gia_Man_t * pAig, * pCare, * pResult; + int i; + if ( p->nConstrs == 0 ) + { + pAig = Gia_ManDup( p ); + pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 ); + pCare->pName = Abc_UtilStrsav( "care" ); + for ( i = 0; i < Gia_ManPiNum(p); i++ ) + Gia_ManAppendCi( pCare ); + Gia_ManAppendCo( pCare, 1 ); + } + else + { + Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) ); + pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 ); + pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 ); + Vec_IntFree( vOuts ); + } + pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); + Gia_ManStop( pAig ); + Gia_ManStop( pCare ); + return pResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h new file mode 100644 index 00000000..21f5afc2 --- /dev/null +++ b/src/proof/ssc/sscInt.h @@ -0,0 +1,122 @@ +/**CFile**************************************************************** + + FileName [sscInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Choice computation for tech-mapping.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__ssc__sscInt_h +#define ABC__aig__ssc__sscInt_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig/gia/gia.h" +#include "sat/bsat/satSolver.h" +#include "ssc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// choicing manager +typedef struct Ssc_Man_t_ Ssc_Man_t; +struct Ssc_Man_t_ +{ + // parameters + Ssc_Pars_t * pPars; // choicing parameters + Gia_Man_t * pAig; // subject AIG + Gia_Man_t * pCare; // care set AIG + Gia_Man_t * pFraig; // resulting AIG + Vec_Int_t * vPivot; // one SAT pattern + // SAT solving + sat_solver * pSat; // recyclable SAT solver + Vec_Int_t * vSatVars; // mapping of each node into its SAT var + Vec_Int_t * vUsedNodes; // nodes whose SAT vars are assigned + int nRecycles; // the number of times SAT solver was recycled + int nCallsSince; // the number of calls since the last recycle + Vec_Int_t * vFanins; // fanins of the CNF node + // SAT calls statistics + int nSatCalls; // the number of SAT calls + int nSatProof; // the number of proofs + int nSatFailsReal; // the number of timeouts + int nSatCallsUnsat; // the number of unsat SAT calls + int nSatCallsSat; // the number of sat SAT calls + // runtime stats + clock_t timeSimInit; // simulation and class computation + clock_t timeSimSat; // simulation of the counter-examples + clock_t timeSat; // solving SAT + clock_t timeSatSat; // sat + clock_t timeSatUnsat; // unsat + clock_t timeSatUndec; // undecided + clock_t timeChoice; // choice computation + clock_t timeOther; // other runtime + clock_t timeTotal; // total runtime +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Ssc_ObjSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj)); } +static inline void Ssc_ObjSetSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj, int Num ) { Vec_IntWriteEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj), Num); } + +static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; } +static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== sscClass.c =================================================*/ +extern int Ssc_GiaClassesRefine( Gia_Man_t * p ); +/*=== sscCnf.c ===================================================*/ +extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj ); +/*=== sscCore.c ==================================================*/ +/*=== sscSat.c ===================================================*/ +extern int Ssc_NodesAreEquiv( Ssc_Man_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); +extern void Ssc_ManSatSolverRecycle( Ssc_Man_t * p ); +extern void Ssc_ManStartSolver( Ssc_Man_t * p ); +extern Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p ); +/*=== sscSim.c ===================================================*/ +extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot ); +extern void Ssc_GiaSimRound( Gia_Man_t * p ); +extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ); +/*=== sscUtil.c ===================================================*/ +extern Gia_Man_t * Ssc_GenerateOneHot( int nVars ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c new file mode 100644 index 00000000..1519b89e --- /dev/null +++ b/src/proof/ssc/sscSat.c @@ -0,0 +1,113 @@ +/**CFile**************************************************************** + + FileName [sscSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [SAT procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sscInt.h" +#include "sat/cnf/cnf.h" +#include "aig/gia/giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the SAT solver for constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_ManStartSolver( Ssc_Man_t * p ) +{ + Aig_Man_t * pAig = Gia_ManToAig( p->pFraig, 0 ); + Cnf_Dat_t * pDat = Cnf_Derive( pAig, 0 ); + sat_solver * pSat; + int i, status; + assert( p->pSat == NULL && p->vSatVars == NULL ); + assert( Aig_ManObjNumMax(pAig) == Gia_ManObjNum(p->pFraig) ); + Aig_ManStop( pAig ); +//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL ); + // save variable mapping + p->vSatVars = Vec_IntAllocArray( pDat->pVarNums, Gia_ManObjNum(p->pFraig) ); pDat->pVarNums = NULL; + // start the SAT solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pDat->nVars + 1000 ); + for ( i = 0; i < pDat->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) ) + { + Cnf_DataFree( pDat ); + sat_solver_delete( pSat ); + return; + } + } + Cnf_DataFree( pDat ); + status = sat_solver_simplify( pSat ); + if ( status == 0 ) + { + sat_solver_delete( pSat ); + return; + } + p->pSat = pSat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p ) +{ + Vec_Int_t * vInit; + Gia_Obj_t * pObj; + int i, status; + status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 ); + if ( status != l_True ) // unsat or undec + return NULL; + vInit = Vec_IntAlloc( Gia_ManPiNum(p->pFraig) ); + Gia_ManForEachPi( p->pFraig, pObj, i ) + Vec_IntPush( vInit, sat_solver_var_value(p->pSat, Ssc_ObjSatNum(p, pObj)) ); + return vInit; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c new file mode 100644 index 00000000..86837000 --- /dev/null +++ b/src/proof/ssc/sscSim.c @@ -0,0 +1,294 @@ +/**CFile**************************************************************** + + FileName [sscSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [Simulation procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sscInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline word Ssc_Random() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 0); } +static inline word Ssc_Random1( int Bit ) { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 1) | (word)Bit; } +static inline word Ssc_Random2() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 2) | (word)2; } + +static inline void Ssc_SimAnd( word * pSim, word * pSim0, word * pSim1, int nWords, int fComp0, int fComp1 ) +{ + int w; + if ( fComp0 && fComp1 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] = ~(pSim0[w] | pSim1[w]); + else if ( fComp0 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] = ~pSim0[w] & pSim1[w]; + else if ( fComp1 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] = pSim0[w] & ~pSim1[w]; + else + for ( w = 0; w < nWords; w++ ) + pSim[w] = pSim0[w] & pSim1[w]; +} + +static inline void Ssc_SimDup( word * pSim, word * pSim0, int nWords, int fComp0 ) +{ + int w; + if ( fComp0 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] = ~pSim0[w]; + else + for ( w = 0; w < nWords; w++ ) + pSim[w] = pSim0[w]; +} + +static inline void Ssc_SimConst( word * pSim, int nWords, int fComp0 ) +{ + int w; + if ( fComp0 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] = ~(word)0; + else + for ( w = 0; w < nWords; w++ ) + pSim[w] = 0; +} + +static inline void Ssc_SimOr( word * pSim, word * pSim0, int nWords, int fComp0 ) +{ + int w; + if ( fComp0 ) + for ( w = 0; w < nWords; w++ ) + pSim[w] |= ~pSim0[w]; + else + for ( w = 0; w < nWords; w++ ) + pSim[w] |= pSim0[w]; +} + +static inline int Ssc_SimFindBitWord( word t ) +{ + int n = 0; + if ( t == 0 ) return -1; + if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; } + if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; } + if ( (t & 0x00000000000000FF) == 0 ) { n += 8; t >>= 8; } + if ( (t & 0x000000000000000F) == 0 ) { n += 4; t >>= 4; } + if ( (t & 0x0000000000000003) == 0 ) { n += 2; t >>= 2; } + if ( (t & 0x0000000000000001) == 0 ) { n++; } + return n; +} +static inline int Ssc_SimFindBit( word * pSim, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pSim[w] ) + return 64*w + Ssc_SimFindBitWord(pSim[w]); + return -1; +} + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Vec_WrdDoubleSimInfo( Vec_Wrd_t * p, int nObjs ) +{ + word * pArray = ABC_CALLOC( word, 2 * Vec_WrdSize(p) ); + int i, nWords = Vec_WrdSize(p) / nObjs; + assert( Vec_WrdSize(p) % nObjs == 0 ); + for ( i = 0; i < nObjs; i++ ) + memcpy( pArray + 2*i*nWords, p->pArray + i*nWords, sizeof(word) * nWords ); + ABC_FREE( p->pArray ); p->pArray = pArray; + p->nSize = p->nCap = 2*nWords*nObjs; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords ) +{ + p->iPatsPi = 0; + if ( p->vSimsPi == NULL ) + p->vSimsPi = Vec_WrdStart(0); + Vec_WrdFill( p->vSimsPi, nWords * Gia_ManPiNum(p), 0 ); + assert( nWords == Gia_ObjSimWords( p ) ); +} +void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot ) +{ + word * pSimPi; + int i, w; + Ssc_GiaResetPiPattern( p, nWords ); + pSimPi = Gia_ObjSimPi( p, 0 ); + for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += nWords ) + { + pSimPi[0] = vPivot ? Ssc_Random1(Vec_IntEntry(vPivot, i)) : Ssc_Random2(); + for ( w = 1; w < nWords; w++ ) + pSimPi[w] = Ssc_Random(); +// if ( i < 10 ) +// Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" ); + } +} +void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat ) +{ + word * pSimPi; + int i; + assert( Vec_IntSize(vPat) == Gia_ManPiNum(p) ); + if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) ) + Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManPiNum(p) ); + assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) ); + pSimPi = Gia_ObjSimPi( p, 0 ); + for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += Gia_ObjSimWords(p) ) + if ( Vec_IntEntry(vPat, i) ) + Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi ); + p->iPatsPi++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssc_GiaResetSimInfo( Gia_Man_t * p ) +{ + assert( Vec_WrdSize(p->vSimsPi) % Gia_ManPiNum(p) == 0 ); + if ( p->vSims == NULL ) + p->vSims = Vec_WrdAlloc(0); + Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 ); +} +void Ssc_GiaSimRound( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + word * pSim, * pSim0, * pSim1; + int i, nWords = Gia_ObjSimWords(p); + Ssc_GiaResetSimInfo( p ); + assert( nWords == Vec_WrdSize(p->vSims) / Gia_ManObjNum(p) ); + // constant node + Ssc_SimConst( Gia_ObjSim(p, 0), nWords, 0 ); + // primary inputs + pSim = Gia_ObjSim( p, 1 ); + pSim0 = Gia_ObjSimPi( p, 0 ); + Gia_ManForEachPi( p, pObj, i ) + { + assert( pSim == Gia_ObjSimObj( p, pObj ) ); + Ssc_SimDup( pSim, pSim0, nWords, 0 ); + pSim += nWords; + pSim0 += nWords; + } + // intermediate nodes + pSim = Gia_ObjSim( p, 1+Gia_ManPiNum(p) ); + Gia_ManForEachAnd( p, pObj, i ) + { + assert( pSim == Gia_ObjSim( p, i ) ); + pSim0 = pSim - pObj->iDiff0 * nWords; + pSim1 = pSim - pObj->iDiff1 * nWords; + Ssc_SimAnd( pSim, pSim0, pSim1, nWords, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) ); + pSim += nWords; + } + // primary outputs + pSim = Gia_ObjSim( p, Gia_ManObjNum(p) - Gia_ManPoNum(p) ); + Gia_ManForEachPo( p, pObj, i ) + { + assert( pSim == Gia_ObjSimObj( p, pObj ) ); + pSim0 = pSim - pObj->iDiff0 * nWords; + Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) ); + pSim += nWords; + } +} + +/**Function************************************************************* + + Synopsis [Returns one SAT assignment of the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) +{ + Vec_Int_t * vInit; + Gia_Obj_t * pObj; + int i, iBit, nWords = Gia_ObjSimWords( p ); + word * pRes = ABC_FALLOC( word, nWords ); + Gia_ManForEachPo( p, pObj, i ) + Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 ); + iBit = Ssc_SimFindBit( pRes, nWords ); + ABC_FREE( pRes ); + if ( iBit == -1 ) + return NULL; + vInit = Vec_IntAlloc( 100 ); + Gia_ManForEachPi( p, pObj, i ) + Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) ); + return vInit; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) +{ + Vec_Int_t * vInit; + Ssc_GiaRandomPiPattern( p, 1, NULL ); + Ssc_GiaSimRound( p ); + vInit = Ssc_GiaGetOneSim( p ); + return vInit; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c new file mode 100644 index 00000000..a96503d0 --- /dev/null +++ b/src/proof/ssc/sscUtil.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [sscUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sweeping under constraints.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 29, 2008.] + + Revision [$Id: sscUtil.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sscInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Hsh_Obj_t_ Hsh_Obj_t; +struct Hsh_Obj_t_ +{ + int iThis; + int iNext; +}; + +typedef struct Hsh_Man_t_ Hsh_Man_t; +struct Hsh_Man_t_ +{ + unsigned * pData; // user's data + int * pTable; // hash table + Hsh_Obj_t * pObjs; + int nObjs; + int nSize; + int nTableSize; +}; + +static inline int * Hsh_ObjData( Hsh_Man_t * p, int iThis ) { return p->pData + p->nSize * iThis; } +static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return iObj == -1 ? NULL : p->pObjs + iObj; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize ) +{ + Hsh_Man_t * p; + p = ABC_CALLOC( Hsh_Man_t, 1 ); + p->pData = pData; + p->nSize = nSize; + p->nTableSize = Abc_PrimeCudd( nDatas ); + p->pTable = ABC_FALLOC( int, p->nTableSize ); + p->pObjs = ABC_FALLOC( Hsh_Obj_t, p->nTableSize ); + return p; +} +void Hsh_ManStop( Hsh_Man_t * p ) +{ + ABC_FREE( p->pObjs ); + ABC_FREE( p->pTable ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize ) +{ + static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457}; + unsigned char * pDataC = (unsigned char *)pData; + int c, nChars = nSize * 4, Key = 0; + for ( c = 0; c < nChars; c++ ) + Key += pDataC[c] * s_BigPrimes[c % 7]; + return Key % nTableSize; +} +int Hsh_ManAdd( Hsh_Man_t * p, int iThis ) +{ + Hsh_Obj_t * pObj; + int * pThis = Hsh_ObjData( p, iThis ); + int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize ); + for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) ) + if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(int) * p->nSize ) ) + return pObj - p->pObjs; + assert( p->nObjs < p->nTableSize ); + pObj = p->pObjs + p->nObjs; + pObj->iThis = iThis; + return (*pPlace = p->nObjs++); +} + +/**Function************************************************************* + + Synopsis [Hashes data by value.] + + Description [Array of 'nTotal' int entries, each of size 'nSize' ints, + is hashed and the resulting unique numbers is returned in the array.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Hsh_ManHashData( int * pData, int nDatas, int nSize, int nInts ) +{ + Vec_Int_t * vRes; + Hsh_Man_t * p; + int i; + assert( nDatas * nSize == nInts ); + p = Hsh_ManStart( pData, nDatas, nSize ); + vRes = Vec_IntAlloc( 1000 ); + for ( i = 0; i < nDatas; i++ ) + Vec_IntPush( vRes, Hsh_ManAdd(p, i) ); + Hsh_ManStop( p ); + return vRes; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3