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

Deriving cell mapping with &if -kz.

This commit is contained in:
Alan Mishchenko 2014-10-04 19:18:34 -07:00
parent 4c7165a4f7
commit 24083998ab
10 changed files with 221 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -2991,6 +2991,10 @@ SOURCE=.\src\misc\util\utilFile.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\misc\util\utilIsop.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilMem.c SOURCE=.\src\misc\util\utilMem.c
# End Source File # End Source File
# Begin Source File # Begin Source File

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

@ -135,7 +135,7 @@ struct Gia_Man_t_
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
Vec_Ptr_t * vSeqModelVec; // sequential counter-examples Vec_Ptr_t * vSeqModelVec; // sequential counter-examples
int * pCopies; // intermediate copies Vec_Int_t vCopies; // intermediate copies
Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vTruths; // used for truth table computation
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
Vec_Int_t * vGateClasses; // classes of gates for abstraction Vec_Int_t * vGateClasses; // classes of gates for abstraction
@ -465,11 +465,15 @@ static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) {
static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); } static inline int Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); }
static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Vec_IntEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)); }
static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit); }
static inline int Gia_ObjCopyArray( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); }
static inline void Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); }
static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
static inline int Gia_ObjFanin0CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p,pObj)), Gia_ObjFaninC0(pObj)); }
static inline int Gia_ObjFanin1CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId1p(p,pObj)), Gia_ObjFaninC1(pObj)); }
static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }

5
src/aig/gia/giaEnable.c
View File

@ -362,8 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
Gia_Man_t * pNew; Gia_Man_t * pNew;
Gia_Obj_t * pObj, * pObjRi, * pObjRo; Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int f, i; int f, i;
ABC_FREE( p->pCopies ); Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->pSpec = Abc_UtilStrsav( p->pSpec );
@ -413,7 +412,7 @@ Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, i
vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs ); vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs );
Vec_IntFree( vTemp ); Vec_IntFree( vTemp );
Gia_ManStop( pFrames ); Gia_ManStop( pFrames );
ABC_FREE( p->pCopies ); ABC_FREE( p->vCopies.pArray );
// cofactor all these variables // cofactor all these variables
pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose ); pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose );
Vec_IntFree( vCofSigs ); Vec_IntFree( vCofSigs );

4
src/aig/gia/giaEquiv.c
View File

@ -1017,7 +1017,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
} }
*/ */
assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) );
vXorLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
if ( fDualOut ) if ( fDualOut )
@ -1052,7 +1052,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
// Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" ); // Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 ); Gia_ManAppendCo( pNew, 0 );
} }
ABC_FREE( p->pCopies ); ABC_FREE( p->vCopies.pArray );
Vec_IntFree( vXorLits ); Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew ); Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );

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

@ -1425,9 +1425,51 @@ 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, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, void * pNtkCell, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) 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 )
{ {
return 0; int iLit;
if ( Vec_IntSize(vLeaves) <= nLutMax )
iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
else
{
Gia_Obj_t * pObj;
int i, Id;
// extract variable permutation
word Perm = If_DsdManGetFuncPerm( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) );
assert( Perm > 0 );
// 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
iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, vLits, vCover );
// copy GIA back into the manager
Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 );
Gia_ObjSetCopyArray( pTemp, 0, 0 );
Gia_ManForEachCiId( pTemp, Id, i )
Gia_ObjSetCopyArray( pTemp, Id, Vec_IntEntry(vLeaves, i) );
// collect nodes
Gia_ManIncrementTravId( pTemp );
Id = Abc_Lit2Var( iLit );
Gia_ManCollectAnds( pTemp, &Id, 1, vCover );
// copy GIA
Gia_ManForEachObjVec( vCover, pTemp, pObj, i )
{
iLit = Gia_ManAppendAnd( pNew, Gia_ObjFanin0CopyArray(pTemp, pObj), Gia_ObjFanin1CopyArray(pTemp, pObj) );
Gia_ObjSetCopyArray( pTemp, Gia_ObjId(pTemp, pObj), iLit );
}
iLit = Abc_LitNotCond( Gia_ObjCopyArray(pTemp, Id), Abc_LitIsCompl(iLit) );
}
// write packing
if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 )
{
Vec_IntPush( vPacking, 1 );
Vec_IntPush( vPacking, Abc_Lit2Var(iLit) );
Vec_IntAddToEntry( vPacking, 0, 1 );
}
return iLit;
} }
/**Function************************************************************* /**Function*************************************************************
@ -1443,15 +1485,15 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t *
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
{ {
Gia_Man_t * pNew; 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;
Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
Vec_Int_t * vPiVars = NULL, * vPoVars = NULL; Vec_Int_t * vPiVars = NULL, * vPoVars = NULL;
sat_solver * pSat = NULL; sat_solver * pSat = NULL;
void * pNtkCell = NULL; Ifn_Ntk_t * pNtkCell = NULL;
int i, k, Entry; int i, k, nLutMax, Entry;
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;
@ -1499,8 +1541,16 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
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 ( pSat == NULL )
pSat = (sat_solver *)If_ManSatBuildFromCell( NULL, &vPiVars, &vPoVars, (void **)&pNtkCell ); {
pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking ); pSat = (sat_solver *)If_ManSatBuildFromCell( If_DsdManGetCellStr(pIfMan->pIfDsdMan), &vPiVars, &vPoVars, &pNtkCell );
nLutMax = Ifn_NtkLutSizeMax( pNtkCell );
pHashed = Gia_ManStart( 10000 );
Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 );
for ( k = 0; k < pIfMan->pPars->nLutSize; k++ )
Gia_ManAppendCi( 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 = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
} }
else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm ) else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm )
@ -1549,8 +1599,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Vec_IntFreeP( &vPoVars ); Vec_IntFreeP( &vPoVars );
if ( pNtkCell ) if ( pNtkCell )
ABC_FREE( pNtkCell ); ABC_FREE( pNtkCell );
if ( pSat != NULL ) if ( pSat )
sat_solver_delete(pSat); sat_solver_delete(pSat);
if ( pHashed )
Gia_ManStop( pHashed );
// printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n", // printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n",
// If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) ); // If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) );
// finish mapping // finish mapping

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

@ -16139,7 +16139,15 @@ int Abc_CommandDsdMatch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
} }
if ( pStruct ) if ( pStruct )
{
char * pStructCur = If_DsdManGetCellStr( pDsdMan );
if ( pStructCur && strcmp(pStructCur, pStruct) )
{
Abc_Print( -1, "DSD manager matched with cell %s needs to be cleaned before matching with cell %s.\n", pStructCur, pStruct );
return 0;
}
Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose ); Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose );
}
else else
If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose ); If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose );
return 0; return 0;
@ -31414,6 +31422,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManVarNum(pDsdMan) ); Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManVarNum(pDsdMan) );
return 1; return 1;
} }
if ( pPars->fDeriveLuts && If_DsdManGetCellStr(pDsdMan) == NULL )
{
Abc_Print( -1, "DSD manager is not matched with any particular cell.\n" );
return 1;
}
pPars->fCutMin = 1; pPars->fCutMin = 1;
pPars->fUseDsd = 1; pPars->fUseDsd = 1;
If_DsdManSetNewAsUseless( pDsdMan ); If_DsdManSetNewAsUseless( pDsdMan );
@ -31454,7 +31467,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
pPars->fTruth = 1; pPars->fTruth = 1;
pPars->fExpRed = 0; pPars->fExpRed = 0;
if ( pPars->pLutStruct == NULL ) if ( pPars->pLutStruct == NULL && !pPars->fUseDsdTune )
pPars->fDeriveLuts = 1; pPars->fDeriveLuts = 1;
} }
// modify the subgraph recording // modify the subgraph recording

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

@ -81,6 +81,7 @@ typedef struct If_Set_t_ If_Set_t;
typedef struct If_LibLut_t_ If_LibLut_t; typedef struct If_LibLut_t_ If_LibLut_t;
typedef struct If_LibBox_t_ If_LibBox_t; typedef struct If_LibBox_t_ If_LibBox_t;
typedef struct If_DsdMan_t_ If_DsdMan_t; typedef struct If_DsdMan_t_ If_DsdMan_t;
typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
typedef struct Ifif_Par_t_ Ifif_Par_t; typedef struct Ifif_Par_t_ Ifif_Par_t;
struct Ifif_Par_t_ struct Ifif_Par_t_
@ -560,6 +561,8 @@ 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 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 );
extern int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm ); extern int If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
@ -624,7 +627,14 @@ extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ); extern int If_CutComputeTruth( 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 ); 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 void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk ); 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 void Ifn_NtkPrint( Ifn_Ntk_t * p );
extern int Ifn_NtkLutSizeMax( 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 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 );
/*=== 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 );

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

@ -90,6 +90,7 @@ struct If_DsdMan_t_
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
char * pCellStr; // symbolic cell description
int nObjsPrev; // previous number of objects int nObjsPrev; // previous number of objects
int fNewAsUseless; // set new as useless int fNewAsUseless; // set new as useless
int nUniqueHits; // statistics int nUniqueHits; // statistics
@ -195,6 +196,14 @@ 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 )
{
return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0;
}
char * If_DsdManGetCellStr( If_DsdMan_t * p )
{
return p->pCellStr;
}
/**Function************************************************************* /**Function*************************************************************
@ -339,6 +348,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
Gia_ManStopP( &p->pTtGia ); Gia_ManStopP( &p->pTtGia );
Vec_IntFreeP( &p->vCover ); Vec_IntFreeP( &p->vCover );
If_ManSatUnbuild( p->pSat ); If_ManSatUnbuild( p->pSat );
ABC_FREE( p->pCellStr );
ABC_FREE( p->pStore ); ABC_FREE( p->pStore );
ABC_FREE( p->pBins ); ABC_FREE( p->pBins );
ABC_FREE( p ); ABC_FREE( p );
@ -720,6 +730,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
If_DsdManPrintDistrib( p ); If_DsdManPrintDistrib( p );
printf( "Number of inputs = %d. LUT size = %d. Marks = %s. NewAsUseless = %s. Bookmark = %d.\n", printf( "Number of inputs = %d. LUT size = %d. Marks = %s. NewAsUseless = %s. Bookmark = %d.\n",
p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev ); p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev );
if ( p->pCellStr )
printf( "Symbolic cell description: %s\n", p->pCellStr );
if ( p->pTtGia ) if ( p->pTtGia )
fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) ); fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) );
fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses ); fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses );
@ -1061,6 +1073,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;
fwrite( &Num, 4, 1, pFile );
if ( Num )
fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
Num = p->pCellStr ? strlen(p->pCellStr) : 0;
fwrite( &Num, 4, 1, pFile );
if ( Num )
fwrite( p->pCellStr, sizeof(char)*Num, 1, pFile );
fclose( pFile ); fclose( pFile );
} }
If_DsdMan_t * If_DsdManLoad( char * pFileName ) If_DsdMan_t * If_DsdManLoad( char * pFileName )
@ -1139,6 +1159,18 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) ); assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) );
} }
ABC_FREE( pTruth ); ABC_FREE( pTruth );
RetValue = fread( &Num, 4, 1, pFile );
if ( Num )
{
p->vPerms = Vec_WrdStart( Num );
RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
}
RetValue = fread( &Num, 4, 1, pFile );
if ( Num )
{
p->pCellStr = ABC_CALLOC( char, Num + 1 );
RetValue = fread( p->pCellStr, sizeof(char)*Num, 1, pFile );
}
fclose( pFile ); fclose( pFile );
return p; return p;
} }
@ -1187,6 +1219,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 );
If_DsdVecForEachObj( &p->vObjs, pObj, i ) If_DsdVecForEachObj( &p->vObjs, pObj, i )
pObj->fMark = 0; pObj->fMark = 0;
} }
@ -2371,13 +2404,6 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec
} }
typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
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 void Ifn_NtkPrint( Ifn_Ntk_t * p );
extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
extern int Ifn_NtkInputNum( Ifn_Ntk_t * p );
/**Function************************************************************* /**Function*************************************************************
@ -2408,6 +2434,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
ABC_FREE( pNtk ); ABC_FREE( pNtk );
return; return;
} }
ABC_FREE( p->pCellStr );
p->pCellStr = Abc_UtilStrsav( pStruct );
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);
@ -2544,6 +2572,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
ABC_FREE( pNtk ); ABC_FREE( pNtk );
return; return;
} }
ABC_FREE( p->pCellStr );
p->pCellStr = Abc_UtilStrsav( pStruct );
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) );
// check the largest LUT // check the largest LUT

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

@ -58,8 +58,6 @@ static char * Ifn_Symbs[16] = {
}; };
typedef struct Ifn_Obj_t_ Ifn_Obj_t; typedef struct Ifn_Obj_t_ Ifn_Obj_t;
typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
struct Ifn_Obj_t_ struct Ifn_Obj_t_
{ {
unsigned Type : 3; // node type unsigned Type : 3; // node type
@ -621,9 +619,10 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t **
Gia_ManStop( p2 ); Gia_ManStop( p2 );
return pSat; return pSat;
} }
void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk ) void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk )
{ {
Ifn_Ntk_t * p = Ifn_NtkParse( pStr ); Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
Ifn_Prepare( p, NULL, p->nInps );
*ppNtk = p; *ppNtk = p;
if ( p == NULL ) if ( p == NULL )
return NULL; return NULL;
@ -651,7 +650,7 @@ void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
} }
int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits ) int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
{ {
int v, Value, m, mNew, nMints = (1 << nVars); int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps);
assert( (1 << nInps) == Vec_IntSize(vPoVars) ); assert( (1 << nInps) == Vec_IntSize(vPoVars) );
assert( nVars <= nInps ); assert( nVars <= nInps );
// remap minterms // remap minterms
@ -685,7 +684,7 @@ void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vV
Vec_IntForEachEntry( vPiVars, iVar, i ) Vec_IntForEachEntry( vPiVars, iVar, i )
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
} }
int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues ) 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 )
{ {
// extract permutation // extract permutation
int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE]; int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
@ -696,7 +695,7 @@ int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t *
assert( pPerm[i] < nVars ); assert( pPerm[i] < nVars );
} }
// perform SAT check // perform SAT check
RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues ); RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
Vec_IntClear( vValues ); Vec_IntClear( vValues );
if ( RetValue == 0 ) if ( RetValue == 0 )
return 0; return 0;
@ -708,7 +707,7 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
Vec_Int_t * vValues = Vec_IntAlloc( 100 ); Vec_Int_t * vValues = Vec_IntAlloc( 100 );
Vec_Int_t * vPiVars, * vPoVars; Vec_Int_t * vPiVars, * vPoVars;
sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars ); sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
int RetValue = Ifn_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues ); int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
Vec_IntPrint( vValues ); Vec_IntPrint( vValues );
// cleanup // cleanup
sat_solver_delete( pSat ); sat_solver_delete( pSat );
@ -718,6 +717,78 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
return RetValue; return RetValue;
} }
/**Function*************************************************************
Synopsis [Derive GIA using programmable bits.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover )
{
Gia_Man_t * pNew = (Gia_Man_t *)pGia;
int i, Id, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
assert( Gia_ManCiNum(pNew) == p->nInps && p->nParsVIni < 1000 );
Gia_ManForEachCiId( pNew, Id, i )
pVarMap[i] = Abc_Var2Lit( Id, 0 );
for ( i = p->nInps; i < p->nObjs; i++ )
{
int Type = p->Nodes[i].Type;
int nFans = p->Nodes[i].nFanins;
int * pFans = p->Nodes[i].Fanins;
int iFanin = p->Nodes[i].iFirst;
assert( nFans <= 6 );
if ( Type == IFN_DSD_AND )
{
iLit = 1;
for ( k = 0; k < nFans; k++ )
iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
pVarMap[i] = iLit;
}
else if ( Type == IFN_DSD_XOR )
{
iLit = 0;
for ( k = 0; k < nFans; k++ )
iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
pVarMap[i] = iLit;
}
else if ( Type == IFN_DSD_MUX )
{
assert( nFans == 3 );
pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
}
else if ( Type == IFN_DSD_PRIME )
{
int pFaninLits[16];
// collect truth table
word uTruth = 0;
int nMints = (1 << nFans);
for ( k = 0; k < nMints; k++ )
if ( Vec_IntEntry( vValues, iVar++ ) )
uTruth |= ((word)1 << k);
// collect function
for ( k = 0; k < nFans; k++ )
pFaninLits[k] = pVarMap[pFans[k]];
// implement the function
nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 );
if ( nVarsNew == 0 )
pVarMap[i] = (int)(uTruth & 1);
else
{
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits };
pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!!
}
}
else assert( 0 );
}
assert( iVar == Vec_IntSize(vValues) );
return pVarMap[p->nObjs - 1];
}
/**Function************************************************************* /**Function*************************************************************

8
src/proof/cec/cecCorr.c
View File

@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
assert( nFrames > 0 ); assert( nFrames > 0 );
assert( Gia_ManRegNum(p) > 0 ); assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL ); assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); Vec_IntFill( &p->vCopies, -1, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
Gia_ManAppendCo( pNew, iObjNew ); Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits ); Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew ); Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies ); ABC_FREE( p->vCopies.pArray );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
@ -229,7 +229,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
assert( Gia_ManRegNum(p) > 0 ); assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL ); assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) ); Vec_IntFill( &p->vCopies, -1, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
@ -270,7 +270,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
Gia_ManAppendCo( pNew, iObjNew ); Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits ); Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew ); Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies ); ABC_FREE( p->vCopies.pArray );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );