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 'origin/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2023-06-06 11:55:17 +02:00
parent 2c1c83f75b a5a6254db1
commit 0b361354b3
95 changed files with 8769 additions and 350 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/build-posix-cmake.yml vendored
View File

@ -5,7 +5,7 @@ jobs:
build-posix:
strategy:
matrix:
os: [macos-latest, ubuntu-latest]
os: [macos-11, ubuntu-latest]
use_namespace: [false, true]
runs-on: ${{ matrix.os }}

1
.gitignore vendored
View File

@ -11,6 +11,7 @@ lib/abc*
lib/m114*
lib/bip*
docs/
.vscode/
src/ext*
src/xxx/

24
abclib.dsp
View File

@ -675,6 +675,10 @@ SOURCE=.\src\base\io\ioWriteDot.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteEdgelist.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioWriteEqn.c
# End Source File
# Begin Source File
@ -5107,6 +5111,14 @@ SOURCE=.\src\aig\gia\giaMuxes.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaNewBdd.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaNewTt.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaNf.c
# End Source File
# Begin Source File
@ -5303,6 +5315,18 @@ SOURCE=.\src\aig\gia\giaTtopt.cpp
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaTransduction.cpp
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaTransduction.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaTranStoch.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaUnate.c
# End Source File
# Begin Source File

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

@ -225,7 +225,7 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1U << (ObjId & 31)); }
static inline int Aig_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);

4
src/aig/aig/aigShow.c
View File

@ -340,7 +340,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
***********************************************************************/
void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
{
extern void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
char FileNameDot[200];
FILE * pFile;
// create the file name
@ -355,7 +355,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
// generate the file
Aig_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}

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

@ -1105,10 +1105,12 @@ static inline Gia_Obj_t * Gia_ObjFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int i
static inline void Gia_ObjSetFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int i, Gia_Obj_t * pFan ) { Vec_IntWriteEntry( p->vFanout, Gia_ObjFoffset(p, pObj) + i, Gia_ObjId(p, pFan) ); }
static inline void Gia_ObjSetFanoutInt( Gia_Man_t * p, Gia_Obj_t * pObj, int i, int x ) { Vec_IntWriteEntry( p->vFanout, Gia_ObjFoffset(p, pObj) + i, x ); }
#define Gia_ObjForEachFanoutStatic( p, pObj, pFanout, i ) \
for ( i = 0; (i < Gia_ObjFanoutNum(p, pObj)) && (((pFanout) = Gia_ObjFanout(p, pObj, i)), 1); i++ )
#define Gia_ObjForEachFanoutStaticId( p, Id, FanId, i ) \
for ( i = 0; (i < Gia_ObjFanoutNumId(p, Id)) && (((FanId) = Gia_ObjFanoutId(p, Id, i)), 1); i++ )
#define Gia_ObjForEachFanoutStatic( p, pObj, pFanout, i ) \
for ( i = 0; (i < Gia_ObjFanoutNum(p, pObj)) && (((pFanout) = Gia_ObjFanout(p, pObj, i)), 1); i++ )
#define Gia_ObjForEachFanoutStaticId( p, Id, FanId, i ) \
for ( i = 0; (i < Gia_ObjFanoutNumId(p, Id)) && ((FanId = Gia_ObjFanoutId(p, Id, i)), 1); i++ )
#define Gia_ObjForEachFanoutStaticIndex( p, Id, FanId, i, Index ) \
for ( i = 0; (i < Gia_ObjFanoutNumId(p, Id)) && (Index = Vec_IntEntry(p->vFanout, Id)+i) && ((FanId = Vec_IntEntry(p->vFanout, Index)), 1); i++ )
static inline int Gia_ManHasMapping( Gia_Man_t * p ) { return p->vMapping != NULL; }
static inline int Gia_ObjIsLut( Gia_Man_t * p, int Id ) { return Vec_IntEntry(p->vMapping, Id) != 0; }
@ -1141,6 +1143,8 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsLut(p, i) ) {} else
#define Gia_LutForEachFanin( p, i, iFan, k ) \
for ( k = 0; k < Gia_ObjLutSize(p,i) && ((iFan = Gia_ObjLutFanins(p,i)[k]),1); k++ )
#define Gia_LutForEachFaninIndex( p, i, iFan, k, Index ) \
for ( k = 0; k < Gia_ObjLutSize(p,i) && (Index = Vec_IntEntry(p->vMapping, i)+1+k) && ((iFan = Vec_IntEntry(p->vMapping, Index)),1); k++ )
#define Gia_LutForEachFaninObj( p, i, pFanin, k ) \
for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ )
@ -1234,6 +1238,8 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObj) = Gia_ManCo(p, Gia_ManPoNum(p)+i)); i++ )
#define Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) \
for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObjRi) = Gia_ManCo(p, Gia_ManPoNum(p)+i)) && ((pObjRo) = Gia_ManCi(p, Gia_ManPiNum(p)+i)); i++ )
#define Gia_ManForEachRoToRiVec( vRoIds, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vRoIds)) && ((pObj) = Gia_ObjRoToRi(p, Gia_ManObj(p, Vec_IntEntry(vRoIds, i)))); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@ -1379,6 +1385,7 @@ extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p );
extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
extern int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 );
extern void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla );
/*=== giaEdge.c ==========================================================*/
extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray );
extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p );
@ -1436,7 +1443,7 @@ extern void Gia_ManFanoutStart( Gia_Man_t * p );
extern void Gia_ManFanoutStop( Gia_Man_t * p );
extern void Gia_ManStaticFanoutStart( Gia_Man_t * p );
extern void Gia_ManStaticFanoutStop( Gia_Man_t * p );
extern void Gia_ManStaticMappingFanoutStart( Gia_Man_t * p );
extern void Gia_ManStaticMappingFanoutStart( Gia_Man_t * p, Vec_Int_t ** pvIndex );
/*=== giaForce.c =========================================================*/
extern void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose );
/*=== giaFrames.c =========================================================*/
@ -1609,6 +1616,7 @@ extern Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes );
extern Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes );
extern void Gia_ManPtrWrdDumpBin( char * pFileName, Vec_Ptr_t * p, int fVerbose );
extern Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose );
extern Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p );
/*=== giaSpeedup.c ============================================================*/
extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
@ -1761,10 +1769,14 @@ extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
extern Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose );
/*=== giaTtopt.c ===========================================================*/
/*=== giaTtopt.cpp ===========================================================*/
extern Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds );
extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity );
/*=== giaTransduction.cpp ===========================================================*/
extern Gia_Man_t * Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose );
extern Gia_Man_t * Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );

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

@ -5407,6 +5407,138 @@ Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates with the care set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupWithCare( Gia_Man_t * p, Gia_Man_t * pCare )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iCare = -1;
assert( Gia_ManCiNum(pCare) == Gia_ManCiNum(p) );
assert( Gia_ManCoNum(pCare) == 1 );
assert( Gia_ManRegNum(p) == 0 );
assert( Gia_ManRegNum(pCare) == 0 );
pNew = Gia_ManStart( 2*Gia_ManObjNum(p) + Gia_ManObjNum(pCare) );
pNew->pName = Abc_UtilStrsavTwo( pNew->pName ? pNew->pName : (char *)"test", (char *)"_care" );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(pCare)->Value = 0;
Gia_ManForEachCi( pCare, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( pCare, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( pCare, pObj, i )
iCare = Gia_ObjFanin0Copy(pObj);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManCi(pCare, i)->Value;
Gia_ManForEachAnd( p, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, iCare, pObj->Value );
}
Gia_ManForEachCo( p, pObj, i )
{
pObj->Value = Gia_ObjFanin0Copy(pObj);
pObj->Value = Gia_ManHashAnd( pNew, iCare, pObj->Value );
Gia_ManAppendCo( pNew, pObj->Value );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla )
{
extern void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vLevels, Vec_Int_t * vRes, int fSigned, int fCla );
int i, k, x, fCompl, iLit; char pNameP[32], pNameT[32];
Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB );
Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB );
Vec_Int_t * vRes = Vec_IntAlloc( nArgA + nArgB );
Vec_Int_t * vArgA = Vec_IntAlloc( nArgA );
Vec_Int_t * vArgB = Vec_IntAlloc( nArgB ), * vLevel;
Gia_Man_t * pProd = Gia_ManStart( 1000 );
Gia_Man_t * pTree = Gia_ManStart( 1000 ), * pTemp;
Gia_ManHashAlloc( pTree );
pProd->pName = Abc_UtilStrsav( "prod" );
pTree->pName = Abc_UtilStrsav( "tree" );
for ( x = 0; x < nArgA; x++ )
Vec_IntPush( vArgA, Gia_ManAppendCi(pProd) );
for ( x = 0; x < nArgB; x++ )
Vec_IntPush( vArgB, Gia_ManAppendCi(pProd) );
for ( x = 0; x < nArgA + nArgB; x++ )
{
for ( i = 0; i < nArgA; i++ )
for ( k = 0; k < nArgB; k++ )
{
if ( i + k != x )
continue;
fCompl = fSigned && ((i == nArgA-1) ^ (k == nArgB-1));
iLit = Abc_LitNotCond(Gia_ManAppendAnd(pProd, Vec_IntEntry(vArgA, i), Vec_IntEntry(vArgB, k)), fCompl);
Gia_ManAppendCo( pProd, iLit );
Vec_WecPush( vProds, i+k, Gia_ManAppendCi(pTree) );
Vec_WecPush( vLevels, i+k, 0 );
}
}
if ( fSigned )
{
Vec_WecPush( vProds, nArgA, 1 );
Vec_WecPush( vLevels, nArgA, 0 );
Vec_WecPush( vProds, nArgA+nArgB-1, 1 );
Vec_WecPush( vLevels, nArgA+nArgB-1, 0 );
}
if ( Seed )
{
Abc_Random( 1 );
for ( x = 0; x < Seed; x++ )
Abc_Random( 0 );
Vec_WecForEachLevel( vProds, vLevel, x )
if ( Vec_IntSize(vLevel) > 1 )
Vec_IntRandomizeOrder( vLevel );
}
Wlc_BlastReduceMatrix( pTree, vProds, vLevels, vRes, fSigned, fCla );
Vec_IntShrink( vRes, nArgA + nArgB );
assert( Vec_IntSize(vRes) == nArgA + nArgB );
Vec_IntForEachEntry( vRes, iLit, x )
Gia_ManAppendCo( pTree, iLit );
pTree = Gia_ManCleanup( pTemp = pTree );
Gia_ManStop( pTemp );
sprintf( pNameP, "prod%d%d.aig", nArgA, nArgB );
sprintf( pNameT, "tree%d%d.aig", nArgA, nArgB );
Gia_AigerWrite( pProd, pNameP, 0, 0, 0 );
Gia_AigerWrite( pTree, pNameT, 0, 0, 0 );
Gia_ManStop( pProd );
Gia_ManStop( pTree );
printf( "Dumped files \"%s\" and \"%s\".\n", pNameP, pNameT );
Vec_WecFree( vProds );
Vec_WecFree( vLevels );
Vec_IntFree( vArgA );
Vec_IntFree( vArgB );
Vec_IntFree( vRes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -528,7 +528,7 @@ int Gia_ManChoiceMinLevel_rec( Gia_Man_t * p, int iPivot, int fDiveIn, Vec_Int_t
{
int Level0, Level1, LevelMax;
Gia_Obj_t * pPivot = Gia_ManObj( p, iPivot );
if ( Gia_ObjIsCi(pPivot) )
if ( Gia_ObjIsCi(pPivot) || iPivot == 0 )
return 0;
if ( Gia_ObjLevel(p, pPivot) )
return Gia_ObjLevel(p, pPivot);

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

@ -324,12 +324,20 @@ Vec_Int_t * Gia_ManStartMappingFanoutMap( Gia_Man_t * p, Vec_Int_t * vFanoutNums
SeeAlso []
***********************************************************************/
void Gia_ManStaticMappingFanoutStart( Gia_Man_t * p )
void Gia_ObjCheckDupMappingFanins( Gia_Man_t * p, int iObj )
{
int * pFanins = Gia_ObjLutFanins( p, iObj );
int i, k, nFanins = Gia_ObjLutSize( p, iObj );
for ( i = 0; i < nFanins; i++ )
for ( k = i + 1; k < nFanins; k++ )
assert( pFanins[i] != pFanins[k] );
}
void Gia_ManStaticMappingFanoutStart( Gia_Man_t * p, Vec_Int_t ** pvIndex )
{
Vec_Int_t * vCounts;
int * pRefsOld;
Gia_Obj_t * pObj, * pFanin;
int i, k, iFan, iFanout;
int i, k, iFan, iFanout, Index;
assert( p->vFanoutNums == NULL );
assert( p->vFanout == NULL );
// recompute reference counters
@ -339,17 +347,22 @@ void Gia_ManStaticMappingFanoutStart( Gia_Man_t * p )
p->pLutRefs = pRefsOld;
// start the fanout maps
p->vFanout = Gia_ManStartMappingFanoutMap( p, p->vFanoutNums );
if ( pvIndex )
*pvIndex = Vec_IntStart( Vec_IntSize(p->vFanout) );
// incrementally add fanouts
vCounts = Vec_IntStart( Gia_ManObjNum(p) );
Gia_ManForEachLut( p, i )
{
Gia_ObjCheckDupMappingFanins( p, i );
pObj = Gia_ManObj( p, i );
Gia_LutForEachFanin( p, i, iFan, k )
Gia_LutForEachFaninIndex( p, i, iFan, k, Index )
{
pFanin = Gia_ManObj( p, iFan );
iFanout = Vec_IntEntry( vCounts, iFan );
Gia_ObjSetFanout( p, pFanin, iFanout, pObj );
Vec_IntAddToEntry( vCounts, iFan, 1 );
if ( pvIndex )
Vec_IntWriteEntry( *pvIndex, Vec_IntEntry(p->vFanout, iFan) + iFanout, Index );
}
}
Gia_ManForEachCo( p, pObj, i )

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

@ -558,11 +558,12 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
FILE * pTable = fopen( pDumpFile, "a+" );
if ( strcmp( FileNameOld, p->pName ) )
{
sprintf( FileNameOld, "%s", p->pName );
sprintf( FileNameOld, "%s_out", p->pName );
fprintf( pTable, "\n" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, " " );
fprintf( pTable, "%d ", Gia_ManAndNum(p) );
//fprintf( pTable, "%d ", Gia_ManAndNum(p) );
fprintf( pTable, "%d ", Gia_ManRegNum(p) );
fprintf( pTable, "%d ", nLuts );
fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) );
//fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) );
@ -575,11 +576,13 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
//printf( "This part of the code is currently not used.\n" );
//assert( 0 );
fprintf( pTable, " " );
fprintf( pTable, " " );
fprintf( pTable, "%d ", Gia_ManRegNum(p) );
fprintf( pTable, "%d ", nLuts );
fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) );
//fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) );
//fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) );
fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC );
// fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC );
clk = Abc_Clock();
}
fclose( pTable );

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

@ -1789,7 +1789,7 @@ void Mf_ManOptimization( Mf_Man_t * p )
Gia_Man_t * pGia = p->pGia0;
int i, Count, nNodes = Mf_ManMappingFromMapping( p );
Gia_ManLevelNum( pGia );
Gia_ManStaticMappingFanoutStart( pGia );
Gia_ManStaticMappingFanoutStart( pGia, NULL );
Mf_ManPrintFanoutProfile( p, pGia->vFanoutNums );
printf( "\nIndividual logic cones for mapping with %d nodes:\n", nNodes );
Vec_IntForEachEntry( pGia->vFanoutNums, Count, i )

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

@ -67,7 +67,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
int nBoxes = Gia_ManBoxNum(p), nVars;
int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
int i, j, k, curCi, curCo, nBoxIns, nBoxOuts;
int i, j, k, curCi, curCo, nBoxIns, nBoxOuts, w, nWords;
int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0;
int nLutSizeMax = Gia_ManLutSizeMax( p );
nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 );
@ -113,15 +113,11 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) );
Vec_IntShrink( vArray, nVars );
if ( nVars <= 6 )
Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
else
{
int w, nWords = Abc_Truth6WordNum( nVars );
Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
for ( w = 0; w < nWords; w++ )
Vec_WrdPush( vTruths2, pTruth[w] );
}
Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
nWords = Abc_Truth6WordNum( nVars );
Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
for ( w = 0; w < nWords; w++ )
Vec_WrdPush( vTruths2, pTruth[w] );
if ( Gia_ObjLutIsMux(p, Id) )
{
Vec_StrWriteEntry( vFixed, Counter, (char)1 );
@ -143,6 +139,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
Vec_StrWriteEntry( vEmpty, Counter, (char)1 );
uTruth = Gia_ObjFaninC0(pObj) ? ~uTruths6[0]: uTruths6[0];
Vec_WrdWriteEntry( vTruths, Counter, uTruth );
Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
Vec_WrdPush( vTruths2, uTruth );
}
Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ );
}

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

@ -769,6 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap )
{
if ( iObjLit == -1 )
continue;
// if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) )
// continue;
iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) );
iReprMini = Vec_IntEntry( vGia2Mini, iReprGia );
if ( iReprMini == -1 )

839
src/aig/gia/giaNewBdd.h Normal file
View File

@ -0,0 +1,839 @@
/**CFile****************************************************************
FileName [giaNewBdd.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Implementation of transduction method.]
Author [Yukio Miyasaka]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 2023.]
Revision [$Id: giaNewBdd.h,v 1.00 2023/05/10 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__aig__gia__giaNewBdd_h
#define ABC__aig__gia__giaNewBdd_h
#include <limits>
#include <vector>
#include <iostream>
#include <iomanip>
#include <cmath>
ABC_NAMESPACE_CXX_HEADER_START
namespace NewBdd {
typedef unsigned short var;
typedef int bvar;
typedef unsigned lit;
typedef unsigned short ref;
typedef unsigned long long size;
typedef unsigned edge;
typedef unsigned uniq;
typedef unsigned cac;
static inline var VarMax() { return std::numeric_limits<var>::max(); }
static inline bvar BvarMax() { return std::numeric_limits<bvar>::max(); }
static inline lit LitMax() { return std::numeric_limits<lit>::max(); }
static inline ref RefMax() { return std::numeric_limits<ref>::max(); }
static inline size SizeMax() { return std::numeric_limits<size>::max(); }
static inline uniq UniqHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; }
static inline cac CacHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; }
class Cache {
private:
cac nSize;
cac nMax;
cac Mask;
size nLookups;
size nHits;
size nThold;
double HitRate;
int nVerbose;
std::vector<lit> vCache;
public:
Cache(int nCacheSizeLog, int nCacheMaxLog, int nVerbose): nVerbose(nVerbose) {
if(nCacheMaxLog < nCacheSizeLog)
throw std::invalid_argument("nCacheMax must not be smaller than nCacheSize");
nMax = (cac)1 << nCacheMaxLog;
if(!(nMax << 1))
throw std::length_error("Memout (nCacheMax) in init");
nSize = (cac)1 << nCacheSizeLog;
if(nVerbose)
std::cout << "Allocating " << nSize << " cache entries" << std::endl;
vCache.resize(nSize * 3);
Mask = nSize - 1;
nLookups = 0;
nHits = 0;
nThold = (nSize == nMax)? SizeMax(): nSize;
HitRate = 1;
}
~Cache() {
if(nVerbose)
std::cout << "Free " << nSize << " cache entries" << std::endl;
}
inline lit Lookup(lit x, lit y) {
nLookups++;
if(nLookups > nThold) {
double NewHitRate = (double)nHits / nLookups;
if(nVerbose >= 2)
std::cout << "Cache Hits: " << std::setw(10) << nHits << ", "
<< "Lookups: " << std::setw(10) << nLookups << ", "
<< "Rate: " << std::setw(10) << NewHitRate
<< std::endl;
if(NewHitRate > HitRate)
Resize();
if(nSize == nMax)
nThold = SizeMax();
else {
nThold <<= 1;
if(!nThold)
nThold = SizeMax();
}
HitRate = NewHitRate;
}
cac i = (CacHash(x, y) & Mask) * 3;
if(vCache[i] == x && vCache[i + 1] == y) {
if(nVerbose >= 3)
std::cout << "Cache hit: "
<< "x = " << std::setw(10) << x << ", "
<< "y = " << std::setw(10) << y << ", "
<< "z = " << std::setw(10) << vCache[i + 2] << ", "
<< "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
<< std::endl;
nHits++;
return vCache[i + 2];
}
return LitMax();
}
inline void Insert(lit x, lit y, lit z) {
cac i = (CacHash(x, y) & Mask) * 3;
vCache[i] = x;
vCache[i + 1] = y;
vCache[i + 2] = z;
if(nVerbose >= 3)
std::cout << "Cache ent: "
<< "x = " << std::setw(10) << x << ", "
<< "y = " << std::setw(10) << y << ", "
<< "z = " << std::setw(10) << z << ", "
<< "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
<< std::endl;
}
inline void Clear() {
std::fill(vCache.begin(), vCache.end(), 0);
}
void Resize() {
cac nSizeOld = nSize;
nSize <<= 1;
if(nVerbose >= 2)
std::cout << "Reallocating " << nSize << " cache entries" << std::endl;
vCache.resize(nSize * 3);
Mask = nSize - 1;
for(cac j = 0; j < nSizeOld; j++) {
cac i = j * 3;
if(vCache[i] || vCache[i + 1]) {
cac hash = (CacHash(vCache[i], vCache[i + 1]) & Mask) * 3;
vCache[hash] = vCache[i];
vCache[hash + 1] = vCache[i + 1];
vCache[hash + 2] = vCache[i + 2];
if(nVerbose >= 3)
std::cout << "Cache mov: "
<< "x = " << std::setw(10) << vCache[i] << ", "
<< "y = " << std::setw(10) << vCache[i + 1] << ", "
<< "z = " << std::setw(10) << vCache[i + 2] << ", "
<< "hash = " << std::hex << (CacHash(vCache[i], vCache[i + 1]) & Mask) << std::dec
<< std::endl;
}
}
}
};
struct Param {
int nObjsAllocLog;
int nObjsMaxLog;
int nUniqueSizeLog;
double UniqueDensity;
int nCacheSizeLog;
int nCacheMaxLog;
int nCacheVerbose;
bool fCountOnes;
int nGbc;
bvar nReo;
double MaxGrowth;
bool fReoVerbose;
int nVerbose;
std::vector<var> *pVar2Level;
Param() {
nObjsAllocLog = 20;
nObjsMaxLog = 25;
nUniqueSizeLog = 10;
UniqueDensity = 4;
nCacheSizeLog = 15;
nCacheMaxLog = 20;
nCacheVerbose = 0;
fCountOnes = false;
nGbc = 0;
nReo = BvarMax();
MaxGrowth = 1.2;
fReoVerbose = false;
nVerbose = 0;
pVar2Level = NULL;
}
};
class Man {
private:
var nVars;
bvar nObjs;
bvar nObjsAlloc;
bvar nObjsMax;
bvar RemovedHead;
int nGbc;
bvar nReo;
double MaxGrowth;
bool fReoVerbose;
int nVerbose;
std::vector<var> vVars;
std::vector<var> Var2Level;
std::vector<var> Level2Var;
std::vector<lit> vObjs;
std::vector<bvar> vNexts;
std::vector<bool> vMarks;
std::vector<ref> vRefs;
std::vector<edge> vEdges;
std::vector<double> vOneCounts;
std::vector<uniq> vUniqueMasks;
std::vector<bvar> vUniqueCounts;
std::vector<bvar> vUniqueTholds;
std::vector<std::vector<bvar> > vvUnique;
Cache *cache;
public:
inline lit Bvar2Lit(bvar a) const { return (lit)a << 1; }
inline lit Bvar2Lit(bvar a, bool c) const { return ((lit)a << 1) ^ (lit)c; }
inline bvar Lit2Bvar(lit x) const { return (bvar)(x >> 1); }
inline var VarOfBvar(bvar a) const { return vVars[a]; }
inline lit ThenOfBvar(bvar a) const { return vObjs[Bvar2Lit(a)]; }
inline lit ElseOfBvar(bvar a) const { return vObjs[Bvar2Lit(a, true)]; }
inline ref RefOfBvar(bvar a) const { return vRefs[a]; }
inline lit Const0() const { return (lit)0; }
inline lit Const1() const { return (lit)1; }
inline bool IsConst0(lit x) const { return x == Const0(); }
inline bool IsConst1(lit x) const { return x == Const1(); }
inline lit IthVar(var v) const { return Bvar2Lit((bvar)v + 1); }
inline lit LitRegular(lit x) const { return x & ~(lit)1; }
inline lit LitIrregular(lit x) const { return x | (lit)1; }
inline lit LitNot(lit x) const { return x ^ (lit)1; }
inline lit LitNotCond(lit x, bool c) const { return x ^ (lit)c; }
inline bool LitIsCompl(lit x) const { return x & (lit)1; }
inline bool LitIsEq(lit x, lit y) const { return x == y; }
inline var Var(lit x) const { return vVars[Lit2Bvar(x)]; }
inline var Level(lit x) const { return Var2Level[Var(x)]; }
inline lit Then(lit x) const { return LitNotCond(vObjs[LitRegular(x)], LitIsCompl(x)); }
inline lit Else(lit x) const { return LitNotCond(vObjs[LitIrregular(x)], LitIsCompl(x)); }
inline ref Ref(lit x) const { return vRefs[Lit2Bvar(x)]; }
inline double OneCount(lit x) const {
if(vOneCounts.empty())
throw std::logic_error("fCountOnes was not set");
if(LitIsCompl(x))
return std::pow(2.0, nVars) - vOneCounts[Lit2Bvar(x)];
return vOneCounts[Lit2Bvar(x)];
}
public:
inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }
inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }
private:
inline bool Mark(lit x) const { return vMarks[Lit2Bvar(x)]; }
inline edge Edge(lit x) const { return vEdges[Lit2Bvar(x)]; }
inline void SetMark(lit x) { vMarks[Lit2Bvar(x)] = true; }
inline void ResetMark(lit x) { vMarks[Lit2Bvar(x)] = false; }
inline void IncEdge(lit x) { vEdges[Lit2Bvar(x)]++; }
inline void DecEdge(lit x) { vEdges[Lit2Bvar(x)]--; }
inline bool MarkOfBvar(bvar a) const { return vMarks[a]; }
inline edge EdgeOfBvar(bvar a) const { return vEdges[a]; }
inline void SetVarOfBvar(bvar a, var v) { vVars[a] = v; }
inline void SetThenOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a)] = x; }
inline void SetElseOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a, true)] = x; }
inline void SetMarkOfBvar(bvar a) { vMarks[a] = true; }
inline void ResetMarkOfBvar(bvar a) { vMarks[a] = false; }
inline void RemoveBvar(bvar a) {
var v = VarOfBvar(a);
SetVarOfBvar(a, VarMax());
std::vector<bvar>::iterator q = vvUnique[v].begin() + (UniqHash(ThenOfBvar(a), ElseOfBvar(a)) & vUniqueMasks[v]);
for(; *q; q = vNexts.begin() + *q)
if(*q == a)
break;
bvar next = vNexts[*q];
vNexts[*q] = RemovedHead;
RemovedHead = *q;
*q = next;
vUniqueCounts[v]--;
}
private:
void SetMark_rec(lit x) {
if(x < 2 || Mark(x))
return;
SetMark(x);
SetMark_rec(Then(x));
SetMark_rec(Else(x));
}
void ResetMark_rec(lit x) {
if(x < 2 || !Mark(x))
return;
ResetMark(x);
ResetMark_rec(Then(x));
ResetMark_rec(Else(x));
}
bvar CountNodes_rec(lit x) {
if(x < 2 || Mark(x))
return 0;
SetMark(x);
return 1 + CountNodes_rec(Then(x)) + CountNodes_rec(Else(x));
}
void CountEdges_rec(lit x) {
if(x < 2)
return;
IncEdge(x);
if(Mark(x))
return;
SetMark(x);
CountEdges_rec(Then(x));
CountEdges_rec(Else(x));
}
void CountEdges() {
vEdges.resize(nObjsAlloc);
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
CountEdges_rec(Bvar2Lit(a));
for(bvar a = 1; a <= (bvar)nVars; a++)
vEdges[a]++;
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
ResetMark_rec(Bvar2Lit(a));
}
public:
bool Resize() {
if(nObjsAlloc == nObjsMax)
return false;
lit nObjsAllocLit = (lit)nObjsAlloc << 1;
if(nObjsAllocLit > (lit)BvarMax())
nObjsAlloc = BvarMax();
else
nObjsAlloc = (bvar)nObjsAllocLit;
if(nVerbose >= 2)
std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl;
vVars.resize(nObjsAlloc);
vObjs.resize((lit)nObjsAlloc * 2);
vNexts.resize(nObjsAlloc);
vMarks.resize(nObjsAlloc);
if(!vRefs.empty())
vRefs.resize(nObjsAlloc);
if(!vEdges.empty())
vEdges.resize(nObjsAlloc);
if(!vOneCounts.empty())
vOneCounts.resize(nObjsAlloc);
return true;
}
void ResizeUnique(var v) {
uniq nUniqueSize, nUniqueSizeOld;
nUniqueSize = nUniqueSizeOld = vvUnique[v].size();
nUniqueSize <<= 1;
if(!nUniqueSize) {
vUniqueTholds[v] = BvarMax();
return;
}
if(nVerbose >= 2)
std::cout << "Reallocating " << nUniqueSize << " unique table entries for Var " << v << std::endl;
vvUnique[v].resize(nUniqueSize);
vUniqueMasks[v] = nUniqueSize - 1;
for(uniq i = 0; i < nUniqueSizeOld; i++) {
std::vector<bvar>::iterator q, tail, tail1, tail2;
q = tail1 = vvUnique[v].begin() + i;
tail2 = q + nUniqueSizeOld;
while(*q) {
uniq hash = UniqHash(ThenOfBvar(*q), ElseOfBvar(*q)) & vUniqueMasks[v];
if(hash == i)
tail = tail1;
else
tail = tail2;
if(tail != q)
*tail = *q, *q = 0;
q = vNexts.begin() + *tail;
if(tail == tail1)
tail1 = q;
else
tail2 = q;
}
}
vUniqueTholds[v] <<= 1;
if((lit)vUniqueTholds[v] > (lit)BvarMax())
vUniqueTholds[v] = BvarMax();
}
bool Gbc() {
if(nVerbose >= 2)
std::cout << "Garbage collect" << std::endl;
if(!vEdges.empty()) {
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(!EdgeOfBvar(a) && VarOfBvar(a) != VarMax())
RemoveBvar(a);
} else {
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
SetMark_rec(Bvar2Lit(a));
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(!MarkOfBvar(a) && VarOfBvar(a) != VarMax())
RemoveBvar(a);
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
ResetMark_rec(Bvar2Lit(a));
}
cache->Clear();
return RemovedHead;
}
private:
inline lit UniqueCreateInt(var v, lit x1, lit x0) {
std::vector<bvar>::iterator p, q;
p = q = vvUnique[v].begin() + (UniqHash(x1, x0) & vUniqueMasks[v]);
for(; *q; q = vNexts.begin() + *q)
if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0)
return Bvar2Lit(*q);
bvar next = *p;
if(nObjs < nObjsAlloc)
*p = nObjs++;
else if(RemovedHead)
*p = RemovedHead, RemovedHead = vNexts[*p];
else
return LitMax();
SetVarOfBvar(*p, v);
SetThenOfBvar(*p, x1);
SetElseOfBvar(*p, x0);
vNexts[*p] = next;
if(!vOneCounts.empty())
vOneCounts[*p] = OneCount(x1) / 2 + OneCount(x0) / 2;
if(nVerbose >= 3) {
std::cout << "Create node " << std::setw(10) << *p << ": "
<< "Var = " << std::setw(6) << v << ", "
<< "Then = " << std::setw(10) << x1 << ", "
<< "Else = " << std::setw(10) << x0;
if(!vOneCounts.empty())
std::cout << ", Ones = " << std::setw(10) << vOneCounts[*q];
std::cout << std::endl;
}
vUniqueCounts[v]++;
if(vUniqueCounts[v] > vUniqueTholds[v]) {
bvar a = *p;
ResizeUnique(v);
return Bvar2Lit(a);
}
return Bvar2Lit(*p);
}
inline lit UniqueCreate(var v, lit x1, lit x0) {
if(x1 == x0)
return x1;
lit x;
while(true) {
if(!LitIsCompl(x0))
x = UniqueCreateInt(v, x1, x0);
else
x = UniqueCreateInt(v, LitNot(x1), LitNot(x0));
if(x == LitMax()) {
bool fRemoved = false;
if(nGbc > 1)
fRemoved = Gbc();
if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc()))
throw std::length_error("Memout (node)");
} else
break;
}
return LitIsCompl(x0)? LitNot(x): x;
}
lit And_rec(lit x, lit y) {
if(x == 0 || y == 1)
return x;
if(x == 1 || y == 0)
return y;
if(Lit2Bvar(x) == Lit2Bvar(y))
return (x == y)? x: 0;
if(x > y)
std::swap(x, y);
lit z = cache->Lookup(x, y);
if(z != LitMax())
return z;
var v;
lit x0, x1, y0, y1;
if(Level(x) < Level(y))
v = Var(x), x1 = Then(x), x0 = Else(x), y0 = y1 = y;
else if(Level(x) > Level(y))
v = Var(y), x0 = x1 = x, y1 = Then(y), y0 = Else(y);
else
v = Var(x), x1 = Then(x), x0 = Else(x), y1 = Then(y), y0 = Else(y);
lit z1 = And_rec(x1, y1);
IncRef(z1);
lit z0 = And_rec(x0, y0);
IncRef(z0);
z = UniqueCreate(v, z1, z0);
DecRef(z1);
DecRef(z0);
cache->Insert(x, y, z);
return z;
}
private:
bvar Swap(var i) {
var v1 = Level2Var[i];
var v2 = Level2Var[i + 1];
bvar f = 0;
bvar diff = 0;
for(std::vector<bvar>::iterator p = vvUnique[v1].begin(); p != vvUnique[v1].end(); p++) {
std::vector<bvar>::iterator q = p;
while(*q) {
if(!EdgeOfBvar(*q)) {
SetVarOfBvar(*q, VarMax());
bvar next = vNexts[*q];
vNexts[*q] = RemovedHead;
RemovedHead = *q;
*q = next;
vUniqueCounts[v1]--;
continue;
}
lit f1 = ThenOfBvar(*q);
lit f0 = ElseOfBvar(*q);
if(Var(f1) == v2 || Var(f0) == v2) {
DecEdge(f1);
if(Var(f1) == v2 && !Edge(f1))
DecEdge(Then(f1)), DecEdge(Else(f1)), diff--;
DecEdge(f0);
if(Var(f0) == v2 && !Edge(f0))
DecEdge(Then(f0)), DecEdge(Else(f0)), diff--;
bvar next = vNexts[*q];
vNexts[*q] = f;
f = *q;
*q = next;
vUniqueCounts[v1]--;
continue;
}
q = vNexts.begin() + *q;
}
}
while(f) {
lit f1 = ThenOfBvar(f);
lit f0 = ElseOfBvar(f);
lit f00, f01, f10, f11;
if(Var(f1) == v2)
f11 = Then(f1), f10 = Else(f1);
else
f10 = f11 = f1;
if(Var(f0) == v2)
f01 = Then(f0), f00 = Else(f0);
else
f00 = f01 = f0;
if(f11 == f01)
f1 = f11;
else {
f1 = UniqueCreate(v1, f11, f01);
if(!Edge(f1))
IncEdge(f11), IncEdge(f01), diff++;
}
IncEdge(f1);
IncRef(f1);
if(f10 == f00)
f0 = f10;
else {
f0 = UniqueCreate(v1, f10, f00);
if(!Edge(f0))
IncEdge(f10), IncEdge(f00), diff++;
}
IncEdge(f0);
DecRef(f1);
SetVarOfBvar(f, v2);
SetThenOfBvar(f, f1);
SetElseOfBvar(f, f0);
std::vector<bvar>::iterator q = vvUnique[v2].begin() + (UniqHash(f1, f0) & vUniqueMasks[v2]);
lit next = vNexts[f];
vNexts[f] = *q;
*q = f;
vUniqueCounts[v2]++;
f = next;
}
Var2Level[v1] = i + 1;
Var2Level[v2] = i;
Level2Var[i] = v2;
Level2Var[i + 1] = v1;
return diff;
}
void Sift() {
bvar count = CountNodes();
std::vector<var> sift_order(nVars);
for(var v = 0; v < nVars; v++)
sift_order[v] = v;
for(var i = 0; i < nVars; i++) {
var max_j = i;
for(var j = i + 1; j < nVars; j++)
if(vUniqueCounts[sift_order[j]] > vUniqueCounts[sift_order[max_j]])
max_j = j;
if(max_j != i)
std::swap(sift_order[max_j], sift_order[i]);
}
for(var v = 0; v < nVars; v++) {
bvar lev = Var2Level[sift_order[v]];
bool UpFirst = lev < (bvar)(nVars / 2);
bvar min_lev = lev;
bvar min_diff = 0;
bvar diff = 0;
bvar thold = count * (MaxGrowth - 1);
if(fReoVerbose)
std::cout << "Sift " << sift_order[v] << " : Level = " << lev << " Count = " << count << " Thold = " << thold << std::endl;
if(UpFirst) {
lev--;
for(; lev >= 0; lev--) {
diff += Swap(lev);
if(fReoVerbose)
std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
if(diff < min_diff)
min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
else if(diff > thold) {
lev--;
break;
}
}
lev++;
}
for(; lev < (bvar)nVars - 1; lev++) {
diff += Swap(lev);
if(fReoVerbose)
std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
if(diff <= min_diff)
min_lev = lev + 1, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
else if(diff > thold) {
lev++;
break;
}
}
lev--;
if(UpFirst) {
for(; lev >= min_lev; lev--) {
diff += Swap(lev);
if(fReoVerbose)
std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
}
} else {
for(; lev >= 0; lev--) {
diff += Swap(lev);
if(fReoVerbose)
std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
if(diff <= min_diff)
min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
else if(diff > thold) {
lev--;
break;
}
}
lev++;
for(; lev < min_lev; lev++) {
diff += Swap(lev);
if(fReoVerbose)
std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
}
}
count += min_diff;
if(fReoVerbose)
std::cout << "Sifted " << sift_order[v] << " : Level = " << min_lev << " Count = " << count << " Thold = " << thold << std::endl;
}
}
public:
Man(int nVars_, Param p) {
nVerbose = p.nVerbose;
// parameter sanity check
if(p.nObjsMaxLog < p.nObjsAllocLog)
throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc");
if(nVars_ >= (int)VarMax())
throw std::length_error("Memout (nVars) in init");
nVars = nVars_;
lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
if(!nObjsMaxLit)
throw std::length_error("Memout (nObjsMax) in init");
if(nObjsMaxLit > (lit)BvarMax())
nObjsMax = BvarMax();
else
nObjsMax = (bvar)nObjsMaxLit;
lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
if(!nObjsAllocLit)
throw std::length_error("Memout (nObjsAlloc) in init");
if(nObjsAllocLit > (lit)BvarMax())
nObjsAlloc = BvarMax();
else
nObjsAlloc = (bvar)nObjsAllocLit;
if(nObjsAlloc <= (bvar)nVars)
throw std::invalid_argument("nObjsAlloc must be larger than nVars");
uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog;
if(!nUniqueSize)
throw std::length_error("Memout (nUniqueSize) in init");
// allocation
if(nVerbose)
std::cout << "Allocating " << nObjsAlloc << " nodes and " << nVars << " x " << nUniqueSize << " unique table entries" << std::endl;
vVars.resize(nObjsAlloc);
vObjs.resize((lit)nObjsAlloc * 2);
vNexts.resize(nObjsAlloc);
vMarks.resize(nObjsAlloc);
vvUnique.resize(nVars);
vUniqueMasks.resize(nVars);
vUniqueCounts.resize(nVars);
vUniqueTholds.resize(nVars);
for(var v = 0; v < nVars; v++) {
vvUnique[v].resize(nUniqueSize);
vUniqueMasks[v] = nUniqueSize - 1;
if((lit)(nUniqueSize * p.UniqueDensity) > (lit)BvarMax())
vUniqueTholds[v] = BvarMax();
else
vUniqueTholds[v] = (bvar)(nUniqueSize * p.UniqueDensity);
}
if(p.fCountOnes) {
if(nVars > 1023)
throw std::length_error("nVars must be less than 1024 to count ones");
vOneCounts.resize(nObjsAlloc);
}
// set up cache
cache = new Cache(p.nCacheSizeLog, p.nCacheMaxLog, p.nCacheVerbose);
// create nodes for variables
nObjs = 1;
vVars[0] = VarMax();
for(var v = 0; v < nVars; v++)
UniqueCreateInt(v, 1, 0);
// set up variable order
Var2Level.resize(nVars);
Level2Var.resize(nVars);
for(var v = 0; v < nVars; v++) {
if(p.pVar2Level)
Var2Level[v] = (*p.pVar2Level)[v];
else
Var2Level[v] = v;
Level2Var[Var2Level[v]] = v;
}
// set other parameters
RemovedHead = 0;
nGbc = p.nGbc;
nReo = p.nReo;
MaxGrowth = p.MaxGrowth;
fReoVerbose = p.fReoVerbose;
if(nGbc || nReo != BvarMax())
vRefs.resize(nObjsAlloc);
}
~Man() {
if(nVerbose) {
std::cout << "Free " << nObjsAlloc << " nodes (" << nObjs << " live nodes)" << std::endl;
std::cout << "Free {";
std::string delim;
for(var v = 0; v < nVars; v++) {
std::cout << delim << vvUnique[v].size();
delim = ", ";
}
std::cout << "} unique table entries" << std::endl;
if(!vRefs.empty())
std::cout << "Free " << vRefs.size() << " refs" << std::endl;
}
delete cache;
}
void Reorder() {
if(nVerbose >= 2)
std::cout << "Reorder" << std::endl;
int nGbc_ = nGbc;
nGbc = 0;
CountEdges();
Sift();
vEdges.clear();
cache->Clear();
nGbc = nGbc_;
}
inline lit And(lit x, lit y) {
if(nObjs > nReo) {
Reorder();
while(nReo < nObjs) {
nReo <<= 1;
if((lit)nReo > (lit)BvarMax())
nReo = BvarMax();
}
}
return And_rec(x, y);
}
inline lit Or(lit x, lit y) {
return LitNot(And(LitNot(x), LitNot(y)));
}
public:
void SetRef(std::vector<lit> const &vLits) {
vRefs.clear();
vRefs.resize(nObjsAlloc);
for(size_t i = 0; i < vLits.size(); i++)
IncRef(vLits[i]);
}
void TurnOffReo() {
nReo = BvarMax();
if(!nGbc)
vRefs.clear();
}
bvar CountNodes() {
bvar count = 1;
if(!vEdges.empty()) {
for(bvar a = 1; a < nObjs; a++)
if(EdgeOfBvar(a))
count++;
return count;
}
for(bvar a = 1; a <= (bvar)nVars; a++) {
count++;
SetMarkOfBvar(a);
}
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
count += CountNodes_rec(Bvar2Lit(a));
for(bvar a = 1; a <= (bvar)nVars; a++)
ResetMarkOfBvar(a);
for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
if(RefOfBvar(a))
ResetMark_rec(Bvar2Lit(a));
return count;
}
bvar CountNodes(std::vector<lit> const &vLits) {
bvar count = 1;
for(size_t i = 0; i < vLits.size(); i++)
count += CountNodes_rec(vLits[i]);
for(size_t i = 0; i < vLits.size(); i++)
ResetMark_rec(vLits[i]);
return count;
}
void PrintStats() {
bvar nRemoved = 0;
bvar a = RemovedHead;
while(a)
a = vNexts[a], nRemoved++;
bvar nLive = 1;
for(var v = 0; v < nVars; v++)
nLive += vUniqueCounts[v];
std::cout << "ref: " << std::setw(10) << (vRefs.empty()? 0: CountNodes()) << ", "
<< "used: " << std::setw(10) << nObjs << ", "
<< "live: " << std::setw(10) << nLive << ", "
<< "dead: " << std::setw(10) << nRemoved << ", "
<< "alloc: " << std::setw(10) << nObjsAlloc
<< std::endl;
}
};
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

281
src/aig/gia/giaNewTt.h Normal file
View File

@ -0,0 +1,281 @@
/**CFile****************************************************************
FileName [giaNewTt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Implementation of transduction method.]
Author [Yukio Miyasaka]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 2023.]
Revision [$Id: giaNewTt.h,v 1.00 2023/05/10 00:00:00 Exp $]
***********************************************************************/
#ifndef ABC__aig__gia__giaNewTt_h
#define ABC__aig__gia__giaNewTt_h
#include <limits>
#include <iomanip>
#include <iostream>
#include <vector>
#include <bitset>
ABC_NAMESPACE_CXX_HEADER_START
namespace NewTt {
typedef int bvar;
typedef unsigned lit;
typedef unsigned short ref;
typedef unsigned long long size;
static inline bvar BvarMax() { return std::numeric_limits<bvar>::max(); }
static inline lit LitMax() { return std::numeric_limits<lit>::max(); }
static inline ref RefMax() { return std::numeric_limits<ref>::max(); }
static inline size SizeMax() { return std::numeric_limits<size>::max(); }
struct Param {
int nObjsAllocLog;
int nObjsMaxLog;
int nVerbose;
bool fCountOnes;
int nGbc;
int nReo; // dummy
Param() {
nObjsAllocLog = 15;
nObjsMaxLog = 20;
nVerbose = 0;
fCountOnes = false;
nGbc = 0;
nReo = BvarMax();
}
};
class Man {
private:
typedef unsigned long long word;
typedef std::bitset<64> bsw;
static inline int ww() { return 64; } // word width
static inline int lww() { return 6; } // log word width
static inline word one() {return 0xffffffffffffffffull; }
static inline word vars(int i) {
static const word vars[] = {0xaaaaaaaaaaaaaaaaull,
0xccccccccccccccccull,
0xf0f0f0f0f0f0f0f0ull,
0xff00ff00ff00ff00ull,
0xffff0000ffff0000ull,
0xffffffff00000000ull};
return vars[i];
}
static inline word ones(int i) {
static const word ones[] = {0x0000000000000001ull,
0x0000000000000003ull,
0x000000000000000full,
0x00000000000000ffull,
0x000000000000ffffull,
0x00000000ffffffffull,
0xffffffffffffffffull};
return ones[i];
}
private:
int nVars;
bvar nObjs;
bvar nObjsAlloc;
bvar nObjsMax;
size nSize;
size nTotalSize;
std::vector<word> vVals;
std::vector<bvar> vDeads;
std::vector<ref> vRefs;
int nGbc;
int nVerbose;
public:
inline lit Bvar2Lit(bvar a) const { return (lit)a << 1; }
inline bvar Lit2Bvar(lit x) const { return (bvar)(x >> 1); }
inline lit IthVar(int v) const { return ((lit)v + 1) << 1; }
inline lit LitNot(lit x) const { return x ^ (lit)1; }
inline lit LitNotCond(lit x, bool c) const { return x ^ (lit)c; }
inline bool LitIsCompl(lit x) const { return x & (lit)1; }
inline ref Ref(lit x) const { return vRefs[Lit2Bvar(x)]; }
inline lit Const0() const { return (lit)0; }
inline lit Const1() const { return (lit)1; }
inline bool IsConst0(lit x) const {
bvar a = Lit2Bvar(x);
word c = LitIsCompl(x)? one(): 0;
for(size j = 0; j < nSize; j++)
if(vVals[nSize * a + j] ^ c)
return false;
return true;
}
inline bool IsConst1(lit x) const {
bvar a = Lit2Bvar(x);
word c = LitIsCompl(x)? one(): 0;
for(size j = 0; j < nSize; j++)
if(~(vVals[nSize * a + j] ^ c))
return false;
return true;
}
inline bool LitIsEq(lit x, lit y) const {
if(x == y)
return true;
if(x == LitMax() || y == LitMax())
return false;
bvar xvar = Lit2Bvar(x);
bvar yvar = Lit2Bvar(y);
word c = LitIsCompl(x) ^ LitIsCompl(y)? one(): 0;
for(size j = 0; j < nSize; j++)
if(vVals[nSize * xvar + j] ^ vVals[nSize * yvar + j] ^ c)
return false;
return true;
}
inline size OneCount(lit x) const {
bvar a = Lit2Bvar(x);
size count = 0;
if(nVars > 6) {
for(size j = 0; j < nSize; j++)
count += bsw(vVals[nSize * a + j]).count();
} else
count = bsw(vVals[nSize * a] & ones(nVars)).count();
return LitIsCompl(x)? ((size)1 << nVars) - count: count;
}
public:
inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }
inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }
public:
bool Resize() {
if(nObjsAlloc == nObjsMax)
return false;
lit nObjsAllocLit = (lit)nObjsAlloc << 1;
if(nObjsAllocLit > (lit)BvarMax())
nObjsAlloc = BvarMax();
else
nObjsAlloc = (bvar)nObjsAllocLit;
nTotalSize = nTotalSize << 1;
if(nVerbose >= 2)
std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl;
vVals.resize(nTotalSize);
if(!vRefs.empty())
vRefs.resize(nObjsAlloc);
return true;
}
bool Gbc() {
if(nVerbose >= 2)
std::cout << "Garbage collect" << std::endl;
for(bvar a = nVars + 1; a < nObjs; a++)
if(!vRefs[a])
vDeads.push_back(a);
return vDeads.size();
}
public:
Man(int nVars, Param p): nVars(nVars) {
if(p.nObjsMaxLog < p.nObjsAllocLog)
throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc");
if(nVars >= lww())
nSize = 1ull << (nVars - lww());
else
nSize = 1;
if(!nSize)
throw std::length_error("Memout (nVars) in init");
if(!(nSize << p.nObjsMaxLog))
throw std::length_error("Memout (nObjsMax) in init");
lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
if(!nObjsMaxLit)
throw std::length_error("Memout (nObjsMax) in init");
if(nObjsMaxLit > (lit)BvarMax())
nObjsMax = BvarMax();
else
nObjsMax = (bvar)nObjsMaxLit;
lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
if(!nObjsAllocLit)
throw std::length_error("Memout (nObjsAlloc) in init");
if(nObjsAllocLit > (lit)BvarMax())
nObjsAlloc = BvarMax();
else
nObjsAlloc = (bvar)nObjsAllocLit;
if(nObjsAlloc <= (bvar)nVars)
throw std::invalid_argument("nObjsAlloc must be larger than nVars");
nTotalSize = nSize << p.nObjsAllocLog;
vVals.resize(nTotalSize);
if(p.fCountOnes && nVars > 63)
throw std::length_error("nVars must be less than 64 to count ones");
nObjs = 1;
for(int i = 0; i < 6 && i < nVars; i++) {
for(size j = 0; j < nSize; j++)
vVals[nSize * nObjs + j] = vars(i);
nObjs++;
}
for(int i = 0; i < nVars - 6; i++) {
for(size j = 0; j < nSize; j += (2ull << i))
for(size k = 0; k < (1ull << i); k++)
vVals[nSize * nObjs + j + k] = one();
nObjs++;
}
nVerbose = p.nVerbose;
nGbc = p.nGbc;
if(nGbc || p.nReo != BvarMax())
vRefs.resize(nObjsAlloc);
}
inline lit And(lit x, lit y) {
bvar xvar = Lit2Bvar(x);
bvar yvar = Lit2Bvar(y);
word xcompl = LitIsCompl(x)? one(): 0;
word ycompl = LitIsCompl(y)? one(): 0;
unsigned j;
if(nObjs >= nObjsAlloc && vDeads.empty()) {
bool fRemoved = false;
if(nGbc > 1)
fRemoved = Gbc();
if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc()))
throw std::length_error("Memout (node)");
}
bvar zvar;
if(nObjs < nObjsAlloc)
zvar = nObjs++;
else
zvar = vDeads.back(), vDeads.resize(vDeads.size() - 1);
for(j = 0; j < nSize; j++)
vVals[nSize * zvar + j] = (vVals[nSize * xvar + j] ^ xcompl) & (vVals[nSize * yvar + j] ^ ycompl);
return zvar << 1;
}
inline lit Or(lit x, lit y) {
return LitNot(And(LitNot(x), LitNot(y)));
}
void Reorder() {} // dummy
public:
void SetRef(std::vector<lit> const &vLits) {
vRefs.clear();
vRefs.resize(nObjsAlloc);
for(size_t i = 0; i < vLits.size(); i++)
IncRef(vLits[i]);
}
void TurnOffReo() {
if(!nGbc)
vRefs.clear();
}
void PrintNode(lit x) const {
bvar a = Lit2Bvar(x);
word c = LitIsCompl(x)? one(): 0;
for(size j = 0; j < nSize; j++)
std::cout << bsw(vVals[nSize * a + j] ^ c);
std::cout << std::endl;
}
};
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

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

@ -851,7 +851,7 @@ Gia_Man_t * Gia_ManDupCones2( Gia_Man_t * p, int * pOuts, int nOuts, Vec_Int_t *
***********************************************************************/
int Min_ManRemoveItem( Vec_Wec_t * vCexes, int iItem, int iFirst, int iLimit )
{
Vec_Int_t * vLevel, * vLevel0 = Vec_WecEntry(vCexes, iItem); int i;
Vec_Int_t * vLevel = NULL, * vLevel0 = Vec_WecEntry(vCexes, iItem); int i;
assert( iFirst <= iItem && iItem < iLimit );
Vec_WecForEachLevelReverseStartStop( vCexes, vLevel, i, iLimit, iFirst )
if ( Vec_IntSize(vLevel) > 0 )

39
src/aig/gia/giaQbf.c
View File

@ -482,6 +482,45 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars )
Vec_IntFree( vVarMap );
printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
}
void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars )
{
// original problem: \exists p \forall x \exists y. M(p,x,y)
// negated problem: \forall p \exists x \exists y. !M(p,x,y)
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
Vec_Int_t * vVarMap, * vForAlls, * vExists1, * vExists2;
Gia_Obj_t * pObj;
char * pFileName;
int i, Entry;
// complement the last clause
//int * pLit = pCnf->pClauses[pCnf->nClauses] - 1; *pLit ^= 1;
// create var map
vVarMap = Vec_IntStart( pCnf->nVars );
Gia_ManForEachCi( pGia, pObj, i )
Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], i < nPars ? 1 : 2 );
// create various maps
vExists1 = Vec_IntAlloc( nPars );
vForAlls = Vec_IntAlloc( Gia_ManCiNum(pGia) - nPars );
vExists2 = Vec_IntAlloc( pCnf->nVars - Gia_ManCiNum(pGia) );
Vec_IntForEachEntry( vVarMap, Entry, i )
if ( Entry == 1 )
Vec_IntPush( vExists1, i );
else if ( Entry == 2 )
Vec_IntPush( vForAlls, i );
else
Vec_IntPush( vExists2, i );
// generate CNF
pFileName = Extra_FileNameGenericAppend( pGia->pSpec, ".qdimacs" );
Cnf_DataWriteIntoFileInv( pCnf, pFileName, 0, vExists1, vForAlls, vExists2 );
Cnf_DataFree( pCnf );
Vec_IntFree( vExists1 );
Vec_IntFree( vForAlls );
Vec_IntFree( vExists2 );
Vec_IntFree( vVarMap );
printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
}
/**Function*************************************************************

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

@ -1125,7 +1125,7 @@ void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
}
void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, int fPath )
{
extern void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
char FileNameDot[200];
FILE * pFile;
Vec_Int_t * vXors = NULL, * vAdds = fAdders ? Ree_ManComputeCuts( pMan, &vXors, 0 ) : NULL;
@ -1145,7 +1145,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds,
else
Gia_WriteDotAigSimple( pMan, FileNameDot, vBold );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
Vec_IntFreeP( &vAdds );
Vec_IntFreeP( &vXors );

519
src/aig/gia/giaSif.c
View File

@ -6,7 +6,7 @@
PackageName [Scalable AIG package.]
Synopsis []
Synopsis [Sequential mapping.]
Author [Alan Mishchenko]
@ -19,11 +19,9 @@
***********************************************************************/
#include "gia.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -43,7 +41,348 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
static inline void Gia_ManCutMerge( int * pCut, int * pCut1, int * pCut2, int nSize )
void Gia_ManSifDupNode_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( Gia_ObjUpdateTravIdCurrent(p, pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManSifDupNode_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManSifDupNode_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
void Gia_ManSifDupNode( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, Vec_Int_t * vCopy )
{
int k, iFan;
Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
Gia_ManIncrementTravId( p );
Gia_LutForEachFanin( p, iObj, iFan, k )
{
assert( Vec_IntEntry(vCopy, iFan) >= 0 );
Gia_ManObj(p, iFan)->Value = Vec_IntEntry(vCopy, iFan);
Gia_ObjUpdateTravIdCurrentId(p, iFan);
}
Gia_ManSifDupNode_rec( pNew, p, pObj );
Vec_IntWriteEntry( vCopy, iObj, pObj->Value );
}
Vec_Int_t * Gia_ManSifInitNeg( Gia_Man_t * p, Vec_Int_t * vMoves, Vec_Int_t * vRegs )
{
Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRegs) );
Gia_Obj_t * pObj; int i, iObj;
Gia_Man_t * pNew = Gia_ManStart( 1000 ), * pTemp;
Vec_Int_t * vCopy = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_IntWriteEntry( vCopy, 0, 0 );
Gia_ManForEachRo( p, pObj, i )
Vec_IntWriteEntry( vCopy, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Vec_IntForEachEntry( vMoves, iObj, i )
Gia_ManSifDupNode( pNew, p, iObj, vCopy );
Vec_IntForEachEntry( vRegs, iObj, i )
{
int iLit = Vec_IntEntry( vCopy, iObj );
assert( iLit >= 0 );
Gia_ManAppendCo( pNew, iLit );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
Gia_ManSetPhase( pNew );
Gia_ManForEachPo( pNew, pObj, i )
Vec_IntPush( vRes, pObj->fPhase );
Gia_ManStop( pNew );
Vec_IntFree( vCopy );
assert( Vec_IntSize(vRes) == Vec_IntSize(vRegs) );
return vRes;
}
Vec_Int_t * Gia_ManSifInitPos( Gia_Man_t * p, Vec_Int_t * vMoves, Vec_Int_t * vRegs )
{
extern int * Abc_NtkSolveGiaMiter( Gia_Man_t * p );
int i, iObj, iLitAnd = 1, * pResult = NULL;
Gia_Obj_t * pObj; Vec_Int_t * vRes = NULL;
Gia_Man_t * pNew = Gia_ManStart( 1000 ), * pTemp;
Vec_Int_t * vCopy = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_IntWriteEntry( vCopy, 0, 0 );
Vec_IntForEachEntry( vRegs, iObj, i )
Vec_IntWriteEntry( vCopy, iObj, Gia_ManAppendCi(pNew) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Vec_IntForEachEntry( vMoves, iObj, i )
Gia_ManSifDupNode( pNew, p, iObj, vCopy );
Gia_ManForEachRi( p, pObj, i )
{
int iFan = Gia_ObjFaninId0p(p, pObj);
int iLit = Vec_IntEntry(vCopy, iFan);
if ( iLit == -1 )
continue;
iLit = Abc_LitNotCond( iLit, Gia_ObjFaninC0(pObj) );
iLitAnd = Gia_ManAppendAnd2( pNew, iLitAnd, Abc_LitNot(iLit) );
}
Gia_ManAppendCo( pNew, iLitAnd );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
pResult = Abc_NtkSolveGiaMiter( pNew );
if ( pResult )
{
vRes = Vec_IntAllocArray( pResult, Vec_IntSize(vRegs) );
Gia_ManSetPhasePattern( pNew, vRes );
assert( Gia_ManPo(pNew, 0)->fPhase == 1 );
}
else
{
vRes = Vec_IntStart( Vec_IntSize(vRegs) );
printf( "***!!!*** The SAT problem has no solution. Using all-0 initial state. ***!!!***\n" );
}
Gia_ManStop( pNew );
Vec_IntFree( vCopy );
assert( Vec_IntSize(vRes) == Vec_IntSize(vRegs) );
return vRes;
}
Gia_Man_t * Gia_ManSifDerive( Gia_Man_t * p, Vec_Int_t * vCounts, int fVerbose )
{
Gia_Man_t * pNew = NULL; Gia_Obj_t * pObj;
Vec_Int_t * vCopy = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_Int_t * vCopy2 = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_Int_t * vLuts[3], * vRos[3], * vRegs[2], * vInits[2], * vTemp;
int i, k, Id, iFan;
for ( i = 0; i < 3; i++ )
{
vLuts[i] = Vec_IntAlloc(100);
vRos[i] = Vec_IntAlloc(100);
if ( i == 2 ) break;
vRegs[i] = Vec_IntAlloc(100);
}
Gia_ManForEachLut( p, i )
if ( Vec_IntEntry(vCounts, i) == 1 )
Vec_IntPush( vLuts[0], i );
else if ( Vec_IntEntry(vCounts, i) == -1 )
Vec_IntPush( vLuts[1], i );
else if ( Vec_IntEntry(vCounts, i) == 0 )
Vec_IntPush( vLuts[2], i );
else assert( 0 );
assert( Vec_IntSize(vLuts[0]) || Vec_IntSize(vLuts[1]) );
if ( Vec_IntSize(vLuts[0]) )
{
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vLuts[0], Id, i )
Gia_ObjSetTravIdCurrentId(p, Id);
Gia_ManForEachRo( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj))) )
Vec_IntPush( vRos[0], Gia_ObjId(p, pObj) );
assert( !Vec_IntSize(vLuts[0]) == !Vec_IntSize(vRos[0]) );
}
if ( Vec_IntSize(vLuts[1]) )
{
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vLuts[1], Id, i )
Gia_LutForEachFanin( p, Id, iFan, k )
Gia_ObjSetTravIdCurrentId(p, iFan);
Gia_ManForEachRo( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
Vec_IntPush( vRos[1], Gia_ObjId(p, pObj) );
assert( !Vec_IntSize(vLuts[1]) == !Vec_IntSize(vRos[1]) );
}
Gia_ManIncrementTravId( p );
for ( k = 0; k < 2; k++ )
Vec_IntForEachEntry( vRos[k], Id, i )
Gia_ObjSetTravIdCurrentId(p, Id);
Gia_ManForEachRo( p, pObj, i )
if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
Vec_IntPush( vRos[2], Gia_ObjId(p, pObj) );
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vLuts[0], Id, i )
Gia_ObjSetTravIdCurrentId(p, Id);
Vec_IntForEachEntry( vLuts[0], Id, i )
Gia_LutForEachFanin( p, Id, iFan, k )
if ( !Gia_ObjUpdateTravIdCurrentId(p, iFan) )
Vec_IntPush( vRegs[0], iFan );
Vec_IntSort( vRegs[0], 0 );
assert( Vec_IntCountDuplicates(vRegs[1]) == 0 );
assert( !Vec_IntSize(vLuts[0]) == !Vec_IntSize(vRegs[0]) );
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vLuts[0], Id, i )
Gia_LutForEachFanin( p, Id, iFan, k )
Gia_ObjSetTravIdCurrentId(p, iFan);
Vec_IntForEachEntry( vLuts[2], Id, i )
Gia_LutForEachFanin( p, Id, iFan, k )
Gia_ObjSetTravIdCurrentId(p, iFan);
Gia_ManForEachCo( p, pObj, i )
Gia_ObjSetTravIdCurrentId(p, Gia_ObjFaninId0p(p, pObj));
Vec_IntForEachEntry( vRos[1], Id, i )
if ( Gia_ObjIsTravIdCurrentId(p, Id) )
Vec_IntPush( vRegs[1], Id );
Vec_IntForEachEntry( vLuts[1], Id, i )
if ( Gia_ObjIsTravIdCurrentId(p, Id) )
Vec_IntPush( vRegs[1], Id );
Vec_IntSort( vRegs[1], 0 );
assert( Vec_IntCountDuplicates(vRegs[1]) == 0 );
assert( !Vec_IntSize(vLuts[1]) == !Vec_IntSize(vRegs[1]) );
vInits[0] = Vec_IntSize(vLuts[0]) ? Gia_ManSifInitPos( p, vLuts[0], vRegs[0] ) : Vec_IntAlloc(0);
vInits[1] = Vec_IntSize(vLuts[1]) ? Gia_ManSifInitNeg( p, vLuts[1], vRegs[1] ) : Vec_IntAlloc(0);
if ( fVerbose )
{
printf( "Flops : %5d %5d %5d\n", Vec_IntSize(vRos[0]), Vec_IntSize(vRos[1]), Vec_IntSize(vRos[2]) );
printf( "LUTs : %5d %5d %5d\n", Vec_IntSize(vLuts[0]), Vec_IntSize(vLuts[1]), Vec_IntSize(vLuts[2]) );
printf( "Spots : %5d %5d %5d\n", Vec_IntSize(vRegs[0]), Vec_IntSize(vRegs[1]), 0 );
}
pNew = Gia_ManStart( Gia_ManObjNum(p) + Vec_IntSize(vRegs[0]) + Vec_IntSize(vRegs[1]) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Vec_IntWriteEntry( vCopy, 0, 0 );
Gia_ManForEachPi( p, pObj, i )
Vec_IntWriteEntry( vCopy, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
Vec_IntForEachEntry( vRos[2], Id, i )
Vec_IntWriteEntry( vCopy, Id, Gia_ManAppendCi(pNew) );
Vec_IntForEachEntry( vRegs[1], Id, i )
Vec_IntWriteEntry( vCopy, Id, Abc_LitNotCond(Gia_ManAppendCi(pNew), Vec_IntEntry(vInits[1], i)) );
vTemp = Vec_IntAlloc(100);
Vec_IntForEachEntry( vRegs[0], Id, i )
Vec_IntPush( vTemp, Vec_IntEntry(vCopy, Id) );
Vec_IntForEachEntry( vRegs[0], Id, i )
Vec_IntWriteEntry( vCopy, Id, Abc_LitNotCond(Gia_ManAppendCi(pNew), Vec_IntEntry(vInits[0], i)) );
Vec_IntForEachEntry( vLuts[0], Id, i )
Gia_ManSifDupNode( pNew, p, Id, vCopy );
Vec_IntForEachEntry( vRegs[0], Id, i )
Vec_IntWriteEntry( vCopy, Id, Vec_IntEntry(vTemp, i) );
Vec_IntFree( vTemp );
Gia_ManForEachRoToRiVec( vRos[0], p, pObj, i )
Vec_IntWriteEntry( vCopy, Vec_IntEntry(vRos[0], i), Abc_LitNotCond(Vec_IntEntry(vCopy, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj)) );
Vec_IntForEachEntry( vLuts[2], Id, i )
Gia_ManSifDupNode( pNew, p, Id, vCopy );
Gia_ManForEachRoToRiVec( vRos[1], p, pObj, i )
Vec_IntWriteEntry( vCopy2, Vec_IntEntry(vRos[1], i), Abc_LitNotCond(Vec_IntEntry(vCopy, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj)) );
Vec_IntForEachEntry( vLuts[1], Id, i )
Gia_ManSifDupNode( pNew, p, Id, vCopy2 );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vCopy, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj)) );
Gia_ManForEachRoToRiVec( vRos[2], p, pObj, i )
Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vCopy, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj)) );
Vec_IntForEachEntry( vRegs[1], Id, i )
Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vCopy2, Id), Vec_IntEntry(vInits[1], i)) );
Vec_IntForEachEntry( vRegs[0], Id, i )
Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vCopy, Id), Vec_IntEntry(vInits[0], i)) );
Gia_ManSetRegNum( pNew, Vec_IntSize(vRos[2]) + Vec_IntSize(vRegs[0]) + Vec_IntSize(vRegs[1]) );
for ( i = 0; i < 3; i++ )
{
Vec_IntFreeP( &vLuts[i] );
Vec_IntFreeP( &vRos[i] );
if ( i == 2 ) break;
Vec_IntFreeP( &vRegs[i] );
Vec_IntFreeP( &vInits[i] );
}
Vec_IntFree( vCopy );
Vec_IntFree( vCopy2 );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManSifArea_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCuts, int nSize )
{
int i, * pCut, Area = 1;
if ( Gia_ObjUpdateTravIdCurrent(p, pObj) )
return 0;
if ( !Gia_ObjIsAnd(pObj) )
return 0;
pCut = Vec_IntEntryP( vCuts, Gia_ObjId(p, pObj)*nSize );
for ( i = 1; i <= pCut[0]; i++ )
Area += Gia_ManSifArea_rec( p, Gia_ManObj(p, pCut[i] >> 8), vCuts, nSize );
return Area;
}
int Gia_ManSifArea( Gia_Man_t * p, Vec_Int_t * vCuts, int nSize )
{
Gia_Obj_t * pObj; int i, nArea = 0;
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
nArea += Gia_ManSifArea_rec( p, Gia_ObjFanin0(pObj), vCuts, nSize );
return nArea;
}
int Gia_ManSifDelay_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
{
int i, * pCut, Delay, nFails = 0;
if ( Gia_ObjUpdateTravIdCurrent(p, pObj) )
return 0;
if ( !Gia_ObjIsAnd(pObj) )
return 0;
pCut = Vec_IntEntryP( vCuts, Gia_ObjId(p, pObj)*nSize );
Delay = -ABC_INFINITY-10000;
for ( i = 1; i <= pCut[0]; i++ )
{
nFails += Gia_ManSifDelay_rec( p, Gia_ManObj(p, pCut[i] >> 8), vCuts, vTimes, nSize );
Delay = Abc_MaxInt( Delay, Vec_IntEntry(vTimes, pCut[i] >> 8) );
}
Delay += 1;
return nFails + (int)(Delay > Vec_IntEntry(vTimes, Gia_ObjId(p, pObj)));
}
int Gia_ManSifDelay( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
{
Gia_Obj_t * pObj; int i, nFails = 0;
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
nFails += Gia_ManSifDelay_rec( p, Gia_ObjFanin0(pObj), vCuts, vTimes, nSize );
return nFails;
}
static inline int Gia_ManSifTimeToCount( int Value, int Period )
{
return (Period*0xFFFF + Value)/Period + ((Period*0xFFFF + Value)%Period != 0) - 0x10000;
}
Vec_Int_t * Gia_ManSifTimesToCounts( Gia_Man_t * p, Vec_Int_t * vTimes, int Period )
{
int i, Times;
Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(p) );
Vec_IntFillExtra( vTimes, Gia_ManObjNum(p), 0 );
Vec_IntForEachEntry( vTimes, Times, i )
if ( Gia_ObjIsLut(p, i) )
Vec_IntWriteEntry( vCounts, i, Gia_ManSifTimeToCount(Times, Period) );
return vCounts;
}
Gia_Man_t * Gia_ManSifTransform( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int fVerbose )
{
Gia_Man_t * pNew = NULL; Vec_Int_t * vCounts = NULL;
if ( fVerbose )
printf( "Current area = %d. Period = %d. ", Gia_ManSifArea(p, vCuts, nLutSize+1), Period );
if ( fVerbose )
printf( "Delay checking failed for %d cuts.\n", Gia_ManSifDelay( p, vCuts, vTimes, nLutSize+1 ) );
vCounts = Gia_ManSifTimesToCounts( p, vTimes, Period );
pNew = Gia_ManSifDerive( p, vCounts, fVerbose );
Vec_IntFreeP( &vCounts );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_ManSifCutMerge( int * pCut, int * pCut1, int * pCut2, int nSize )
{
int * pBeg = pCut+1;
int * pBeg1 = pCut1+1;
@ -85,7 +424,7 @@ static inline void Gia_ManCutMerge( int * pCut, int * pCut1, int * pCut2, int nS
pCut[0] = pBeg-(pCut+1);
assert( pCut[0] < nSize );
}
static inline int Gia_ManCutChoice( Gia_Man_t * p, int Level, int iObj, int iSibl, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
static inline int Gia_ManSifCutChoice( Gia_Man_t * p, int Level, int iObj, int iSibl, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
{
int * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
int * pCut2 = Vec_IntEntryP( vCuts, iSibl*nSize );
@ -97,127 +436,165 @@ static inline int Gia_ManCutChoice( Gia_Man_t * p, int Level, int iObj, int iSib
pCut[i] = pCut2[i];
return Level2;
}
static inline int Gia_ManCutOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
static inline int Gia_ManSifCutOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
{
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
int iFan0 = Gia_ObjFaninId0(pObj, iObj);
int iFan1 = Gia_ObjFaninId1(pObj, iObj);
int Cut0[2] = { 1, iFan0 };
int Cut1[2] = { 1, iFan1 };
int Cut0[2] = { 1, iFan0 << 8 };
int Cut1[2] = { 1, iFan1 << 8 };
int * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
int * pCut0 = Vec_IntEntryP( vCuts, iFan0*nSize );
int * pCut1 = Vec_IntEntryP( vCuts, iFan1*nSize );
int Level_ = Vec_IntEntry( vTimes, iObj );
int Level0 = Vec_IntEntry( vTimes, iFan0 );
int Level1 = Vec_IntEntry( vTimes, iFan1 );
int Level = Abc_MaxInt( Level0, Level1 );
if ( Level == 0 )
Level = 1;
int Level = -ABC_INFINITY, i;
assert( pCut0[0] > 0 && pCut1[0] > 0 );
if ( Level0 == Level1 )
Gia_ManCutMerge( pCut, pCut0, pCut1, nSize );
Gia_ManSifCutMerge( pCut, pCut0, pCut1, nSize );
else if ( Level0 > Level1 )
Gia_ManCutMerge( pCut, pCut0, Cut1, nSize );
Gia_ManSifCutMerge( pCut, pCut0, Cut1, nSize );
else //if ( Level0 < Level1 )
Gia_ManCutMerge( pCut, pCut1, Cut0, nSize );
Gia_ManSifCutMerge( pCut, pCut1, Cut0, nSize );
if ( pCut[0] == -1 )
{
pCut[0] = 2;
pCut[1] = iFan0;
pCut[2] = iFan1;
Level++;
pCut[1] = iFan0 << 8;
pCut[2] = iFan1 << 8;
}
for ( i = 1; i <= pCut[0]; i++ )
Level = Abc_MaxInt( Level, Vec_IntEntry(vTimes, pCut[i] >> 8) );
Level++;
if ( Gia_ObjSibl(p, iObj) )
Level = Gia_ManCutChoice( p, Level, iObj, Gia_ObjSibl(p, iObj), vCuts, vTimes, nSize );
Level = Gia_ManSifCutChoice( p, Level, iObj, Gia_ObjSibl(p, iObj), vCuts, vTimes, nSize );
assert( pCut[0] > 0 && pCut[0] < nSize );
Vec_IntUpdateEntry( vTimes, iObj, Level );
return Level > Level_;
}
int Gia_ManCheckIter( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period )
int Gia_ManSifCheckIter( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period )
{
int i, fChange = 0, nSize = nLutSize+1;
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObjRo), Vec_IntEntry(vTimes, Gia_ObjId(p, pObjRi)) - Period );
Gia_ManForEachAnd( p, pObj, i )
fChange |= Gia_ManCutOne( p, i, vCuts, vTimes, nSize );
Gia_ManForEachRi( p, pObj, i )
fChange |= Gia_ManSifCutOne( p, i, vCuts, vTimes, nSize );
Gia_ManForEachCo( p, pObj, i )
Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) );
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
{
int TimeNew = Vec_IntEntry(vTimes, Gia_ObjId(p, pObjRi)) - Period;
TimeNew = Abc_MaxInt( TimeNew, Vec_IntEntry(vTimes, Gia_ObjId(p, pObjRo)) );
Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObjRo), TimeNew );
}
return fChange;
}
int Gia_ManCheckPeriod( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int * pIters )
int Gia_ManSifCheckPeriod( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int * pIters )
{
Gia_Obj_t * pObj; int i;
Gia_Obj_t * pObj; int i, Id, nSize = nLutSize+1;
assert( Gia_ManRegNum(p) > 0 );
Vec_IntFill( vTimes, Gia_ManObjNum(p), -ABC_INFINITY );
Gia_ManForEachCiId( p, Id, i )
Vec_IntWriteEntry( vCuts, Id*nSize, 1 );
Gia_ManForEachCiId( p, Id, i )
Vec_IntWriteEntry( vCuts, Id*nSize+1, Id << 8 );
Vec_IntFill( vTimes, Gia_ManObjNum(p), -Period );
Vec_IntWriteEntry( vTimes, 0, 0 );
Gia_ManForEachPi( p, pObj, i )
Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), 0 );
for ( *pIters = 0; *pIters < 100; (*pIters)++ )
{
if ( !Gia_ManCheckIter(p, vCuts, vTimes, nLutSize, Period) )
if ( !Gia_ManSifCheckIter(p, vCuts, vTimes, nLutSize, Period) )
return 1;
Gia_ManForEachPo( p, pObj, i )
if ( Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) > Period )
if ( Vec_IntEntry(vTimes, Gia_ObjId(p, pObj)) > Period )
return 0;
Gia_ManForEachObj( p, pObj, i )
if ( Vec_IntEntry(vTimes, Gia_ObjId(p, pObj)) > 2*Period )
return 0;
}
return 0;
}
static inline void Gia_ManPrintCutOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nSize )
{
int i, * pCut = Vec_IntEntryP( vCuts, iObj*nSize );
printf( "Obj %4d : Depth %d CutSize %d Cut {", iObj, Vec_IntEntry(vTimes, iObj), pCut[0] );
for ( i = 1; i <= pCut[0]; i++ )
printf( " %d", pCut[i] );
printf( " }\n" );
}
int Gia_ManTestMapComb( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize )
int Gia_ManSifMapComb( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize )
{
Gia_Obj_t * pObj; int i, Id, Res = 0, nSize = nLutSize+1;
Vec_IntFill( vTimes, Gia_ManObjNum(p), 0 );
Gia_ManForEachCiId( p, Id, i )
Vec_IntWriteEntry( vCuts, Id*nSize, 1 );
Gia_ManForEachCiId( p, Id, i )
Vec_IntWriteEntry( vCuts, Id*nSize+1, Id );
Vec_IntWriteEntry( vCuts, Id*nSize+1, Id << 8 );
Gia_ManForEachAnd( p, pObj, i )
Gia_ManCutOne( p, i, vCuts, vTimes, nSize );
Gia_ManSifCutOne( p, i, vCuts, vTimes, nSize );
Gia_ManForEachCo( p, pObj, i )
Res = Abc_MaxInt( Res, Vec_IntEntry(vTimes, Gia_ObjFaninId0p(p, pObj)) );
//Gia_ManForEachAnd( p, pObj, i )
// Gia_ManPrintCutOne( p, i, vCuts, vTimes, nSize );
return Res;
}
void Gia_ManPrintTimes( Gia_Man_t * p, Vec_Int_t * vTimes, int Period )
void Gia_ManSifPrintTimes( Gia_Man_t * p, Vec_Int_t * vTimes, int Period )
{
int Pos[16] = {0};
int Neg[16] = {0};
Gia_Obj_t * pObj; int i;
Gia_ManForEachAnd( p, pObj, i )
{
int Time = Vec_IntEntry(vTimes, i)-Period;
Time = Abc_MinInt( Time, 10*Period );
Time = Abc_MaxInt( Time, -10*Period );
if ( Time >= 0 )
Pos[(Time + Period-1)/Period]++;
int i, Value, Pos[256] = {0}, Neg[256] = {0};
Gia_ManForEachLut( p, i )
{
Value = Gia_ManSifTimeToCount( Vec_IntEntry(vTimes, i), Period );
Value = Abc_MinInt( Value, 255 );
Value = Abc_MaxInt( Value, -255 );
if ( Value >= 0 )
Pos[Value]++;
else
Neg[(-Time + Period-1)/Period]++;
Neg[-Value]++;
}
printf( "Statistics: " );
for ( i = 15; i > 0; i-- )
for ( i = 255; i > 0; i-- )
if ( Neg[i] )
printf( " -%d=%d", i, Neg[i] );
for ( i = 0; i < 16; i++ )
for ( i = 0; i < 256; i++ )
if ( Pos[i] )
printf( " %d=%d", i, Pos[i] );
printf( "\n" );
}
Gia_Man_t * Gia_ManTestSif( Gia_Man_t * p, int nLutSize, int fVerbose )
int Gia_ManSifDeriveMapping_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCuts, int nSize )
{
int nIters, nSize = nLutSize+1; // (2+1+nSize)*4=40 bytes/node
int i, * pCut, Area = 1;
if ( !Gia_ObjIsAnd(pObj) )
return 0;
if ( Gia_ObjUpdateTravIdCurrent(p, pObj) )
return 0;
pCut = Vec_IntEntryP( vCuts, Gia_ObjId(p, pObj)*nSize );
for ( i = 1; i <= pCut[0]; i++ )
Area += Gia_ManSifDeriveMapping_rec( p, Gia_ManObj(p, pCut[i] >> 8), vCuts, nSize );
Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
Vec_IntPush( p->vMapping, pCut[0] );
for ( i = 1; i <= pCut[0]; i++ )
{
Gia_Obj_t * pObj = Gia_ManObj(p, pCut[i] >> 8);
assert( !Gia_ObjIsAnd(pObj) || Gia_ObjIsLut(p, pCut[i] >> 8) );
Vec_IntPush( p->vMapping, pCut[i] >> 8 );
}
Vec_IntPush( p->vMapping, -1 );
return Area;
}
int Gia_ManSifDeriveMapping( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int fVerbose )
{
Gia_Obj_t * pObj; int i, nArea = 0;
if ( p->vMapping != NULL )
{
printf( "Removing available combinational mapping.\n" );
Vec_IntFreeP( &p->vMapping );
}
assert( p->vMapping == NULL );
p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
nArea += Gia_ManSifDeriveMapping_rec( p, Gia_ObjFanin0(pObj), vCuts, nLutSize+1 );
return nArea;
}
Gia_Man_t * Gia_ManSifPerform( Gia_Man_t * p, int nLutSize, int fEvalOnly, int fVerbose )
{
Gia_Man_t * pNew = NULL;
int nIters, Status, nSize = nLutSize+1; // (2+1+nSize)*4=40 bytes/node
abctime clk = Abc_Clock();
Vec_Int_t * vCuts = Vec_IntStart( Gia_ManObjNum(p) * nSize );
Vec_Int_t * vTimes = Vec_IntAlloc( Gia_ManObjNum(p) );
int Lower = 0;
int Upper = Gia_ManTestMapComb( p, vCuts, vTimes, nLutSize );
int Upper = Gia_ManSifMapComb( p, vCuts, vTimes, nLutSize );
int CombD = Upper;
if ( fVerbose && Gia_ManRegNum(p) )
printf( "Clock period %2d is %s\n", Lower, 0 ? "Yes" : "No " );
if ( fVerbose && Gia_ManRegNum(p) )
@ -225,7 +602,7 @@ Gia_Man_t * Gia_ManTestSif( Gia_Man_t * p, int nLutSize, int fVerbose )
while ( Gia_ManRegNum(p) > 0 && Upper - Lower > 1 )
{
int Middle = (Upper + Lower) / 2;
int Status = Gia_ManCheckPeriod( p, vCuts, vTimes, nLutSize, Middle, &nIters );
int Status = Gia_ManSifCheckPeriod( p, vCuts, vTimes, nLutSize, Middle, &nIters );
if ( Status )
Upper = Middle;
else
@ -234,18 +611,34 @@ Gia_Man_t * Gia_ManTestSif( Gia_Man_t * p, int nLutSize, int fVerbose )
printf( "Clock period %2d is %s after %d iterations\n", Middle, Status ? "Yes" : "No ", nIters );
}
if ( fVerbose )
printf( "Clock period = %2d ", Upper );
printf( "Best period = <<%d>> (%.2f %%) ", Upper, (float)(100.0*(CombD-Upper)/CombD) );
if ( fVerbose )
printf( "LUT size = %d ", nLutSize );
if ( fVerbose )
printf( "Memory usage = %.2f MB ", 4.0*(2+1+nSize)*Gia_ManObjNum(p)/(1 << 20) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Gia_ManCheckPeriod( p, vCuts, vTimes, nLutSize, Upper, &nIters );
//Gia_ManPrintTimes( p, vTimes, Upper );
if ( Upper == CombD )
{
Vec_IntFree( vCuts );
Vec_IntFree( vTimes );
printf( "Combinational delay (%d) cannot be improved.\n", CombD );
return Gia_ManDup( p );
}
Status = Gia_ManSifCheckPeriod( p, vCuts, vTimes, nLutSize, Upper, &nIters );
assert( Status );
Status = Gia_ManSifDeriveMapping( p, vCuts, vTimes, nLutSize, Upper, fVerbose );
if ( fEvalOnly )
{
printf( "Optimized level %2d (%6.2f %% less than comb level %2d). LUT size = %d. Area estimate = %d.\n",
Upper, (float)(100.0*(CombD-Upper)/CombD), CombD, nLutSize, Gia_ManSifArea(p, vCuts, nLutSize+1) );
printf( "The command is invoked in the evaluation mode. Retiming is not performed.\n" );
}
else
pNew = Gia_ManSifTransform( p, vCuts, vTimes, nLutSize, Upper, fVerbose );
Vec_IntFree( vCuts );
Vec_IntFree( vTimes );
return NULL;
return pNew;
}
////////////////////////////////////////////////////////////////////////

428
src/aig/gia/giaSimBase.c
View File

@ -3260,6 +3260,434 @@ void Gia_ManRelDeriveTest( Gia_Man_t * p )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManRelOutsTfo_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vTfo )
{
if ( Gia_ObjIsTravIdPrevious(p, pObj) )
return 1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return 0;
if ( pObj->fPhase )
{
Gia_ObjSetTravIdPrevious(p, pObj);
return 1;
}
if ( Gia_ObjIsAnd(pObj) )
{
int Val0 = Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin0(pObj), vTfo );
int Val1 = Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin1(pObj), vTfo );
if ( Val0 || Val1 )
{
Gia_ObjSetTravIdPrevious(p, pObj);
Vec_IntPush( vTfo, Gia_ObjId(p, pObj) );
return 1;
}
}
Gia_ObjSetTravIdCurrent(p, pObj);
return 0;
}
Vec_Int_t * Gia_ManRelOutsTfo( Gia_Man_t * p, Vec_Int_t * vOuts )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vTfo = Vec_IntAlloc( 100 );
Gia_ManIncrementTravId( p );
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrentId( p, 0 );
Gia_ManCleanPhase( p );
Gia_ManForEachObjVec( vOuts, p, pObj, i )
pObj->fPhase = 1;
Gia_ManForEachCo( p, pObj, i )
if ( Gia_ManRelOutsTfo_rec( p, Gia_ObjFanin0(pObj), vTfo ) )
Vec_IntPush( vTfo, Gia_ObjId(p, pObj) );
Gia_ManForEachObjVec( vOuts, p, pObj, i )
pObj->fPhase = 0;
//Vec_IntPrint( vTfo );
return vTfo;
}
void Gia_ManSimPatSimTfo( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vTfo )
{
Gia_Obj_t * pObj;
int i, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
Gia_ManForEachObjVec( vTfo, p, pObj, i )
if ( Gia_ObjIsAnd(pObj) )
Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vSims );
else
Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords, vSims );
}
void Gia_ManSimPatSimMiter( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2, word * pSims, int nWords )
{
Gia_Obj_t * pObj; int i;
Gia_ManForEachCo( p, pObj, i )
Abc_TtOrXor( pSims, Vec_WrdEntryP(vSims, Gia_ObjId(p, pObj)*nWords), Vec_WrdEntryP(vSims2, Gia_ObjId(p, pObj)*nWords), nWords );
Abc_TtNot( pSims, nWords );
}
Vec_Wrd_t * Gia_ManRelDeriveRel( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t * vSims )
{
extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
int i, o, iObj, nMintsO = 1 << Vec_IntSize(vOuts);
int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
Vec_Wrd_t * vSims2 = Vec_WrdDup( vSims );
Vec_Wrd_t * vRel = Vec_WrdStart( nWords * 64 );
Vec_Wrd_t * vRel2 = Vec_WrdStart( nWords * 64 );
Vec_Int_t * vTfo = Gia_ManRelOutsTfo( p, vOuts );
assert( 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs) + nMintsO <= 64 );
assert( Vec_WrdSize(p->vSimsPi) % Gia_ManCiNum(p) == 0 );
Vec_IntForEachEntry( vIns, iObj, o )
memcpy( Vec_WrdEntryP(vRel, nWords*o), Vec_WrdEntryP(vSims, iObj*nWords), sizeof(word)*nWords );
Vec_IntForEachEntry( vDivs, iObj, o )
memcpy( Vec_WrdEntryP(vRel, nWords*(Vec_IntSize(vIns)+o)), Vec_WrdEntryP(vSims, iObj*nWords), sizeof(word)*nWords );
for ( o = 0; o < nMintsO; o++ )
{
word * pRes = Vec_WrdEntryP(vRel, nWords*(Vec_IntSize(vIns)+Vec_IntSize(vDivs)+o));
Vec_IntForEachEntry( vOuts, iObj, i )
memset( Vec_WrdEntryP(vSims2, iObj*nWords), ((o >> i) & 1) ? 0xFF : 0x00, sizeof(word)*nWords );
Gia_ManSimPatSimTfo( p, vSims2, vTfo );
Gia_ManSimPatSimMiter( p, vSims, vSims2, pRes, nWords );
}
Extra_BitMatrixTransposeP( vRel, nWords, vRel2, 1 );
Vec_IntFree( vTfo );
Vec_WrdFree( vSims2 );
Vec_WrdFree( vRel );
return vRel2;
}
void Gia_ManRelDeriveSims( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel, Vec_Wrd_t ** pvSimsIn, Vec_Wrd_t ** pvSimsOut )
{
Vec_Wrd_t * vVals = Vec_WrdStartFull( 1 << Vec_IntSize(vIns) );
Vec_Wrd_t * vSets = Vec_WrdStartFull( 1 << Vec_IntSize(vIns) );
int m, nMints = 1 << Gia_ManCiNum(p), nCares = 0;
int nMintsI = 1 << Vec_IntSize(vIns);
int nShift = Vec_IntSize(vIns) + Vec_IntSize(vDivs);
int MaskI = Abc_Tt6Mask( Vec_IntSize(vIns) );
int MaskD = Abc_Tt6Mask( nShift );
for ( m = 0; m < nMints; m++ )
{
word Sign = Vec_WrdEntry( vRel, m );
*Vec_WrdEntryP( vVals, (int)Sign & MaskI ) = (int)Sign & MaskD;
*Vec_WrdEntryP( vSets, (int)Sign & MaskI ) &= Sign >> nShift;
}
for ( m = 0; m < nMintsI; m++ )
if ( ~Vec_WrdEntry(vSets, m) )
nCares++;
assert( *pvSimsIn == NULL );
assert( *pvSimsOut == NULL );
*pvSimsIn = Vec_WrdAlloc( nCares );
*pvSimsOut = Vec_WrdAlloc( nCares );
for ( m = 0; m < nMintsI; m++ )
if ( ~Vec_WrdEntry(vSets, m) )
{
Vec_WrdPush( *pvSimsIn, Vec_WrdEntry(vVals, m) << 1 );
Vec_WrdPush( *pvSimsOut, Vec_WrdEntry(vSets, m) );
}
assert( Vec_WrdSize(*pvSimsIn) == nCares );
Vec_WrdFree( vSets );
Vec_WrdFree( vVals );
}
int Gia_ManRelCheck_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( Gia_ObjIsTravIdPrevious(p, pObj) )
return 1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return 0;
if ( pObj->fPhase )
{
Gia_ObjSetTravIdPrevious(p, pObj);
return 1;
}
if ( Gia_ObjIsAnd(pObj) )
{
int Val0 = Gia_ManRelCheck_rec( p, Gia_ObjFanin0(pObj) );
int Val1 = Gia_ManRelCheck_rec( p, Gia_ObjFanin1(pObj) );
if ( Val0 && Val1 )
{
Gia_ObjSetTravIdPrevious(p, pObj);
return 1;
}
}
Gia_ObjSetTravIdCurrent(p, pObj);
return 0;
}
int Gia_ManRelCheck( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts )
{
Gia_Obj_t * pObj; int i, Res = 1;
Gia_ManIncrementTravId( p );
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrentId( p, 0 );
Gia_ManCleanPhase( p );
Gia_ManForEachObjVec( vIns, p, pObj, i )
pObj->fPhase = 1;
Gia_ManForEachObjVec( vDivs, p, pObj, i )
if ( !Gia_ManRelCheck_rec( p, pObj ) )
Res = 0;
Gia_ManForEachObjVec( vOuts, p, pObj, i )
if ( !Gia_ManRelCheck_rec( p, pObj ) )
Res = 0;
Gia_ManForEachObjVec( vIns, p, pObj, i )
pObj->fPhase = 0;
return Res;
}
void Gia_ManRelCompute( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Vec_Wrd_t ** pvSimsIn, Vec_Wrd_t ** pvSimsOut )
{
Vec_Wrd_t * vSims, * vRel;
//Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
if ( !Gia_ManRelCheck( p, vIns, vDivs, vOuts ) )
printf( "Window is NOT consistent.\n" );
else
printf( "Window is consistent.\n" );
vSims = Gia_ManSimPatSim( p );
vRel = Gia_ManRelDeriveRel( p, vIns, vDivs, vOuts, vSims );
Gia_ManRelDeriveSims( p, vIns, vDivs, vOuts, vSims, vRel, pvSimsIn, pvSimsOut );
Vec_WrdFree( vRel );
Vec_WrdFree( vSims );
Vec_WrdFreeP( &p->vSimsPi );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
/*
Vec_Int_t * Gia_ManRelInitIns1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 22 );
Vec_IntPush( vRes, 41 );
Vec_IntPush( vRes, 45 );
Vec_IntPush( vRes, 59 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitDivs1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 46 );
Vec_IntPush( vRes, 47 );
Vec_IntPush( vRes, 48 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitOuts1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 65 );
Vec_IntPush( vRes, 66 );
return vRes;
}
*/
Vec_Int_t * Gia_ManRelInitIns1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 22 );
Vec_IntPush( vRes, 25 );
Vec_IntPush( vRes, 42 );
Vec_IntPush( vRes, 59 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitDivs1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 43 );
Vec_IntPush( vRes, 44 );
Vec_IntPush( vRes, 45 );
Vec_IntPush( vRes, 46 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitOuts1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 60 );
Vec_IntPush( vRes, 61 );
return vRes;
}
/*
Vec_Int_t * Gia_ManRelInitIns1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 22 );
Vec_IntPush( vRes, 25 );
Vec_IntPush( vRes, 42 );
Vec_IntPush( vRes, 50 );
Vec_IntPush( vRes, 67 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitDivs1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 43 );
Vec_IntPush( vRes, 44 );
Vec_IntPush( vRes, 45 );
Vec_IntPush( vRes, 46 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitOuts1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 73 );
Vec_IntPush( vRes, 74 );
return vRes;
}
*/
/*
Vec_Int_t * Gia_ManRelInitIns1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 43 );
Vec_IntPush( vRes, 46 );
//Vec_IntPush( vRes, 49 );
Vec_IntPush( vRes, 50 );
Vec_IntPush( vRes, 67 );
Vec_IntPush( vRes, 75 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitDivs1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitOuts1()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 73 );
Vec_IntPush( vRes, 86 );
Vec_IntPush( vRes, 88 );
return vRes;
}
*/
void Gia_ManRelDeriveTest1( Gia_Man_t * p )
{
extern void Exa6_WriteFile2( char * pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut );
word Entry; int i;
Vec_Int_t * vIns = Gia_ManRelInitIns1();
Vec_Int_t * vDivs = Gia_ManRelInitDivs1();
Vec_Int_t * vOuts = Gia_ManRelInitOuts1();
Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
Gia_ManRelCompute( p, vIns, vDivs, vOuts, &vSimsDiv, &vSimsOut );
printf( "Inputs:\n" );
Vec_WrdForEachEntry( vSimsDiv, Entry, i )
Abc_TtPrintBits( &Entry, 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs) );
printf( "Outputs:\n" );
Vec_WrdForEachEntry( vSimsOut, Entry, i )
Abc_TtPrintBits( &Entry, 1 << Vec_IntSize(vOuts) );
printf( "\n" );
Exa6_WriteFile2( "mul44_i5_n0_t3_s11.rel", Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), vSimsDiv, vSimsOut );
Vec_WrdFree( vSimsDiv );
Vec_WrdFree( vSimsOut );
Vec_IntFree( vIns );
Vec_IntFree( vDivs );
Vec_IntFree( vOuts );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManChangeTest3( Gia_Man_t * p )
{
extern void Exa6_WriteFile2( char * pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut );
extern void Exa_ManExactPrint( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nDivs, int nOuts );
extern Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose );
extern Gia_Man_t * Gia_ManDupMini( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vDivs, Vec_Int_t * vOuts, Mini_Aig_t * pMini );
Gia_Man_t * pNew = NULL;
Mini_Aig_t * pMini = NULL;
Vec_Int_t * vIns = Gia_ManRelInitIns1();
Vec_Int_t * vDivs = Gia_ManRelInitDivs1();
Vec_Int_t * vOuts = Gia_ManRelInitOuts1();
int nNodes = 4;
Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
Gia_ManRelCompute( p, vIns, vDivs, vOuts, &vSimsDiv, &vSimsOut );
Exa_ManExactPrint( vSimsDiv, vSimsOut, 1 + Vec_IntSize(vIns) + Vec_IntSize(vDivs), Vec_IntSize(vOuts) );
//Exa6_WriteFile2( "mul44_i%d_n%d_t%d_s%d.rel", Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), nNodes );
pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), nNodes, 1, 1 );
if ( pMini )
{
pNew = Gia_ManDupMini( p, vIns, vDivs, vOuts, pMini );
Mini_AigStop( pMini );
}
Vec_WrdFree( vSimsDiv );
Vec_WrdFree( vSimsOut );
Vec_IntFree( vIns );
Vec_IntFree( vDivs );
Vec_IntFree( vOuts );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
{
Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
int n, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
int i, nLimit = Gia_ManCiNum(p) < 6 ? 1 << Gia_ManCiNum(p) : 64*nWords;
Vec_Str_t * vOut = Vec_StrAlloc( nLimit*(Gia_ManCoNum(p) + 3)+1 );
assert( Vec_WrdSize(vSims) == nWords * Gia_ManCoNum(p) );
for ( n = 0; n < nLimit; n++ )
{
for ( i = 0; i < Gia_ManCoNum(p); i++ )
Vec_StrPush( vOut, (char)('0' + Abc_TtGetBit(Vec_WrdEntryP(vSims, i*nWords), n)) );
Vec_StrPush( vOut, ' ' );
Vec_StrPush( vOut, '1' );
Vec_StrPush( vOut, '\n' );
}
Vec_StrPush( vOut, '\0' );
Vec_WrdFree( vSims );
Vec_WrdFree( vSimsPi );
return vOut;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

424
src/aig/gia/giaTranStoch.c Normal file
View File

@ -0,0 +1,424 @@
/**CFile****************************************************************
FileName [giaTranStoch.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Implementation of transduction method.]
Author [Yukio Miyasaka]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 2023.]
Revision [$Id: giaTranStoch.c,v 1.00 2023/05/10 00:00:00 Exp $]
***********************************************************************/
#include <base/abc/abc.h>
#include <aig/aig/aig.h>
#include <opt/dar/dar.h>
#include <aig/gia/gia.h>
#include <aig/gia/giaAig.h>
#include <base/main/main.h>
#include <base/main/mainInt.h>
#include <map/mio/mio.h>
#include <opt/sfm/sfm.h>
#include <opt/fxu/fxu.h>
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif
ABC_NAMESPACE_IMPL_START
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
extern int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
Abc_Ntk_t * Gia_ManTranStochPut( Gia_Man_t * pGia ) {
Abc_Ntk_t * pNtk;
Aig_Man_t * pMan = Gia_ManToAig( pGia, 0 );
pNtk = Abc_NtkFromAigPhase( pMan );
Aig_ManStop( pMan );
return pNtk;
}
Abc_Ntk_t * Gia_ManTranStochIf( Abc_Ntk_t * pNtk ) {
If_Par_t Pars, * pPars = &Pars;
If_ManSetDefaultPars( pPars );
pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
pPars->nLutSize = pPars->pLutLib->LutMax;
return Abc_NtkIf( pNtk, pPars );
}
void Gia_ManTranStochMfs2( Abc_Ntk_t * pNtk ) {
Sfm_Par_t Pars, * pPars = &Pars;
Sfm_ParSetDefault( pPars );
Abc_NtkPerformMfs( pNtk, pPars );
}
Gia_Man_t * Gia_ManTranStochGet( Abc_Ntk_t * pNtk ) {
Gia_Man_t * pGia;
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
pGia = Gia_ManFromAig( pAig );
Aig_ManStop( pAig );
return pGia;
}
void Gia_ManTranStochFx( Abc_Ntk_t * pNtk ) {
Fxu_Data_t Params, * p = &Params;
Abc_NtkSetDefaultFxParams( p );
Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fCanonDivs, p->fVerbose, p->fVeryVerbose );
Abc_NtkFxuFreeInfo( p );
}
Gia_Man_t * Gia_ManTranStochRefactor( Gia_Man_t * pGia ) {
Gia_Man_t * pNew;
Aig_Man_t * pAig, * pTemp;
Dar_RefPar_t Pars, * pPars = &Pars;
Dar_ManDefaultRefParams( pPars );
pPars->fUseZeros = 1;
pAig = Gia_ManToAig( pGia, 0 );
Dar_ManRefactor( pAig, pPars );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
pNew = Gia_ManFromAig( pAig );
Aig_ManStop( pAig );
return pNew;
}
struct Gia_ManTranStochParam {
Gia_Man_t * pStart;
int nSeed;
int nHops;
int nRestarts;
int nSeedBase;
int fMspf;
int fMerge;
int fResetHop;
int fZeroCostHop;
int fRefactor;
int fTruth;
int fNewLine;
Gia_Man_t * pExdc;
int nVerbose;
#ifdef ABC_USE_PTHREADS
int nSp;
int nIte;
Gia_Man_t * pRes;
int fWorking;
pthread_mutex_t * mutex;
#endif
};
typedef struct Gia_ManTranStochParam Gia_ManTranStochParam;
void Gia_ManTranStochLock( Gia_ManTranStochParam * p ) {
#ifdef ABC_USE_PTHREADS
if ( p->fWorking )
pthread_mutex_lock( p->mutex );
#endif
}
void Gia_ManTranStochUnlock( Gia_ManTranStochParam * p ) {
#ifdef ABC_USE_PTHREADS
if ( p->fWorking )
pthread_mutex_unlock( p->mutex );
#endif
}
Gia_Man_t * Gia_ManTranStochOpt1( Gia_ManTranStochParam * p, Gia_Man_t * pOld ) {
Gia_Man_t * pGia, * pNew;
int i = 0, n;
pGia = Gia_ManDup( pOld );
do {
n = Gia_ManAndNum( pGia );
if ( p->fTruth )
pNew = Gia_ManTransductionTt( pGia, (p->fMerge? 8: 7), p->fMspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 );
else
pNew = Gia_ManTransductionBdd( pGia, (p->fMerge? 8: 7), p->fMspf, p->nSeed++, 0, 0, 0, 0, p->pExdc, p->fNewLine, p->nVerbose > 0? p->nVerbose - 1: 0 );
Gia_ManStop( pGia );
pGia = pNew;
if ( p->fRefactor ) {
pNew = Gia_ManTranStochRefactor( pGia );
Gia_ManStop( pGia );
pGia = pNew;
} else {
Gia_ManTranStochLock( p );
pNew = Gia_ManCompress2( pGia, 1, 0 );
Gia_ManTranStochUnlock( p );
Gia_ManStop( pGia );
pGia = pNew;
}
if ( p->nVerbose )
printf( "* ite %d : #nodes = %5d\n", i, Gia_ManAndNum( pGia ) );
i++;
} while ( n > Gia_ManAndNum( pGia ) );
return pGia;
}
Gia_Man_t * Gia_ManTranStochOpt2( Gia_ManTranStochParam * p ) {
int i, n = Gia_ManAndNum( p->pStart );
Gia_Man_t * pGia, * pBest, * pNew;
Abc_Ntk_t * pNtk, * pNtkRes;
pGia = Gia_ManDup( p->pStart );
pBest = Gia_ManDup( pGia );
for ( i = 0; 1; i++ ) {
pNew = Gia_ManTranStochOpt1( p, pGia );
Gia_ManStop( pGia );
pGia = pNew;
if ( n > Gia_ManAndNum( pGia ) ) {
n = Gia_ManAndNum( pGia );
Gia_ManStop( pBest );
pBest = Gia_ManDup( pGia );
if ( p->fResetHop )
i = 0;
}
if ( i == p->nHops )
break;
if ( p->fZeroCostHop ) {
pNew = Gia_ManTranStochRefactor( pGia );
Gia_ManStop( pGia );
pGia = pNew;
} else {
Gia_ManTranStochLock( p );
pNtk = Gia_ManTranStochPut( pGia );
Gia_ManTranStochUnlock( p );
Gia_ManStop( pGia );
pNtkRes = Gia_ManTranStochIf( pNtk );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
Gia_ManTranStochMfs2( pNtk );
Gia_ManTranStochLock( p );
pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
Gia_ManTranStochUnlock( p );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
pGia = Gia_ManTranStochGet( pNtk );
Abc_NtkDelete( pNtk );
}
if ( p->nVerbose )
printf( "* hop %d : #nodes = %5d\n", i, Gia_ManAndNum( pGia ) );
}
Gia_ManStop( pGia );
return pBest;
}
Gia_Man_t * Gia_ManTranStochOpt3( Gia_ManTranStochParam * p ) {
int i, n = Gia_ManAndNum( p->pStart );
Gia_Man_t * pBest, * pNew;
pBest = Gia_ManDup( p->pStart );
for ( i = 0; i <= p->nRestarts; i++ ) {
p->nSeed = 1234 * (i + p->nSeedBase);
pNew = Gia_ManTranStochOpt2( p );
if ( p->nRestarts && p->nVerbose )
printf( "* res %2d : #nodes = %5d\n", i, Gia_ManAndNum( pNew ) );
if ( n > Gia_ManAndNum( pNew ) ) {
n = Gia_ManAndNum( pNew );
Gia_ManStop( pBest );
pBest = pNew;
} else {
Gia_ManStop( pNew );
}
}
return pBest;
}
#ifdef ABC_USE_PTHREADS
void * Gia_ManTranStochWorkerThread( void * pArg ) {
Gia_ManTranStochParam * p = (Gia_ManTranStochParam *)pArg;
volatile int * pPlace = &p->fWorking;
while ( 1 ) {
while ( *pPlace == 0 );
assert( p->fWorking );
if ( p->pStart == NULL ) {
pthread_exit( NULL );
assert( 0 );
return NULL;
}
p->nSeed = 1234 * (p->nIte + p->nSeedBase);
p->pRes = Gia_ManTranStochOpt2( p );
p->fWorking = 0;
}
assert( 0 );
return NULL;
}
#endif
Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nSeedBase, int fMspf, int fMerge, int fResetHop, int fZeroCostHop, int fRefactor, int fTruth, int fSingle, int fOriginalOnly, int fNewLine, Gia_Man_t * pExdc, int nThreads, int nVerbose ) {
int i, j = 0;
Gia_Man_t * pNew, * pBest, * pStart;
Abc_Ntk_t * pNtk, * pNtkRes; Vec_Ptr_t * vpStarts;
Gia_ManTranStochParam Par, *p = &Par;
p->nRestarts = nRestarts;
p->nHops = nHops;
p->nSeedBase = nSeedBase;
p->fMspf = fMspf;
p->fMerge = fMerge;
p->fResetHop = fResetHop;
p->fZeroCostHop = fZeroCostHop;
p->fRefactor = fRefactor;
p->fTruth = fTruth;
p->fNewLine = fNewLine;
p->pExdc = pExdc;
p->nVerbose = nVerbose;
#ifdef ABC_USE_PTHREADS
p->fWorking = 0;
#endif
// setup start points
vpStarts = Vec_PtrAlloc( 4 );
Vec_PtrPush( vpStarts, Gia_ManDup( pGia ) );
if ( !fOriginalOnly ) {
{ // &put; collapse; st; &get;
pNtk = Gia_ManTranStochPut( pGia );
pNtkRes = Abc_NtkCollapse( pNtk, ABC_INFINITY, 0, 1, 0, 0, 0 );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
pNew = Gia_ManTranStochGet( pNtk );
Abc_NtkDelete( pNtk );
Vec_PtrPush( vpStarts, pNew );
}
{ // &ttopt;
pNew = Gia_ManTtopt( pGia, Gia_ManCiNum( pGia ), Gia_ManCoNum( pGia ), 100 );
Vec_PtrPush( vpStarts, pNew );
}
{ // &put; collapse; sop; fx;
pNtk = Gia_ManTranStochPut( pGia );
pNtkRes = Abc_NtkCollapse( pNtk, ABC_INFINITY, 0, 1, 0, 0, 0 );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
Gia_ManTranStochFx( pNtk );
pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
Abc_NtkDelete( pNtk );
pNtk = pNtkRes;
pNew = Gia_ManTranStochGet( pNtk );
Abc_NtkDelete( pNtk );
Vec_PtrPush( vpStarts, pNew );
}
}
if ( fSingle ) {
pBest = (Gia_Man_t *)Vec_PtrEntry( vpStarts, 0 );
for ( i = 1; i < Vec_PtrSize( vpStarts ); i++ ) {
pStart = (Gia_Man_t *)Vec_PtrEntry( vpStarts, i );
if ( Gia_ManAndNum( pStart ) < Gia_ManAndNum( pBest ) ) {
Gia_ManStop( pBest );
pBest = pStart;
j = i;
} else {
Gia_ManStop( pStart );
}
}
Vec_PtrClear( vpStarts );
Vec_PtrPush( vpStarts, pBest );
}
// optimize
pBest = Gia_ManDup( pGia );
if ( nThreads == 1 ) {
Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, i ) {
if ( p->nVerbose )
printf( "*begin starting point %d: #nodes = %5d\n", i + j, Gia_ManAndNum( pStart ) );
p->pStart = pStart;
pNew = Gia_ManTranStochOpt3( p );
if ( p->nVerbose )
printf( "*end starting point %d: #nodes = %5d\n", i + j, Gia_ManAndNum( pNew ) );
if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( pNew ) ) {
Gia_ManStop( pBest );
pBest = pNew;
} else {
Gia_ManStop( pNew );
}
Gia_ManStop( pStart );
}
} else {
#ifdef ABC_USE_PTHREADS
static pthread_mutex_t mutex;
int k, status, nIte, fAssigned, fWorking;
Gia_ManTranStochParam ThData[100];
pthread_t WorkerThread[100];
p->pRes = NULL;
p->mutex = &mutex;
if ( p->nVerbose )
p->nVerbose--;
for ( i = 0; i < nThreads; i++ ) {
ThData[i] = *p;
status = pthread_create( WorkerThread + i, NULL, Gia_ManTranStochWorkerThread, (void *)(ThData + i) );
assert( status == 0 );
}
Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, k ) {
for ( nIte = 0; nIte <= p->nRestarts; nIte++ ) {
fAssigned = 0;
while ( !fAssigned ) {
for ( i = 0; i < nThreads; i++ ) {
if ( ThData[i].fWorking )
continue;
if ( ThData[i].pRes != NULL ) {
if( nVerbose )
printf( "*sp %d res %4d : #nodes = %5d\n", ThData[i].nSp, ThData[i].nIte, Gia_ManAndNum( ThData[i].pRes ) );
if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( ThData[i].pRes ) ) {
Gia_ManStop( pBest );
pBest = ThData[i].pRes;
} else {
Gia_ManStop( ThData[i].pRes );
}
ThData[i].pRes = NULL;
}
ThData[i].nSp = j + k;
ThData[i].nIte = nIte;
ThData[i].pStart = pStart;
ThData[i].fWorking = 1;
fAssigned = 1;
break;
}
}
}
}
fWorking = 1;
while ( fWorking ) {
fWorking = 0;
for ( i = 0; i < nThreads; i++ ) {
if( ThData[i].fWorking ) {
fWorking = 1;
continue;
}
if ( ThData[i].pRes != NULL ) {
if( nVerbose )
printf( "*sp %d res %4d : #nodes = %5d\n", ThData[i].nSp, ThData[i].nIte, Gia_ManAndNum( ThData[i].pRes ) );
if ( Gia_ManAndNum( pBest ) > Gia_ManAndNum( ThData[i].pRes ) ) {
Gia_ManStop( pBest );
pBest = ThData[i].pRes;
} else {
Gia_ManStop( ThData[i].pRes );
}
ThData[i].pRes = NULL;
}
}
}
for ( i = 0; i < nThreads; i++ ) {
ThData[i].pStart = NULL;
ThData[i].fWorking = 1;
}
#else
printf( "ERROR: pthread is off" );
#endif
Vec_PtrForEachEntry( Gia_Man_t *, vpStarts, pStart, i )
Gia_ManStop( pStart );
}
if ( nVerbose )
printf( "best: %d\n", Gia_ManAndNum( pBest ) );
Vec_PtrFree( vpStarts );
return pBest;
}
ABC_NAMESPACE_IMPL_END

166
src/aig/gia/giaTransduction.cpp Normal file
View File

@ -0,0 +1,166 @@
/**CFile****************************************************************
FileName [giaTransduction.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Implementation of transduction method.]
Author [Yukio Miyasaka]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 2023.]
Revision [$Id: giaTransduction.c,v 1.00 2023/05/10 00:00:00 Exp $]
***********************************************************************/
#ifndef _WIN32
#ifdef _WIN32
#ifndef __MINGW32__
#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information
#endif
#endif
#include "giaTransduction.h"
#include "giaNewBdd.h"
#include "giaNewTt.h"
ABC_NAMESPACE_IMPL_START
Gia_Man_t *Gia_ManTransductionBdd(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose) {
if(nRandom) {
srand(nRandom);
nSortType = rand() % 4;
nPiShuffle = rand();
nParameter = rand() % 16;
}
NewBdd::Param p;
Transduction::Transduction<NewBdd::Man, NewBdd::Param, NewBdd::lit, 0xffffffff> t(pGia, nVerbose, fNewLine, nSortType, nPiShuffle, fLevel, pExdc, p);
int count = t.CountWires();
switch(nType) {
case 0:
count -= fMspf? t.Mspf(): t.Cspf();
break;
case 1:
count -= t.Resub(fMspf);
break;
case 2:
count -= t.ResubMono(fMspf);
break;
case 3:
count -= t.ResubShared(fMspf);
break;
case 4:
count -= t.RepeatResub(false, fMspf);
break;
case 5:
count -= t.RepeatResub(true, fMspf);
break;
case 6: {
bool fInner = (nParameter / 4) % 2;
count -= t.RepeatInner(fMspf, fInner);
break;
}
case 7: {
bool fInner = (nParameter / 4) % 2;
bool fOuter = (nParameter / 8) % 2;
count -= t.RepeatOuter(fMspf, fInner, fOuter);
break;
}
case 8: {
bool fFirstMerge = nParameter % 2;
bool fMspfMerge = fMspf? (nParameter / 2) % 2: false;
bool fInner = (nParameter / 4) % 2;
bool fOuter = (nParameter / 8) % 2;
count -= t.RepeatAll(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter);
break;
}
default:
std::cout << "Unknown transduction type " << nType << std::endl;
}
assert(t.Verify());
assert(count == t.CountWires());
return t.GenerateAig();
}
Gia_Man_t *Gia_ManTransductionTt(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose) {
if(nRandom) {
srand(nRandom);
nSortType = rand() % 4;
nPiShuffle = rand();
nParameter = rand() % 16;
}
NewTt::Param p;
Transduction::Transduction<NewTt::Man, NewTt::Param, NewTt::lit, 0xffffffff> t(pGia, nVerbose, fNewLine, nSortType, nPiShuffle, fLevel, pExdc, p);
int count = t.CountWires();
switch(nType) {
case 0:
count -= fMspf? t.Mspf(): t.Cspf();
break;
case 1:
count -= t.Resub(fMspf);
break;
case 2:
count -= t.ResubMono(fMspf);
break;
case 3:
count -= t.ResubShared(fMspf);
break;
case 4:
count -= t.RepeatResub(false, fMspf);
break;
case 5:
count -= t.RepeatResub(true, fMspf);
break;
case 6: {
bool fInner = (nParameter / 4) % 2;
count -= t.RepeatInner(fMspf, fInner);
break;
}
case 7: {
bool fInner = (nParameter / 4) % 2;
bool fOuter = (nParameter / 8) % 2;
count -= t.RepeatOuter(fMspf, fInner, fOuter);
break;
}
case 8: {
bool fFirstMerge = nParameter % 2;
bool fMspfMerge = fMspf? (nParameter / 2) % 2: false;
bool fInner = (nParameter / 4) % 2;
bool fOuter = (nParameter / 8) % 2;
count -= t.RepeatAll(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter);
break;
}
default:
std::cout << "Unknown transduction type " << nType << std::endl;
}
assert(t.Verify());
assert(count == t.CountWires());
return t.GenerateAig();
}
ABC_NAMESPACE_IMPL_END
#else
#include "gia.h"
ABC_NAMESPACE_IMPL_START
Gia_Man_t * Gia_ManTransductionBdd(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose)
{
return NULL;
}
Gia_Man_t * Gia_ManTransductionTt(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose)
{
return NULL;
}
ABC_NAMESPACE_IMPL_END
#endif

1768
src/aig/gia/giaTransduction.h Normal file
View File

File diff suppressed because it is too large Load Diff

2
src/aig/gia/module.make
View File

@ -103,6 +103,8 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaSwitch.c \
src/aig/gia/giaTim.c \
src/aig/gia/giaTis.c \
src/aig/gia/giaTransduction.cpp \
src/aig/gia/giaTranStoch.c \
src/aig/gia/giaTruth.c \
src/aig/gia/giaTsim.c \
src/aig/gia/giaTtopt.cpp \

4
src/aig/ivy/ivyShow.c
View File

@ -46,7 +46,7 @@ static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_
***********************************************************************/
void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
{
extern void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
static int Counter = 0;
char FileNameDot[200];
FILE * pFile;
@ -63,7 +63,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
// generate the file
Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
/**Function*************************************************************

130
src/aig/miniaig/miniaig.h
View File

@ -103,6 +103,12 @@ static int Mini_AigNodeFanin1( Mini_Aig_t * p, int Id )
assert( p->pArray[2*Id+1] == MINI_AIG_NULL || p->pArray[2*Id+1] < 2*Id );
return p->pArray[2*Id+1];
}
static void Mini_AigFlipLastPo( Mini_Aig_t * p )
{
assert( p->pArray[p->nSize-1] == MINI_AIG_NULL );
assert( p->pArray[p->nSize-2] != MINI_AIG_NULL );
p->pArray[p->nSize-2] ^= 1;
}
// working with variables and literals
static int Mini_AigVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
@ -156,6 +162,34 @@ static Mini_Aig_t * Mini_AigStartSupport( int nIns, int nObjsAlloc )
p->pArray[i] = MINI_AIG_NULL;
return p;
}
static Mini_Aig_t * Mini_AigStartArray( int nIns, int n0InAnds, int * p0InAnds, int nOuts, int * pOuts )
{
Mini_Aig_t * p; int i;
assert( 1+nIns <= n0InAnds );
p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
p->nCap = 2*(n0InAnds + nOuts);
p->nSize = 2*(n0InAnds + nOuts);
p->pArray = MINI_AIG_ALLOC( int, p->nCap );
for ( i = 0; i < 2*(1 + nIns); i++ )
p->pArray[i] = MINI_AIG_NULL;
memcpy( p->pArray + 2*(1 + nIns), p0InAnds + 2*(1 + nIns), 2*(n0InAnds - 1 - nIns)*sizeof(int) );
for ( i = 0; i < nOuts; i++ )
{
p->pArray[2*(n0InAnds + i)+0] = pOuts[i];
p->pArray[2*(n0InAnds + i)+1] = MINI_AIG_NULL;
}
return p;
}
static Mini_Aig_t * Mini_AigDup( Mini_Aig_t * p )
{
Mini_Aig_t * pNew;
pNew = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
pNew->nCap = p->nCap;
pNew->nSize = p->nSize;
pNew->pArray = MINI_AIG_ALLOC( int, p->nSize );
memcpy( pNew->pArray, p->pArray, p->nSize * sizeof(int) );
return pNew;
}
static void Mini_AigStop( Mini_Aig_t * p )
{
MINI_AIG_FREE( p->pArray );
@ -346,6 +380,32 @@ static int Mini_AigMuxMulti_rec( Mini_Aig_t * p, int * pCtrl, int * pData, int n
Res1 = Mini_AigMuxMulti_rec( p, pCtrl+1, pData+nData/2, nData/2 );
return Mini_AigMux( p, pCtrl[0], Res1, Res0 );
}
static Mini_Aig_t * Mini_AigTransformXor( Mini_Aig_t * p )
{
Mini_Aig_t * pNew = Mini_AigStart();
int i, * pCopy = MINI_AIG_ALLOC( int, Mini_AigNodeNum(p) );
Mini_AigForEachPi( p, i )
pCopy[i] = Mini_AigCreatePi(pNew);
Mini_AigForEachAnd( p, i )
{
int iLit0 = Mini_AigNodeFanin0(p, i);
int iLit1 = Mini_AigNodeFanin1(p, i);
iLit0 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit0)], Mini_AigLitIsCompl(iLit0) );
iLit1 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit1)], Mini_AigLitIsCompl(iLit1) );
if ( iLit0 <= iLit1 )
pCopy[i] = Mini_AigAnd( pNew, iLit0, iLit1 );
else
pCopy[i] = Mini_AigXor( pNew, iLit0, iLit1 );
}
Mini_AigForEachPo( p, i )
{
int iLit0 = Mini_AigNodeFanin0( p, i );
iLit0 = Mini_AigLitNotCond( pCopy[Mini_AigLit2Var(iLit0)], Mini_AigLitIsCompl(iLit0) );
pCopy[i] = Mini_AigCreatePo( pNew, iLit0 );
}
MINI_AIG_FREE( pCopy );
return pNew;
}
static unsigned s_MiniTruths5[5] = {
@ -501,6 +561,76 @@ static void Mini_AigDumpVerilog( char * pFileName, char * pModuleName, Mini_Aig_
fclose( pFile );
}
// procedure to dump MiniAIG into a BLIF file
static void Mini_AigDumpBlif( char * pFileName, char * pModuleName, Mini_Aig_t * p, int fVerbose )
{
int i, k, iFaninLit0, iFaninLit1;
char * pObjIsPi = MINI_AIG_FALLOC( char, Mini_AigNodeNum(p) );
FILE * pFile = fopen( pFileName, "wb" );
assert( Mini_AigPiNum(p) <= 26 );
if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); MINI_AIG_FREE( pObjIsPi ); return; }
// write interface
//fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() );
fprintf( pFile, ".model %s\n", pModuleName );
if ( Mini_AigPiNum(p) )
{
k = 0;
fprintf( pFile, ".inputs" );
Mini_AigForEachPi( p, i )
{
pObjIsPi[i] = k;
fprintf( pFile, " %c", (char)('a'+k++) );
}
}
k = 0;
fprintf( pFile, "\n.outputs" );
Mini_AigForEachPo( p, i )
fprintf( pFile, " o%d", k++ );
fprintf( pFile, "\n\n" );
// write LUTs
Mini_AigForEachAnd( p, i )
{
iFaninLit0 = Mini_AigNodeFanin0( p, i );
iFaninLit1 = Mini_AigNodeFanin1( p, i );
fprintf( pFile, ".names" );
if ( pObjIsPi[iFaninLit0 >> 1] >= 0 )
fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit0 >> 1]) );
else
fprintf( pFile, " n%d", iFaninLit0 >> 1 );
if ( pObjIsPi[iFaninLit1 >> 1] >= 0 )
fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit1 >> 1]) );
else
fprintf( pFile, " n%d", iFaninLit1 >> 1 );
fprintf( pFile, " n%d\n", i );
if ( iFaninLit0 < iFaninLit1 )
fprintf( pFile, "%d%d 1\n", !(iFaninLit0 & 1), !(iFaninLit1 & 1) );
else if ( !(iFaninLit0 & 1) == !(iFaninLit1 & 1) )
fprintf( pFile, "10 1\n01 1\n" );
else
fprintf( pFile, "00 1\n11 1\n" );
}
// write assigns
fprintf( pFile, "\n" );
k = 0;
Mini_AigForEachPo( p, i )
{
iFaninLit0 = Mini_AigNodeFanin0( p, i );
fprintf( pFile, ".names" );
if ( pObjIsPi[iFaninLit0 >> 1] >= 0 )
fprintf( pFile, " %c", (char)('a'+pObjIsPi[iFaninLit0 >> 1]) );
else
fprintf( pFile, " n%d", iFaninLit0 >> 1 );
fprintf( pFile, " o%d\n", k++ );
fprintf( pFile, "%d 1\n", !(iFaninLit0 & 1) );
}
fprintf( pFile, ".end\n\n" );
MINI_AIG_FREE( pObjIsPi );
fclose( pFile );
if ( fVerbose )
printf( "Written MiniAIG into the BLIF file \"%s\".\n", pFileName );
}
// checks if MiniAIG is normalized (first inputs, then internal nodes, then outputs)
static int Mini_AigIsNormalized( Mini_Aig_t * p )
{

12
src/aig/saig/saigIoa.c
View File

@ -45,17 +45,17 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
{
static char Buffer[16];
static char Buffer[1000];
if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
sprintf( Buffer, "n%0*d", (unsigned char)Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
else if ( Saig_ObjIsPi(p, pObj) )
sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
sprintf( Buffer, "pi%0*d", (unsigned char)Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
else if ( Saig_ObjIsPo(p, pObj) )
sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
sprintf( Buffer, "po%0*d", (unsigned char)Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
else if ( Saig_ObjIsLo(p, pObj) )
sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
sprintf( Buffer, "lo%0*d", (unsigned char)Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
else if ( Saig_ObjIsLi(p, pObj) )
sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
sprintf( Buffer, "li%0*d", (unsigned char)Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
else
assert( 0 );
return Buffer;

3
src/base/abc/abc.h
View File

@ -783,6 +783,7 @@ extern ABC_DLL void Abc_NtkAppendToCone( Abc_Ntk_t * pNtkNew, Abc_
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromRange( Abc_Ntk_t * pNtk );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNodes( Vec_Ptr_t * vSops );
extern ABC_DLL void Abc_NtkDelete( Abc_Ntk_t * pNtk );
@ -877,7 +878,7 @@ extern ABC_DLL void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_P
extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode );
extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode );
/*=== abcRefactor.c ==========================================================*/
extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
/*=== abcRewrite.c ==========================================================*/
extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
/*=== abcSat.c ==========================================================*/

37
src/base/abc/abcNtk.c
View File

@ -1229,6 +1229,41 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Creates the network composed of one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkCreateFromRange( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pNodeNew, * pNodePo;
Gia_Man_t * p = Abc_NtkClpGia( pNtk ); int i;
Vec_Str_t * vStr = Gia_ManComputeRange( p );
Gia_ManStop( p );
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtkNew->pName = Extra_UtilStrsav("range");
Abc_NtkForEachCo( pNtk, pObj, i )
Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
pNodeNew = Abc_NtkCreateObj( pNtkNew, ABC_OBJ_NODE );
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vStr) );
Vec_StrFree( vStr );
Abc_NtkForEachCi( pNtkNew, pObj, i )
Abc_ObjAddFanin( pNodeNew, pObj );
pNodePo = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pNodePo, pNodeNew );
Abc_ObjAssignName( pNodePo, "range", NULL );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkCreateFromNode(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Creates the network composed of one node with the given SOP.]
@ -1286,7 +1321,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNodes( Vec_Ptr_t * vSop )
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pFanin, * pNode, * pNodePo;
Vec_Ptr_t * vNames;
int i, k, nVars; char Buffer[10];
int i, k, nVars; char Buffer[100];
char * pSop = (char *)Vec_PtrEntry(vSop, 0);
// start the network
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );

22
src/base/abc/abcShow.c
View File

@ -40,7 +40,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
static void Abc_ShowGetFileName( char * pName, char * pBuffer );
////////////////////////////////////////////////////////////////////////
@ -71,7 +71,7 @@ void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc )
}
Cudd_DumpDot( dd, 1, (DdNode **)&bFunc, NULL, NULL, pFile );
fclose( pFile );
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
/**Function*************************************************************
@ -119,7 +119,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode, int fCompl )
fclose( pFile );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl, int fReorder )
{
@ -181,7 +181,7 @@ void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl, int fReorder )
Abc_NtkCleanCopy( pNtk );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
#else
@ -246,7 +246,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
Abc_NtkManCutStop( p );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
/**Function*************************************************************
@ -260,7 +260,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
SeeAlso []
***********************************************************************/
void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse )
void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse, int fKeepDot )
{
FILE * pFile;
Abc_Ntk_t * pNtk;
@ -307,7 +307,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse )
Vec_PtrFree( vNodes );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, fKeepDot );
Abc_NtkDelete( pNtk );
}
@ -323,7 +323,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse )
SeeAlso []
***********************************************************************/
void Abc_ShowFile( char * FileNameDot )
void Abc_ShowFile( char * FileNameDot, int fKeepDot )
{
FILE * pFile;
char * FileGeneric;
@ -390,7 +390,7 @@ void Abc_ShowFile( char * FileNameDot )
// spawn the viewer
#ifdef WIN32
_unlink( FileNameDot );
if ( !fKeepDot ) _unlink( FileNameDot );
if ( _spawnl( _P_NOWAIT, pGsNameWin, pGsNameWin, FileNamePs, NULL ) == -1 )
if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe",
"C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 )
@ -403,7 +403,7 @@ void Abc_ShowFile( char * FileNameDot )
#else
{
char CommandPs[1000];
unlink( FileNameDot );
if ( !fKeepDot ) unlink( FileNameDot );
sprintf( CommandPs, "%s %s &", pGsNameUnix, FileNamePs );
#if defined(__wasm)
if ( 1 )
@ -524,7 +524,7 @@ void Abc_NtkShowFlopDependency( Abc_Ntk_t * pNtk )
// write the DOT file
Abc_NtkWriteFlopDependency( pNtk, FileNameDot );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}

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

File diff suppressed because it is too large Load Diff

102
src/base/abci/abcIvy.c
View File

@ -25,6 +25,7 @@
#include "proof/fraig/fraig.h"
#include "map/mio/mio.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
@ -556,7 +557,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
//printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
//ABC_PRT( "Time", Abc_Clock() - clk );
}
@ -1141,6 +1142,105 @@ Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
return vArray;
}
/**Function*************************************************************
Synopsis [Convert Ivy into Gia.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Ivy_Obj_t * Gia_ObjChild0Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Ivy_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
static inline Ivy_Obj_t * Gia_ObjChild1Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Ivy_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
Ivy_Man_t * Gia_ManToIvySimple( Gia_Man_t * p )
{
Ivy_Man_t * pNew;
Gia_Obj_t * pObj; int i;
Ivy_Obj_t ** ppNodes = ABC_FALLOC( Ivy_Obj_t *, Gia_ManObjNum(p) );
// create the new manager
pNew = Ivy_ManStart();
// create the PIs
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
ppNodes[i] = Ivy_And( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, i), Gia_ObjChild1Copy3(ppNodes, pObj, i) );
else if ( Gia_ObjIsCi(pObj) )
ppNodes[i] = Ivy_ObjCreatePi( pNew );
else if ( Gia_ObjIsCo(pObj) )
ppNodes[i] = Ivy_ObjCreatePo( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, Gia_ObjId(p, pObj)) );
else if ( Gia_ObjIsConst0(pObj) )
ppNodes[i] = Ivy_Not(Ivy_ManConst1(pNew));
else
assert( 0 );
assert( i == 0 || Ivy_ObjId(ppNodes[i]) == i );
}
ABC_FREE( ppNodes );
return pNew;
}
static inline int Gia_ObjChild0Copy4( int * pNodes, Ivy_Obj_t * pObj ) { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin0)->Id], Ivy_IsComplement(pObj->pFanin0) ); }
static inline int Gia_ObjChild1Copy4( int * pNodes, Ivy_Obj_t * pObj ) { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin1)->Id], Ivy_IsComplement(pObj->pFanin1) ); }
Gia_Man_t * Gia_ManFromIvySimple( Ivy_Man_t * p )
{
Gia_Man_t * pNew;
Ivy_Obj_t * pObj;
int i, * pNodes = ABC_FALLOC( int, Ivy_ManObjIdMax(p) + 1 );
pNew = Gia_ManStart( Ivy_ManObjIdMax(p) );
pNew->pName = Abc_UtilStrsav( "from_ivy" );
Ivy_ManForEachObj( p, pObj, i )
{
if ( Ivy_ObjIsAnd(pObj) )
pNodes[pObj->Id] = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy4(pNodes, pObj), Gia_ObjChild1Copy4(pNodes, pObj) );
else if ( Ivy_ObjIsCi(pObj) )
pNodes[pObj->Id] = Gia_ManAppendCi( pNew );
else if ( Ivy_ObjIsCo(pObj) )
pNodes[pObj->Id] = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy4(pNodes, pObj) );
else if ( Ivy_ObjIsConst1(pObj) )
pNodes[pObj->Id] = 1;
else
assert( 0 );
}
ABC_FREE( pNodes );
return pNew;
}
Gia_Man_t * Gia_ManIvyFraig( Gia_Man_t * p, int nConfLimit, int fUseProve, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Gia_Man_t * pNew;
Ivy_Man_t * pMan, * pTemp;
pMan = Gia_ManToIvySimple( p );
if ( pMan == NULL )
return NULL;
Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose;
pParams->fProve = fUseProve;
pParams->fDoSparse = 1;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
pNew = Gia_ManFromIvySimple( pMan );
if ( pMan->pData )
{
p->pCexSeq = Abc_CexDeriveFromCombModel( (int *)pMan->pData, Ivy_ManPiNum(pMan), 0, -1 );
p->pCexSeq->iPo = Gia_ManFindFailedPoCex( p, p->pCexSeq, 0 );
ABC_FREE( pMan->pData );
}
Ivy_ManStop( pTemp );
Ivy_ManStop( pMan );
return pNew;
}
Gia_Man_t * Gia_ManIvyFraigTest( Gia_Man_t * p, int nConfLimit, int fVerbose )
{
Ivy_Man_t * pMan = Gia_ManToIvySimple( p );
Gia_Man_t * pNew = Gia_ManFromIvySimple( pMan );
Ivy_ManStop( pMan );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -100,6 +100,8 @@ Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnT
Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter );
Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
}
Abc_NtkForEachCo( pNtk, pObj, i )
Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter++ );
*pnTotal = Counter;
return vStarts;
}
@ -167,6 +169,8 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
if ( Abc_ObjFaninNum(pObj) <= 6 )
{
word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
int Offset = Vec_IntEntry( vStarts, pObj->iTemp );
Vec_WrdWriteEntry( vTruths2, Offset, uTruth );
Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
if ( uTruth == 0 || ~uTruth == 0 )
continue;
@ -177,6 +181,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
int Offset = Vec_IntEntry( vStarts, pObj->iTemp );
word * pRes = Vec_WrdEntryP( vTruths2, Offset );
Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes );
Vec_WrdWriteEntry( vTruths, pObj->iTemp, pRes[0] );
// check const0
for ( k = 0; k < nWords; k++ )
if ( pRes[k] )
@ -324,11 +329,13 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
}
// update fanins
vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
pNode->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), pTruth, vCover );
if ( Abc_SopGetVarNum((char *)pNode->pData) == 0 )
continue;
assert( Abc_SopGetVarNum((char *)pNode->pData) == Vec_IntSize(vArray) );
Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
}
Vec_IntFree( vCover );
Vec_IntFree( vMap );

11
src/base/abci/abcOdc.c
View File

@ -44,12 +44,13 @@ struct Odc_Obj_t_
struct Odc_Man_t_
{
// dont'-care parameters
// don't-care parameters
int nVarsMax; // the max number of cut variables
int nLevels; // the number of ODC levels
int fVerbose; // the verbosiness flag
int fVeryVerbose;// the verbosiness flag to print per-node stats
int nPercCutoff; // cutoff percentage
int skipQuant;
// windowing
Abc_Obj_t * pNode; // the node for windowing
@ -177,6 +178,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
p->fVerbose = fVerbose;
p->fVeryVerbose = fVeryVerbose;
p->nPercCutoff = 10;
p->skipQuant = 0;
// windowing
p->vRoots = Vec_PtrAlloc( 128 );
@ -744,7 +746,10 @@ unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uM
// skip visited objects
pObj = Odc_Lit2Obj( p, Lit );
if ( Odc_ObjIsTravIdCurrent(p, pObj) )
{
p->skipQuant = 1;
return pObj->uData;
}
Odc_ObjSetTravIdCurrent(p, pObj);
// skip objects out of the cone
if ( (pObj->uMask & uMask) == 0 )
@ -764,6 +769,7 @@ unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uM
uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
uRes1 = Odc_And( p, uLit0, uLit1 );
// find the result
p->skipQuant = 0;
return pObj->uData = ((uRes1 << 16) | uRes0);
}
@ -783,6 +789,7 @@ int Abc_NtkDontCareQuantify( Odc_Man_t * p )
Odc_Lit_t uRes0, uRes1;
unsigned uData;
int i;
p->skipQuant = 0;
assert( p->iRoot < 0xffff );
assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
@ -790,6 +797,8 @@ int Abc_NtkDontCareQuantify( Odc_Man_t * p )
// compute the cofactors w.r.t. this variable
Odc_ManIncrementTravId( p );
uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
if ( p->skipQuant )
continue;
uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16), Odc_IsComplement(p->iRoot) );
// quantify this variable existentially

100
src/base/abci/abcPrint.c
View File

@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
abctime s_MappingTime = 0;
int s_MappingMem = 0;
abctime s_ResubTime = 0;
//abctime s_ResubTime = 0;
abctime s_ResynTime = 0;
////////////////////////////////////////////////////////////////////////
@ -1069,26 +1069,6 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_NodeMffcConeSuppPrint( pNode );
}
/**Function*************************************************************
Synopsis [Prints the factored form of one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
{
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsSopLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
Abc_NodePrintFactor( pFile, pNode, fUseRealNames );
}
/**Function*************************************************************
Synopsis [Prints the factored form of one node.]
@ -1128,8 +1108,86 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
Dec_GraphPrint( stdout, pGraph, (char **)NULL, Abc_ObjName(pNode) );
Dec_GraphFree( pGraph );
}
void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
{
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsSopLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
Abc_NodePrintFactor( pFile, pNode, fUseRealNames );
}
/**Function*************************************************************
Synopsis [Prints the SOPs of one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NodePrintSop( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
{
Vec_Ptr_t * vNamesIn = NULL;
char * pCube, * pCur, * pSop; int nVars;
if ( Abc_ObjIsCo(pNode) )
pNode = Abc_ObjFanin0(pNode);
if ( Abc_ObjIsPi(pNode) )
{
fprintf( pFile, "Skipping the PI node.\n" );
return;
}
if ( Abc_ObjIsLatch(pNode) )
{
fprintf( pFile, "Skipping the latch.\n" );
return;
}
assert( Abc_ObjIsNode(pNode) );
pSop = (char *)pNode->pData;
nVars = Abc_SopGetVarNum( pSop );
if ( nVars == 0 )
{
fprintf( pFile, "%s = ", Abc_ObjName(pNode) );
fprintf( pFile, "Constant %d", Abc_SopGetPhase(pSop) );
return;
}
if ( !Abc_SopGetPhase(pSop) )
fprintf( pFile, "!" );
fprintf( pFile, "%s = ", Abc_ObjName(pNode) );
if ( fUseRealNames )
vNamesIn = Abc_NodeGetFaninNames(pNode);
Abc_SopForEachCube( pSop, nVars, pCube )
{
if ( pCube != pSop )
fprintf( pFile, " +" );
if ( vNamesIn )
{
for ( pCur = pCube; *pCur != ' '; pCur++ )
if ( *pCur != '-' )
fprintf( pFile, " %s%s", *pCur == '0' ? "!" : "", (char *)Vec_PtrEntry(vNamesIn, pCur-pCube) );
}
else
{
for ( pCur = pCube; *pCur != ' '; pCur++ )
if ( *pCur != '-' )
fprintf( pFile, " %s%c", *pCur == '0' ? "!" : "", (char)('a' + pCur-pCube) );
}
}
fprintf( pFile, "\n" );
if ( vNamesIn )
Abc_NodeFreeNames( vNamesIn );
}
void Abc_NtkPrintSop( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
{
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsSopLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
Abc_NodePrintSop( pFile, pNode, fUseRealNames );
}
/**Function*************************************************************
Synopsis [Prints the level stats of the PO node.]

6
src/base/abci/abcProve.c
View File

@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
@ -151,7 +151,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
break;
if ( --Counter == 0 )
break;
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
break;
if ( --Counter == 0 )
@ -340,7 +340,7 @@ Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
return pNtk;
}

6
src/base/abci/abcQuant.c
View File

@ -51,14 +51,14 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
pNtk = *ppNtk;
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
if ( fMoreEffort )
{
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
@ -340,7 +340,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
// compute the network composed of the initial states
pNtkFront = Abc_NtkInitialState( pNtkRel );
pNtkReached = Abc_NtkDup( pNtkFront );
//Abc_NtkShow( pNtkReached, 0, 0, 0 );
//Abc_NtkShow( pNtkReached, 0, 0, 0, 0 );
// if ( fVerbose )
// printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );

9
src/base/abci/abcRefactor.c
View File

@ -149,7 +149,7 @@ int Abc_NodeConeIsConst1( word * pTruth, int nVars )
SeeAlso []
***********************************************************************/
Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int nMinSaved, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
{
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
int fVeryVerbose = 0;
@ -205,7 +205,8 @@ clk = Abc_Clock();
nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required );
p->timeEval += Abc_Clock() - clk;
// quit if there is no improvement
if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) )
//if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) )
if ( nNodesAdded == -1 || nNodesSaved - nNodesAdded < nMinSaved )
{
Dec_GraphFree( pFForm );
return NULL;
@ -323,7 +324,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
SeeAlso []
***********************************************************************/
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
{
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
@ -371,7 +372,7 @@ clk = Abc_Clock();
pManRef->timeCut += Abc_Clock() - clk;
// evaluate this cut
clk = Abc_Clock();
pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, nMinSaved, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
pManRef->timeRes += Abc_Clock() - clk;
if ( pFForm == NULL )
continue;

11
src/base/abci/abcResub.c
View File

@ -117,7 +117,7 @@ static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required );
static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax );
static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
extern abctime s_ResubTime;
//extern abctime s_ResubTime;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -134,7 +134,7 @@ extern abctime s_ResubTime;
SeeAlso []
***********************************************************************/
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
{
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
@ -214,6 +214,11 @@ clk = Abc_Clock();
pManRes->timeRes += Abc_Clock() - clk;
if ( pFForm == NULL )
continue;
if ( pManRes->nLastGain < nMinSaved )
{
Dec_GraphFree( pFForm );
continue;
}
pManRes->nTotalGain += pManRes->nLastGain;
/*
if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 )
@ -266,7 +271,7 @@ pManRes->timeTotal = Abc_Clock() - clkStart;
printf( "Abc_NtkRefactor: The network check has failed.\n" );
return 0;
}
s_ResubTime = Abc_Clock() - clkStart;
//s_ResubTime = Abc_Clock() - clkStart;
return 1;
}

32
src/base/abci/abcSat.c
View File

@ -22,6 +22,8 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#include "sat/bsat/satSolver.h"
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
@ -143,6 +145,36 @@ sat_solver_store_free( pSat );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkSolveGiaMiter( Gia_Man_t * p )
{
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
int RetValue = 0;
int * pResult = NULL;
Abc_Ntk_t * pNtk;
Aig_Man_t * pMan;
pMan = Gia_ManToAig( p, 0 );
pNtk = Abc_NtkFromAigPhase( pMan );
pNtk->pName = Extra_UtilStrsav(p->pName);
Aig_ManStop( pMan );
RetValue = Abc_NtkMiterSat( pNtk, 1000000, 0, 0, NULL, NULL );
if ( RetValue == 0 ) // sat
pResult = pNtk->pModel, pNtk->pModel = NULL;
Abc_NtkDelete( pNtk );
return pResult;
}
/**Function*************************************************************
Synopsis [Returns the array of CI IDs.]

3
src/base/abci/abcSaucy.c
View File

@ -2650,7 +2650,8 @@ saucy_alloc(Abc_Ntk_t * pNtk)
if (s->ninduce && s->sinduce && s->left.cfront && s->left.clen
&& s->right.cfront && s->right.clen
&& s->stuff && s->bucket && s->count && s->ccount
&& s->clist && s->nextnon-1 && s->prevnon
//&& s->clist && s->nextnon-1 && s->prevnon
&& s->clist && s->nextnon[-1] && s->prevnon
&& s->start && s->gamma && s->theta && s->left.unlab
&& s->right.lab && s->right.unlab
&& s->left.lab && s->splitvar && s->splitwho && s->junk

30
src/base/abci/abcScorr.c
View File

@ -444,6 +444,36 @@ Abc_Ntk_t * Abc_NtkTestScorr( char * pFileNameIn, char * pFileNameOut, int nStep
return pResult;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pCorPars )
{
Gia_Man_t * pRes = NULL;
Aig_Man_t * pOld, * pNew;
Ssw_Pars_t SswPars, * pSswPars = &SswPars;
Ssw_ManSetDefaultParams( pSswPars );
pSswPars->nBTLimit = pCorPars->nBTLimit;
pSswPars->nFramesK = pCorPars->nFrames;
pSswPars->fLatchCorr = pCorPars->fLatchCorr;
pSswPars->fVerbose = pCorPars->fVerbose;
pOld = Gia_ManToAigSimple( p );
pNew = Ssw_SignalCorrespondence( pOld, pSswPars );
pRes = Gia_ManFromAigSimple( pNew );
Gia_ManReprFromAigRepr( pOld, p );
Aig_ManStop( pOld );
Aig_ManStop( pNew );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

4
src/base/cmd/cmdLoad.c
View File

@ -58,8 +58,8 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
// check if there is the binary
if ( (pFile = fopen( Vec_StrArray(vCommand), "r" )) == NULL )
{
Vec_StrFree( vCommand );
Abc_Print( -1, "Cannot run the binary \"%s\".\n\n", Vec_StrArray(vCommand) );
Vec_StrFree( vCommand );
return 1;
}
fclose( pFile );
@ -74,9 +74,9 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
// run the command line
if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
{
Vec_StrFree( vCommand );
Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
Vec_StrFree( vCommand );
return 1;
}
Vec_StrFree( vCommand );

65
src/base/io/io.c
View File

@ -66,6 +66,7 @@ static int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteEdgelist( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv );
@ -147,6 +148,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_edgelist",IoCommandWriteEdgelist, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
// Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
@ -3169,6 +3171,69 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteEdgelist( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int c, fSpecial = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
{
switch ( c )
{
case 'N':
fSpecial ^= 1;
break;
/*
case 'a':
fUseHie ^= 1;
break;
case 'h':
goto usage;
*/
default:
goto usage;
}
}
if ( pAbc->pNtkCur == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
if ( fSpecial ) // keep original naming
Io_WriteEdgelist( pAbc->pNtkCur, pFileName, 1, 0, 0, fSpecial); //last option is fName
else
Io_WriteEdgelist( pAbc->pNtkCur, pFileName, 1, 0, 0, fSpecial); //last option is fName
return 0;
usage:
fprintf( pAbc->Err, "usage: write_edgelist [-N] <file>\n" );
fprintf( pAbc->Err, "\t writes the network into edgelist file\n" );
fprintf( pAbc->Err, "\t part of Verilog-2-PyG (PyTorch Geometric). more details https://github.com/ycunxi/Verilog-to-PyG \n" );
fprintf( pAbc->Err, "\t-N : toggle keeping original naming of the netlist in edgelist (default=False)\n");
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .el)\n" );
return 1;
}
/**Function*************************************************************
Synopsis []

2
src/base/io/ioAbc.h
View File

@ -125,6 +125,8 @@ extern void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes,
extern void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse );
/*=== abcWriteEqn.c ===========================================================*/
extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteEdgelist.c ===========================================================*/
extern void Io_WriteEdgelist( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches, int fBb2Wb, int fSeq , int fName);
/*=== abcWriteGml.c ===========================================================*/
extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteList.c ==========================================================*/

9
src/base/io/ioReadPla.c
View File

@ -370,10 +370,11 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, in
Abc_Ntk_t * pNtk;
Abc_Obj_t * pTermPi, * pTermPo, * pNode;
Vec_Str_t ** ppSops = NULL;
char Buffer[100];
char Buffer[1000];
int nInputs = -1, nOutputs = -1, nProducts = -1;
char * pCubeIn, * pCubeOut;
int i, k, iLine, nDigits, nCubes;
int i, k, iLine, nCubes;
unsigned char nDigits;
// allocate the empty network
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
@ -445,7 +446,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, in
ABC_FREE( ppSops );
return NULL;
}
nDigits = Abc_Base10Log( nInputs );
nDigits = (unsigned char)Abc_Base10Log( nInputs );
for ( i = 0; i < nInputs; i++ )
{
sprintf( Buffer, "x%0*d", nDigits, i );
@ -462,7 +463,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, in
ABC_FREE( ppSops );
return NULL;
}
nDigits = Abc_Base10Log( nOutputs );
nDigits = (unsigned char)Abc_Base10Log( nOutputs );
for ( i = 0; i < nOutputs; i++ )
{
sprintf( Buffer, "z%0*d", nDigits, i );

1252
src/base/io/ioWriteEdgelist.c Normal file
View File

File diff suppressed because it is too large Load Diff

15
src/base/io/ioWriteVerilog.c
View File

@ -557,9 +557,23 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
}
else
{
Vec_Int_t * vMap = Vec_IntStartFull( 2*Abc_NtkObjNumMax(pNtk) );
vLevels = Vec_VecAlloc( 10 );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( Abc_ObjFaninNum(pObj) == 1 || Abc_ObjIsCo(Abc_ObjFanout0(Abc_ObjFanout0(pObj))) )
{
int iLit = Abc_Var2Lit( Abc_ObjId( Abc_ObjFanin0(Abc_ObjFanin0(pObj)) ), Abc_NodeIsInv(pObj) );
int iObj = Vec_IntEntry( vMap, iLit );
if ( iObj == -1 )
Vec_IntWriteEntry( vMap, iLit, Abc_ObjId(Abc_ObjFanout0(pObj)) );
else
{
fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
fprintf( pFile, "%s;\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_NtkObj(pNtk, iObj))) );
continue;
}
}
pFunc = (Hop_Obj_t *)pObj->pData;
fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
// set the input names
@ -581,6 +595,7 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
ABC_FREE( Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData );
}
Vec_VecFree( vLevels );
Vec_IntFree( vMap );
}
}

1
src/base/io/module.make
View File

@ -24,6 +24,7 @@ SRC += src/base/io/io.c \
src/base/io/ioWriteCnf.c \
src/base/io/ioWriteDot.c \
src/base/io/ioWriteEqn.c \
src/base/io/ioWriteEdgelist.c \
src/base/io/ioWriteGml.c \
src/base/io/ioWriteList.c \
src/base/io/ioWritePla.c \

19
src/base/main/libSupport.c
View File

@ -61,7 +61,7 @@ void open_libs() {
DIR* dirp;
struct dirent* dp;
char *env, *init_p, *p;
int done;
//int done;
env = getenv ("ABC_LIB_PATH");
if (env == NULL) {
@ -74,12 +74,14 @@ void open_libs() {
}
// Extract directories and read libraries
done = 0;
//done = 0;
p = init_p;
while (!done) {
//while (!done) {
for (;;) {
char *endp = strchr (p,':');
if (endp == NULL) done = 1; // last directory in the list
else *endp = 0; // end of string
//if (endp == NULL) done = 1; // last directory in the list
//else *endp = 0; // end of string
if (endp != NULL) *endp = 0; // end of string
dirp = opendir(p);
if (dirp == NULL) {
@ -119,7 +121,12 @@ void open_libs() {
}
}
closedir(dirp);
p = endp+1;
//p = endp+1;
if (endp == NULL) {
break; // last directory in the list
} else {
p = endp+1;
}
}
ABC_FREE(init_p);

2
src/base/main/mainUtils.c
View File

@ -261,7 +261,7 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
******************************************************************************/
char * DateReadFromDateString( char * datestr )
{
static char result[25];
static char result[100];
char day[10];
char month[10];
char zone[10];

75
src/base/wlc/wlc.c
View File

@ -705,6 +705,81 @@ Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_PrintTernary( FILE * pFile, word * pFunc, word * pCare, int nBits )
{
int i;
for ( i = nBits-1; i >= 0; i-- )
if ( Abc_TtGetBit(pCare, i) )
fprintf( pFile, "%c", '0' + Abc_TtGetBit(pFunc, i) );
else
fprintf( pFile, "-" );
fprintf( pFile, "\n" );
}
void Wlc_AdderTreeGen( int n )
{
word Care[1<<10] = {0};
word Truth[8][1<<10] = {{0}};
int nIns = 0, pIns[16][2] = {{0}};
int i, k, x, Res, Mint, nMints = 1 << (n*n);
assert( n >= 2 && n <= 4 );
for ( x = 0; x < 2*n; x++ )
{
for ( i = 0; i < n; i++ )
for ( k = 0; k < n; k++ )
if ( i + k == x )
pIns[nIns][0] = i, pIns[nIns][1] = k, nIns++;
}
for ( x = 0; x < nIns; x++ )
printf( "(%d, %d) ", pIns[x][0], pIns[x][1] );
printf( "\n" );
for ( i = 0; i < (1<<n); i++ )
for ( k = 0; k < (1<<n); k++ )
{
Mint = 0;
for ( x = 0; x < nIns; x++ )
if ( ((i >> pIns[x][0]) & 1) && ((k >> pIns[x][1]) & 1) )
Mint |= 1 << x;
assert( Mint < (1<<16) );
Abc_TtSetBit( Care, Mint );
Res = i * k;
for ( x = 0; x < 2*n; x++ )
if ( (Res >> x) & 1 )
Abc_TtSetBit( Truth[x], Mint );
}
if ( n == 2 )
{
Care[0] = Abc_Tt6Stretch( Care[0], n*n );
for ( i = 0; i < 2*n; i++ )
Truth[i][0] = Abc_Tt6Stretch( Truth[i][0], n*n );
nMints = 64;
}
for ( x = 0; x < nMints; x++ )
printf( "%d", Abc_TtGetBit(Care, x) );
printf( "\n\n" );
for ( i = 0; i < 2*n; i++, printf( "\n" ) )
for ( x = 0; x < nMints; x++ )
printf( "%d", Abc_TtGetBit(Truth[i], x) );
if ( 1 )
{
FILE * pFile = fopen( "tadd.truth", "wb" );
for ( i = 0; i < 2*n; i++ )
Extra_PrintTernary( pFile, Truth[i], Care, nMints );
fclose( pFile );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -623,7 +623,7 @@ void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int n
ABC_FREE( pQuo );
}
// non-restoring divider
void Wlc_BlastDivider2( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
void Wlc_BlastDividerNR( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
{
int i, * pRes = Vec_IntArray(vRes);
int k, * pQuo = ABC_ALLOC( int, nNum );
@ -653,7 +653,14 @@ void Wlc_BlastDivider2( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int
}
ABC_FREE( pQuo );
}
void Wlc_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
void Wlc_BlastDividerTop( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest )
{
if ( fNonRest )
Wlc_BlastDividerNR( pNew, pNum, nNum, pDiv, nDiv, fQuo, vRes );
else
Wlc_BlastDivider( pNew, pNum, nNum, pDiv, nDiv, fQuo, vRes );
}
void Wlc_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest )
{
Vec_Int_t * vNum = Vec_IntAlloc( nNum );
Vec_Int_t * vDiv = Vec_IntAlloc( nDiv );
@ -665,10 +672,10 @@ void Wlc_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv,
int k, iDiffSign = Gia_ManHashXor( pNew, pNum[nNum-1], pDiv[nDiv-1] );
Wlc_BlastMinus( pNew, pNum, nNum, vNum );
Wlc_BlastMinus( pNew, pDiv, nDiv, vDiv );
Wlc_BlastDivider( pNew, pNum, nNum, pDiv, nDiv, fQuo, vRes00 );
Wlc_BlastDivider( pNew, pNum, nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes01 );
Wlc_BlastDivider( pNew, Vec_IntArray(vNum), nNum, pDiv, nDiv, fQuo, vRes10 );
Wlc_BlastDivider( pNew, Vec_IntArray(vNum), nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes11 );
Wlc_BlastDividerTop( pNew, pNum, nNum, pDiv, nDiv, fQuo, vRes00, fNonRest );
Wlc_BlastDividerTop( pNew, pNum, nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes01, fNonRest );
Wlc_BlastDividerTop( pNew, Vec_IntArray(vNum), nNum, pDiv, nDiv, fQuo, vRes10, fNonRest );
Wlc_BlastDividerTop( pNew, Vec_IntArray(vNum), nNum, Vec_IntArray(vDiv), nDiv, fQuo, vRes11, fNonRest );
Vec_IntClear( vRes );
for ( k = 0; k < nNum; k++ )
{
@ -1124,13 +1131,14 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
int This = i == nArgA ? FillA : pArgA[i];
int Prev = i ? pArgA[i-1] : 0;
int Part = Gia_ManHashOr( pNew, Gia_ManHashAnd(pNew, One, This), Gia_ManHashAnd(pNew, Two, Prev) );
pp = Gia_ManHashXor( pNew, Part, Neg );
if ( pp == 0 || (fSigned && i == nArgA) )
continue;
Vec_WecPush( vProds, k+i, pp );
Vec_WecPush( vLevels, k+i, 0 );
if ( pp )
{
Vec_WecPush( vProds, k+i, pp );
Vec_WecPush( vLevels, k+i, 0 );
}
}
if ( fSigned ) i--;
// perform sign extension
@ -1143,13 +1151,19 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
Vec_WecPush( vProds, k+i+1, Sign );
Vec_WecPush( vLevels, k+i+1, 0 );
if ( Sign != 1 )
{
Vec_WecPush( vProds, k+i+2, Abc_LitNot(Sign) );
Vec_WecPush( vLevels, k+i+2, 0 );
}
}
else
{
if ( Sign != 1 )
{
Vec_WecPush( vProds, k+i, Abc_LitNot(Sign) );
Vec_WecPush( vLevels, k+i, 0 );
}
Vec_WecPush( vProds, k+i+1, 1 );
Vec_WecPush( vLevels, k+i+1, 0 );
@ -1817,9 +1831,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
if ( fSigned )
Wlc_BlastDividerSigned( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes );
Wlc_BlastDividerSigned( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes, pPar->fNonRest );
else
Wlc_BlastDivider( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes );
Wlc_BlastDividerTop( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes, pPar->fNonRest );
Vec_IntShrink( vRes, nRange );
if ( !pPar->fDivBy0 )
Wlc_BlastZeroCondition( pNew, pFans1, nRange1, vRes );

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

@ -1222,7 +1222,7 @@ usage:
Abc_Print( -2, "\t-o : toggle using additional POs on the word-level boundaries [default = %s]\n", pPar->fAddOutputs? "yes": "no" );
Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", pPar->fMulti? "yes": "no" );
Abc_Print( -2, "\t-b : toggle generating radix-4 Booth multipliers [default = %s]\n", pPar->fBooth? "yes": "no" );
Abc_Print( -2, "\t-q : toggle generating non-restoring square root [default = %s]\n", pPar->fNonRest? "yes": "no" );
Abc_Print( -2, "\t-q : toggle generating non-restoring square root and divider [default = %s]\n", pPar->fNonRest? "yes": "no" );
Abc_Print( -2, "\t-a : toggle generating carry-look-ahead adder [default = %s]\n", pPar->fCla? "yes": "no" );
Abc_Print( -2, "\t-y : toggle creating different divide-by-0 condition [default = %s]\n", pPar->fDivBy0? "yes": "no" );
Abc_Print( -2, "\t-d : toggle creating dual-output multi-output miter [default = %s]\n", pPar->fCreateMiter? "yes": "no" );

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

@ -367,7 +367,8 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
{
Ndr_Data_t * p = (Ndr_Data_t *)pData;
Wlc_Obj_t * pObj; Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 );
int Mod = 2, i, k, Obj, * pArray, nDigits, fFound, NameId, NameIdMax;
int Mod = 2, i, k, Obj, * pArray, fFound, NameId, NameIdMax;
unsigned char nDigits;
Vec_Wrd_t * vTruths = NULL; int nTruths[2] = {0};
Wlc_Ntk_t * pTemp, * pNtk = Wlc_NtkAlloc( "top", Ndr_DataObjNum(p, Mod)+1 );
Wlc_NtkCheckIntegrity( pData );
@ -488,11 +489,11 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
Vec_IntFree(vName2Obj);
// create fake object names
NameIdMax = Vec_IntFindMax(&pNtk->vNameIds);
nDigits = Abc_Base10Log( NameIdMax+1 );
nDigits = (unsigned char)Abc_Base10Log( NameIdMax+1 );
pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
for ( i = 1; i <= NameIdMax; i++ )
{
char pName[100]; sprintf( pName, "s%0*d", nDigits, i );
char pName[1000]; sprintf( pName, "s%0*d", nDigits, i );
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound && i == NameId );
}

6
src/base/wlc/wlcNtk.c
View File

@ -1292,10 +1292,10 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
void Wlc_NtkShortNames( Wlc_Ntk_t * p )
{
Wlc_Obj_t * pObj;
char pBuffer[100];
int nDigits, NameId, fFound, i;
char pBuffer[1000];
int NameId, fFound, i;
int nFlops = Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p);
nDigits = Abc_Base10Log( nFlops );
unsigned char nDigits = (unsigned char)Abc_Base10Log( nFlops );
Wlc_NtkForEachCo( p, pObj, i )
{
if ( Wlc_ObjIsPo(pObj) )

4
src/base/wlc/wlcShow.c
View File

@ -358,7 +358,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
***********************************************************************/
void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold )
{
extern void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
FILE * pFile;
char FileNameDot[200];
char * pName = Extra_FileDesignName(p->pName);
@ -377,7 +377,7 @@ void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold )
// generate the file
Wlc_NtkDumpDot( p, FileNameDot, vBold );
// visualize the file
Abc_ShowFile( FileNameDot );
Abc_ShowFile( FileNameDot, 0 );
}
////////////////////////////////////////////////////////////////////////

8
src/base/wln/wlnBlast.c
View File

@ -72,8 +72,8 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
extern void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
extern void Wlc_BlastZeroCondition( Gia_Man_t * pNew, int * pDiv, int nDiv, Vec_Int_t * vRes );
extern void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes );
extern void Wlc_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes );
extern void Wlc_BlastDividerTop( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest );
extern void Wlc_BlastDividerSigned( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest );
extern void Wlc_BlastPower( Gia_Man_t * pNew, int * pNum, int nNum, int * pExp, int nExp, Vec_Int_t * vTemp, Vec_Int_t * vRes );
int k, iLit, iLit0, iLit1;
@ -321,9 +321,9 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
int fDivBy0 = 1; // correct with 1
int fSigned = fSign0 && fSign1;
if ( fSigned )
Wlc_BlastDividerSigned( pNew, Vec_IntArray(vArg0), nRangeMax, Vec_IntArray(vArg1), nRangeMax, Type == ABC_OPER_ARI_DIV, vRes );
Wlc_BlastDividerSigned( pNew, Vec_IntArray(vArg0), nRangeMax, Vec_IntArray(vArg1), nRangeMax, Type == ABC_OPER_ARI_DIV, vRes, 0 );
else
Wlc_BlastDivider( pNew, Vec_IntArray(vArg0), nRangeMax, Vec_IntArray(vArg1), nRangeMax, Type == ABC_OPER_ARI_DIV, vRes );
Wlc_BlastDividerTop( pNew, Vec_IntArray(vArg0), nRangeMax, Vec_IntArray(vArg1), nRangeMax, Type == ABC_OPER_ARI_DIV, vRes, 0 );
Vec_IntShrink( vRes, nRange );
if ( !fDivBy0 )
Wlc_BlastZeroCondition( pNew, Vec_IntArray(vArg1), nRange, vRes );

2
src/base/wln/wlnNdr.c
View File

@ -256,7 +256,7 @@ Wln_Ntk_t * Wln_NtkFromNdr( void * pData, int fDump )
pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
for ( i = 1; i <= NameIdMax; i++ )
{
char pName[100]; sprintf( pName, "s%0*d", nDigits, i );
char pName[1000]; sprintf( pName, "s%0*d", (unsigned char)nDigits, i );
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound && i == NameId );
}

10
src/base/wln/wlnRead.c
View File

@ -576,7 +576,7 @@ void Rtl_NtkNormRanges( Rtl_Ntk_t * p )
int Offset = Rtl_WireOffset( p, Wire );
int First = Rtl_WireFirst( p, Wire );
assert( First >> 4 == NameId );
if ( Offset );
if ( Offset )
{
Left -= Offset;
Right -= Offset;
@ -1098,13 +1098,13 @@ void Rtl_NtkPrintWire( Rtl_Ntk_t * p, int * pWire )
void Rtl_NtkPrintCell( Rtl_Ntk_t * p, int * pCell )
{
int i, Par, Val;
Rtl_CellForEachAttr( p, pCell, Par, Val, i )
fprintf( Rtl_NtkFile(p), " attribute %s %s\n", Rtl_NtkStr(p, Par), Rtl_NtkStr(p, Val) );
Rtl_CellForEachAttr( p, pCell, Par, Val, i ) {
fprintf( Rtl_NtkFile(p), " attribute %s %s\n", Rtl_NtkStr(p, Par), Rtl_NtkStr(p, Val) ); }
fprintf( Rtl_NtkFile(p), " cell %s %s\n", Rtl_NtkStr(p, Rtl_CellType(pCell)), Rtl_NtkStr(p, pCell[1]) );
Rtl_CellForEachParam( p, pCell, Par, Val, i )
fprintf( Rtl_NtkFile(p), " parameter" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" );
Rtl_CellForEachConnect( p, pCell, Par, Val, i )
fprintf( Rtl_NtkFile(p), " connect" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" );
Rtl_CellForEachConnect( p, pCell, Par, Val, i ) {
fprintf( Rtl_NtkFile(p), " connect" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" ); }
fprintf( Rtl_NtkFile(p), " end\n" );
}
void Rtl_NtkPrintConnection( Rtl_Ntk_t * p, int * pCon )

21
src/base/wln/wlnRtl.c
View File

@ -147,13 +147,15 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p
int fSVlog = strstr(pFileName, ".sv") != NULL;
if ( strstr(pFileName, ".rtl") )
return Rtl_LibReadFile( pFileName, pFileName );
sprintf( Command, "%s -qp \"read_verilog %s %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
sprintf( Command, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
Wln_GetYosysName(),
pDefines ? pDefines : "",
fSVlog ? "-sv ":"", pFileName,
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileName,
pTopModule ? "-top " : "",
pTopModule ? pTopModule : "",
fCollapse ? "flatten; " : "",
fCollapse ? "flatten; ": "",
pFileTemp );
if ( fVerbose )
printf( "%s\n", Command );
@ -176,13 +178,14 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char *
char * pFileTemp = "_temp_.aig";
int fRtlil = strstr(pFileName, ".rtl") != NULL;
int fSVlog = strstr(pFileName, ".sv") != NULL;
sprintf( Command, "%s -qp \"%s %s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? " -sv ":" ",
pFileName,
pTopModule ? "-top " : "-auto-top",
fSVlog ? "-sv " : "",
pFileName,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
fTechMap ? "techmap; setundef -zero; " : "", pFileTemp );
if ( fVerbose )

2
src/bool/bdc/bdcSpfd.c
View File

@ -211,7 +211,7 @@ void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
vWeight = Vec_IntAlloc( 100 );
// initialize elementary variables
pNode = ABC_CALLOC( Bdc_Nod_t, nVars );
pNode = ABC_CALLOC( Bdc_Nod_t, (unsigned char)nVars );
for ( i = 0; i < nVars; i++ )
pNode[i].Truth = Truths[i];
for ( i = 0; i < nVars; i++ )

8
src/bool/kit/kit.h
View File

@ -175,10 +175,10 @@ static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
#define KIT_MAX(a,b) (((a) > (b))? (a) : (b))
#define KIT_INFINITY (100000000)
static inline int Kit_CubeHasLit( unsigned uCube, int i ) { return(uCube & (unsigned)(1<<i)) > 0; }
static inline unsigned Kit_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1<<i); }
static inline unsigned Kit_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1<<i); }
static inline unsigned Kit_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1<<i); }
static inline int Kit_CubeHasLit( unsigned uCube, int i ) { return(uCube & (unsigned)(1U<<i)) > 0; }
static inline unsigned Kit_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1U<<i); }
static inline unsigned Kit_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1U<<i); }
static inline unsigned Kit_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1U<<i); }
static inline int Kit_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall; }
static inline unsigned Kit_CubeSharp( unsigned uCube, unsigned uMask ) { return uCube & ~uMask; }

2
src/bool/kit/kitCloud.c
View File

@ -31,7 +31,7 @@ ABC_NAMESPACE_IMPL_START
typedef struct Kit_Mux_t_ Kit_Mux_t;
struct Kit_Mux_t_
{
unsigned v : 5; // variable
unsigned v : 6; // variable
unsigned t : 12; // then edge
unsigned e : 12; // else edge
unsigned c : 1; // complemented attr of else edge

2
src/bool/kit/kitHop.c
View File

@ -182,7 +182,7 @@ void Kit_IsopResubInt( Kit_Graph_t * pGraph, Vec_Int_t * vRes )
Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphVarInt(pGraph), Kit_GraphIsComplement(pGraph)) );
else
{
Kit_Node_t * pNode; int i;
Kit_Node_t * pNode = NULL; int i;
Kit_GraphForEachNode( pGraph, pNode, i )
{
Kit_Node_t * pFan0 = Kit_GraphNodeFanin0( pGraph, pNode );

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

@ -91,7 +91,7 @@ struct If_DsdMan_t_
Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function
int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules
int * pSched[IF_MAX_FUNC_LUTSIZE+1]; // grey code schedules
int nTtBits; // the number of truth table bits
int nConfigWords; // the number of words for config data per node
Vec_Wrd_t * vConfigs; // permutations

6
src/map/if/ifMan.c
View File

@ -97,9 +97,9 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->pPars->nLutSize, 8 * p->nTruth6Words[p->pPars->nLutSize], p->nCutBytes, p->nObjBytes, p->nSetBytes, p->pPars->fCutMin? "yes":"no" );
// room for temporary truth tables
p->puTemp[0] = p->pPars->fTruth? ABC_ALLOC( unsigned, 8 * p->nTruth6Words[p->pPars->nLutSize] ) : NULL;
p->puTemp[1] = p->puTemp[0] + p->nTruth6Words[p->pPars->nLutSize]*2;
p->puTemp[2] = p->puTemp[1] + p->nTruth6Words[p->pPars->nLutSize]*2;
p->puTemp[3] = p->puTemp[2] + p->nTruth6Words[p->pPars->nLutSize]*2;
p->puTemp[1] = p->pPars->fTruth? p->puTemp[0] + p->nTruth6Words[p->pPars->nLutSize]*2 : NULL;
p->puTemp[2] = p->pPars->fTruth? p->puTemp[1] + p->nTruth6Words[p->pPars->nLutSize]*2 : NULL;
p->puTemp[3] = p->pPars->fTruth? p->puTemp[2] + p->nTruth6Words[p->pPars->nLutSize]*2 : NULL;
p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words[p->pPars->nLutSize] ) : NULL;
if ( pPars->fUseDsd )
{

5
src/map/mapper/mapperLib.c
View File

@ -15,9 +15,12 @@
Revision [$Id: mapperLib.c,v 1.6 2005/01/23 06:59:44 alanmi Exp $]
***********************************************************************/
#define _BSD_SOURCE
//#define _BSD_SOURCE
#ifndef WIN32
#ifndef _DEFAULT_SOURCE
#define _DEFAULT_SOURCE
#endif
#include <unistd.h>
#endif

5
src/map/mio/mio.c
View File

@ -16,9 +16,12 @@
***********************************************************************/
#define _BSD_SOURCE
//#define _BSD_SOURCE
#ifndef WIN32
#ifndef _DEFAULT_SOURCE
#define _DEFAULT_SOURCE
#endif
#include <unistd.h>
#endif

2
src/map/mio/mioUtils.c
View File

@ -1711,7 +1711,7 @@ void Mio_LibraryShortNames( Mio_Library_t * pLib )
{
char Buffer[10000];
Mio_Gate_t * pGate; Mio_Pin_t * pPin;
int c = 0, i, nDigits = Abc_Base10Log( Mio_LibraryReadGateNum(pLib) );
int c = 0, i; unsigned char nDigits = (unsigned char)Abc_Base10Log( Mio_LibraryReadGateNum(pLib) );
// itereate through classes
Mio_LibraryForEachGate( pLib, pGate )
{

8
src/map/scl/sclLibUtil.c
View File

@ -197,11 +197,11 @@ void Abc_SclShortNames( SC_Lib * p )
char Buffer[10000];
SC_Cell * pClass, * pCell; SC_Pin * pPin;
int i, k, n, nClasses = Abc_SclLibClassNum(p);
int nDigits = Abc_Base10Log( nClasses );
unsigned char nDigits = (unsigned char)Abc_Base10Log( nClasses );
// itereate through classes
SC_LibForEachCellClass( p, pClass, i )
{
int nDigits2 = Abc_Base10Log( Abc_SclClassCellNum(pClass) );
unsigned char nDigits2 = (unsigned char)Abc_Base10Log( Abc_SclClassCellNum(pClass) );
SC_RingForEachCell( pClass, pCell, k )
{
ABC_FREE( pCell->pName );
@ -214,13 +214,13 @@ void Abc_SclShortNames( SC_Lib * p )
SC_CellForEachPinIn( pCell, pPin, n )
{
ABC_FREE( pPin->pName );
sprintf( Buffer, "%c", 'a'+n );
sprintf( Buffer, "%c", (char)('a'+n) );
pPin->pName = Abc_UtilStrsav( Buffer );
}
SC_CellForEachPinOut( pCell, pPin, n )
{
ABC_FREE( pPin->pName );
sprintf( Buffer, "%c", 'z'-n+pCell->n_inputs );
sprintf( Buffer, "%c", (char)('z'-n+pCell->n_inputs) );
pPin->pName = Abc_UtilStrsav( Buffer );
}
}

7
src/map/super/superGate.c
View File

@ -147,9 +147,12 @@ void Super_Precompute( Mio_Library_t * pLibGen, int nVarsMax, int nLevels, int n
return;
}
vStr = Super_PrecomputeStr( pLibGen, nVarsMax, nLevels, nGatesMax, tDelayMax, tAreaMax, TimeLimit, fSkipInv, fVerbose );
fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
if ( vStr )
{
fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
Vec_StrFree( vStr );
}
fclose( pFile );
Vec_StrFree( vStr );
// report the result of writing
if ( fVerbose )
{

10
src/misc/extra/extraUtilUtil.c
View File

@ -280,7 +280,7 @@ char * Extra_UtilFileSearch(char *file, char *path, char *mode)
save_path = path = Extra_UtilStrsav(path);
quit = 0;
do {
for (;;) {
cp = strchr(path, ':');
if (cp != 0) {
*cp = '\0';
@ -304,8 +304,12 @@ char * Extra_UtilFileSearch(char *file, char *path, char *mode)
return filename;
}
ABC_FREE(filename);
path = ++cp;
} while (! quit);
if (quit) {
break;
} else {
path = ++cp;
}
}
ABC_FREE(save_path);
return 0;

159
src/misc/util/utilTruth.h
View File

@ -162,24 +162,34 @@ static inline int Abc_TtBitCount16( int i ) { return Abc_TtBitCount8[i & 0xFF] +
***********************************************************************/
// read/write/flip i-th bit of a bit string table:
static inline int Abc_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (word)(i & 63)) & 1; }
static inline void Abc_TtSetBit( word * p, int i ) { p[i>>6] |= (word)(((word)1)<<(i & 63)); }
static inline void Abc_TtXorBit( word * p, int i ) { p[i>>6] ^= (word)(((word)1)<<(i & 63)); }
static inline int Abc_TtGetBit( word * p, int k ) { return (int)(p[k>>6] >> (k & 63)) & 1; }
static inline void Abc_TtSetBit( word * p, int k ) { p[k>>6] |= (((word)1)<<(k & 63)); }
static inline void Abc_TtXorBit( word * p, int k ) { p[k>>6] ^= (((word)1)<<(k & 63)); }
// read/write k-th digit d of a quaternary number:
static inline int Abc_TtGetQua( word * p, int k ) { return (int)(p[k>>5] >> (word)((k<<1) & 63)) & 3; }
static inline void Abc_TtSetQua( word * p, int k, int d ) { p[k>>5] |= (word)(((word)d)<<((k<<1) & 63)); }
static inline void Abc_TtXorQua( word * p, int k, int d ) { p[k>>5] ^= (word)(((word)d)<<((k<<1) & 63)); }
static inline int Abc_TtGetQua( word * p, int k ) { return (int)(p[k>>5] >> ((k<<1) & 63)) & 3; }
static inline void Abc_TtSetQua( word * p, int k, int d ) { p[k>>5] |= (((word)d)<<((k<<1) & 63)); }
static inline void Abc_TtXorQua( word * p, int k, int d ) { p[k>>5] ^= (((word)d)<<((k<<1) & 63)); }
// read/write k-th digit d of a hexadecimal number:
static inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> (word)((k<<2) & 63)) & 15; }
static inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (word)(((word)d)<<((k<<2) & 63)); }
static inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (word)(((word)d)<<((k<<2) & 63)); }
static inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15; }
static inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (((word)d)<<((k<<2) & 63)); }
static inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (((word)d)<<((k<<2) & 63)); }
// read/write k-th digit d of a 256-base number:
static inline int Abc_TtGet256( word * p, int k ) { return (int)(p[k>>3] >> (word)((k<<3) & 63)) & 255; }
static inline void Abc_TtSet256( word * p, int k, int d ) { p[k>>3] |= (word)(((word)d)<<((k<<3) & 63)); }
static inline void Abc_TtXor256( word * p, int k, int d ) { p[k>>3] ^= (word)(((word)d)<<((k<<3) & 63)); }
static inline int Abc_TtGet256( word * p, int k ) { return (int)(p[k>>3] >> ((k<<3) & 63)) & 255; }
static inline void Abc_TtSet256( word * p, int k, int d ) { p[k>>3] |= (((word)d)<<((k<<3) & 63)); }
static inline void Abc_TtXor256( word * p, int k, int d ) { p[k>>3] ^= (((word)d)<<((k<<3) & 63)); }
// read/write k-th digit d of a 2^16-base number:
static inline int Abc_TtGet65536( word * p, int k ) { return (int)(p[k>>2] >> ((k<<4) & 63))&0xFFFF; }
static inline void Abc_TtSet65536( word * p, int k, int d ) { p[k>>2] |= (((word)d)<<((k<<4) & 63)); }
static inline void Abc_TtXor65536( word * p, int k, int d ) { p[k>>2] ^= (((word)d)<<((k<<4) & 63)); }
// read/write k-th digit d of a 2^2^v-base number:
static inline int Abc_TtGetV( word * p, int v, int k ) { return (int)((p[k>>(6-v)] << (64-(1<<v)-((k<<v) & 63))) >> (64-(1<<v)));}
static inline void Abc_TtSetV( word * p, int v, int k, int d ) { p[k>>(6-v)] |= (((word)d)<<((k<<v) & 63)); }
static inline void Abc_TtXorV( word * p, int v, int k, int d ) { p[k>>(6-v)] ^= (((word)d)<<((k<<v) & 63)); }
/**Function*************************************************************
@ -664,6 +674,65 @@ static inline void Abc_TtIthVar( word * pOut, int iVar, int nVars )
pOut[k] = 0;
}
}
static inline void Abc_TtTruth2( word * pOut, word * pIn0, word * pIn1, int Truth, int nWords )
{
int w;
assert( Truth >= 0 && Truth <= 0xF );
switch ( Truth )
{
case 0x0 : for ( w = 0; w < nWords; w++ ) pOut[w] = 0; break; // 0000
case 0x1 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & ~pIn0[w]; break; // 0001
case 0x2 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & pIn0[w]; break; // 0010
case 0x3 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] ; break; // 0011
case 0x4 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & ~pIn0[w]; break; // 0100
case 0x5 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn0[w]; break; // 0101
case 0x6 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ pIn0[w]; break; // 0110
case 0x7 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | ~pIn0[w]; break; // 0111
case 0x8 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & pIn0[w]; break; // 1000
case 0x9 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ ~pIn0[w]; break; // 1001
case 0xA : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn0[w]; break; // 1010
case 0xB : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | pIn0[w]; break; // 1011
case 0xC : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ; break; // 1100
case 0xD : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | ~pIn0[w]; break; // 1101
case 0xE : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | pIn0[w]; break; // 1110
case 0xF : for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0; break; // 1111
default : assert( 0 );
}
}
static inline void Abc_TtTruth4( word Entry, word ** pNodes, word * pOut, int nWords, int fCompl )
{
unsigned First = (unsigned)Entry;
unsigned Second = (unsigned)(Entry >> 32);
int i, k = 5;
for ( i = 0; i < 4; i++ )
{
int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF;
if ( Pair == 0 )
break;
Lit0 = Pair & 0xF;
Lit1 = Pair >> 4;
assert( Lit0 != Lit1 );
if ( Lit0 < Lit1 )
Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords );
else
Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) );
}
for ( i = 0; i < 3; i++ )
{
int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF;
if ( Pair == 0 )
break;
Lit0 = Pair & 0x1F;
Lit1 = Pair >> 5;
assert( Lit0 != Lit1 );
if ( Lit0 < Lit1 )
Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords );
else
Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) );
}
assert( k > 5 );
Abc_TtCopy( pOut, pNodes[k-1], nWords, (int)(Entry >> 62) ^ fCompl );
}
/**Function*************************************************************
@ -1337,30 +1406,45 @@ static inline void Abc_TtPrintHex( word * pTruth, int nVars )
{
word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
int k;
assert( nVars >= 2 );
for ( pThis = pTruth; pThis < pLimit; pThis++ )
for ( k = 0; k < 16; k++ )
printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
if ( nVars < 2 )
printf( "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
else
{
assert( nVars >= 2 );
for ( pThis = pTruth; pThis < pLimit; pThis++ )
for ( k = 0; k < 16; k++ )
printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
}
printf( "\n" );
}
static inline void Abc_TtPrintHexRev( FILE * pFile, word * pTruth, int nVars )
{
word * pThis;
int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = StartK - 1; k >= 0; k-- )
fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
if ( nVars < 2 )
fprintf( pFile, "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
else
{
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = StartK - 1; k >= 0; k-- )
fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
}
// printf( "\n" );
}
static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
{
word * pThis;
int k;
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = 0; k < 16; k++ )
printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
if ( nVars < 2 )
printf( "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
else
{
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = 0; k < 16; k++ )
printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
}
printf( "\n" );
}
static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
@ -1368,10 +1452,15 @@ static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
word * pThis;
char * pStrInit = pStr;
int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = StartK - 1; k >= 0; k-- )
*pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
if ( nVars < 2 )
*pStr++ = Abc_TtPrintDigit((int)pTruth[0] & 15);
else
{
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
for ( k = StartK - 1; k >= 0; k-- )
*pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
}
return pStr - pStrInit;
}
static inline void Abc_TtPrintHexArrayRev( FILE * pFile, word * pTruth, int nDigits )
@ -1461,6 +1550,20 @@ static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
SeeAlso []
***********************************************************************/
static inline void Abc_TtPrintBits( word * pTruth, int nBits )
{
int k;
for ( k = 0; k < nBits; k++ )
printf( "%d", Abc_InfoHasBit( (unsigned *)pTruth, k ) );
printf( "\n" );
}
static inline void Abc_TtPrintBits2( word * pTruth, int nBits )
{
int k;
for ( k = nBits-1; k >= 0; k-- )
printf( "%d", Abc_InfoHasBit( (unsigned *)pTruth, k ) );
printf( "\n" );
}
static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
{
word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);

75
src/misc/vec/vecWrd.h
View File

@ -1217,6 +1217,36 @@ static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize )
return (Vec_Wrd_t *)vResInt;
}
/**Function*************************************************************
Synopsis [Returns the number of common entries.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_WrdTwoCountCommon( Vec_Wrd_t * vArr1, Vec_Wrd_t * vArr2 )
{
word * pBeg1 = vArr1->pArray;
word * pBeg2 = vArr2->pArray;
word * pEnd1 = vArr1->pArray + vArr1->nSize;
word * pEnd2 = vArr2->pArray + vArr2->nSize;
int Counter = 0;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( *pBeg1 == *pBeg2 )
pBeg1++, pBeg2++, Counter++;
else if ( *pBeg1 < *pBeg2 )
pBeg1++;
else
pBeg2++;
}
return Counter;
}
/**Function*************************************************************
Synopsis [Comparison procedure for two integers.]
@ -1284,7 +1314,46 @@ static inline void Vec_WrdAppend( Vec_Wrd_t * vVec1, Vec_Wrd_t * vVec2 )
SeeAlso []
***********************************************************************/
static inline void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords )
static inline void Vec_WrdDumpBoolOne( FILE * pFile, word * pSim, int nBits, int fReverse )
{
int k;
if ( fReverse )
for ( k = nBits-1; k >= 0; k-- )
fprintf( pFile, "%d", (int)((pSim[k/64] >> (k%64)) & 1) );
else
for ( k = 0; k < nBits; k++ )
fprintf( pFile, "%d", (int)((pSim[k/64] >> (k%64)) & 1) );
fprintf( pFile, "\n" );
}
static inline void Vec_WrdDumpBool( char * pFileName, Vec_Wrd_t * p, int nWords, int nBits, int fReverse, int fVerbose )
{
int i, nNodes = Vec_WrdSize(p) / nWords;
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return;
}
assert( Vec_WrdSize(p) % nWords == 0 );
for ( i = 0; i < nNodes; i++ )
Vec_WrdDumpBoolOne( pFile, Vec_WrdEntryP(p, i*nWords), nBits, fReverse );
fclose( pFile );
if ( fVerbose )
printf( "Written %d bits of simulation data for %d objects into file \"%s\".\n", nBits, Vec_WrdSize(p)/nWords, pFileName );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_WrdDumpHexOne( FILE * pFile, word * pSim, int nWords )
{
int k, Digit, nDigits = nWords*16;
for ( k = 0; k < nDigits; k++ )
@ -1302,7 +1371,7 @@ static inline void Vec_WrdPrintHex( Vec_Wrd_t * p, int nWords )
int i, nNodes = Vec_WrdSize(p) / nWords;
assert( Vec_WrdSize(p) % nWords == 0 );
for ( i = 0; i < nNodes; i++ )
Gia_ManSimPatWriteOne( stdout, Vec_WrdEntryP(p, i*nWords), nWords );
Vec_WrdDumpHexOne( stdout, Vec_WrdEntryP(p, i*nWords), nWords );
}
static inline void Vec_WrdDumpHex( char * pFileName, Vec_Wrd_t * p, int nWords, int fVerbose )
{
@ -1315,7 +1384,7 @@ static inline void Vec_WrdDumpHex( char * pFileName, Vec_Wrd_t * p, int nWords,
}
assert( Vec_WrdSize(p) % nWords == 0 );
for ( i = 0; i < nNodes; i++ )
Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(p, i*nWords), nWords );
Vec_WrdDumpHexOne( pFile, Vec_WrdEntryP(p, i*nWords), nWords );
fclose( pFile );
if ( fVerbose )
printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(p)/nWords, pFileName );

1
src/opt/dar/dar.h
View File

@ -46,6 +46,7 @@ struct Dar_RwrPar_t_
{
int nCutsMax; // the maximum number of cuts to try
int nSubgMax; // the maximum number of subgraphs to try
int nMinSaved; // the minumum number of nodes saved
int fFanout; // support fanout representation
int fUpdateLevel; // update level
int fUseZeros; // performs zero-cost replacement

4
src/opt/dar/darCore.c
View File

@ -53,6 +53,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
memset( pPars, 0, sizeof(Dar_RwrPar_t) );
pPars->nCutsMax = 8; // 8
pPars->nSubgMax = 5; // 5 is a "magic number"
pPars->nMinSaved = 1;
pPars->fFanout = 1;
pPars->fUpdateLevel = 0;
pPars->fUseZeros = 0;
@ -177,7 +178,8 @@ p->timeCuts += Abc_Clock() - clk;
pCut->nLeaves = nLeavesOld;
}
// check the best gain
if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
//if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
if ( p->GainBest < p->pPars->nMinSaved )
{
// Aig_ObjOrderAdvance( pAig );
continue;

3
src/opt/dar/darScript.c
View File

@ -849,6 +849,7 @@ pPars->timeSynth = Abc_Clock() - clk;
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
@ -873,6 +874,8 @@ pPars->timeSynth = Abc_Clock() - clk;
// perform choice computation
if ( pPars->fUseNew )
pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
else if ( pPars->fUseNew2 )
pMan = Cec_ComputeChoicesNew2( pGia, pPars->nBTLimit, pPars->fVerbose );
else if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else

2
src/opt/dau/dauMerge.c
View File

@ -48,7 +48,7 @@ typedef struct Dau_Sto_t_ Dau_Sto_t;
struct Dau_Sto_t_
{
int iVarUsed; // counter of used variables
char pOutput[DAU_MAX_STR]; // storage for reduced function
char pOutput[2*DAU_MAX_STR+10]; // storage for reduced function
char * pPosOutput; // place in the output
char pStore[DAU_MAX_VAR][DAU_MAX_STR]; // storage for definitions
char * pPosStore[DAU_MAX_VAR]; // place in the store

5
src/opt/sfm/sfmCnf.c
View File

@ -76,7 +76,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
{
if ( Truth == 0 || ~Truth == 0 )
{
//assert( nVars == 0 );
assert( nVars == 0 );
Vec_StrPush( vCnf, (char)(Truth == 0) );
Vec_StrPush( vCnf, (char)-1 );
return 1;
@ -92,6 +92,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
{
Vec_StrPush( vCnf, (char)1 );
Vec_StrPush( vCnf, (char)-1 );
assert( 0 );
return 1;
}
// const1
@ -102,6 +103,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
{
Vec_StrPush( vCnf, (char)0 );
Vec_StrPush( vCnf, (char)-1 );
assert( 0 );
return 1;
}
}
@ -196,6 +198,7 @@ void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap
Vec_Int_t * vClause;
signed char Entry;
int i, Lit;
assert( Vec_StrEntry(vCnf, 1) != -1 || Vec_IntSize(vFaninMap) == 1 );
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
Vec_StrForEachEntry( vCnf, Entry, i )

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

@ -115,6 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
int i, iFanin, iVar = -1;
int iFaninRem = -1, iFaninSkip = -1;
int nFanins = Sfm_ObjFaninNum(p, iNode);
word uTruth, uSign, uMask;
abctime clk;
assert( Sfm_ObjIsNode(p, iNode) );
@ -214,7 +215,12 @@ finish:
if ( fSkipUpdate )
return 0;
// update the network
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth, p->pTruth );
// the number of fanins cannot increase
assert( nFanins >= Sfm_ObjFaninNum(p, iNode) );
//printf( "Modifying node %d with %d fanins (resulting in %d fanins). ", iNode, nFanins, Sfm_ObjFaninNum(p, iNode) );
//Abc_TtPrintHexRev( stdout, p->pTruth, Sfm_ObjFaninNum(p, iNode) );
//printf( "\n" );
return 1;
}
@ -304,7 +310,7 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
return 1;
}
// try simplifying local functions
if ( p->pPars->fUseDcs )
if ( p->pPars->fUseDcs && Sfm_ObjFaninNum(p, iNode) <= 6 )
if ( Sfm_NodeResubOne( p, iNode ) )
return 1;
/*
@ -360,7 +366,7 @@ void Sfm_NtkPrint( Sfm_Ntk_t * p )
***********************************************************************/
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
int i, k, Counter = 0;
int i, k, Counter = 0, CounterLarge = 0;
//Sfm_NtkPrint( p );
p->timeTotal = Abc_Clock();
if ( pPars->fVerbose )
@ -382,8 +388,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
continue;
if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
continue;
if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
//if ( Sfm_ObjFaninNum(p, i) < 2 )
// continue;
if ( Sfm_ObjFaninNum(p, i) > SFM_SUPP_MAX )
{
CounterLarge++;
continue;
}
for ( k = 0; Sfm_NodeResub(p, i); k++ )
{
// Counter++;
@ -396,6 +407,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
p->timeTotal = Abc_Clock() - p->timeTotal;
if ( pPars->fVerbose && CounterLarge )
printf( "MFS skipped %d (out of %d) nodes with more than %d fanins.\n", CounterLarge, p->nNodes, SFM_SUPP_MAX );
if ( pPars->fVerbose )
Sfm_NtkPrintStats( p );
//Sfm_NtkPrint( p );

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

@ -39,6 +39,7 @@
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "base/abc/abc.h"
#include "misc/util/utilTruth.h"
#include "sfm.h"
////////////////////////////////////////////////////////////////////////
@ -47,7 +48,8 @@
ABC_NAMESPACE_HEADER_START
#define SFM_FANIN_MAX 6
#define SFM_FANIN_MAX 12
#define SFM_WORDS_MAX ((SFM_FANIN_MAX>6) ? (1<<(SFM_FANIN_MAX-6)) : 1)
#define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321
@ -123,6 +125,10 @@ struct Sfm_Ntk_t_
Vec_Int_t * vValues; // SAT variable values
Vec_Wec_t * vClauses; // CNF clauses for the node
Vec_Int_t * vFaninMap; // mapping fanins into their SAT vars
word TtElems[SFM_FANIN_MAX][SFM_WORDS_MAX];
word * pTtElems[SFM_FANIN_MAX];
word pTruth[SFM_WORDS_MAX];
word pCube[SFM_WORDS_MAX];
// nodes
int nTotalNodesBeg;
int nTotalEdgesBeg;
@ -216,7 +222,7 @@ extern int Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mi
/*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
extern void Sfm_NtkPrepare( Sfm_Ntk_t * p );
extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth );
/*=== sfmSat.c ==========================================================*/
extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p );

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

@ -166,7 +166,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
***********************************************************************/
Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
{
Sfm_Ntk_t * p;
Sfm_Ntk_t * p; int i;
Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
p = ABC_CALLOC( Sfm_Ntk_t, 1 );
p->nObjs = Vec_WecSize( vFanins );
@ -192,6 +192,10 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
Vec_IntFill( &p->vVar2Id, 2*p->nObjs, -1 );
p->vCover = Vec_IntAlloc( 1 << 16 );
p->vCnfs = Sfm_CreateCnf( p );
// elementary truth tables
for ( i = 0; i < SFM_FANIN_MAX; i++ )
p->pTtElems[i] = p->TtElems[i];
Abc_TtElemInit( p->pTtElems, SFM_FANIN_MAX );
return p;
}
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
@ -315,13 +319,14 @@ void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkUpdateLevelR_rec( p, iFanin );
}
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth )
{
int iFanin = Sfm_ObjFanin( p, iNode, f );
int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) - (int)(iFaninNew == -1) );
assert( Sfm_ObjIsNode(p, iNode) );
assert( iFanin != iFaninNew );
assert( Sfm_ObjFaninNum(p, iNode) <= 6 );
if ( uTruth == 0 || ~uTruth == 0 )
assert( Sfm_ObjFaninNum(p, iNode) <= SFM_FANIN_MAX );
if ( Abc_TtIsConst0(pTruth, nWords) || Abc_TtIsConst1(pTruth, nWords) )
{
Sfm_ObjForEachFanin( p, iNode, iFanin, f )
{
@ -346,7 +351,9 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
Sfm_NtkUpdateLevelR_rec( p, iFanin );
// update truth table
Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
if ( p->vTruths2 && Vec_WrdSize(p->vTruths2) )
Abc_TtCopy( Vec_WrdEntryP(p->vTruths2, Vec_IntEntry(p->vStarts, iNode)), pTruth, nWords, 0 );
Sfm_TruthToCnf( uTruth, pTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
}
/**Function*************************************************************

14
src/opt/sfm/sfmSat.c
View File

@ -153,13 +153,15 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
***********************************************************************/
word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
{
word * pSign, uCube, uTruth = 0;
word * pSign;
int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
int pLits[2], nVars = sat_solver_nvars( p->pSat );
int nWords = Abc_Truth6WordNum( Vec_IntSize(p->vDivIds) );
sat_solver_setnvars( p->pSat, nVars + 1 );
pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
assert( Vec_IntSize(p->vDivIds) <= 6 );
assert( Vec_IntSize(p->vDivIds) <= SFM_FANIN_MAX );
Abc_TtClear( p->pTruth, nWords );
while ( 1 )
{
// find onset minterm
@ -168,7 +170,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_False )
return uTruth;
return p->pTruth[0];
assert( status == l_True );
// remember variable values
Vec_IntClear( p->vValues );
@ -189,7 +191,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( p->pSat, &pFinal );
uCube = ~(word)0;
Abc_TtFill( p->pCube, nWords );
Vec_IntClear( p->vLits );
Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
for ( i = 0; i < nFinal; i++ )
@ -198,9 +200,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
continue;
Vec_IntPush( p->vLits, pFinal[i] );
iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
Abc_TtAndSharp( p->pCube, p->pCube, p->pTtElems[iVar], nWords, !Abc_LitIsCompl(pFinal[i]) );
}
uTruth |= uCube;
Abc_TtOr( p->pTruth, p->pTruth, p->pCube, nWords );
status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
assert( status );
nIter++;

11
src/proof/cec/cecChoice.c
View File

@ -422,6 +422,17 @@ Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
Gia_ManStop( pGia );
return pAig;
}
Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
extern Gia_Man_t * Cec5_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Aig_Man_t * pAig;
Gia_Man_t * pNew = Cec5_ManSimulateTest3( pGia, nConfs, fVerbose );
Gia_ManStop( pNew );
pGia = Gia_ManEquivToChoices( pGia, 3 );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

28
src/proof/cec/cecSatG2.c
View File

@ -875,7 +875,7 @@ static inline void Cec4_ObjSimCi( Gia_Man_t * p, int iObj )
int w;
word * pSim = Cec4_ObjSim( p, iObj );
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = Gia_ManRandomW( 0 );
pSim[w] = Abc_RandomW( 0 );
pSim[0] <<= 1;
}
static inline void Cec4_ObjClearSimCi( Gia_Man_t * p, int iObj )
@ -1729,6 +1729,27 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
pMan->timeResimLoc += Abc_Clock() - clk;
return NULL;
}
void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
{
int i, iObj, iPrev, Counter = 0;
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
{
Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
}
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
{
Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars );
@ -1743,7 +1764,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
assert( Gia_ObjId(p, pObj) == i+1 );
// check if any output trivially fails under all-0 pattern
Gia_ManRandom( 1 );
Abc_Random( 1 );
Gia_ManSetPhase( p );
if ( pPars->nLevelMax )
Gia_ManLevelNum(p);
@ -1864,6 +1885,9 @@ finalize:
Cec4_ManDestroy( pMan );
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );
if ( ppNew && *ppNew == NULL )
*ppNew = Gia_ManDup(p);
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )

6
src/proof/cec/cecSatG3.c
View File

@ -917,7 +917,7 @@ static inline void Cec5_ObjSimCi( Gia_Man_t * p, int iObj )
int w;
word * pSim = Cec5_ObjSim( p, iObj );
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = Gia_ManRandomW( 0 );
pSim[w] = Abc_RandomW( 0 );
pSim[0] <<= 1;
}
static inline void Cec5_ObjClearSimCi( Gia_Man_t * p, int iObj )
@ -1871,6 +1871,7 @@ void Cec5_ManExtend( Cec5_Man_t * pMan, CbsP_Man_t * pCbs ){
int Cec5_ManSweepNodeCbs( Cec5_Man_t * p, CbsP_Man_t * pCbs, int iObj, int iRepr, int fTagFail );
int Cec5_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly, int fCbs, int approxLim, int subBatchSz, int adaRecycle )
{
extern void Gia_ManRemoveWrongChoices( Gia_Man_t * p );
Gia_Obj_t * pObj, * pRepr;
CbsP_Man_t * pCbs = NULL;
int i, fSimulate = 1;
@ -1902,7 +1903,7 @@ int Cec5_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
assert( Gia_ObjId(p, pObj) == i+1 );
// check if any output trivially fails under all-0 pattern
Gia_ManRandom( 1 );
Abc_Random( 1 );
Gia_ManSetPhase( p );
if ( pPars->nLevelMax )
Gia_ManLevelNum(p);
@ -2119,6 +2120,7 @@ finalize:
CbsP_ManStop(pCbs);
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle )

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

@ -53,6 +53,7 @@ struct Dch_Pars_t_
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
int fUseNew; // uses new implementation
int fUseNew2; // uses new implementation
int fLightSynth; // uses lighter version of synthesis
int fSkipRedSupp; // skip choices with redundant support vars
int fVerbose; // verbose stats

2
src/proof/ssw/sswCore.c
View File

@ -444,6 +444,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// if parameters are not given, create them
if ( pPars == NULL )
Ssw_ManSetDefaultParams( pPars = &Pars );
/*
// consider the case of empty AIG
if ( Aig_ManNodeNum(pAig) == 0 )
{
@ -452,6 +453,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
return Aig_ManDupOrdered(pAig);
}
*/
// check and update parameters
if ( pPars->fLatchCorrOpt )
{

1021
src/sat/bmc/bmcMaj.c
View File

File diff suppressed because it is too large Load Diff

9
src/sat/bsat/satSolver.c
View File

@ -511,13 +511,14 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
{
int i, lev, minl = 0, lbd = 0;
for (i = 0; i < (int)c->size; i++)
unsigned int i, lev, minl = 0;
int lbd = 0;
for (i = 0; i < c->size; i++)
{
lev = var_level(s, lit_var(c->lits[i]));
if ( !(minl & (1 << (lev & 31))) )
if ( !(minl & (1U << (lev & 31))) )
{
minl |= 1 << (lev & 31);
minl |= 1U << (lev & 31);
lbd++;
// printf( "%d ", lev );
}

1
src/sat/cnf/cnf.h
View File

@ -160,6 +160,7 @@ extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec
extern void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits );
extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists );
extern void Cnf_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 );
extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
extern void * Cnf_DataWriteIntoSolverInt( void * pSat, Cnf_Dat_t * p, int nFrames, int fInit );
extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );

89
src/sat/cnf/cnfMan.c
View File

@ -303,6 +303,48 @@ void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Ve
gzprintf( pFile, "\n" );
gzclose( pFile );
}
void Cnf_DataWriteIntoFileInvGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 )
{
gzFile pFile;
int * pLit, * pStop, i, VarId;
pFile = gzopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
return;
}
gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
if ( vExists1 )
{
gzprintf( pFile, "e " );
Vec_IntForEachEntry( vExists1, VarId, i )
gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
gzprintf( pFile, "0\n" );
}
if ( vForAlls )
{
gzprintf( pFile, "a " );
Vec_IntForEachEntry( vForAlls, VarId, i )
gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
gzprintf( pFile, "0\n" );
}
if ( vExists2 )
{
gzprintf( pFile, "e " );
Vec_IntForEachEntry( vExists2, VarId, i )
gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
gzprintf( pFile, "0\n" );
}
for ( i = 0; i < p->nClauses; i++ )
{
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
gzprintf( pFile, "0\n" );
}
gzprintf( pFile, "\n" );
gzclose( pFile );
}
/**Function*************************************************************
@ -355,6 +397,53 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_
fprintf( pFile, "\n" );
fclose( pFile );
}
void Cnf_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 )
{
FILE * pFile;
int * pLit, * pStop, i, VarId;
if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
{
Cnf_DataWriteIntoFileInvGz( p, pFileName, fReadable, vExists1, vForAlls, vExists2 );
return;
}
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
return;
}
fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
if ( vExists1 )
{
fprintf( pFile, "e " );
Vec_IntForEachEntry( vExists1, VarId, i )
fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
fprintf( pFile, "0\n" );
}
if ( vForAlls )
{
fprintf( pFile, "a " );
Vec_IntForEachEntry( vForAlls, VarId, i )
fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
fprintf( pFile, "0\n" );
}
if ( vExists2 )
{
fprintf( pFile, "e " );
Vec_IntForEachEntry( vExists2, VarId, i )
fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
fprintf( pFile, "0\n" );
}
for ( i = 0; i < p->nClauses; i++ )
{
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
fprintf( pFile, "0\n" );
}
fprintf( pFile, "\n" );
fclose( pFile );
}
/**Function*************************************************************

2
src/sat/glucose/Vec.h
View File

@ -99,7 +99,7 @@ template<class T>
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
if (add > INT_MAX - cap || (((data = (T*)::realloc((void*)data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
#ifdef __wasm
abort();
#else

4
src/sat/glucose2/Vec.h
View File

@ -101,7 +101,7 @@ template<class T>
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
if (add > INT_MAX - cap || (((data = (T*)::realloc((void*)data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
#ifdef __wasm
abort();
#else
@ -112,7 +112,7 @@ void vec<T>::capacity(int min_cap) {
template<class T>
void vec<T>::prelocate(int ext_cap) {
if (cap >= ext_cap) return;
if (ext_cap > INT_MAX || (((data = (T*)::realloc(data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM))
if (ext_cap > INT_MAX || (((data = (T*)::realloc((void*)data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM))
#ifdef __wasm
abort();
#else