mirror of https://github.com/YosysHQ/abc.git
Version abc80729
This commit is contained in:
Alan Mishchenko
parent
20a5a0d4af
commit
582a059e34
2
Makefile
2
Makefile
|
|
@ -25,7 +25,7 @@ MODULES := \
|
|||
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
|
||||
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
|
||||
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr \
|
||||
src/aig/int
|
||||
src/aig/int src/aig/dch
|
||||
|
||||
default: $(PROG)
|
||||
|
||||
|
|
|
|||
36
abc.dsp
36
abc.dsp
|
|
@ -42,7 +42,7 @@ RSC=rc.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
|
||||
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
|
||||
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
||||
# ADD RSC /l 0x409 /d "NDEBUG"
|
||||
BSC32=bscmake.exe
|
||||
|
|
@ -66,7 +66,7 @@ LINK32=link.exe
|
|||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
|
||||
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
|
||||
# SUBTRACT CPP /X
|
||||
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
||||
# ADD RSC /l 0x409 /d "_DEBUG"
|
||||
|
|
@ -3273,6 +3273,38 @@ SOURCE=.\src\aig\int\intMan.c
|
|||
SOURCE=.\src\aig\int\intUtil.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "dch"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dch.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchAig.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchCore.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchSat.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\dch\dchSim.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "Header Files"
|
||||
|
|
|
|||
3
readme
3
readme
|
|
@ -15,6 +15,9 @@ To compile with Microsoft Visual Studio higher than 6.0,
|
|||
remove ABC_CHECK_LEAKS from the preprocessor definitions
|
||||
for the debug version (Project->Settings->C/C++->Preprocessor Definitions)
|
||||
|
||||
If compilation does not start because of the cyclic dependency check,
|
||||
try "touching" all files: find ./ -type f -exec touch "{}" \;
|
||||
|
||||
Several things to try if it does not compile on your platform:
|
||||
- Try running all code (not only Makefile and depends.sh) through dos2unix
|
||||
- Try the following actions:
|
||||
|
|
|
|||
|
|
@ -0,0 +1,72 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dch.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __DCH_H__
|
||||
#define __DCH_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// choicing parameters
|
||||
typedef struct Dch_Pars_t_ Dch_Pars_t;
|
||||
struct Dch_Pars_t_
|
||||
{
|
||||
int nWords; // the number of simulation words
|
||||
int nBTLimit; // conflict limit at a node
|
||||
int nSatVarMax; // the max number of SAT variables
|
||||
int fVerbose; // verbose stats
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== dchCore.c ==========================================================*/
|
||||
extern void Dch_ManSetDefaultParams( Dch_Pars_t * p );
|
||||
extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,186 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchAig.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [AIG manipulation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dchInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the cumulative AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj->pData )
|
||||
return;
|
||||
Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) );
|
||||
Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) );
|
||||
pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the cumulative AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
|
||||
{
|
||||
Aig_Man_t * pAig, * pAig2, * pAigTotal;
|
||||
Aig_Obj_t * pObj, * pObjPi, * pObjPo;
|
||||
int i, k, nNodes;
|
||||
assert( Vec_PtrSize(vAigs) > 0 );
|
||||
// make sure they have the same number of PIs/POs
|
||||
nNodes = 0;
|
||||
pAig = Vec_PtrEntry( vAigs, 0 );
|
||||
Vec_PtrForEachEntry( vAigs, pAig2, i )
|
||||
{
|
||||
assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
|
||||
assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
|
||||
nNodes += Aig_ManNodeNum(pAig);
|
||||
Aig_ManCleanData( pAig2 );
|
||||
}
|
||||
// map constant nodes
|
||||
pAigTotal = Aig_ManStart( nNodes );
|
||||
Vec_PtrForEachEntry( vAigs, pAig2, k )
|
||||
Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
|
||||
// map primary inputs
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
{
|
||||
pObjPi = Aig_ObjCreatePi( pAigTotal );
|
||||
Vec_PtrForEachEntry( vAigs, pAig2, k )
|
||||
Aig_ManPi( pAig2, i )->pData = pObjPi;
|
||||
}
|
||||
// construct the AIG in the order of POs
|
||||
Aig_ManForEachPo( pAig, pObj, i )
|
||||
{
|
||||
Vec_PtrForEachEntry( vAigs, pAig2, k )
|
||||
{
|
||||
pObjPo = Aig_ManPo( pAig2, i );
|
||||
Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
|
||||
}
|
||||
Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) );
|
||||
}
|
||||
// mark the cone of the first AIG
|
||||
Aig_ManIncrementTravId( pAigTotal );
|
||||
Aig_ManForEachObj( pAig, pObj, i )
|
||||
if ( pObj->pData )
|
||||
Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
|
||||
// cleanup should not be done
|
||||
return pAigTotal;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the AIG with choices from representatives.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_DeriveChoiceAig_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj )
|
||||
{
|
||||
Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
|
||||
if ( pObj->pData )
|
||||
return;
|
||||
// construct AIG for the representative
|
||||
pRepr = pOld->pReprs[pObj->Id];
|
||||
if ( pRepr != NULL )
|
||||
Dch_DeriveChoiceAig_rec( pNew, pOld, pRepr );
|
||||
// skip choices with combinatinal loops
|
||||
if ( Aig_ObjCheckTfi( pOld, pObj, pRepr ) )
|
||||
{
|
||||
pOld->pReprs[pObj->Id] = NULL;
|
||||
return;
|
||||
}
|
||||
Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin0(pObj) );
|
||||
Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin1(pObj) );
|
||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
if ( pRepr == NULL )
|
||||
return;
|
||||
// add choice
|
||||
assert( pObj->nRefs == 0 );
|
||||
pObjNew = pObj->pData;
|
||||
pReprNew = pRepr->pData;
|
||||
pNew->pEquivs[pObjNew->Id] = pNew->pEquivs[pReprNew->Id];
|
||||
pNew->pEquivs[pReprNew->Id] = pObjNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the AIG with choices from representatives.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
|
||||
{
|
||||
Aig_Man_t * pChoices;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
// start recording equivalences
|
||||
pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
|
||||
pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
|
||||
// map constants and PIs
|
||||
Aig_ManCleanData( pAig );
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pChoices );
|
||||
// construct choice nodes from the POs
|
||||
assert( pAig->pReprs != NULL );
|
||||
Aig_ManForEachPo( pAig, pObj, i )
|
||||
{
|
||||
Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) );
|
||||
Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) );
|
||||
}
|
||||
// there is no need for cleanup
|
||||
return pChoices;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,98 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchCore.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [The core procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dchInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_ManSetDefaultParams( Dch_Pars_t * p )
|
||||
{
|
||||
memset( p, 0, sizeof(Dch_Pars_t) );
|
||||
p->nWords = 4; // the number of simulation words
|
||||
p->nBTLimit = 1000; // conflict limit at a node
|
||||
p->nSatVarMax = 5000; // the max number of SAT variables
|
||||
p->fVerbose = 1; // verbose stats
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs computation of AIGs with choices.]
|
||||
|
||||
Description [Takes several AIGs and performs choicing.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
|
||||
{
|
||||
Dch_Man_t * p;
|
||||
Aig_Man_t * pResult;
|
||||
int i;
|
||||
|
||||
assert( Vec_PtrSize(vAigs) > 0 );
|
||||
|
||||
printf( "AIGs considered for choicing:\n" );
|
||||
Vec_PtrForEachEntry( vAigs, pResult, i )
|
||||
{
|
||||
Aig_ManPrintStats( pResult );
|
||||
}
|
||||
|
||||
// start the choicing manager
|
||||
p = Dch_ManCreate( vAigs, pPars );
|
||||
// compute candidate equivalence classes
|
||||
p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose );
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// create choices
|
||||
// pResult = Dch_DeriveChoiceAig( p->pAigTotal );
|
||||
Aig_ManCleanup( p->pAigTotal );
|
||||
pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
|
||||
|
||||
Dch_ManStop( p );
|
||||
return pResult;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,102 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchInt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __DCH_INT_H__
|
||||
#define __DCH_INT_H__
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "aig.h"
|
||||
#include "satSolver.h"
|
||||
#include "dch.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// equivalence classes
|
||||
typedef struct Dch_Cla_t_ Dch_Cla_t;
|
||||
struct Dch_Cla_t_
|
||||
{
|
||||
int nNodes; // the number of nodes in the class
|
||||
int pNodes[0]; // the nodes of the class
|
||||
};
|
||||
|
||||
// choicing manager
|
||||
typedef struct Dch_Man_t_ Dch_Man_t;
|
||||
struct Dch_Man_t_
|
||||
{
|
||||
// parameters
|
||||
Dch_Pars_t * pPars;
|
||||
// AIGs used in the package
|
||||
Vec_Ptr_t * vAigs; // user-given AIGs
|
||||
Aig_Man_t * pAigTotal; // intermediate AIG
|
||||
Aig_Man_t * pAigFraig; // final AIG
|
||||
// equivalence classes
|
||||
Dch_Cla_t ** ppClasses; // classes for representative nodes
|
||||
// SAT solving
|
||||
sat_solver * pSat; // recyclable SAT solver
|
||||
Vec_Int_t ** ppSatVars; // SAT variables for used nodes
|
||||
Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
|
||||
// runtime stats
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== dchAig.c =====================================================*/
|
||||
extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
|
||||
extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig );
|
||||
|
||||
/*=== dchMan.c =====================================================*/
|
||||
extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
|
||||
extern void Dch_ManStop( Dch_Man_t * p );
|
||||
|
||||
/*=== dchSat.c =====================================================*/
|
||||
|
||||
/*=== dchSim.c =====================================================*/
|
||||
extern Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,102 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchMan.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Computation of equivalence classes using simulation.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dchInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates the interpolation manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
|
||||
{
|
||||
Dch_Man_t * p;
|
||||
// create interpolation manager
|
||||
p = ALLOC( Dch_Man_t, 1 );
|
||||
memset( p, 0, sizeof(Dch_Man_t) );
|
||||
p->pPars = pPars;
|
||||
// AIGs
|
||||
p->vAigs = vAigs;
|
||||
p->pAigTotal = Dch_DeriveTotalAig( vAigs );
|
||||
// equivalence classes
|
||||
Aig_ManReprStart( p->pAigTotal, Aig_ManObjNumMax(p->pAigTotal) );
|
||||
// SAT solving
|
||||
p->ppSatVars = CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAigTotal) );
|
||||
p->vUsedNodes = Vec_PtrAlloc( 1000 );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the interpolation manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_ManStop( Dch_Man_t * p )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
{
|
||||
/*
|
||||
p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
|
||||
printf( "Runtime statistics:\n" );
|
||||
PRTP( "Rewriting ", p->timeRwr, p->timeTotal );
|
||||
PRTP( "CNF mapping", p->timeCnf, p->timeTotal );
|
||||
PRTP( "SAT solving", p->timeSat, p->timeTotal );
|
||||
PRTP( "Interpol ", p->timeInt, p->timeTotal );
|
||||
PRTP( "Containment", p->timeEqu, p->timeTotal );
|
||||
PRTP( "Other ", p->timeOther, p->timeTotal );
|
||||
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
|
||||
*/
|
||||
}
|
||||
if ( p->pAigTotal )
|
||||
Aig_ManStop( p->pAigTotal );
|
||||
if ( p->pAigFraig )
|
||||
Aig_ManStop( p->pAigFraig );
|
||||
FREE( p->ppClasses );
|
||||
FREE( p->ppSatVars );
|
||||
Vec_PtrFree( p->vUsedNodes );
|
||||
free( p );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchSat.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Choice computation for tech-mapping.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dchInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,225 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dchSim.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Computation of equivalence classes using simulation.]
|
||||
|
||||
Synopsis [Calls to the SAT solver.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 29, 2008.]
|
||||
|
||||
Revision [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dchInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj )
|
||||
{
|
||||
return Vec_PtrEntry( vSims, pObj->Id );
|
||||
}
|
||||
static inline unsigned Dch_ObjRandomSim()
|
||||
{
|
||||
return Aig_ManRandom(0);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Perform random simulation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
|
||||
{
|
||||
unsigned * pSim, * pSim0, * pSim1;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, k;
|
||||
|
||||
// assign const 1 sim info
|
||||
pObj = Aig_ManConst1(pAig);
|
||||
pSim = Dch_ObjSim( vSims, pObj );
|
||||
memset( pSim, 0xff, sizeof(unsigned) * nWords );
|
||||
|
||||
// assign primary input random sim info
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Dch_ObjSim( vSims, pObj );
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
pSim[k] = Dch_ObjRandomSim();
|
||||
}
|
||||
|
||||
// simulate AIG in the topological order
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
{
|
||||
pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) );
|
||||
pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) );
|
||||
pSim = Dch_ObjSim( vSims, pObj );
|
||||
|
||||
if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
|
||||
{
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
pSim[k] = ~pSim0[k] & ~pSim1[k];
|
||||
}
|
||||
else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
|
||||
{
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
pSim[k] = ~pSim0[k] & pSim1[k];
|
||||
}
|
||||
else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
|
||||
{
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
pSim[k] = pSim0[k] & ~pSim1[k];
|
||||
}
|
||||
else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
|
||||
{
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
pSim[k] = pSim0[k] & pSim1[k];
|
||||
}
|
||||
}
|
||||
|
||||
// get simulation information for primary outputs
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Hashing nodes by sim info.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
|
||||
{
|
||||
unsigned * pSim0, * pSim1;
|
||||
Aig_Obj_t * pObj, * pUnique;
|
||||
int i, k, j, nodeId, Counter, c, CountNodes;
|
||||
|
||||
Vec_Int_t * vUniqueNodes, * vNodeCounters;
|
||||
|
||||
vUniqueNodes = Vec_IntAlloc( 1000 );
|
||||
vNodeCounters = Vec_IntStart( Aig_ManObjNumMax(pAig) );
|
||||
|
||||
Aig_ManForEachObj( pAig, pObj, i )
|
||||
{
|
||||
if ( Aig_ObjIsPo(pObj) )
|
||||
continue;
|
||||
|
||||
// node's sim info
|
||||
pSim0 = Dch_ObjSim( vSims, pObj );
|
||||
|
||||
Vec_IntForEachEntry( vUniqueNodes, nodeId, j )
|
||||
{
|
||||
pUnique = Aig_ManObj( pAig, nodeId );
|
||||
// unique node's sim info
|
||||
pSim1 = Dch_ObjSim( vSims, pUnique );
|
||||
|
||||
for ( k = 0; k < nWords; k++ )
|
||||
if ( pSim0[k] != pSim1[k] )
|
||||
break;
|
||||
if ( k == nWords ) // sim info is same as this node
|
||||
{
|
||||
Counter = Vec_IntEntry( vNodeCounters, nodeId );
|
||||
Vec_IntWriteEntry( vNodeCounters, nodeId, Counter+1 );
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if ( j == Vec_IntSize(vUniqueNodes) ) // sim info of pObj is unique
|
||||
{
|
||||
Vec_IntPush( vUniqueNodes, pObj->Id );
|
||||
|
||||
Counter = Vec_IntEntry( vNodeCounters, pObj->Id );
|
||||
assert( Counter == 0 );
|
||||
Vec_IntWriteEntry( vNodeCounters, pObj->Id, Counter+1 );
|
||||
}
|
||||
}
|
||||
|
||||
Counter = 0;
|
||||
Vec_IntForEachEntry( vNodeCounters, c, k )
|
||||
if ( c > 1 )
|
||||
Counter++;
|
||||
|
||||
|
||||
printf( "Detected %d non-trivial candidate equivalence classes for %d nodes.\n",
|
||||
Counter, Vec_IntSize(vUniqueNodes) );
|
||||
|
||||
CountNodes = 0;
|
||||
Vec_IntForEachEntry( vUniqueNodes, nodeId, k )
|
||||
{
|
||||
if ( Vec_IntEntry( vNodeCounters, nodeId ) == 1 )
|
||||
continue;
|
||||
// printf( "%d ", Vec_IntEntry( vNodeCounters, nodeId ) );
|
||||
CountNodes += Vec_IntEntry( vNodeCounters, nodeId );
|
||||
}
|
||||
// printf( "\n" );
|
||||
printf( "Nodes participating in non-trivial classes = %d.\n", CountNodes );
|
||||
|
||||
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives candidate equivalence classes of AIG nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose )
|
||||
{
|
||||
Dch_Cla_t ** ppClasses; // place for equivalence classes
|
||||
Aig_MmFlex_t * pMemCla; // memory for equivalence classes
|
||||
Vec_Ptr_t * vSims;
|
||||
|
||||
// start storage for equivalence classes
|
||||
ppClasses = CALLOC( Dch_Cla_t *, Aig_ManObjNumMax(pAig) );
|
||||
pMemCla = Aig_MmFlexStart();
|
||||
|
||||
// allocate simulation information
|
||||
vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
|
||||
|
||||
// run simulation
|
||||
Dch_PerformRandomSimulation( pAig, vSims, nWords );
|
||||
|
||||
// hash nodes by sim info
|
||||
Dch_HashNodesBySimulationInfo( pAig, vSims, nWords );
|
||||
|
||||
// collect equivalence classes
|
||||
// ppClasses = NULL;
|
||||
|
||||
// clean up and return
|
||||
Aig_MmFlexStop( pMemCla, 0 );
|
||||
Vec_PtrFree( vSims );
|
||||
return ppClasses;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
SRC += src/aig/dch/dchAig.c \
|
||||
src/aig/dch/dchCore.c \
|
||||
src/aig/dch/dchMan.c \
|
||||
src/aig/dch/dchSat.c \
|
||||
src/aig/dch/dchSim.c
|
||||
|
|
@ -38,7 +38,7 @@
|
|||
SAT solver run may return a counter-ex that distinguishes the given
|
||||
representative node from the constant-1 node but this counter-ex
|
||||
does not distinguish the nodes in the non-costant class... This is why
|
||||
there is no check of refinment after a counter-ex in the sequential case.
|
||||
there is no check of refinement after a counter-ex in the sequential case.
|
||||
*/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -410,7 +410,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
|
|||
}
|
||||
// perform partitioning
|
||||
if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
|
||||
|| (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 1) )
|
||||
|| (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0) )
|
||||
return Fra_FraigInductionPart( pManAig, pParams );
|
||||
|
||||
nNodesBeg = Aig_ManNodeNum(pManAig);
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ extern "C" {
|
|||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// simulation manager
|
||||
// interpolation manager
|
||||
typedef struct Inter_Man_t_ Inter_Man_t;
|
||||
struct Inter_Man_t_
|
||||
{
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@
|
|||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the interpolation manager.]
|
||||
Synopsis [Creates the interpolation manager.]
|
||||
|
||||
Description []
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
|
|||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees the interpolation manager.]
|
||||
Synopsis [Cleans the interpolation manager.]
|
||||
|
||||
Description []
|
||||
|
||||
|
|
|
|||
|
|
@ -649,7 +649,11 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
|
|||
if ( pAig->vClockDoms )
|
||||
{
|
||||
if ( Vec_VecSize(pAig->vClockDoms) == 0 )
|
||||
printf( "Register classes are small. Seq synthesis is not performed.\n" );
|
||||
{
|
||||
printf( "Register classes are below the limit (%d). Seq synthesis is not performed.\n", nMinDomSize );
|
||||
Aig_ManStop( pAig );
|
||||
pAig = NULL;
|
||||
}
|
||||
else
|
||||
printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
|
||||
printf( "\n" );
|
||||
|
|
|
|||
|
|
@ -29,6 +29,80 @@
|
|||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Remaps representatives of the equivalence classes.]
|
||||
|
||||
Description [For each equivalence class, if the current representative
|
||||
of the class cannot be used because its corresponding net has no-merge
|
||||
attribute, find the topologically-shallowest node, which can be used
|
||||
as a representative.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Ntl_ManUpdateNoMergeReprs( Aig_Man_t * pAig, Aig_Obj_t ** pReprs )
|
||||
{
|
||||
Aig_Obj_t ** pReprsNew = NULL;
|
||||
Aig_Obj_t * pObj, * pRepres, * pRepresNew;
|
||||
Ntl_Net_t * pNet, * pNetObj;
|
||||
int i;
|
||||
|
||||
// allocate room for the new representative
|
||||
pReprsNew = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
|
||||
memset( pReprsNew, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
|
||||
Aig_ManForEachObj( pAig, pObj, i )
|
||||
{
|
||||
// get the old representative node
|
||||
pRepres = pReprs[pObj->Id];
|
||||
if ( pRepres == NULL )
|
||||
continue;
|
||||
// if this representative node is already remapped, skip it
|
||||
pRepresNew = pReprsNew[ pRepres->Id ];
|
||||
if ( pRepresNew != NULL )
|
||||
continue;
|
||||
// get the net of the representative node
|
||||
pNet = pRepres->pData;
|
||||
assert( pRepres->pData != NULL );
|
||||
if ( Ntl_ObjIsBox(pNet->pDriver) && pNet->pDriver->pImplem->attrNoMerge )
|
||||
{
|
||||
// the net belongs to the no-merge box
|
||||
pNetObj = pObj->pData;
|
||||
if ( Ntl_ObjIsBox(pNetObj->pDriver) && pNetObj->pDriver->pImplem->attrNoMerge )
|
||||
continue;
|
||||
// the object's net does not belong to the no-merge box
|
||||
// pObj can be used instead of pRepres
|
||||
pReprsNew[ pRepres->Id ] = pObj;
|
||||
}
|
||||
else
|
||||
{
|
||||
// otherwise, it is fine to use pRepres
|
||||
pReprsNew[ pRepres->Id ] = pRepres;
|
||||
}
|
||||
}
|
||||
// update the representatives
|
||||
Aig_ManForEachObj( pAig, pObj, i )
|
||||
{
|
||||
// get the representative node
|
||||
pRepres = pReprs[ pObj->Id ];
|
||||
if ( pRepres == NULL )
|
||||
continue;
|
||||
// if the representative has no mapping, undo the mapping of the node
|
||||
pRepresNew = pReprsNew[ pRepres->Id ];
|
||||
if ( pRepresNew == NULL || pRepresNew == pObj )
|
||||
{
|
||||
pReprs[ pObj->Id ] = NULL;
|
||||
continue;
|
||||
}
|
||||
// remap the representative
|
||||
assert( pObj->Id > pRepresNew->Id );
|
||||
pReprs[ pObj->Id ] = pRepresNew;
|
||||
}
|
||||
free( pReprsNew );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Transfers equivalence class info from pAigCol to pAig.]
|
||||
|
|
@ -112,6 +186,10 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
|
|||
// recall pointers to the nets of pNew
|
||||
Aig_ManForEachObj( pAig, pObj, i )
|
||||
pObj->pData = pObj->pNext, pObj->pNext = NULL;
|
||||
|
||||
// remap no-merge representatives to point to
|
||||
// the shallowest nodes in the class without no-merge
|
||||
Ntl_ManUpdateNoMergeReprs( pAig, pReprs );
|
||||
return pReprs;
|
||||
}
|
||||
|
||||
|
|
@ -156,7 +234,8 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
|
|||
if ( pNet->pDriver->pImplem->attrNoMerge )
|
||||
continue;
|
||||
// do not reduce the net if the replacement net has no-merge attribute
|
||||
if ( pNetRepr != NULL && pNetRepr->pDriver->pImplem->attrNoMerge )
|
||||
if ( pNetRepr != NULL && Ntl_ObjIsBox(pNetRepr->pDriver) &&
|
||||
pNetRepr->pDriver->pImplem->attrNoMerge )
|
||||
continue;
|
||||
}
|
||||
if ( pNetRepr == NULL )
|
||||
|
|
@ -393,6 +472,11 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
|
|||
pAig = Ntl_ManExtract( p );
|
||||
pNew = Ntl_ManInsertAig( p, pAig );
|
||||
pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
|
||||
if ( pAigCol == NULL )
|
||||
{
|
||||
Aig_ManStop( pAig );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
// perform SCL for the given design
|
||||
pTemp = Fra_FraigInduction( pAigCol, pPars );
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Network and node package.]
|
||||
|
||||
|
||||
Synopsis [Command file.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
|
@ -35,6 +35,7 @@
|
|||
#include "saig.h"
|
||||
#include "nwkMerge.h"
|
||||
#include "int.h"
|
||||
#include "dch.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -135,6 +136,7 @@ static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg
|
|||
static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDch ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -398,6 +400,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "dchoice", Abc_CommandDChoice, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "dch", Abc_CommandDch, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
|
||||
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
|
||||
|
|
@ -8932,6 +8935,110 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Dch_Pars_t Pars, * pPars = &Pars;
|
||||
FILE * pOut, * pErr;
|
||||
Abc_Ntk_t * pNtk, * pNtkRes;
|
||||
int c;
|
||||
|
||||
extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
Dch_ManSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'W':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nWords = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nWords < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nBTLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'S':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nSatVarMax < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pErr, "Empty network.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
fprintf( pErr, "This command works only for strashed networks.\n" );
|
||||
return 1;
|
||||
}
|
||||
pNtkRes = Abc_NtkDch( pNtk, pPars );
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Command has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: dch [-WCS num] [-vh]\n" );
|
||||
fprintf( pErr, "\t performs computation of structural choices\n" );
|
||||
fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
|
||||
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
|
||||
fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
|
||||
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -16328,7 +16435,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
|
||||
extern void * Ntl_ManDup( void * pOld );
|
||||
extern void Ntl_ManFree( void * p );
|
||||
extern Aig_Man_t * Ntl_ManCollapseSeq( void * p );
|
||||
extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize );
|
||||
|
||||
// set defaults
|
||||
fAig = 0;
|
||||
|
|
@ -16361,7 +16468,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
if ( fCollapsed )
|
||||
{
|
||||
pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl );
|
||||
pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 );
|
||||
Saig_ManDumpBlif( pTemp, pFileName );
|
||||
Aig_ManStop( pTemp );
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@
|
|||
#include "fra.h"
|
||||
#include "fraig.h"
|
||||
#include "int.h"
|
||||
#include "dch.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -815,6 +816,42 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
|
|||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Gives the current ABC network to AIG manager for processing.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
|
||||
{
|
||||
extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
|
||||
|
||||
Vec_Ptr_t * vAigs;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
int i;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
pMan = Abc_NtkToDar( pNtk, 0, 0 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
|
||||
Aig_ManStop( pMan );
|
||||
pMan = Dch_ComputeChoices( vAigs, pPars );
|
||||
// pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
|
||||
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
|
||||
Aig_ManStop( pMan );
|
||||
// cleanup
|
||||
Vec_PtrForEachEntry( vAigs, pTemp, i )
|
||||
Aig_ManStop( pTemp );
|
||||
Vec_PtrFree( vAigs );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Gives the current ABC network to AIG manager for processing.]
|
||||
|
|
|
|||
Loading…
Reference in New Issue