Skip to content

A
abc
Commit 96d3348d by Alan Mishchenko
Options

Fixing out-of-bound problem when collecting GIA nodes.

parent f829eca5
Showing with 156 additions and 34 deletions
src/aig/gia/gia.h
......@@ -889,7 +889,7 @@ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
/*=== giaTruth.c ===========================================================*/
extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax );
extern void Gia_ObjComputeTruthTableStop( Gia_Man_t * p );
......
src/aig/gia/giaTruth.c
......@@ -105,23 +105,28 @@ word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSu
SeeAlso []
***********************************************************************/
void Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
int Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( !Gia_ObjIsAnd(pObj) )
return;
return 0;
if ( pObj->fMark0 )
return;
return 0;
pObj->fMark0 = 1;
Gia_ObjCollectInternal_rec( p, Gia_ObjFanin0(pObj) );
Gia_ObjCollectInternal_rec( p, Gia_ObjFanin1(pObj) );
if ( Vec_IntSize(p->vTtNodes) > 253 )
return 1;
Gia_ObjSetNum( p, pObj, Vec_IntSize(p->vTtNodes) );
Vec_IntPush( p->vTtNodes, Gia_ObjId(p, pObj) );
return 0;
}
void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int RetValue;
Vec_IntClear( p->vTtNodes );
Gia_ObjCollectInternal_rec( p, pObj );
RetValue = Gia_ObjCollectInternal_rec( p, pObj );
assert( Vec_IntSize(p->vTtNodes) < 254 );
return RetValue;
}
/**Function*************************************************************
......@@ -158,7 +163,12 @@ unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
}
// collect internal nodes
pRoot = Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj;
Gia_ObjCollectInternal( p, pRoot );
if ( Gia_ObjCollectInternal( p, pRoot ) )
{
Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
pTemp->fMark0 = 0;
return NULL;
}
// compute the truth table for internal nodes
Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
{
......
src/base/abci/abcRec3.c
......@@ -611,6 +611,11 @@ int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
clk = clock();
If_CutTraverse( pIfMan, pRoot, pCut, vNodes );
p->timeTruth += clock() - clk;
if ( Vec_PtrSize(vNodes) > 253 )
{
p->nFilterSize++;
return 1;
}
// semi-canonicize truth table
clk = clock();
......
src/opt/dau/dauDsd.c
......@@ -27,17 +27,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define DAU_MAX_STR 300
static word s_Truth6[6] =
{
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
#define DAU_MAX_STR 256
/*
This code performs truth-table-based decomposition for 6-variable functions.
......@@ -85,7 +75,7 @@ word Dau_DsdToTruth_rec( char ** p )
if ( **p == '!' )
(*p)++, fCompl = 1;
if ( **p >= 'a' && **p <= 'f' )
return fCompl ? ~s_Truth6[**p - 'a'] : s_Truth6[**p - 'a'];
return fCompl ? ~s_Truths6[**p - 'a'] : s_Truths6[**p - 'a'];
if ( **p == '(' || **p == '[' || **p == '<' )
{
word Res = 0;
......@@ -197,12 +187,12 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
// special case when function is a var
if ( nVarsNew == 1 )
{
if ( t == s_Truth6[ pVarsNew[0] ] )
if ( t == s_Truths6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = 'a' + pVarsNew[0];
return Pos;
}
if ( t == ~s_Truth6[ pVarsNew[0] ] )
if ( t == ~s_Truths6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[0];
......@@ -274,7 +264,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
{
PosStart = Pos;
sprintf( pNest, "(%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[3]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[3]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
......@@ -282,7 +272,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
{
PosStart = Pos;
sprintf( pNest, "(%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[2]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[2]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
......@@ -290,7 +280,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
{
PosStart = Pos;
sprintf( pNest, "(!%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[1]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
......@@ -298,7 +288,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
{
PosStart = Pos;
sprintf( pNest, "(!%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[0]) | (~s_Truth6[pVarsNew[u]] & Cof[1]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[0]) | (~s_Truths6[pVarsNew[u]] & Cof[1]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
......@@ -306,7 +296,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
{
PosStart = Pos;
sprintf( pNest, "[%c%c]", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truth6[pVarsNew[u]] & Cof[1]) | (~s_Truth6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
......@@ -408,16 +398,16 @@ char * Dau_DsdPerform( word t )
***********************************************************************/
void Dau_DsdTest()
{
// word t = s_Truth6[0] & s_Truth6[1] & s_Truth6[2];
// word t = ~s_Truth6[0] | (s_Truth6[1] ^ ~s_Truth6[2]);
// word t = (s_Truth6[1] & s_Truth6[2]) | (s_Truth6[0] & s_Truth6[3]);
// word t = (~s_Truth6[1] & ~s_Truth6[2]) | (s_Truth6[0] ^ s_Truth6[3]);
// word t = ((~s_Truth6[1] & ~s_Truth6[2]) | (s_Truth6[0] ^ s_Truth6[3])) ^ s_Truth6[5];
// word t = ((s_Truth6[1] & ~s_Truth6[2]) ^ (s_Truth6[0] & s_Truth6[3])) & s_Truth6[5];
// word t = (~(~s_Truth6[0] & ~s_Truth6[4]) & s_Truth6[2]) | (~s_Truth6[1] & ~s_Truth6[0] & ~s_Truth6[4]);
// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
// word t = ~s_Truths6[0] | (s_Truths6[1] ^ ~s_Truths6[2]);
// word t = (s_Truths6[1] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3]);
// word t = (~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3]);
// word t = ((~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3])) ^ s_Truths6[5];
// word t = ((s_Truths6[1] & ~s_Truths6[2]) ^ (s_Truths6[0] & s_Truths6[3])) & s_Truths6[5];
// word t = (~(~s_Truths6[0] & ~s_Truths6[4]) & s_Truths6[2]) | (~s_Truths6[1] & ~s_Truths6[0] & ~s_Truths6[4]);
// word t = 0x0000000000005F3F;
// word t = 0xF3F5030503050305;
// word t = (s_Truth6[0] & s_Truth6[1] & (s_Truth6[2] ^ s_Truth6[4])) | (~s_Truth6[0] & ~s_Truth6[1] & ~(s_Truth6[2] ^ s_Truth6[4]));
// word t = (s_Truths6[0] & s_Truths6[1] & (s_Truths6[2] ^ s_Truths6[4])) | (~s_Truths6[0] & ~s_Truths6[1] & ~(s_Truths6[2] ^ s_Truths6[4]));
// word t = 0x05050500f5f5f5f3;
word t = 0x9ef7a8d9c7193a0f;
char * p = Dau_DsdPerform( t );
......@@ -710,6 +700,123 @@ char * Dau_DsdRun( word * p, int nVars )
return pBuffer;
}
typedef struct Dau_Dsd_t_ Dau_Dsd_t;
struct Dau_Dsd_t_
{
int nVarsInit; // the initial number of variables
int nVarsUsed; // the current number of variables
char pVarDefs[32][8]; // variable definitions
char pOutput[DAU_MAX_STR]; // output stream
int nPos; // writing position
};
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dua_DsdInit( Dau_Dsd_t * p, int nVarsInit )
{
int i;
memset( p, 0, sizeof(Dau_Dsd_t) );
p->nVarsInit = p->nVarsUsed = nVarsInit;
for ( i = 0; i < nVarsInit; i++ )
p->pVarDefs[i][0] = 'a';
}
void Dua_DsdWrite( Dau_Dsd_t * p, char * pStr )
{
while ( *pStr )
p->pOutput[ p->nPos++ ] = *pStr++;
}
void Dua_DsdWriteInv( Dau_Dsd_t * p, int Cond )
{
if ( Cond )
p->pOutput[ p->nPos++ ] = '!';
}
void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar )
{
char * pStr;
for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
Dua_DsdWriteVar( p, *pStr - 'a' );
else
p->pOutput[ p->nPos++ ] = *pStr;
}
void Dua_DsdWriteStop( Dau_Dsd_t * p )
{
p->pOutput[ p->nPos++ ] = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dua_DsdMinBase( word t, int nVars, int * pVarsNew )
{
int v, nVarsNew = 0;
for ( v = 0; v < nVars; v++ )
if ( Abc_Tt6HasVar( t, v ) )
pVarsNew[nVarsNew++] = v;
return nVarsNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars )
{
}
char * Dau_DsdDecompose( word t, int nVarsInit )
{
Dau_Dsd_t P, * p = &P;
int nVars, pVars[6];
Dua_DsdInit( p, nVarsInit );
if ( t == 0 )
Dua_DsdWrite( p, "0" );
else if ( ~t == 0 )
Dua_DsdWrite( p, "1" );
else
{
nVars = Dua_DsdMinBase( t, nVarsInit, pVars );
assert( nVars > 0 && nVars < 6 );
if ( nVars == 1 )
{
Dua_DsdWriteInv( p, (int)(t & 1) );
Dua_DsdWriteVar( p, pVars[0] );
}
else
Dau_DsdDecomposeInternal( p, t, pVars, nVars );
}
Dua_DsdWriteStop( p );
return p->pOutput;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment