Skip to content

Commit 0b1d7c6

Browse files
alanminkoalanminko
committed
Supporting structural choices in rewiring.
1 parent 5daa0c3 commit 0b1d7c6

File tree

8 files changed

+268
-19
lines changed

8 files changed

+268
-19
lines changed

‎src/aig/gia/gia.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1413,6 +1413,10 @@ extern Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p );
14131413
extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
14141414
extern int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
14151415
extern void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla );
1416+
typedef struct Gia_ChMan_t_ Gia_ChMan_t;
1417+
extern Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia );
1418+
extern void Gia_ManDupChoicesAdd( Gia_ChMan_t * pMan, Gia_Man_t * pGia );
1419+
extern Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * pMan );
14161420
/*=== giaEdge.c ==========================================================*/
14171421
extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray );
14181422
extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p );

‎src/aig/gia/giaDup.c‎

Lines changed: 209 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@
2222
#include "misc/tim/tim.h"
2323
#include "misc/vec/vecWec.h"
2424
#include "proof/cec/cec.h"
25+
#include "misc/util/utilTruth.h"
2526

2627
ABC_NAMESPACE_IMPL_START
2728

@@ -6269,6 +6270,214 @@ Gia_Man_t * Gia_ManDupFanouts( Gia_Man_t * p )
62696270
return pNew;
62706271
}
62716272

6273+
/**Function*************************************************************
6274+
6275+
Synopsis [Reorders choice nodes.]
6276+
6277+
Description []
6278+
6279+
SideEffects []
6280+
6281+
SeeAlso []
6282+
6283+
***********************************************************************/
6284+
void Gia_ManPrintChoices( Gia_Man_t * p )
6285+
{
6286+
Gia_Obj_t * pObj; int i;
6287+
Gia_ManForEachAnd( p, pObj, i )
6288+
if ( p->pSibls[i] )
6289+
printf( "%d -> %d\n", i, p->pSibls[i] );
6290+
}
6291+
void Gia_ManReorderChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
6292+
{
6293+
if ( ~pObj->Value )
6294+
return;
6295+
assert( Gia_ObjIsAnd(pObj) );
6296+
Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj));
6297+
Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
6298+
Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
6299+
if ( pSibl ) Gia_ManReorderChoices_rec( pNew, p, pSibl );
6300+
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
6301+
if ( pSibl ) {
6302+
int iObjNew = Abc_Lit2Var(pObj->Value);
6303+
int iNextNew = Abc_Lit2Var(pSibl->Value);
6304+
assert( iObjNew > iNextNew );
6305+
assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
6306+
pNew->pSibls[iObjNew] = iNextNew;
6307+
}
6308+
}
6309+
Gia_Man_t * Gia_ManReorderChoices( Gia_Man_t * p )
6310+
{
6311+
assert( p->pSibls );
6312+
Gia_Obj_t * pObj; int i;
6313+
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) );
6314+
pNew->pName = Abc_UtilStrsav( p->pName );
6315+
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
6316+
pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
6317+
Gia_ManFillValue(p);
6318+
Gia_ManForEachCi( p, pObj, i )
6319+
pObj->Value = Gia_ManAppendCi(pNew);
6320+
Gia_ManForEachCo( p, pObj, i )
6321+
Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
6322+
Gia_ManForEachCo( p, pObj, i )
6323+
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
6324+
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
6325+
extern int Gia_ManTestChoices( Gia_Man_t * p );
6326+
Gia_ManTestChoices( pNew );
6327+
//Gia_ManPrintChoices( pNew );
6328+
return pNew;
6329+
}
6330+
6331+
6332+
/**Function*************************************************************
6333+
6334+
Synopsis [Duplicates AIGs while creating choices.]
6335+
6336+
Description []
6337+
6338+
SideEffects []
6339+
6340+
SeeAlso []
6341+
6342+
***********************************************************************/
6343+
6344+
struct Gia_ChMan_t_
6345+
{
6346+
Gia_Man_t * pNew;
6347+
Vec_Mem_t * vTtMem;
6348+
Vec_Int_t * vSibls;
6349+
Vec_Int_t * vObj2Tt;
6350+
Vec_Int_t * vTt2Obj;
6351+
Vec_Int_t * vCoLits;
6352+
word * pTruth;
6353+
int nWords;
6354+
};
6355+
6356+
int Gia_ManDupChoicesMark_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vObj2Tt, int iFunc )
6357+
{
6358+
if ( Abc_Lit2Var(Vec_IntEntry(vObj2Tt, iObj)) == iFunc )
6359+
return 1;
6360+
if ( Gia_ObjIsTravIdCurrentId(pGia, iObj) )
6361+
return 0;
6362+
Gia_ObjSetTravIdCurrentId(pGia, iObj);
6363+
Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj);
6364+
if ( !Gia_ObjIsAnd(pObj) )
6365+
return 0;
6366+
if ( Gia_ManDupChoicesMark_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vObj2Tt, iFunc ) )
6367+
return 1;
6368+
if ( Gia_ManDupChoicesMark_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vObj2Tt, iFunc ) )
6369+
return 1;
6370+
return 0;
6371+
}
6372+
int Gia_ManDupChoicesMark( Gia_Man_t * pGia, int iLit0, int iLit1, Vec_Int_t * vObj2Tt, int iFunc )
6373+
{
6374+
Gia_ManIncrementTravId( pGia );
6375+
if ( Gia_ManDupChoicesMark_rec( pGia, Abc_Lit2Var(iLit0), vObj2Tt, iFunc ) )
6376+
return 1;
6377+
if ( Gia_ManDupChoicesMark_rec( pGia, Abc_Lit2Var(iLit1), vObj2Tt, iFunc ) )
6378+
return 1;
6379+
return 0;
6380+
}
6381+
void Gia_ManDupChoicesNode( Gia_ChMan_t * p, Gia_Man_t * pGia, int iObj )
6382+
{
6383+
Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj );
6384+
assert( ~Gia_ObjFanin0(pObj)->Value && ~Gia_ObjFanin1(pObj)->Value );
6385+
int obLits[2] = { Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) };
6386+
int ttLits[2] = { Vec_IntEntry(p->vObj2Tt, Abc_Lit2Var(obLits[0])), Vec_IntEntry(p->vObj2Tt, Abc_Lit2Var(obLits[1])) };
6387+
int fCompl[2] = { Abc_LitIsCompl(ttLits[0]) ^ Abc_LitIsCompl(obLits[0]), Abc_LitIsCompl(ttLits[1]) ^ Abc_LitIsCompl(obLits[1]) };
6388+
word * pTruth[2] = { Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(ttLits[0])), Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(ttLits[1])) };
6389+
Abc_TtAndCompl( p->pTruth, pTruth[0], fCompl[0], pTruth[1], fCompl[1], p->nWords );
6390+
int fComp = (int)p->pTruth[0] & 1; if ( fComp ) Abc_TtNot( p->pTruth, p->nWords );
6391+
int nFuncs = Vec_MemEntryNum( p->vTtMem );
6392+
int iFunc = Vec_MemHashInsert( p->vTtMem, p->pTruth );
6393+
assert( iFunc <= nFuncs );
6394+
if ( iFunc == nFuncs ) { // new function
6395+
pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
6396+
Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(iFunc, fComp ^ Abc_LitIsCompl(pObj->Value)) );
6397+
Vec_IntPush( p->vTt2Obj, Abc_Lit2Var(pObj->Value) );
6398+
return;
6399+
}
6400+
int iRepr = Vec_IntEntry( p->vTt2Obj, iFunc );
6401+
pObj->Value = Abc_Var2Lit( iRepr, fComp ^ Abc_LitIsCompl(Vec_IntEntry(p->vObj2Tt, iRepr)) );
6402+
if ( iRepr <= Gia_ManCiNum(pGia) || Gia_ManDupChoicesMark(p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj), p->vObj2Tt, iFunc) )
6403+
return;
6404+
int nObjNew = Gia_ManObjNum(p->pNew);
6405+
int iLitNew = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
6406+
if ( Abc_Lit2Var(iLitNew) == nObjNew )
6407+
Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(iFunc, fComp ^ Abc_LitIsCompl(iLitNew)) );
6408+
}
6409+
void Gia_ManDupChoicesAdd( Gia_ChMan_t * p, Gia_Man_t * pGia )
6410+
{
6411+
Gia_Obj_t * pObj; int i;
6412+
assert( Gia_ManCiNum(p->pNew) == Gia_ManCiNum(pGia) );
6413+
assert( !p->vCoLits || Vec_IntSize(p->vCoLits) == Gia_ManCoNum(pGia) );
6414+
assert( Gia_ManRegNum(p->pNew) == Gia_ManRegNum(pGia) );
6415+
Gia_ManFillValue( pGia );
6416+
Gia_ManForEachCi( pGia, pObj, i )
6417+
pObj->Value = Gia_ManCiLit( p->pNew, i );
6418+
Gia_ManForEachAnd( pGia, pObj, i )
6419+
Gia_ManDupChoicesNode( p, pGia, i );
6420+
assert( Vec_IntSize(p->vObj2Tt) == Gia_ManObjNum(p->pNew) );
6421+
assert( Vec_IntSize(p->vTt2Obj) == Vec_MemEntryNum(p->vTtMem) );
6422+
}
6423+
Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia )
6424+
{
6425+
Gia_ChMan_t * p = ABC_CALLOC( Gia_ChMan_t, 1 );
6426+
p->pNew = Gia_ManStart( 10*Gia_ManObjNum(pGia) );
6427+
p->pNew->pName = Abc_UtilStrsav( pGia->pName );
6428+
p->pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
6429+
p->vTtMem = Vec_MemAllocWithTTs( Gia_ManCiNum(pGia) );
6430+
p->vTt2Obj = Vec_IntStartNatural( 1 + Gia_ManCiNum(pGia) );
6431+
p->vObj2Tt = Vec_IntAlloc( 10*Gia_ManObjNum(pGia) );
6432+
p->nWords = Abc_TtWordNum( Gia_ManCiNum(pGia) );
6433+
p->pTruth = ABC_CALLOC( word, p->nWords );
6434+
Gia_Obj_t * pObj; int i;
6435+
for ( i = 0; i <= Gia_ManCiNum(pGia); i++ )
6436+
Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(i, 0) );
6437+
Gia_ManForEachCi( pGia, pObj, i )
6438+
Gia_ManAppendCi(p->pNew);
6439+
Gia_ManSetRegNum( p->pNew, Gia_ManRegNum(pGia) );
6440+
Gia_ManHashStart( p->pNew );
6441+
Gia_ManDupChoicesAdd( p, pGia );
6442+
p->vCoLits = Vec_IntAlloc( Gia_ManCoNum(pGia) );
6443+
Gia_ManForEachCo( pGia, pObj, i )
6444+
Vec_IntPush( p->vCoLits, Gia_ObjFanin0Copy(pObj) );
6445+
return p;
6446+
}
6447+
Vec_Int_t * Gia_ManDupChoicesCreateSibls( Gia_ChMan_t * p )
6448+
{
6449+
int iObj, ttLit;
6450+
Vec_Int_t * vSibls = Vec_IntStart( Gia_ManObjNum(p->pNew) );
6451+
assert( Vec_IntSize(p->vTt2Obj) == Vec_MemEntryNum(p->vTtMem) );
6452+
Vec_IntForEachEntry( p->vObj2Tt, ttLit, iObj ) {
6453+
int iPrev = Vec_IntEntry(p->vTt2Obj, Abc_Lit2Var(ttLit));
6454+
assert( iPrev <= iObj );
6455+
if ( iPrev == iObj )
6456+
continue;
6457+
Vec_IntWriteEntry( vSibls, iPrev, iObj );
6458+
Vec_IntWriteEntry( p->vTt2Obj, Abc_Lit2Var(ttLit), iObj );
6459+
}
6460+
return vSibls;
6461+
}
6462+
Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * p )
6463+
{
6464+
Gia_Man_t * pTemp, * pNew = p->pNew; int i, iLit;
6465+
p->vSibls = Gia_ManDupChoicesCreateSibls( p );
6466+
p->pNew->pSibls = Vec_IntReleaseArray( p->vSibls );
6467+
Vec_IntForEachEntry( p->vCoLits, iLit, i )
6468+
Gia_ManAppendCo( p->pNew, iLit );
6469+
Vec_MemFree( p->vTtMem );
6470+
Vec_IntFree( p->vSibls );
6471+
Vec_IntFree( p->vTt2Obj );
6472+
Vec_IntFree( p->vObj2Tt );
6473+
Vec_IntFree( p->vCoLits );
6474+
ABC_FREE( p->pTruth );
6475+
ABC_FREE( p );
6476+
pTemp = Gia_ManReorderChoices( pNew );
6477+
Gia_ManStop( pNew );
6478+
return pTemp;
6479+
}
6480+
62726481
////////////////////////////////////////////////////////////////////////
62736482
/// END OF FILE ///
62746483
////////////////////////////////////////////////////////////////////////

‎src/base/abci/abc.c‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46597,14 +46597,14 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
4659746597
***********************************************************************/
4659846598
int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
4659946599
{
46600-
extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose);
46600+
extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose);
4660146601
FILE *pFile = NULL;
4660246602
Gia_Man_t *pTemp, *pExc = NULL;
46603-
int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0;
46603+
int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0, fChoices = 0;
4660446604
float nLevelGrowRatio = 0;
4660546605
Extra_UtilGetoptReset();
4660646606

46607-
while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVch" ) ) != EOF ) {
46607+
while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVcsh" ) ) != EOF ) {
4660846608
switch ( c ) {
4660946609
case 'I':
4661046610
if ( globalUtilOptind >= argc )
@@ -46733,6 +46733,9 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
4673346733
case 'c':
4673446734
fCheck ^= 1;
4673546735
break;
46736+
case 's':
46737+
fChoices ^= 1;
46738+
break;
4673646739
case 'h':
4673746740
default:
4673846741
goto usage;
@@ -46754,14 +46757,14 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
4675446757
return 1;
4675546758
}
4675646759

46757-
pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, nVerbose );
46760+
pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fChoices, nVerbose );
4675846761
if ( pExc )
4675946762
Gia_ManStop( pExc );
4676046763
Abc_FrameUpdateGia( pAbc, pTemp );
4676146764
return 0;
4676246765

4676346766
usage:
46764-
Abc_Print( -2, "usage: &rewire [-IEGDFLRMASTV <num>]\n" );
46767+
Abc_Print( -2, "usage: &rewire [-IEGDFLRMASTV <num>] [-csh]\n" );
4676546768
Abc_Print( -2, "\t performs AIG re-wiring\n" );
4676646769
Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n", nIters );
4676746770
Abc_Print( -2, "\t-E <num> : the number of fanins to add to all nodes [default = %d]\n", nExpands );
@@ -46777,6 +46780,7 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
4677746780
Abc_Print( -2, "\t-T <num> : the timeout in seconds (0: unlimited) [default = %d]\n", nTimeOut );
4677846781
Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n", nVerbose );
4677946782
Abc_Print( -2, "\t-c : check the equivalence [default = %s]\n", fCheck ? "yes" : "no" );
46783+
Abc_Print( -2, "\t-s : toggle accumulating structural choices [default = %s]\n", fChoices ? "yes" : "no" );
4678046784
Abc_Print( -2, "\t-h : prints the command usage\n" );
4678146785
Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" );
4678246786
return 1;

‎src/misc/vec/vecMem.h‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,6 +420,32 @@ static inline Vec_Mem_t * Vec_MemAllocForTT( int nVars, int fCompl )
420420
ABC_FREE( uTruth );
421421
return vTtMem;
422422
}
423+
static inline Vec_Mem_t * Vec_MemAllocWithTTs( int nVars )
424+
{
425+
static word sTruths6[6] = {
426+
ABC_CONST(0xAAAAAAAAAAAAAAAA),
427+
ABC_CONST(0xCCCCCCCCCCCCCCCC),
428+
ABC_CONST(0xF0F0F0F0F0F0F0F0),
429+
ABC_CONST(0xFF00FF00FF00FF00),
430+
ABC_CONST(0xFFFF0000FFFF0000),
431+
ABC_CONST(0xFFFFFFFF00000000)
432+
};
433+
Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars );
434+
int i, k, nWords = nVars <= 6 ? 1 : (1 << (nVars - 6));
435+
word * pTruth = ABC_CALLOC( word, nWords );
436+
int Value = Vec_MemHashInsert( vTtMem, pTruth ); assert( Value == 0 );
437+
for ( i = 0; i < nVars; i++ ) {
438+
if ( i < 6 )
439+
for ( k = 0; k < nWords; k++ )
440+
pTruth[k] = sTruths6[i];
441+
else
442+
for ( k = 0; k < nWords; k++ )
443+
pTruth[k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
444+
Value = Vec_MemHashInsert( vTtMem, pTruth ); assert( Value == 1+i );
445+
}
446+
ABC_FREE( pTruth );
447+
return vTtMem;
448+
}
423449
static inline void Vec_MemAddMuxTT( Vec_Mem_t * p, int nVars )
424450
{
425451
int Value, nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));

0 commit comments

Comments
 (0)