diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | abcexe.dsp | 4 | ||||
-rw-r--r-- | abclib.dsp | 32 | ||||
-rw-r--r-- | src/aig/gia/gia.h | 21 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 85 | ||||
-rw-r--r-- | src/aig/gia/giaHash.c | 31 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaSweeper.c | 169 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 9 | ||||
-rw-r--r-- | src/base/abci/abc.c | 79 | ||||
-rw-r--r-- | src/proof/ssc/module.make | 5 | ||||
-rw-r--r-- | src/proof/ssc/ssc.h | 76 | ||||
-rw-r--r-- | src/proof/ssc/sscClass.c | 245 | ||||
-rw-r--r-- | src/proof/ssc/sscCore.c | 191 | ||||
-rw-r--r-- | src/proof/ssc/sscInt.h | 122 | ||||
-rw-r--r-- | src/proof/ssc/sscSat.c | 113 | ||||
-rw-r--r-- | src/proof/ssc/sscSim.c | 294 | ||||
-rw-r--r-- | src/proof/ssc/sscUtil.c | 152 |
18 files changed, 1461 insertions, 173 deletions
@@ -23,7 +23,7 @@ MODULES := \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \ src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \ src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ - src/proof/abs \ + src/proof/abs src/proof/ssc \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ src/aig/miniaig \ src/python @@ -89,6 +89,10 @@ LINK32=link.exe SOURCE=.\src\base\main\main.c # End Source File +# Begin Source File + +SOURCE=.\src\sat\bsat\satSolver.c +# End Source File # End Group # Begin Group "Header Files" @@ -4522,6 +4522,38 @@ SOURCE=.\src\proof\abs\absUtil.c SOURCE=.\src\proof\abs\absVta.c # End Source File # End Group +# Begin Group "ssc" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\proof\ssc\ssc.h +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscClass.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscInt.h +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscSat.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\ssc\sscUtil.c +# End Source File +# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 737f6a67..6dad5eb5 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -167,6 +167,12 @@ struct Gia_Man_t_ int iData2; // various user data int nAnd2Delay; // AND2 delay scaled to match delay numbers used int fVerbose; // verbose reports + // bit-parallel simulation + int iPatsPi; + Vec_Wrd_t * vSims; + Vec_Wrd_t * vSimsPi; + Vec_Int_t * vClassOld; + Vec_Int_t * vClassNew; // truth table computation for small functions int nTtVars; // truth table variables int nTtWords; // truth table words @@ -379,7 +385,7 @@ static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } -static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } +static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); } @@ -423,6 +429,11 @@ static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); } +static inline int Gia_ObjSimWords( Gia_Man_t * p ) { return Vec_WrdSize( p->vSimsPi ) / Gia_ManPiNum( p ); } +static inline word * Gia_ObjSimPi( Gia_Man_t * p, int PiId ) { return Vec_WrdEntryP( p->vSimsPi, PiId * Gia_ObjSimWords(p) ); } +static inline word * Gia_ObjSim( Gia_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vSims, Id * Gia_ObjSimWords(p) ); } +static inline word * Gia_ObjSimObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjSim( p, Gia_ObjId(p, pObj) ); } + // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p ) @@ -755,6 +766,8 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else +#define Gia_ManForEachCand( p, pObj, i ) \ + for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsCand(pObj) ) {} else #define Gia_ManForEachAndReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ @@ -837,6 +850,7 @@ extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); +extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); @@ -859,6 +873,7 @@ extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); +extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); @@ -921,6 +936,7 @@ extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ); extern void Gia_ManHashProfile( Gia_Man_t * p ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); +extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ); /*=== giaIf.c ===========================================================*/ extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); @@ -1015,7 +1031,7 @@ extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, i extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ); extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime ); extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc ); -extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ); +extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); @@ -1075,6 +1091,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManPrint( Gia_Man_t * p ); extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); +extern void Gia_ManInvertPos( Gia_Man_t * pAig ); extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 ); extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 74867eff..78aac33c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -577,7 +577,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) if ( pNew->nRegs > 0 ) pNew->nRegs = 0; if ( pNew->pHTable == NULL ) - Gia_ManHashAlloc( pNew ); + Gia_ManHashStart( pNew ); Gia_ManConst0(pTwo)->Value = 0; Gia_ManForEachObj1( pTwo, pObj, i ) { @@ -589,19 +589,24 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } } - - -/**Function************************************************************* - - Synopsis [Append second AIG on top of the first with the permutation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ +void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo ) +{ + Gia_Obj_t * pObj; + int i; + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) ); + if ( pNew->pHTable == NULL ) + Gia_ManHashStart( pNew ); + Gia_ManConst0(pTwo)->Value = 0; + Gia_ManForEachObj1( pTwo, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } +} Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) { Gia_Man_t * pNew; @@ -2185,6 +2190,58 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) } +/**Function************************************************************* + + Synopsis [Generates AIG representing 1-hot condition for N inputs.] + + Description [The condition is true of all POs are 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManOneHot( int nSkips, int nVars ) +{ + Gia_Man_t * p; + int i, b, Shift, iGiaLit, nLogVars = Abc_Base2Log( nVars ); + int * pTemp = ABC_CALLOC( int, (1 << nLogVars) ); + p = Gia_ManStart( nSkips + 4 * nVars + 1 ); + p->pName = Abc_UtilStrsav( "onehot" ); + for ( i = 0; i < nSkips; i++ ) + Gia_ManAppendCi( p ); + for ( i = 0; i < nVars; i++ ) + pTemp[i] = Gia_ManAppendCi( p ); + Gia_ManHashStart( p ); + for ( b = 0; b < nLogVars; b++ ) + for ( i = 0, Shift = (1<<b); i < (1 << nLogVars); i += 2*Shift ) + { + iGiaLit = Gia_ManHashAnd( p, pTemp[i], pTemp[i + Shift] ); + if ( iGiaLit ) + Gia_ManAppendCo( p, iGiaLit ); + pTemp[i] = Gia_ManHashOr( p, pTemp[i], pTemp[i + Shift] ); + } + Gia_ManHashStop( p ); + Gia_ManAppendCo( p, Abc_LitNot(pTemp[0]) ); + ABC_FREE( pTemp ); + assert( Gia_ManObjNum(p) <= nSkips + 4 * nVars + 1 ); + return p; +} +Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ) +{ + Gia_Man_t * pOneHot, * pNew = Gia_ManDup( p ); + if ( Gia_ManRegNum(pNew) == 0 ) + { + Abc_Print( 0, "Appending 1-hotness constraints to the PIs.\n" ); + pOneHot = Gia_ManOneHot( 0, Gia_ManCiNum(pNew) ); + } + else + pOneHot = Gia_ManOneHot( Gia_ManPiNum(pNew), Gia_ManRegNum(pNew) ); + Gia_ManDupAppendShare( pNew, pOneHot ); + pNew->nConstrs += Gia_ManPoNum(pOneHot); + Gia_ManStop( pOneHot ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 4ae01f06..81980b40 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -625,6 +625,37 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) } +/**Function************************************************************* + + Synopsis [Creates well-balanced AND gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ) +{ + if ( Vec_IntSize(vLits) == 0 ) + return 0; + while ( Vec_IntSize(vLits) > 1 ) + { + int i, k = 0, Lit1, Lit2, LitRes; + Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i ) + { + LitRes = Gia_ManHashAnd( p, Lit1, Lit2 ); + Vec_IntWriteEntry( vLits, k++, LitRes ); + } + if ( Vec_IntSize(vLits) & 1 ) + Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) ); + Vec_IntShrink( vLits, k ); + } + assert( Vec_IntSize(vLits) == 1 ); + return Vec_IntEntry(vLits, 0); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 732a5075..75a0f801 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -77,6 +77,10 @@ void Gia_ManStop( Gia_Man_t * p ) assert( p->pManTime == NULL ); Vec_PtrFreeFree( p->vNamesIn ); Vec_PtrFreeFree( p->vNamesOut ); + Vec_IntFreeP( &p->vClassNew ); + Vec_IntFreeP( &p->vClassOld ); + Vec_WrdFreeP( &p->vSims ); + Vec_WrdFreeP( &p->vSimsPi ); Vec_FltFreeP( &p->vTiming ); Vec_VecFreeP( &p->vClockDoms ); Vec_IntFreeP( &p->vLutConfigs ); diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 844c3e45..3f597982 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -21,6 +21,7 @@ #include "gia.h" #include "base/main/main.h" #include "sat/bsat/satSolver.h" +#include "proof/ssc/ssc.h" ABC_NAMESPACE_IMPL_START @@ -965,62 +966,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_SweeperGen64Patterns( Gia_Man_t * pGiaCond, Vec_Wrd_t * vSim ) -{ - Vec_Int_t * vCex; - int i, k; - for ( i = 0; i < 64; i++ ) - { - if ( Gia_SweeperCondCheckUnsat( pGiaCond ) != 0 ) - return 0; - vCex = Gia_SweeperGetCex( pGiaCond ); - for ( k = 0; k < Gia_ManPiNum(pGiaCond); k++ ) - { - if ( Vec_IntEntry(vCex, k) ) - Abc_InfoXorBit( (unsigned *)Vec_WrdEntryP(vSim, i), k ); - printf( "%d", Vec_IntEntry(vCex, k) ); - } - printf( "\n" ); - } - return 1; -} -int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) -{ - Gia_Obj_t * pObj; - word Sim, Sim0, Sim1; - int i, Count = 0; - assert( Vec_WrdEntry(vSim, 0) == 0 ); -// assert( Vec_WrdEntry(vSim, 1) != 0 ); // may not hold - Gia_ManForEachAnd( p, pObj, i ) - { - Sim0 = Vec_WrdEntry( vSim, Gia_ObjFaninId0p( p, pObj ) ); - Sim1 = Vec_WrdEntry( vSim, Gia_ObjFaninId1p( p, pObj ) ); - Sim = (Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0) & (Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1); - Vec_WrdWriteEntry( vSim, i, Sim ); - if ( pObj->fMark0 == 1 ) // considered - continue; - if ( pObj->fMark1 == 1 ) // non-constant - continue; - if ( (pObj->fPhase ? ~Sim : Sim) != 0 ) - { - pObj->fMark1 = 1; - Count++; - } - } - return Count; -} - -/**Function************************************************************* - Synopsis [Performs conditional sweeping of the cone.] Description [Returns the result as a new GIA manager with as many inputs @@ -1031,16 +976,15 @@ int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) SeeAlso [] ***********************************************************************/ -void Gia_SweeperSweepInt( Gia_Man_t * pGiaCond, Gia_Man_t * pGiaOuts, Vec_Wrd_t * vSim ) -{ -} -Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) +Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerbose ) { - Gia_Man_t * pGiaCond, * pGiaOuts; Vec_Int_t * vProbeConds; - Vec_Wrd_t * vSim; - Gia_Obj_t * pObj; - int i, Count; + Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes; + Ssc_Pars_t Pars, * pPars = &Pars; + Ssc_ManSetDefaultParams( pPars ); + pPars->nWords = nWords; + pPars->nBTLimit = nConfs; + pPars->fVerbose = fVerbose; // sweeper is running assert( Gia_SweeperIsRunning(p) ); // extract conditions and logic cones @@ -1048,22 +992,11 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); Gia_ManSetPhase( pGiaOuts ); - // start the sweeper for the conditions - Gia_SweeperStart( pGiaCond ); - Gia_ManForEachPo( pGiaCond, pObj, i ) - Gia_SweeperCondPush( pGiaCond, Gia_SweeperProbeCreate(pGiaCond, Gia_ObjFaninLit0p(pGiaCond, pObj)) ); - // generate 64 patterns that satisfy the conditions - vSim = Vec_WrdStart( Gia_ManObjNum(pGiaOuts) ); - Gia_SweeperGen64Patterns( pGiaCond, vSim ); - Count = Gia_SweeperSimulate( pGiaOuts, vSim ); - printf( "Disproved %d nodes.\n", Count ); - - // consider the remaining ones -// Gia_SweeperSweepInt( pGiaCond, pGiaOuts, vSim ); - Vec_WrdFree( vSim ); + // perform sweeping under constraints + pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars ); + Gia_ManStop( pGiaCond ); Gia_ManStop( pGiaOuts ); - Gia_SweeperStop( pGiaCond ); - return pGiaCond; + return pGiaRes; } /**Function************************************************************* @@ -1085,14 +1018,14 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ) +Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose ) { Gia_Man_t * pNew; Vec_Int_t * vLits; // sweeper is running assert( Gia_SweeperIsRunning(p) ); // sweep the logic - pNew = Gia_SweeperSweep( p, vProbeIds ); + pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerbose ); // execute command line if ( pCommLime ) { @@ -1110,37 +1043,6 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) -{ - if ( Vec_IntSize(vLits) == 0 ) - return 0; - while ( Vec_IntSize(vLits) > 1 ) - { - int i, k = 0, Lit1, Lit2, LitRes; - Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i ) - { - LitRes = Gia_ManHashAnd( p, Lit1, Lit2 ); - Vec_IntWriteEntry( vLits, k++, LitRes ); - } - if ( Vec_IntSize(vLits) & 1 ) - Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) ); - Vec_IntShrink( vLits, k ); - } - assert( Vec_IntSize(vLits) == 1 ); - return Vec_IntEntry(vLits, 0); -} - -/**Function************************************************************* - Synopsis [Sweeper sweeper test.] Description [] @@ -1150,43 +1052,30 @@ int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ) +Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose ) { - Gia_Man_t * pGia; + Gia_Man_t * p, * pGia; Gia_Obj_t * pObj; - Vec_Int_t * vLits, * vOuts; - int i, k, Lit; - + Vec_Int_t * vOuts; + int i; + // add one-hotness constraints + p = Gia_ManDupOneHot( pInit ); // create sweeper Gia_SweeperStart( p ); - - // create 1-hot constraint - vLits = Vec_IntAlloc( 1000 ); - for ( i = 0; i < Gia_ManPiNum(p); i++ ) - for ( k = i+1; k < Gia_ManPiNum(p); k++ ) - { - int Lit0 = Gia_Obj2Lit(p, Gia_ManPi(p, i)); - int Lit1 = Gia_Obj2Lit(p, Gia_ManPi(p, k)); - Vec_IntPush( vLits, Abc_LitNot(Gia_ManHashAnd(p, Lit0, Lit1)) ); - } - Lit = 0; - for ( i = 0; i < Gia_ManPiNum(p); i++ ) - Lit = Gia_ManHashOr( p, Lit, Gia_Obj2Lit(p, Gia_ManPi(p, i)) ); - Vec_IntPush( vLits, Lit ); - Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ManCreateAndGate( p, vLits ) ) ); - Vec_IntFree( vLits ); -//Gia_ManPrint( p ); - - // create outputs + // collect outputs and create conditions vOuts = Vec_IntAlloc( Gia_ManPoNum(p) ); Gia_ManForEachPo( p, pObj, i ) - Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); - + if ( i < Gia_ManPoNum(p) - p->nConstrs ) // this is the user's output + Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); + else // this is a constraint + Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); // perform the sweeping - pGia = Gia_SweeperSweep( p, vOuts ); + pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose ); +// pGia = Gia_ManDup( p ); Vec_IntFree( vOuts ); - + // sop the sweeper Gia_SweeperStop( p ); + Gia_ManStop( p ); return pGia; } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5adf9ebd..6f4389a8 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1163,10 +1163,15 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig ) if ( Gia_ManConstrNum(pAig) == 0 ) return; Gia_ManForEachPo( pAig, pObj, i ) - { if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) ) Gia_ObjFlipFaninC0( pObj ); - } +} +void Gia_ManInvertPos( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFlipFaninC0( pObj ); } /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index af1c8ecf..533db448 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51,6 +51,7 @@ #include "base/cmd/cmd.h" #include "proof/abs/abs.h" #include "sat/bmc/bmc.h" +#include "proof/ssc/ssc.h" #ifndef _WIN32 #include <unistd.h> @@ -321,6 +322,7 @@ static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Add1Hot ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -817,6 +819,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&show", Abc_CommandAbc9Show, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Hash, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&add1hot", Abc_CommandAbc9Add1Hot, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); @@ -24543,6 +24546,52 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Add1Hot( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp; + int c, fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Add1Hot(): There is no AIG.\n" ); + return 1; + } + pTemp = Gia_ManDupOneHot( pAbc->pGia ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &add1hot [-vh]\n" ); + Abc_Print( -2, "\t adds 1-hotness constraints as additional primary outputs\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; @@ -27081,12 +27130,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); Gia_Man_t * pTemp; int c; - int nWords = 1; - int nConfs = 0; - int fVerbose = 0; + Ssc_Pars_t Pars, * pPars = &Pars; + Ssc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF ) { @@ -27098,9 +27145,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); goto usage; } - nWords = atoi(argv[globalUtilOptind]); + pPars->nWords = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nWords < 0 ) + if ( pPars->nWords < 0 ) goto usage; break; case 'C': @@ -27109,13 +27156,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nConfs = atoi(argv[globalUtilOptind]); + pPars->nBTLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nConfs < 0 ) + if ( pPars->nBTLimit < 0 ) goto usage; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; default: goto usage; @@ -27126,16 +27173,17 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" ); return 1; } - pTemp = Gia_SweeperFraigTest( pAbc->pGia, nWords, nConfs, fVerbose ); + Abc_Print( 0, "Current AIG contains %d constraints.\n", pAbc->pGia->nConstrs ); + pTemp = Ssc_PerformSweepingConstr( pAbc->pGia, pPars ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" ); - Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", nWords ); - Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfs ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -31438,7 +31486,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) { -// Gia_Man_t * pTemp = NULL; + Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; int fSwitch = 0; // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); @@ -31451,6 +31499,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Unr_ManTest( Gia_Man_t * pGia ); // extern void Mig_ManTest( Gia_Man_t * pGia ); // extern int Gia_ManVerify( Gia_Man_t * pGia ); + extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -31502,6 +31551,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Unr_ManTest( pAbc->pGia ); // Mig_ManTest( pAbc->pGia ); // Gia_ManVerifyWithBoxes( pAbc->pGia ); + pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); + Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); 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 + |