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

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

This commit is contained in:
Miodrag Milanovic 2022-11-09 08:42:08 +01:00
parent ab5b16ede2 70cb339f86
commit be9a35c036
32 changed files with 4121 additions and 87 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abcexe.dsp
View File

@ -88,10 +88,6 @@ LINK32=link.exe
# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
# Begin Source File
SOURCE=.\src\aig\gia\giaSif.c
# End Source File
# Begin Source File
SOURCE=.\src\base\main\main.c
# End Source File
# End Group

8
abclib.dsp
View File

@ -5191,6 +5191,10 @@ SOURCE=.\src\aig\gia\giaSatoko.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaSatSyn.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaScl.c
# End Source File
# Begin Source File
@ -5295,6 +5299,10 @@ SOURCE=.\src\aig\gia\giaTsim.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaTtopt.cpp
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaUnate.c
# End Source File
# Begin Source File

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

@ -527,18 +527,22 @@ static inline int Gia_ObjDiff1( Gia_Obj_t * pObj ) {
static inline int Gia_ObjFaninC0( Gia_Obj_t * pObj ) { return pObj->fCompl0; }
static inline int Gia_ObjFaninC1( Gia_Obj_t * pObj ) { return pObj->fCompl1; }
static inline int Gia_ObjFaninC2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes && Abc_LitIsCompl(p->pMuxes[Gia_ObjId(p, pObj)]); }
static inline int Gia_ObjFaninC( Gia_Obj_t * pObj, int n ) { return n ? Gia_ObjFaninC1(pObj) : Gia_ObjFaninC0(pObj); }
static inline Gia_Obj_t * Gia_ObjFanin0( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff0; }
static inline Gia_Obj_t * Gia_ObjFanin1( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff1; }
static inline Gia_Obj_t * Gia_ObjFanin2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return p->pMuxes ? Gia_ManObj(p, Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)])) : NULL; }
static inline Gia_Obj_t * Gia_ObjFanin( Gia_Obj_t * pObj, int n ) { return n ? Gia_ObjFanin1(pObj) : Gia_ObjFanin0(pObj); }
static inline Gia_Obj_t * Gia_ObjChild0( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); }
static inline Gia_Obj_t * Gia_ObjChild1( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); }
static inline Gia_Obj_t * Gia_ObjChild2( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin2(p, pObj), Gia_ObjFaninC2(p, pObj) ); }
static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff0; }
static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; }
static inline int Gia_ObjFaninId2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? Abc_Lit2Var(p->pMuxes[ObjId]) : -1; }
static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int ObjId, int n ){ return n ? Gia_ObjFaninId1(pObj, ObjId) : Gia_ObjFaninId0(pObj, ObjId); }
static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); }
static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); }
static inline int Gia_ObjFaninId2p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)]) : -1; }
static inline int Gia_ObjFaninIdp( Gia_Man_t * p, Gia_Obj_t * pObj, int n){ return n ? Gia_ObjFaninId1p(p, pObj) : Gia_ObjFaninId0p(p, pObj); }
static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
static inline int Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1; }
@ -1544,6 +1548,9 @@ extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName, int fGiaSimple
extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
extern Gia_Man_t * Gia_ManReadMiniLut( char * pFileName );
extern void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName );
/*=== giaMinLut.c ===========================================================*/
extern word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare );
extern Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts );
/*=== giaMuxes.c ===========================================================*/
extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
extern void Gia_ManPrintMuxStats( Gia_Man_t * p );
@ -1754,6 +1761,10 @@ 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 ===========================================================*/
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 );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
@ -1763,7 +1774,6 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
ABC_NAMESPACE_HEADER_END

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

@ -20,6 +20,7 @@
#include "gia.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecHsh.h"
ABC_NAMESPACE_IMPL_START
@ -29,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
#define GIA_MAX_CUTSIZE 8
#define GIA_MAX_CUTNUM 51
#define GIA_MAX_CUTNUM 65
#define GIA_MAX_TT_WORDS ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1)
#define GIA_CUT_NO_LEAF 0xF
@ -778,6 +779,218 @@ void Gia_ManExtractTest( Gia_Man_t * pGia )
Abc_PrintTime( 0, "Creating windows", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis [Extract a given number of cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_StoCutPrint( int * pCut )
{
int v;
printf( "{" );
for ( v = 1; v <= pCut[0]; v++ )
printf( " %d", pCut[v] );
printf( " }\n" );
}
void Gia_StoPrintCuts( Vec_Int_t * vThis, int iObj, int nCutSize )
{
int i, * pCut;
printf( "Cuts of node %d (size = %d):\n", iObj, nCutSize );
Sdb_ForEachCut( Vec_IntArray(vThis), pCut, i )
if ( !nCutSize || pCut[0] == nCutSize )
Gia_StoCutPrint( pCut );
}
Vec_Wec_t * Gia_ManFilterCuts( Gia_Man_t * pGia, Vec_Wec_t * vStore, int nCutSize, int nCuts )
{
abctime clkStart = Abc_Clock();
Vec_Wec_t * vCutsSel = Vec_WecAlloc( nCuts );
Vec_Int_t * vLevel, * vCut = Vec_IntAlloc( 10 );
Vec_Wec_t * vCuts = Vec_WecAlloc( 1000 );
Hsh_VecMan_t * p = Hsh_VecManStart( 1000 ); int i, s;
Vec_WecForEachLevel( vStore, vLevel, i ) if ( Vec_IntSize(vLevel) )
{
int v, k, * pCut, Value;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k )
{
if ( pCut[0] < 2 )
continue;
for ( v = 1; v <= pCut[0]; v++ )
if ( pCut[v] < 9 )
break;
if ( v <= pCut[0] )
continue;
Vec_IntClear( vCut );
Vec_IntPushArray( vCut, pCut+1, pCut[0] );
Value = Hsh_VecManAdd( p, vCut );
if ( Value == Vec_WecSize(vCuts) )
{
Vec_Int_t * vTemp = Vec_WecPushLevel(vCuts);
Vec_IntPush( vTemp, 0 );
Vec_IntAppend( vTemp, vCut );
}
Vec_IntAddToEntry( Vec_WecEntry(vCuts, Value), 0, 1 );
}
}
printf( "Collected cuts = %d.\n", Vec_WecSize(vCuts) );
for ( s = 3; s <= nCutSize; s++ )
Vec_WecForEachLevel( vCuts, vLevel, i )
if ( Vec_IntSize(vLevel) - 1 == s )
{
int * pCut = Vec_IntEntryP(vLevel, 1);
int u, v, Value;
for ( u = 0; u < s; u++ )
{
Vec_IntClear( vCut );
for ( v = 0; v < s; v++ ) if ( v != u )
Vec_IntPush( vCut, pCut[v] );
assert( Vec_IntSize(vCut) == s-1 );
Value = Hsh_VecManAdd( p, vCut );
if ( Value < Vec_WecSize(vCuts) )
Vec_IntAddToEntry( vLevel, 0, Vec_IntEntry(Vec_WecEntry(vCuts, Value), 0) );
}
}
Hsh_VecManStop( p );
Vec_IntFree( vCut );
// collect
Vec_WecSortByFirstInt( vCuts, 1 );
Vec_WecForEachLevelStop( vCuts, vLevel, i, Abc_MinInt(Vec_WecSize(vCuts), nCuts) )
Vec_IntAppend( Vec_WecPushLevel(vCutsSel), vLevel );
Abc_PrintTime( 0, "Cut filtering time", Abc_Clock() - clkStart );
return vCutsSel;
}
int Gia_ManCountRefs( Gia_Man_t * pGia, Vec_Int_t * vLevel )
{
int i, iObj, nRefs = 0;
Vec_IntForEachEntry( vLevel, iObj, i )
nRefs += Gia_ObjRefNumId(pGia, iObj);
return nRefs;
}
Vec_Wrd_t * Gia_ManGenSims( Gia_Man_t * pGia )
{
Vec_Wrd_t * vSims;
Vec_WrdFreeP( &pGia->vSimsPi );
pGia->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pGia) );
vSims = Gia_ManSimPatSim( pGia );
return vSims;
}
int Gia_ManFindSatDcs( Gia_Man_t * pGia, Vec_Wrd_t * vSims, Vec_Int_t * vLevel )
{
int nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
int i, w, iObj, Res = 0, Pres[256] = {0}, nMints = 1 << Vec_IntSize(vLevel);
for ( w = 0; w < 64*nWords; w++ )
{
int iInMint = 0;
Vec_IntForEachEntry( vLevel, iObj, i )
if ( Abc_TtGetBit( Vec_WrdEntryP(vSims, iObj*nWords), w ) )
iInMint |= 1 << i;
Pres[iInMint]++;
}
for ( i = 0; i < nMints; i++ )
Res += Pres[i] == 0;
return Res;
}
int Gia_ManCollectCutDivs( Gia_Man_t * p, Vec_Int_t * vIns )
{
Gia_Obj_t * pObj; int i, Res = 0;
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_IntSort( vIns, 0 );
Vec_IntPush( vRes, 0 );
Vec_IntAppend( vRes, vIns );
Gia_ManIncrementTravId( p );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vIns, p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
continue;
else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
{
if ( !Gia_ObjIsTravIdPrevious(p, pObj) )
Vec_IntPush( vRes, i );
Gia_ObjSetTravIdCurrent( p, pObj );
}
// printf( "Divisors: " );
// Vec_IntPrint( vRes );
Res = Vec_IntSize(vRes);
Vec_IntFree( vRes );
return Res;
}
void Gia_ManConsiderCuts( Gia_Man_t * pGia, Vec_Wec_t * vCuts )
{
Vec_Wrd_t * vSims = Gia_ManGenSims( pGia );
Vec_Int_t * vLevel; int i;
Gia_ManCreateRefs( pGia );
Vec_WecForEachLevel( vCuts, vLevel, i )
{
printf( "Cut %3d ", i );
printf( "Ref = %3d : ", Vec_IntEntry(vLevel, 0) );
Vec_IntShift( vLevel, 1 );
printf( "Ref = %3d : ", Gia_ManCountRefs(pGia, vLevel) );
printf( "SDC = %3d : ", Gia_ManFindSatDcs(pGia, vSims, vLevel) );
printf( "Div = %3d : ", Gia_ManCollectCutDivs(pGia, vLevel) );
Vec_IntPrint( vLevel );
Vec_IntShift( vLevel, -1 );
}
Vec_WrdFree( vSims );
}
Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 )
{
int nCutSize = nCutSize0;
int nCutNum = 64;
int fCutMin = 0;
int fTruthMin = 0;
int fVerbose = fVerbose0;
Vec_Wec_t * vCutsSel;
Gia_Sto_t * p = Gia_StoAlloc( pGia, nCutSize, nCutNum, fCutMin, fTruthMin, fVerbose );
Gia_Obj_t * pObj; int i, iObj;
assert( nCutSize <= GIA_MAX_CUTSIZE );
assert( nCutNum < GIA_MAX_CUTNUM );
// prepare references
Gia_ManForEachObj( p->pGia, pObj, iObj )
Gia_StoRefObj( p, iObj );
// compute cuts
Gia_StoComputeCutsConst0( p, 0 );
Gia_ManForEachCiId( p->pGia, iObj, i )
Gia_StoComputeCutsCi( p, iObj );
Gia_ManForEachAnd( p->pGia, pObj, iObj )
Gia_StoComputeCutsNode( p, iObj );
if ( p->fVerbose )
{
printf( "Running cut computation with CutSize = %d CutNum = %d CutMin = %s TruthMin = %s\n",
p->nCutSize, p->nCutNum, p->fCutMin ? "yes":"no", p->fTruthMin ? "yes":"no" );
printf( "CutPair = %.0f ", p->CutCount[0] );
printf( "Merge = %.0f (%.2f %%) ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
printf( "Eval = %.0f (%.2f %%) ", p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
printf( "\n" );
printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ",
p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
}
vCutsSel = Gia_ManFilterCuts( pGia, p->vCuts, nCutSize0, nCuts0 );
Gia_ManConsiderCuts( pGia, vCutsSel );
Gia_StoFree( p );
return vCutsSel;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -860,6 +860,27 @@ Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap )
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCiNum(p) + Gia_ManCoNum(p) );
Gia_ManHashStart( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendBuf( pNew, pObj->Value );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
Gia_ManHashStop( pNew );
return pNew;
}
/**Function*************************************************************

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

@ -1869,7 +1869,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
if ( ~pObj->Value )
return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) && !Gia_ObjFailed(p,Gia_ObjId(p,pObj)) )
{
if ( Gia_ObjIsConst0(pRepr) )
{

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

@ -1891,7 +1891,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
if ( !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance &&
!pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize &&
!pIfMan->pPars->fEnableCheck75 && !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune &&
!pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars )
!pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars && !pIfMan->pPars->fUseCheck1 && !pIfMan->pPars->fUseCheck2 )
If_CutRotatePins( pIfMan, pCutBest );
// collect leaves of the best cut
Vec_IntClear( vLeaves );

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

@ -733,7 +733,7 @@ void Gia_RsbCiWindowTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n ) { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj); }
//static inline int Gia_ObjFaninId( Gia_Obj_t * pObj, int iObj, int n ) { return n ? Gia_ObjFaninId1(pObj, iObj) : Gia_ObjFaninId0(pObj, iObj); }
static inline int Gia_ObjTravIsTopTwo( Gia_Man_t * p, int iNodeA ) { return (p->pTravIds[iNodeA] >= p->nTravIds - 1); }
static inline int Gia_ObjTravIsSame( Gia_Man_t * p, int iNodeA, int iNodeB ) { return (p->pTravIds[iNodeA] == p->pTravIds[iNodeB]); }

60
src/aig/gia/giaSatSyn.c Normal file
View File

@ -0,0 +1,60 @@
/**CFile****************************************************************
FileName [giaSyn.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [High-effort synthesis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaSyn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int nTimeLimit, int fUseXor, int fFancy, int fVerbose )
{
Gia_Man_t * pNew = NULL;
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -22,6 +22,7 @@
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
//#include <immintrin.h>
#include "aig/miniaig/miniaig.h"
ABC_NAMESPACE_IMPL_START
@ -2706,6 +2707,81 @@ Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose )
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManProcessBuffs( Gia_Man_t * pHie, Vec_Wrd_t * vSimsH, int nWords, Vec_Mem_t * vStore, Vec_Int_t * vLabels )
{
Vec_Int_t * vPoSigs = Vec_IntAlloc( Gia_ManBufNum(pHie) );
Vec_Int_t * vMap;
Vec_Wec_t * vNodes = Vec_WecStart( Gia_ManBufNum(pHie) );
Gia_Obj_t * pObj; int i, Sig, Value;
Gia_ManForEachBuf( pHie, pObj, i )
{
word * pSim = Vec_WrdEntryP(vSimsH, Gia_ObjId(pHie, pObj)*nWords);
int fCompl = pSim[0] & 1;
if ( fCompl )
Abc_TtNot( pSim, nWords );
Vec_IntPush( vPoSigs, Vec_MemHashInsert(vStore, pSim) );
if ( fCompl )
Abc_TtNot( pSim, nWords );
}
Vec_IntPrint( vPoSigs );
vMap = Vec_IntStartFull( Vec_MemEntryNum(vStore) );
Vec_IntForEachEntry( vPoSigs, Sig, i )
{
assert( Vec_IntEntry(vMap, Sig) == -1 );
Vec_IntWriteEntry( vMap, Sig, i );
}
Vec_IntForEachEntry( vLabels, Sig, i )
{
if ( Sig < 0 )
continue;
Value = Vec_IntEntry(vMap, Sig);
if ( Value == -1 )
continue;
assert( Value >= 0 && Value < Gia_ManBufNum(pHie) );
Vec_WecPush( vNodes, Value, i );
}
Vec_WecPrint( vNodes, 0 );
Vec_WecFree( vNodes );
Vec_IntFree( vMap );
Vec_IntFree( vPoSigs );
return NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld )
{
Gia_Obj_t * pObj; int i;
Gia_ManSetPhase( pNew );
Gia_ManSetPhase( pOld );
Gia_ManForEachCo( pNew, pObj, i )
if ( pObj->fPhase ^ Gia_ManCo(pOld, i)->fPhase )
{
printf( "Updating out %d.\n", i );
Gia_ObjFlipFaninC0( pObj );
}
}
/**Function*************************************************************
Synopsis []
@ -2723,7 +2799,8 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
Vec_Wrd_t * vSims = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords );
Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat );
Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie );
Gia_Obj_t * pObj; int * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
Vec_Int_t * vLabels = Vec_IntStartFull( Gia_ManObjNum(pFlat) );
Gia_Obj_t * pObj; int fCompl, Value, * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
pFlat->vSimsPi = NULL;
pHie->vSimsPi = NULL;
@ -2739,7 +2816,13 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
word * pSim = Vec_WrdEntryP(vSims0, i*nWords);
nC0s += Abc_TtIsConst0(pSim, nWords);
nC1s += Abc_TtIsConst1(pSim, nWords);
Vec_MemHashInsert( vStore, pSim );
fCompl = pSim[0] & 1;
if ( fCompl )
Abc_TtNot( pSim, nWords );
Value = Vec_MemHashInsert( vStore, pSim );
if ( fCompl )
Abc_TtNot( pSim, nWords );
Vec_IntWriteEntry( vLabels, i, Value );
}
nUnique = Vec_MemEntryNum( vStore );
printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n",
@ -2765,10 +2848,12 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
//if ( Gia_ObjIsBuf(pObj) )
// printf( "%d(%d) ", i, nBoundary-1 );
}
Gia_ManProcessBuffs( pHie, vSims1, nWords, vStore, vLabels );
Vec_MemHashFree( vStore );
Vec_MemFree( vStore );
Vec_WrdFree( vSims0 );
Vec_WrdFree( vSims1 );
Vec_IntFree( vLabels );
printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary. ",
nMatched, 100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)),
@ -2777,6 +2862,405 @@ void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fV
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Gia_ManRelTfos( Gia_Man_t * p, Vec_Int_t * vObjs )
{
Gia_Obj_t * pObj;
Vec_Wec_t * vNodes = Vec_WecStart( Vec_IntSize(vObjs)+1 );
Vec_Int_t * vSigns = Vec_IntStart( Gia_ManObjNum(p) );
int n, k, i, iObj, * pSigns = Vec_IntArray(vSigns);
assert( Vec_IntSize(vObjs) < 32 );
Vec_IntForEachEntry( vObjs, iObj, i )
pSigns[iObj] |= 1 << i;
Gia_ManForEachAnd( p, pObj, i )
{
if ( pSigns[i] == 0 )
for ( n = 0; n < 2; n++ )
pSigns[i] |= pSigns[Gia_ObjFaninId(pObj, i, n)];
if ( pSigns[i] == 0 )
continue;
Vec_WecPush( vNodes, Vec_IntSize(vObjs), i );
for ( k = 0; k < Vec_IntSize(vObjs); k++ )
if ( (pSigns[i] >> k) & 1 )
Vec_WecPush( vNodes, k, i );
}
Vec_IntFree( vSigns );
return vNodes;
}
Vec_Wrd_t * Gia_ManRelDerive( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
{
int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
int i, m, iVar, iMint = 0, nMints = 1 << Vec_IntSize(vObjs);
Vec_Wrd_t * vCopy = Vec_WrdDup(vSims); Vec_Int_t * vLevel;
Vec_Wrd_t * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
Vec_Wec_t * vNodes = Gia_ManRelTfos( p, vObjs );
Vec_WecPrint( vNodes, 0 );
Gia_ManForEachAnd( p, pObj, i )
assert( pObj->fPhase == 0 );
Gia_ManForEachObjVec( vObjs, p, pObj, i )
pObj->fPhase = 1;
vLevel = Vec_WecEntry( vNodes, Vec_IntSize(vObjs) );
Gia_ManForEachObjVec( vLevel, p, pObj, i )
if ( pObj->fPhase )
Abc_TtClear( Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords), nWords );
else
Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
for ( m = 0; m < nMints; m++ )
{
Gia_ManForEachCo( p, pObj, i )
{
word * pSimO = Vec_WrdEntryP(vCopy, Gia_ObjId(p, pObj)*nWords);
word * pSimF = Vec_WrdEntryP(vCopy, Gia_ObjFaninId0p(p, pObj)*nWords);
word * pSimR = Vec_WrdEntryP(vRel, (iMint*Gia_ManCoNum(p) + i)*nWords);
Abc_TtXor( pSimR, pSimF, pSimO, nWords, Gia_ObjFaninC0(pObj) );
}
if ( m == nMints-1 )
break;
iVar = Abc_TtSuppFindFirst( (m+1) ^ ((m+1) >> 1) ^ (m) ^ ((m) >> 1) );
vLevel = Vec_WecEntry( vNodes, iVar );
assert( Vec_IntEntry(vLevel, 0) == Vec_IntEntry(vObjs, iVar) );
Abc_TtNot( Vec_WrdEntryP(vCopy, Vec_IntEntry(vObjs, iVar)*nWords), nWords );
Gia_ManForEachObjVec( vLevel, p, pObj, i )
if ( !pObj->fPhase )
Gia_ManSimPatSimAnd( p, Gia_ObjId(p, pObj), pObj, nWords, vCopy );
iMint ^= 1 << iVar;
}
Gia_ManForEachObjVec( vObjs, p, pObj, i )
pObj->fPhase = 0;
Vec_WrdFree( vCopy );
Vec_WecFree( vNodes );
return vRel;
}
Vec_Wrd_t * Gia_ManRelDerive2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims )
{
int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Gia_Obj_t * pObj;
int i, Id, m, Index, nMints = 1 << Vec_IntSize(vObjs);
Vec_Wrd_t * vPos, * vRel = Vec_WrdStart( Gia_ManCoNum(p) * nWords * nMints );
for ( m = 0; m < nMints; m++ )
{
Gia_Man_t * pNew = Gia_ManDup( p );
Gia_ManForEachAnd( pNew, pObj, i )
{
if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId0(pObj, i))) >= 0 )
pObj->iDiff0 = i, pObj->fCompl0 ^= (m >> Index) & 1;
if ( (Index = Vec_IntFind(vObjs, Gia_ObjFaninId1(pObj, i))) >= 0 )
pObj->iDiff1 = i, pObj->fCompl1 ^= (m >> Index) & 1;
}
vPos = Gia_ManSimPatSimOut( pNew, p->vSimsPi, 1 );
Gia_ManForEachCoId( p, Id, i )
Abc_TtXor( Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p) + i)*nWords), Vec_WrdEntryP(vPos, i*nWords), Vec_WrdEntryP(vSims, Id*nWords), nWords, 0 );
Vec_WrdFree( vPos );
Gia_ManStop( pNew );
}
return vRel;
}
void Gia_ManRelPrint( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
{
int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
for ( w = 0; w < 64*nWords; w++ )
{
Gia_ManForEachCiId( p, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
printf( " " );
Vec_IntForEachEntry( vObjs, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
printf( " " );
Gia_ManForEachCoId( p, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
printf( " " );
for ( m = 0; m < nMints; m++ )
{
printf( " " );
for ( i = 0; i < Vec_IntSize(vObjs); i++ )
printf( "%d", (m >> i) & 1 );
printf( "=" );
Gia_ManForEachCoId( p, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w) );
}
printf( "\n" );
}
}
void Gia_ManRelPrint2( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vSims, Vec_Wrd_t * vRel )
{
int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
int i, Id, m, nMints = 1 << Vec_IntSize(vObjs);
int nWordsM = Abc_Truth6WordNum(Vec_IntSize(vObjs));
Vec_Wrd_t * vRes = Vec_WrdStart( 64*nWords * nWordsM );
printf( "Relation has %d inputs and %d outputs:\n", Gia_ManCiNum(p), Vec_IntSize(vObjs) );
for ( w = 0; w < 64*nWords; w++ )
{
int iMint = 0;
int nValid = 0;
Gia_ManForEachCiId( p, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
printf( " " );
Vec_IntForEachEntry( vObjs, Id, i )
{
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) )
iMint |= 1 << i;
}
printf( " " );
Gia_ManForEachCoId( p, Id, i )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vSims, Id*nWords), w) );
printf( " " );
for ( m = 0; m < nMints; m++ )
{
int Count = 0;
Gia_ManForEachCoId( p, Id, i )
Count += Abc_TtGetBit(Vec_WrdEntryP(vRel, (m*Gia_ManCoNum(p)+i)*nWords), w);
printf( "%d", Count == 0 );
nValid += Count > 0;
if ( Count == 0 )
Abc_TtSetBit( Vec_WrdEntryP(vRes, w*nWordsM), m );
}
printf( " " );
for ( m = 0; m < nMints; m++ )
printf( "%d", Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), m) );
printf( " " );
assert( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint) );
for ( i = 0; i < Vec_IntSize(vObjs); i++ )
if ( Abc_TtGetBit(Vec_WrdEntryP(vRes, w*nWordsM), iMint ^ (1 << i)) )
printf( "-" );
else
printf( "%d", (iMint >> i) & 1 );
printf( " %d", nMints-nValid );
printf( "\n" );
}
Vec_WrdFree( vRes );
}
Vec_Int_t * Gia_ManRelInitObjs()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
/*
Vec_IntPush( vRes, 33 );
Vec_IntPush( vRes, 52 );
Vec_IntPush( vRes, 53 );
Vec_IntPush( vRes, 65 );
Vec_IntPush( vRes, 79 );
Vec_IntPush( vRes, 81 );
*/
/*
Vec_IntPush( vRes, 60 );
Vec_IntPush( vRes, 61 );
Vec_IntPush( vRes, 71 );
Vec_IntPush( vRes, 72 );
*/
/*
Vec_IntPush( vRes, 65 );
Vec_IntPush( vRes, 79 );
Vec_IntPush( vRes, 81 );
*/
Vec_IntPush( vRes, 52 );
Vec_IntPush( vRes, 54 );
Vec_IntPrint( vRes );
return vRes;
}
void Gia_ManRelDeriveTest2( Gia_Man_t * p )
{
Vec_Int_t * vObjs = Gia_ManRelInitObjs();
Vec_Wrd_t * vSims, * vRel, * vRel2; int nWords;
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
vSims = Gia_ManSimPatSim( p );
vRel = Gia_ManRelDerive( p, vObjs, vSims );
vRel2 = Gia_ManRelDerive2( p, vObjs, vSims );
//assert( !memcmp(vRel2->pArray, vRel->pArray, sizeof(word)*Vec_WrdSize(vRel)) );
Gia_ManRelPrint2( p, vObjs, vSims, vRel );
Vec_WrdFree( vRel2 );
Vec_WrdFree( vRel );
Vec_WrdFree( vSims );
Vec_IntFree( vObjs );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManRelInitIns()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 12 );
Vec_IntPush( vRes, 18 );
Vec_IntPush( vRes, 21 );
Vec_IntPush( vRes, 34 );
Vec_IntPush( vRes, 45 );
Vec_IntPush( vRes, 59 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitOuts()
{
Vec_Int_t * vRes = Vec_IntAlloc( 10 );
Vec_IntPush( vRes, 65 );
Vec_IntPush( vRes, 66 );
return vRes;
}
Vec_Int_t * Gia_ManRelInitMffc( Gia_Man_t * p, Vec_Int_t * vOuts )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_IntSort( vOuts, 0 );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vOuts, p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
Gia_ManIncrementTravId( p );
Gia_ManForEachCo( p, pObj, i )
if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
Gia_ManForEachAndReverse( p, pObj, i )
if ( Gia_ObjIsTravIdPrevious(p, pObj) )
continue;
else if ( Gia_ObjIsTravIdCurrent(p, pObj) )
{
if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
if ( !Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin1(pObj)) )
Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin1(pObj) );
}
Gia_ManForEachAnd( p, pObj, i )
if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
Vec_IntPush( vRes, i );
printf( "MFFC: " );
Vec_IntPrint( vRes );
return vRes;
}
Vec_Int_t * Gia_ManRelInitDivs( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vOuts )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vMffc = Gia_ManRelInitMffc( p, vOuts );
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_IntSort( vIns, 0 );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vMffc, p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
Vec_IntFree( vMffc );
Vec_IntPush( vRes, 0 );
Vec_IntAppend( vRes, vIns );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vIns, p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
continue;
else if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
{
if ( !Gia_ObjIsTravIdPrevious(p, pObj) )
Vec_IntPush( vRes, i );
Gia_ObjSetTravIdCurrent( p, pObj );
}
printf( "Divisors: " );
Vec_IntPrint( vRes );
return vRes;
}
Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts )
{
Vec_Int_t * vRes = Vec_IntStartFull( 1 << Vec_IntSize(vIns) );
int w, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
for ( w = 0; w < 64*nWords; w++ )
{
int i, iObj, iMint = 0, iMint2 = 0;
Vec_IntForEachEntry( vIns, iObj, i )
if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
iMint |= 1 << i;
if ( Vec_IntEntry(vRes, iMint) >= 0 )
continue;
Vec_IntForEachEntry( vOuts, iObj, i )
if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), w) )
iMint2 |= 1 << i;
Vec_IntWriteEntry( vRes, iMint, iMint2 );
}
return vRes;
}
void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs )
{
extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose );
int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1);
Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
int Entry0 = Vec_IntEntry( vRel, 0 );
word Value, Phase = 0;
int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
Vec_IntForEachEntry( vDivs, iObj, i )
if ( Vec_WrdEntry(vSims, iObj*nWords) & 1 )
Phase |= 1 << i;
assert( Entry0 >= 0 );
printf( "Entry0 = %d\n", Entry0 );
Entry0 ^= 1;
// for ( m = 0; m < nMints; m++ )
Vec_IntForEachEntry( vRel, Entry, m )
{
if ( Entry == -1 )
continue;
Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, iMint), Entry0 ^ Entry );
Value = 0;
Vec_IntForEachEntry( vDivs, iObj, i )
if ( Abc_TtGetBit(Vec_WrdEntryP(vSims, iObj*nWords), m) )
Abc_TtSetBit( &Value, i );
Vec_WrdEntryP(vSimsOut, iMint)[0] = Value ^ Phase;
iMint++;
}
assert( iMint == nMints );
printf( "Created %d minterms.\n", iMint );
Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 );
Vec_WrdFree( vSimsIn );
Vec_WrdFree( vSimsOut );
}
void Gia_ManRelDeriveTest( Gia_Man_t * p )
{
Vec_Int_t * vIns = Gia_ManRelInitIns();
Vec_Int_t * vOuts = Gia_ManRelInitOuts();
Vec_Wrd_t * vSims; Vec_Int_t * vRel, * vDivs; int nWords;
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
vSims = Gia_ManSimPatSim( p );
vRel = Gia_ManRelDeriveSimple( p, vSims, vIns, vOuts );
vDivs = Gia_ManRelInitDivs( p, vIns, vOuts );
//printf( "Neg = %d\n", Vec_IntCountEntry(vRel, -1) );
Gia_ManRelSolve( p, vSims, vIns, vOuts, vRel, vDivs );
Vec_IntFree( vDivs );
Vec_IntPrint( vRel );
Vec_IntFree( vRel );
Vec_WrdFree( vSims );
Vec_IntFree( vIns );
Vec_IntFree( vOuts );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1213
src/aig/gia/giaTtopt.cpp Normal file
View File

File diff suppressed because it is too large Load Diff

31
src/aig/gia/giaUtil.c
View File

@ -3130,6 +3130,37 @@ void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName )
}
}
/**Function*************************************************************
Synopsis [Transform flops.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintArray( Gia_Man_t * p )
{
Gia_Obj_t * pObj; int i, nSize = Gia_ManObjNum(p);
printf( "static int s_ArraySize = %d;\n", nSize );
printf( "static int s_ArrayData[%d] = {\n", 2*nSize );
printf( " 0, 0," );
printf( "\n " );
Gia_ManForEachCi( p, pObj, i )
printf( "0, 0, " );
printf( "\n " );
Gia_ManForEachAnd( p, pObj, i )
printf( "%d, %d, ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit1p(p, pObj) );
printf( "\n " );
Gia_ManForEachCo( p, pObj, i )
printf( "%d, %d, ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) );
printf( "\n" );
printf( "};\n" );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -77,6 +77,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaSatLut.c \
src/aig/gia/giaSatMap.c \
src/aig/gia/giaSatoko.c \
src/aig/gia/giaSatSyn.c \
src/aig/gia/giaSat3.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaScript.c \
@ -104,5 +105,6 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaTis.c \
src/aig/gia/giaTruth.c \
src/aig/gia/giaTsim.c \
src/aig/gia/giaTtopt.cpp \
src/aig/gia/giaUnate.c \
src/aig/gia/giaUtil.c

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

@ -144,6 +144,18 @@ static Mini_Aig_t * Mini_AigStart()
Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
return p;
}
static Mini_Aig_t * Mini_AigStartSupport( int nIns, int nObjsAlloc )
{
Mini_Aig_t * p; int i;
assert( 1+nIns < nObjsAlloc );
p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );
p->nCap = 2*nObjsAlloc;
p->nSize = 2*(1+nIns);
p->pArray = MINI_AIG_ALLOC( int, p->nCap );
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = MINI_AIG_NULL;
return p;
}
static void Mini_AigStop( Mini_Aig_t * p )
{
MINI_AIG_FREE( p->pArray );
@ -170,6 +182,31 @@ static int Mini_AigAndNum( Mini_Aig_t * p )
nNodes++;
return nNodes;
}
static int Mini_AigXorNum( Mini_Aig_t * p )
{
int i, nNodes = 0;
Mini_AigForEachAnd( p, i )
nNodes += p->pArray[2*i] > p->pArray[2*i+1];
return nNodes;
}
static int Mini_AigLevelNum( Mini_Aig_t * p )
{
int i, Level = 0;
int * pLevels = MINI_AIG_CALLOC( int, Mini_AigNodeNum(p) );
Mini_AigForEachAnd( p, i )
{
int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
int Lel1 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin1(p, i))];
pLevels[i] = 1 + (Lel0 > Lel1 ? Lel0 : Lel1);
}
Mini_AigForEachPo( p, i )
{
int Lel0 = pLevels[Mini_AigLit2Var(Mini_AigNodeFanin0(p, i))];
Level = Level > Lel0 ? Level : Lel0;
}
MINI_AIG_FREE( pLevels );
return Level;
}
static void Mini_AigPrintStats( Mini_Aig_t * p )
{
printf( "MiniAIG stats: PI = %d PO = %d FF = %d AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) );
@ -648,6 +685,25 @@ int main( int argc, char ** argv )
}
*/
/*
#include "aig/miniaig/miniaig.h"
// this procedure creates a MiniAIG for function F = a*b + ~c and writes it into a file "test.aig"
void Mini_AigTest()
{
Mini_Aig_t * p = Mini_AigStart(); // create empty AIG manager (contains only const0 node)
int litApos = Mini_AigCreatePi( p ); // create input A (returns pos lit of A)
int litBpos = Mini_AigCreatePi( p ); // create input B (returns pos lit of B)
int litCpos = Mini_AigCreatePi( p ); // create input C (returns pos lit of C)
int litCneg = Mini_AigLitNot( litCpos ); // neg lit of C
int litAnd = Mini_AigAnd( p, litApos, litBpos ); // lit for a*b
int litOr = Mini_AigOr( p, litAnd, litCneg ); // lit for a*b + ~c
Mini_AigCreatePo( p, litOr ); // create primary output
Mini_AigerWrite( "test.aig", p, 1 ); // write the result into a file
Mini_AigStop( p ); // deallocate MiniAIG
}
*/
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////

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

@ -506,7 +506,7 @@ static inline void Ndr_WriteVerilogModule( FILE * pFile, void * pDesign, int Mod
else if ( nArray == 3 && Type == ABC_OPER_ARI_ADD )
fprintf( pFile, "%s + %s + %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
else if ( Type == ABC_OPER_BIT_MUX )
fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[2]], pNames[pArray[1]] );
else
fprintf( pFile, "<cannot write operation %s>;\n", Abc_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) );
}

85
src/base/abc/abcUtil.c
View File

@ -3267,6 +3267,91 @@ Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp )
return Abc_NtkStrashToGia( pNtkNew );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int s_ArraySize = 145;
static int s_ArrayData[290] = {
0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
10, 6, 14, 12, 10, 2, 22, 20, 2, 24, 16, 4, 28, 18, 16, 10, 8, 4, 34, 32, 30, 36, 38, 26, 16, 6, 36, 20, 44, 42, 46, 40, 42, 44, 14, 6, 52, 34, 32, 54, 56, 50, 58, 48, 32, 24, 20, 2, 12, 6, 66, 34, 68, 64, 62, 70, 28, 68, 74, 72, 76, 58, 70, 62, 80, 78, 68, 28, 84, 74, 4, 2, 88, 20, 64, 90, 92, 86, 66, 32, 18, 96, 98, 56, 100, 94, 52, 36, 104, 38, 90, 42, 36, 2, 108, 110, 112, 106, 114, 100, 102, 116, 118, 82, 116, 60, 120, 122, 124, 60, 118, 60, 102, 82, 128, 130, 132, 82, 134, 126, 82, 116, 122, 138, 122, 118, 142, 140, 60, 102, 130, 146, 130, 118, 150, 148, 152, 144, 154, 136, 18, 156, 144, 126, 68, 160, 32, 136, 164, 162, 166, 158, 28, 160, 70, 126, 90, 144, 174, 172, 176, 170, 152, 134, 36, 180, 2, 134, 184, 182, 186, 178, 188, 168, 64, 144, 164, 158, 194, 192, 96, 156, 44, 154, 200, 170, 202, 198, 204, 176, 206, 196, 204, 168, 62, 126, 212, 186, 24, 134, 108, 152, 218, 192, 220, 216, 222, 214, 224, 210, 220, 194, 110, 152, 30, 180, 232, 230, 184, 172, 236, 234, 238, 228, 234, 182, 242, 220, 244, 168, 42, 154, 248, 202, 54, 136, 252, 164, 254, 214, 256, 250, 218, 194, 252, 198, 262, 242, 264, 260, 232, 220, 268, 262, 270, 168,
191, 191, 209, 209, 226, 226, 240, 240, 246, 246, 259, 259, 267, 267, 272, 272,
};
int Abc_NtkHasConstNode()
{
int i;
for ( i = 1; i < s_ArraySize; i++ )
if ( s_ArrayData[2*i] || s_ArrayData[2*i+1] )
break;
for ( ; i < s_ArraySize; i++ )
if ( s_ArrayData[2*i] < 2 && s_ArrayData[2*i+1] < 2 )
return 1;
return 0;
}
Abc_Ntk_t * Abc_NtkFromArray()
{
Vec_Ptr_t * vNodes = Vec_PtrAlloc( s_ArraySize ); int i, nPos = 0;
Abc_Ntk_t * pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
Abc_Obj_t * pObjNew = Abc_NtkHasConstNode() ? Abc_NtkCreateNode(pNtkNew) : NULL;
if ( pObjNew ) pObjNew->pData = Abc_SopCreateConst0((Mem_Flex_t *)pNtkNew->pManFunc);
Vec_PtrPush( vNodes, pObjNew );
for ( i = 1; i < s_ArraySize; i++ )
if ( !s_ArrayData[2*i] && !s_ArrayData[2*i+1] )
Vec_PtrPush( vNodes, Abc_NtkCreatePi(pNtkNew) );
else
break;
for ( ; i < s_ArraySize; i++ )
{
char * pSop = NULL;
if ( s_ArrayData[2*i] > s_ArrayData[2*i+1] )
pSop = Abc_SopCreateXor( (Mem_Flex_t *)pNtkNew->pManFunc, 2 );
else if ( s_ArrayData[2*i] < s_ArrayData[2*i+1] )
pSop = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
else
break;
pObjNew = Abc_NtkCreateNode( pNtkNew );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i])) );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i+1])) );
if ( Abc_LitIsCompl(s_ArrayData[2*i]) ) Abc_SopComplementVar( pSop, 0 );
if ( Abc_LitIsCompl(s_ArrayData[2*i+1]) ) Abc_SopComplementVar( pSop, 1 );
pObjNew->pData = pSop;
Vec_PtrPush( vNodes, pObjNew );
}
for ( ; i < s_ArraySize; i++ )
{
char * pSop = NULL;
assert( s_ArrayData[2*i] == s_ArrayData[2*i+1] );
pObjNew = Abc_NtkCreateNode( pNtkNew );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Vec_PtrEntry(vNodes, Abc_Lit2Var(s_ArrayData[2*i])) );
if ( Abc_LitIsCompl(s_ArrayData[2*i]) )
pSop = Abc_SopCreateInv( (Mem_Flex_t *)pNtkNew->pManFunc );
else
pSop = Abc_SopCreateBuf( (Mem_Flex_t *)pNtkNew->pManFunc );
pObjNew->pData = pSop;
Vec_PtrPush( vNodes, pObjNew );
nPos++;
}
for ( i = 0; i < nPos; i++ )
Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), (Abc_Obj_t *)Vec_PtrEntry(vNodes, s_ArraySize-nPos+i) );
Vec_PtrFree( vNodes );
pNtkNew->pName = Extra_UtilStrsav("test");
Abc_NtkAddDummyPiNames( pNtkNew );
Abc_NtkAddDummyPoNames( pNtkNew );
Abc_NtkAddDummyBoxNames( pNtkNew );
if ( !Abc_NtkCheck( pNtkNew ) )
Abc_Print( 1, "Abc_NtkFromArray(): Network check has failed.\n" );
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -499,6 +499,9 @@ static int Abc_CommandAbc9LNetRead ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9LNetSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9LNetEval ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9LNetOpt ( Abc_Frame_t * pAbc, int argc, char ** argv );
//#ifndef _WIN32
static int Abc_CommandAbc9Ttopt ( Abc_Frame_t * pAbc, int argc, char ** argv );
//#endif
static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Struct ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -561,6 +564,7 @@ static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9DeepSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StochSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1248,6 +1252,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&lnetsim", Abc_CommandAbc9LNetSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&lneteval", Abc_CommandAbc9LNetEval, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&lnetopt", Abc_CommandAbc9LNetOpt, 0 );
//#ifndef _WIN32
Cmd_CommandAdd( pAbc, "ABC9", "&ttopt", Abc_CommandAbc9Ttopt, 0 );
//#endif
Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&struct", Abc_CommandAbc9Struct, 0 );
@ -1310,6 +1317,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&deepsyn", Abc_CommandAbc9DeepSyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satsyn", Abc_CommandAbc9SatSyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&stochsyn", Abc_CommandAbc9StochSyn, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
@ -8764,11 +8772,13 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars );
int c;
extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars );
int c, fKissat = 0, fKissat2 = 0;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INTadconugklvh" ) ) != EOF )
{
switch ( c )
{
@ -8808,12 +8818,30 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'd':
pPars->fDynConstr ^= 1;
break;
case 'c':
pPars->fDumpCnf ^= 1;
break;
case 'o':
pPars->fFewerVars ^= 1;
break;
case 'n':
pPars->fOrderNodes ^= 1;
break;
case 'u':
pPars->fUniqFans ^= 1;
break;
case 'g':
pPars->fGlucose ^= 1;
break;
case 'k':
fKissat ^= 1;
break;
case 'l':
fKissat2 ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -8845,21 +8873,31 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
return 1;
}
if ( pPars->fGlucose )
if ( fKissat )
Exa_ManExactSynthesis4( pPars );
else if ( fKissat2 )
Exa_ManExactSynthesis5( pPars );
else if ( pPars->fGlucose )
Exa_ManExactSynthesis( pPars );
else
Exa_ManExactSynthesis2( pPars );
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INT <num>] [-adconugklvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
Abc_Print( -2, "\t-n : toggle ordering internal nodes [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
Abc_Print( -2, "\t-u : toggle using unique fanouts [default = %s]\n", pPars->fUniqFans ? "yes" : "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
@ -9029,7 +9067,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MINKiaoegvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MINKianegvh" ) ) != EOF )
{
switch ( c )
{
@ -9083,7 +9121,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'o':
case 'n':
pPars->fOrderNodes ^= 1;
break;
case 'e':
@ -9179,7 +9217,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: allexact [-MIKN <num>] [-iaoevh] <hex>\n" );
Abc_Print( -2, "usage: allexact [-MIKN <num>] [-ianevh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t-M <num> : the majority support size (overrides -I and -K) [default = %d]\n", pPars->nMajSupp );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
@ -9187,7 +9225,7 @@ usage:
Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
Abc_Print( -2, "\t-n : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
Abc_Print( -2, "\t-e : toggle enumerating all solutions [default = %s]\n", pPars->fEnumSols ? "yes" : "no" );
// Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
@ -14065,6 +14103,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
//Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
//Mnist_ExperimentWithScaling( nDecMax );
//Gyx_ProblemSolveTest();
{
extern Abc_Ntk_t * Abc_NtkFromArray();
Abc_Ntk_t * pNtkRes = Abc_NtkFromArray();
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@ -32417,13 +32460,14 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp;
int c, Limit = 2;
int Multi = 0;
int fAddBuffs = 0;
int fAddStrash = 0;
int fCollapse = 0;
int fAddMuxes = 0;
int fStrMuxes = 0;
int fCollapse = 0;
int fAddMuxes = 0;
int fStrMuxes = 0;
int fRehashMap = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "LMacmrsh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsh" ) ) != EOF )
{
switch ( c )
{
@ -32449,6 +32493,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Multi <= 0 )
goto usage;
break;
case 'b':
fAddBuffs ^= 1;
break;
case 'a':
fAddStrash ^= 1;
break;
@ -32475,6 +32522,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
return 1;
}
if ( fAddBuffs )
{
extern Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p );
pTemp = Gia_ManDupAddBufs( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
if ( Multi > 0 )
{
extern Gia_Man_t * Gia_ManDupAddPis( Gia_Man_t * p, int nMulti );
@ -32549,8 +32603,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &st [-LM num] [-acmrsh]\n" );
Abc_Print( -2, "usage: &st [-LM num] [-bacmrsh]\n" );
Abc_Print( -2, "\t performs structural hashing\n" );
Abc_Print( -2, "\t-b : toggle adding buffers at the inputs and outputs [default = %s]\n", fAddBuffs? "yes": "no" );
Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
@ -39522,7 +39577,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fUse34Spec ^= 1;
break;
case 'b':
pPars->fUseBat ^= 1;
//pPars->fUseBat ^= 1;
pPars->fUseCheck1 ^= 1;
break;
case 'g':
pPars->fDelayOpt ^= 1;
@ -39543,7 +39599,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fEnableCheck75u ^= 1;
break;
case 'i':
pPars->fUseCofVars ^= 1;
//pPars->fUseCofVars ^= 1;
pPars->fUseCheck2 ^= 1;
break;
// case 'j':
// pPars->fEnableCheck07 ^= 1;
@ -39656,6 +39713,16 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncCell = If_CutPerformCheck07;
pPars->fCutMin = 1;
}
if ( pPars->fUseCheck1 || pPars->fUseCheck2 )
{
if ( pPars->nLutSize > 6 )
{
Abc_Print( -1, "This feature only works for no more than 6-LUTs.\n" );
return 1;
}
pPars->pFuncCell = pPars->fUseCheck2 ? If_MatchCheck2 : If_MatchCheck1;
pPars->fCutMin = 1;
}
if ( pPars->fUseCofVars )
{
if ( !(pPars->nLutSize & 1) )
@ -42165,6 +42232,116 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Ttopt( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
char * pFileName = NULL;
int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
nIns = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
goto usage;
}
nOuts = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" );
goto usage;
}
Limit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a positive integer.\n" );
goto usage;
}
nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
default:
goto usage;
}
}
if ( argc > globalUtilOptind + 1 )
{
return 0;
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Empty GIA network.\n" );
return 1;
}
if ( argc == globalUtilOptind + 1 )
{
FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
if ( pFile == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] );
return 0;
}
fclose( pFile );
pFileName = argv[globalUtilOptind];
}
if ( pFileName )
pTemp = Gia_ManTtoptCare( pAbc->pGia, nIns, nOuts, nRounds, pFileName, Limit );
else
pTemp = Gia_ManTtopt( pAbc->pGia, nIns, nOuts, nRounds );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &ttopt [-IORX num] [-vh] <file>\n" );
Abc_Print( -2, "\t performs specialized AIG optimization\n" );
Abc_Print( -2, "\t-I num : the input support size [default = %d]\n", nIns );
Abc_Print( -2, "\t-O num : the output group size [default = %d]\n", nOuts );
Abc_Print( -2, "\t-R num : patterns are cares starting this value [default = %d]\n", Limit );
Abc_Print( -2, "\t-X num : the number of optimization rounds [default = %d]\n", nRounds );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
Abc_Print( -2, "\t<file> : file name with simulation information\n");
Abc_Print( -2, "\t\n" );
Abc_Print( -2, "\t This command was contributed by Yukio Miyasaka.\n" );
Abc_Print( -2, "\t The paper describing the method: Y. Miyasaka et al. \"Synthesizing\n" );
Abc_Print( -2, "\t a class of practical Boolean functions using truth tables\". Proc. IWLS 2022.\n" );
Abc_Print( -2, "\t https://people.eecs.berkeley.edu/~alanmi/publications/2022/iwls22_reo.pdf\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -48322,6 +48499,96 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SatSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int TimeOut, int fUseXor, int fFancy, int fVerbose );
Gia_Man_t * pTemp; int c, nNodes = 0, nOuts = 0, TimeOut = 0, fUseXor = 0, fFancy = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NTafvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nNodes < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
nOuts = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nOuts < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOut < 0 )
goto usage;
break;
case 'a':
fUseXor ^= 1;
break;
case 'f':
fFancy ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SatSyn(): There is no AIG.\n" );
return 0;
}
pTemp = Gia_ManSyn( pAbc->pGia, nNodes, nOuts, TimeOut, fUseXor, fFancy, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &satsyn [-NOT <num>] [-afvh]\n" );
Abc_Print( -2, "\t performs synthesis\n" );
Abc_Print( -2, "\t-N <num> : the number of window nodes [default = %d]\n", nNodes );
Abc_Print( -2, "\t-O <num> : the number of window outputs [default = %d]\n", nOuts );
Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-a : toggle using xor-nodes [default = %s]\n", fUseXor? "yes": "no" );
Abc_Print( -2, "\t-f : toggle using additional feature [default = %s]\n", fFancy? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -50090,6 +50357,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManPrintArray( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManPerformNewResub( Gia_Man_t * p, int nWinCount, int nCutSize, int nProcs, int fVerbose );
extern void Gia_RsbEnumerateWindows( Gia_Man_t * p, int nInputsMax, int nLevelsMax );
extern int Gia_ManSumTotalOfSupportSizes( Gia_Man_t * p );
@ -50154,7 +50422,16 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
return 1;
}
Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
if ( argc == globalUtilOptind + 1 )
{
extern void Gia_ManUpdateCoPhase( Gia_Man_t * pNew, Gia_Man_t * pOld );
Gia_Man_t * pTemp = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 );
Gia_ManUpdateCoPhase( pAbc->pGia, pTemp );
Gia_ManStop( pTemp );
return 0;
}
//Abc_FrameUpdateGia( pAbc, Gia_ManPerformNewResub(pAbc->pGia, 100, 6, 1, 1) );
Gia_ManPrintArray( pAbc->pGia );
// printf( "AIG in \"%s\" has the sum of output support sizes equal to %d.\n", pAbc->pGia->pSpec, Gia_ManSumTotalOfSupportSizes(pAbc->pGia) );
return 0;
usage:

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

@ -535,10 +535,23 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
SeeAlso []
***********************************************************************/
void Ndr_DumpNdr( void * pDesign )
{
int i;
char ** pNames = ABC_CALLOC( char *, 10000 );
for ( i = 0; i < 10000; i++ )
{
char Buffer[100];
sprintf( Buffer, "s%d", i );
pNames[i] = Abc_UtilStrsav( Buffer );
}
Ndr_WriteVerilog( "temp.v", pDesign, pNames, 0 );
}
Wlc_Ntk_t * Wlc_ReadNdr( char * pFileName )
{
void * pData = Ndr_Read( pFileName );
Wlc_Ntk_t * pNtk = Wlc_NtkFromNdr( pData );
//Ndr_DumpNdr( pData );
//char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
//Ndr_WriteVerilog( NULL, pData, ppNames, 0 );
//Ndr_Delete( pData );

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

@ -289,9 +289,17 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
{
int fBooth = 1;
int fCla = 0;
int fSigned = fSign0 && fSign1;
int fSigned = fSign0 && fSign1;
//int i, iObj;
Vec_IntShrink( vArg0, nSizeArg0 );
Vec_IntShrink( vArg1, nSizeArg1 );
//printf( "Adding %d + %d + %d buffers\n", nSizeArg0, nSizeArg1, nRange );
//Vec_IntForEachEntry( vArg0, iObj, i )
// Vec_IntWriteEntry( vArg0, i, Gia_ManAppendBuf(pNew, iObj) );
//Vec_IntForEachEntry( vArg1, iObj, i )
// Vec_IntWriteEntry( vArg1, i, Gia_ManAppendBuf(pNew, iObj) );
if ( Wlc_NtkCountConstBits(Vec_IntArray(vArg0), Vec_IntSize(vArg0)) < Wlc_NtkCountConstBits(Vec_IntArray(vArg1), Vec_IntSize(vArg1)) )
ABC_SWAP( Vec_Int_t, *vArg0, *vArg1 )
if ( fBooth )
@ -303,6 +311,9 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
else
Vec_IntShrink( vRes, nRange );
assert( Vec_IntSize(vRes) == nRange );
//Vec_IntForEachEntry( vRes, iObj, i )
// Vec_IntWriteEntry( vRes, i, Gia_ManAppendBuf(pNew, iObj) );
return;
}
if ( Type == ABC_OPER_ARI_DIV || Type == ABC_OPER_ARI_MOD )

47
src/base/wln/wlnCom.c
View File

@ -92,12 +92,13 @@ void Wln_End( Abc_Frame_t * pAbc )
******************************************************************************/
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
FILE * pFile;
char * pFileName = NULL;
char * pTopModule= NULL;
char * pDefines = NULL;
int fBlast = 0;
int fInvert = 0;
int fTechMap = 1;
@ -105,7 +106,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCollapse = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TDbismcvh" ) ) != EOF )
{
switch ( c )
{
@ -118,6 +119,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
pTopModule = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
goto usage;
}
pDefines = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'b':
fBlast ^= 1;
break;
@ -164,11 +174,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pNew = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
@ -180,11 +190,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Rtl_Lib_t * pLib = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
@ -194,11 +204,12 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
}
return 0;
usage:
Abc_Print( -2, "usage: %%yosys [-T <module>] [-bismcvh] <file_name>\n" );
Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-bismcvh] <file_name>\n" );
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\"\n" );
Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
Abc_Print( -2, "\t-i : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
Abc_Print( -2, "\t-m : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
Abc_Print( -2, "\t-c : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "yes": "no" );
@ -330,13 +341,13 @@ usage:
******************************************************************************/
int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose );
extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose );
Gia_Man_t * pNew = NULL;
Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
char * pTopModule = NULL;
int c, fInv = 0, fVerbose = 0;
int c, fInv = 0, fRev = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Tcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Tcrvh" ) ) != EOF )
{
switch ( c )
{
@ -352,6 +363,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fInv ^= 1;
break;
case 'r':
fRev ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -366,16 +380,17 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "The design is not entered.\n" );
return 1;
}
pNew = Rtl_LibCollapse( pLib, pTopModule, fVerbose );
pNew = Rtl_LibCollapse( pLib, pTopModule, fRev, fVerbose );
if ( fInv )
Gia_ManInvertPos( pNew );
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
Abc_Print( -2, "usage: %%collapse [-T <module>] [-cvh] <file_name>\n" );
Abc_Print( -2, "usage: %%collapse [-T <module>] [-crvh] <file_name>\n" );
Abc_Print( -2, "\t collapse hierarchical design into an AIG\n" );
Abc_Print( -2, "\t-T : specify the top module of the design [default = none]\n" );
Abc_Print( -2, "\t-c : toggle complementing miter outputs after collapsing [default = %s]\n", fInv? "yes": "no" );
Abc_Print( -2, "\t-r : toggle bit order reversal in the word-level IO [default = %s]\n", fRev? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

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

@ -1725,6 +1725,42 @@ int Rtl_NtkInsertSignalRange( Rtl_Ntk_t * p, int Sig, int * pLits, int nLits )
return nBits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Rtl_NtkRevPermInput( Rtl_Ntk_t * p )
{
Vec_Int_t * vNew = Vec_IntAlloc( 100 ); int b, i, Count = 0;
for ( i = 0; i < p->nInputs; i++ )
{
int Width = Rtl_WireWidth( p, i );
for ( b = 0; b < Width; b++ )
Vec_IntPush( vNew, Count + Width-1-b );
Count += Width;
}
return vNew;
}
Vec_Int_t * Rtl_NtkRevPermOutput( Rtl_Ntk_t * p )
{
Vec_Int_t * vNew = Vec_IntAlloc( 100 ); int b, i, Count = 0;
for ( i = 0; i < p->nOutputs; i++ )
{
int Width = Rtl_WireWidth( p, p->nInputs + i );
for ( b = 0; b < Width; b++ )
Vec_IntPush( vNew, Count + Width-1-b );
Count += Width;
}
return vNew;
}
/**Function*************************************************************
Synopsis []
@ -2693,6 +2729,41 @@ Gia_Man_t * Rtl_ReduceInverse( Rtl_Lib_t * pLib, Gia_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupPermIO( Gia_Man_t * p, Vec_Int_t * vPermI, Vec_Int_t * vPermO )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
assert( Vec_IntSize(vPermI) == Gia_ManCiNum(p) );
assert( Vec_IntSize(vPermO) == Gia_ManCoNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
Gia_ManCi(p, Vec_IntEntry(vPermI, i))->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjIsBuf(pObj) )
pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
else
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
assert( Abc_Lit2Var(pObj->Value) == i );
}
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, Vec_IntEntry(vPermO, i))) );
return pNew;
}
/**Function*************************************************************
Synopsis []
@ -2715,7 +2786,7 @@ int Rtl_LibReturnNtk( Rtl_Lib_t * p, char * pModule )
}
return iNtk;
}
Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose )
{
Gia_Man_t * pGia = NULL;
int NameId = Wln_ReadFindToken( pTopModule, p->pManName );
@ -2733,6 +2804,16 @@ Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
Vec_IntPush( vRoots, iNtk );
Rtl_LibBlast2( p, vRoots, 1 );
pGia = Gia_ManDup( pTop->pGia );
if ( fRev )
{
Gia_Man_t * pTemp;
Vec_Int_t * vPermI = Rtl_NtkRevPermInput( pTop );
Vec_Int_t * vPermO = Rtl_NtkRevPermOutput( pTop );
pGia = Gia_ManDupPermIO( pTemp = pGia, vPermI, vPermO );
Vec_IntFree( vPermI );
Vec_IntFree( vPermO );
Gia_ManStop( pTemp );
}
//Gia_AigerWrite( pGia, "temp_miter.aig", 0, 0, 0 );
if ( pTop->pGia->vBarBufs )
pGia->vBarBufs = Vec_IntDup( pTop->pGia->vBarBufs );

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

@ -139,7 +139,7 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
return 1;
#endif
}
Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose )
Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
{
Rtl_Lib_t * pNtk = NULL;
char Command[1000];
@ -147,8 +147,10 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
int fSVlog = strstr(pFileName, ".sv") != NULL;
if ( strstr(pFileName, ".rtl") )
return Rtl_LibReadFile( pFileName, pFileName );
sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName,
sprintf( Command, "%s -qp \"read_verilog %s %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
Wln_GetYosysName(),
pDefines ? pDefines : "",
fSVlog ? "-sv ":"", pFileName,
pTopModule ? "-top " : "",
pTopModule ? pTopModule : "",
fCollapse ? "flatten; " : "",
@ -167,16 +169,17 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
unlink( pFileTemp );
return pNtk;
}
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
{
Gia_Man_t * pGia = NULL;
char Command[1000];
char * pFileTemp = "_temp_.aig";
int fRtlil = strstr(pFileName, ".rtl") != NULL;
int fSVlog = strstr(pFileName, ".sv") != NULL;
sprintf( Command, "%s -qp \"%s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
sprintf( Command, "%s -qp \"%s %s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? pDefines : "",
fSVlog ? " -sv ":" ",
pFileName,
pTopModule ? "-top " : "-auto-top",

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

@ -140,6 +140,8 @@ struct If_Par_t_
int fUseCofVars; // use cofactoring variables
int fUseAndVars; // use bi-decomposition
int fUseTtPerm; // compute truth tables of the cut functions
int fUseCheck1; // compute truth tables of the cut functions
int fUseCheck2; // compute truth tables of the cut functions
int fDeriveLuts; // enables deriving LUT structures
int fDoAverage; // optimize average rather than maximum level
int fHashMapping; // perform AIG hashing after mapping
@ -553,6 +555,8 @@ extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int n
char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 );
extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
extern int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
extern int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
/*=== ifDelay.c =============================================================*/
extern int If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, Vec_Int_t * vAig, int * piRes, int nSuppAll, int * pArea );

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

@ -767,7 +767,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
(p->pPars->fUseDsd || p->pPars->pFuncCell2 || p->pPars->fUseBat ||
p->pPars->pLutStruct || p->pPars->fUserRecLib || p->pPars->fUserSesLib ||
p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec ||
p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u || p->pPars->fUseCheck1 || p->pPars->fUseCheck2) )
{
If_Cut_t * pFirst = pCutSet->ppCuts[0];
if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )

30
src/map/if/ifDec07.c
View File

@ -1116,6 +1116,36 @@ int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
if ( nLeaves < nVars )
return 1;
assert( nLeaves == nVars );
if ( Abc_Tt6Check1( ((word *)pTruth)[0], nLeaves ) )
return 1;
return 0;
}
int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
if ( nLeaves < nVars )
return 1;
assert( nLeaves == nVars );
if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
return 1;
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -167,7 +167,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
int fFunc0R, fFunc1R;
int i, k, v, iCutDsd, fChange;
int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib ||
p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2;
p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2;
int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0);
assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );

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

@ -72,6 +72,8 @@ void Abc_SclHashCells( SC_Lib * p )
SC_LibForEachCell( p, pCell, i )
{
pPlace = Abc_SclHashLookup( p, pCell->pName );
if ( *pPlace != -1 && pCell->pName )
printf( "There are two standard cells with the same name (%s).\n", pCell->pName );
assert( *pPlace == -1 );
*pPlace = i;
}

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

@ -1589,7 +1589,31 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
Supp |= (1 << v), (*pSuppSize)++;
return Supp;
}
static inline int Abc_Tt6Check1( word t, int nVars )
{
int n, v, u;
for ( n = 0; n < 2; n++ )
for ( v = 0; v < nVars; v++ )
{
word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
for ( u = 0; u < nVars; u++ )
if ( v != u && !Abc_Tt6HasVar(Cof, u) )
return 1;
}
return 0;
}
static inline int Abc_Tt6Check2( word t, int nVars )
{
int n, v;
for ( n = 0; n < 2; n++ )
for ( v = 0; v < nVars; v++ )
{
word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
if ( Cof == 0 || ~Cof == 0 )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks if there is a var whose both cofs have supp <= nSuppLim.]

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

@ -418,7 +418,6 @@ Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
Aig_Man_t * pAig;
Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
pGia = Gia_ManEquivToChoices( pGia, 3 );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;

20
src/proof/cec/cecClass.c
View File

@ -265,10 +265,13 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
SeeAlso []
***********************************************************************/
int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
static int s_Count = 0;
int Cec_ManSimClassRefineOne_rec( Cec_ManSim_t * p, int i )
{
unsigned * pSim0, * pSim1;
int Ent;
s_Count++;
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
@ -290,9 +293,22 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
Cec_ManSimClassCreate( p->pAig, p->vClassOld );
Cec_ManSimClassCreate( p->pAig, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1 + Cec_ManSimClassRefineOne_rec( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
int Cec_ManSimClassRefineOne_( Cec_ManSim_t * p, int i )
{
int Res;
s_Count = 0;
Res = Cec_ManSimClassRefineOne_rec( p, i );
if ( s_Count > 10 )
printf( "%d ", s_Count );
return Res;
}
int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
{
return Cec_ManSimClassRefineOne_rec( p, i );
}
/**Function*************************************************************

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

@ -54,10 +54,14 @@ struct Bmc_EsPar_t_
int fMajority;
int fUseIncr;
int fOnlyAnd;
int fDynConstr;
int fDumpCnf;
int fGlucose;
int fOrderNodes;
int fEnumSols;
int fFewerVars;
int fQuadrEnc;
int fUniqFans;
int RuntimeLim;
int fVerbose;
char * pTtStr;
@ -73,10 +77,14 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
pPars->fMajority = 0;
pPars->fUseIncr = 0;
pPars->fOnlyAnd = 0;
pPars->fDynConstr = 0;
pPars->fDumpCnf = 0;
pPars->fGlucose = 0;
pPars->fOrderNodes = 0;
pPars->fEnumSols = 0;
pPars->fFewerVars = 0;
pPars->fQuadrEnc = 0;
pPars->fUniqFans = 0;
pPars->RuntimeLim = 0;
pPars->fVerbose = 1;
}

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

File diff suppressed because it is too large Load Diff