From a620c09c401a3d219d91151f39e74943b65d7f40 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 22 Jul 2023 16:44:33 -0700 Subject: [PATCH 01/11] Adding functional comparison to &compare. --- src/aig/gia/giaSimBase.c | 52 ++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 18 ++++++++++---- 2 files changed, 65 insertions(+), 5 deletions(-) diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 47f645413..97335d378 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p ) return vOut; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q ) +{ + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + Vec_Wrd_t * vSimsP = Gia_ManSimPatSimOut( p, vSimsPi, 0 ); + Vec_Wrd_t * vSimsQ = Gia_ManSimPatSimOut( q, vSimsPi, 0 ); + int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0; + Gia_Obj_t * pObjP, * pObjQ; + Gia_ManSetPhase( p ); + Gia_ManSetPhase( q ); + Gia_ManForEachObj( p, pObjP, i ) { + word * pSim = Vec_WrdEntryP( vSimsP, i * nWords ); + if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords ); + } + Gia_ManForEachObj( q, pObjQ, i ) { + word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords ); + if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords ); + } + Gia_ManForEachAnd( q, pObjQ, i ) { + word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords ); + int fFirst = 1; + Gia_ManForEachObj( p, pObjP, k ) { + word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords ); + if ( !Abc_TtEqual(pSimQ, pSimP, nWords) ) + continue; + if ( fFirst ) { + printf( "%5d :", i ); + fFirst = 0; + Count++; + } + printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase ); + } + if ( !fFirst ) + printf( "\n"); + } + printf( "Found %d equivalent nodes.\n", Count ); + Vec_WrdFree( vSimsP ); + Vec_WrdFree( vSimsQ ); + Vec_WrdFree( vSimsPi ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index baf0d7eec..d2bc978d4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45032,17 +45032,21 @@ usage: int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 ); + extern void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q ); Gia_Man_t * pGia0, * pGia1; char ** pArgvNew; int nArgcNew; - int c, fVerbose = 0; + int c, fFunc = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF ) { switch ( c ) { + case 'f': + fFunc ^= 1; + break; case 'v': fVerbose ^= 1; - break; + break; case 'h': goto usage; default: @@ -45063,14 +45067,18 @@ int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" ); return 1; } - Gia_Iso4TestTwo( pGia0, pGia1 ); + if ( fFunc ) + Gia_ManComparePrint( pGia0, pGia1 ); + else + Gia_Iso4TestTwo( pGia0, pGia1 ); Gia_ManStop( pGia0 ); Gia_ManStop( pGia1 ); return 0; usage: - Abc_Print( -2, "usage: &compare [-vh]\n" ); + Abc_Print( -2, "usage: &compare [-fvh]\n" ); Abc_Print( -2, "\t compared two AIGs for structural similarity\n" ); + Abc_Print( -2, "\t-f : toggle functional comparison [default = %s]\n", fFunc? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; From 0108175c6c32d3e8b693d80b9e4559a62767634d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 22 Jul 2023 17:08:01 -0700 Subject: [PATCH 02/11] Bug fix in 'dsd'. --- src/base/abci/abcDsd.c | 8 ++++---- src/bdd/dsd/dsd.h | 4 ++-- src/bdd/dsd/dsdApi.c | 4 ++-- src/bdd/dsd/dsdInt.h | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 5121a4fc4..27d86ae89 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -175,11 +175,11 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * // save the CI nodes in the DSD nodes Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew); - Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew ); + Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (word)(ABC_PTRINT_T)pNodeNew ); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); - Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy ); + Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNode->pCopy ); } // collect DSD nodes in DFS order (leaves and const1 are not collected) @@ -298,7 +298,7 @@ printf( "\n" ); } } pNodeNew->pData = bLocal; - Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew ); + Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNodeNew ); return pNodeNew; } @@ -417,7 +417,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager Abc_ObjForEachFanin( pNode, pFanin, i ) { pFaninDsd = Dsd_ManagerReadInput( pManDsd, i ); - Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin ); + Dsd_NodeSetMark( pFaninDsd, (word)(ABC_PTRINT_T)pFanin ); } // construct the intermediate nodes diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 837579510..4c5cd8915 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -92,8 +92,8 @@ extern DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ); extern Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ); extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ); extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p ); -extern int Dsd_NodeReadMark( Dsd_Node_t * p ); -extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); +extern word Dsd_NodeReadMark( Dsd_Node_t * p ); +extern void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ); extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index 181dfb281..a94d0d26c 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -56,7 +56,7 @@ DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ) { return p->S; } Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ) { return p->pDecs; } Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ) { return p->pDecs[i]; } int Dsd_NodeReadDecsNum( Dsd_Node_t * p ) { return p->nDecs; } -int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; } +word Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; } /**Function************************************************************* @@ -74,7 +74,7 @@ int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; } SeeAlso [] ***********************************************************************/ -void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } +void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ){ p->Mark = Mark; } /**Function************************************************************* diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 37e9746f5..89bfd22ee 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -57,7 +57,7 @@ struct Dsd_Node_t_ DdNode * G; // function of the node DdNode * S; // support of this function Dsd_Node_t ** pDecs; // pointer to structures for formal inputs - int Mark; // the mark used by CASE 4 of disjoint decomposition + word Mark; // the mark used by CASE 4 of disjoint decomposition short nDecs; // the number of formal inputs short nVisits; // the counter of visits }; From 683882f2bb82f5414a6cec7c735984268d451c8a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 22 Jul 2023 22:18:28 -0700 Subject: [PATCH 03/11] Experiments with stochastic synthesis. --- src/aig/gia/giaDeep.c | 1 + src/aig/gia/giaStoch.c | 185 ++++++++++++++++++++++++++++++++++++++++- src/base/abci/abc.c | 22 +++-- 3 files changed, 199 insertions(+), 9 deletions(-) diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index 815a546e4..b58169f42 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -120,6 +120,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in } if ( nTimeToStop && Abc_Clock() > nTimeToStop ) { + if ( !Abc_FrameIsBatchMode() ) printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); break; } diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 94f539988..57775b5cc 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -22,6 +22,19 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" + +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include +#include +#endif + +#endif + + ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// @@ -32,6 +45,169 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Processing on a single core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_StochProcessOne( Gia_Man_t * p, char * pScript, int Rand, int TimeSecs ) +{ + Gia_Man_t * pNew; + char FileName[100], Command[1000]; + sprintf( FileName, "%06x.aig", Rand ); + Gia_AigerWrite( p, FileName, 0, 0, 0 ); + sprintf( Command, "./abc -q \"&read %s; %s; &write %s\"", FileName, pScript, FileName ); + if ( system( (char *)Command ) ) + { + fprintf( stderr, "The following command has returned non-zero exit status:\n" ); + fprintf( stderr, "\"%s\"\n", (char *)Command ); + fprintf( stderr, "Sorry for the inconvenience.\n" ); + fflush( stdout ); + unlink( FileName ); + return Gia_ManDup(p); + } + pNew = Gia_AigerRead( FileName, 0, 0, 0 ); + unlink( FileName ); + if ( pNew && Gia_ManAndNum(pNew) < Gia_ManAndNum(p) ) + return pNew; + Gia_ManStopP( &pNew ); + return Gia_ManDup(p); +} +void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose ) +{ + Gia_Man_t * pGia, * pNew; int i; + Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) ); + Abc_Random(1); + for ( i = 0; i < Vec_PtrSize(vGias); i++ ) + Vec_IntPush( vRands, Abc_Random(0) % 0x1000000 ); + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) + { + pNew = Gia_StochProcessOne( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs ); + Gia_ManStop( pGia ); + Vec_PtrWriteEntry( vGias, i, pNew ); + } + Vec_IntFree( vRands ); +} + +/**Function************************************************************* + + Synopsis [Processing on a many cores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#ifndef ABC_USE_PTHREADS + +void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) +{ + Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); +} + +#else // pthreads are used + + +#define PAR_THR_MAX 100 +typedef struct Gia_StochThData_t_ +{ + Vec_Ptr_t * vGias; + char * pScript; + int Index; + int Rand; + int nTimeOut; + int fWorking; +} Gia_StochThData_t; + +void * Gia_StochWorkerThread( void * pArg ) +{ + Gia_StochThData_t * pThData = (Gia_StochThData_t *)pArg; + volatile int * pPlace = &pThData->fWorking; + Gia_Man_t * pGia, * pNew; + while ( 1 ) + { + while ( *pPlace == 0 ); + assert( pThData->fWorking ); + if ( pThData->Index == -1 ) + { + pthread_exit( NULL ); + assert( 0 ); + return NULL; + } + pGia = (Gia_Man_t *)Vec_PtrEntry( pThData->vGias, pThData->Index ); + pNew = Gia_StochProcessOne( pGia, pThData->pScript, pThData->Rand, pThData->nTimeOut ); + Gia_ManStop( pGia ); + Vec_PtrWriteEntry( pThData->vGias, pThData->Index, pNew ); + pThData->fWorking = 0; + } + assert( 0 ); + return NULL; +} + +void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) +{ + Gia_StochThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + int i, k, status; + if ( fVerbose ) + printf( "Running concurrent synthesis with %d processes.\n", nProcs ); + fflush( stdout ); + if ( nProcs < 2 ) + return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); + // subtract manager thread + nProcs--; + assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); + // start threads + Abc_Random(1); + for ( i = 0; i < nProcs; i++ ) + { + ThData[i].vGias = vGias; + ThData[i].pScript = pScript; + ThData[i].Index = -1; + ThData[i].Rand = Abc_Random(0) % 0x1000000; + ThData[i].nTimeOut = TimeSecs; + ThData[i].fWorking = 0; + status = pthread_create( WorkerThread + i, NULL, Gia_StochWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); + } + // look at the threads + for ( k = 0; k < Vec_PtrSize(vGias); k++ ) + { + for ( i = 0; i < nProcs; i++ ) + { + if ( ThData[i].fWorking ) + continue; + ThData[i].Index = k; + ThData[i].fWorking = 1; + break; + } + if ( i == nProcs ) + k--; + } + // wait till threads finish + for ( i = 0; i < nProcs; i++ ) + if ( ThData[i].fWorking ) + i = -1; + // stop threads + for ( i = 0; i < nProcs; i++ ) + { + assert( !ThData[i].fWorking ); + // stop + ThData[i].Index = -1; + ThData[i].fWorking = 1; + } +} + +#endif // pthreads are used + + /**Function************************************************************* Synopsis [] @@ -184,7 +360,7 @@ Gia_Man_t * Gia_ManDupDivideOne( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vA pNew->vMapping = vMapping; return pNew; } -Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript ) +Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript, int nProcs, int TimeOut ) { Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) ); int i; for ( i = 0; i < Vec_WecSize(vCis); i++ ) @@ -192,7 +368,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds Gia_ManCollectNodes( p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i) ); Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) ); } - Gia_ManStochSynthesis( vAigs, pScript ); + //Gia_ManStochSynthesis( vAigs, pScript ); + Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); return vAigs; } Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash ) @@ -388,7 +565,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds ) SeeAlso [] ***********************************************************************/ -void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript ) +void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ) { abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; abctime clkStart = Abc_Clock(); @@ -407,7 +584,7 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF ); Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds ); Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds ); - Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript ); + Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut ); Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs ); int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew); Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d2bc978d4..2a1550b8a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -49426,10 +49426,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript ); - int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, fVerbose = 0; char * pScript; + extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); + int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NITSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF ) { switch ( c ) { @@ -49477,6 +49477,17 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Seed < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -49497,17 +49508,18 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); - Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript ); + Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); ABC_FREE( pScript ); return 0; usage: - Abc_Print( -2, "usage: &stochsyn [-NITS ] [-tvh]