diff options
38 files changed, 2237 insertions, 110 deletions
@@ -13,7 +13,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \ src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \ src/misc/extra src/misc/mvc src/misc/st src/misc/util \ src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \ - src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \ + src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \ src/opt/sim src/opt/ret src/opt/res src/opt/lpk src/opt/fret \ src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \ src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" @@ -1613,6 +1613,38 @@ SOURCE=.\src\opt\fret\fretMain.c SOURCE=.\src\opt\fret\fretTime.c # End Source File # End Group +# Begin Group "mfs" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\mfs\mfs.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsInt.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsSat.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsStrash.c +# End Source File +# Begin Source File + +SOURCE=.\src\opt\mfs\mfsWin.c +# End Source File +# End Group # End Group # Begin Group "map" @@ -2666,6 +2698,10 @@ SOURCE=.\src\aig\fra\fraCore.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraHot.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraImp.c # End Source File # Begin Source File @@ -2674,6 +2710,10 @@ SOURCE=.\src\aig\fra\fraInd.c # End Source File # Begin Source File +SOURCE=.\src\aig\fra\fraIndVer.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\fra\fraLcr.c # End Source File # Begin Source File @@ -36,6 +36,7 @@ alias pex print_exdc -d alias pf print_factor alias pfan print_fanio alias pl print_level +alias plat print_latch alias pio print_io alias pk print_kmap alias ps print_stats diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 5bff39f7..12151343 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -142,6 +142,7 @@ struct Aig_Man_t_ Vec_Int_t * vFlopNums; void * pSeqModel; Aig_Man_t * pManHaig; + Aig_Man_t * pManExdc; // timing statistics int time1; int time2; @@ -210,6 +211,7 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) #endif +static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; } static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); } static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); } static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } @@ -536,6 +538,7 @@ extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ); extern int Aig_ManSeqCleanup( Aig_Man_t * p ); extern int Aig_ManCountMergeRegs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); +extern void Aig_ManComputeSccs( Aig_Man_t * p ); /*=== aigSeq.c ========================================================*/ extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); /*=== aigShow.c ========================================================*/ diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 1388c73e..1979f4f9 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -294,6 +294,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); if ( p->vFlopNums) Vec_IntFree( p->vFlopNums ); + if ( p->pManExdc ) Aig_ManStop( p->pManExdc ); FREE( p->pSeqModel ); FREE( p->pName ); FREE( p->pObjCopies ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index de13653c..e2100b57 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -257,9 +257,10 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p ) Synopsis [Computes supports of the POs in the multi-output AIG.] - Description [] + Description [Returns the array of integer arrays containing indices + of the primary inputs.] - SideEffects [] + SideEffects [Adds the integer PO number at end of each array.] SeeAlso [] diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 9721dd17..70586c68 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -391,6 +391,115 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) return p; } +/**Function************************************************************* + + Synopsis [Computes strongly connected components of registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManComputeSccs( Aig_Man_t * p ) +{ + Vec_Ptr_t * vSupports, * vMatrix, * vMatrix2; + Vec_Int_t * vSupp, * vSupp2, * vComp; + char * pVarsTot; + int i, k, m, iOut, iIn, nComps; + if ( Aig_ManRegNum(p) == 0 ) + { + printf( "The network is combinational.\n" ); + return; + } + // get structural supports for each output + vSupports = Aig_ManSupports( p ); + // transforms the supports into the latch dependency matrix + vMatrix = Vec_PtrStart( Aig_ManRegNum(p) ); + Vec_PtrForEachEntry( vSupports, vSupp, i ) + { + // skip true POs + iOut = Vec_IntPop( vSupp ); + iOut -= Aig_ManPoNum(p) - Aig_ManRegNum(p); + if ( iOut < 0 ) + continue; + // remove PIs + m = 0; + Vec_IntForEachEntry( vSupp, iIn, k ) + { + iIn -= Aig_ManPiNum(p) - Aig_ManRegNum(p); + if ( iIn < 0 ) + continue; + assert( iIn < Aig_ManRegNum(p) ); + Vec_IntWriteEntry( vSupp, m++, iIn ); + } + Vec_IntShrink( vSupp, m ); + // store support in the matrix + assert( iOut < Aig_ManRegNum(p) ); + Vec_PtrWriteEntry( vMatrix, iOut, vSupp ); + } + // create the reverse matrix + vMatrix2 = Vec_PtrAlloc( Aig_ManRegNum(p) ); + for ( i = 0; i < Aig_ManRegNum(p); i++ ) + Vec_PtrPush( vMatrix2, Vec_IntAlloc(8) ); + Vec_PtrForEachEntry( vMatrix, vSupp, i ) + { + Vec_IntForEachEntry( vSupp, iIn, k ) + { + vSupp2 = Vec_PtrEntry( vMatrix2, iIn ); + Vec_IntPush( vSupp2, i ); + } + } + + // detect strongly connected components + vComp = Vec_IntAlloc( Aig_ManRegNum(p) ); + pVarsTot = ALLOC( char, Aig_ManRegNum(p) ); + memset( pVarsTot, 0, Aig_ManRegNum(p) * sizeof(char) ); + for ( nComps = 0; ; nComps++ ) + { + Vec_IntClear( vComp ); + // get the first support + for ( iOut = 0; iOut < Aig_ManRegNum(p); iOut++ ) + if ( pVarsTot[iOut] == 0 ) + break; + if ( iOut == Aig_ManRegNum(p) ) + break; + pVarsTot[iOut] = 1; + Vec_IntPush( vComp, iOut ); + Vec_IntForEachEntry( vComp, iOut, i ) + { + vSupp = Vec_PtrEntry( vMatrix, iOut ); + Vec_IntForEachEntry( vSupp, iIn, k ) + { + if ( pVarsTot[iIn] ) + continue; + pVarsTot[iIn] = 1; + Vec_IntPush( vComp, iIn ); + } + vSupp2 = Vec_PtrEntry( vMatrix2, iOut ); + Vec_IntForEachEntry( vSupp2, iIn, k ) + { + if ( pVarsTot[iIn] ) + continue; + pVarsTot[iIn] = 1; + Vec_IntPush( vComp, iIn ); + } + } + if ( Vec_IntSize(vComp) == Aig_ManRegNum(p) ) + { + printf( "There is only one SCC of registers in this network.\n" ); + break; + } + printf( "SCC #%d contains %5d registers.\n", nComps+1, Vec_IntSize(vComp) ); + } + free( pVarsTot ); + Vec_IntFree( vComp ); + Vec_PtrFree( vMatrix ); + Vec_VecFree( (Vec_Vec_t *)vMatrix2 ); + Vec_VecFree( (Vec_Vec_t *)vSupports ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 5726469f..ddb2dafe 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -132,6 +132,8 @@ extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops ); extern Cnf_Man_t * Cnf_ManStart(); extern void Cnf_ManStop( Cnf_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); +extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals ); +extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 47bc0b67..fab9093d 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -109,6 +109,57 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Allocates the new CNF.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals ) +{ + Cnf_Dat_t * pCnf; + pCnf = ALLOC( Cnf_Dat_t, 1 ); + memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->pMan = pAig; + pCnf->nVars = nVars; + pCnf->nClauses = nClauses; + pCnf->nLiterals = nLiterals; + pCnf->pClauses = ALLOC( int *, nClauses + 1 ); + pCnf->pClauses[0] = ALLOC( int, nLiterals ); + pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(pAig) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [Allocates the new CNF.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ) +{ + Cnf_Dat_t * pCnf; + int i; + pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals ); + memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals ); + memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) ); + for ( i = 1; i < p->nClauses; i++ ) + pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]); + return pCnf; +} + +/**Function************************************************************* + Synopsis [] Description [] diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 8d7116c7..339fd810 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -80,6 +80,7 @@ struct Fra_Par_t_ int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only int fUseImps; // use implications + int fUse1Hot; // use one-hotness conditions int fWriteImps; // record implications int fDontShowBar; // does not show progressbar during fraiging }; @@ -153,6 +154,8 @@ struct Fra_Man_t_ int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example Vec_Int_t * vCex; + // one-hotness conditions + Vec_Int_t * vOneHots; // satisfiability solving sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used @@ -265,6 +268,14 @@ extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p ); extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ); +/*=== fraHot.c ========================================================*/ +extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ); +extern void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ); /*=== fraImp.c ========================================================*/ extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ); @@ -275,7 +286,9 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ); extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ); extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter ); +/*=== fraIndVer.c =====================================================*/ +extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); /*=== fraLcr.c ========================================================*/ extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ @@ -290,6 +303,7 @@ extern void Fra_ManPrint( Fra_Man_t * p ); /*=== fraSat.c ========================================================*/ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); +extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose ); diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index e5b8a126..7929b25d 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -67,7 +67,6 @@ struct Clu_Man_t_ // clauses proven Vec_Int_t * vLitsProven; Vec_Int_t * vClausesProven; - int nClausesProven; // counter-examples Vec_Ptr_t * vCexes; int nCexes; @@ -516,6 +515,21 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) nCountConst = nCountImps = 0; CostMax = p->nSimWords * 32; + + // add the property + { + Aig_Obj_t * pObj; + int Lits[1]; + pObj = Aig_ManPo( p->pAig, 0 ); + Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); + Vec_IntPush( p->vLits, Lits[0] ); + Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); + Vec_IntPush( p->vCosts, CostMax ); + nCountConst++; +// printf( "Added the target property to the set of clauses to be inductively checked.\n" ); + } + + pSeq->nWordsPref = p->nSimWordsPref; Aig_ManForEachLoSeq( p->pAig, pObj1, i ) { @@ -1600,11 +1614,11 @@ if ( p->fVerbose ) clk = clock(); // derive CNF - if ( p->fTarget ) - p->pAig->nRegs++; +// if ( p->fTarget ) +// p->pAig->nRegs++; p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) ); - if ( p->fTarget ) - p->pAig->nRegs--; +// if ( p->fTarget ) +// p->pAig->nRegs--; if ( fVerbose ) { //PRT( "CNF ", clock() - clk ); @@ -1705,6 +1719,9 @@ clk = clock(); } clk = clock(); } + // add proved clauses to storage + Fra_ClausAddToStorage( p ); + // report the results if ( p->fTarget ) { if ( Counter == -1 ) @@ -1722,12 +1739,14 @@ clk = clock(); printf( "Finished proving inductive clauses. " ); PRT( "Time ", clock() - clkTotal ); } - - // add proved clauses to storage - Fra_ClausAddToStorage( p ); } - if ( !p->fTarget && p->fVerbose ) + // verify the computed interpolant + Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven ); +// printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" ); + +// if ( !p->fTarget && p->fVerbose ) + if ( p->fVerbose ) { Fra_ClausPrintIndClauses( p ); Fra_ClausEstimateCoverage( p ); diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 95d65e25..0157421b 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -378,6 +378,7 @@ clk = clock(); // call back the procedure to check implications if ( pManAig->pImpFunc ) pManAig->pImpFunc( p, pManAig->pImpData ); + // no need to filter one-hot clauses because they satisfy base case by construction // finalize the fraiged manager Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c new file mode 100644 index 00000000..6783b459 --- /dev/null +++ b/src/aig/fra/fraHot.c @@ -0,0 +1,424 @@ +/**CFile**************************************************************** + + FileName [fraHot.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Computing and using one-hotness conditions.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraHot.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Fra_RegToLit( int n, int c ) { return c? -n-1 : n+1; } +static inline int Fra_LitReg( int n ) { return (n>0)? n-1 : -n-1; } +static inline int Fra_LitSign( int n ) { return (n<0); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_OneHotNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Fra_ObjSim(pSeq, pObj->Id); + for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ ) + if ( pSims[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_OneHotNodesAreEqual( Fra_Sml_t * pSeq, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + unsigned * pSims0, * pSims1; + int i; + pSims0 = Fra_ObjSim(pSeq, pObj0->Id); + pSims1 = Fra_ObjSim(pSeq, pObj1->Id); + for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ ) + if ( pSims0[i] != pSims1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if implications holds.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2, int fCompl1, int fCompl2 ) +{ + unsigned * pSim1, * pSim2; + int k; + pSim1 = Fra_ObjSim(pSeq, pObj1->Id); + pSim2 = Fra_ObjSim(pSeq, pObj2->Id); + if ( fCompl1 && fCompl2 ) + { + for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ ) + if ( pSim1[k] & pSim2[k] ) + return 0; + } + else if ( fCompl1 ) + { + for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ ) + if ( pSim1[k] & ~pSim2[k] ) + return 0; + } + else if ( fCompl2 ) + { + for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ ) + if ( ~pSim1[k] & pSim2[k] ) + return 0; + } + else + assert( 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes one-hot implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) +{ + int fSkipConstEqu = 1; + Vec_Int_t * vOneHots; + Aig_Obj_t * pObj1, * pObj2; + int i, k; + int nTruePis = Aig_ManPiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig); + assert( pSim->pAig == p->pManAig ); + vOneHots = Vec_IntAlloc( 100 ); + Aig_ManForEachLoSeq( pSim->pAig, pObj1, i ) + { + if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) ) + continue; + assert( i-nTruePis >= 0 ); +// Aig_ManForEachLoSeq( pSim->pAig, pObj2, k ) +// Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) + Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, i+1 ) + { + if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) ) + continue; + if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) ) + continue; + assert( k-nTruePis >= 0 ); + if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) ) + { + Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) ); + Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) ); + continue; + } + if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) ) + { + Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) ); + Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) ); + continue; + } + if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) ) + { + Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) ); + Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) ); + continue; + } + } + } + return vOneHots; +} + +/**Function************************************************************* + + Synopsis [Assumes one-hot implications in the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +**********************************************************************/ +void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + Aig_Obj_t * pObj1, * pObj2; + int i, Out1, Out2, pLits[2]; + int nPiNum = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); + assert( p->pPars->nFramesK == 1 ); // add to only one frame + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; + pObj1 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out1) ); + pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) ); + pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) ); + pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) ); + // add contraint to solver + if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) ) + { + printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" ); + sat_solver_delete( p->pSat ); + p->pSat = NULL; + return; + } + } +} + +/**Function************************************************************* + + Synopsis [Checks one-hot implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +**********************************************************************/ +void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + Aig_Obj_t * pObj1, * pObj2; + int RetValue, i, Out1, Out2; + int nTruePos = Aig_ManPoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; + pObj1 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out1) ); + pObj2 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out2) ); + RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ); + if ( RetValue != 1 ) + { + p->pCla->fRefinement = 1; + if ( RetValue == 0 ) + Fra_SmlResimulate( p ); + if ( Vec_IntEntry(vOneHots, i) != 0 ) + printf( "Fra_OneHotCheck(): Clause is not refined!\n" ); + assert( Vec_IntEntry(vOneHots, i) == 0 ); + } + } +} + +/**Function************************************************************* + + Synopsis [Removes those implications that no longer hold.] + + Description [Returns 1 if refinement has happened.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + Aig_Obj_t * pObj1, * pObj2; + int i, Out1, Out2, RetValue = 0; + int nPiNum = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + assert( p->pSml->pAig == p->pManAig ); + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; + // get the corresponding nodes + pObj1 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out1) ); + pObj2 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out2) ); + // check if implication holds using this simulation info + if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) ) + { + Vec_IntWriteEntry( vOneHots, i, 0 ); + Vec_IntWriteEntry( vOneHots, i+1, 0 ); + RetValue = 1; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Removes those implications that no longer hold.] + + Description [Returns 1 if refinement has happened.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + int i, Out1, Out2, Counter = 0; + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; + Counter++; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Estimates the coverage of state space by clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + int nSimWords = (1<<14); + int nRegs = Aig_ManRegNum(p->pManAig); + Vec_Ptr_t * vSimInfo; + unsigned * pSim1, * pSim2, * pSimTot; + int i, w, Out1, Out2, nCovered, Counter = 0; + int clk = clock(); + + // generate random sim-info at register outputs + vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords ); + srand( 0xAABBAABB ); + for ( i = 0; i < nRegs; i++ ) + { + pSim1 = Vec_PtrEntry( vSimInfo, i ); + for ( w = 0; w < nSimWords; w++ ) + pSim1[w] = Fra_ObjRandomSim(); + } + pSimTot = Vec_PtrEntry( vSimInfo, nRegs ); + + // collect simulation info + memset( pSimTot, 0, sizeof(unsigned) * nSimWords ); + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; +//printf( "(%c%d,%c%d) ", +//Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1), +//Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) ); + Counter++; + pSim1 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) ); + pSim2 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) ); + if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) ) + for ( w = 0; w < nSimWords; w++ ) + pSimTot[w] |= pSim1[w] & pSim2[w]; + else if ( Fra_LitSign(Out1) ) + for ( w = 0; w < nSimWords; w++ ) + pSimTot[w] |= pSim1[w] & ~pSim2[w]; + else if ( Fra_LitSign(Out2) ) + for ( w = 0; w < nSimWords; w++ ) + pSimTot[w] |= ~pSim1[w] & pSim2[w]; + else + assert( 0 ); + } +//printf( "\n" ); + // count the total number of patterns contained in the don't-care + nCovered = 0; + for ( w = 0; w < nSimWords; w++ ) + nCovered += Aig_WordCountOnes( pSimTot[w] ); + Vec_PtrFree( vSimInfo ); + // print the result + printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) ); + printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 ); + PRT( "Time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Creates one-hotness EXDC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj1, * pObj2, * pObj; + int i, Out1, Out2; + pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 ); + for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ ) + Aig_ObjCreatePi(pNew); + for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) + { + Out1 = Vec_IntEntry( vOneHots, i ); + Out2 = Vec_IntEntry( vOneHots, i+1 ); + if ( Out1 == 0 && Out2 == 0 ) + continue; + pObj1 = Aig_ManPi( pNew, Fra_LitReg(Out1) ); + pObj2 = Aig_ManPi( pNew, Fra_LitReg(Out2) ); + pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) ); + pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) ); + pObj = Aig_Or( pNew, pObj1, pObj2 ); + Aig_ObjCreatePo( pNew, pObj ); + } + Aig_ManCleanup(pNew); + printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 1c2140bb..f345b6d1 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -288,6 +288,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, pPars->fLatchCorr = fLatchCorr; pPars->fUseImps = fUseImps; pPars->fWriteImps = fWriteImps; + pPars->fUse1Hot = fUse1Hot; + + assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) ); + assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) ); // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); @@ -316,6 +320,9 @@ PRT( "Time", clock() - clk ); } Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs ); // Fra_ClassesPostprocess( p->pCla ); + // compute one-hotness conditions + if ( p->pPars->fUse1Hot ) + p->vOneHots = Fra_OneHotCompute( p, p->pSml ); // allocate new simulation manager for simulating counter-examples Fra_SmlStop( p->pSml ); p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); @@ -347,6 +354,7 @@ PRT( "Time", clock() - clk ); { int nLitsOld = Fra_ClassesCountLits(p->pCla); int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; + int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes @@ -377,7 +385,7 @@ p->timeTrav += clock() - clk2; if ( p->pSat == NULL ) printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" ); } - + // set the pointers to the manager Aig_ManForEachObj( p->pManFraig, pObj, i ) pObj->pData = p; @@ -395,6 +403,10 @@ p->timeTrav += clock() - clk2; } Cnf_DataFree( pCnf ); + // add one-hotness clauses + if ( p->pPars->fUse1Hot ) + Fra_OneHotAssume( p, p->vOneHots ); + // report the intermediate results if ( fVerbose ) { @@ -403,6 +415,8 @@ p->timeTrav += clock() - clk2; Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); if ( p->pCla->vImps ) printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) ); + if ( p->pPars->fUse1Hot ) + printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) ); printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) ); printf( "\n" ); } @@ -411,6 +425,8 @@ p->timeTrav += clock() - clk2; p->nSatCallsRecent = 0; p->nSatCallsSkipped = 0; clk2 = clock(); + if ( p->pPars->fUse1Hot ) + Fra_OneHotCheck( p, p->vOneHots ); Fra_FraigSweep( p ); if ( fVerbose ) { @@ -430,7 +446,8 @@ clk2 = clock(); // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla)); if ( p->pCla->fRefinement && nLitsOld == Fra_ClassesCountLits(p->pCla) && - nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) ) + nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) && + nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) ) { printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" ); break; @@ -451,13 +468,21 @@ clk2 = clock(); // move the classes into representatives and reduce AIG clk2 = clock(); -// Fra_ClassesPrint( p->pCla, 1 ); - Fra_ClassesSelectRepr( p->pCla ); - Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - pManAigNew = Aig_ManDupRepr( pManAig, 0 ); + if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) ) + { + pManAigNew = Aig_ManDup( pManAig, 1 ); + pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots ); + } + else + { + // Fra_ClassesPrint( p->pCla, 1 ); + Fra_ClassesSelectRepr( p->pCla ); + Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); + pManAigNew = Aig_ManDupRepr( pManAig, 0 ); + } // add implications to the manager - if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) - Fra_ImpRecordInManager( p, pManAigNew ); +// if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) +// Fra_ImpRecordInManager( p, pManAigNew ); // cleanup the new manager Aig_ManSeqCleanup( pManAigNew ); // Aig_ManCountMergeRegs( pManAigNew ); diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c new file mode 100644 index 00000000..efc516c9 --- /dev/null +++ b/src/aig/fra/fraIndVer.c @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [fraIndVer.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Verification of the inductive invariant.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraIndVer.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Verifies the inductive invariant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ) +{ + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int * pStart; + int RetValue, Beg, End, i, k; + int CounterBase = 0, CounterInd = 0; + int clk = clock(); + + if ( nFrames != 1 ) + { + printf( "Invariant verification: Can only verify for K = 1\n" ); + return 1; + } + + // derive CNF + pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) ); +/* + // add the property + { + Aig_Obj_t * pObj; + int Lits[1]; + + pObj = Aig_ManPo( pAig, 0 ); + Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); + + Vec_IntPush( vLits, Lits[0] ); + Vec_IntPush( vClauses, Vec_IntSize(vLits) ); + printf( "Added the target property to the set of clauses to be inductively checked.\n" ); + } +*/ + // derive initialized frames for the base case + pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 ); + // check clauses in the base case + Beg = 0; + pStart = Vec_IntArray( vLits ); + Vec_IntForEachEntry( vClauses, End, i ) + { + // complement the literals + for ( k = Beg; k < End; k++ ) + pStart[k] = lit_neg(pStart[k]); + RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 ); + for ( k = Beg; k < End; k++ ) + pStart[k] = lit_neg(pStart[k]); + Beg = End; + if ( RetValue == l_False ) + continue; +// printf( "Clause %d failed the base case.\n", i ); + CounterBase++; + } + sat_solver_delete( pSat ); + + // derive initialized frames for the base case + pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 ); + assert( pSat->size == 2 * pCnf->nVars ); + // add clauses to the first frame + Beg = 0; + pStart = Vec_IntArray( vLits ); + Vec_IntForEachEntry( vClauses, End, i ) + { + RetValue = sat_solver_addclause( pSat, pStart + Beg, pStart + End ); + Beg = End; + if ( RetValue == 0 ) + { + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + printf( "Invariant verification: SAT solver is unsat after adding a clause.\n" ); + return 0; + } + } + // simplify the solver + if ( pSat->qtail != pSat->qhead ) + { + RetValue = sat_solver_simplify(pSat); + assert( RetValue != 0 ); + assert( pSat->qtail == pSat->qhead ); + } + + // check clauses in the base case + Beg = 0; + pStart = Vec_IntArray( vLits ); + Vec_IntForEachEntry( vClauses, End, i ) + { + // complement the literals + for ( k = Beg; k < End; k++ ) + { + pStart[k] += 2 * pCnf->nVars; + pStart[k] = lit_neg(pStart[k]); + } + RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 ); + for ( k = Beg; k < End; k++ ) + { + pStart[k] = lit_neg(pStart[k]); + pStart[k] -= 2 * pCnf->nVars; + } + Beg = End; + if ( RetValue == l_False ) + continue; +// printf( "Clause %d failed the inductive case.\n", i ); + CounterInd++; + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + if ( CounterBase ) + printf( "Invariant verification: %d clauses (out of %d) FAILED the base case.\n", CounterBase, Vec_IntSize(vClauses) ); + if ( CounterInd ) + printf( "Invariant verification: %d clauses (out of %d) FAILED the inductive case.\n", CounterInd, Vec_IntSize(vClauses) ); + if ( CounterBase || CounterInd ) + return 0; + printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) ); + PRT( "Time", clock() - clk ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index f505b0c2..b06f98d4 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -251,6 +251,7 @@ void Fra_ManStop( Fra_Man_t * p ) if ( p->pCla ) Fra_ClassesStop( p->pCla ); if ( p->pSml ) Fra_SmlStop( p->pSml ); if ( p->vCex ) Vec_IntFree( p->vCex ); + if ( p->vOneHots ) Vec_IntFree( p->vOneHots ); FREE( p->pMemFraig ); FREE( p->pMemFanins ); FREE( p->pMemSatNums ); @@ -279,7 +280,8 @@ void Fra_ManPrint( Fra_Man_t * p ) printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); - if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); + if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); + if ( p->pPars->fUse1Hot ) Fra_OneHotEstimateCoverage( p, p->vOneHots ); PRT( "AIG simulation ", p->pSml->timeSim ); PRT( "AIG traversal ", p->timeTrav ); if ( p->timeRwr ) diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 819605d6..8332fa77 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -300,6 +300,113 @@ p->timeSatFail += clock() - clk; /**Function************************************************************* + Synopsis [Runs the result of test for pObj => pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ) +{ + int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock(); + int status; + + // make sure the nodes are not complemented + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + assert( pNew != pOld ); + + // if at least one of the nodes is a failed node, perform adjustments: + // if the backtrack limit is small, simply skip this node + // if the backtrack limit is > 10, take the quare root of the limit + nBTLimit = p->pPars->nBTLimitNode; +/* + if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) + { + p->nSatFails++; + // fail immediately +// return -1; + if ( nBTLimit <= 10 ) + return -1; + nBTLimit = (int)pow(nBTLimit, 0.7); + } +*/ + p->nSatCalls++; + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + { + p->pSat = sat_solver_new(); + p->nSatVars = 1; + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + } + + // if the nodes do not have SAT variables, allocate them + Fra_CnfNodeAddToSolver( p, pOld, pNew ); + + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + + // prepare variable activity + if ( p->pPars->fConeBias ) + Fra_SetActivityFactors( p, pOld, pNew ); + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 +clk = clock(); +// pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 ); +// pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); + pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL ); + pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR ); +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, + p->nBTLimitGlobal, p->nInsLimitGlobal ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + // continue solving the other implication + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + Fra_SmlSavePattern( p ); + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatFail += clock() - clk; + // mark the node as the failed node + if ( pOld != p->pManFraig->pConst1 ) + pOld->fMarkB = 1; + pNew->fMarkB = 1; + p->nSatFailsReal++; + return -1; + } + // return SAT proof + p->nSatProof++; + return 1; +} + +/**Function************************************************************* + Synopsis [Runs equivalence test for one node.] Description [Returns the fraiged node.] diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index c6bdc20e..3e0fca6a 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); } else { @@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose for ( nFrames = 1; ; nFrames++ ) { clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { @@ -185,7 +185,7 @@ PRT( "Time", clock() - clk ); for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { clk = clock(); - pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 1ad2d4f7..fe11ac36 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -657,6 +657,8 @@ clk = clock(); nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL ); if ( p->pCla->vImps ) nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); + if ( p->vOneHots ) + nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots ); p->timeRef += clock() - clk; if ( !p->pPars->nFramesK && nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make index ffaca75c..e3a88aae 100644 --- a/src/aig/fra/module.make +++ b/src/aig/fra/module.make @@ -5,8 +5,10 @@ SRC += src/aig/fra/fraBmc.c \ src/aig/fra/fraClaus.c \ src/aig/fra/fraCnf.c \ src/aig/fra/fraCore.c \ + src/aig/fra/fraHot.c \ src/aig/fra/fraImp.c \ src/aig/fra/fraInd.c \ + src/aig/fra/fraIndVer.c \ src/aig/fra/fraLcr.c \ src/aig/fra/fraMan.c \ src/aig/fra/fraPart.c \ diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 11161698..e6f8b8f2 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -199,6 +199,7 @@ struct Abc_Ntk_t_ int * pModel; // counter-example (for miters) void * pSeqModel; // counter-example (for sequential miters) Abc_Ntk_t * pExdc; // the EXDC network (if given) + void * pManExdc; // the EXDC network (if given) void * pData; // misc Abc_Ntk_t * pCopy; Hop_Man_t * pHaig; // history AIG diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index d78a3a6a..85cb1569 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -23,6 +23,8 @@ #include "main.h" #include "mio.h" +#include "aig.h" + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -346,6 +348,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) // duplicate the EXDC Ntk if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + if ( pNtk->pManExdc ) + pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" ); pNtk->pCopy = pNtkNew; @@ -431,6 +435,7 @@ Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk ) Abc_ObjAssignName( Abc_NtkCo(pNtkNew, i), "1_", Abc_ObjName(pObj) ); Abc_ObjAssignName( Abc_NtkCo(pNtkNew, Abc_NtkCoNum(pNtk) + i), "2_", Abc_ObjName(pObj) ); } + Abc_NtkOrderCisCos( pNtkNew ); // perform the final check if ( !Abc_NtkCheck( pNtkNew ) ) @@ -936,6 +941,11 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // free EXDC Ntk if ( pNtk->pExdc ) Abc_NtkDelete( pNtk->pExdc ); + if ( pNtk->pManExdc ) + { + Aig_ManStop( pNtk->pManExdc ); + pNtk->pManExdc = NULL; + } // dereference the BDDs if ( Abc_NtkHasBdd(pNtk) ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f0905155..338f38fc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29,6 +29,7 @@ #include "lpk.h" #include "aig.h" #include "dar.h" +#include "mfs.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -66,8 +67,9 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -244,8 +246,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "eliminate", Abc_CommandEliminate, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); @@ -650,17 +653,23 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int fPrintSccs; + extern void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fPrintSccs = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { + case 's': + fPrintSccs ^= 1; + break; case 'h': goto usage; default: @@ -675,11 +684,14 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) } // print the nodes Abc_NtkPrintLatch( pOut, pNtk ); + if ( fPrintSccs ) + Abc_NtkPrintSccs( pNtk, 0 ); return 0; usage: - fprintf( pErr, "usage: print_latch [-h]\n" ); + fprintf( pErr, "usage: print_latch [-sh]\n" ); fprintf( pErr, "\t prints information about latches\n" ); + fprintf( pErr, "\t-s : toggles printing SCCs of registers [default = %s]\n", fPrintSccs? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -2946,6 +2958,158 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Lpk_Par_t Pars, * pPars = &Pars; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + memset( pPars, 0, sizeof(Lpk_Par_t) ); + pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure + pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC + pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) + pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels + pPars->fSatur = 1; + pPars->fZeroCost = 0; + pPars->fFirst = 0; + pPars->fOldAlgo = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutsMax < 2 || pPars->nLutsMax > 8 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutsOver = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutsOver < 0 || pPars->nLutsOver > 8 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nVarsShared = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nGrowthLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) + goto usage; + break; + case 's': + pPars->fSatur ^= 1; + break; + case 'z': + pPars->fZeroCost ^= 1; + break; + case 'f': + pPars->fFirst ^= 1; + break; + case 'o': + pPars->fOldAlgo ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "This command can only be applied to a logic network.\n" ); + return 1; + } + if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 ) + { + fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared ); + return 1; + } + + // modify the current network + if ( !Lpk_Resynthesize( pNtk, pPars ) ) + { + fprintf( pErr, "Resynthesis has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" ); + fprintf( pErr, "\t performs \"rewriting\" for LUT networks;\n" ); + fprintf( pErr, "\t determines LUT size as the max fanin count of a node;\n" ); + fprintf( pErr, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" ); + fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"imfs\")\n" ); + fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); + fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); + fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); + fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); + fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); + fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -3078,65 +3242,52 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; - Lpk_Par_t Pars, * pPars = &Pars; + Mfs_Par_t Pars, * pPars = &Pars; int c; - + +// printf( "Implementation of this command is not finished.\n" ); +// return 1; + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - memset( pPars, 0, sizeof(Lpk_Par_t) ); - pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure - pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC - pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) - pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels - pPars->fSatur = 1; - pPars->fZeroCost = 0; - pPars->fFirst = 0; - pPars->fOldAlgo = 0; + pPars->nWinTfoLevs = 2; + pPars->nFanoutsMax = 10; + pPars->nGrowthLevel = 0; + pPars->fArea = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF ) { switch ( c ) { - case 'N': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nLutsMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nLutsMax < 2 || pPars->nLutsMax > 8 ) - goto usage; - break; - case 'Q': + case 'W': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" ); goto usage; } - pPars->nLutsOver = atoi(argv[globalUtilOptind]); + pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nLutsOver < 0 || pPars->nLutsOver > 8 ) + if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 ) goto usage; break; - case 'S': + case 'F': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - pPars->nVarsShared = atoi(argv[globalUtilOptind]); + pPars->nFanoutsMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 ) + if ( pPars->nFanoutsMax < 1 ) goto usage; break; case 'L': @@ -3150,17 +3301,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) goto usage; break; - case 's': - pPars->fSatur ^= 1; - break; - case 'z': - pPars->fZeroCost ^= 1; - break; - case 'f': - pPars->fFirst ^= 1; - break; - case 'o': - pPars->fOldAlgo ^= 1; + case 'a': + pPars->fArea ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -3185,14 +3327,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command can only be applied to a logic network.\n" ); return 1; } - if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 ) - { - fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared ); - return 1; - } // modify the current network - if ( !Lpk_Resynthesize( pNtk, pPars ) ) + if ( !Abc_NtkMfs( pNtk, pPars ) ) { fprintf( pErr, "Resynthesis has failed.\n" ); return 1; @@ -3200,26 +3337,18 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" ); - fprintf( pErr, "\t performs \"rewriting\" for LUT networks;\n" ); - fprintf( pErr, "\t determines LUT size as the max fanin count of a node;\n" ); - fprintf( pErr, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" ); - fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"imfs\")\n" ); - fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); - fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); - fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); - fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); - fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); - fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); - fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); - fprintf( pErr, "\t-o : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" ); + fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" ); + fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" ); + fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs ); + fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax ); + fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); +// fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); - fprintf( pErr, "\t-w : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); +// fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } - /**Function************************************************************* Synopsis [] @@ -11552,10 +11681,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int nMaxLevs; int fUseImps; int fRewrite; + int fFraiging; int fLatchCorr; int fWriteImps; + int fUse1Hot; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11568,11 +11699,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) nMaxLevs = 0; fUseImps = 0; fRewrite = 0; + fFraiging = 0; fLatchCorr = 0; fWriteImps = 0; + fUse1Hot = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirlevh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF ) { switch ( c ) { @@ -11626,12 +11759,18 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRewrite ^= 1; break; + case 'f': + fFraiging ^= 1; + break; case 'l': fLatchCorr ^= 1; break; case 'e': fWriteImps ^= 1; break; + case 't': + fUse1Hot ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11660,8 +11799,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } + if ( nFramesK > 1 && fUse1Hot ) + { + printf( "Currrently can only use one-hotness for simple induction (K=1).\n" ); + return 0; + } + + if ( nFramesP && fUse1Hot ) + { + printf( "Currrently can only use one-hotness without prefix.\n" ); + return 0; + } + // get the new network - pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -11672,7 +11823,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" ); + fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); @@ -11681,7 +11832,9 @@ usage: fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); + fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", fFraiging? "yes": "no" ); fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" ); + fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", fUse1Hot? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -13376,7 +13529,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: bmc [-F num] [-C num] [-rvh]\n" ); fprintf( pErr, "\t perform bounded model checking\n" ); - fprintf( pErr, "\t-F num : number of time frames [default = %d]\n", nFrames ); + fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-r : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1563bdfe..2a15c3a4 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -184,6 +184,11 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); } + if ( pMan->pManExdc ) + { + pNtkNew->pManExdc = pMan->pManExdc; + pMan->pManExdc = NULL; + } if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); return pNtkNew; @@ -1022,7 +1027,7 @@ PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -1034,8 +1039,10 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in // so fraiging does not reduce the number of functions represented by nodes Fraig_ParamsSetDefault( &Params ); Params.nBTLimit = 100000; -// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - pNtkFraig = Abc_NtkDup( pNtk ); + if ( fFraiging ) + pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + else + pNtkFraig = Abc_NtkDup( pNtk ); if ( fVerbose ) { PRT( "Initial fraiging time", clock() - clk ); @@ -1046,7 +1053,7 @@ PRT( "Initial fraiging time", clock() - clk ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -1530,6 +1537,28 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose return pNtkAig; } +/**Function************************************************************* + + Synopsis [Interplates two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return; + Aig_ManComputeSccs( pMan ); + Aig_ManStop( pMan ); +} + + #include "ntl.h" diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 4003a6d6..6135d009 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -322,11 +322,11 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) Counter2++; } } - fprintf( pFile, "%-15s: ", pNtk->pName ); - fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", - Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] ); - fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); - fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); +// fprintf( pFile, "%-15s: ", pNtk->pName ); + fprintf( pFile, "Total latches = %5d. Init0 = %d. Init1 = %d. InitDC = %d. Const data = %d.\n", + Abc_NtkLatchNum(pNtk), InitNums[1], InitNums[2], InitNums[3], Counter0 ); +// fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); +// fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); } /**Function************************************************************* diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/src/map/pcm/module.make diff --git a/src/map/ply/module.make b/src/map/ply/module.make new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/src/map/ply/module.make diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h new file mode 100644 index 00000000..a7ca3819 --- /dev/null +++ b/src/opt/mfs/mfs.h @@ -0,0 +1,73 @@ +/**CFile**************************************************************** + + FileName [mfs.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFS_H__ +#define __MFS_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Mfs_Par_t_ Mfs_Par_t; +struct Mfs_Par_t_ +{ + // general parameters + int nWinTfoLevs; // the maximum fanout levels + int nFanoutsMax; // the maximum number of fanouts + int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis + int fArea; // performs optimization for area + int fDelay; // performs optimization for delay + int fVerbose; // enable basic stats + int fVeryVerbose; // enable detailed stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfsCore.c ==========================================================*/ +extern int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c new file mode 100644 index 00000000..fe0d84c3 --- /dev/null +++ b/src/opt/mfs/mfsCore.c @@ -0,0 +1,143 @@ +/**CFile**************************************************************** + + FileName [mfsCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + int clk; + // prepare data structure for this node + Mfs_ManClean( p ); + // compute window roots, window support, and window nodes +clk = clock(); + p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax ); + p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); + p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); +p->timeWin += clock() - clk; + // construct AIG for the window +clk = clock(); + p->pAigWin = Abc_NtkConstructAig( p, pNode ); +p->timeAig += clock() - clk; + // translate it into CNF +clk = clock(); + p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) ); +p->timeCnf += clock() - clk; + // create the SAT problem +clk = clock(); + p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + // solve the SAT problem + Abc_NtkMfsSolveSat( p, pNode ); +p->timeSat += clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) +{ + Mfs_Man_t * p; + Abc_Obj_t * pObj; + int i, Counter; + + assert( Abc_NtkIsLogic(pNtk) ); + if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX ) + { + printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); + return 1; + } + // perform the network sweep + Abc_NtkSweep( pNtk, 0 ); + // convert into the AIG + if ( !Abc_NtkToAig(pNtk) ) + { + fprintf( stdout, "Converting to BDD has failed.\n" ); + return 0; + } + assert( Abc_NtkHasAig(pNtk) ); + if ( pNtk->pManExdc != NULL ) + printf( "Performing don't-care computation with don't-cares.\n" ); + + // start the manager + p = Mfs_ManAlloc(); + p->pPars = pPars; + p->pNtk = pNtk; + p->pCare = pNtk->pManExdc; + + // label the register outputs + if ( p->pCare ) + { + Counter = 1; + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFaninNum(pObj) == 0 ) + pObj->pData = NULL; + else + pObj->pData = (void *)Counter++; + assert( Counter == Abc_NtkLatchNum(pNtk) + 1 ); + } + + // compute don't-cares for each node + Abc_NtkForEachNode( pNtk, pObj, i ) + Abc_NtkMfsNode( p, pObj ); + + // undo labesl + if ( p->pCare ) + { + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pData = NULL; + } + + // free the manager + Mfs_ManStop( p ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h new file mode 100644 index 00000000..6ba5903e --- /dev/null +++ b/src/opt/mfs/mfsInt.h @@ -0,0 +1,110 @@ +/**CFile**************************************************************** + + FileName [mfsInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFS_INT_H__ +#define __MFS_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" +#include "mfs.h" +#include "aig.h" +#include "cnf.h" +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define MFS_FANIN_MAX 10 + +typedef struct Mfs_Man_t_ Mfs_Man_t; +struct Mfs_Man_t_ +{ + // input data + Mfs_Par_t * pPars; + Abc_Ntk_t * pNtk; + Aig_Man_t * pCare; + // intermeditate data for the node + Vec_Ptr_t * vRoots; // the roots of the window + Vec_Ptr_t * vSupp; // the support of the window + Vec_Ptr_t * vNodes; // the internal nodes of the window + Vec_Int_t * vProjVars; // the projection variables + // solving data + Aig_Man_t * pAigWin; // window AIG with constraints + Cnf_Dat_t * pCnf; // the CNF for the window + sat_solver * pSat; // the SAT solver used + // the result of solving + int nFanins; // the number of fanins + int nWords; // the number of words + int nCares; // the number of care minterms + unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set + // performance statistics + int nNodesTried; + int nNodesBad; + int nMintsCare; + int nMintsTotal; + // statistics + int timeWin; + int timeAig; + int timeCnf; + int timeSat; +}; + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfsMan.c ==========================================================*/ +extern Mfs_Man_t * Mfs_ManAlloc(); +extern void Mfs_ManStop( Mfs_Man_t * p ); +extern void Mfs_ManClean( Mfs_Man_t * p ); +/*=== mfsSat.c ==========================================================*/ +extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); +/*=== mfsStrash.c ==========================================================*/ +extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ); +/*=== mfsWin.c ==========================================================*/ +extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c new file mode 100644 index 00000000..1341e373 --- /dev/null +++ b/src/opt/mfs/mfsMan.c @@ -0,0 +1,132 @@ +/**CFile**************************************************************** + + FileName [mfsMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedure to manipulation the manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mfs_Man_t * Mfs_ManAlloc() +{ + Mfs_Man_t * p; + // start the manager + p = ALLOC( Mfs_Man_t, 1 ); + memset( p, 0, sizeof(Mfs_Man_t) ); + p->vProjVars = Vec_IntAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfs_ManClean( Mfs_Man_t * p ) +{ + if ( p->pAigWin ) + Aig_ManStop( p->pAigWin ); + if ( p->pCnf ) + Cnf_DataFree( p->pCnf ); + if ( p->pSat ) + sat_solver_delete( p->pSat ); + if ( p->vRoots ) + Vec_PtrFree( p->vRoots ); + if ( p->vSupp ) + Vec_PtrFree( p->vSupp ); + if ( p->vNodes ) + Vec_PtrFree( p->vNodes ); + p->pAigWin = NULL; + p->pCnf = NULL; + p->pSat = NULL; + p->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfs_ManPrint( Mfs_Man_t * p ) +{ + printf( "Nodes tried = %d. Bad nodes = %d.\n", + p->nNodesTried, p->nNodesBad ); + printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n", + p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal ); + PRT( "Win", p->timeWin ); + PRT( "Aig", p->timeAig ); + PRT( "Cnf", p->timeCnf ); + PRT( "Sat", p->timeSat ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfs_ManStop( Mfs_Man_t * p ) +{ + Mfs_ManPrint( p ); + Mfs_ManClean( p ); + Vec_IntFree( p->vProjVars ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c new file mode 100644 index 00000000..d995000f --- /dev/null +++ b/src/opt/mfs/mfsSat.c @@ -0,0 +1,113 @@ +/**CFile**************************************************************** + + FileName [mfsSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Enumerates through the SAT assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) +{ + int Lits[MFS_FANIN_MAX]; + int RetValue, iVar, b, Mint; + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue != l_True ) + return 0; + // add SAT assignment to the solver + Mint = 0; + Vec_IntForEachEntry( p->vProjVars, iVar, b ) + { + Lits[b] = toLit( iVar ); + if ( sat_solver_var_value( p->pSat, iVar ) ) + { + Mint |= (1 << b); + Lits[b] = lit_neg( Lits[b] ); + } + } + assert( !Aig_InfoHasBit(p->uCare, Mint) ); + Aig_InfoSetBit( p->uCare, Mint ); + // add the blocking clause + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + if ( RetValue == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Enumerates through the SAT assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Aig_Obj_t * pObjPo; + int i; + // collect projection variables + Vec_IntClear( p->vProjVars ); + Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) + { + assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); + Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + } + + // prepare the truth table of care set + p->nFanins = Vec_IntSize( p->vProjVars ); + p->nWords = Aig_TruthWordNum( p->nFanins ); + memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); + + // iterate through the SAT assignments + while ( Abc_NtkMfsSolveSat_iter( p ) ); + + // write statistics + p->nCares = 0; + for ( i = 0; i < p->nWords; i++ ) + p->nCares += Aig_WordCountOnes( p->uCare[i] ); + + p->nMintsCare += p->nCares; + p->nMintsTotal += 32 * p->nWords; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c new file mode 100644 index 00000000..7b467936 --- /dev/null +++ b/src/opt/mfs/mfsStrash.c @@ -0,0 +1,224 @@ +/**CFile**************************************************************** + + FileName [mfsStrash.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Structural hashing of the window with ODCs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Construct BDDs and mark AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); + Abc_MfsConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan ); + pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Converts the network from AIG to BDD representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan ) +{ + Hop_Man_t * pHopMan; + Hop_Obj_t * pRoot; + Abc_Obj_t * pFanin; + int i; + // get the local AIG + pHopMan = pObjOld->pNtk->pManFunc; + pRoot = pObjOld->pData; + // check the case of a constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + { + pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) ); + pObjOld->pNext = pObjOld->pCopy; + return; + } + + // assign the fanin nodes + Abc_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy; + // construct the AIG + Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + + // assign the fanin nodes + Abc_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pNext; + // construct the AIG + Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Computes the care set of the node under ODCs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pRoot, * pExor; + Abc_Obj_t * pObj; + int i; + // assign AIG nodes to the leaves + Vec_PtrForEachEntry( p->vSupp, pObj, i ) + pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreatePi( pMan ); + // strash intermediate nodes + Abc_NtkIncrementTravId( pNode->pNtk ); + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + { + Abc_MfsConvertHopToAig( pObj, pMan ); + if ( pObj == pNode ) + pObj->pNext = Abc_ObjNot(pObj->pNext); + } + // create the observability condition + pRoot = Aig_ManConst0(pMan); + Vec_PtrForEachEntry( p->vRoots, pObj, i ) + { + pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext ); + pRoot = Aig_Or( pMan, pRoot, pExor ); + } + return pRoot; +} + +/**Function************************************************************* + + Synopsis [Adds relevant constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pObj0, * pObj1; + if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent( pMan, pObj ); + if ( Aig_ObjIsPi(pObj) ) + return pObj->pData = NULL; + pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan ); + if ( pObj0 == NULL ) + return pObj->pData = NULL; + pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan ); + if ( pObj1 == NULL ) + return pObj->pData = NULL; + pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) ); + pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) ); + return pObj->pData = Aig_And( pMan, pObj0, pObj1 ); +} + +/**Function************************************************************* + + Synopsis [Creates AIG for the window with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Aig_Man_t * pMan; + Abc_Obj_t * pFanin; + Aig_Obj_t * pObjAig, * pPi, * pPo; + int i; + // start the new manager + pMan = Aig_ManStart( 1000 ); + // construct the root node's AIG cone + pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan ); + Aig_ObjCreatePo( pMan, pObjAig ); + if ( p->pCare ) + { + // mark the care set + Aig_ManIncrementTravId( p->pCare ); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + if ( pFanin->pData == NULL ) + continue; + pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 ); + Aig_ObjSetTravIdCurrent( p->pCare, pPi ); + pPi->pData = pFanin->pCopy; + } + // construct the constraints + Aig_ManForEachPo( p->pCare, pPo, i ) + { + pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pMan, pObjAig ); + } + } + // construct the fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pObjAig = (Aig_Obj_t *)pFanin->pCopy; + Aig_ObjCreatePo( pMan, pObjAig ); + } + Aig_ManCleanup( pMan ); + return pMan; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c new file mode 100644 index 00000000..b812d44d --- /dev/null +++ b/src/opt/mfs/mfsWin.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [mfsWin.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the node should be a root.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_MfsComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit ) +{ + Abc_Obj_t * pFanout; + int i; + // the node is the root if one of the following is true: + // (1) the node has more than fanouts than the limit + if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit ) + return 1; + // (2) the node has CO fanouts + // (3) the node has fanouts above the cutoff level + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots ) +{ + Abc_Obj_t * pFanout; + int i; + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + // check if the node should be the root + if ( Abc_MfsComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) ) + Vec_PtrPush( vRoots, pNode ); + else // if not, explore its fanouts + Abc_ObjForEachFanout( pNode, pFanout, i ) + Abc_MfsComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots ); +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [Returns 1 if the only root is this node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ) +{ + Vec_Ptr_t * vRoots; + vRoots = Vec_PtrAlloc( 10 ); + Abc_NtkIncrementTravId( pNode->pNtk ); + Abc_MfsComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots ); + assert( Vec_PtrSize(vRoots) > 0 ); +// if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode ) +// return 0; + return vRoots; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfs_.c b/src/opt/mfs/mfs_.c new file mode 100644 index 00000000..32caf7ff --- /dev/null +++ b/src/opt/mfs/mfs_.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [mfs_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfs_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make new file mode 100644 index 00000000..7b9f1260 --- /dev/null +++ b/src/opt/mfs/module.make @@ -0,0 +1,5 @@ +SRC += src/opt/mfs/mfsCore.c \ + src/opt/mfs/mfsMan.c \ + src/opt/mfs/mfsSat.c \ + src/opt/mfs/mfsStrash.c \ + src/opt/mfs/mfsWin.c diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index fbc9874d..8a13d203 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -946,6 +946,7 @@ sat_solver* sat_solver_new(void) veci_new(&s->stack); veci_new(&s->model); veci_new(&s->act_vars); + veci_new(&s->temp_clause); // initialize arrays s->wlists = 0; @@ -1020,6 +1021,7 @@ void sat_solver_delete(sat_solver* s) veci_delete(&s->stack); veci_delete(&s->model); veci_delete(&s->act_vars); + veci_delete(&s->temp_clause); free(s->binary); // delete arrays @@ -1052,6 +1054,12 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) lbool* values; lit last; + veci_resize( &s->temp_clause, 0 ); + for ( i = begin; i < end; i++ ) + veci_push( &s->temp_clause, *i ); + begin = veci_begin( &s->temp_clause ); + end = begin + veci_size( &s->temp_clause ); + if (begin == end) return false; //printlits(begin,end); printf("\n"); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index c1bf32a7..9ffc2b75 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -187,6 +187,8 @@ struct sat_solver_t FILE * pFile; int nClauses; int nRoots; + + veci temp_clause; // temporary storage for a CNF clause }; static int sat_solver_var_value( sat_solver* s, int v ) |