luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

&mfs: Handle blackboxes robustly 

When the network is being handed over to the "sfm" core, all blackboxes
are modeled by inserting new PIs, POs, and those being connected by
buffers to the nodes representing the CIs, COs. Make two changes:

 * Robustly deny the fake PIs from being considered when shopping for
   LUT fanin substitutions. Such reconnection occurring would trip up
   the code reintegrating the result.

 * Make sure the buffer connecting the fake-PO to the CO doesn't get
   rewritten as part of the `mfs` transformation, and extend this
   protection to any whitebox models.
This commit is contained in:
Martin Povišer 2024-03-22 22:42:43 +01:00
parent fda490235e
commit d7fc8fe98f
6 changed files with 26 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/aig/gia/giaMfs.c
View File

@ -58,6 +58,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
Vec_Wec_t * vFanins; // mfs data Vec_Wec_t * vFanins; // mfs data
Vec_Str_t * vFixed; // mfs data Vec_Str_t * vFixed; // mfs data
Vec_Str_t * vEmpty; // mfs data Vec_Str_t * vEmpty; // mfs data
Vec_Str_t * vDenied; // mfs data
Vec_Wrd_t * vTruths; // mfs data Vec_Wrd_t * vTruths; // mfs data
Vec_Int_t * vArray; Vec_Int_t * vArray;
Vec_Int_t * vStarts; Vec_Int_t * vStarts;
@ -81,9 +82,14 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
vFanins = Vec_WecStart( nMfsVars ); vFanins = Vec_WecStart( nMfsVars );
vFixed = Vec_StrStart( nMfsVars ); vFixed = Vec_StrStart( nMfsVars );
vEmpty = Vec_StrStart( nMfsVars ); vEmpty = Vec_StrStart( nMfsVars );
vDenied = Vec_StrStart( nMfsVars );
vTruths = Vec_WrdStart( nMfsVars ); vTruths = Vec_WrdStart( nMfsVars );
vStarts = Vec_IntStart( nMfsVars ); vStarts = Vec_IntStart( nMfsVars );
vTruths2 = Vec_WrdAlloc( 10000 ); vTruths2 = Vec_WrdAlloc( 10000 );
// deny the PIs which are modeling blackbox outputs from being considered
// in substitutions
for (int i = 0; i < nBbOuts; i++)
Vec_StrWriteEntry( vDenied, i, (char)1 );
// set internal PIs // set internal PIs
Gia_ManCleanCopyArray( p ); Gia_ManCleanCopyArray( p );
Gia_ManForEachCiId( p, Id, i ) Gia_ManForEachCiId( p, Id, i )
@ -232,6 +238,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
Vec_IntFill( vArray, 1, iBbOut++ ); Vec_IntFill( vArray, 1, iBbOut++ );
Vec_StrWriteEntry( vFixed, Counter, (char)1 ); Vec_StrWriteEntry( vFixed, Counter, (char)1 );
Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); Vec_StrWriteEntry( vEmpty, Counter, (char)1 );
Vec_StrWriteEntry( vDenied, Counter, (char)1 );
Vec_WrdWriteEntry( vTruths, Counter, uTruths6[0] ); Vec_WrdWriteEntry( vTruths, Counter, uTruths6[0] );
} }
for ( i = 0; i < nBoxIns; i++ ) for ( i = 0; i < nBoxIns; i++ )
@ -240,7 +247,9 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
pObj = Gia_ManCo( p, curCo + i ); pObj = Gia_ManCo( p, curCo + i );
Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
// connect it with the special primary output (iBbIn) // connect it with the special primary output (iBbIn)
vArray = Vec_WecEntry( vFanins, nMfsVars - nBbIns + iBbIn++ ); int poNum = nMfsVars - nBbIns + iBbIn++;
vArray = Vec_WecEntry( vFanins, poNum );
Vec_StrWriteEntry( vFixed, poNum, (char)1 );
assert( Vec_IntSize(vArray) == 0 ); assert( Vec_IntSize(vArray) == 0 );
Vec_IntFill( vArray, 1, Counter ); Vec_IntFill( vArray, 1, Counter );
} }
@ -268,7 +277,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
} }
// finalize // finalize
Vec_IntFree( vLeaves ); Vec_IntFree( vLeaves );
return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths, vStarts, vTruths2 ); return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vDenied, vTruths, vStarts, vTruths2 );
} }
/**Function************************************************************* /**Function*************************************************************

4
src/base/abci/abcMfs.c
View File

@ -216,7 +216,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
// for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ ) // for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ )
// if ( rand() % 10 == 0 ) // if ( rand() % 10 == 0 )
// Vec_StrWriteEntry( vFixed, i, (char)1 ); // Vec_StrWriteEntry( vFixed, i, (char)1 );
return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 );
} }
Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot )
{ {
@ -285,7 +285,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot )
Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkForEachNode( pNtk, pObj, i )
if ( i >= iPivot ) if ( i >= iPivot )
Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 ); Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 );
return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 );
} }
/**Function************************************************************* /**Function*************************************************************

2
src/opt/sfm/sfm.h
View File

@ -89,7 +89,7 @@ struct Sfm_Par_t_
extern void Sfm_ParSetDefault( Sfm_Par_t * pPars ); extern void Sfm_ParSetDefault( Sfm_Par_t * pPars );
extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
/*=== sfmNtk.c ==========================================================*/ /*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 );
extern void Sfm_NtkFree( Sfm_Ntk_t * p ); extern void Sfm_NtkFree( Sfm_Ntk_t * p );
extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );

12
src/opt/sfm/sfmCore.c
View File

@ -115,7 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
int fSkipUpdate = 0; int fSkipUpdate = 0;
int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
int i, iFanin, iVar = -1; int i, iFanin, iVar = -1;
int iFaninRem = -1, iFaninSkip = -1; int iFaninRem = -1;
int nFanins = Sfm_ObjFaninNum(p, iNode); int nFanins = Sfm_ObjFaninNum(p, iNode);
word uTruth, uSign, uMask; word uTruth, uSign, uMask;
abctime clk; abctime clk;
@ -138,9 +138,6 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
else else
iFaninRem = iFanin; iFaninRem = iFanin;
assert( iFaninRem != -1 ); assert( iFaninRem != -1 );
// find fanin to skip
if ( Sfm_ObjIsFixed(p, iFaninRem) && Sfm_ObjFaninNum(p, iFaninRem) == 1 )
iFaninSkip = Sfm_ObjFanin(p, iFaninRem, 0);
clk = Abc_Clock(); clk = Abc_Clock();
uTruth = Sfm_ComputeInterpolant( p ); uTruth = Sfm_ComputeInterpolant( p );
p->timeSat += Abc_Clock() - clk; p->timeSat += Abc_Clock() - clk;
@ -176,11 +173,10 @@ p->timeSat += Abc_Clock() - clk;
// find the next divisor to try // find the next divisor to try
uMask = (~(word)0) >> (64 - p->nCexes); uMask = (~(word)0) >> (64 - p->nCexes);
Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar ) Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar )
if ( uSign == uMask && Vec_IntEntry(p->vDivs, iVar) != iFaninSkip ) if ( uSign == uMask && !Sfm_ObjIsDenied(p, Vec_IntEntry(p->vDivs, iVar)) )
break; break;
if ( iVar == Vec_IntSize(p->vDivs) ) if ( iVar == Vec_IntSize(p->vDivs) )
return 0; return 0;
assert( Vec_IntEntry(p->vDivs, iVar) != iFaninSkip );
// try replacing the critical fanin // try replacing the critical fanin
Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) ); Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
clk = Abc_Clock(); clk = Abc_Clock();
@ -289,6 +285,10 @@ p->timeSat += Abc_Clock() - clk;
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{ {
int i, iFanin; int i, iFanin;
if (Sfm_NodeReadFixed(p, iNode))
return 0;
p->nNodesTried++; p->nNodesTried++;
// prepare SAT solver // prepare SAT solver
if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) ) if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )

2
src/opt/sfm/sfmInt.h
View File

@ -81,6 +81,7 @@ struct Sfm_Ntk_t_
// user data // user data
Vec_Str_t * vFixed; // persistent objects Vec_Str_t * vFixed; // persistent objects
Vec_Str_t * vEmpty; // transparent objects Vec_Str_t * vEmpty; // transparent objects
Vec_Str_t * vDenied; // denied objects
Vec_Wrd_t * vTruths; // truth tables Vec_Wrd_t * vTruths; // truth tables
Vec_Wec_t vFanins; // fanins Vec_Wec_t vFanins; // fanins
Vec_Int_t * vStarts; // offsets Vec_Int_t * vStarts; // offsets
@ -157,6 +158,7 @@ static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return
static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; } static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; }
static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; } static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; }
static inline int Sfm_ObjIsFixed( Sfm_Ntk_t * p, int i ) { return Vec_StrEntry(p->vFixed, i); } static inline int Sfm_ObjIsFixed( Sfm_Ntk_t * p, int i ) { return Vec_StrEntry(p->vFixed, i); }
static inline int Sfm_ObjIsDenied( Sfm_Ntk_t * p, int i ) { return p->vDenied && Vec_StrEntry(p->vDenied, i); }
static inline int Sfm_ObjAddsLevelArray( Vec_Str_t * p, int i ) { return p == NULL || Vec_StrEntry(p, i) == 0; } static inline int Sfm_ObjAddsLevelArray( Vec_Str_t * p, int i ) { return p == NULL || Vec_StrEntry(p, i) == 0; }
static inline int Sfm_ObjAddsLevel( Sfm_Ntk_t * p, int i ) { return Sfm_ObjAddsLevelArray(p->vEmpty, i); } static inline int Sfm_ObjAddsLevel( Sfm_Ntk_t * p, int i ) { return Sfm_ObjAddsLevelArray(p->vEmpty, i); }

6
src/opt/sfm/sfmNtk.c
View File

@ -58,7 +58,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
assert( Fanin + nPos < Vec_WecSize(vFanins) ); assert( Fanin + nPos < Vec_WecSize(vFanins) );
// POs have one fanout // POs have one fanout
if ( i + nPos >= Vec_WecSize(vFanins) ) if ( i + nPos >= Vec_WecSize(vFanins) )
assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 ); assert( Vec_IntSize(vArray) == 1 );
} }
} }
@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
{ {
Sfm_Ntk_t * p; int i; Sfm_Ntk_t * p; int i;
Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
@ -177,6 +177,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
p->vFixed = vFixed; p->vFixed = vFixed;
p->vEmpty = vEmpty; p->vEmpty = vEmpty;
p->vTruths = vTruths; p->vTruths = vTruths;
p->vDenied = vDenied;
p->vFanins = *vFanins; p->vFanins = *vFanins;
p->vStarts = vStarts; p->vStarts = vStarts;
p->vTruths2 = vTruths2; p->vTruths2 = vTruths2;
@ -221,6 +222,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
// user data // user data
Vec_StrFree( p->vFixed ); Vec_StrFree( p->vFixed );
Vec_StrFreeP( &p->vEmpty ); Vec_StrFreeP( &p->vEmpty );
Vec_StrFreeP( &p->vDenied );
Vec_WrdFree( p->vTruths ); Vec_WrdFree( p->vTruths );
Vec_WecErase( &p->vFanins ); Vec_WecErase( &p->vFanins );
Vec_IntFree( p->vStarts ); Vec_IntFree( p->vStarts );