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

Enabling AIGs without structural hashing.

This commit is contained in:
Alan Mishchenko 2016-05-20 13:50:19 -07:00
parent c6a290ee97
commit 555ed0b158
14 changed files with 60 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -112,6 +112,7 @@ struct Gia_Man_t_
int nHTable; // hash table size
int fAddStrash; // performs additional structural hashing
int fSweeper; // sweeper is running
int fGiaSimple; // simple mode (no const-propagation and strashing)
int * pRefs; // the reference count
int * pLutRefs; // the reference count
Vec_Int_t * vLevels; // levels of the nodes
@ -632,7 +633,7 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
Gia_Obj_t * pObj = Gia_ManAppendObj( p );
assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
assert( p->fGiaSimple || Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
if ( iLit0 < iLit1 )
{
pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
@ -1112,8 +1113,8 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck );
extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
extern Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );

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

@ -173,7 +173,7 @@ Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck )
Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck )
{
Gia_Man_t * pNew, * pTemp;
Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
@ -255,6 +255,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pNew->nConstrs = nConstr;
pNew->fGiaSimple = fGiaSimple;
// prepare the array of nodes
vNodes = Vec_IntAlloc( 1 + nTotal );
@ -282,7 +283,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
}
// create the AND gates
if ( !fSkipStrash )
if ( !fGiaSimple && !fSkipStrash )
Gia_ManHashAlloc( pNew );
for ( i = 0; i < nAnds; i++ )
{
@ -293,7 +294,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
if ( fSkipStrash )
if ( !fGiaSimple && fSkipStrash )
{
if ( iNode0 == iNode1 )
Vec_IntPush( vNodes, Gia_ManAppendBuf(pNew, iNode0) );
@ -303,7 +304,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
else
Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
}
if ( !fSkipStrash )
if ( !fGiaSimple && !fSkipStrash )
Gia_ManHashStop( pNew );
// remember the place where symbols begin
@ -526,7 +527,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
vStr = Vec_StrStart( Gia_AigerReadInt(pCur) ); pCur += 4;
memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
pCur += Vec_StrSize(vStr);
pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 );
pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0, 0 );
Vec_StrFree( vStr );
if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
}
@ -790,7 +791,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
Vec_IntFreeP( &vPoTypes );
}
if ( !fSkipStrash && Gia_ManHasDangling(pNew) )
if ( !fGiaSimple && !fSkipStrash && Gia_ManHasDangling(pNew) )
{
Tim_Man_t * pManTime;
Vec_Int_t * vFlopMap, * vGateMap, * vObjMap;
@ -853,7 +854,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
ABC_FREE( pInit );
}
Vec_IntFreeP( &vInits );
if ( !fSkipStrash && pNew->vMapping )
if ( !fGiaSimple && !fSkipStrash && pNew->vMapping )
{
Abc_Print( 0, "Structural hashing enabled while reading AIGER invalidated the mapping. Consider using \"&r -s\".\n" );
Vec_IntFreeP( &pNew->vMapping );
@ -872,7 +873,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck )
{
FILE * pFile;
Gia_Man_t * pNew;
@ -888,7 +889,7 @@ Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
RetValue = fread( pContents, nFileSize, 1, pFile );
fclose( pFile );
pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fGiaSimple, fSkipStrash, fCheck );
ABC_FREE( pContents );
if ( pNew )
{

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

@ -1185,7 +1185,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
return;
}
// read AIGER file
pMiter = Gia_AigerRead( pFileName, 0, 0 );
pMiter = Gia_AigerRead( pFileName, 0, 0, 0 );
if ( pMiter == NULL )
{
Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
@ -1869,13 +1869,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_AigerRead( pName1, 0, 0 );
pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
if ( pGia1 == NULL )
{
Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_AigerRead( pName2, 0, 0 );
pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );
@ -2008,13 +2008,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_AigerRead( pName1, 0, 0 );
pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
if ( pGia1 == NULL )
{
Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_AigerRead( pName2, 0, 0 );
pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );

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

@ -575,7 +575,11 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
***********************************************************************/
int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
{
// return Gia_ManAppendAnd2( p, iLit0, iLit1 );
if ( p->fGiaSimple )
{
assert( p->nHTable == 0 );
return Gia_ManAppendAnd( p, iLit0, iLit1 );
}
if ( iLit0 < 2 )
return iLit0 ? iLit1 : 0;
if ( iLit1 < 2 )

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

@ -906,7 +906,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
return Status;
}
// read original AIG
pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0, 0 );
if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
{
Gia_ManStop( pSpec );

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

@ -14737,7 +14737,7 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_AigerRead( FileName, 1, 0 );
pGia = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -15043,7 +15043,7 @@ int Abc_CommandRecMerge3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_AigerRead( FileName, 1, 0 );
pGia = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -26331,12 +26331,16 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUseMini = 0;
int fVerbose = 0;
int fGiaSimple = 0;
int fSkipStrash = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "smvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fGiaSimple ^= 1;
break;
case 's':
fSkipStrash ^= 1;
break;
@ -26379,14 +26383,15 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
// else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
// Abc3_ReadShowHie( FileName, fSkipStrash );
else
pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
pAig = Gia_AigerRead( FileName, fGiaSimple, fSkipStrash, 0 );
if ( pAig )
Abc_FrameUpdateGia( pAbc, pAig );
return 0;
usage:
Abc_Print( -2, "usage: &r [-smvh] <file>\n" );
Abc_Print( -2, "usage: &r [-csmvh] <file>\n" );
Abc_Print( -2, "\t reads the current AIG from the AIGER file\n" );
Abc_Print( -2, "\t-c : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-s : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
@ -30628,7 +30633,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -30791,7 +30796,7 @@ int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -32171,7 +32176,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -38359,7 +38364,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
fclose( pFile );
pGold = Gia_AigerRead( pFileName, 0, 0 );
pGold = Gia_AigerRead( pFileName, 0, 0, 0 );
if ( pGold == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9FFTest(): Cannot read file \"%s\" with golden model.\n", pFileName );
@ -39689,7 +39694,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );

2
src/base/abci/abcTim.c
View File

@ -566,7 +566,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
Gia_ManReverseClasses( pGia, 1 );
// read file
pGia2 = Gia_AigerRead( pFileName, 1, 1 );
pGia2 = Gia_AigerRead( pFileName, 0, 1, 1 );
// normalize choices
if ( Gia_ManHasChoices(pGia2) )

2
src/base/cmd/cmdPlugin.c
View File

@ -391,7 +391,7 @@ Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken )
fclose( pFile );
}
// derive AIG
pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 );
pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0, 0 );
}
Vec_StrFree( vStr );
return pGia;

2
src/base/wlc/wlc.h
View File

@ -252,7 +252,7 @@ extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
/*=== wlcBlast.c ========================================================*/
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple );
/*=== wlcCom.c ========================================================*/
extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
/*=== wlcNtk.c ========================================================*/

7
src/base/wlc/wlcBlast.c
View File

@ -716,7 +716,7 @@ void Wlc_BlastSquare( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
SeeAlso []
***********************************************************************/
Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple )
{
int fVerbose = 0;
int fUseOldMultiplierBlasting = 0;
@ -740,7 +740,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
// create AIG manager
pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
pNew->fGiaSimple = fGiaSimple;
if ( !fGiaSimple )
Gia_ManHashAlloc( pNew );
// prepare for AIG with boxes
if ( vBoxIds )
{
@ -770,6 +772,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
// create AIG manager for logic of the boxes
pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
Gia_ManHashAlloc( pExtra );
assert( !fGiaSimple );
}
// blast in the topological order
Wlc_NtkForEachObj( p, pObj, i )

12
src/base/wlc/wlcCom.c
View File

@ -328,12 +328,15 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
Vec_Int_t * vBoxIds = NULL;
Gia_Man_t * pNew = NULL;
int c, fMulti = 0, fVerbose = 0;
int c, fGiaSimple = 0, fMulti = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cmvh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fGiaSimple ^= 1;
break;
case 'm':
fMulti ^= 1;
break;
@ -358,7 +361,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Warning: There is no multipliers in the design.\n" );
}
// transform
pNew = Wlc_NtkBitBlast( pNtk, vBoxIds );
pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, fGiaSimple );
Vec_IntFreeP( &vBoxIds );
if ( pNew == NULL )
{
@ -368,8 +371,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
Abc_Print( -2, "usage: %%blast [-mvh]\n" );
Abc_Print( -2, "usage: %%blast [-cmvh]\n" );
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
Abc_Print( -2, "\t-c : toggle using AIG w/o const propagation and strashing [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

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

@ -1287,7 +1287,7 @@ void Io_ReadWordTest( char * pFileName )
return;
Wlc_WriteVer( pNtk, "test.v", 0, 0 );
pNew = Wlc_NtkBitBlast( pNtk, NULL );
pNew = Wlc_NtkBitBlast( pNtk, NULL, 0 );
Gia_AigerWrite( pNew, "test.aig", 0, 0 );
Gia_ManStop( pNew );

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

@ -129,7 +129,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
{
Gia_Obj_t * pObj;
Vec_Ptr_t * vOne, * vRes;
Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL );
Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, 0 );
Wlc_Obj_t * pWlcObj;
int f, i, k, w, nBits, Counter = 0;
// allocate simulation info for one timeframe

4
src/sat/bmc/bmcEco.c
View File

@ -283,8 +283,8 @@ void Bmc_EcoMiterTest()
}
fclose( pFile );
// read files
pGold = Gia_AigerRead( pFileGold, 0, 0 );
pOld = Gia_AigerRead( pFileOld, 0, 0 );
pGold = Gia_AigerRead( pFileGold, 0, 0, 0 );
pOld = Gia_AigerRead( pFileOld, 0, 0, 0 );
// create ECO miter
vFans = Vec_IntAlloc( Gia_ManCiNum(pOld) );
Gia_ManForEachCi( pOld, pObj, i )