From f8a6432d75f0f4bd85c56bab9ca417c27e9a35ab Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 24 Jul 2024 20:23:07 -0700 Subject: [PATCH] Implementation of functional abstraction. --- src/aig/gia/giaDup.c | 176 +++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 114 +++++++++++++++++++++++++++- src/base/io/io.c | 10 ++- 3 files changed, 298 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 64e7a16c9..a0b722bf1 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5960,6 +5960,182 @@ Gia_Man_t * Gia_ManDupWindow( Gia_Man_t * p, Vec_Int_t * vCut ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Gia_ManCollectIntTfos( Gia_Man_t * p, Vec_Int_t * vVarNums ) +{ + Vec_Wec_t * vTfos = Vec_WecStart( Vec_IntSize(vVarNums) ); + Vec_Int_t * vNodes = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj; int i, k, Input, iNode; + Gia_ManIncrementTravId( p ); + Vec_IntForEachEntry( vVarNums, Input, i ) + Gia_ObjSetTravIdCurrentId( p, Gia_ManCiIdToId(p, Input) ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) || Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ) + Gia_ObjSetTravIdCurrentId( p, i ), Vec_IntPush( vNodes, i ); + Vec_IntForEachEntry( vVarNums, Input, i ) + { + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrentId( p, Gia_ManCiIdToId(p, Input) ); + Vec_IntForEachEntry( vNodes, iNode, k ) + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(Gia_ManObj(p, iNode), iNode)) || Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(Gia_ManObj(p, iNode), iNode)) ) + Gia_ObjSetTravIdCurrentId( p, iNode ), Vec_WecPush( vTfos, i, iNode ); + } + Vec_IntFree( vNodes ); + return vTfos; +} +Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums ) +{ + Vec_Int_t * vOutLits = Vec_IntStartFull( 1 << Vec_IntSize(vVarNums) ); + Vec_Wec_t * vTfos = Gia_ManCollectIntTfos( p, vVarNums ); + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRoot = Gia_ManCo(p, 0); int i, iLit; + assert( Gia_ManPoNum(p) == 1 && Gia_ManRegNum(p) == 0 ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCiVec( vVarNums, p, pObj, i ) + pObj->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntWriteEntry( vOutLits, 0, Gia_ObjFanin0Copy(pRoot) ); + int m, g, x, b = 0; + for ( m = 1; m < Vec_IntSize(vOutLits); m++ ) + { + g = m ^ (m >> 1); x = (b ^ g) == 1 ? 0 : Abc_Base2Log(b ^ g); b = g; + Vec_Int_t * vNode = Vec_WecEntry( vTfos, x ); + Gia_ManPi(p, Vec_IntEntry(vVarNums, x))->Value ^= 1; + Gia_ManForEachObjVec( vNode, p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntWriteEntry( vOutLits, g, Gia_ObjFanin0Copy(pRoot) ); + } + assert( Vec_IntFindMin(vOutLits) >= 0 ); + Vec_IntForEachEntry( vOutLits, iLit, i ) + Gia_ManAppendCo( pNew, iLit ); + Vec_IntFree( vOutLits ); + Vec_WecFree( vTfos ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCofPattern( Gia_Man_t * p ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) ); + Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(p) ); + Gia_Obj_t * pObj; int i, iLit, iClass = 0; + assert( Gia_ManCoNum(p) == 1 << Abc_Base2Log(Gia_ManCoNum(p)) ); + Gia_ManForEachPo( p, pObj, i ) + { + iLit = Gia_ObjFaninLit0p(p, pObj); + if ( Vec_IntEntry(vMap, iLit) == -1 ) + Vec_IntWriteEntry( vMap, iLit, iClass++ ); + Vec_IntPush( vRes, Vec_IntEntry(vMap, iLit) ); + } + Vec_IntFree( vMap ); + return vRes; +} +Vec_Int_t * Gia_ManCofClassPattern( Gia_Man_t * p, Vec_Int_t * vVarNums, int fVerbose ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); + Gia_Man_t * pCofs = Gia_ManDupCofs( p, vVarNums ); + Gia_Man_t * pSweep = Cec4_ManSimulateTest3( pCofs, 0, 0 ); + Vec_Int_t * vRes = Gia_ManCofPattern( pSweep ); + assert( Vec_IntSize(vRes) == 1 << Vec_IntSize(vVarNums) ); + Gia_ManStop( pSweep ); + Gia_ManStop( pCofs ); + if ( fVerbose ) + { + int i, Class, nClasses = Vec_IntFindMax(vRes)+1; + printf( "Pattern %d -> %d: ", Vec_IntSize(vVarNums), nClasses ); + if ( nClasses <= 36 ) + Vec_IntForEachEntry( vRes, Class, i ) + printf( "%c", (Class < 10 ? (int)'0' : (int)'A'-10) + Class ); + printf( "\n" ); + } + return vRes; +} +Gia_Man_t * Gia_ManDupEncode( Gia_Man_t * p, Vec_Int_t * vVarNums, int fVerbose ) +{ + extern Vec_Int_t * Gia_GenDecoder( Gia_Man_t * p, int * pLits, int nLits ); + Gia_Man_t * pNew, * pTemp; + Vec_Int_t * vCols = Gia_ManCofClassPattern( p, vVarNums, fVerbose ); + Vec_Int_t * vVars = Vec_IntAlloc( 100 ), * vDec; + int i, k, Limit = Vec_IntSize(vCols), Entry; + int nClasses = Vec_IntFindMax(vCols)+1; + int nExtras = Abc_Base2Log(nClasses); + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + for ( i = 0; i < Vec_IntSize(vVarNums) + nExtras; i++ ) + Vec_IntPush( vVars, Gia_ManAppendCi(pNew) ); + Gia_ManHashAlloc( pNew ); + vDec = Gia_GenDecoder( pNew, Vec_IntEntryP(vVars, Vec_IntSize(vVarNums)), nExtras ); + Vec_IntForEachEntry( vCols, Entry, i ) + Vec_IntWriteEntry( vCols, i, Vec_IntEntry(vDec, Entry) ); + Vec_IntFree( vDec ); + for ( i = Vec_IntSize(vVarNums) - 1; i >= 0; i--, Limit /= 2 ) + for ( k = 0; k < Limit; k += 2 ) + Vec_IntWriteEntry( vCols, k/2, Gia_ManHashMux(pNew, Vec_IntEntry(vVars, i), Vec_IntEntry(vCols, k+1), Vec_IntEntry(vCols, k)) ); + Gia_ManAppendCo( pNew, Vec_IntEntry(vCols, 0) ); + Vec_IntFree( vCols ); + Vec_IntFree( vVars ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + if ( fVerbose ) + printf( "Generated AIG with %d inputs and %d nodes representing %d PIs with %d columns.\n", + Gia_ManPiNum(pNew), Gia_ManAndNum(pNew), Vec_IntSize(vVarNums), nClasses ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCofClassRand( Gia_Man_t * p, int nVars, int nRands ) +{ + for ( int n = 0; n < nRands; n++ ) + { + Vec_Int_t * vIns = Vec_IntStartNatural( Gia_ManPiNum(p) ); + Vec_IntRandomizeOrder( vIns ); + Vec_IntShrink( vIns, nVars ); + Vec_IntPrint( vIns ); + Vec_Int_t * vTemp = Gia_ManCofClassPattern( p, vIns, 1 ); + Vec_IntFree( vTemp ); + Vec_IntFree( vIns ); + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dbd1f4843..cca768542 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -611,6 +611,7 @@ static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GenRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenMux ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Window ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9FunAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1404,8 +1405,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&genrel", Abc_CommandAbc9GenRel, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genmux", Abc_CommandAbc9GenMux, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&window", Abc_CommandAbc9Window, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&funabs", Abc_CommandAbc9FunAbs, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { // extern Mf_ManTruthCount(); // Mf_ManTruthCount(); @@ -53468,6 +53470,116 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9FunAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDupEncode( Gia_Man_t * p, Vec_Int_t * vVarNums, int fVerbose ); + extern Vec_Int_t * Gia_ManCofClassPattern( Gia_Man_t * p, Vec_Int_t * vVarNums, int fVerbose ); + extern void Gia_ManCofClassRand( Gia_Man_t * p, int nVars, int nRands ); + Gia_Man_t * pNew = NULL; + Vec_Int_t * vVars = NULL; + int c, nVars = 6, nRands = 0, fPrint = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KRpvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRands = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRands < 0 ) + goto usage; + break; + case 'p': + fPrint ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9FunAbs(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManPoNum(pAbc->pGia) != 1 || Gia_ManRegNum(pAbc->pGia) != 0 ) { + Abc_Print( -1, "Abc_CommandAbc9FunAbs(): Works only for comb AIGs with one output.\n" ); + return 0; + } + if ( nVars >= Gia_ManPiNum(pAbc->pGia) ) { + Abc_Print( -1, "Abc_CommandAbc9FunAbs(): The number of variables (%d) should be less the PI count (%d).\n", nVars, Gia_ManPiNum(pAbc->pGia) ); + return 0; + } + if ( nRands ) { + Gia_ManCofClassRand( pAbc->pGia, nVars, nRands ); + return 0; + } + if ( argc == globalUtilOptind ) { + vVars = Vec_IntStartNatural( nVars ); + printf( "Abstracting the first %d variables of the AIG.\n", nVars ); + } + else { + vVars = Vec_IntAlloc( argc ); + for ( c = globalUtilOptind; c < argc; c++ ) + Vec_IntPush( vVars, atoi(argv[c]) ); + printf( "Abstracting variables: " ); + Vec_IntPrint( vVars ); + } + if ( fPrint ) { + Vec_Int_t * vTemp = Gia_ManCofClassPattern( pAbc->pGia, vVars, 1 ); + Vec_IntFree( vTemp ); + } + else { + pNew = Gia_ManDupEncode( pAbc->pGia, vVars, fVerbose ); + Abc_FrameUpdateGia( pAbc, pNew ); + } + Vec_IntFree( vVars ); + return 0; + +usage: + Abc_Print( -2, "usage: &funabs [-KR num] [-pvh] ... \n" ); + Abc_Print( -2, "\t generates an abstraction of the function\n" ); + Abc_Print( -2, "\t-K num : the number of primary inputs [default = %d]\n", nVars ); + Abc_Print( -2, "\t-R num : the number of random K-set to try [default = %d]\n", nRands ); + Abc_Print( -2, "\t-p : toggles printing statistics only [default = %s]\n", fPrint ? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the index list of primary inputs to be abstrated\n"); + return 1; +} + + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/io.c b/src/base/io/io.c index 55a02dee2..fa7a961a5 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1060,7 +1060,15 @@ usage: fprintf( pAbc->Err, "\t-x : toggle reading Exclusive SOP rather than SOP [default = %s]\n", fSkipPrepro? "yes":"no" ); fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); - fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n\n" ); + fprintf( pAbc->Err, "\t Please note that the PLA parser is somewhat slow for large SOPs.\n" ); + fprintf( pAbc->Err, "\t On the other hand, BLIF parser reads a 3M SOP and converts it into a 7.5K AIG in 1 sec:\n" ); + fprintf( pAbc->Err, "\t abc 16> read test.blif; ps; bdd -s; ps; muxes; strash; ps\n" ); + fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 nd = 1 edge = 25 cube = 2910537 lev = 1\n" ); + fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 nd = 1 edge = 25 bdd = 2937 lev = 1\n" ); + fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 and = 7514 lev = 48\n" ); + fprintf( pAbc->Err, "\t abc 19> time\n" ); + fprintf( pAbc->Err, "\t elapse: 1.05 seconds, total: 1.05 seconds\n" ); return 1; }