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

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2025-12-05 14:00:53 +01:00
parent ef1a3d0f42 b7f8df0941
commit 49efc5bb45
20 changed files with 1885 additions and 113 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -189,6 +189,7 @@ struct Gia_Man_t_
Vec_Int_t * vCoNumsOrig; // original CO names
Vec_Int_t * vIdsOrig; // original object IDs
Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent
Vec_Int_t * vEquLitIds; // original object IDs proved equivalent
Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
@ -1419,6 +1420,8 @@ typedef struct Gia_ChMan_t_ Gia_ChMan_t;
extern Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia );
extern void Gia_ManDupChoicesAdd( Gia_ChMan_t * pMan, Gia_Man_t * pGia );
extern Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * pMan );
extern Vec_Int_t * Gia_ManComputeMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vOuts );
extern Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAnds, Vec_Int_t * vCos );
/*=== giaEdge.c ==========================================================*/
extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray );
extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p );
@ -1727,7 +1730,7 @@ extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBox
extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft );
extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq );
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec );
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fNameMap, int fDumpFiles, int fVerbose, char * pFileSpec );
extern Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia );
/*=== giaTruth.c ===========================================================*/
extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths );

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

@ -907,6 +907,25 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
Vec_IntFree( vPairs );
}
// read object ID mapping
else if ( *pCur == 'y' )
{
pCur++;
int nInts = Gia_AigerReadInt(pCur)/4; pCur += 4;
if ( fSkipStrash ) {
pNew->vEquLitIds = Vec_IntStart( nInts );
memcpy( Vec_IntArray(pNew->vEquLitIds), pCur, (size_t)4*nInts );
if ( Vec_IntSize(pNew->vEquLitIds) != Gia_ManObjNum(pNew) ) {
printf( "Cannot read extension \"y\" because object count changed. Use \"&r -s <file.aig>\".\n" );
Vec_IntFreeP( &pNew->vEquLitIds );
}
else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" );
}
else {
if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
}
pCur += 4*nInts;
}
else break;
}
}
@ -1529,6 +1548,7 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) );
for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
if ( fVerbose ) printf( "Finished writing extension \"r\".\n" );
}
// write register inits
if ( p->vRegInits )
@ -1677,6 +1697,15 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) );
fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile );
}
// write object classes
if ( p->vEquLitIds )
{
fprintf( pFile, "y" );
Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) );
assert( Vec_IntSize(p->vEquLitIds) == Gia_ManObjNum(p) );
fwrite( Vec_IntArray(p->vEquLitIds), 1, 4*Gia_ManObjNum(p), pFile );
if ( fVerbose ) printf( "Finished writing extension \"y\".\n" );
}
// write name
if ( p->pName )
{
@ -1916,4 +1945,3 @@ int main( int argc, char ** argv )
ABC_NAMESPACE_IMPL_END

6
src/aig/gia/giaCut.c
View File

@ -292,8 +292,8 @@ static inline int Gia_CutCompare2( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
}
static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
{
if ( pCut0->CostF > pCut1->CostF ) return -1;
if ( pCut0->CostF < pCut1->CostF ) return 1;
if ( pCut0->CostF > pCut1->CostF ) return -1;
if ( pCut0->CostF < pCut1->CostF ) return 1;
if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
return 0;
@ -1230,7 +1230,7 @@ void Gia_ManComputeCutsCore( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fT
Vec_Wec_t * Gia_ManCompute54Cuts( Gia_Man_t * pGia, int fVerbose )
{
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, 5, 16, 0, fVerbose );
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, 5, 8, 0, fVerbose );
Vec_Wec_t * vRes = Vec_WecAlloc( 1000 );
Vec_Int_t * vLevel; int i, k, c, * pCut;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {

78
src/aig/gia/giaDup.c
View File

@ -1103,23 +1103,31 @@ Vec_Int_t * Gia_ManCreatePerm( int n )
}
return vPerm;
}
Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p )
Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p, int fVerbose )
{
Vec_Int_t * vPiPerm = Gia_ManCreatePerm( Gia_ManCiNum(p) );
Vec_Int_t * vPoPerm = Gia_ManCreatePerm( Gia_ManCoNum(p) );
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
int i, fCompl = 0;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (Abc_Random(0) & 1);
if ( fVerbose ) printf( "Input NP transform: " );
Gia_ManForEachPi( p, pObj, i ) {
Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (fCompl = (Abc_Random(0) & 1));
if ( fVerbose ) printf( "%s%d ", fCompl ? "~":"", Vec_IntEntry(vPiPerm,i) );
}
if ( fVerbose ) printf( "\n" );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (Abc_Random(0) & 1) );
if ( fVerbose ) printf( "Output NP transform: " );
Gia_ManForEachPo( p, pObj, i ) {
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (fCompl = (Abc_Random(0) & 1)) );
if ( fVerbose ) printf( "%s%d ", fCompl ? "~":"", Vec_IntEntry(vPoPerm,i) );
}
if ( fVerbose ) printf( "\n" );
Vec_IntFree( vPiPerm );
Vec_IntFree( vPoPerm );
return pNew;
@ -6601,6 +6609,64 @@ Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * p )
return pTemp;
}
/**Function*************************************************************
Synopsis [Extracting MFFC of the nodes supported by a set of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
// collecting internal nodes and outputs in the MFF of a given set of literals
Vec_Int_t * Gia_ManComputeMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vOuts )
{
Vec_Int_t * vTfo = Vec_IntAlloc( 100 );
Gia_Obj_t * pObj; int i, Lit;
Vec_IntClear( vOuts );
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vLits, Lit, i )
Gia_ObjSetTravIdCurrentId( p, Abc_Lit2Var(Lit) );
Gia_ManForEachAnd( p, pObj, i ) {
if ( Gia_ObjIsTravIdCurrentId(p, i) )
continue;
if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) && Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) )
Gia_ObjSetTravIdCurrentId( p, i ), Vec_IntPush( vTfo, i );
else if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) )
Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId0(pObj, i) );
else if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) )
Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId1(pObj, i) );
}
Gia_ManForEachCo( p, pObj, i )
if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0p(p, pObj)) )
Vec_IntPushUniqueOrder( vOuts, Gia_ObjFaninId0p(p, pObj) );
Vec_IntTwoFilter( vOuts, vTfo );
return vTfo;
}
// extracting the AIG of the MFFC defined by a given set of literals
Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAnds, Vec_Int_t * vCos )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, Lit;
pNew = Gia_ManStart( 5000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->fGiaSimple = 1;
Gia_ManConst0(p)->Value = 0;
Vec_IntForEachEntry( vLits, Lit, i )
Gia_ManObj(p, Abc_Lit2Var(Lit))->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), Abc_LitIsCompl(Lit) );
Gia_ManForEachObjVec( vAnds, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachObjVec( vCos, p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -106,6 +106,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vCofVars );
Vec_IntFreeP( &p->vIdsOrig );
Vec_IntFreeP( &p->vIdsEquiv );
Vec_IntFreeP( &p->vEquLitIds );
Vec_IntFreeP( &p->vLutConfigs );
Vec_IntFreeP( &p->vEdgeDelay );
Vec_IntFreeP( &p->vEdgeDelayR );
@ -641,7 +642,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
}
if ( pPars && pPars->fSlacks )
Gia_ManDfsSlacksPrint( p );
if ( Gia_ManHasMapping(p) && pPars->fMapOutStats )
if ( Gia_ManHasMapping(p) && pPars && pPars->fMapOutStats )
Gia_ManPrintOutputLutStats( p );
}

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

@ -290,15 +290,19 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
int nBoxes = Gia_ManBoxNum(p);
int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
int i, k, Id, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin;
int i, k, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin, iBox;
int nMfsNodes;
word * pTruth, uTruthVar = ABC_CONST(0xAAAAAAAAAAAAAAAA);
Vec_Wec_t * vGroups = Vec_WecStart( nBoxes );
Vec_Int_t * vMfs2Gia, * vMfs2Old;
Vec_Int_t * vGroupMap;
Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft;
Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft, * vBoxKeep;
Vec_Int_t * vArray, * vLeaves;
Vec_Int_t * vMapping, * vMapping2;
Vec_Int_t * vCoDrivers;
Vec_Int_t * vPiBoxes = NULL;
Vec_Int_t * vBbCiMap = NULL;
Vec_Int_t * vBbOutLit = NULL;
int nBbIns = 0, nBbOuts = 0;
if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts );
nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts;
@ -340,8 +344,40 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
assert( curCo == Gia_ManCoNum(p) );
// collect nodes in the given order
if ( nBbOuts > 0 )
{
int iBbOut = 0;
vPiBoxes = Vec_IntStartFull( nBbOuts + nRealPis );
vBbCiMap = Vec_IntStartFull( Gia_ManCiNum(p) );
vBbOutLit = Vec_IntStartFull( nBbOuts );
curCi = nRealPis;
curCo = 0;
for ( i = 0; i < nBoxes; i++ )
{
nBoxIns = Tim_ManBoxInputNum( pManTime, i );
nBoxOuts = Tim_ManBoxOutputNum( pManTime, i );
if ( Tim_ManBoxIsBlack(pManTime, i) )
for ( k = 0; k < nBoxOuts; k++ )
{
assert( iBbOut < nBbOuts );
Vec_IntWriteEntry( vPiBoxes, iBbOut, i );
Vec_IntWriteEntry( vBbCiMap, curCi + k, iBbOut );
iBbOut++;
}
curCo += nBoxIns;
curCi += nBoxOuts;
}
curCo += nRealPos;
assert( curCi == Gia_ManCiNum(p) );
assert( curCo == Gia_ManCoNum(p) );
assert( iBbOut == nBbOuts );
}
vBoxesLeft = Vec_IntAlloc( nBoxes );
vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes );
vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes, vPiBoxes );
Vec_IntUniqify( vBoxesLeft ); // reduce to sorted unique indices expected by the timing manager
vBoxKeep = Vec_IntStart( nBoxes );
Vec_IntForEachEntry( vBoxesLeft, iBox, i )
Vec_IntWriteEntry( vBoxKeep, iBox, 1 );
assert( Vec_IntSize(vBoxesLeft) <= nBoxes );
assert( Vec_IntSize(vMfsTopo) > 0 );
@ -360,13 +396,28 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
// map constant
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, 0), 0 );
// map primary inputs
Gia_ManForEachCiId( p, Id, i )
if ( i < nRealPis )
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, Id), Gia_ManAppendCi(pNew) );
// map primary inputs (real ones and preserved box outputs)
Gia_ManForEachCi( p, pObj, i )
{
int iCiId = Gia_ObjId( p, pObj );
int iBox = pManTime ? Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) ) : -1;
int iBbOut = vBbCiMap ? Vec_IntEntry(vBbCiMap, i) : -1;
if ( iBox >= 0 && !Vec_IntEntry(vBoxKeep, iBox) )
{
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), -1 );
if ( iBbOut >= 0 && vBbOutLit )
Vec_IntWriteEntry( vBbOutLit, iBbOut, -1 );
continue;
}
iLitNew = Gia_ManAppendCi(pNew);
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), iLitNew );
if ( iBbOut >= 0 && vBbOutLit )
Vec_IntWriteEntry( vBbOutLit, iBbOut, iLitNew );
}
// map internal nodes
vLeaves = Vec_IntAlloc( 6 );
vCover = Vec_IntAlloc( 1 << 16 );
vCoDrivers = Vec_IntStartFull( Gia_ManCoNum(p) );
Vec_IntForEachEntry( vMfsTopo, iMfsId, i )
{
pTruth = Sfm_NodeReadTruth( pNtk, iMfsId );
@ -374,16 +425,21 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
if ( Vec_IntSize(vArray) == 1 && Vec_IntEntry(vArray,0) < nBbOuts ) // skip unreal inputs
{
// create CI for the output of black box
assert( Abc_LitIsCompl(iGroup) );
iLitNew = Gia_ManAppendCi( pNew );
assert( vBbOutLit != NULL );
iLitNew = Vec_IntEntry( vBbOutLit, Vec_IntEntry(vArray,0) );
assert( iLitNew >= 0 );
Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
continue;
}
Vec_IntClear( vLeaves );
Vec_IntForEachEntry( vArray, Fanin, k )
{
iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 );
if ( Fanin < nBbOuts )
iLitNew = Vec_IntEntry( vBbOutLit, Fanin );
else
iLitNew = Vec_IntEntry( vMfs2Gia, Fanin );
assert( iLitNew >= 0 );
Vec_IntPush( vLeaves, iLitNew );
}
if ( iGroup == -1 ) // internal node
@ -411,36 +467,36 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) );
}
}
else if ( Abc_LitIsCompl(iGroup) ) // internal CI
else if ( Abc_LitIsCompl(iGroup) ) // internal CI (box output)
{
//Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) );
iLitNew = Gia_ManAppendCi( pNew );
iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId );
if ( iLitNew < 0 )
continue;
}
else // internal CO
{
int iObjOld = Vec_IntEntry( vMfs2Old, iMfsId );
int iCoIdx;
assert( iObjOld >= 0 );
assert( pTruth[0] == uTruthVar || pTruth[0] == ~uTruthVar );
iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) );
//printf("Group = %d. po = %d\n", iGroup>>1, iMfsId );
iLitNew = Abc_LitNotCond( Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar );
iCoIdx = Gia_ObjCioId( Gia_ManObj(p, iObjOld) );
Vec_IntWriteEntry( vCoDrivers, iCoIdx, iLitNew );
}
Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
}
Vec_IntFree( vCover );
Vec_IntFree( vLeaves );
// map primary outputs
// map primary outputs (internal box inputs followed by real POs)
Gia_ManForEachCo( p, pObj, i )
{
if ( i < Gia_ManCoNum(p) - nRealPos ) // internal COs
if ( i < Gia_ManCoNum(p) - nRealPos )
{
iMfsId = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
iGroup = Vec_IntEntry( vGroupMap, iMfsId );
if ( Vec_IntFind(vMfsTopo, iGroup) >= 0 )
{
iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId );
if ( iLitNew < 0 )
continue;
assert( iLitNew >= 0 );
}
iLitNew = Vec_IntEntry( vCoDrivers, i );
if ( iLitNew == -1 )
continue;
Gia_ManAppendCo( pNew, iLitNew );
continue;
}
iLitNew = Vec_IntEntry( vMfs2Gia, Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p, pObj)) );
@ -483,6 +539,11 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
Vec_IntFree( vMfs2Gia );
Vec_IntFree( vMfs2Old );
Vec_IntFree( vBoxesLeft );
Vec_IntFree( vBoxKeep );
Vec_IntFree( vCoDrivers );
Vec_IntFreeP( &vPiBoxes );
Vec_IntFreeP( &vBbCiMap );
Vec_IntFreeP( &vBbOutLit );
return pNew;
}
@ -550,4 +611,3 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars )
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

61
src/aig/gia/giaMulFind.c
View File

@ -726,8 +726,16 @@ Vec_Wrd_t * Gia_ManMulFindSim( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned
}
return vRes;
}
void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fVerbose )
Vec_Wrd_t * Gia_ManMulFindSim2( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned )
{
extern word * product_many(word *pInfo1, int nBits1, word *pInfo2, int nBits2, int fSigned );
word * pRes = product_many( Vec_WrdArray(vSim0), Vec_WrdSize(vSim0), Vec_WrdArray(vSim1), Vec_WrdSize(vSim1), fSigned );
return Vec_WrdAllocArray( pRes, Vec_WrdSize(vSim0) + Vec_WrdSize(vSim1) );
}
int Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fVerbose )
{
//abctime clkTotal = Abc_Clock();
int nDetected = 0;
Abc_Random(1);
for ( int m = 0; m < Vec_WecSize(vTerms)/3; m++ ) {
Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0);
@ -735,8 +743,8 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV
Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2);
Vec_Wrd_t * vSim0 = Vec_WrdStartRandom( Vec_IntSize(vIn0) );
Vec_Wrd_t * vSim1 = Vec_WrdStartRandom( Vec_IntSize(vIn1) );
Vec_Wrd_t * vSimU = Gia_ManMulFindSim( vSim0, vSim1, 0 );
Vec_Wrd_t * vSimS = Gia_ManMulFindSim( vSim0, vSim1, 1 );
Vec_Wrd_t * vSimU = Gia_ManMulFindSim2( vSim0, vSim1, 0 );
Vec_Wrd_t * vSimS = Gia_ManMulFindSim2( vSim0, vSim1, 1 );
Vec_Int_t * vTfo = Gia_ManMulFindTfo( p, vIn0, vIn1, fLits );
Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo, fLits );
Vec_Int_t * vOutU = Vec_IntAlloc( 100 );
@ -762,10 +770,14 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV
if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntSize(vOutU) ||
Vec_IntCountEntry(vOutS, -1) < Vec_IntSize(vOutS) )
{
if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) )
if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) ) {
Vec_IntAppend( vOut, vOutU ), Vec_IntPush(vOut, 0);
else
nDetected = Vec_IntSize(vOutU) - Vec_IntCountEntry(vOutU, -1);
}
else {
Vec_IntAppend( vOut, vOutS ), Vec_IntPush(vOut, 1);
nDetected = Vec_IntSize(vOutS) - Vec_IntCountEntry(vOutS, -1);
}
}
else
{
@ -782,6 +794,8 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fV
Vec_IntFree( vOutS );
}
Vec_WecRemoveEmpty( vTerms );
//Abc_PrintTime( 1, "Output detection time", Abc_Clock() - clkTotal );
return nDetected;
}
/**Function*************************************************************
@ -831,23 +845,40 @@ void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast )
{
int i, Temp, Limit = Vec_IntSize(vSet) - fSkipLast;
printf( "{" );
Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) {
if ( Temp == -1 )
printf( "n/a%s", i < Limit-1 ? " ":"" );
else
printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
if ( Vec_IntSize(vSet) > 16 ) {
Vec_IntForEachEntryStop( vSet, Temp, i, 4 ) {
if ( Temp == -1 )
printf( "n/a%s", i < Limit-1 ? " ":"" );
else
printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
}
printf( "... " );
Vec_IntForEachEntryStartStop( vSet, Temp, i, Limit-4, Limit ) {
if ( Temp == -1 )
printf( "n/a%s", i < Limit-1 ? " ":"" );
else
printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
}
}
else {
Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) {
if ( Temp == -1 )
printf( "n/a%s", i < Limit-1 ? " ":"" );
else
printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
}
}
printf( "}" );
}
void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth )
void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth, int fInputLits )
{
Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0);
Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1);
Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2);
printf( "%sooth %ssigned %d x %d: ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un", Vec_IntSize(vIn0), Vec_IntSize(vIn1) );
Gia_ManMulFindPrintSet( vIn0, 0, 0 );
Gia_ManMulFindPrintSet( vIn0, fInputLits, 0 );
printf( " * " );
Gia_ManMulFindPrintSet( vIn1, 0, 0 );
Gia_ManMulFindPrintSet( vIn1, fInputLits, 0 );
printf( " = " );
Gia_ManMulFindPrintSet( vOut, 1, 1 );
printf( "\n" );
@ -862,9 +893,9 @@ void Gia_ManMulFind( Gia_Man_t * p, int nCutNum, int fVerbose )
Vec_Wec_t * vTermsA = Gia_ManMulFindA( p, vCuts3, fVerbose );
printf( "Detected %d booth and %d non-booth multipliers.\n", Vec_WecSize(vTermsB)/3, Vec_WecSize(vTermsA)/3 );
for ( m = 0; m < Vec_WecSize(vTermsA)/3; m++ )
Gia_ManMulFindPrintOne( vTermsA, m, 0 );
Gia_ManMulFindPrintOne( vTermsA, m, 0, 0 );
for ( m = 0; m < Vec_WecSize(vTermsB)/3; m++ )
Gia_ManMulFindPrintOne( vTermsB, m, 1 );
Gia_ManMulFindPrintOne( vTermsB, m, 1, 0 );
Vec_WecFree( vTermsB );
Vec_WecFree( vTermsA );
Vec_WecFree( vCuts3 );

120
src/aig/gia/giaTim.c
View File

@ -952,7 +952,100 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
SeeAlso []
***********************************************************************/
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec )
Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 )
{
Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2));
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
int i, Entry, iRepr, fCompl, iLit;
Gia_Obj_t * pObj;
Gia_ManSetPhase( p1 );
Gia_ManSetPhase( p2 );
Vec_IntForEachEntry( vMap1, Entry, i )
{
if ( Entry == -1 )
continue;
pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
if ( ~pObj->Value == 0 )
continue;
fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) );
Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit( i, fCompl ) );
}
Vec_IntForEachEntry( vMap2, Entry, i )
{
if ( Entry == -1 )
continue;
pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
if ( ~pObj->Value == 0 )
continue;
fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) );
if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 )
continue;
Vec_IntWriteEntry( vRes, i, Abc_LitNotCond( iLit, fCompl ) );
}
Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 );
Vec_IntForEachEntry( vMap1, Entry, i )
{
if ( Entry == -1 )
continue;
pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
if ( !Gia_ObjIsCo(pObj) )
continue;
Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i );
}
Vec_IntForEachEntry( vMap2, Entry, i )
{
if ( Entry == -1 )
continue;
pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
if ( !Gia_ObjIsCo(pObj) )
continue;
assert( Vec_IntEntry(vRes, i) == -1 );
Vec_IntWriteEntry( vRes, i, Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 ) );
assert( Vec_IntEntry(vRes, i) != -1 );
}
Vec_IntFree( vMap );
return vRes;
}
void Gia_ManVerifyVerifyNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2, Vec_Int_t * vMapRes )
{
int iImpl, iReprSpec, iReprImpl, nSize = Vec_IntSize(vMap2);
Gia_Obj_t * pObjSpec, * pObjImpl;
if ( vMapRes == NULL || p == NULL || p->pReprs == NULL )
return;
assert( Vec_IntSize(vMapRes) == nSize );
Gia_ManSetPhase( p1 );
Gia_ManSetPhase( p2 );
for ( iImpl = 0; iImpl < nSize; iImpl++ )
if ( Vec_IntEntry(vMapRes, iImpl) >= 0 )
{
int Entry = Vec_IntEntry( vMapRes, iImpl );
int iSpec = Abc_Lit2Var( Entry );
int fCompl = Abc_LitIsCompl( Entry );
int iLitSpec = Vec_IntEntry( vMap1, iSpec );
int iLitImpl = Vec_IntEntry( vMap2, iImpl );
pObjSpec = Gia_ManObj( p1, Abc_Lit2Var(iLitSpec) );
if ( Gia_ObjIsCo(pObjSpec) )
continue;
if ( ~pObjSpec->Value == 0 )
continue;
pObjImpl = Gia_ManObj( p2, Abc_Lit2Var(iLitImpl) );
if ( ~pObjImpl->Value == 0 )
continue;
iReprSpec = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjSpec->Value) );
iReprImpl = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjImpl->Value) );
if ( iReprSpec != iReprImpl )
printf( "Found functional mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec );
if ( (pObjImpl->fPhase ^ Abc_LitIsCompl(iLitImpl)) != (pObjSpec->fPhase ^ Abc_LitIsCompl(iLitSpec) ^ fCompl) )
printf( "Found phase mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec );
}
}
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fObjIdMap, int fDumpFiles, int fVerbose, char * pFileSpec )
{
int Status = -1;
Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
@ -1052,12 +1145,30 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
{
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
Cec_ManCecSetDefaultParams( pPars );
pPars->nBTLimit = nBTLimit;
pPars->TimeLimit = nTimeLim;
pPars->fVerbose = fVerbose;
pPars->nBTLimit = nBTLimit;
pPars->TimeLimit = nTimeLim;
pPars->fUseOrigIds = fObjIdMap;
pPars->fVerbose = fVerbose;
Status = Cec_ManVerify( pMiter, pPars );
if ( pPars->iOutFail >= 0 )
Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
if ( fObjIdMap ) {
Gia_Man_t * pReduced = Gia_ManOrigIdsReduce( pMiter, pMiter->vIdsEquiv );
Gia_ManStop( pReduced );
Gia_Obj_t * pObj; int i;
Vec_Int_t * vCopy0 = Vec_IntAlloc(Gia_ManObjNum(pSpec));
Gia_ManForEachObj( pSpec, pObj, i )
Vec_IntPush( vCopy0, pObj->Value );
Vec_Int_t * vCopy1 = Vec_IntAlloc(Gia_ManObjNum(pGia));
Gia_ManForEachObj( pGia, pObj, i )
Vec_IntPush( vCopy1, pObj->Value );
Vec_IntFreeP( &pGia->vEquLitIds );
pGia->vEquLitIds = Gia_ManVerifyFindNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1 );
assert( Vec_IntSize(pGia->vEquLitIds) == Gia_ManObjNum(pGia) );
Gia_ManVerifyVerifyNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1, pGia->vEquLitIds );
Vec_IntFree( vCopy0 );
Vec_IntFree( vCopy1 );
}
Gia_ManStop( pMiter );
}
}
@ -1094,4 +1205,3 @@ Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia )
ABC_NAMESPACE_IMPL_END

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

@ -172,6 +172,7 @@ static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAndExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1002,6 +1003,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact", Abc_CommandMajExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "andexact", Abc_CommandAndExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 );
@ -10768,7 +10770,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmpvh" ) ) != EOF )
{
switch ( c )
{
@ -10896,6 +10898,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMinNodes ^= 1;
break;
case 'p':
pPars->fUsePerm ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -10945,15 +10950,31 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize );
return 1;
}
if ( pPars->nVars > 12 )
if ( pPars->fKissat )
{
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
if ( pPars->nVars > 14 )
{
Abc_Print( -1, "Function should not have more than 14 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 8 )
{
Abc_Print( -1, "Node size should not be more than 8 inputs.\n" );
return 1;
}
}
if ( pPars->nLutSize > 6 )
else
{
Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
return 1;
if ( pPars->nVars > 12 )
{
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 6 )
{
Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
return 1;
}
}
if ( pPars->nRandFuncs ) {
pPars->fGlucose = 1;
@ -10972,8 +10993,8 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmpvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of N-input function using M K-input lookup-tables\n" );
Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-M <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
@ -10994,6 +11015,187 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle use specialized permutation when minimizing nodes [default = %s]\n", pPars->fUsePerm ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAndExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
extern char * Abc_NtkReadTruth( Abc_Ntk_t * pNtk );
int c;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMTSHYiadsmvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nVars < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nNodes < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->RuntimeLim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->RuntimeLim < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->Seed < 0 )
goto usage;
break;
case 'H':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-H\" should be followed by a string.\n" );
goto usage;
}
pPars->n1HotAlgo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'Y':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" );
goto usage;
}
pPars->pSymStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'i':
pPars->fUseIncr ^= 1;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'd':
pPars->fDumpBlif ^= 1;
break;
case 's':
pPars->fSilent ^= 1;
break;
case 'm':
pPars->fMinNodes ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc == globalUtilOptind + 1 )
pPars->pTtStr = argv[globalUtilOptind];
else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
{
pPars->pTtStr = Abc_NtkReadTruth( Abc_FrameReadNtk(pAbc) );
if ( pPars->pTtStr )
pPars->nVars = Abc_NtkCiNum(Abc_FrameReadNtk(pAbc));
}
if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 )
{
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( pPars->nVars == 0 && pPars->pTtStr )
pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr));
if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
}
if ( pPars->nVars == 0 && pPars->pSymStr )
pPars->nVars = (int)strlen(pPars->pSymStr) - 1;
if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) )
{
Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) );
return 1;
}
if ( pPars->nVars > pPars->nNodes + 1 )
{
Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input nodes.\n", pPars->nVars, pPars->nNodes );
return 1;
}
if ( pPars->nVars > 14 )
{
Abc_Print( -1, "Function should not have more than 14 inputs.\n" );
return 1;
}
if ( pPars->nNodes > 16 )
{
Abc_Print( -1, "Node count cannot be more than 16 inputs.\n" );
return 1;
}
if ( pPars->fMinNodes )
Exa9_ManExactSynthesisIter( pPars );
else
Exa9_ManExactSynthesis( pPars );
if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
ABC_FREE( pPars->pTtStr );
return 0;
usage:
Abc_Print( -2, "usage: andexact [-NMTSH <num>] [-Y str] [-iadmsvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of N-input function using two-input gates\n" );
Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-M <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-S <num> : the random seed for random function generation with -F <num> [default = %d]\n", pPars->Seed );
Abc_Print( -2, "\t-H <num> : the 1-hotness algorithm used (0 = naive; 1 = seq; 2 = bim; 3 = cmd) [default = %d]\n", pPars->n1HotAlgo );
Abc_Print( -2, "\t-Y <str> : charasteristic string of a symmetric function [default = %s]\n", pPars->pSymStr ? pPars->pSymStr : "unused" );
Abc_Print( -2, "\t-i : toggle using incremental SAT (CEGAR over minterms) [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
@ -42241,9 +42443,9 @@ usage:
int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * pFileSpec = NULL;
int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fDumpFiles = 0, fVerbose = 0;
int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fObjIdMap = 0, fDumpFiles = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTsdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTsmdvh" ) ) != EOF )
{
switch ( c )
{
@ -42272,6 +42474,9 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSeq ^= 1;
break;
case 'm':
fObjIdMap ^= 1;
break;
case 'd':
fDumpFiles ^= 1;
break;
@ -42290,15 +42495,16 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
Extra_FileNameCorrectPath( pFileSpec );
printf( "Taking spec from file \"%s\".\n", pFileSpec );
}
Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fDumpFiles, fVerbose, pFileSpec );
Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fObjIdMap, fDumpFiles, fVerbose, pFileSpec );
return 0;
usage:
Abc_Print( -2, "usage: &verify [-CT num] [-sdvh] <file>\n" );
Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] <file>\n" );
Abc_Print( -2, "\t performs verification of combinational design\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeLim );
Abc_Print( -2, "\t-s : toggle using sequential verification [default = %s]\n", fSeq? "yes":"no");
Abc_Print( -2, "\t-m : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no");
Abc_Print( -2, "\t-d : toggle dumping AIGs to be compared [default = %s]\n", fDumpFiles? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
@ -48170,7 +48376,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p, int fVerbose );
Gia_Man_t * pTemp;
int c, RandSeed = 0, fVerbose = 0;
Extra_UtilGetoptReset();
@ -48211,7 +48417,7 @@ int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Random(1);
for ( c = 0; c < RandSeed; c++ )
Abc_Random(0);
pTemp = Gia_ManDupRandPerm( pAbc->pGia );
pTemp = Gia_ManDupRandPerm( pAbc->pGia, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;

1
src/misc/util/module.make
View File

@ -7,6 +7,7 @@ SRC += src/misc/util/utilBridge.c \
src/misc/util/utilIsop.c \
src/misc/util/utilLinear.c \
src/misc/util/utilMiniver.c \
src/misc/util/utilMulSim.c \
src/misc/util/utilNam.c \
src/misc/util/utilPrefix.cpp \
src/misc/util/utilPth.c \

230
src/misc/util/utilMulSim.c Normal file
View File

@ -0,0 +1,230 @@
/**CFile****************************************************************
FileName [utilMulSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Generating multiplier simulation info.]
Synopsis [Generating multiplier simulation info.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Feburary 13, 2011.]
Revision [$Id: utilMulSim.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <assert.h>
#include "misc/util/abc_global.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define SIG_WIDTH 64 // 64 simulation patterns in each signature word
// ----------------------------------------------------------------------
// Core 32-bit-limb big integer unsigned multiply
// ----------------------------------------------------------------------
uint32_t * product(const uint32_t *pArg1, int nInts1,
const uint32_t *pArg2, int nInts2)
{
assert( pArg1 && pArg2 && nInts1 > 0 && nInts2 > 0 );
int nRes = nInts1 + nInts2;
uint32_t *pRes = (uint32_t *)calloc((size_t)nRes, sizeof(uint32_t));
if (!pRes) return NULL;
// Schoolbook multiplication in base 2^32
for (int i = 0; i < nInts1; ++i) {
uint64_t a = pArg1[i];
if (a == 0) continue;
uint64_t carry = 0;
for (int j = 0; j < nInts2; ++j) {
uint64_t t = (uint64_t)pRes[i + j] + a * (uint64_t)pArg2[j] + carry;
pRes[i + j] = (uint32_t)t;
carry = t >> 32;
}
pRes[i + nInts2] = (uint32_t)carry;
}
return pRes;
}
// ----------------------------------------------------------------------
// Bit-matrix helpers: signatures <-> per-pattern 32-bit-limb big ints
// ----------------------------------------------------------------------
static void transpose_signatures_to_pattern(const uint64_t *sigs,
int nBits,
uint32_t *dst,
int nInts,
int patternIdx)
{
memset(dst, 0, (size_t)nInts * sizeof(uint32_t));
for (int bit = 0; bit < nBits; ++bit) {
uint64_t sigWord = sigs[bit];
uint64_t bitVal = (sigWord >> patternIdx) & 1ULL;
if (!bitVal) continue;
int word = bit / 32;
int offset = bit & 31;
dst[word] |= (uint32_t)(1u << offset);
}
}
static void transpose_pattern_to_signatures(const uint32_t *src,
int nIntsRes,
int nBitsRes,
uint64_t *outSigs,
int patternIdx)
{
for (int bit = 0; bit < nBitsRes; ++bit) {
int word = bit / 32;
int offset = bit & 31;
if (word >= nIntsRes)
break;
uint32_t bitVal = (src[word] >> offset) & 1u;
if (bitVal)
outSigs[bit] |= (uint64_t)1ULL << patternIdx;
}
}
// ----------------------------------------------------------------------
// Signed helpers for 32-bit-limb big ints (two's complement on nBits)
// ----------------------------------------------------------------------
static int is_negative(const uint32_t *x, int nBits)
{
int bitPos = nBits - 1;
int word = bitPos / 32;
int offset = bitPos & 31;
return (x[word] >> offset) & 1u;
}
static void mask_to_nBits(uint32_t *x, int nInts, int nBits)
{
if (nBits <= 0) {
for (int i = 0; i < nInts; ++i)
x[i] = 0;
return;
}
int lastWord = (nBits - 1) / 32; // index of last used word
int usedBitsInLast = nBits - lastWord * 32; // 1..32
// Zero any words above the last used word
for (int i = lastWord + 1; i < nInts; ++i)
x[i] = 0;
// If nBits is not a multiple of 32, mask off the high bits of last word
if (usedBitsInLast < 32) {
uint32_t mask = ((uint32_t)1u << usedBitsInLast) - 1u;
x[lastWord] &= mask;
}
}
static void twos_complement_inplace(uint32_t *x, int nInts, int nBits)
{
// Invert
for (int i = 0; i < nInts; ++i)
x[i] = ~x[i];
mask_to_nBits(x, nInts, nBits);
// Add 1
uint64_t carry = 1;
for (int i = 0; i < nInts; ++i) {
uint64_t sum = (uint64_t)x[i] + carry;
x[i] = (uint32_t)sum;
carry = sum >> 32;
if (!carry)
break;
}
mask_to_nBits(x, nInts, nBits);
}
// ----------------------------------------------------------------------
// product_many: unsigned and signed (two's-complement) versions
// ----------------------------------------------------------------------
uint64_t * product_many_unsigned(uint64_t *pInfo1, int nBits1,
uint64_t *pInfo2, int nBits2)
{
assert( pInfo1 && pInfo2 && nBits1 > 0 && nBits2 > 0 );
int nInts1 = (nBits1 + 31) / 32;
int nInts2 = (nBits2 + 31) / 32;
int nBitsRes = nBits1 + nBits2;
int nIntsRes = nInts1 + nInts2;
uint64_t *outSigs = (uint64_t *)calloc((size_t)nBitsRes, sizeof(uint64_t));
if (!outSigs) return NULL;
uint32_t *tmp1 = (uint32_t *)calloc((size_t)nInts1, sizeof(uint32_t));
uint32_t *tmp2 = (uint32_t *)calloc((size_t)nInts2, sizeof(uint32_t));
assert( tmp1 && tmp2 );
for (int pattern = 0; pattern < SIG_WIDTH; ++pattern) {
transpose_signatures_to_pattern(pInfo1, nBits1, tmp1, nInts1, pattern);
transpose_signatures_to_pattern(pInfo2, nBits2, tmp2, nInts2, pattern);
uint32_t *tmpRes = product(tmp1, nInts1, tmp2, nInts2); assert( tmpRes );
transpose_pattern_to_signatures(tmpRes, nIntsRes, nBitsRes, outSigs, pattern);
free(tmpRes);
}
free(tmp1);
free(tmp2);
return outSigs;
}
uint64_t * product_many_signed(uint64_t *pInfo1, int nBits1,
uint64_t *pInfo2, int nBits2)
{
assert( pInfo1 && pInfo2 && nBits1 > 0 && nBits2 > 0 );
int nInts1 = (nBits1 + 31) / 32;
int nInts2 = (nBits2 + 31) / 32;
int nBitsRes = nBits1 + nBits2;
int nIntsRes = nInts1 + nInts2;
uint64_t *outSigs = (uint64_t *)calloc((size_t)nBitsRes, sizeof(uint64_t));
if (!outSigs) return NULL;
uint32_t *op1 = (uint32_t *)calloc((size_t)nInts1, sizeof(uint32_t));
uint32_t *op2 = (uint32_t *)calloc((size_t)nInts2, sizeof(uint32_t));
assert( op1 && op2 );
for (int pattern = 0; pattern < SIG_WIDTH; ++pattern) {
transpose_signatures_to_pattern(pInfo1, nBits1, op1, nInts1, pattern);
transpose_signatures_to_pattern(pInfo2, nBits2, op2, nInts2, pattern);
int neg1 = is_negative(op1, nBits1);
int neg2 = is_negative(op2, nBits2);
int negRes = neg1 ^ neg2;
if (neg1) twos_complement_inplace(op1, nInts1, nBits1);
if (neg2) twos_complement_inplace(op2, nInts2, nBits2);
uint32_t *tmpRes = product(op1, nInts1, op2, nInts2); assert( tmpRes );
if (negRes)
twos_complement_inplace(tmpRes, nIntsRes, nBitsRes);
else
mask_to_nBits(tmpRes, nIntsRes, nBitsRes);
transpose_pattern_to_signatures(tmpRes, nIntsRes, nBitsRes, outSigs, pattern);
free(tmpRes);
}
free(op1);
free(op2);
return outSigs;
}
word * product_many(word *pInfo1, int nBits1, word *pInfo2, int nBits2, int fSigned )
{
if ( fSigned )
return (word *)product_many_signed((uint64_t *)pInfo1, nBits1, (uint64_t *)pInfo2, nBits2);
else
return (word *)product_many_unsigned((uint64_t *)pInfo1, nBits1, (uint64_t *)pInfo2, nBits2);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

6
src/misc/vec/vecInt.h
View File

@ -1947,16 +1947,16 @@ static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Synopsis [Keeps only those entries in vArr1, which are in vArr2.]
Description [Keeps only those entries of vArr1, which are in vArr2.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntTwoMerge1( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
static inline void Vec_IntTwoFilter( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
{
int * pBeg = vArr1->pArray;
int * pBeg1 = vArr1->pArray;

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

@ -95,7 +95,7 @@ extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
/*=== sfmWin.c ==========================================================*/
extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes );
extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes );
ABC_NAMESPACE_HEADER_END
@ -105,4 +105,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

66
src/opt/sfm/sfmWin.c
View File

@ -133,37 +133,52 @@ static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return
SeeAlso []
***********************************************************************/
void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft )
static void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes );
static void Sfm_NtkDfsVisitGroup( Sfm_Ntk_t * p, int iGroup, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes )
{
int i, iFanin;
if ( Sfm_ObjIsPi(p, iNode) )
return;
int i, iFanin, k, Obj;
Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
Vec_IntForEachEntry( vGroup, Obj, i )
assert( Sfm_ObjIsNode(p, Obj) );
Vec_IntForEachEntry( vGroup, Obj, i )
Sfm_ObjSetTravIdCurrent( p, Obj );
Vec_IntForEachEntry( vGroup, Obj, i )
Sfm_ObjForEachFanin( p, Obj, iFanin, k )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
Vec_IntForEachEntry( vGroup, Obj, i )
Vec_IntPush( vNodes, Obj );
Vec_IntPush( vBoxesLeft, iGroup );
}
static void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes )
{
int i, iFanin, iGroup;
if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
return;
if ( Vec_IntEntry(vGroupMap, iNode) >= 0 )
iGroup = Vec_IntEntry(vGroupMap, iNode);
if ( iGroup >= 0 )
{
int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) );
Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
Vec_IntForEachEntry( vGroup, iNode, i )
assert( Sfm_ObjIsNode(p, iNode) );
Vec_IntForEachEntry( vGroup, iNode, i )
Sfm_ObjSetTravIdCurrent( p, iNode );
Vec_IntForEachEntry( vGroup, iNode, i )
Sfm_ObjForEachFanin( p, iNode, iFanin, k )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
Vec_IntForEachEntry( vGroup, iNode, i )
Vec_IntPush( vNodes, iNode );
Vec_IntPush( vBoxesLeft, iGroup );
Sfm_NtkDfsVisitGroup( p, Abc_Lit2Var(iGroup), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
return;
}
else
if ( Sfm_ObjIsPi(p, iNode) )
{
Sfm_ObjSetTravIdCurrent(p, iNode);
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
Vec_IntPush( vNodes, iNode );
if ( vPiBoxes && iNode < Vec_IntSize(vPiBoxes) )
{
int iBox = Vec_IntEntry( vPiBoxes, iNode );
if ( iBox >= 0 )
{
Sfm_ObjSetTravIdCurrent( p, iNode );
Sfm_NtkDfsVisitGroup( p, iBox, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
}
}
return;
}
Sfm_ObjSetTravIdCurrent(p, iNode);
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
Vec_IntPush( vNodes, iNode );
}
Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes )
Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes )
{
Vec_Int_t * vNodes;
int i;
@ -174,10 +189,10 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa
{
Vec_Int_t * vGroup;
Vec_WecForEachLevel( vGroups, vGroup, i )
Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
}
Sfm_NtkForEachPo( p, i )
Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
return vNodes;
}
@ -478,4 +493,3 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
ABC_NAMESPACE_IMPL_END

1
src/proof/cec/cec.h
View File

@ -135,6 +135,7 @@ struct Cec_ParCec_t_
int fUseSmartCnf; // use smart CNF computation
int fRewriting; // enables AIG rewriting
int fNaive; // performs naive SAT-based checking
int fUseOrigIds; // enable recording of original IDs
int fSilent; // print no messages
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats

3
src/proof/cec/cecCec.c
View File

@ -359,11 +359,13 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
pParsFra->nItersMax = 1000;
pParsFra->nBTLimit = pPars->nBTLimit;
pParsFra->TimeLimit = pPars->TimeLimit;
pParsFra->fUseOrigIds = pPars->fUseOrigIds;
pParsFra->fVerbose = pPars->fVerbose;
pParsFra->fVeryVerbose = pPars->fVeryVerbose;
pParsFra->fCheckMiter = 1;
pParsFra->fDualOut = 1;
pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent );
ABC_SWAP( Vec_Int_t *, pInit->vIdsEquiv, p->vIdsEquiv );
pPars->iOutFail = pParsFra->iOutFail;
// update
pInit->pCexComb = p->pCexComb; p->pCexComb = NULL;
@ -383,6 +385,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
}
return 0;
}
Vec_IntFreeP( &pInit->vIdsEquiv );
p = Gia_ManDup( pInit );
Gia_ManEquivFixOutputPairs( p );
p = Gia_ManCleanup( pNew = p );

4
src/sat/bmc/bmc.h
View File

@ -68,10 +68,12 @@ struct Bmc_EsPar_t_
int fLutCascade;
int fLutInFixed;
int fMinNodes;
int fUsePerm;
int RuntimeLim;
int nRandFuncs;
int nMintNum;
int Seed;
int n1HotAlgo;
int fDumpBlif;
int fVerbose;
int fSilent;
@ -101,6 +103,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
pPars->fUniqFans = 0;
pPars->fLutCascade = 0;
pPars->RuntimeLim = 0;
pPars->n1HotAlgo = 1;
pPars->fVerbose = 0;
}
@ -273,4 +276,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

19
src/sat/bmc/bmcMaj8.c
View File

@ -47,6 +47,7 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
#define MAJ_MAX_LUT 8
typedef struct Exa8_Man_t_ Exa8_Man_t;
struct Exa8_Man_t_
@ -63,7 +64,7 @@ struct Exa8_Man_t_
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
int VarMarks[MAJ_NOBJS][MAJ_MAX_LUT][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS]; // values of the first nVars variables
Vec_Wec_t * vOutLits; // output vars
Vec_Wec_t * vInVars; // input vars
@ -214,6 +215,7 @@ static int Exa8_ManMarkup( Exa8_Man_t * p )
{
int i, k, j;
assert( p->nObjs <= MAJ_NOBJS );
assert( p->nLutSize <= MAJ_MAX_LUT );
// assign functionality variables
p->iVar = 1 + p->LutMask * p->nNodes;
// assign connectivity variables
@ -347,7 +349,7 @@ static inline int Exa8_ManFindFanin( Exa8_Man_t * p, int i, int k )
static inline int Exa8_ManEval( Exa8_Man_t * p )
{
static int Flag = 0;
int i, k, j, iMint; word * pFanins[6];
int i, k, j, iMint; word * pFanins[MAJ_MAX_LUT];
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
@ -678,7 +680,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
abctime clkTotal = Abc_Clock();
Exa8_Man_t * p;
int fCompl = 0;
word pTruth[64];
assert( pPars->nVars <= 14 );
assert( pPars->nLutSize <= 8 );
int nTruthWords = Abc_TtWordNum( pPars->nVars );
word * pTruth = ABC_CALLOC( word, nTruthWords );
assert( pTruth );
if ( pPars->pSymStr ) {
word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
@ -689,8 +695,6 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->pTtStr )
Abc_TtReadHex( pTruth, pPars->pTtStr );
else assert( 0 );
assert( pPars->nVars <= 12 );
assert( pPars->nLutSize <= 6 );
if ( pPars->fUseIncr && !pPars->fSilent )
printf( "Warning: Ignoring incremental option when using Kissat.\n" );
pPars->fUseIncr = 0;
@ -758,6 +762,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa8_ManFree( p );
ABC_FREE( pTruth );
return Res;
}
@ -770,7 +775,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
printf( "\nTrying M = %d:\n", n );
pPars->nNodes = n;
if ( fGenPerm ) {
if ( !pPars->fUsePerm && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
@ -790,7 +795,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
if ( 0 && fGenPerm ) {
else if ( pPars->fUsePerm && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );

1011
src/sat/bmc/bmcMaj9.c Normal file
View File

File diff suppressed because it is too large Load Diff

1
src/sat/bmc/module.make
View File

@ -27,6 +27,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcMaj3.c \
src/sat/bmc/bmcMaj7.c \
src/sat/bmc/bmcMaj8.c \
src/sat/bmc/bmcMaj9.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMesh.c \
src/sat/bmc/bmcMesh2.c \