summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h8
-rw-r--r--src/aig/gia/giaEquiv.c169
-rw-r--r--src/aig/gia/giaGen.c426
-rw-r--r--src/aig/gia/giaMan.c7
-rw-r--r--src/aig/gia/giaSim.c636
-rw-r--r--src/aig/gia/giaSim5.c55
-rw-r--r--src/aig/gia/giaSimBase.c1178
-rw-r--r--src/aig/gia/giaUtil.c162
-rw-r--r--src/aig/gia/module.make3
-rw-r--r--src/aig/saig/saigInd.c4
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 04:02:52 +0000