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

Support for representing programmable cell configuration data.

This commit is contained in:
Alan Mishchenko 2015-03-08 20:17:59 -07:00
parent 9e4f8e9fdf
commit 56f783157a
9 changed files with 333 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -131,6 +131,8 @@ struct Gia_Man_t_
Vec_Int_t * vMapping; // mapping for each node Vec_Int_t * vMapping; // mapping for each node
Vec_Int_t * vCellMapping; // mapping for each node Vec_Int_t * vCellMapping; // mapping for each node
Vec_Int_t * vPacking; // packing information Vec_Int_t * vPacking; // packing information
Vec_Int_t * vConfigs; // cell configurations
char * pCellStr; // cell description
Vec_Int_t * vLutConfigs; // LUT configurations Vec_Int_t * vLutConfigs; // LUT configurations
Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexComb; // combinational counter-example
Abc_Cex_t * pCexSeq; // sequential counter-example Abc_Cex_t * pCexSeq; // sequential counter-example

24
src/aig/gia/giaAiger.c
View File

@ -670,6 +670,21 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"r\".\n" ); if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
} }
// read configuration data
else if ( *pCur == 'b' )
{
int nSize;
pCur++;
nSize = Gia_AigerReadInt(pCur);
pCurTemp = pCur + nSize + 4; pCur += 4;
pNew->pCellStr = Abc_UtilStrsav( pCur ); pCur += strlen(pCur) + 1;
nSize = nSize - strlen(pNew->pCellStr) - 1;
assert( nSize % 4 == 0 );
pNew->vConfigs = Vec_IntStart(nSize / 4);
memcpy(Vec_IntArray(pNew->vConfigs), pCur, nSize); pCur += nSize;
assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"b\".\n" );
}
// read choices // read choices
else if ( *pCur == 'q' ) else if ( *pCur == 'q' )
{ {
@ -1267,6 +1282,15 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ ) for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) ); Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
} }
// write configuration data
if ( p->vConfigs )
{
fprintf( pFile, "b" );
assert( p->pCellStr != NULL );
Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vConfigs) + strlen(p->pCellStr) + 1 );
fwrite( p->pCellStr, 1, strlen(p->pCellStr) + 1, pFile );
fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
}
// write choices // write choices
if ( Gia_ManHasChoices(p) ) if ( Gia_ManHasChoices(p) )
{ {

107
src/aig/gia/giaIf.c
View File

@ -1467,9 +1467,54 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int fCompl )
{
If_Obj_t * pIfObj;
word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input
char * pCutPerm = If_CutDsdPerm( pIfMan, pCutBest ); // DSD input -> cut input
word * pArray; int v, i, Lit, Var;
int nVarNum = If_DsdManVarNum(pIfMan->pIfDsdMan);
int nTtBitNum = If_DsdManTtBitNum(pIfMan->pIfDsdMan);
int nPermBitNum = If_DsdManPermBitNum(pIfMan->pIfDsdMan);
int nPermBitOne = nPermBitNum / nVarNum;
// prepare storage
int nIntNum = Vec_IntEntry( vConfigs, 1 );
for ( i = 0; i < nIntNum; i++ )
Vec_IntPush( vConfigs, 0 );
pArray = (word *)Vec_IntEntryP( vConfigs, Vec_IntSize(vConfigs) - nIntNum );
assert( nPermBitNum % nVarNum == 0 );
// set truth table bits
for ( i = 0; i < nTtBitNum; i++ )
if ( Abc_TtGetBit(pPerm + 1, i) )
Abc_TtSetBit( pArray, i );
// set permutation bits
for ( v = 0; v < nVarNum; v++ )
{
// get DSD variable
Var = ((pPerm[0] >> (v * 4)) & 0xF);
assert( Var < (int)pCutBest->nLeaves );
// get AIG literal
Lit = (int)pCutPerm[Var];
assert( Abc_Lit2Var(Lit) < (int)pCutBest->nLeaves );
// complement if polarity has changed
pIfObj = If_ManObj( pIfMan, pCutBest->pLeaves[Abc_Lit2Var(Lit)] );
Lit = Abc_LitNotCond( Lit, Abc_LitIsCompl(pIfObj->iCopy) );
// create config literal
for ( i = 0; i < nPermBitOne; i++ )
if ( (Lit >> i) & 1 )
Abc_TtSetBit( pArray, nTtBitNum + v * nPermBitOne + i );
}
// remember complementation
assert( nTtBitNum + nPermBitNum < 32 * nIntNum );
if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ fCompl )
Abc_TtSetBit( pArray, nTtBitNum + nPermBitNum );
// update count
Vec_IntAddToEntry( vConfigs, 0, 1 );
}
int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vConfigs )
{ {
int iLit; int iLit;
assert( 0 );
if ( Vec_IntSize(vLeaves) <= nLutMax ) if ( Vec_IntSize(vLeaves) <= nLutMax )
iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 ); iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
else else
@ -1478,19 +1523,10 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
int i, Id, iLitTemp; int i, Id, iLitTemp;
// extract variable permutation // extract variable permutation
char * pCutPerm = If_CutDsdPerm( pIfMan, pCutBest ); // DSD input -> cut input char * pCutPerm = If_CutDsdPerm( pIfMan, pCutBest ); // DSD input -> cut input
word Perm = If_DsdManGetFuncPerm( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input
assert( Perm > 0 ); int nBits = If_DsdManTtBitNum( pIfMan->pIfDsdMan );
// (extend storage for configuration bits)
// derive mapping from cell inputs into cut inputs
// retrieve config bits of the LUTs
// perform boolean matching
if ( !If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, If_CutTruthW(pIfMan, pCutBest), Vec_IntSize(vLeaves), Perm, Ifn_NtkInputNum(pNtkCell), vLits ) )
{
printf( "Boolean matching does not exist.\n" );
return -1;
}
// use config bits to generate the network // use config bits to generate the network
iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, vLits, vCover ); iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, pPerm + 1, vLeaves, vCover );
// copy GIA back into the manager // copy GIA back into the manager
Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 ); Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 );
Gia_ObjSetCopyArray( pTemp, 0, 0 ); Gia_ObjSetCopyArray( pTemp, 0, 0 );
@ -1512,15 +1548,12 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
iLit = Abc_LitNotCond( Gia_ObjCopyArray(pTemp, Id), Abc_LitIsCompl(iLit) ); iLit = Abc_LitNotCond( Gia_ObjCopyArray(pTemp, Id), Abc_LitIsCompl(iLit) );
} }
// write packing // write packing
if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 ) // if ( vConfigs && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 )
{ // Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest );
Vec_IntPush( vPacking, 1 );
Vec_IntPush( vPacking, Abc_Lit2Var(iLit) );
Vec_IntAddToEntry( vPacking, 0, 1 );
}
return iLit; return iLit;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Converts IF into GIA manager.] Synopsis [Converts IF into GIA manager.]
@ -1669,23 +1702,31 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Gia_Man_t * pNew, * pHashed = NULL; Gia_Man_t * pNew, * pHashed = NULL;
If_Cut_t * pCutBest; If_Cut_t * pCutBest;
If_Obj_t * pIfObj, * pIfLeaf; If_Obj_t * pIfObj, * pIfLeaf;
Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL, * vConfigs = NULL;
Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
Vec_Int_t * vPiVars = NULL, * vPoVars = NULL;
sat_solver * pSat = NULL;
Ifn_Ntk_t * pNtkCell = NULL; Ifn_Ntk_t * pNtkCell = NULL;
int i, k, nLutMax = -1, Entry; sat_solver * pSat = NULL;
int i, k, Entry, nLutMax = -1; int Count = 0;
assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth ); assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
// if ( pIfMan->pPars->fEnableCheck07 ) // if ( pIfMan->pPars->fEnableCheck07 )
// pIfMan->pPars->fDeriveLuts = 0; // pIfMan->pPars->fDeriveLuts = 0;
// start mapping and packing // start mapping and packing
vMapping = Vec_IntStart( If_ManObjNum(pIfMan) ); vMapping = Vec_IntStart( If_ManObjNum(pIfMan) );
vMapping2 = Vec_IntStart( 1 ); vMapping2 = Vec_IntStart( 1 );
if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u || pIfMan->pPars->fEnableCheck07 || pIfMan->pPars->fUseDsdTune) ) if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u || pIfMan->pPars->fEnableCheck07) )
{ {
vPacking = Vec_IntAlloc( 1000 ); vPacking = Vec_IntAlloc( 1000 );
Vec_IntPush( vPacking, 0 ); Vec_IntPush( vPacking, 0 );
} }
if ( pIfMan->pPars->fUseDsdTune )
{
int nTtBitNum = If_DsdManTtBitNum(pIfMan->pIfDsdMan);
int nPermBitNum = If_DsdManPermBitNum(pIfMan->pIfDsdMan);
int nConfigInts = Abc_BitWordNum(nTtBitNum + nPermBitNum + 1);
vConfigs = Vec_IntAlloc( 1000 );
Vec_IntPush( vConfigs, 0 );
Vec_IntPush( vConfigs, nConfigInts );
}
// create new manager // create new manager
pNew = Gia_ManStart( If_ManObjNum(pIfMan) ); pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
// iterate through nodes used in the mapping // iterate through nodes used in the mapping
@ -1722,11 +1763,13 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 ); pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
} }
/*
else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts ) else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts )
{ {
if ( pSat == NULL ) if ( pNtkCell == NULL )
{ {
pSat = (sat_solver *)If_ManSatBuildFromCell( If_DsdManGetCellStr(pIfMan->pIfDsdMan), &vPiVars, &vPoVars, &pNtkCell ); assert( If_DsdManGetCellStr(pIfMan->pIfDsdMan) != NULL );
pNtkCell = Ifn_NtkParse( If_DsdManGetCellStr(pIfMan->pIfDsdMan) );
nLutMax = Ifn_NtkLutSizeMax( pNtkCell ); nLutMax = Ifn_NtkLutSizeMax( pNtkCell );
pHashed = Gia_ManStart( 10000 ); pHashed = Gia_ManStart( 10000 );
Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 ); Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 );
@ -1734,9 +1777,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Gia_ManAppendCi( pHashed ); Gia_ManAppendCi( pHashed );
Gia_ManHashAlloc( pHashed ); Gia_ManHashAlloc( pHashed );
} }
pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pHashed, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, nLutMax, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking ); pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pHashed, pCutBest, pNtkCell, nLutMax, vLeaves, vLits, vCover, vMapping, vMapping2, vConfigs );
pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
} }
*/
else if ( pIfMan->pPars->fUseAndVars && pIfMan->pPars->fUseCofVars && pIfMan->pPars->fDeriveLuts && (int)pCutBest->nLeaves > pIfMan->pPars->nLutSize/2 ) else if ( pIfMan->pPars->fUseAndVars && pIfMan->pPars->fUseCofVars && pIfMan->pPars->fDeriveLuts && (int)pCutBest->nLeaves > pIfMan->pPars->nLutSize/2 )
{ {
int truthId = Abc_Lit2Var(pCutBest->iCutFunc); int truthId = Abc_Lit2Var(pCutBest->iCutFunc);
@ -1764,6 +1808,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
// perform decomposition of the cut // perform decomposition of the cut
pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 ); pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );
pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 )
Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, Abc_LitIsCompl(pIfObj->iCopy) );
} }
else else
{ {
@ -1796,8 +1842,6 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Vec_IntFree( vCover ); Vec_IntFree( vCover );
Vec_IntFree( vLeaves ); Vec_IntFree( vLeaves );
Vec_IntFree( vLeaves2 ); Vec_IntFree( vLeaves2 );
Vec_IntFreeP( &vPiVars );
Vec_IntFreeP( &vPoVars );
if ( pNtkCell ) if ( pNtkCell )
ABC_FREE( pNtkCell ); ABC_FREE( pNtkCell );
if ( pSat ) if ( pSat )
@ -1820,8 +1864,13 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
// attach mapping and packing // attach mapping and packing
assert( pNew->vMapping == NULL ); assert( pNew->vMapping == NULL );
assert( pNew->vPacking == NULL ); assert( pNew->vPacking == NULL );
assert( pNew->vConfigs == NULL );
assert( pNew->pCellStr == NULL );
pNew->vMapping = vMapping; pNew->vMapping = vMapping;
pNew->vPacking = vPacking; pNew->vPacking = vPacking;
pNew->vConfigs = vConfigs;
pNew->pCellStr = vConfigs ? Abc_UtilStrsav( If_DsdManGetCellStr(pIfMan->pIfDsdMan) ) : NULL;
assert( !vConfigs || Vec_IntSize(vConfigs) == 2 + Vec_IntEntry(vConfigs, 0) * Vec_IntEntry(vConfigs, 1) );
// verify that COs have mapping // verify that COs have mapping
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;

2
src/aig/gia/giaMan.c
View File

@ -114,6 +114,8 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vMapping ); Vec_IntFreeP( &p->vMapping );
Vec_IntFreeP( &p->vCellMapping ); Vec_IntFreeP( &p->vCellMapping );
Vec_IntFreeP( &p->vPacking ); Vec_IntFreeP( &p->vPacking );
Vec_IntFreeP( &p->vConfigs );
ABC_FREE( p->pCellStr );
Vec_FltFreeP( &p->vInArrs ); Vec_FltFreeP( &p->vInArrs );
Vec_FltFreeP( &p->vOutReqs ); Vec_FltFreeP( &p->vOutReqs );
Gia_ManStopP( &p->pAigExtra ); Gia_ManStopP( &p->pAigExtra );

10
src/base/abci/abc.c
View File

@ -26745,12 +26745,10 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
return 1; return 1;
} }
if ( Gia_ManHasMapping(pAbc->pGia) ) if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs )
{ pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells( pAbc->pGia );
pTemp = (Gia_Man_t *)Dsm_ManDeriveGia( pAbc->pGia, fAddMuxes ); else if ( Gia_ManHasMapping(pAbc->pGia) )
// if ( !Abc_FrameReadFlag("silentmode") ) pTemp = (Gia_Man_t *)Dsm_ManDeriveGia( pAbc->pGia, fAddMuxes ); // delay-oriented unmapping
// printf( "Performed delay-oriented unmapping.\n" );
}
else if ( fAddMuxes ) else if ( fAddMuxes )
{ {
if ( pAbc->pGia->pMuxes ) if ( pAbc->pGia->pMuxes )

2
src/base/wlc/wlcStdin.c
View File

@ -110,7 +110,7 @@ Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radi
void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix ) void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix )
{ {
Vec_Str_t * vNum; Vec_Str_t * vNum;
int i, NameId, Name, Start, nBits = -1; int i, NameId, Name, Start = -1, nBits = -1;
assert( pCex->nRegs == 0 ); assert( pCex->nRegs == 0 );
// get the name ID // get the name ID
NameId = Abc_NamStrFind( p->pManName, pName ); NameId = Abc_NamStrFind( p->pManName, pName );

10
src/map/if/if.h
View File

@ -559,12 +559,14 @@ extern char * If_DsdManFileName( If_DsdMan_t * p );
extern int If_DsdManVarNum( If_DsdMan_t * p ); extern int If_DsdManVarNum( If_DsdMan_t * p );
extern int If_DsdManObjNum( If_DsdMan_t * p ); extern int If_DsdManObjNum( If_DsdMan_t * p );
extern int If_DsdManLutSize( If_DsdMan_t * p ); extern int If_DsdManLutSize( If_DsdMan_t * p );
extern int If_DsdManTtBitNum( If_DsdMan_t * p );
extern int If_DsdManPermBitNum( If_DsdMan_t * p );
extern void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize ); extern void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize );
extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd ); extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
extern int If_DsdManReadMark( If_DsdMan_t * p, int iDsd ); extern int If_DsdManReadMark( If_DsdMan_t * p, int iDsd );
extern void If_DsdManSetNewAsUseless( If_DsdMan_t * p ); extern void If_DsdManSetNewAsUseless( If_DsdMan_t * p );
extern word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd ); extern word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd );
extern char * If_DsdManGetCellStr( If_DsdMan_t * p ); extern char * If_DsdManGetCellStr( If_DsdMan_t * p );
extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose ); extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose );
extern int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig ); extern int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig );
@ -631,13 +633,15 @@ extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut
extern int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ); extern int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
/*=== ifTune.c ===========================================================*/ /*=== ifTune.c ===========================================================*/
extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr ); extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm ); extern int Ifn_NtkTtBits( char * pStr );
extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig );
extern void Ifn_NtkPrint( Ifn_Ntk_t * p ); extern void Ifn_NtkPrint( Ifn_Ntk_t * p );
extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
extern int Ifn_NtkInputNum( Ifn_Ntk_t * p ); extern int Ifn_NtkInputNum( Ifn_Ntk_t * p );
extern void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk ); extern void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk );
extern int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues ); extern int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues );
extern int If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vValues ); extern int If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, word * pTtData, Vec_Int_t * vLeaves, Vec_Int_t * vValues );
extern void * If_ManDeriveGiaFromCells( void * p );
/*=== ifUtil.c ============================================================*/ /*=== ifUtil.c ============================================================*/
extern void If_ManCleanNodeCopy( If_Man_t * p ); extern void If_ManCleanNodeCopy( If_Man_t * p );
extern void If_ManCleanCutData( If_Man_t * p ); extern void If_ManCleanCutData( If_Man_t * p );

134
src/map/if/ifDsd.c
View File

@ -44,6 +44,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#define DSD_VERSION "dsd1"
// network types // network types
typedef enum { typedef enum {
IF_DSD_NONE = 0, // 0: unknown IF_DSD_NONE = 0, // 0: unknown
@ -86,7 +88,9 @@ struct If_DsdMan_t_
Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function
int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules
Vec_Wrd_t * vPerms; // permutations int nTtBits; // the number of truth table bits
int nConfigWords; // the number of words for config data per node
Vec_Wrd_t * vConfigs; // permutations
Gia_Man_t * pTtGia; // GIA to represent truth tables Gia_Man_t * pTtGia; // GIA to represent truth tables
Vec_Int_t * vCover; // temporary memory Vec_Int_t * vCover; // temporary memory
void * pSat; // SAT solver void * pSat; // SAT solver
@ -174,6 +178,14 @@ int If_DsdManLutSize( If_DsdMan_t * p )
{ {
return p->LutSize; return p->LutSize;
} }
int If_DsdManTtBitNum( If_DsdMan_t * p )
{
return p->nTtBits;
}
int If_DsdManPermBitNum( If_DsdMan_t * p )
{
return (Abc_Base2Log(p->nVars + 1) + 1) * p->nVars;
}
void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize ) void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize )
{ {
p->LutSize = nLutSize; p->LutSize = nLutSize;
@ -196,9 +208,9 @@ void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
p->nObjsPrev = If_DsdManObjNum(p); p->nObjsPrev = If_DsdManObjNum(p);
p->fNewAsUseless = 1; p->fNewAsUseless = 1;
} }
word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd ) word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd )
{ {
return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0; return p->vConfigs ? Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Abc_Lit2Var(iDsd)) : NULL;
} }
char * If_DsdManGetCellStr( If_DsdMan_t * p ) char * If_DsdManGetCellStr( If_DsdMan_t * p )
{ {
@ -259,6 +271,7 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
p->nBins = Abc_PrimeCudd( 100000 ); p->nBins = Abc_PrimeCudd( 100000 );
p->pBins = ABC_CALLOC( unsigned, p->nBins ); p->pBins = ABC_CALLOC( unsigned, p->nBins );
p->pMem = Mem_FlexStart(); p->pMem = Mem_FlexStart();
p->nConfigWords = 1;
Vec_PtrGrow( &p->vObjs, 10000 ); Vec_PtrGrow( &p->vObjs, 10000 );
Vec_IntGrow( &p->vNexts, 10000 ); Vec_IntGrow( &p->vNexts, 10000 );
Vec_IntGrow( &p->vTruths, 10000 ); Vec_IntGrow( &p->vTruths, 10000 );
@ -338,7 +351,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
if ( p->vIsops[v] ) if ( p->vIsops[v] )
Vec_WecFree( p->vIsops[v] ); Vec_WecFree( p->vIsops[v] );
} }
Vec_WrdFreeP( &p->vPerms ); Vec_WrdFreeP( &p->vConfigs );
Vec_IntFreeP( &p->vTemp1 ); Vec_IntFreeP( &p->vTemp1 );
Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vTemp2 );
ABC_FREE( p->vObjs.pArray ); ABC_FREE( p->vObjs.pArray );
@ -1033,7 +1046,6 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
{ {
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
Vec_Int_t * vSets; Vec_Int_t * vSets;
char * pBuffer = "dsd0";
word * pTruth; word * pTruth;
int i, v, Num; int i, v, Num;
FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" ); FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
@ -1042,7 +1054,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore ); printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
return; return;
} }
fwrite( pBuffer, 4, 1, pFile ); fwrite( DSD_VERSION, 4, 1, pFile );
Num = p->nVars; Num = p->nVars;
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
Num = p->LutSize; Num = p->LutSize;
@ -1073,10 +1085,14 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
} }
} }
Num = p->vPerms ? Vec_WrdSize(p->vPerms) : 0; Num = p->nConfigWords;
fwrite( &Num, 4, 1, pFile );
Num = p->nTtBits;
fwrite( &Num, 4, 1, pFile );
Num = p->vConfigs ? Vec_WrdSize(p->vConfigs) : 0;
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
if ( Num ) if ( Num )
fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); fwrite( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
Num = p->pCellStr ? strlen(p->pCellStr) : 0; Num = p->pCellStr ? strlen(p->pCellStr) : 0;
fwrite( &Num, 4, 1, pFile ); fwrite( &Num, 4, 1, pFile );
if ( Num ) if ( Num )
@ -1099,7 +1115,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
return NULL; return NULL;
} }
RetValue = fread( pBuffer, 4, 1, pFile ); RetValue = fread( pBuffer, 4, 1, pFile );
if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' ) if ( strncmp(pBuffer, DSD_VERSION, strlen(DSD_VERSION)) )
{ {
printf( "Unrecognized format of file \"%s\".\n", pFileName ); printf( "Unrecognized format of file \"%s\".\n", pFileName );
return NULL; return NULL;
@ -1160,10 +1176,14 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
} }
ABC_FREE( pTruth ); ABC_FREE( pTruth );
RetValue = fread( &Num, 4, 1, pFile ); RetValue = fread( &Num, 4, 1, pFile );
p->nConfigWords = Num;
RetValue = fread( &Num, 4, 1, pFile );
p->nTtBits = Num;
RetValue = fread( &Num, 4, 1, pFile );
if ( RetValue && Num ) if ( RetValue && Num )
{ {
p->vPerms = Vec_WrdStart( Num ); p->vConfigs = Vec_WrdStart( Num );
RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); RetValue = fread( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
} }
RetValue = fread( &Num, 4, 1, pFile ); RetValue = fread( &Num, 4, 1, pFile );
if ( RetValue && Num ) if ( RetValue && Num )
@ -1190,14 +1210,16 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
printf( "LUT size should be the same.\n" ); printf( "LUT size should be the same.\n" );
return; return;
} }
assert( p->nTtBits == pNew->nTtBits );
assert( p->nConfigWords == pNew->nConfigWords );
if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) ) if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) )
printf( "Warning! Old manager has %smarks while new manager has %smarks.\n", printf( "Warning! Old manager has %smarks while new manager has %smarks.\n",
If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " ); If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " );
vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) ); vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) );
Vec_IntPush( vMap, 0 ); Vec_IntPush( vMap, 0 );
Vec_IntPush( vMap, 1 ); Vec_IntPush( vMap, 1 );
if ( p->vPerms && pNew->vPerms ) if ( p->vConfigs && pNew->vConfigs )
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs), 0 ); Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * (Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs)), 0 );
If_DsdVecForEachNode( &pNew->vObjs, pObj, i ) If_DsdVecForEachNode( &pNew->vObjs, pObj, i )
{ {
If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k ) If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k )
@ -1205,14 +1227,19 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL ); Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL );
if ( pObj->fMark ) if ( pObj->fMark )
If_DsdVecObjSetMark( &p->vObjs, Id ); If_DsdVecObjSetMark( &p->vObjs, Id );
if ( p->vPerms && pNew->vPerms && i < Vec_WrdSize(pNew->vPerms) ) if ( p->vConfigs && pNew->vConfigs && p->nConfigWords * i < Vec_WrdSize(pNew->vConfigs) )
Vec_WrdFillExtra( p->vPerms, Id, Vec_WrdEntry(pNew->vPerms, i) ); {
//Vec_WrdFillExtra( p->vConfigs, Id, Vec_WrdEntry(pNew->vConfigs, i) );
word * pConfigNew = Vec_WrdEntryP(pNew->vConfigs, p->nConfigWords * i);
word * pConfigOld = Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Id);
memcpy( pConfigOld, pConfigNew, sizeof(word) * p->nConfigWords );
}
Vec_IntPush( vMap, Id ); Vec_IntPush( vMap, Id );
} }
assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) ); assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
Vec_IntFree( vMap ); Vec_IntFree( vMap );
if ( p->vPerms && pNew->vPerms ) if ( p->vConfigs && pNew->vConfigs )
Vec_WrdShrink( p->vPerms, Vec_PtrSize(&p->vObjs) ); Vec_WrdShrink( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs) );
} }
void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose ) void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose )
{ {
@ -1226,7 +1253,7 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
int i; int i;
ABC_FREE( p->pCellStr ); ABC_FREE( p->pCellStr );
Vec_WrdFreeP( &p->vPerms ); Vec_WrdFreeP( &p->vConfigs );
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = 0; pObj->fMark = 0;
} }
@ -1235,7 +1262,7 @@ void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose )
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
int i; int i;
ABC_FREE( p->pCellStr ); ABC_FREE( p->pCellStr );
Vec_WrdFreeP( &p->vPerms ); Vec_WrdFreeP( &p->vConfigs );
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = !pObj->fMark; pObj->fMark = !pObj->fMark;
} }
@ -2440,7 +2467,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
int fVeryVerbose = 0; int fVeryVerbose = 0;
ProgressBar * pProgress = NULL; ProgressBar * pProgress = NULL;
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
word * pTruth, Perm; word * pTruth, * pConfig;
int i, nVars, Value, LutSize; int i, nVars, Value, LutSize;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
// parse the structure // parse the structure
@ -2458,6 +2485,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) ) if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
LutSize = Ifn_NtkLutSizeMax(pNtk); LutSize = Ifn_NtkLutSizeMax(pNtk);
p->nTtBits = Ifn_NtkTtBits( pStruct );
p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
// print // print
if ( fVerbose ) if ( fVerbose )
{ {
@ -2471,30 +2500,32 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
if ( i >= p->nObjsPrev ) if ( i >= p->nObjsPrev )
pObj->fMark = 0; pObj->fMark = 0;
if ( p->vPerms == NULL ) if ( p->vConfigs == NULL )
p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
else else
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
{ {
if ( (i & 0xFF) == 0 ) if ( (i & 0xFF) == 0 )
Extra_ProgressBarUpdate( pProgress, i, NULL ); Extra_ProgressBarUpdate( pProgress, i, NULL );
nVars = If_DsdObjSuppSize(pObj); nVars = If_DsdObjSuppSize(pObj);
if ( nVars <= LutSize ) //if ( nVars <= LutSize )
continue; // continue;
pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
if ( fVeryVerbose ) if ( fVeryVerbose )
Dau_DsdPrintFromTruth( pTruth, nVars ); Dau_DsdPrintFromTruth( pTruth, nVars );
if ( fVerbose ) if ( fVerbose )
printf( "%6d : %2d ", i, nVars ); printf( "%6d : %2d ", i, nVars );
Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, &Perm ); pConfig = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * i );
Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, pConfig );
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "\n" ); printf( "\n" );
if ( Value == 0 ) if ( Value == 0 )
{
If_DsdVecObjSetMark( &p->vObjs, i ); If_DsdVecObjSetMark( &p->vObjs, i );
else memset( pConfig, 0, sizeof(word) * p->nConfigWords );
Vec_WrdWriteEntry( p->vPerms, i, Perm ); }
} }
p->nObjsPrev = 0; p->nObjsPrev = 0;
p->LutSize = 0; p->LutSize = 0;
@ -2531,12 +2562,13 @@ typedef struct Ifn_ThData_t_
{ {
Ifn_Ntk_t * pNtk; // network Ifn_Ntk_t * pNtk; // network
word pTruth[DAU_MAX_WORD]; word pTruth[DAU_MAX_WORD];
word pConfig[10]; // configuration data
int nConfigWords;// configuration data word count
int nVars; // support int nVars; // support
int Id; // object int Id; // object
int nConfls; // conflicts int nConfls; // conflicts
int Result; // result int Result; // result
int Status; // state int Status; // state
word Perm; // permutation
abctime clkUsed; // total runtime abctime clkUsed; // total runtime
} Ifn_ThData_t; } Ifn_ThData_t;
void * Ifn_WorkerThread( void * pArg ) void * Ifn_WorkerThread( void * pArg )
@ -2555,7 +2587,8 @@ void * Ifn_WorkerThread( void * pArg )
return NULL; return NULL;
} }
clk = Abc_Clock(); clk = Abc_Clock();
pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, &pThData->Perm ); memset( pThData->pConfig, 0, sizeof(word) * pThData->nConfigWords );
pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, pThData->pConfig );
pThData->clkUsed += Abc_Clock() - clk; pThData->clkUsed += Abc_Clock() - clk;
pThData->Status = 0; pThData->Status = 0;
// printf( "Finished object %d\n", pThData->Id ); // printf( "Finished object %d\n", pThData->Id );
@ -2597,6 +2630,9 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
// check the largest LUT // check the largest LUT
LutSize = Ifn_NtkLutSizeMax(pNtk); LutSize = Ifn_NtkLutSizeMax(pNtk);
p->nTtBits = Ifn_NtkTtBits( pStruct );
p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
assert( p->nConfigWords <= 10 );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Considering programmable cell: " ); printf( "Considering programmable cell: " );
@ -2610,10 +2646,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
if ( i >= p->nObjsPrev ) if ( i >= p->nObjsPrev )
pObj->fMark = 0; pObj->fMark = 0;
if ( p->vPerms == NULL ) if ( p->vConfigs == NULL )
p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
else else
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
// perform concurrent solving // perform concurrent solving
@ -2625,13 +2661,14 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
// start the threads // start the threads
for ( i = 0; i < nProcs; i++ ) for ( i = 0; i < nProcs; i++ )
{ {
ThData[i].pNtk = Ifn_NtkParse( pStruct ); ThData[i].pNtk = Ifn_NtkParse( pStruct );
ThData[i].nVars = -1; // support ThData[i].nVars = -1; // support
ThData[i].Id = -1; // object ThData[i].Id = -1; // object
ThData[i].nConfls = nConfls; // conflicts ThData[i].nConfls = nConfls; // conflicts
ThData[i].Result = -1; // result ThData[i].Result = -1; // result
ThData[i].Status = 0; // state ThData[i].Status = 0; // state
ThData[i].clkUsed = 0; // total runtime ThData[i].clkUsed = 0; // total runtime
ThData[i].nConfigWords = p->nConfigWords;
status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 ); status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 );
} }
// run the threads // run the threads
@ -2649,7 +2686,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
if ( ThData[i].Result == 0 ) if ( ThData[i].Result == 0 )
If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id ); If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
else else
Vec_WrdWriteEntry( p->vPerms, ThData[i].Id, ThData[i].Perm ); {
word * pTtWords = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * ThData[i].Id );
memcpy( pTtWords, ThData[i].pConfig, sizeof(word) * p->nConfigWords );
}
ThData[i].Id = -1; ThData[i].Id = -1;
ThData[i].Result = -1; ThData[i].Result = -1;
} }
@ -2659,8 +2699,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
Extra_ProgressBarUpdate( pProgress, k, NULL ); Extra_ProgressBarUpdate( pProgress, k, NULL );
pObj = If_DsdVecObj( &p->vObjs, k ); pObj = If_DsdVecObj( &p->vObjs, k );
nVars = If_DsdObjSuppSize(pObj); nVars = If_DsdObjSuppSize(pObj);
if ( nVars <= LutSize ) //if ( nVars <= LutSize )
continue; // continue;
clk = Abc_Clock(); clk = Abc_Clock();
If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth ); If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth );
clkUsed += Abc_Clock() - clk; clkUsed += Abc_Clock() - clk;
@ -2738,10 +2778,10 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
if ( i >= p->nObjsPrev ) if ( i >= p->nObjsPrev )
pObj->fMark = 0; pObj->fMark = 0;
if ( p->vPerms == NULL ) if ( p->vConfigs == NULL )
p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); p->vConfigs = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
else else
Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); Vec_WrdFillExtra( p->vConfigs, Vec_PtrSize(&p->vObjs), 0 );
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
{ {
@ -2767,7 +2807,7 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
if ( Value ) if ( Value )
If_DsdVecObjSetMark( &p->vObjs, i ); If_DsdVecObjSetMark( &p->vObjs, i );
else else
Vec_WrdWriteEntry( p->vPerms, i, Perm ); Vec_WrdWriteEntry( p->vConfigs, i, Perm );
} }
p->nObjsPrev = 0; p->nObjsPrev = 0;
p->LutSize = 0; p->LutSize = 0;

142
src/map/if/ifTune.c
View File

@ -95,7 +95,7 @@ static inline word * Ifn_ObjTruth( Ifn_Ntk_t * p, int i ) { return p->pTt
// - primary inputs [0; p->nInps) // - primary inputs [0; p->nInps)
// - internal nodes [p->nInps; p->nObjs) // - internal nodes [p->nInps; p->nObjs)
// - configuration params [p->nObjs; p->nParsVIni) // - configuration params [p->nObjs; p->nParsVIni)
// - variable selection params [p->nParsVIni; p->pPars) // - variable selection params [p->nParsVIni; p->nPars)
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
@ -460,6 +460,16 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
// printf( "Finished parsing: " ); Ifn_NtkPrint(p); // printf( "Finished parsing: " ); Ifn_NtkPrint(p);
return p; return p;
} }
int Ifn_NtkTtBits( char * pStr )
{
int i, Counter = 0;
Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStr );
for ( i = pNtk->nInps; i < pNtk->nObjs; i++ )
if ( pNtk->Nodes[i].Type == IFN_DSD_PRIME )
Counter += (1 << pNtk->Nodes[i].nFanins);
ABC_FREE( pNtk );
return Counter;
}
@ -728,13 +738,21 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover ) int If_ManSatDeriveGiaFromBits( Gia_Man_t * pNew, Ifn_Ntk_t * p, word * pConfigData, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
{ {
Gia_Man_t * pNew = (Gia_Man_t *)pGia; int i, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
int i, Id, k, iLit, iVar = 0, nVarsNew, pVarMap[1000]; int nTtBits = p->nParsVIni - p->nObjs;
assert( Gia_ManCiNum(pNew) == p->nInps && p->nParsVIni < 1000 ); int nPermBits = Abc_Base2Log(p->nInps + 1) + 1;
Gia_ManForEachCiId( pNew, Id, i ) int fCompl = Abc_TtGetBit( pConfigData, nTtBits + nPermBits * p->nInps );
pVarMap[i] = Abc_Var2Lit( Id, 0 ); assert( Vec_IntSize(vLeaves) <= p->nInps && p->nParsVIni < 1000 );
for ( i = 0; i < p->nInps; i++ )
{
for ( iLit = k = 0; k < nPermBits; k++ )
if ( Abc_TtGetBit(pConfigData, nTtBits + i * nPermBits + k) )
iLit |= (1 << k);
assert( Abc_Lit2Var(iLit) < Vec_IntSize(vLeaves) );
pVarMap[i] = Abc_Lit2LitL( Vec_IntArray(vLeaves), iLit );
}
for ( i = p->nInps; i < p->nObjs; i++ ) for ( i = p->nInps; i < p->nObjs; i++ )
{ {
int Type = p->Nodes[i].Type; int Type = p->Nodes[i].Type;
@ -768,7 +786,7 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues,
word uTruth = 0; word uTruth = 0;
int nMints = (1 << nFans); int nMints = (1 << nFans);
for ( k = 0; k < nMints; k++ ) for ( k = 0; k < nMints; k++ )
if ( Vec_IntEntry( vValues, iVar++ ) ) if ( Abc_TtGetBit(pConfigData, iVar++) )
uTruth |= ((word)1 << k); uTruth |= ((word)1 << k);
uTruth = Abc_Tt6Stretch( uTruth, nFans ); uTruth = Abc_Tt6Stretch( uTruth, nFans );
// collect function // collect function
@ -787,8 +805,89 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues,
} }
else assert( 0 ); else assert( 0 );
} }
assert( iVar == Vec_IntSize(vValues) ); assert( iVar == nTtBits );
return pVarMap[p->nObjs - 1]; return Abc_LitNotCond( pVarMap[p->nObjs - 1], fCompl );
}
/**Function*************************************************************
Synopsis [Derive GIA using programmable bits.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * If_ManDeriveGiaFromCells( void * pGia )
{
Gia_Man_t * p = (Gia_Man_t *)pGia;
Gia_Man_t * pNew, * pTemp;
Vec_Int_t * vCover, * vLeaves;
Ifn_Ntk_t * pNtkCell;
Gia_Obj_t * pObj;
word * pConfigData;
//word * pTruth;
int k, i, iLut, iVar;
int nConfigInts, Count = 0;
assert( p->vConfigs != NULL );
assert( p->pCellStr != NULL );
assert( Gia_ManHasMapping(p) );
// derive cell network
pNtkCell = Ifn_NtkParse( p->pCellStr );
Ifn_Prepare( pNtkCell, NULL, pNtkCell->nInps );
nConfigInts = Vec_IntEntry( p->vConfigs, 1 );
// create new manager
pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// map primary inputs
Gia_ManFillValue(p);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// iterate through nodes used in the mapping
vLeaves = Vec_IntAlloc( 16 );
vCover = Vec_IntAlloc( 1 << 16 );
Gia_ManHashStart( pNew );
//Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
Gia_ManForEachAnd( p, pObj, iLut )
{
if ( Gia_ObjIsBuf(pObj) )
{
pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
continue;
}
if ( !Gia_ObjIsLut(p, iLut) )
continue;
// collect leaves
//Vec_IntClear( vLeaves );
//Gia_LutForEachFanin( p, iLut, iVar, k )
// Vec_IntPush( vLeaves, iVar );
//pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
// collect incoming literals
Vec_IntClear( vLeaves );
Gia_LutForEachFanin( p, iLut, iVar, k )
Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
pConfigData = (word *)Vec_IntEntryP( p->vConfigs, 2 + nConfigInts * Count++ );
Gia_ManObj(p, iLut)->Value = If_ManSatDeriveGiaFromBits( pNew, pNtkCell, pConfigData, vLeaves, vCover );
}
assert( Vec_IntEntry(p->vConfigs, 0) == Count );
assert( Vec_IntSize(p->vConfigs) == 2 + nConfigInts * Count );
//Gia_ObjComputeTruthTableStop( p );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Vec_IntFree( vLeaves );
Vec_IntFree( vCover );
ABC_FREE( pNtkCell );
// perform cleanup
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
} }
/**Function************************************************************* /**Function*************************************************************
@ -1196,6 +1295,21 @@ word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
} }
return Perm; return Perm;
} }
void Ifn_NtkMatchCollectConfig( Ifn_Ntk_t * p, sat_solver * pSat, word * pConfig )
{
int i, v, Mint;
assert( p->nParsVNum <= 4 );
for ( i = 0; i < p->nInps; i++ )
{
for ( Mint = v = 0; v < p->nParsVNum; v++ )
if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
Mint |= (1 << v);
Abc_TtSetHex( pConfig, i, Mint );
}
for ( v = p->nObjs; v < p->nParsVIni; v++ )
if ( sat_solver_var_value(pSat, v) )
Abc_TtSetBit( pConfig + 1, v - p->nObjs );
}
void Ifn_NtkMatchPrintPerm( word Perm, int nInps ) void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
{ {
int i; int i;
@ -1204,7 +1318,7 @@ void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) ); printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
printf( "\n" ); printf( "\n" );
} }
int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm ) int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig )
{ {
word * pTruth1; word * pTruth1;
int RetValue = 0; int RetValue = 0;
@ -1218,7 +1332,7 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
Ifn_NtkAddConstraints( p, pSat ); Ifn_NtkAddConstraints( p, pSat );
if ( fVeryVerbose ) if ( fVeryVerbose )
Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk ); Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
if ( pPerm ) *pPerm = 0; if ( pConfig ) assert( *pConfig == 0 );
for ( i = 0; i < nIterMax; i++ ) for ( i = 0; i < nIterMax; i++ )
{ {
// get variable assignment // get variable assignment
@ -1248,8 +1362,8 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
iMint = Abc_TtFindFirstBit( pTruth1, p->nVars ); iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
if ( iMint == -1 ) if ( iMint == -1 )
{ {
if ( pPerm ) if ( pConfig )
*pPerm = Ifn_NtkMatchCollectPerm( p, pSat ); Ifn_NtkMatchCollectConfig( p, pSat, pConfig );
/* /*
if ( pPerm ) if ( pPerm )
{ {