Skip to content

Commit

Permalink
Implementation of functional abstraction.
Browse files Browse the repository at this point in the history
  • Loading branch information
@alanminko
alanminko committed Jul 25, 2024
1 parent 6262dcf commit f8a6432
Show file tree
Hide file tree
Showing 3 changed files with 298 additions and 2 deletions.
176 changes: 176 additions & 0 deletions src/aig/gia/giaDup.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ///
////////////////////////////////////////////////////////////////////////
Expand Down
114 changes: 113 additions & 1 deletion src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -53468,6 +53470,116 @@ int Abc_CommandAbc9Window( Abc_Frame_t * pAbc, int argc, char ** argv )
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] <node1> <node2> ... <nodeN>\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<nodes> : the index list of primary inputs to be abstrated\n");
return 1;
}


/**Function*************************************************************

Synopsis []
Expand Down
10 changes: 9 additions & 1 deletion src/base/io/io.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1060,7 +1060,15 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
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;
}

Expand Down

0 comments on commit f8a6432

Please sign in to comment.