diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 8 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 169 | ||||
-rw-r--r-- | src/aig/gia/giaGen.c | 426 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 7 | ||||
-rw-r--r-- | src/aig/gia/giaSim.c | 636 | ||||
-rw-r--r-- | src/aig/gia/giaSim5.c | 55 | ||||
-rw-r--r-- | src/aig/gia/giaSimBase.c | 1178 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 162 | ||||
-rw-r--r-- | src/aig/gia/module.make | 3 | ||||
-rw-r--r-- | src/aig/saig/saigInd.c | 4 |
10 files changed, 1847 insertions, 801 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 0efc263b..0e281b7c 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -208,6 +208,7 @@ struct Gia_Man_t_ int nSimWordsMax; Vec_Wrd_t * vSims; Vec_Wrd_t * vSimsPi; + Vec_Wrd_t * vSimsPo; Vec_Int_t * vClassOld; Vec_Int_t * vClassNew; // incremental simulation @@ -231,6 +232,13 @@ struct Gia_Man_t_ Vec_Wrd_t * vSuppWords; // support information Vec_Int_t vCopiesTwo; // intermediate copies Vec_Int_t vSuppVars; // used variables + // additional info + char * pUserFile; + Gia_Man_t * pUserSpec; + Gia_Man_t * pUserAig; + Vec_Ptr_t * vUserNames; + Vec_Wec_t * vUserNodes; + Vec_Int_t * vUserArray; }; diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index db1563fc..ce92b72f 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -508,6 +508,67 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) } } + +/**Function************************************************************* + + Synopsis [Map representatives into class members with minimum level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManChoiceMinLevel_rec( Gia_Man_t * p, int iPivot, int fDiveIn, Vec_Int_t * vMap ) +{ + int Level0, Level1, LevelMax; + Gia_Obj_t * pPivot = Gia_ManObj( p, iPivot ); + if ( Gia_ObjIsCi(pPivot) ) + return 0; + if ( Gia_ObjLevel(p, pPivot) ) + return Gia_ObjLevel(p, pPivot); + if ( fDiveIn && Gia_ObjIsClass(p, iPivot) ) + { + int iObj, ObjMin = -1, iRepr = Gia_ObjRepr(p, iPivot), LevMin = ABC_INFINITY; + Gia_ClassForEachObj( p, iRepr, iObj ) + { + int LevCur = Gia_ManChoiceMinLevel_rec( p, iObj, 0, vMap ); + if ( LevMin > LevCur ) + { + LevMin = LevCur; + ObjMin = iObj; + } + } + assert( LevMin > 0 ); + Vec_IntWriteEntry( vMap, iRepr, ObjMin ); + Gia_ClassForEachObj( p, iRepr, iObj ) + Gia_ObjSetLevelId( p, iObj, LevMin ); + return LevMin; + } + assert( Gia_ObjIsAnd(pPivot) ); + Level0 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0(pPivot, iPivot), 1, vMap ); + Level1 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId1(pPivot, iPivot), 1, vMap ); + LevelMax = 1 + Abc_MaxInt(Level0, Level1); + Gia_ObjSetLevel( p, pPivot, LevelMax ); + return LevelMax; +} +Vec_Int_t * Gia_ManChoiceMinLevel( Gia_Man_t * p ) +{ + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + Gia_Obj_t * pObj; + int i, LevelCur, LevelMax = 0; +// assert( Gia_ManRegNum(p) == 0 ); + Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); + Gia_ManForEachCo( p, pObj, i ) + { + LevelCur = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0p(p, pObj), 1, vMap ); + LevelMax = Abc_MaxInt(LevelMax, LevelCur); + } + //printf( "Max level %d\n", LevelMax ); + return vMap; +} + /**Function************************************************************* Synopsis [Returns representative node.] @@ -583,15 +644,24 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS int i; if ( !p->pReprs && p->pSibls ) { + int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Gia_ObjSetRepr( p, i, GIA_VOID ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) if ( p->pSibls[i] > 0 ) - Gia_ObjSetRepr( p, i, p->pSibls[i] ); - printf( "Created equivalence classes.\n" ); + { + if ( pMap[p->pSibls[i]] == -1 ) + pMap[p->pSibls[i]] = p->pSibls[i]; + pMap[i] = pMap[p->pSibls[i]]; + } + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + if ( p->pSibls[i] > 0 ) + Gia_ObjSetRepr( p, i, pMap[i] ); + //printf( "Created equivalence classes.\n" ); ABC_FREE( p->pNexts ); p->pNexts = Gia_ManDeriveNexts( p ); + ABC_FREE( pMap ); } if ( !p->pReprs ) { @@ -643,6 +713,101 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS /**Function************************************************************* + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap, int fDiveIn ) +{ + Gia_Obj_t * pRepr; + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) ) + { + int iTemp, iRepr = Gia_ObjId(p, pRepr); + Gia_Obj_t * pRepr2 = Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ); + Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 ); + Gia_ClassForEachObj( p, iRepr, iTemp ) + { + Gia_Obj_t * pTemp = Gia_ManObj(p, iTemp); + pTemp->Value = Abc_LitNotCond( pRepr2->Value, Gia_ObjPhaseReal(pRepr2) ^ Gia_ObjPhaseReal(pTemp) ); + } + assert( ~pObj->Value ); + assert( ~pRepr->Value ); + assert( ~pRepr2->Value ); + return; + } + Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 ); + Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) +{ + Vec_Int_t * vMap; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + if ( !p->pReprs && p->pSibls ) + { + int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); + p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( p, i, GIA_VOID ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + if ( p->pSibls[i] > 0 ) + { + if ( pMap[p->pSibls[i]] == -1 ) + pMap[p->pSibls[i]] = p->pSibls[i]; + pMap[i] = pMap[p->pSibls[i]]; + } + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + if ( p->pSibls[i] > 0 ) + Gia_ObjSetRepr( p, i, pMap[i] ); + //printf( "Created equivalence classes.\n" ); + ABC_FREE( p->pNexts ); + p->pNexts = Gia_ManDeriveNexts( p ); + ABC_FREE( pMap ); + } + if ( !p->pReprs ) + { + Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" ); + return NULL; + } + // check if there are any equivalences defined + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + if ( i == Gia_ManObjNum(p) ) + return Gia_ManDup( p ); + vMap = Gia_ManChoiceMinLevel( p ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Vec_IntFree( vMap ); + return pNew; +} + + +/**Function************************************************************* + Synopsis [Reduces AIG using equivalence classes.] Description [] diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c new file mode 100644 index 00000000..09a859ad --- /dev/null +++ b/src/aig/gia/giaGen.c @@ -0,0 +1,426 @@ +/**CFile**************************************************************** + + FileName [giaGen.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/util/utilTruth.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Populate internal simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word * Gia_ManObjSim( Gia_Man_t * p, int iObj ) +{ + return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); +} +static inline void Gia_ManObjSimPi( Gia_Man_t * p, int iObj ) +{ + int w; + word * pSim = Gia_ManObjSim( p, iObj ); + for ( w = 0; w < p->nSimWords; w++ ) + pSim[w] = Gia_ManRandomW( 0 ); +// pSim[0] <<= 1; +} +static inline void Gia_ManObjSimPo( Gia_Man_t * p, int iObj ) +{ + int w; + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pSimCo = Gia_ManObjSim( p, iObj ); + word * pSimDri = Gia_ManObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); + if ( Gia_ObjFaninC0(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + pSimCo[w] = ~pSimDri[w]; + else + for ( w = 0; w < p->nSimWords; w++ ) + pSimCo[w] = pSimDri[w]; +} +static inline void Gia_ManObjSimAnd( Gia_Man_t * p, int iObj ) +{ + int w; + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pSim = Gia_ManObjSim( p, iObj ); + word * pSim0 = Gia_ManObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); + word * pSim1 = Gia_ManObjSim( p, Gia_ObjFaninId1(pObj, iObj) ); + if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + pSim[w] = ~pSim0[w] & ~pSim1[w]; + else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + pSim[w] = ~pSim0[w] & pSim1[w]; + else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + pSim[w] = pSim0[w] & ~pSim1[w]; + else + for ( w = 0; w < p->nSimWords; w++ ) + pSim[w] = pSim0[w] & pSim1[w]; +} +int Gia_ManSimulateWords( Gia_Man_t * p, int nWords ) +{ + Gia_Obj_t * pObj; int i; + // allocate simulation info for one timeframe + Vec_WrdFreeP( &p->vSims ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords ); + p->nSimWords = nWords; + // perform simulation + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManObjSimAnd( p, i ); + else if ( Gia_ObjIsCi(pObj) ) + Gia_ManObjSimPi( p, i ); + else if ( Gia_ObjIsCo(pObj) ) + Gia_ManObjSimPo( p, i ); + else assert( 0 ); + } + return 1; +} + +int Gia_ManSimulateWordsInit( Gia_Man_t * p, Vec_Wrd_t * vSimsIn ) +{ + Gia_Obj_t * pObj; int i, Id; + int nWords = Vec_WrdSize(vSimsIn) / Gia_ManCiNum(p); + assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) ); + // allocate simulation info for one timeframe + Vec_WrdFreeP( &p->vSims ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords ); + p->nSimWords = nWords; + // set input sim info + Gia_ManForEachCiId( p, Id, i ) + memcpy( Vec_WrdEntryP(p->vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords ); + // perform simulation + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManObjSimAnd( p, i ); + else if ( Gia_ObjIsCi(pObj) ) + continue; + else if ( Gia_ObjIsCo(pObj) ) + Gia_ManObjSimPo( p, i ); + else assert( 0 ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Dump data files.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDumpFiles( Gia_Man_t * p, int nCexesT, int nCexesV, int Seed, char * pFileName ) +{ + int n, nSize[2] = {nCexesT*64, nCexesV*64}; + + char pFileNameOutTX[100]; + char pFileNameOutTY[100]; + char pFileNameOutVX[100]; + char pFileNameOutVY[100]; + + sprintf( pFileNameOutTX, "train_%s_%d_%d.data", pFileName ? pFileName : Gia_ManName(p), nSize[0], Gia_ManCiNum(p) ); + sprintf( pFileNameOutTY, "train_%s_%d_%d.data", pFileName ? pFileName : Gia_ManName(p), nSize[0], Gia_ManCoNum(p) ); + sprintf( pFileNameOutVX, "test_%s_%d_%d.data", pFileName ? pFileName : Gia_ManName(p), nSize[1], Gia_ManCiNum(p) ); + sprintf( pFileNameOutVY, "test_%s_%d_%d.data", pFileName ? pFileName : Gia_ManName(p), nSize[1], Gia_ManCoNum(p) ); + + Gia_ManRandomW( 1 ); + for ( n = 0; n < Seed; n++ ) + Gia_ManRandomW( 0 ); + for ( n = 0; n < 2; n++ ) + { + int Res = Gia_ManSimulateWords( p, nSize[n] ); + + Vec_Bit_t * vBitX = Vec_BitAlloc( nSize[n] * Gia_ManCiNum(p) ); + Vec_Bit_t * vBitY = Vec_BitAlloc( nSize[n] * Gia_ManCoNum(p) ); + + FILE * pFileOutX = fopen( n ? pFileNameOutVX : pFileNameOutTX, "wb" ); + FILE * pFileOutY = fopen( n ? pFileNameOutVY : pFileNameOutTY, "wb" ); + + int i, k, Id, Num, Value, nBytes; + for ( k = 0; k < nSize[n]; k++ ) + { + Gia_ManForEachCiId( p, Id, i ) + { + Vec_BitPush( vBitX, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + //printf( "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + } + //printf( " " ); + Gia_ManForEachCoId( p, Id, i ) + { + Vec_BitPush( vBitY, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + //printf( "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + } + //printf( "\n" ); + } + assert( Vec_BitSize(vBitX) <= Vec_BitCap(vBitX) ); + assert( Vec_BitSize(vBitY) <= Vec_BitCap(vBitY) ); + + Num = 2; Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); + Num = nSize[n]; Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); + Num = Gia_ManCiNum(p); Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); + + nBytes = nSize[n] * Gia_ManCiNum(p) / 8; + assert( nSize[n] * Gia_ManCiNum(p) % 8 == 0 ); + Value = fwrite( Vec_BitArray(vBitX), 1, nBytes, pFileOutX ); + assert( Value == nBytes ); + + Num = 2; Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); + Num = nSize[n]; Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); + Num = Gia_ManCoNum(p); Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); + + nBytes = nSize[n] * Gia_ManCoNum(p) / 8; + assert( nSize[n] * Gia_ManCoNum(p) % 8 == 0 ); + Value = fwrite( Vec_BitArray(vBitY), 1, nBytes, pFileOutY ); + assert( Value == nBytes ); + + fclose( pFileOutX ); + fclose( pFileOutY ); + + Vec_BitFree( vBitX ); + Vec_BitFree( vBitY ); + + Res = 0; + } + printf( "Finished dumping files \"%s\" and \"%s\".\n", pFileNameOutTX, pFileNameOutTY ); + printf( "Finished dumping files \"%s\" and \"%s\".\n", pFileNameOutVX, pFileNameOutVY ); +} + +/**Function************************************************************* + + Synopsis [Dump data files.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDumpPlaFiles( Gia_Man_t * p, int nCexesT, int nCexesV, int Seed, char * pFileName ) +{ + int n, nSize[2] = {nCexesT*64, nCexesV*64}; + + char pFileNameOutT[100]; + char pFileNameOutV[100]; + + sprintf( pFileNameOutT, "train_%s_%d.pla", pFileName ? pFileName : Gia_ManName(p), nSize[0], Gia_ManCiNum(p) ); + sprintf( pFileNameOutV, "test_%s_%d.pla", pFileName ? pFileName : Gia_ManName(p), nSize[1], Gia_ManCiNum(p) ); + + Gia_ManRandomW( 1 ); + for ( n = 0; n < Seed; n++ ) + Gia_ManRandomW( 0 ); + for ( n = 0; n < 2; n++ ) + { + int Res = Gia_ManSimulateWords( p, nSize[n] ); + int i, k, Id; + + FILE * pFileOut = fopen( n ? pFileNameOutV : pFileNameOutT, "wb" ); + + fprintf( pFileOut, ".i %d\n", Gia_ManCiNum(p) ); + fprintf( pFileOut, ".o %d\n", Gia_ManCoNum(p) ); + fprintf( pFileOut, ".p %d\n", nSize[n] ); + for ( k = 0; k < nSize[n]; k++ ) + { + Gia_ManForEachCiId( p, Id, i ) + { + //Vec_BitPush( vBitX, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + fprintf( pFileOut, "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + } + fprintf( pFileOut, " " ); + Gia_ManForEachCoId( p, Id, i ) + { + //Vec_BitPush( vBitY, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + fprintf( pFileOut, "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); + } + fprintf( pFileOut, "\n" ); + } + fprintf( pFileOut, ".e\n" ); + + fclose( pFileOut ); + + Res = 0; + } + printf( "Finished dumping files \"%s\" and \"%s\".\n", pFileNameOutT, pFileNameOutV ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSimParamRead( char * pFileName, int * pnIns, int * pnWords ) +{ + int c, nIns = -1, nLines = 0, Count = 0, fReadDot = 0; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return 0; + } + while ( (c = fgetc(pFile)) != EOF ) + { + if ( c == '.' ) + fReadDot = 1; + if ( c == '\n' ) + { + if ( !fReadDot ) + { + if ( nIns == -1 ) + nIns = Count; + else if ( nIns != Count ) + { + printf( "The number of symbols (%d) does not match other lines (%d).\n", Count, nIns ); + fclose( pFile ); + return 0; + } + Count = 0; + nLines++; + } + fReadDot = 0; + } + if ( fReadDot ) + continue; + if ( c != '0' && c != '1' ) + continue; + Count++; + } + if ( nLines % 64 > 0 ) + { + printf( "The number of lines (%d) is not divisible by 64.\n", nLines ); + fclose( pFile ); + return 0; + } + *pnIns = nIns - 1; + *pnWords = nLines / 64; + //printf( "Expecting %d inputs and %d words of simulation data.\n", *pnIns, *pnWords ); + return 1; +} +void Gia_ManSimFileRead( char * pFileName, int nIns, int nWords, Vec_Wrd_t * vSimsIn, Vec_Int_t * vValues ) +{ + int c, nPats = 0, Count = 0, fReadDot = 0; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return; + } + assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); + while ( (c = fgetc(pFile)) != EOF ) + { + if ( c == '.' ) + fReadDot = 1; + if ( c == '\n' ) + fReadDot = 0; + if ( fReadDot ) + continue; + if ( c != '0' && c != '1' ) + continue; + if ( Count == nIns ) + { + Vec_IntPush( vValues, c - '0' ); + Count = 0; + nPats++; + } + else + { + if ( c == '1' ) + Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, Count * nWords), nPats ); + Count++; + } + } + assert( nPats == 64*nWords ); + fclose( pFile ); + printf( "Read %d simulation patterns for %d inputs.\n", 64*nWords, nIns ); +} +void Gia_ManCompareValues( Gia_Man_t * p, Vec_Wrd_t * vSimsIn, Vec_Int_t * vValues ) +{ + int i, Value, Count = 0, nWords = Vec_WrdSize(vSimsIn) / Gia_ManCiNum(p); + word * pSims; + assert( Vec_IntSize(vValues) == nWords * 64 ); + Gia_ManSimulateWordsInit( p, vSimsIn ); + assert( p->nSimWords == nWords ); + pSims = Gia_ManObjSim( p, Gia_ObjId(p, Gia_ManCo(p, 0)) ); + Vec_IntForEachEntry( vValues, Value, i ) + if ( Abc_TtGetBit(pSims, i) == Value ) + Count++; + printf( "Total = %6d. Errors = %6d. Correct = %6d. (%6.2f %%)\n", + Vec_IntSize(vValues), Vec_IntSize(vValues) - Count, Count, 100.0*Count/Vec_IntSize(vValues) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManTestOneFile( Gia_Man_t * p, char * pFileName ) +{ + Vec_Wrd_t * vSimsIn; + Vec_Int_t * vValues; + int nIns, nWords; + if ( !Gia_ManSimParamRead( pFileName, &nIns, &nWords ) ) + return; + vSimsIn = Vec_WrdStart( nIns * nWords ); + vValues = Vec_IntAlloc( nWords * 64 ); + Gia_ManSimFileRead( pFileName, nIns, nWords, vSimsIn, vValues ); + Gia_ManCompareValues( p, vSimsIn, vValues ); + Vec_WrdFree( vSimsIn ); + Vec_IntFree( vValues ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 8df96ee0..2c10bedf 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -88,6 +88,12 @@ void Gia_ManStop( Gia_Man_t * p ) assert( p->pManTime == NULL ); Vec_PtrFreeFree( p->vNamesIn ); Vec_PtrFreeFree( p->vNamesOut ); + ABC_FREE( p->pUserFile ); + Gia_ManStopP( &p->pUserSpec ); + Gia_ManStopP( &p->pUserAig ); + Vec_PtrFreeFree( p->vUserNames ); + Vec_WecFreeP( &p->vUserNodes ); + Vec_IntFreeP( &p->vUserArray ); Vec_IntFreeP( &p->vSwitching ); Vec_IntFreeP( &p->vSuper ); Vec_IntFreeP( &p->vStore ); @@ -95,6 +101,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vClassOld ); Vec_WrdFreeP( &p->vSims ); Vec_WrdFreeP( &p->vSimsPi ); + Vec_WrdFreeP( &p->vSimsPo ); Vec_IntFreeP( &p->vTimeStamps ); Vec_FltFreeP( &p->vTiming ); Vec_VecFreeP( &p->vClockDoms ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 564be76c..001bd8ac 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -1223,642 +1223,6 @@ int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords ) -{ - Vec_Wrd_t * vSims = Vec_WrdAlloc( nWords ); int i; - for ( i = 0; i < nWords; i++ ) - Vec_WrdPush( vSims, Gia_ManRandomW(0) ); - return vSims; -} -void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn ) -{ - int i, Id; - assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); - assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) ); - Gia_ManForEachCiId( p, Id, i ) - memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords ); -} -static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) -{ - word pComps[2] = { 0, ~(word)0 }; - word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; - word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; - word * pSims = Vec_WrdArray(vSims); - word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); - word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i); - word * pSims2 = pSims + nWords*i; int w; - for ( w = 0; w < nWords; w++ ) - pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); -} -static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) -{ - word pComps[2] = { 0, ~(word)0 }; - word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; - word * pSims = Vec_WrdArray(vSims); - word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); - word * pSims2 = pSims + nWords*i; int w; - for ( w = 0; w < nWords; w++ ) - pSims2[w] = (pSims0[w] ^ Diff0); -} -Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia ) -{ - Gia_Obj_t * pObj; - int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); - Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords ); - assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); - Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi ); - Gia_ManForEachAnd( pGia, pObj, i ) - Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims ); - Gia_ManForEachCo( pGia, pObj, i ) - Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims ); - return vSims; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/\ -Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse ) -{ - int nWordsBase = Vec_WrdSize(vBase) / nInputs; - int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w; - Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) ); - assert( Vec_WrdSize(vBase) % nInputs == 0 ); - assert( Vec_WrdSize(vAddOn) % nInputs == 0 ); - assert( nWordsUse <= nWordsAddOn ); - for ( i = 0; i < nInputs; i++ ) - { - word * pSimsB = Vec_WrdEntryP( vBase, i * nWordsBase ); - word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn ); - for ( w = 0; w < nWordsBase; w++ ) - Vec_WrdPush( vSimsIn, pSimsB[w] ); - for ( w = 0; w < nWordsUse; w++ ) - Vec_WrdPush( vSimsIn, pSimsA[w] ); - } - assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) ); - return vSimsIn; -} -int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits ) -{ - word * pSimsI, * pSimsC; int i, k; - for ( i = 0; i < iPat; i++ ) - { - for ( k = 0; k < nLits; k++ ) - { - int iVar = Abc_Lit2Var( pLits[k] ); - pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); - pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); - if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) ) - break; - } - if ( k == nLits ) - break; - } - for ( k = 0; k < nLits; k++ ) - { - int iVar = Abc_Lit2Var( pLits[k] ); - pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); - pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); - if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) ) - Abc_TtXorBit( pSimsI, i ); - Abc_TtSetBit( pSimsC, i ); - assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) ); - } - return (int)(i == iPat); -} -Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes ) -{ - int c, iCur = 0, iPat = 0; - int nWordsMax = Abc_Bit6WordNum( nCexes ); - Vec_Wrd_t * vSimsIn = Gia_ManSimPatGenRandom( Gia_ManCiNum(p) * nWordsMax ); - Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax ); - Vec_Wrd_t * vSimsRes = NULL; - for ( c = 0; c < nCexes; c++ ) - { - int Out = Vec_IntEntry( vCexStore, iCur++ ); - int Size = Vec_IntEntry( vCexStore, iCur++ ); - iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size ); - iCur += Size; - assert( iPat <= nCexes ); - Out = 0; - } - printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat ); - assert( iCur == Vec_IntSize(vCexStore) ); - vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) ); - printf( "Combined %d words of the original info with %d words of additional info.\n", - Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) ); - Vec_WrdFree( vSimsIn ); - Vec_WrdFree( vSimsCare ); - return vSimsRes; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 ) -{ - Gia_Obj_t * pObj; - int i, nUnique; - Vec_Mem_t * vStore; - vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page - Vec_MemHashAlloc( vStore, 1 << 12 ); - Gia_ManForEachCand( p, pObj, i ) - { - word * pSim = Vec_WrdEntryP(vSims, i*nWords); - if ( pnC0 && Abc_TtIsConst0(pSim, nWords) ) - (*pnC0)++; - if ( pnC1 && Abc_TtIsConst1(pSim, nWords) ) - (*pnC1)++; - Vec_MemHashInsert( vStore, pSim ); - } - nUnique = Vec_MemEntryNum( vStore ); - Vec_MemHashFree( vStore ); - Vec_MemFree( vStore ); - return nUnique; -} -Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims ) -{ - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p); - pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) ); - Gia_ManHashStart( pNew ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachAnd( p, pObj, i ) - { - word * pSim = Vec_WrdEntryP(vSims, i*nWords); - if ( Abc_TtIsConst0(pSim, nWords) ) - Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) ); - if ( Abc_TtIsConst1(pSim, nWords) ) - Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) ); - } - Gia_ManHashStop( pNew ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) -{ - int k, Digit, nDigits = nWords*16; - for ( k = 0; k < nDigits; k++ ) - { - Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); - if ( Digit < 10 ) - fprintf( pFile, "%d", Digit ); - else - fprintf( pFile, "%c", 'A' + Digit-10 ); - } - fprintf( pFile, "\n" ); -} -void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) -{ - int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; - FILE * pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for writing.\n", pFileName ); - return; - } - assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); - for ( i = 0; i < nNodes; i++ ) - Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); - fclose( pFile ); - printf( "Written %d words of simulation data.\n", nWords ); -} -int Gia_ManSimPatReadOne( char c ) -{ - int Digit = 0; - if ( c >= '0' && c <= '9' ) - Digit = c - '0'; - else if ( c >= 'A' && c <= 'F' ) - Digit = c - 'A' + 10; - else if ( c >= 'a' && c <= 'f' ) - Digit = c - 'a' + 10; - else assert( 0 ); - assert( Digit >= 0 && Digit < 16 ); - return Digit; -} -Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ) -{ - Vec_Wrd_t * vSimsIn = NULL; - int c, nWords = -1, nChars = 0; word Num = 0; - FILE * pFile = fopen( pFileName, "rb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for reading.\n", pFileName ); - return NULL; - } - vSimsIn = Vec_WrdAlloc( 1000 ); - while ( (c = fgetc(pFile)) != EOF ) - { - if ( c == '\n' && nWords == -1 ) - nWords = Vec_WrdSize(vSimsIn); - if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' ) - continue; - Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4); - if ( ++nChars < 16 ) - continue; - Vec_WrdPush( vSimsIn, Num ); - nChars = 0; - Num = 0; - } - assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); - fclose( pFile ); - printf( "Read %d words of simulation data.\n", nWords ); - return vSimsIn; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManSimProfile( Gia_Man_t * pGia ) -{ - Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia ); - int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia); - int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s ); - printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", - nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s ); - Vec_WrdFree( vSims ); -} -void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose ) -{ - extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); - int i, Status, Counts[3] = {0}; - Gia_Man_t * pGia; - Vec_Wrd_t * vSimsIn = NULL; - Vec_Str_t * vStatus = NULL; - Vec_Int_t * vCexStore = NULL; - Vec_Wrd_t * vSims = Gia_ManSimPatSim( p ); - Gia_ManSimProfile( p ); - pGia = Gia_ManSimPatGenMiter( p, vSims ); - vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 ); - Gia_ManStop( pGia ); - Vec_StrForEachEntry( vStatus, Status, i ) - { - assert( Status >= -1 && Status <= 1 ); - Counts[Status+1]++; - } - printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] ); - if ( Counts[1] == 0 ) - printf( "There are no counter-examples. No need for more simulation.\n" ); - else - { - vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] ); - Vec_WrdFreeP( &p->vSimsPi ); - p->vSimsPi = vSimsIn; - Gia_ManSimProfile( p ); - } - Vec_StrFree( vStatus ); - Vec_IntFree( vCexStore ); - Vec_WrdFree( vSims ); -} - - - - - -typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t; -struct Gia_SimRsbMan_t_ -{ - Gia_Man_t * pGia; - Vec_Int_t * vTfo; - Vec_Int_t * vCands; - Vec_Int_t * vFanins; - Vec_Int_t * vFanins2; - Vec_Wrd_t * vSimsObj; - Vec_Wrd_t * vSimsObj2; - int nWords; - word * pFunc[3]; -}; - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia ) -{ - Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 ); - p->pGia = pGia; - p->nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); - p->pFunc[0] = ABC_CALLOC( word, p->nWords ); - p->pFunc[1] = ABC_CALLOC( word, p->nWords ); - p->pFunc[2] = ABC_CALLOC( word, p->nWords ); - p->vTfo = Vec_IntAlloc( 1000 ); - p->vCands = Vec_IntAlloc( 1000 ); - p->vFanins = Vec_IntAlloc( 10 ); - p->vFanins2 = Vec_IntAlloc( 10 ); - p->vSimsObj = Gia_ManSimPatSim( pGia ); - p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) ); - assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) ); - Gia_ManStaticFanoutStart( pGia ); - return p; -} -void Gia_SimRsbFree( Gia_SimRsbMan_t * p ) -{ - Gia_ManStaticFanoutStop( p->pGia ); - Vec_IntFree( p->vTfo ); - Vec_IntFree( p->vCands ); - Vec_IntFree( p->vFanins ); - Vec_IntFree( p->vFanins2 ); - Vec_WrdFree( p->vSimsObj ); - Vec_WrdFree( p->vSimsObj2 ); - ABC_FREE( p->pFunc[0] ); - ABC_FREE( p->pFunc[1] ); - ABC_FREE( p->pFunc[2] ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo ) -{ - int i, iFan; - if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) - return; - Gia_ObjSetTravIdCurrentId(p, iObj); - Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) - if ( iFanout == -1 || iFan == iFanout ) - Gia_SimRsbTfo_rec( p, iFan, -1, vTfo ); - Vec_IntPush( vTfo, iObj ); -} -Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout ) -{ - assert( iObj > 0 ); - Vec_IntClear( p->vTfo ); - Gia_ManIncrementTravId( p->pGia ); - Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo ); - assert( Vec_IntEntryLast(p->vTfo) == iObj ); - Vec_IntPop( p->vTfo ); - Vec_IntReverseOrder( p->vTfo ); - Vec_IntSort( p->vTfo, 0 ); - return p->vTfo; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet ) -{ - int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) ); - word * pTruth = ABC_CALLOC( word, nTruthWords ); - word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); - word * pFanins[16] = {NULL}; int s, b, iMint, i, iFanin; - assert( Vec_IntSize(vFanins) <= 16 ); - Vec_IntForEachEntry( vFanins, iFanin, i ) - pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin ); - for ( s = 0; s < 64*p->nWords; s++ ) - { - if ( !Abc_TtGetBit(p->pFunc[2], s) || !Abc_TtGetBit(pFunc, s) == fOnSet ) - continue; - iMint = 0; - for ( b = 0; b < Vec_IntSize(vFanins); b++ ) - if ( Abc_TtGetBit(pFanins[b], s) ) - iMint |= 1 << b; - Abc_TtSetBit( pTruth, iMint ); - } - return pTruth; -} -int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins ) -{ - word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 ); - word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 ); - int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 ); - ABC_FREE( pTruth0 ); - ABC_FREE( pTruth1 ); - return Res; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 ) -{ - word pComps[2] = { 0, ~(word)0 }; - word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; - word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; - Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims; - Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims; - word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) ); - word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) ); - word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w; - for ( w = 0; w < nWords; w++ ) - pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); -} -word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo ) -{ - word * pSims = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); - word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj ); int iNode, i; - Abc_TtCopy( pSims2, pSims, p->nWords, 1 ); - Abc_TtClear( p->pFunc[2], p->nWords ); - Vec_IntForEachEntry( vTfo, iNode, i ) - { - Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode); - if ( Gia_ObjIsAnd(pNode) ) - Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 ); - else if ( Gia_ObjIsCo(pNode) ) - { - word * pSimsA = Vec_WrdEntryP( p->vSimsObj, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); - word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); - Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords ); - } - else assert( 0 ); - } - return p->pFunc[2]; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ObjSimCollect( Gia_SimRsbMan_t * p ) -{ - int i, k, iTemp, iFanout; - Vec_IntClear( p->vFanins2 ); - assert( Vec_IntSize(p->vFanins) > 0 ); - Vec_IntForEachEntry( p->vFanins, iTemp, i ) - { - Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp ); - if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) ) - Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) ); - if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) ) - Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) ); - Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k ) - if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) ) - Vec_IntPush( p->vFanins2, iFanout ); - } -} -Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands ) -{ - assert( iObj > 0 ); - assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) ); - Vec_IntClear( p->vCands ); - Vec_IntFill( p->vFanins, 1, iObj ); - while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands ) - { - int i, iTemp; - Vec_IntForEachEntry( p->vFanins, iTemp, i ) - Gia_ObjSetTravIdCurrentId( p->pGia, iTemp ); - Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2 - Vec_IntAppend( p->vCands, p->vFanins2 ); - ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 ); - } - assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands ); - if ( Vec_IntSize(p->vCands) > nCands ) - Vec_IntShrink( p->vCands, nCands ); - return p->vCands; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs ) -{ - int i, iCand, RetValue = 0; - Vec_Int_t * vTfo = Gia_SimRsbTfo( p, iObj, -1 ); - word * pCareSet = Gia_SimRsbCareSet( p, iObj, vTfo ); - word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); - Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands ); - Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 ); - Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 ); - -/* -printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) ); -Vec_IntPrint( vTfo ); -Vec_IntPrint( vCands ); -Extra_PrintBinary( stdout, (unsigned *)pCareSet, 64 ); printf( "\n" ); -Extra_PrintBinary( stdout, (unsigned *)pFunc, 64 ); printf( "\n" ); -Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 ); printf( "\n" ); -Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 ); printf( "\n" ); -*/ - Vec_IntForEachEntry( vCands, iCand, i ) - { - word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand ); - if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) && - !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) ) - { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } - if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) && - !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) ) - { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } - } - return RetValue; -} - -int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose ) -{ - Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0; - Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia ); - assert( pGia->vSimsPi != NULL ); - Gia_ManLevelNum( pGia ); - Gia_ManForEachAnd( pGia, pObj, iObj ) - //if ( iObj == 6 ) - nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs ); - printf( "Resubstitution is possible for %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d)\n", - nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs ); - Gia_SimRsbFree( p ); - return nCount; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSim5.c b/src/aig/gia/giaSim5.c new file mode 100644 index 00000000..bdfd78b4 --- /dev/null +++ b/src/aig/gia/giaSim5.c @@ -0,0 +1,55 @@ +/**CFile**************************************************************** + + FileName [giaSim5.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Simulation engine.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSim5.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "base/main/main.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +void Sim_Init( Abc_Frame_t * pAbc ) {} +void Sim_End( Abc_Frame_t * pAbc ) {} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c new file mode 100644 index 00000000..db8008e7 --- /dev/null +++ b/src/aig/gia/giaSimBase.c @@ -0,0 +1,1178 @@ +/**CFile**************************************************************** + + FileName [giaSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Fast sequential simulator.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/util/utilTruth.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t; +struct Gia_SimRsbMan_t_ +{ + Gia_Man_t * pGia; + Vec_Int_t * vTfo; + Vec_Int_t * vCands; + Vec_Int_t * vFanins; + Vec_Int_t * vFanins2; + Vec_Wrd_t * vSimsObj; + Vec_Wrd_t * vSimsObj2; + int nWords; + word * pFunc[3]; +}; + + +typedef struct Gia_SimAbsMan_t_ Gia_SimAbsMan_t; +struct Gia_SimAbsMan_t_ +{ + // problem formulation + Gia_Man_t * pGia; // AIG manager + word * pSet[2]; // offset/onset truth tables + int nCands; // candidate count + int nWords; // word count + Vec_Wrd_t * vSims; // candidate simulation info + Vec_Int_t * vResub; // the result + // intermediate result + Vec_Int_t * vValues; // function values in each pattern + Vec_Int_t * vPatPairs; // used minterms + int nWordsTable; // words of table data + word * pTableTemp; // temporary table pattern + Vec_Wrd_t * vCoverTable; // columns = minterms; rows = classes + Vec_Int_t * vTtMints; // truth table minterms +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords ) +{ + Vec_Wrd_t * vSims = Vec_WrdAlloc( nWords ); int i; + for ( i = 0; i < nWords; i++ ) + Vec_WrdPush( vSims, Gia_ManRandomW(0) ); + return vSims; +} +void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn ) +{ + int i, Id; + assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); + assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords ); +} +static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) +{ + word pComps[2] = { 0, ~(word)0 }; + word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; + word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; + word * pSims = Vec_WrdArray(vSims); + word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); + word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i); + word * pSims2 = pSims + nWords*i; int w; + for ( w = 0; w < nWords; w++ ) + pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); +} +static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) +{ + word pComps[2] = { 0, ~(word)0 }; + word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; + word * pSims = Vec_WrdArray(vSims); + word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); + word * pSims2 = pSims + nWords*i; int w; + for ( w = 0; w < nWords; w++ ) + pSims2[w] = (pSims0[w] ^ Diff0); +} +Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia ) +{ + Gia_Obj_t * pObj; + int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); + Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords ); + assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); + Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi ); + Gia_ManForEachAnd( pGia, pObj, i ) + Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims ); + Gia_ManForEachCo( pGia, pObj, i ) + Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims ); + return vSims; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimPatValuesDerive( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vValues ) +{ + int i, Id; + assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); + assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) ); + Gia_ManForEachCoId( p, Id, i ) + memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords ); +} +Vec_Wrd_t * Gia_ManSimPatValues( Gia_Man_t * p ) +{ + int i, Id, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + Vec_Wrd_t * vSims = Gia_ManSimPatSim( p ); + Vec_Wrd_t * vValues = Vec_WrdStart( Gia_ManCoNum(p) * nWords ); + assert( Vec_WrdSize(p->vSimsPi) == nWords * Gia_ManCiNum(p) ); + assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) ); + assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); + Gia_ManForEachCoId( p, Id, i ) + memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords ); + Vec_WrdFree( vSims ); + return vValues; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/\ +Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse ) +{ + int nWordsBase = Vec_WrdSize(vBase) / nInputs; + int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w; + Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) ); + assert( Vec_WrdSize(vBase) % nInputs == 0 ); + assert( Vec_WrdSize(vAddOn) % nInputs == 0 ); + assert( nWordsUse <= nWordsAddOn ); + for ( i = 0; i < nInputs; i++ ) + { + word * pSimsB = Vec_WrdEntryP( vBase, i * nWordsBase ); + word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn ); + for ( w = 0; w < nWordsBase; w++ ) + Vec_WrdPush( vSimsIn, pSimsB[w] ); + for ( w = 0; w < nWordsUse; w++ ) + Vec_WrdPush( vSimsIn, pSimsA[w] ); + } + assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) ); + return vSimsIn; +} +int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits ) +{ + word * pSimsI, * pSimsC; int i, k; + for ( i = 0; i < iPat; i++ ) + { + for ( k = 0; k < nLits; k++ ) + { + int iVar = Abc_Lit2Var( pLits[k] ); + pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); + pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); + if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) ) + break; + } + if ( k == nLits ) + break; + } + for ( k = 0; k < nLits; k++ ) + { + int iVar = Abc_Lit2Var( pLits[k] ); + pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); + pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); + if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) ) + Abc_TtXorBit( pSimsI, i ); + Abc_TtSetBit( pSimsC, i ); + assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) ); + } + return (int)(i == iPat); +} +Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes ) +{ + int c, iCur = 0, iPat = 0; + int nWordsMax = Abc_Bit6WordNum( nCexes ); + Vec_Wrd_t * vSimsIn = Gia_ManSimPatGenRandom( Gia_ManCiNum(p) * nWordsMax ); + Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax ); + Vec_Wrd_t * vSimsRes = NULL; + for ( c = 0; c < nCexes; c++ ) + { + int Out = Vec_IntEntry( vCexStore, iCur++ ); + int Size = Vec_IntEntry( vCexStore, iCur++ ); + iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size ); + iCur += Size; + assert( iPat <= nCexes ); + Out = 0; + } + printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat ); + assert( iCur == Vec_IntSize(vCexStore) ); + vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) ); + printf( "Combined %d words of the original info with %d words of additional info.\n", + Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) ); + Vec_WrdFree( vSimsIn ); + Vec_WrdFree( vSimsCare ); + return vSimsRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 ) +{ + Gia_Obj_t * pObj; + int i, nUnique; + Vec_Mem_t * vStore; + vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page + Vec_MemHashAlloc( vStore, 1 << 12 ); + Gia_ManForEachCand( p, pObj, i ) + { + word * pSim = Vec_WrdEntryP(vSims, i*nWords); + if ( pnC0 && Abc_TtIsConst0(pSim, nWords) ) + (*pnC0)++; + if ( pnC1 && Abc_TtIsConst1(pSim, nWords) ) + (*pnC1)++; + Vec_MemHashInsert( vStore, pSim ); + } + nUnique = Vec_MemEntryNum( vStore ); + Vec_MemHashFree( vStore ); + Vec_MemFree( vStore ); + return nUnique; +} +Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p); + pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachAnd( p, pObj, i ) + { + word * pSim = Vec_WrdEntryP(vSims, i*nWords); + if ( Abc_TtIsConst0(pSim, nWords) ) + Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) ); + if ( Abc_TtIsConst1(pSim, nWords) ) + Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) ); + } + Gia_ManHashStop( pNew ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) +{ + int k, Digit, nDigits = nWords*16; + for ( k = 0; k < nDigits; k++ ) + { + Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); + if ( Digit < 10 ) + fprintf( pFile, "%d", Digit ); + else + fprintf( pFile, "%c", 'A' + Digit-10 ); + } + fprintf( pFile, "\n" ); +} +void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) +{ + int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); + for ( i = 0; i < nNodes; i++ ) + Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); + fclose( pFile ); + printf( "Written %d words of simulation data.\n", nWords ); +} +int Gia_ManSimPatReadOne( char c ) +{ + int Digit = 0; + if ( c >= '0' && c <= '9' ) + Digit = c - '0'; + else if ( c >= 'A' && c <= 'F' ) + Digit = c - 'A' + 10; + else if ( c >= 'a' && c <= 'f' ) + Digit = c - 'a' + 10; + else assert( 0 ); + assert( Digit >= 0 && Digit < 16 ); + return Digit; +} +Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ) +{ + Vec_Wrd_t * vSimsIn = NULL; + int c, nWords = -1, nChars = 0; word Num = 0; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + vSimsIn = Vec_WrdAlloc( 1000 ); + while ( (c = fgetc(pFile)) != EOF ) + { + if ( c == '\n' && nWords == -1 ) + nWords = Vec_WrdSize(vSimsIn); + if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' ) + continue; + Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4); + if ( ++nChars < 16 ) + continue; + Vec_WrdPush( vSimsIn, Num ); + nChars = 0; + Num = 0; + } + assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); + fclose( pFile ); + printf( "Read %d words of simulation data.\n", nWords ); + return vSimsIn; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimProfile( Gia_Man_t * pGia ) +{ + Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia ); + int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia); + int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s ); + printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", + nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s ); + Vec_WrdFree( vSims ); +} +void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose ) +{ + extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); + int i, Status, Counts[3] = {0}; + Gia_Man_t * pGia; + Vec_Wrd_t * vSimsIn = NULL; + Vec_Str_t * vStatus = NULL; + Vec_Int_t * vCexStore = NULL; + Vec_Wrd_t * vSims = Gia_ManSimPatSim( p ); + Gia_ManSimProfile( p ); + pGia = Gia_ManSimPatGenMiter( p, vSims ); + vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 ); + Gia_ManStop( pGia ); + Vec_StrForEachEntry( vStatus, Status, i ) + { + assert( Status >= -1 && Status <= 1 ); + Counts[Status+1]++; + } + printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] ); + if ( Counts[1] == 0 ) + printf( "There are no counter-examples. No need for more simulation.\n" ); + else + { + vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] ); + Vec_WrdFreeP( &p->vSimsPi ); + p->vSimsPi = vSimsIn; + Gia_ManSimProfile( p ); + } + Vec_StrFree( vStatus ); + Vec_IntFree( vCexStore ); + Vec_WrdFree( vSims ); +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia ) +{ + Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 ); + p->pGia = pGia; + p->nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); + p->pFunc[0] = ABC_CALLOC( word, p->nWords ); + p->pFunc[1] = ABC_CALLOC( word, p->nWords ); + p->pFunc[2] = ABC_CALLOC( word, p->nWords ); + p->vTfo = Vec_IntAlloc( 1000 ); + p->vCands = Vec_IntAlloc( 1000 ); + p->vFanins = Vec_IntAlloc( 10 ); + p->vFanins2 = Vec_IntAlloc( 10 ); + p->vSimsObj = Gia_ManSimPatSim( pGia ); + p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) ); + assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) ); + Gia_ManStaticFanoutStart( pGia ); + return p; +} +void Gia_SimRsbFree( Gia_SimRsbMan_t * p ) +{ + Gia_ManStaticFanoutStop( p->pGia ); + Vec_IntFree( p->vTfo ); + Vec_IntFree( p->vCands ); + Vec_IntFree( p->vFanins ); + Vec_IntFree( p->vFanins2 ); + Vec_WrdFree( p->vSimsObj ); + Vec_WrdFree( p->vSimsObj2 ); + ABC_FREE( p->pFunc[0] ); + ABC_FREE( p->pFunc[1] ); + ABC_FREE( p->pFunc[2] ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo ) +{ + int i, iFan; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return; + Gia_ObjSetTravIdCurrentId(p, iObj); + Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) + if ( iFanout == -1 || iFan == iFanout ) + Gia_SimRsbTfo_rec( p, iFan, -1, vTfo ); + Vec_IntPush( vTfo, iObj ); +} +Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout ) +{ + assert( iObj > 0 ); + Vec_IntClear( p->vTfo ); + Gia_ManIncrementTravId( p->pGia ); + Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo ); + assert( Vec_IntEntryLast(p->vTfo) == iObj ); + Vec_IntPop( p->vTfo ); + Vec_IntReverseOrder( p->vTfo ); + Vec_IntSort( p->vTfo, 0 ); + return p->vTfo; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet ) +{ + int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) ); + word * pTruth = ABC_CALLOC( word, nTruthWords ); + word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); + word * pFanins[16] = {NULL}; int s, b, iMint, i, iFanin; + assert( Vec_IntSize(vFanins) <= 16 ); + Vec_IntForEachEntry( vFanins, iFanin, i ) + pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin ); + for ( s = 0; s < 64*p->nWords; s++ ) + { + if ( !Abc_TtGetBit(p->pFunc[2], s) || Abc_TtGetBit(pFunc, s) != fOnSet ) + continue; + iMint = 0; + for ( b = 0; b < Vec_IntSize(vFanins); b++ ) + if ( Abc_TtGetBit(pFanins[b], s) ) + iMint |= 1 << b; + Abc_TtSetBit( pTruth, iMint ); + } + return pTruth; +} +int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins ) +{ + word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 ); + word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 ); + int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 ); + ABC_FREE( pTruth0 ); + ABC_FREE( pTruth1 ); + return Res; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 ) +{ + word pComps[2] = { 0, ~(word)0 }; + word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; + word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; + Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims; + Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims; + word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) ); + word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) ); + word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w; + for ( w = 0; w < nWords; w++ ) + pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); +} +word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo ) +{ + word * pSims = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); + word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj ); int iNode, i; + Abc_TtCopy( pSims2, pSims, p->nWords, 1 ); + Abc_TtClear( p->pFunc[2], p->nWords ); + Vec_IntForEachEntry( vTfo, iNode, i ) + { + Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode); + if ( Gia_ObjIsAnd(pNode) ) + Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 ); + else if ( Gia_ObjIsCo(pNode) ) + { + word * pSimsA = Vec_WrdEntryP( p->vSimsObj, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); + word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); + Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords ); + } + else assert( 0 ); + } + return p->pFunc[2]; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ObjSimCollect( Gia_SimRsbMan_t * p ) +{ + int i, k, iTemp, iFanout; + Vec_IntClear( p->vFanins2 ); + assert( Vec_IntSize(p->vFanins) > 0 ); + Vec_IntForEachEntry( p->vFanins, iTemp, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp ); + if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) ) + Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) ); + if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) ) + Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) ); + Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k ) + if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) ) + Vec_IntPush( p->vFanins2, iFanout ); + } +} +Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands ) +{ + assert( iObj > 0 ); + assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) ); + Vec_IntClear( p->vCands ); + Vec_IntFill( p->vFanins, 1, iObj ); + while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands ) + { + int i, iTemp; + Vec_IntForEachEntry( p->vFanins, iTemp, i ) + Gia_ObjSetTravIdCurrentId( p->pGia, iTemp ); + Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2 + Vec_IntAppend( p->vCands, p->vFanins2 ); + ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 ); + } + assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands ); + if ( Vec_IntSize(p->vCands) > nCands ) + Vec_IntShrink( p->vCands, nCands ); + return p->vCands; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs ) +{ + int i, iCand, RetValue = 0; + Vec_Int_t * vTfo = Gia_SimRsbTfo( p, iObj, -1 ); + word * pCareSet = Gia_SimRsbCareSet( p, iObj, vTfo ); + word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); + Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands ); + Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 ); + Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 ); + +/* +printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) ); +Vec_IntPrint( vTfo ); +Vec_IntPrint( vCands ); +Extra_PrintBinary( stdout, (unsigned *)pCareSet, 64 ); printf( "\n" ); +Extra_PrintBinary( stdout, (unsigned *)pFunc, 64 ); printf( "\n" ); +Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 ); printf( "\n" ); +Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 ); printf( "\n" ); +*/ + Vec_IntForEachEntry( vCands, iCand, i ) + { + word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand ); + if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) && + !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) ) + { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } + if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) && + !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) ) + { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } + } + return RetValue; +} + +int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0; + Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia ); + assert( pGia->vSimsPi != NULL ); + Gia_ManLevelNum( pGia ); + Gia_ManForEachAnd( pGia, pObj, iObj ) + //if ( iObj == 6 ) + nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs ); + printf( "Can resubstitute %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d) ", + nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Gia_SimRsbFree( p ); + return nCount; +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimRelAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsIn, Vec_Wrd_t * vSimsIn ) +{ + int i, m, Id, nMints = nWords / nWordsIn; + assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); + assert( Vec_WrdSize(vSimsIn) == nWordsIn * Gia_ManCiNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + for ( m = 0; m < nMints; m++ ) + memcpy( Vec_WrdEntryP(vSims, Id * nWords + nWordsIn * m), + Vec_WrdEntryP(vSimsIn, i * nWordsIn), sizeof(word) * nWordsIn ); +} +int Gia_ManSimRelCompare( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, int iPat, int iMint ) +{ + int i, Id; + Gia_ManForEachCoId( p, Id, i ) + { + word * pSim = Vec_WrdEntryP( vSims, nWords * Id + iMint * nWordsOut ); + word * pSimOut = Vec_WrdEntryP( vSimsOut, nWordsOut * i ); +/* + int k; + for ( k = 0; k < 64*nWordsOut; k++ ) + printf( "%d", Abc_TtGetBit( pSim, k ) ); + printf( "\n" ); + for ( k = 0; k < 64*nWordsOut; k++ ) + printf( "%d", Abc_TtGetBit( pSimOut, k ) ); + printf( "\n\n" ); +*/ + if ( Abc_TtGetBit(pSim, iPat) != Abc_TtGetBit(pSimOut, iPat) ) + return 0; + } + return 1; +} +void Gia_ManSimRelCollectOutputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, Vec_Wrd_t * vRel ) +{ + int i, m, nMints = nWords / nWordsOut; + assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); + assert( Vec_WrdSize(vSimsOut) == nWordsOut * Gia_ManCoNum(p) ); + assert( Vec_WrdSize(vRel) == nWordsOut * nMints ); + for ( i = 0; i < 64 * nWordsOut; i++ ) + for ( m = 0; m < nMints; m++ ) + if ( Gia_ManSimRelCompare(p, nWords, vSims, nWordsOut, vSimsOut, i, m) ) + Abc_TtSetBit( Vec_WrdArray(vRel), i*nMints+m ); +} +Vec_Wrd_t * Gia_ManSimRel( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vVals ) +{ + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + int nMints = 1 << Vec_IntSize(vObjs), i, m, iObj; + Gia_Obj_t * pObj; + Vec_Wrd_t * vRel = Vec_WrdStart( nWords * nMints ); + Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords * nMints ); + Gia_ManSimRelAssignInputs( p, nWords * nMints, vSims, nWords, p->vSimsPi ); + Vec_IntForEachEntry( vObjs, iObj, i ) + for ( m = 0; m < nMints; m++ ) + if ( (m >> i) & 1 ) + memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0xFF, sizeof(word)*nWords ); + else + memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0x00, sizeof(word)*nWords ); + Gia_ManCleanPhase( p ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 1; + Gia_ManForEachAnd( p, pObj, i ) + if ( !pObj->fPhase ) + Gia_ManSimPatSimAnd( p, i, pObj, nWords * nMints, vSims ); + Gia_ManForEachCo( p, pObj, i ) + if ( !pObj->fPhase ) + Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords * nMints, vSims ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 0; + Gia_ManSimRelCollectOutputs( p, nWords * nMints, vSims, nWords, vVals, vRel ); + Vec_WrdFree( vSims ); + return vRel; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSimRelPrint( Gia_Man_t * p, Vec_Wrd_t * vRel, Vec_Int_t * vOutMints ) +{ + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + int nMints = Vec_WrdSize(vRel) / nWords; + int i, k, m, Count; + for ( i = 0; i < 64 * nWords; i++ ) + { + for ( k = 0; k < Gia_ManCiNum(p); k++ ) + printf( "%d", Abc_TtGetBit( Vec_WrdEntryP(p->vSimsPi, k), i ) ); + printf( " " ); + Count = 0; + for ( m = 0; m < nMints; m++ ) + { + printf( "%d", Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) ); + Count += Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ); + } + printf( " Count = %2d ", Count ); + if ( vOutMints ) + { + printf( " %3d ", Vec_IntEntry(vOutMints, i) ); + if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+Vec_IntEntry(vOutMints, i) ) ) + printf( "yes" ); + else + printf( "no" ); + } + printf( "\n" ); + } +} +Vec_Int_t * Gia_ManSimPatStart( int nItems ) +{ + Vec_Int_t * vValues = Vec_IntAlloc( nItems ); + Vec_IntPush( vValues, 17 ); + Vec_IntPush( vValues, 39 ); + Vec_IntPush( vValues, 56 ); + Vec_IntPush( vValues, 221 ); + return vValues; +} +void Gia_ManSimRelTest( Gia_Man_t * p ) +{ + int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + Vec_Int_t * vObjs = Gia_ManSimPatStart( 4 ); // can be CI/AND/CO + Vec_Wrd_t * vVals = Gia_ManSimPatValues( p ); + Vec_Wrd_t * vRel = Gia_ManSimRel( p, vObjs, vVals ); + assert( p->vSimsPi != NULL ); + Gia_ManSimRelPrint( p, vRel, NULL ); + Vec_IntFree( vObjs ); + Vec_WrdFree( vVals ); + Vec_WrdFree( vRel ); +} + + + + + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_Sim5CollectValues( word * pOffSet, word * pOnSet, int nWords ) +{ + Vec_Int_t * vBits = Vec_IntAlloc( 64*nWords ); int i, Count[2] = {0}; + for ( i = 0; i < 64*nWords; i++ ) + if ( Abc_TtGetBit( pOffSet, i ) ) + Vec_IntPush( vBits, 0 ), Count[0]++; + else if ( Abc_TtGetBit( pOnSet, i ) ) + Vec_IntPush( vBits, 1 ), Count[1]++; + else + Vec_IntPush( vBits, -1 ); + //printf( "Offset = %d. Onset = %d. Dcset = %d.\n", Count[0], Count[1], 64*nWords - Count[0] - Count[1] ); + return vBits; +} +Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vResub ) +{ + Gia_SimAbsMan_t * p = ABC_CALLOC( Gia_SimAbsMan_t, 1 ); + p->pGia = pGia; + p->pSet[0] = pOffSet; + p->pSet[1] = pOnSet; + p->nCands = Vec_WrdSize(vSims)/nWords; + p->nWords = nWords; + p->vSims = vSims; + p->vResub = vResub; + p->vValues = Gia_Sim5CollectValues( pOffSet, pOnSet, nWords ); + p->vPatPairs = Vec_IntAlloc( 100 ); + p->vCoverTable = Vec_WrdAlloc( 10000 ); + p->vTtMints = Vec_IntAlloc( 100 ); + assert( Vec_WrdSize(vSims) % nWords == 0 ); + return p; +} +void Gia_SimAbsFree( Gia_SimAbsMan_t * p ) +{ + Vec_IntFree( p->vValues ); + Vec_IntFree( p->vPatPairs ); + Vec_WrdFree( p->vCoverTable ); + Vec_IntFree( p->vTtMints ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SimAbsCheckSolution( Gia_SimAbsMan_t * p ) +{ + int x, y, z, w, fFound = 0; + assert( Vec_WrdSize(p->vCoverTable) == p->nWordsTable * (p->nCands+1) ); + + Abc_TtClear( p->pTableTemp, p->nWordsTable ); + for ( x = 0; x < Vec_IntSize(p->vPatPairs)/2; x++ ) + Abc_TtXorBit( p->pTableTemp, x ); + + for ( x = 0; x < p->nCands; x++ ) + { + word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); + for ( w = 0; w < p->nWordsTable; w++ ) + if ( p->pTableTemp[w] != pSimTableX[w] ) + break; + if ( w == p->nWordsTable ) + { + printf( "Found solution { %d }\n", x ); + fFound = 1; + } + } + if ( fFound ) + return; + + for ( x = 0; x < p->nCands; x++ ) + for ( y = 0; y < x; y++ ) + { + word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); + word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y ); + for ( w = 0; w < p->nWordsTable; w++ ) + if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w]) ) + break; + if ( w == p->nWordsTable ) + { + printf( "Found solution { %d %d }\n", y, x ); + fFound = 1; + } + } + if ( fFound ) + return; + + for ( x = 0; x < p->nCands; x++ ) + for ( y = 0; y < x; y++ ) + for ( z = 0; z < y; z++ ) + { + word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); + word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y ); + word * pSimTableZ = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * z ); + for ( w = 0; w < p->nWordsTable; w++ ) + if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w] | pSimTableZ[w]) ) + break; + if ( w == p->nWordsTable ) + printf( "Found solution { %d %d %d }\n", z, y, x ); + } +} + +void Gia_SimAbsSolve( Gia_SimAbsMan_t * p ) +{ + abctime clk = Abc_Clock(); + int i, k, iPat, iPat2; +/* + Vec_Int_t * vSimPats = Vec_IntDup( p->vPatPairs ); + Vec_IntUniqify( vSimPats ); + printf( "Selected %d pattern pairs contain %d unique patterns.\n", Vec_IntSize(p->vPatPairs)/2, Vec_IntSize(vSimPats) ); + Vec_IntFree( vSimPats ); +*/ + // set up the covering problem + p->nWordsTable = Abc_Bit6WordNum( Vec_IntSize(p->vPatPairs)/2 ); + Vec_WrdFill( p->vCoverTable, p->nWordsTable * (p->nCands + 1), 0 ); + p->pTableTemp = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * p->nCands ); + for ( i = 0; i < p->nCands; i++ ) + { + word * pSimCand = Vec_WrdEntryP( p->vSims, p->nWords * i ); + word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i ); + //printf( "%4d : ", i ); + //Extra_PrintBinary( stdout, (word *)pSimCand, p->nCands ); printf( "\n" ); + Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, k ) + { + assert( Vec_IntEntry(p->vValues, iPat) == 0 ); + assert( Vec_IntEntry(p->vValues, iPat2) == 1 ); + if ( Abc_TtGetBit(pSimCand, iPat) != Abc_TtGetBit(pSimCand, iPat2) ) + Abc_TtXorBit(pSimTable, k/2); + } + assert( k == Vec_IntSize(p->vPatPairs) ); + } + + if ( 0 ) + { + printf( " " ); + for ( i = 0; i < p->nCands; i++ ) + printf( "%d", i % 10 ); + printf( "\n" ); + + Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, i ) + { + printf( "%4d ", i/2 ); + printf( "%4d ", iPat ); + printf( "%4d ", iPat2 ); + for ( k = 0; k < p->nCands; k++ ) + { + word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * k ); + printf( "%c", Abc_TtGetBit(pSimTable, i/2) ? '*' : ' ' ); + } + printf( "\n" ); + } + } + + //Gia_SimAbsCheckSolution(p); + + Vec_IntClear( p->vResub ); + Abc_TtClear( p->pTableTemp, p->nWordsTable ); + for ( i = 0; i < Vec_IntSize(p->vPatPairs)/2; i++ ) + Abc_TtXorBit( p->pTableTemp, i ); + + while ( !Abc_TtIsConst0(p->pTableTemp, p->nWordsTable) ) + { + word * pSimTable; + int iArgMax = -1, CostThis, CostMax = -1; + // compute the cost of each column + for ( i = 0; i < p->nCands; i++ ) + { + pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i ); + CostThis = Abc_TtCountOnesVecMask( pSimTable, p->pTableTemp, p->nWordsTable, 0 ); + if ( CostMax >= CostThis ) + continue; + CostMax = CostThis; + iArgMax = i; + } + // find the best column + Vec_IntPush( p->vResub, iArgMax ); + // delete values of this column + pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * iArgMax ); + Abc_TtSharp( p->pTableTemp, p->pTableTemp, pSimTable, p->nWordsTable ); + } + printf( "Solution %2d for covering problem [%5d x %5d]: ", Vec_IntSize(p->vResub), Vec_IntSize(p->vPatPairs)/2, p->nCands ); + Vec_IntForEachEntry( p->vResub, iPat, i ) + printf( "%4d ", iPat ); + for ( ; i < 16; i++ ) + printf( " ", iPat ); + printf( " " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +} +int Gia_SimAbsRefine( Gia_SimAbsMan_t * p ) +{ + int i, b, Value, iPat, iMint, iObj, Count = 0; + word ** pFanins = ABC_ALLOC( word *, Vec_IntSize(p->vResub) ); + assert( Vec_IntSize(p->vResub) > 0 ); + Vec_IntForEachEntry( p->vResub, iObj, b ) + pFanins[b] = Vec_WrdEntryP( p->vSims, p->nWords * iObj ); + Vec_IntFill( p->vTtMints, 1 << Vec_IntSize(p->vResub), -1 ); + Vec_IntForEachEntry( p->vValues, Value, i ) + { + if ( Value == -1 ) + continue; + iMint = 0; + for ( b = 0; b < Vec_IntSize(p->vResub); b++ ) + if ( Abc_TtGetBit(pFanins[b], i) ) + iMint |= 1 << b; + iPat = Vec_IntEntry( p->vTtMints, iMint ); + if ( iPat == -1 ) + { + Vec_IntWriteEntry( p->vTtMints, iMint, i ); + continue; + } + assert( Abc_TtGetBit(p->pSet[Value], i) ); + if ( Abc_TtGetBit(p->pSet[Value], iPat) ) + continue; + assert( Abc_TtGetBit(p->pSet[!Value], iPat) ); + Vec_IntPushTwo( p->vPatPairs, Value ? iPat : i, Value ? i : iPat ); + //printf( "iPat1 = %d iPat2 = %d Mint = %d\n", Value ? iPat : i, Value ? i : iPat, iMint ); + Count++; + if ( Count == 64 ) + return 1; + } + //printf( "Refinement added %d minterm pairs.\n", Count ); + ABC_FREE( pFanins ); + return Count != 0; +} +Vec_Int_t * Gia_SimAbsFind( Vec_Int_t * vValues, int Value ) +{ + Vec_Int_t * vSubset = Vec_IntAlloc( 100 ); int i, Entry; + Vec_IntForEachEntry( vValues, Entry, i ) + if ( Entry == Value ) + Vec_IntPush( vSubset, i ); + return vSubset; +} +void Gia_SimAbsInit( Gia_SimAbsMan_t * p ) +{ + int n, nPairsInit = 64; + Vec_Int_t * vValue0 = Gia_SimAbsFind( p->vValues, 0 ); + Vec_Int_t * vValue1 = Gia_SimAbsFind( p->vValues, 1 ); + Vec_IntClear( p->vPatPairs ); + printf( "There %d offset and %d onset minterms (%d pairs).\n", Vec_IntSize(vValue0), Vec_IntSize(vValue1), Vec_IntSize(vValue0)*Vec_IntSize(vValue1) ); + Gia_ManRandom( 1 ); + assert( Vec_IntSize(vValue0) > 0 ); + assert( Vec_IntSize(vValue1) > 0 ); + for ( n = 0; n < nPairsInit; n++ ) + Vec_IntPushTwo( p->vPatPairs, + Vec_IntEntry(vValue0, Gia_ManRandom(0) % Vec_IntSize(vValue0)), + Vec_IntEntry(vValue1, Gia_ManRandom(0) % Vec_IntSize(vValue1)) ); + Vec_IntFree( vValue0 ); + Vec_IntFree( vValue1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSimsCands, int nWords ) +{ + Vec_Int_t * vResub = Vec_IntAlloc( 10 ); + Gia_SimAbsMan_t * p = Gia_SimAbsAlloc( pGia, pOffSet, pOnSet, vSimsCands, nWords, vResub ); + Gia_SimAbsInit( p ); + while ( 1 ) + { + Gia_SimAbsSolve( p ); + if ( !Gia_SimAbsRefine( p ) ) + break; + } + Gia_SimAbsFree( p ); + return vResub; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index ea6cb147..072c9872 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2223,167 +2223,6 @@ void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p ) /**Function************************************************************* - Synopsis [Populate internal simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline word * Gia_ManObjSim( Gia_Man_t * p, int iObj ) -{ - return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); -} -static inline void Gia_ManObjSimPi( Gia_Man_t * p, int iObj ) -{ - int w; - word * pSim = Gia_ManObjSim( p, iObj ); - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = Gia_ManRandomW( 0 ); -// pSim[0] <<= 1; -} -static inline void Gia_ManObjSimPo( Gia_Man_t * p, int iObj ) -{ - int w; - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - word * pSimCo = Gia_ManObjSim( p, iObj ); - word * pSimDri = Gia_ManObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); - if ( Gia_ObjFaninC0(pObj) ) - for ( w = 0; w < p->nSimWords; w++ ) - pSimCo[w] = ~pSimDri[w]; - else - for ( w = 0; w < p->nSimWords; w++ ) - pSimCo[w] = pSimDri[w]; -} -static inline void Gia_ManObjSimAnd( Gia_Man_t * p, int iObj ) -{ - int w; - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - word * pSim = Gia_ManObjSim( p, iObj ); - word * pSim0 = Gia_ManObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); - word * pSim1 = Gia_ManObjSim( p, Gia_ObjFaninId1(pObj, iObj) ); - if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = ~pSim0[w] & ~pSim1[w]; - else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = ~pSim0[w] & pSim1[w]; - else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = pSim0[w] & ~pSim1[w]; - else - for ( w = 0; w < p->nSimWords; w++ ) - pSim[w] = pSim0[w] & pSim1[w]; -} -int Gia_ManSimulateWords( Gia_Man_t * p, int nWords ) -{ - Gia_Obj_t * pObj; int i; - // allocate simulation info for one timeframe - Vec_WrdFreeP( &p->vSims ); - p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords ); - p->nSimWords = nWords; - // perform simulation - Gia_ManForEachObj1( p, pObj, i ) - { - if ( Gia_ObjIsAnd(pObj) ) - Gia_ManObjSimAnd( p, i ); - else if ( Gia_ObjIsCi(pObj) ) - Gia_ManObjSimPi( p, i ); - else if ( Gia_ObjIsCo(pObj) ) - Gia_ManObjSimPo( p, i ); - else assert( 0 ); - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [Dump data files.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManDumpFiles( Gia_Man_t * p, int nCexesT, int nCexesV ) -{ - int n, nSize[2] = {nCexesT*64, nCexesV*64}; - - char pFileNameOutTX[100]; - char pFileNameOutTY[100]; - char pFileNameOutVX[100]; - char pFileNameOutVY[100]; - - sprintf( pFileNameOutTX, "data/%s_%d_%d.data", Gia_ManName(p), nSize[0], Gia_ManCiNum(p) ); - sprintf( pFileNameOutTY, "data/%s_%d_%d.data", Gia_ManName(p), nSize[0], Gia_ManCoNum(p) ); - sprintf( pFileNameOutVX, "data/%s_%d_%d.data", Gia_ManName(p), nSize[1], Gia_ManCiNum(p) ); - sprintf( pFileNameOutVY, "data/%s_%d_%d.data", Gia_ManName(p), nSize[1], Gia_ManCoNum(p) ); - - Gia_ManRandomW( 1 ); - for ( n = 0; n < 2; n++ ) - { - int Res = Gia_ManSimulateWords( p, nSize[n] ); - - Vec_Bit_t * vBitX = Vec_BitAlloc( nSize[n] * Gia_ManCiNum(p) ); - Vec_Bit_t * vBitY = Vec_BitAlloc( nSize[n] * Gia_ManCoNum(p) ); - - FILE * pFileOutX = fopen( n ? pFileNameOutVX : pFileNameOutTX, "wb" ); - FILE * pFileOutY = fopen( n ? pFileNameOutVY : pFileNameOutTY, "wb" ); - - int i, k, Id, Num, Value, nBytes; - for ( k = 0; k < nSize[n]; k++ ) - { - Gia_ManForEachCiId( p, Id, i ) - { - Vec_BitPush( vBitX, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); - //printf( "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); - } - //printf( " " ); - Gia_ManForEachCoId( p, Id, i ) - { - Vec_BitPush( vBitY, Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); - //printf( "%d", Abc_TtGetBit(Gia_ManObjSim(p, Id), k) ); - } - //printf( "\n" ); - } - assert( Vec_BitSize(vBitX) <= Vec_BitCap(vBitX) ); - assert( Vec_BitSize(vBitY) <= Vec_BitCap(vBitY) ); - - Num = 2; Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); - Num = nSize[n]; Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); - Num = Gia_ManCiNum(p); Value = fwrite( &Num, 1, 4, pFileOutX ); assert( Value == 4 ); - - nBytes = nSize[n] * Gia_ManCiNum(p) / 8; - assert( nSize[n] * Gia_ManCiNum(p) % 8 == 0 ); - Value = fwrite( Vec_BitArray(vBitX), 1, nBytes, pFileOutX ); - assert( Value == nBytes ); - - Num = 2; Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); - Num = nSize[n]; Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); - Num = Gia_ManCoNum(p); Value = fwrite( &Num, 1, 4, pFileOutY ); assert( Value == 4 ); - - nBytes = nSize[n] * Gia_ManCoNum(p) / 8; - assert( nSize[n] * Gia_ManCoNum(p) % 8 == 0 ); - Value = fwrite( Vec_BitArray(vBitY), 1, nBytes, pFileOutY ); - assert( Value == nBytes ); - - fclose( pFileOutX ); - fclose( pFileOutY ); - - Vec_BitFree( vBitX ); - Vec_BitFree( vBitY ); - - Res = 0; - } -} - -/**Function************************************************************* - Synopsis [] Description [] @@ -2449,6 +2288,7 @@ Gia_Man_t * Gia_ManDupWithMuxPos( Gia_Man_t * p ) return pNew; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 83179060..26909410 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -33,6 +33,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaFrames.c \ src/aig/gia/giaFront.c \ src/aig/gia/giaFx.c \ + src/aig/gia/giaGen.c \ src/aig/gia/giaGig.c \ src/aig/gia/giaGlitch.c \ src/aig/gia/giaHash.c \ @@ -75,6 +76,8 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaSim.c \ src/aig/gia/giaSim2.c \ src/aig/gia/giaSim4.c \ + src/aig/gia/giaSim5.c \ + src/aig/gia/giaSimBase.c \ src/aig/gia/giaSort.c \ src/aig/gia/giaSpeedup.c \ src/aig/gia/giaSplit.c \ diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index f437dba0..d3665c85 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -383,9 +383,9 @@ nextrun: else if ( status == l_Undef ) printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 ); else if ( fUnique || fUniqueAll ) - printf( "Completed %d interations and added %d uniqueness constraints.\n", f+1, nConstrs ); + printf( "Completed %d iterations and added %d uniqueness constraints.\n", f+1, nConstrs ); else - printf( "Completed %d interations.\n", f+1 ); + printf( "Completed %d iterations.\n", f+1 ); } // cleanup sat_solver_delete( pSat ); |