diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abc/abc.h | 76 | ||||
-rw-r--r-- | src/base/abc/abcNtk.c | 592 | ||||
-rw-r--r-- | src/base/abc/abcObj.c (renamed from src/base/abc/abcCreate.c) | 538 | ||||
-rw-r--r-- | src/base/abc/module.make | 33 | ||||
-rw-r--r-- | src/base/abci/abc.c (renamed from src/base/abc/abc.c) | 112 | ||||
-rw-r--r-- | src/base/abci/abcAttach.c (renamed from src/base/abc/abcAttach.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcBalance.c (renamed from src/base/abc/abcBalance.c) | 23 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c (renamed from src/base/abc/abcCollapse.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcCut.c (renamed from src/base/abc/abcCut.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcDsd.c (renamed from src/base/abc/abcDsd.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcFpga.c (renamed from src/base/abc/abcFpga.c) | 35 | ||||
-rw-r--r-- | src/base/abci/abcFraig.c (renamed from src/base/abc/abcFraig.c) | 21 | ||||
-rw-r--r-- | src/base/abci/abcFxu.c (renamed from src/base/abc/abcFxu.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcMap.c (renamed from src/base/abc/abcMap.c) | 37 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c (renamed from src/base/abc/abcMiter.c) | 16 | ||||
-rw-r--r-- | src/base/abci/abcNtbdd.c (renamed from src/base/abc/abcNtbdd.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c (renamed from src/base/abc/abcPrint.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcReconv.c (renamed from src/base/abc/abcReconv.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcRefactor.c (renamed from src/base/abc/abcRefactor.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcRenode.c (renamed from src/base/abc/abcRenode.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c (renamed from src/base/abc/abcRewrite.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcSat.c (renamed from src/base/abc/abcSat.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c (renamed from src/base/abc/abcStrash.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcSweep.c (renamed from src/base/abc/abcSweep.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcSymm.c (renamed from src/base/abc/abcSymm.c) | 21 | ||||
-rw-r--r-- | src/base/abci/abcTiming.c (renamed from src/base/abc/abcTiming.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcUnreach.c (renamed from src/base/abc/abcUnreach.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c (renamed from src/base/abc/abcVerify.c) | 0 | ||||
-rw-r--r-- | src/base/abci/abc_.c (renamed from src/sat/sim/simSym.c) | 7 | ||||
-rw-r--r-- | src/base/abci/module.make | 24 | ||||
-rw-r--r-- | src/base/abcs/abcRetime.c (renamed from src/base/abc/abcSeqRetime.c) | 0 | ||||
-rw-r--r-- | src/base/abcs/abcSeq.c (renamed from src/base/abc/abcSeq.c) | 0 | ||||
-rw-r--r-- | src/base/abcs/abc_.c (renamed from src/sat/sim/simUnate.c) | 7 | ||||
-rw-r--r-- | src/base/abcs/module.make | 2 | ||||
-rw-r--r-- | src/base/io/ioWriteDot_old.c | 325 | ||||
-rw-r--r-- | src/map/fpga/fpga.h | 2 | ||||
-rw-r--r-- | src/map/fpga/fpgaCore.c | 41 | ||||
-rw-r--r-- | src/map/fpga/fpgaCreate.c | 2 | ||||
-rw-r--r-- | src/map/fpga/fpgaCutUtils.c | 103 | ||||
-rw-r--r-- | src/map/fpga/fpgaInt.h | 17 | ||||
-rw-r--r-- | src/map/fpga/fpgaMatch.c | 2 | ||||
-rw-r--r-- | src/map/fpga/fpgaSwitch.c | 176 | ||||
-rw-r--r-- | src/map/fpga/fpgaUtils.c | 37 | ||||
-rw-r--r-- | src/map/fpga/module.make | 1 | ||||
-rw-r--r-- | src/map/mapper/mapper.h | 2 | ||||
-rw-r--r-- | src/map/mapper/mapperCore.c | 83 | ||||
-rw-r--r-- | src/map/mapper/mapperCreate.c | 6 | ||||
-rw-r--r-- | src/map/mapper/mapperInt.h | 8 | ||||
-rw-r--r-- | src/map/mapper/mapperLib.c | 1 | ||||
-rw-r--r-- | src/map/mapper/mapperMatch.c | 34 | ||||
-rw-r--r-- | src/map/mapper/mapperRefs.c | 9 | ||||
-rw-r--r-- | src/map/mapper/mapperSwitch.c | 243 | ||||
-rw-r--r-- | src/map/mapper/module.make | 1 | ||||
-rw-r--r-- | src/map/mio/mio.h | 1 | ||||
-rw-r--r-- | src/map/mio/mioApi.c | 17 | ||||
-rw-r--r-- | src/misc/mvc/module.make | 16 | ||||
-rw-r--r-- | src/misc/mvc/mvc.c (renamed from src/sop/mvc/mvc.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvc.h (renamed from src/sop/mvc/mvc.h) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcApi.c (renamed from src/sop/mvc/mvcApi.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcCompare.c (renamed from src/sop/mvc/mvcCompare.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcContain.c (renamed from src/sop/mvc/mvcContain.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcCover.c (renamed from src/sop/mvc/mvcCover.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcCube.c (renamed from src/sop/mvc/mvcCube.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcDivide.c (renamed from src/sop/mvc/mvcDivide.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcDivisor.c (renamed from src/sop/mvc/mvcDivisor.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcList.c (renamed from src/sop/mvc/mvcList.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcLits.c (renamed from src/sop/mvc/mvcLits.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcMan.c (renamed from src/sop/mvc/mvcMan.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcOpAlg.c (renamed from src/sop/mvc/mvcOpAlg.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcOpBool.c (renamed from src/sop/mvc/mvcOpBool.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcPrint.c (renamed from src/sop/mvc/mvcPrint.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcSort.c (renamed from src/sop/mvc/mvcSort.c) | 0 | ||||
-rw-r--r-- | src/misc/mvc/mvcUtils.c (renamed from src/sop/mvc/mvcUtils.c) | 0 | ||||
-rw-r--r-- | src/misc/vec/vecInt.h | 41 | ||||
-rw-r--r-- | src/misc/vec/vecPtr.h | 62 | ||||
-rw-r--r-- | src/misc/vec/vecStr.h | 20 | ||||
-rw-r--r-- | src/misc/vec/vecVec.h | 3 | ||||
-rw-r--r-- | src/opt/sim/module.make | 9 | ||||
-rw-r--r-- | src/opt/sim/sim.h (renamed from src/sat/sim/sim.h) | 110 | ||||
-rw-r--r-- | src/opt/sim/simMan.c (renamed from src/sat/sim/simMan.c) | 178 | ||||
-rw-r--r-- | src/opt/sim/simSat.c (renamed from src/sat/sim/simSat.c) | 0 | ||||
-rw-r--r-- | src/opt/sim/simSupp.c | 594 | ||||
-rw-r--r-- | src/opt/sim/simSwitch.c | 107 | ||||
-rw-r--r-- | src/opt/sim/simSym.c | 93 | ||||
-rw-r--r-- | src/opt/sim/simSymSat.c | 202 | ||||
-rw-r--r-- | src/opt/sim/simSymSim.c | 159 | ||||
-rw-r--r-- | src/opt/sim/simSymStr.c | 481 | ||||
-rw-r--r-- | src/opt/sim/simUtils.c (renamed from src/sat/sim/simUtils.c) | 224 | ||||
-rw-r--r-- | src/sat/fraig/fraig.h | 1 | ||||
-rw-r--r-- | src/sat/fraig/fraigApi.c | 8 | ||||
-rw-r--r-- | src/sat/fraig/fraigFeed.c | 116 | ||||
-rw-r--r-- | src/sat/fraig/fraigInt.h | 14 | ||||
-rw-r--r-- | src/sat/fraig/fraigMan.c | 1 | ||||
-rw-r--r-- | src/sat/fraig/fraigSat.c | 18 | ||||
-rw-r--r-- | src/sat/fraig/fraigTable.c | 52 | ||||
-rw-r--r-- | src/sat/fraig/fraigUtil.c | 65 | ||||
-rw-r--r-- | src/sat/sim/module.make | 6 | ||||
-rw-r--r-- | src/sat/sim/simSupp.c | 273 | ||||
-rw-r--r-- | src/seq/module.make | 1 | ||||
-rw-r--r-- | src/sop/mvc/module.make | 16 |
100 files changed, 3819 insertions, 1706 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 81a1c328..bff4f9f1 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -165,6 +165,8 @@ struct Abc_Ntk_t_ // level information (for AIGs) int LevelMax; // maximum number of levels Vec_Int_t * vLevelsR; // level in the reverse topological order + // support information + Vec_Ptr_t * vSupps; // the external don't-care if given Abc_Ntk_t * pExdc; // the EXDC network // miscellaneous data members @@ -415,39 +417,6 @@ extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ); -/*=== abcCreate.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); -extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); -extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkStartRead( char * pName ); -extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); -extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); -extern Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); -extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); -extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); -extern Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); -extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); -extern Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); -extern Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); -extern Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); -extern Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 ); -extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ); /*=== abcCut.c ==========================================================*/ extern void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj ); extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj ); @@ -486,7 +455,6 @@ extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ); extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ); /*=== abcMap.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose ); extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); /*=== abcMiter.c ==========================================================*/ extern int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk ); @@ -495,11 +463,35 @@ extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ); extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode ); /*=== abcMiter.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); -extern Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ); +extern Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ); extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ); extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ); +/*=== abcObj.c ==========================================================*/ +extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); +extern void Abc_ObjAdd( Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); +extern Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); +extern Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); +extern Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); +extern Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); +extern Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 ); +extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ); /*=== abcNames.c ====================================================*/ extern char * Abc_NtkRegisterName( Abc_Ntk_t * pNtk, char * pName ); extern char * Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pName, char * pSuffix ); @@ -529,6 +521,20 @@ extern Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, extern Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ); extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly ); extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); +/*=== abcNtk.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); +extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); +extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkStartRead( char * pName ); +extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); +extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); +extern Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); +extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); +extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); /*=== abcPrint.c ==========================================================*/ extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ); extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c new file mode 100644 index 00000000..5c199141 --- /dev/null +++ b/src/base/abc/abcNtk.c @@ -0,0 +1,592 @@ +/**CFile**************************************************************** + + FileName [abcNtk.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Network creation/duplication/deletion procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcNtk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "main.h" +#include "mio.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ABC_NUM_STEPS 10 + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates a new Ntk.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ) +{ + Abc_Ntk_t * pNtk; + pNtk = ALLOC( Abc_Ntk_t, 1 ); + memset( pNtk, 0, sizeof(Abc_Ntk_t) ); + pNtk->ntkType = Type; + pNtk->ntkFunc = Func; + // start the object storage + pNtk->vObjs = Vec_PtrAlloc( 100 ); + pNtk->vLats = Vec_PtrAlloc( 100 ); + pNtk->vCis = Vec_PtrAlloc( 100 ); + pNtk->vCos = Vec_PtrAlloc( 100 ); + pNtk->vPtrTemp = Vec_PtrAlloc( 100 ); + pNtk->vIntTemp = Vec_IntAlloc( 100 ); + pNtk->vStrTemp = Vec_StrAlloc( 100 ); + // start the hash table + pNtk->tName2Net = stmm_init_table(strcmp, stmm_strhash); + pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + // start the memory managers + pNtk->pMmNames = Extra_MmFlexStart(); + pNtk->pMmObj = Extra_MmFixedStart( sizeof(Abc_Obj_t) ); + pNtk->pMmStep = Extra_MmStepStart( ABC_NUM_STEPS ); + // get ready to assign the first Obj ID + pNtk->nTravIds = 1; + // start the functionality manager + if ( Abc_NtkHasSop(pNtk) ) + pNtk->pManFunc = Extra_MmFlexStart(); + else if ( Abc_NtkHasBdd(pNtk) ) + pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + else if ( Abc_NtkHasAig(pNtk) ) + pNtk->pManFunc = Abc_AigAlloc( pNtk ); + else if ( Abc_NtkHasMapping(pNtk) ) + pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()); + else + assert( 0 ); + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Starts a new network using existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pObjNew; + int i; + if ( pNtk == NULL ) + return NULL; + // start the network + pNtkNew = Abc_NtkAlloc( Type, Func ); + // duplicate the name and the spec + pNtkNew->pName = util_strsav(pNtk->pName); + pNtkNew->pSpec = util_strsav(pNtk->pSpec); + // clone the PIs/POs/latches + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + pObjNew = Abc_NtkDupObj(pNtkNew, pObj); + Vec_PtrPush( pNtkNew->vCis, pObjNew ); + Vec_PtrPush( pNtkNew->vCos, pObjNew ); + } + // clean the node copy fields + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = NULL; + // transfer the names + Abc_NtkDupCioNamesTable( pNtk, pNtkNew ); + Abc_ManTimeDup( pNtk, pNtkNew ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Finalizes the network using the existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + Abc_Obj_t * pObj, * pDriver, * pDriverNew; + int i; + // set the COs of the strashed network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) ); + pDriverNew = Abc_ObjNotCond(pDriver->pCopy, Abc_ObjFaninC0(pObj)); + Abc_ObjAddFanin( pObj->pCopy, pDriverNew ); + } +} + +/**Function************************************************************* + + Synopsis [Finalizes the network using the existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + Abc_Obj_t * pObj, * pDriver, * pDriverNew; + int i; + // set the COs of the strashed network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) ); + pDriverNew = pDriver->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pDriverNew ); + } +} + +/**Function************************************************************* + + Synopsis [Finalizes the network adding latches to CI/CO lists and creates their names.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i; + // set the COs of the strashed network + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + Vec_PtrPush( pNtk->vCis, pLatch ); + Vec_PtrPush( pNtk->vCos, pLatch ); + Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") ); + } +} + +/**Function************************************************************* + + Synopsis [Starts a new network using existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkStartRead( char * pName ) +{ + Abc_Ntk_t * pNtkNew; + // allocate the empty network + pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP ); + // set the specs + pNtkNew->pName = util_strsav( pName ); + pNtkNew->pSpec = util_strsav( pName ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Finalizes the network using the existing network as a model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i; + assert( Abc_NtkIsNetlist(pNtk) ); + // fix the net drivers + Abc_NtkFixNonDrivenNets( pNtk ); + // create the names table + Abc_NtkCreateCioNamesTable( pNtk ); + // add latches to the CI/CO arrays + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + Vec_PtrPush( pNtk->vCis, pLatch ); + Vec_PtrPush( pNtk->vCos, pLatch ); + } +} + +/**Function************************************************************* + + Synopsis [Duplicate the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin; + int i, k; + if ( pNtk == NULL ) + return NULL; + // start the network + pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc ); + // copy the internal nodes + if ( Abc_NtkHasAig(pNtk) ) + Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc ); + else + { + // duplicate the nets and nodes (CIs/COs/latches already dupped) + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( pObj->pCopy == NULL ) + Abc_NtkDupObj(pNtkNew, pObj); + // reconnect all objects (no need to transfer attributes on edges) + Abc_NtkForEachObj( pNtk, pObj, i ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + } + // duplicate the EXDC Ntk + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Creates the network composed of one output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin; + char Buffer[1000]; + int i, k; + + assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); + assert( Abc_ObjIsCo(pNode) ); + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + // set the name + sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) ); + pNtkNew->pName = util_strsav(Buffer); + + // collect the nodes in the TFI of the output + vNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); + // create the PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + { + if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS + { + pObj->pCopy = Abc_NtkCreatePi(pNtkNew); + Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + } + } + // establish connection between the constant nodes + if ( Abc_NtkIsStrash(pNtk) ) + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); + + // copy the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // if it is an AIG, add to the hash table + if ( Abc_NtkIsStrash(pNtk) ) + { + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + } + else + { + Abc_NtkDupObj( pNtkNew, pObj ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + } + } + Vec_PtrFree( vNodes ); + + // add the PO corresponding to this output + pNode->pCopy = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pNode->pCopy, Abc_ObjFanin0(pNode)->pCopy ); + Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); + + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Creates the network composed of one output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo; + int i; + + assert( Abc_NtkIsLogic(pNtk) ); + + // start the network + Abc_NtkCleanCopy( pNtk ); + pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG ); + pNtkNew->pName = util_strsav(pNtk->pName); + + // collect the nodes in the TFI of the output + vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize ); + // create the PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + { + pObj->pCopy = Abc_NtkCreatePi(pNtkNew); + Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + } + // copy the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj ); + Vec_PtrFree( vNodes ); + + // add the PO + pFinal = Abc_AigConst1( pNtkNew->pManFunc ); + Vec_PtrForEachEntry( vRoots, pObj, i ) + { + pOther = pObj->pCopy; + if ( Vec_IntEntry(vValues, i) == 0 ) + pOther = Abc_ObjNot(pOther); + pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther ); + } + + // add the PO corresponding to this output + pNodePo = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pNodePo, pFinal ); + Abc_NtkLogicStoreName( pNodePo, "miter" ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Deletes the Ntk.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pFanin, * pNodePo; + int i; + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + pNtkNew->pName = util_strsav(Abc_ObjName(pNode)); + // add the PIs corresponding to the fanins of the node + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pFanin->pCopy = Abc_NtkCreatePi( pNtkNew ); + Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) ); + } + // duplicate and connect the node + pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy ); + // create the only PO + pNodePo = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pNodePo, pNode->pCopy ); + Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Deletes the Ntk.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDelete( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int TotalMemory, i; + int LargePiece = (4 << ABC_NUM_STEPS); + if ( pNtk == NULL ) + return; + // make sure all the marks are clean + Abc_NtkForEachObj( pNtk, pObj, i ) + { + // free large fanout arrays + if ( pObj->vFanouts.nCap * 4 > LargePiece ) + FREE( pObj->vFanouts.pArray ); + // check that the other things are okay + assert( pObj->fMarkA == 0 ); + assert( pObj->fMarkB == 0 ); + assert( pObj->fMarkC == 0 ); + } + + // dereference the BDDs + if ( Abc_NtkHasBdd(pNtk) ) + Abc_NtkForEachNode( pNtk, pObj, i ) + Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData ); + + FREE( pNtk->pName ); + FREE( pNtk->pSpec ); + // copy the EXDC Ntk + if ( pNtk->pExdc ) + Abc_NtkDelete( pNtk->pExdc ); + // free the arrays + Vec_PtrFree( pNtk->vObjs ); + Vec_PtrFree( pNtk->vLats ); + Vec_PtrFree( pNtk->vCis ); + Vec_PtrFree( pNtk->vCos ); + Vec_PtrFree( pNtk->vPtrTemp ); + Vec_IntFree( pNtk->vIntTemp ); + Vec_StrFree( pNtk->vStrTemp ); + // free the hash table of Obj name into Obj ID + stmm_free_table( pNtk->tName2Net ); + stmm_free_table( pNtk->tObj2Name ); + TotalMemory = 0; + TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames); + TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj); + TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep); +// fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) ); + // free the storage + Extra_MmFlexStop ( pNtk->pMmNames, 0 ); + Extra_MmFixedStop( pNtk->pMmObj, 0 ); + Extra_MmStepStop ( pNtk->pMmStep, 0 ); + // free the timing manager + if ( pNtk->pManTime ) + Abc_ManTimeStop( pNtk->pManTime ); + // start the functionality manager + if ( Abc_NtkHasSop(pNtk) ) + Extra_MmFlexStop( pNtk->pManFunc, 0 ); + else if ( Abc_NtkHasBdd(pNtk) ) + Extra_StopManager( pNtk->pManFunc ); + else if ( Abc_NtkHasAig(pNtk) ) + Abc_AigFree( pNtk->pManFunc ); + else if ( !Abc_NtkHasMapping(pNtk) ) + assert( 0 ); + free( pNtk ); +} + +/**Function************************************************************* + + Synopsis [Reads the verilog file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNets; + Abc_Obj_t * pNet, * pNode; + int i; + + // check for non-driven nets + vNets = Vec_PtrAlloc( 100 ); + Abc_NtkForEachNet( pNtk, pNet, i ) + { + if ( Abc_ObjFaninNum(pNet) > 0 ) + continue; + // add the constant 0 driver + pNode = Abc_NtkCreateNode( pNtk ); + // set the constant function + Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") ); + // add the fanout net + Abc_ObjAddFanin( pNet, pNode ); + // add the net to those for which the warning will be printed + Vec_PtrPush( vNets, pNet->pData ); + } + + // print the warning + if ( vNets->nSize > 0 ) + { + printf( "Constant-zero drivers were added to %d non-driven nets:\n", vNets->nSize ); + for ( i = 0; i < vNets->nSize; i++ ) + { + if ( i == 0 ) + printf( "%s", vNets->pArray[i] ); + else if ( i == 1 ) + printf( ", %s", vNets->pArray[i] ); + else if ( i == 2 ) + { + printf( ", %s, etc.", vNets->pArray[i] ); + break; + } + } + printf( "\n" ); + } + Vec_PtrFree( vNets ); +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcObj.c index 16d5ec05..f869abf3 100644 --- a/src/base/abc/abcCreate.c +++ b/src/base/abc/abcObj.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Creation/duplication/deletion procedures.] + Synopsis [Object creation/duplication/deletion procedures.] Author [Alan Mishchenko] @@ -26,547 +26,12 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_NUM_STEPS 10 - -static Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); -static void Abc_ObjRecycle( Abc_Obj_t * pObj ); -static void Abc_ObjAdd( Abc_Obj_t * pObj ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Creates a new Ntk.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ) -{ - Abc_Ntk_t * pNtk; - pNtk = ALLOC( Abc_Ntk_t, 1 ); - memset( pNtk, 0, sizeof(Abc_Ntk_t) ); - pNtk->ntkType = Type; - pNtk->ntkFunc = Func; - // start the object storage - pNtk->vObjs = Vec_PtrAlloc( 100 ); - pNtk->vLats = Vec_PtrAlloc( 100 ); - pNtk->vCis = Vec_PtrAlloc( 100 ); - pNtk->vCos = Vec_PtrAlloc( 100 ); - pNtk->vPtrTemp = Vec_PtrAlloc( 100 ); - pNtk->vIntTemp = Vec_IntAlloc( 100 ); - pNtk->vStrTemp = Vec_StrAlloc( 100 ); - // start the hash table - pNtk->tName2Net = stmm_init_table(strcmp, stmm_strhash); - pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); - // start the memory managers - pNtk->pMmNames = Extra_MmFlexStart(); - pNtk->pMmObj = Extra_MmFixedStart( sizeof(Abc_Obj_t) ); - pNtk->pMmStep = Extra_MmStepStart( ABC_NUM_STEPS ); - // get ready to assign the first Obj ID - pNtk->nTravIds = 1; - // start the functionality manager - if ( Abc_NtkHasSop(pNtk) ) - pNtk->pManFunc = Extra_MmFlexStart(); - else if ( Abc_NtkHasBdd(pNtk) ) - pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - else if ( Abc_NtkHasAig(pNtk) ) - pNtk->pManFunc = Abc_AigAlloc( pNtk ); - else if ( Abc_NtkHasMapping(pNtk) ) - pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()); - else - assert( 0 ); - return pNtk; -} - -/**Function************************************************************* - - Synopsis [Starts a new network using existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pObjNew; - int i; - if ( pNtk == NULL ) - return NULL; - // start the network - pNtkNew = Abc_NtkAlloc( Type, Func ); - // duplicate the name and the spec - pNtkNew->pName = util_strsav(pNtk->pName); - pNtkNew->pSpec = util_strsav(pNtk->pSpec); - // clone the PIs/POs/latches - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachLatch( pNtk, pObj, i ) - { - pObjNew = Abc_NtkDupObj(pNtkNew, pObj); - Vec_PtrPush( pNtkNew->vCis, pObjNew ); - Vec_PtrPush( pNtkNew->vCos, pObjNew ); - } - // clean the node copy fields - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = NULL; - // transfer the names - Abc_NtkDupCioNamesTable( pNtk, pNtkNew ); - Abc_ManTimeDup( pNtk, pNtkNew ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Finalizes the network using the existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) -{ - Abc_Obj_t * pObj, * pDriver, * pDriverNew; - int i; - // set the COs of the strashed network - Abc_NtkForEachCo( pNtk, pObj, i ) - { - pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) ); - pDriverNew = Abc_ObjNotCond(pDriver->pCopy, Abc_ObjFaninC0(pObj)); - Abc_ObjAddFanin( pObj->pCopy, pDriverNew ); - } -} - -/**Function************************************************************* - - Synopsis [Finalizes the network adding latches to CI/CO lists and creates their names.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pLatch; - int i; - // set the COs of the strashed network - Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - Vec_PtrPush( pNtk->vCis, pLatch ); - Vec_PtrPush( pNtk->vCos, pLatch ); - Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") ); - } -} - -/**Function************************************************************* - - Synopsis [Starts a new network using existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkStartRead( char * pName ) -{ - Abc_Ntk_t * pNtkNew; - // allocate the empty network - pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP ); - // set the specs - pNtkNew->pName = util_strsav( pName ); - pNtkNew->pSpec = util_strsav( pName ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Finalizes the network using the existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pLatch; - int i; - assert( Abc_NtkIsNetlist(pNtk) ); - // fix the net drivers - Abc_NtkFixNonDrivenNets( pNtk ); - // create the names table - Abc_NtkCreateCioNamesTable( pNtk ); - // add latches to the CI/CO arrays - Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - Vec_PtrPush( pNtk->vCis, pLatch ); - Vec_PtrPush( pNtk->vCos, pLatch ); - } -} - -/**Function************************************************************* - - Synopsis [Duplicate the network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pFanin; - int i, k; - if ( pNtk == NULL ) - return NULL; - // start the network - pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc ); - // copy the internal nodes - if ( Abc_NtkHasAig(pNtk) ) - Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc ); - else - { - // duplicate the nets and nodes (CIs/COs/latches already dupped) - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( pObj->pCopy == NULL ) - Abc_NtkDupObj(pNtkNew, pObj); - // reconnect all objects (no need to transfer attributes on edges) - Abc_NtkForEachObj( pNtk, pObj, i ) - Abc_ObjForEachFanin( pObj, pFanin, k ) - Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); - } - // duplicate the EXDC Ntk - if ( pNtk->pExdc ) - pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Creates the network composed of one output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ) -{ - Vec_Ptr_t * vNodes; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pFanin; - char Buffer[1000]; - int i, k; - - assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); - assert( Abc_ObjIsCo(pNode) ); - - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); - // set the name - sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) ); - pNtkNew->pName = util_strsav(Buffer); - - // collect the nodes in the TFI of the output - vNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - // create the PIs - Abc_NtkForEachCi( pNtk, pObj, i ) - { - if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS - { - pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); - } - } - // establish connection between the constant nodes - if ( Abc_NtkIsStrash(pNtk) ) - Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); - - // copy the nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - // if it is an AIG, add to the hash table - if ( Abc_NtkIsStrash(pNtk) ) - { - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - } - else - { - Abc_NtkDupObj( pNtkNew, pObj ); - Abc_ObjForEachFanin( pObj, pFanin, k ) - Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); - } - } - Vec_PtrFree( vNodes ); - - // add the PO corresponding to this output - pNode->pCopy = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjFanin0(pNode)->pCopy ); - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); - - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Creates the network composed of one output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ) -{ - Vec_Ptr_t * vNodes; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo; - int i; - - assert( Abc_NtkIsLogic(pNtk) ); - - // start the network - Abc_NtkCleanCopy( pNtk ); - pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG ); - pNtkNew->pName = util_strsav(pNtk->pName); - - // collect the nodes in the TFI of the output - vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize ); - // create the PIs - Abc_NtkForEachCi( pNtk, pObj, i ) - { - pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); - } - // copy the nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj ); - Vec_PtrFree( vNodes ); - - // add the PO - pFinal = Abc_AigConst1( pNtkNew->pManFunc ); - Vec_PtrForEachEntry( vRoots, pObj, i ) - { - pOther = pObj->pCopy; - if ( Vec_IntEntry(vValues, i) == 0 ) - pOther = Abc_ObjNot(pOther); - pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther ); - } - - // add the PO corresponding to this output - pNodePo = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pNodePo, pFinal ); - Abc_NtkLogicStoreName( pNodePo, "miter" ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Deletes the Ntk.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pFanin, * pNodePo; - int i; - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); - pNtkNew->pName = util_strsav(Abc_ObjName(pNode)); - // add the PIs corresponding to the fanins of the node - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - pFanin->pCopy = Abc_NtkCreatePi( pNtkNew ); - Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) ); - } - // duplicate and connect the node - pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode ); - Abc_ObjForEachFanin( pNode, pFanin, i ) - Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy ); - // create the only PO - pNodePo = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pNodePo, pNode->pCopy ); - Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Deletes the Ntk.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDelete( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pObj; - int TotalMemory, i; - int LargePiece = (4 << ABC_NUM_STEPS); - if ( pNtk == NULL ) - return; - // make sure all the marks are clean - Abc_NtkForEachObj( pNtk, pObj, i ) - { - // free large fanout arrays - if ( pObj->vFanouts.nCap * 4 > LargePiece ) - FREE( pObj->vFanouts.pArray ); - // check that the other things are okay - assert( pObj->fMarkA == 0 ); - assert( pObj->fMarkB == 0 ); - assert( pObj->fMarkC == 0 ); - } - - // dereference the BDDs - if ( Abc_NtkHasBdd(pNtk) ) - Abc_NtkForEachNode( pNtk, pObj, i ) - Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData ); - - FREE( pNtk->pName ); - FREE( pNtk->pSpec ); - // copy the EXDC Ntk - if ( pNtk->pExdc ) - Abc_NtkDelete( pNtk->pExdc ); - // free the arrays - Vec_PtrFree( pNtk->vObjs ); - Vec_PtrFree( pNtk->vLats ); - Vec_PtrFree( pNtk->vCis ); - Vec_PtrFree( pNtk->vCos ); - Vec_PtrFree( pNtk->vPtrTemp ); - Vec_IntFree( pNtk->vIntTemp ); - Vec_StrFree( pNtk->vStrTemp ); - // free the hash table of Obj name into Obj ID - stmm_free_table( pNtk->tName2Net ); - stmm_free_table( pNtk->tObj2Name ); - TotalMemory = 0; - TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames); - TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj); - TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep); -// fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) ); - // free the storage - Extra_MmFlexStop ( pNtk->pMmNames, 0 ); - Extra_MmFixedStop( pNtk->pMmObj, 0 ); - Extra_MmStepStop ( pNtk->pMmStep, 0 ); - // free the timing manager - if ( pNtk->pManTime ) - Abc_ManTimeStop( pNtk->pManTime ); - // start the functionality manager - if ( Abc_NtkHasSop(pNtk) ) - Extra_MmFlexStop( pNtk->pManFunc, 0 ); - else if ( Abc_NtkHasBdd(pNtk) ) - Extra_StopManager( pNtk->pManFunc ); - else if ( Abc_NtkHasAig(pNtk) ) - Abc_AigFree( pNtk->pManFunc ); - else if ( !Abc_NtkHasMapping(pNtk) ) - assert( 0 ); - free( pNtk ); -} - -/**Function************************************************************* - - Synopsis [Reads the verilog file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) -{ - Vec_Ptr_t * vNets; - Abc_Obj_t * pNet, * pNode; - int i; - - // check for non-driven nets - vNets = Vec_PtrAlloc( 100 ); - Abc_NtkForEachNet( pNtk, pNet, i ) - { - if ( Abc_ObjFaninNum(pNet) > 0 ) - continue; - // add the constant 0 driver - pNode = Abc_NtkCreateNode( pNtk ); - // set the constant function - Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") ); - // add the fanout net - Abc_ObjAddFanin( pNet, pNode ); - // add the net to those for which the warning will be printed - Vec_PtrPush( vNets, pNet->pData ); - } - - // print the warning - if ( vNets->nSize > 0 ) - { - printf( "Constant-zero drivers were added to %d non-driven nets:\n", vNets->nSize ); - for ( i = 0; i < vNets->nSize; i++ ) - { - if ( i == 0 ) - printf( "%s", vNets->pArray[i] ); - else if ( i == 1 ) - printf( ", %s", vNets->pArray[i] ); - else if ( i == 2 ) - { - printf( ", %s, etc.", vNets->pArray[i] ); - break; - } - } - printf( "\n" ); - } - Vec_PtrFree( vNets ); -} - - - - -/**Function************************************************************* - Synopsis [Creates a new Obj.] Description [] @@ -1404,4 +869,3 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/base/abc/module.make b/src/base/abc/module.make index 695e056b..649e71a2 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -1,40 +1,15 @@ -SRC += src/base/abc/abc.c \ - src/base/abc/abcAig.c \ - src/base/abc/abcAttach.c \ - src/base/abc/abcBalance.c \ +SRC += src/base/abc/abcAig.c \ src/base/abc/abcCheck.c \ - src/base/abc/abcCollapse.c \ - src/base/abc/abcCreate.c \ - src/base/abc/abcCut.c \ src/base/abc/abcDfs.c \ - src/base/abc/abcDsd.c \ src/base/abc/abcFanio.c \ - src/base/abc/abcFpga.c \ - src/base/abc/abcFraig.c \ src/base/abc/abcFunc.c \ - src/base/abc/abcFxu.c \ src/base/abc/abcLatch.c \ - src/base/abc/abcMap.c \ src/base/abc/abcMinBase.c \ - src/base/abc/abcMiter.c \ src/base/abc/abcNames.c \ src/base/abc/abcNetlist.c \ - src/base/abc/abcNtbdd.c \ - src/base/abc/abcPrint.c \ - src/base/abc/abcReconv.c \ - src/base/abc/abcRefactor.c \ + src/base/abc/abcNtk.c \ + src/base/abc/abcObj.c \ src/base/abc/abcRefs.c \ - src/base/abc/abcRenode.c \ - src/base/abc/abcRewrite.c \ - src/base/abc/abcSat.c \ - src/base/abc/abcSeq.c \ - src/base/abc/abcSeqRetime.c \ src/base/abc/abcShow.c \ src/base/abc/abcSop.c \ - src/base/abc/abcStrash.c \ - src/base/abc/abcSweep.c \ - src/base/abc/abcSymm.c \ - src/base/abc/abcTiming.c \ - src/base/abc/abcUnreach.c \ - src/base/abc/abcUtil.c \ - src/base/abc/abcVerify.c + src/base/abc/abcUtil.c diff --git a/src/base/abc/abc.c b/src/base/abci/abc.c index dca80ca5..30047d23 100644 --- a/src/base/abc/abc.c +++ b/src/base/abci/abc.c @@ -65,6 +65,7 @@ static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -140,6 +141,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "one_node", Abc_CommandOneNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); + Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -591,10 +593,11 @@ usage: ***********************************************************************/ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) { + Vec_Ptr_t * vSuppFun; FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - extern void * Sim_ComputeSupp( Abc_Ntk_t * pNtk ); + extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -619,12 +622,20 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for combinational networks.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "This command works only for AIGs.\n" ); return 1; } - Sim_ComputeSupp( pNtk ); + vSuppFun = Sim_ComputeFunSupp( pNtk ); + free( vSuppFun->pArray[0] ); + Vec_PtrFree( vSuppFun ); return 0; usage: @@ -660,7 +671,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fUseBdds = 1; + fUseBdds = 0; fNaive = 0; fVerbose = 0; util_getopt_reset(); @@ -688,6 +699,11 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for combinational networks.\n" ); + return 1; + } if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "This command works only for AIGs.\n" ); @@ -2758,6 +2774,62 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + // run the command + pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: test [-h]\n" ); + fprintf( pErr, "\t testbench for new procedures\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + @@ -3249,10 +3321,11 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) char Buffer[100]; double DelayTarget; int fRecovery; - int fVerbose; int fSweep; + int fSwitching; + int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3262,9 +3335,10 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) DelayTarget =-1; fRecovery = 1; fSweep = 1; + fSwitching = 0; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Dasvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Daspvh" ) ) != EOF ) { switch ( c ) { @@ -3285,6 +3359,9 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSweep ^= 1; break; + case 'p': + fSwitching ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -3318,7 +3395,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } fprintf( pOut, "The network was strashed and balanced before mapping.\n" ); // get the new network - pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fVerbose ); + pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose ); if ( pNtkRes == NULL ) { Abc_NtkDelete( pNtk ); @@ -3330,7 +3407,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) else { // get the new network - pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fVerbose ); + pNtkRes = Abc_NtkMap( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Mapping has failed.\n" ); @@ -3350,11 +3427,12 @@ usage: sprintf( Buffer, "not used" ); else sprintf( Buffer, "%.3f", DelayTarget ); - fprintf( pErr, "usage: map [-D num] [-asvh]\n" ); + fprintf( pErr, "usage: map [-D num] [-aspvh]\n" ); fprintf( pErr, "\t performs standard cell mapping of the current network\n" ); fprintf( pErr, "\t-D num : sets the global required times [default = %s]\n", Buffer ); fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" ); fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" ); + fprintf( pErr, "\t-p : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3569,8 +3647,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; int fRecovery; + int fSwitching; int fVerbose; - extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3578,15 +3657,19 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fRecovery = 1; + fSwitching = 0; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "avh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "apvh" ) ) != EOF ) { switch ( c ) { case 'a': fRecovery ^= 1; break; + case 'p': + fSwitching ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -3621,7 +3704,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) } fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" ); // get the new network - pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fVerbose ); + pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fSwitching, fVerbose ); if ( pNtkRes == NULL ) { Abc_NtkDelete( pNtk ); @@ -3633,7 +3716,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) else { // get the new network - pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fVerbose ); + pNtkRes = Abc_NtkFpga( pNtk, fRecovery, fSwitching, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "FPGA mapping has failed.\n" ); @@ -3645,9 +3728,10 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: fpga [-avh]\n" ); + fprintf( pErr, "usage: fpga [-apvh]\n" ); fprintf( pErr, "\t performs FPGA mapping of the current network\n" ); fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" ); + fprintf( pErr, "\t-p : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : prints the command usage\n"); return 1; diff --git a/src/base/abc/abcAttach.c b/src/base/abci/abcAttach.c index a8e06555..a8e06555 100644 --- a/src/base/abc/abcAttach.c +++ b/src/base/abci/abcAttach.c diff --git a/src/base/abc/abcBalance.c b/src/base/abci/abcBalance.c index 7deab3ba..5042d0d5 100644 --- a/src/base/abc/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -25,8 +25,8 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate ); -static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, bool fDuplicate ); -static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, int fDuplicate ); +static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, bool fDuplicate ); +static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int fDuplicate ); static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate ); //////////////////////////////////////////////////////////////////////// @@ -78,6 +78,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica { int fCheck = 1; ProgressBar * pProgress; + Vec_Vec_t * vStorage; Abc_Obj_t * pNode, * pDriver; int i; @@ -85,6 +86,8 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkAig->pManFunc); // set the level of PIs of AIG according to the arrival times of the old network Abc_NtkSetNodeLevelsArrival( pNtk ); + // allocate temporary storage for supergates + vStorage = Vec_VecStart( Abc_AigGetLevelNum(pNtk) + 1 ); // perform balancing of POs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -92,9 +95,10 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica Extra_ProgressBarUpdate( pProgress, i, NULL ); // strash the driver node pDriver = Abc_ObjFanin0(pNode); - Abc_NodeBalance_rec( pNtkAig, pDriver, fDuplicate ); + Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, fDuplicate ); } Extra_ProgressBarStop( pProgress ); + Vec_VecFree( vStorage ); } /**Function************************************************************* @@ -108,7 +112,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool fDuplicate ) +Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, bool fDuplicate ) { Abc_Aig_t * pMan = pNtkNew->pManFunc; Abc_Obj_t * pNodeNew, * pNode1, * pNode2; @@ -120,17 +124,16 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool return pNodeOld->pCopy; assert( Abc_ObjIsNode(pNodeOld) ); // get the implication supergate - vSuper = Abc_NodeBalanceCone( pNodeOld, fDuplicate ); + vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, fDuplicate ); if ( vSuper->nSize == 0 ) { // it means that the supergate contains two nodes in the opposite polarity - Vec_PtrFree( vSuper ); pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pMan)); return pNodeOld->pCopy; } // for each old node, derive the new well-balanced node for ( i = 0; i < vSuper->nSize; i++ ) { - pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), fDuplicate ); + pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, fDuplicate ); vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) ); } // sort the new nodes by level in the decreasing order @@ -147,7 +150,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool assert( pNodeOld->pCopy == NULL ); // mark the old node with the new node pNodeOld->pCopy = vSuper->pArray[0]; - Vec_PtrFree( vSuper ); return pNodeOld->pCopy; } @@ -164,12 +166,13 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, int fDuplicate ) +Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int fDuplicate ) { Vec_Ptr_t * vNodes; int RetValue, i; assert( !Abc_ObjIsComplement(pNode) ); - vNodes = Vec_PtrAlloc( 4 ); + vNodes = Vec_VecEntry( vStorage, pNode->Level ); + Vec_PtrClear( vNodes ); RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate ); assert( vNodes->nSize > 0 ); for ( i = 0; i < vNodes->nSize; i++ ) diff --git a/src/base/abc/abcCollapse.c b/src/base/abci/abcCollapse.c index 4e359506..4e359506 100644 --- a/src/base/abc/abcCollapse.c +++ b/src/base/abci/abcCollapse.c diff --git a/src/base/abc/abcCut.c b/src/base/abci/abcCut.c index f487bd1b..f487bd1b 100644 --- a/src/base/abc/abcCut.c +++ b/src/base/abci/abcCut.c diff --git a/src/base/abc/abcDsd.c b/src/base/abci/abcDsd.c index 013b7ac4..013b7ac4 100644 --- a/src/base/abc/abcDsd.c +++ b/src/base/abci/abcDsd.c diff --git a/src/base/abc/abcFpga.c b/src/base/abci/abcFpga.c index ad411aa5..f30325c0 100644 --- a/src/base/abc/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -25,7 +25,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ); +static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose ); static Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNodeFpga ); @@ -44,11 +44,14 @@ static Abc_Obj_t * Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) +Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose ) { int fCheck = 1; Abc_Ntk_t * pNtkNew; Fpga_Man_t * pMan; + Vec_Int_t * vSwitching; + float * pSwitching = NULL; + int fShowSwitching = 0; assert( Abc_NtkIsStrash(pNtk) ); @@ -56,10 +59,21 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Performing FPGA mapping with choices.\n" ); + // compute switching activity + fShowSwitching |= fSwitching; + if ( fShowSwitching ) + { + extern Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ); + vSwitching = Sim_NtkComputeSwitching( pNtk, 4096 ); + pSwitching = (float *)vSwitching->pArray; + } + // perform FPGA mapping - pMan = Abc_NtkToFpga( pNtk, fRecovery, fVerbose ); + pMan = Abc_NtkToFpga( pNtk, fRecovery, pSwitching, fVerbose ); + if ( pSwitching ) Vec_IntFree( vSwitching ); if ( pMan == NULL ) return NULL; + Fpga_ManSetSwitching( pMan, fSwitching ); if ( !Fpga_Mapping( pMan ) ) { Fpga_ManFree( pMan ); @@ -96,7 +110,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) SeeAlso [] ***********************************************************************/ -Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) +Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose ) { Fpga_Man_t * pMan; ProgressBar * pProgress; @@ -118,7 +132,12 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) // create PIs and remember them in the old nodes Abc_NtkCleanCopy( pNtk ); Abc_NtkForEachCi( pNtk, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i]; + { + pNodeFpga = Fpga_ManReadInputs(pMan)[i]; + pNode->pCopy = (Abc_Obj_t *)pNodeFpga; + if ( pSwitching ) + Fpga_NodeSetSwitching( pNodeFpga, pSwitching[pNode->Id] ); + } // load the AIG into the mapper vNodes = Abc_AigDfs( pNtk, 0, 0 ); @@ -139,6 +158,8 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) assert( pNode->pCopy == NULL ); // remember the node pNode->pCopy = (Abc_Obj_t *)pNodeFpga; + if ( pSwitching ) + Fpga_NodeSetSwitching( pNodeFpga, pSwitching[pNode->Id] ); // set up the choice node if ( Abc_NodeIsAigChoice( pNode ) ) for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) @@ -197,8 +218,8 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkFinalize( pNtk, pNtkNew ); // decouple the PO driver nodes to reduce the number of levels nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); - if ( nDupGates && Fpga_ManReadVerbose(pMan) ) - printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates ); +// if ( nDupGates && Fpga_ManReadVerbose(pMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); return pNtkNew; } diff --git a/src/base/abc/abcFraig.c b/src/base/abci/abcFraig.c index ef4746d5..fbe676a3 100644 --- a/src/base/abc/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -52,12 +52,13 @@ static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) { int fCheck = 1; + Fraig_Params_t * pPars = pParams; Abc_Ntk_t * pNtkNew; Fraig_Man_t * pMan; // perform fraiging pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); // prove the miter if asked to - if ( ((Fraig_Params_t *)pParams)->fTryProve ) + if ( pPars->fTryProve ) Fraig_ManProveMiter( pMan ); // reconstruct FRAIG in the new network pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); @@ -106,10 +107,12 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA // perform strashing vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 ); - pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); + if ( !pParams->fInternal ) + pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( !pParams->fInternal ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); if ( pNode == pConst1 ) pNodeFraig = Fraig_ManReadConst1(pMan); else if ( pNode == pReset ) @@ -121,12 +124,13 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA assert( pNode->pCopy == NULL ); pNode->pCopy = (Abc_Obj_t *)pNodeFraig; } - Extra_ProgressBarStop( pProgress ); + if ( !pParams->fInternal ) + Extra_ProgressBarStop( pProgress ); Vec_PtrFree( vNodes ); // set the primary outputs Abc_NtkForEachCo( pNtk, pNode, i ) - Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjFanin0(pNode)->pCopy ); + Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) ); return pMan; } @@ -145,7 +149,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pNode;//, * pNodeNew; + Abc_Obj_t * pNode, * pNodeNew; int i; // create the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG ); @@ -159,11 +163,10 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkForEachCo( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - Abc_ObjFanin0(pNode)->pCopy = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] ); + pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Extra_ProgressBarStop( pProgress ); - // finalize the new network - Abc_NtkFinalize( pNtk, pNtkNew ); return pNtkNew; } diff --git a/src/base/abc/abcFxu.c b/src/base/abci/abcFxu.c index 0c8994e1..0c8994e1 100644 --- a/src/base/abc/abcFxu.c +++ b/src/base/abci/abcFxu.c diff --git a/src/base/abc/abcMap.c b/src/base/abci/abcMap.c index 28853c8d..45f600ed 100644 --- a/src/base/abc/abcMap.c +++ b/src/base/abci/abcMap.c @@ -27,7 +27,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose ); +static Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose ); static Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase ); static Abc_Obj_t * Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase ); @@ -54,11 +54,14 @@ static Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Sup SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose ) +Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose ) { int fCheck = 1; Abc_Ntk_t * pNtkNew; Map_Man_t * pMan; + Vec_Int_t * vSwitching; + float * pSwitching = NULL; + int fShowSwitching = 0; int clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -82,11 +85,22 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Performing mapping with choices.\n" ); + // compute switching activity + fShowSwitching |= fSwitching; + if ( fShowSwitching ) + { + extern Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ); + vSwitching = Sim_NtkComputeSwitching( pNtk, 4096 ); + pSwitching = (float *)vSwitching->pArray; + } + // perform the mapping - pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, fVerbose ); + pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, pSwitching, fVerbose ); + if ( pSwitching ) Vec_IntFree( vSwitching ); if ( pMan == NULL ) return NULL; clk = clock(); + Map_ManSetSwitching( pMan, fSwitching ); if ( !Map_Mapping( pMan ) ) { Map_ManFree( pMan ); @@ -121,7 +135,7 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fVerbose ) +Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, float * pSwitching, int fVerbose ) { Map_Man_t * pMan; ProgressBar * pProgress; @@ -144,7 +158,12 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i // create PIs and remember them in the old nodes Abc_NtkCleanCopy( pNtk ); Abc_NtkForEachCi( pNtk, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i]; + { + pNodeMap = Map_ManReadInputs(pMan)[i]; + pNode->pCopy = (Abc_Obj_t *)pNodeMap; + if ( pSwitching ) + Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] ); + } // load the AIG into the mapper vNodes = Abc_AigDfs( pNtk, 0, 0 ); @@ -165,6 +184,8 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i assert( pNode->pCopy == NULL ); // remember the node pNode->pCopy = (Abc_Obj_t *)pNodeMap; + if ( pSwitching ) + Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] ); // set up the choice node if ( Abc_NodeIsAigChoice( pNode ) ) for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) @@ -224,8 +245,8 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) Extra_ProgressBarStop( pProgress ); // decouple the PO driver nodes to reduce the number of levels nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); - if ( nDupGates && Map_ManReadVerbose(pMan) ) - printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates ); +// if ( nDupGates && Map_ManReadVerbose(pMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); return pNtkNew; } @@ -446,7 +467,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ) printf( "Performing mapping with choices.\n" ); // perform the mapping - pMan = Abc_NtkToMap( pNtk, -1, 1, 0 ); + pMan = Abc_NtkToMap( pNtk, -1, 1, NULL, 0 ); if ( pMan == NULL ) return NULL; if ( !Map_Mapping( pMan ) ) diff --git a/src/base/abc/abcMiter.c b/src/base/abci/abcMiter.c index a0426dc2..0d75ba1f 100644 --- a/src/base/abc/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -27,7 +27,7 @@ static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ); static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter ); -static void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode ); +static void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode ); static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ); static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes ); @@ -121,8 +121,8 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk Abc_Obj_t * pObj, * pObjNew; int i; // clean the copy field in all objects - Abc_NtkCleanCopy( pNtk1 ); - Abc_NtkCleanCopy( pNtk2 ); +// Abc_NtkCleanCopy( pNtk1 ); +// Abc_NtkCleanCopy( pNtk2 ); if ( fComb ) { // create new PIs and remember them in the old PIs @@ -224,7 +224,7 @@ void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter ) SeeAlso [] ***********************************************************************/ -void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot ) +void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot ) { Vec_Ptr_t * vNodes; Abc_Obj_t * pNode, * pNodeNew, * pConst1, * pConst1New; @@ -310,7 +310,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) +Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) { int fCheck = 1; char Buffer[100]; @@ -324,7 +324,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) // start the new network pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG ); - sprintf( Buffer, "%s_%s_miter", pNtk->pName, Abc_ObjName(Abc_NtkCo(pNtk, Out)) ); + sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) ); pNtkMiter->pName = util_strsav(Buffer); // get the root output @@ -337,7 +337,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) if ( In2 >= 0 ) Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1( pNtkMiter->pManFunc ); // add the first cofactor - Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot ); + Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output pOutput1 = Abc_ObjFanin0(pRoot)->pCopy; @@ -347,7 +347,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 ) if ( In2 >= 0 ) Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter->pManFunc) ); // add the second cofactor - Abc_NtkMiterAddOneNode( pNtk, pNtkMiter, pRoot ); + Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output pOutput2 = Abc_ObjFanin0(pRoot)->pCopy; diff --git a/src/base/abc/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 61c1a110..61c1a110 100644 --- a/src/base/abc/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c diff --git a/src/base/abc/abcPrint.c b/src/base/abci/abcPrint.c index 41b9288e..41b9288e 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abci/abcPrint.c diff --git a/src/base/abc/abcReconv.c b/src/base/abci/abcReconv.c index 766c14f3..766c14f3 100644 --- a/src/base/abc/abcReconv.c +++ b/src/base/abci/abcReconv.c diff --git a/src/base/abc/abcRefactor.c b/src/base/abci/abcRefactor.c index 791d2d53..791d2d53 100644 --- a/src/base/abc/abcRefactor.c +++ b/src/base/abci/abcRefactor.c diff --git a/src/base/abc/abcRenode.c b/src/base/abci/abcRenode.c index c77c0d70..c77c0d70 100644 --- a/src/base/abc/abcRenode.c +++ b/src/base/abci/abcRenode.c diff --git a/src/base/abc/abcRewrite.c b/src/base/abci/abcRewrite.c index 75fe1627..75fe1627 100644 --- a/src/base/abc/abcRewrite.c +++ b/src/base/abci/abcRewrite.c diff --git a/src/base/abc/abcSat.c b/src/base/abci/abcSat.c index 4fb059e5..4fb059e5 100644 --- a/src/base/abc/abcSat.c +++ b/src/base/abci/abcSat.c diff --git a/src/base/abc/abcStrash.c b/src/base/abci/abcStrash.c index 935f1300..935f1300 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abci/abcStrash.c diff --git a/src/base/abc/abcSweep.c b/src/base/abci/abcSweep.c index ca9bd34e..ca9bd34e 100644 --- a/src/base/abc/abcSweep.c +++ b/src/base/abci/abcSweep.c diff --git a/src/base/abc/abcSymm.c b/src/base/abci/abcSymm.c index 8df3a837..f9229639 100644 --- a/src/base/abc/abcSymm.c +++ b/src/base/abci/abcSymm.c @@ -25,6 +25,7 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose ); +static void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose ); static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose ); static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms ); @@ -48,7 +49,25 @@ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose if ( fUseBdds || fNaive ) Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose ); else - printf( "This option is currently not implemented.\n" ); + Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose ); +} + +/**Function************************************************************* + + Synopsis [Symmetry computation using simulation and SAT.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose ) +{ + extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ); + int nSymms = Sim_ComputeTwoVarSymms( pNtk ); + printf( "The total number of symmetries is %d.\n", nSymms ); } /**Function************************************************************* diff --git a/src/base/abc/abcTiming.c b/src/base/abci/abcTiming.c index b8524bd5..b8524bd5 100644 --- a/src/base/abc/abcTiming.c +++ b/src/base/abci/abcTiming.c diff --git a/src/base/abc/abcUnreach.c b/src/base/abci/abcUnreach.c index 0fe3ec63..0fe3ec63 100644 --- a/src/base/abc/abcUnreach.c +++ b/src/base/abci/abcUnreach.c diff --git a/src/base/abc/abcVerify.c b/src/base/abci/abcVerify.c index 55d6cf7d..55d6cf7d 100644 --- a/src/base/abc/abcVerify.c +++ b/src/base/abci/abcVerify.c diff --git a/src/sat/sim/simSym.c b/src/base/abci/abc_.c index 6b8bdaa3..bef3836f 100644 --- a/src/sat/sim/simSym.c +++ b/src/base/abci/abc_.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [simSym.c] + FileName [abc_.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [Simulation to determine two-variable symmetries.] + Synopsis [] Author [Alan Mishchenko] @@ -14,12 +14,11 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "abc.h" -#include "sim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abci/module.make b/src/base/abci/module.make new file mode 100644 index 00000000..d7c0add2 --- /dev/null +++ b/src/base/abci/module.make @@ -0,0 +1,24 @@ +SRC += src/base/abci/abc.c \ + src/base/abci/abcAttach.c \ + src/base/abci/abcBalance.c \ + src/base/abci/abcCollapse.c \ + src/base/abci/abcCut.c \ + src/base/abci/abcDsd.c \ + src/base/abci/abcFpga.c \ + src/base/abci/abcFraig.c \ + src/base/abci/abcFxu.c \ + src/base/abci/abcMap.c \ + src/base/abci/abcMiter.c \ + src/base/abci/abcNtbdd.c \ + src/base/abci/abcPrint.c \ + src/base/abci/abcReconv.c \ + src/base/abci/abcRefactor.c \ + src/base/abci/abcRenode.c \ + src/base/abci/abcRewrite.c \ + src/base/abci/abcSat.c \ + src/base/abci/abcStrash.c \ + src/base/abci/abcSweep.c \ + src/base/abci/abcSymm.c \ + src/base/abci/abcTiming.c \ + src/base/abci/abcUnreach.c \ + src/base/abci/abcVerify.c diff --git a/src/base/abc/abcSeqRetime.c b/src/base/abcs/abcRetime.c index 13b8a926..13b8a926 100644 --- a/src/base/abc/abcSeqRetime.c +++ b/src/base/abcs/abcRetime.c diff --git a/src/base/abc/abcSeq.c b/src/base/abcs/abcSeq.c index d6b1b8e5..d6b1b8e5 100644 --- a/src/base/abc/abcSeq.c +++ b/src/base/abcs/abcSeq.c diff --git a/src/sat/sim/simUnate.c b/src/base/abcs/abc_.c index f7ad3557..bef3836f 100644 --- a/src/sat/sim/simUnate.c +++ b/src/base/abcs/abc_.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [simUnate.c] + FileName [abc_.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [Simulation to determine unateness of variables.] + Synopsis [] Author [Alan Mishchenko] @@ -14,12 +14,11 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: simUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "abc.h" -#include "sim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abcs/module.make b/src/base/abcs/module.make new file mode 100644 index 00000000..ad084bb8 --- /dev/null +++ b/src/base/abcs/module.make @@ -0,0 +1,2 @@ +SRC += src/base/abcs/abcRetime.c \ + src/base/abcs/abcSeq.c diff --git a/src/base/io/ioWriteDot_old.c b/src/base/io/ioWriteDot_old.c deleted file mode 100644 index 59bbbde3..00000000 --- a/src/base/io/ioWriteDot_old.c +++ /dev/null @@ -1,325 +0,0 @@ -/**CFile**************************************************************** - - FileName [ioWriteDot.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Command processing package.] - - Synopsis [Procedures to write the graph structure of AIG in DOT.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "io.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Writes the graph structure of AIG in DOT.] - - Description [Useful for graph visualization using tools such as GraphViz: - http://www.graphviz.org/] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName ) -{ - FILE * pFile; - Abc_Obj_t * pNode, * pFanin, * pPrev, * pTemp; - int LevelMin, LevelMax, fHasCos, Level, i; - int Limit = 200; - - if ( vNodes->nSize < 1 ) - { - printf( "The set has no nodes. DOT file is not written.\n" ); - return; - } - - if ( vNodes->nSize > Limit ) - { - printf( "The set has more than %d nodes. DOT file is not written.\n", Limit ); - return; - } - - // start the output file - if ( (pFile = fopen( pFileName, "w" )) == NULL ) - { - fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); - return; - } - - // mark the nodes from the set - Vec_PtrForEachEntry( vNodes, pNode, i ) - pNode->fMarkC = 1; - if ( vNodesShow ) - Vec_PtrForEachEntry( vNodesShow, pNode, i ) - pNode->fMarkB = 1; - - // find the largest and the smallest levels - LevelMin = 10000; - LevelMax = -1; - fHasCos = 0; - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Abc_ObjIsCo(pNode) ) - { - fHasCos = 1; - continue; - } - if ( LevelMin > (int)pNode->Level ) - LevelMin = pNode->Level; - if ( LevelMax < (int)pNode->Level ) - LevelMax = pNode->Level; - } - - // set the level of the CO nodes - if ( fHasCos ) - { - LevelMax++; - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Abc_ObjIsCo(pNode) ) - pNode->Level = LevelMax; - } - } - - // write the DOT header - fprintf( pFile, "# %s\n", "AIG generated by ABC" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "digraph AIG {\n" ); - fprintf( pFile, "size = \"7.5,10\";\n" ); -// fprintf( pFile, "ranksep = 0.5;\n" ); -// fprintf( pFile, "nodesep = 0.5;\n" ); - fprintf( pFile, "center = true;\n" ); -// fprintf( pFile, "edge [fontsize = 10];\n" ); -// fprintf( pFile, "edge [dir = back];\n" ); -// fprintf( pFile, "edge [dir = none];\n" ); - fprintf( pFile, "\n" ); - - // labels on the left of the picture - fprintf( pFile, "{\n" ); - fprintf( pFile, " node [shape = plaintext];\n" ); - fprintf( pFile, " edge [style = invis];\n" ); - fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); - fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); - // generate node names with labels - for ( Level = LevelMax; Level >= LevelMin; Level-- ) - { - // the visible node name - fprintf( pFile, " Level%d", Level ); - fprintf( pFile, " [label = " ); - // label name - fprintf( pFile, "\"" ); - fprintf( pFile, "\"" ); - fprintf( pFile, "];\n" ); - } - - // genetate the sequence of visible/invisible nodes to mark levels - fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); - for ( Level = LevelMax; Level >= LevelMin; Level-- ) - { - // the visible node name - fprintf( pFile, " Level%d", Level ); - // the connector - if ( Level != LevelMin ) - fprintf( pFile, " ->" ); - else - fprintf( pFile, ";" ); - } - fprintf( pFile, "\n" ); - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - - // generate title box on top - fprintf( pFile, "{\n" ); - fprintf( pFile, " rank = same;\n" ); - fprintf( pFile, " LevelTitle1;\n" ); - fprintf( pFile, " title1 [shape=plaintext,\n" ); - fprintf( pFile, " fontsize=20,\n" ); - fprintf( pFile, " fontname = \"Times-Roman\",\n" ); - fprintf( pFile, " label=\"" ); - fprintf( pFile, "%s", "AIG generated by ABC" ); - fprintf( pFile, "\\n" ); - fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName ); - fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); - fprintf( pFile, "\"\n" ); - fprintf( pFile, " ];\n" ); - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - - // generate statistics box - fprintf( pFile, "{\n" ); - fprintf( pFile, " rank = same;\n" ); - fprintf( pFile, " LevelTitle2;\n" ); - fprintf( pFile, " title2 [shape=plaintext,\n" ); - fprintf( pFile, " fontsize=18,\n" ); - fprintf( pFile, " fontname = \"Times-Roman\",\n" ); - fprintf( pFile, " label=\"" ); - fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin ); - fprintf( pFile, "\\n" ); - fprintf( pFile, "\"\n" ); - fprintf( pFile, " ];\n" ); - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - - // generate the POs - if ( fHasCos ) - { - fprintf( pFile, "{\n" ); - fprintf( pFile, " rank = same;\n" ); - // the labeling node of this level - fprintf( pFile, " Level%d;\n", LevelMax ); - // generat the PO nodes - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( !Abc_ObjIsCo(pNode) ) - continue; - fprintf( pFile, " Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":""), Abc_ObjName(pNode) ); - fprintf( pFile, ", shape = invtriangle" ); - if ( pNode->fMarkB ) - fprintf( pFile, ", style = filled" ); - fprintf( pFile, ", color = coral, fillcolor = coral" ); - fprintf( pFile, "];\n" ); - } - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - } - - // generate nodes of each rank - for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- ) - { - fprintf( pFile, "{\n" ); - fprintf( pFile, " rank = same;\n" ); - // the labeling node of this level - fprintf( pFile, " Level%d;\n", Level ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( (int)pNode->Level != Level ) - continue; - fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); - fprintf( pFile, ", shape = ellipse" ); - if ( pNode->fMarkB ) - fprintf( pFile, ", style = filled" ); - fprintf( pFile, "];\n" ); - } - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - } - - // generate the PI nodes if any - if ( LevelMin == 0 ) - { - fprintf( pFile, "{\n" ); - fprintf( pFile, " rank = same;\n" ); - // the labeling node of this level - fprintf( pFile, " Level%d;\n", LevelMin ); - // generat the PO nodes - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( !Abc_ObjIsCi(pNode) ) - continue; - fprintf( pFile, " Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Bot":""), Abc_ObjName(pNode) ); - fprintf( pFile, ", shape = triangle" ); - if ( pNode->fMarkB ) - fprintf( pFile, ", style = filled" ); - fprintf( pFile, ", color = coral, fillcolor = coral" ); - fprintf( pFile, "];\n" ); - } - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - } - - // generate invisible edges from the square down - fprintf( pFile, "title1 -> title2 [style = invis];\n" ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( (int)pNode->Level != LevelMax ) - continue; - fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id ); - } - - // generate edges - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Abc_ObjFaninNum(pNode) == 0 ) - continue; - // generate the edge from this node to the next - pFanin = Abc_ObjFanin0(pNode); - if ( pFanin->fMarkC ) - { - fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":"") ); - fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" ); - fprintf( pFile, ";\n" ); - } - if ( Abc_ObjFaninNum(pNode) == 1 ) - continue; - // generate the edge from this node to the next - pFanin = Abc_ObjFanin1(pNode); - if ( pFanin->fMarkC ) - { - fprintf( pFile, "Node%d", pNode->Id ); - fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") ); - fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" ); - fprintf( pFile, ";\n" ); - } - // generate the edges between the equivalent nodes - pPrev = pNode; - for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData ) - { - if ( pTemp->fMarkC ) - { - fprintf( pFile, "Node%d", pPrev->Id ); - fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", pTemp->Id ); - fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" ); - fprintf( pFile, ";\n" ); - pPrev = pTemp; - } - } - } - - fprintf( pFile, "}" ); - fprintf( pFile, "\n" ); - fprintf( pFile, "\n" ); - fclose( pFile ); - - // unmark the nodes from the set - Vec_PtrForEachEntry( vNodes, pNode, i ) - pNode->fMarkC = 0; - if ( vNodesShow ) - Vec_PtrForEachEntry( vNodesShow, pNode, i ) - pNode->fMarkB = 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h index 9dad1670..19241a74 100644 --- a/src/map/fpga/fpga.h +++ b/src/map/fpga/fpga.h @@ -91,6 +91,7 @@ extern void Fpga_ManSetFanoutViolations( Fpga_Man_t * p, int nVio ); extern void Fpga_ManSetChoiceNodeNum( Fpga_Man_t * p, int nChoiceNodes ); extern void Fpga_ManSetChoiceNum( Fpga_Man_t * p, int nChoices ); extern void Fpga_ManSetVerbose( Fpga_Man_t * p, int fVerbose ); +extern void Fpga_ManSetSwitching( Fpga_Man_t * p, int fSwitching ); extern void Fpga_ManSetLatchNum( Fpga_Man_t * p, int nLatches ); extern void Fpga_ManSetName( Fpga_Man_t * p, char * pFileName ); @@ -110,6 +111,7 @@ extern void Fpga_NodeSetData1( Fpga_Node_t * p, Fpga_Node_t * pNode ) extern void Fpga_NodeSetArrival( Fpga_Node_t * p, float Time ); extern void Fpga_NodeSetNextE( Fpga_Node_t * p, Fpga_Node_t * pNextE ); extern void Fpga_NodeSetRepr( Fpga_Node_t * p, Fpga_Node_t * pRepr ); +extern void Fpga_NodeSetSwitching( Fpga_Node_t * p, float Switching ); extern int Fpga_NodeIsConst( Fpga_Node_t * p ); extern int Fpga_NodeIsVar( Fpga_Node_t * p ); diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c index 0fc90228..95b9ca49 100644 --- a/src/map/fpga/fpgaCore.c +++ b/src/map/fpga/fpgaCore.c @@ -97,22 +97,26 @@ int Fpga_Mapping( Fpga_Man_t * p ) ***********************************************************************/ int Fpga_MappingPostProcess( Fpga_Man_t * p ) { - float aAreaTotalPrev, aAreaTotalCur, aAreaTotalCur2; + int fShowSwitching = 0; + int fRecoverAreaFlow = 1; + int fRecoverArea = 1; + float aAreaTotalCur, aAreaTotalCur2; int Iter, clk; // compute area, set references, and collect nodes used in the mapping + Iter = 1; aAreaTotalCur = Fpga_MappingSetRefsAndArea( p ); if ( p->fVerbose ) { -printf( "Iteration %dD : Area = %11.1f ", 0, aAreaTotalCur ); +printf( "Iteration %dD : Area = %8.1f ", Iter++, aAreaTotalCur ); +if ( fShowSwitching ) +printf( "Switch = %8.1f ", Fpga_MappingGetSwitching(p,p->vMapping) ); PRT( "Time", p->timeMatch ); } - Iter = 1; - do { + if ( fRecoverAreaFlow ) + { clk = clock(); - // save the previous area flow - aAreaTotalPrev = aAreaTotalCur; // compute the required times and the fanouts Fpga_TimeComputeRequiredGlobal( p ); // remap topologically @@ -124,33 +128,38 @@ clk = clock(); // for some reason, this works better on benchmarks if ( p->fVerbose ) { -printf( "Iteration %dF : Area = %11.1f ", Iter++, aAreaTotalCur ); +printf( "Iteration %dF : Area = %8.1f ", Iter++, aAreaTotalCur ); +if ( fShowSwitching ) +printf( "Switch = %8.1f ", Fpga_MappingGetSwitching(p,p->vMapping) ); PRT( "Time", clock() - clk ); } - // quit if this iteration reduced area flow by less than 1% - } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur ); + } // update reference counters aAreaTotalCur2 = Fpga_MappingSetRefsAndArea( p ); assert( aAreaTotalCur == aAreaTotalCur2 ); - do { + if ( fRecoverArea ) + { clk = clock(); - // save the previous area flow - aAreaTotalPrev = aAreaTotalCur; // compute the required times and the fanouts Fpga_TimeComputeRequiredGlobal( p ); // remap topologically - Fpga_MappingMatchesArea( p ); + if ( p->fSwitching ) + Fpga_MappingMatchesSwitch( p ); + else + Fpga_MappingMatchesArea( p ); // get the resulting area aAreaTotalCur = Fpga_MappingSetRefsAndArea( p ); if ( p->fVerbose ) { -printf( "Iteration %dA : Area = %11.1f ", Iter++, aAreaTotalCur ); +printf( "Iteration %d%s : Area = %8.1f ", Iter++, (p->fSwitching?"S":"A"), aAreaTotalCur ); +if ( fShowSwitching ) +printf( "Switch = %8.1f ", Fpga_MappingGetSwitching(p,p->vMapping) ); PRT( "Time", clock() - clk ); } - // quit if this iteration reduced area flow by less than 1% - } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur ); + } + p->fAreaGlo = aAreaTotalCur; return 1; } diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c index f3abbedb..b7bfa3c5 100644 --- a/src/map/fpga/fpgaCreate.c +++ b/src/map/fpga/fpgaCreate.c @@ -65,6 +65,7 @@ void Fpga_ManSetTimeLimit( Fpga_Man_t * p, float TimeLimit ) { p void Fpga_ManSetChoiceNodeNum( Fpga_Man_t * p, int nChoiceNodes ) { p->nChoiceNodes = nChoiceNodes; } void Fpga_ManSetChoiceNum( Fpga_Man_t * p, int nChoices ) { p->nChoices = nChoices; } void Fpga_ManSetVerbose( Fpga_Man_t * p, int fVerbose ) { p->fVerbose = fVerbose; } +void Fpga_ManSetSwitching( Fpga_Man_t * p, int fSwitching ) { p->fSwitching = fSwitching; } void Fpga_ManSetLatchNum( Fpga_Man_t * p, int nLatches ) { p->nLatches = nLatches; } void Fpga_ManSetName( Fpga_Man_t * p, char * pFileName ) { p->pFileName = pFileName; } @@ -104,6 +105,7 @@ void Fpga_NodeSetData0( Fpga_Node_t * p, char * pData ) { p-> void Fpga_NodeSetData1( Fpga_Node_t * p, Fpga_Node_t * pNode ) { p->pLevel = pNode; } void Fpga_NodeSetNextE( Fpga_Node_t * p, Fpga_Node_t * pNextE ) { p->pNextE = pNextE; } void Fpga_NodeSetRepr( Fpga_Node_t * p, Fpga_Node_t * pRepr ) { p->pRepr = pRepr; } +void Fpga_NodeSetSwitching( Fpga_Node_t * p, float Switching ) { p->Switching = Switching; } /**Function************************************************************* diff --git a/src/map/fpga/fpgaCutUtils.c b/src/map/fpga/fpgaCutUtils.c index abe703a2..2419cac4 100644 --- a/src/map/fpga/fpgaCutUtils.c +++ b/src/map/fpga/fpgaCutUtils.c @@ -439,109 +439,6 @@ float Fpga_CutDeref( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, } - -/**function************************************************************* - - synopsis [Computes the exact area associated with the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -float Fpga_CutGetSwitchDerefed( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ) -{ - float aResult, aResult2; - if ( pCut->nLeaves == 1 ) - return 0; - aResult2 = Fpga_CutRefSwitch( pMan, pNode, pCut, 0 ); - aResult = Fpga_CutDerefSwitch( pMan, pNode, pCut, 0 ); -// assert( aResult == aResult2 ); - return aResult; -} - -/**function************************************************************* - - synopsis [References the cut.] - - description [This procedure is similar to the procedure NodeReclaim.] - - sideeffects [] - - seealso [] - -***********************************************************************/ -float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ) -{ - Fpga_Node_t * pNodeChild; - float aArea; - int i; - - // deref the fanouts -// if ( fFanouts ) -// Fpga_CutInsertFanouts( pMan, pNode, pCut ); - - // start the area of this cut - aArea = pNode->SwitchProb; - // go through the children - for ( i = 0; i < pCut->nLeaves; i++ ) - { - pNodeChild = pCut->ppLeaves[i]; - assert( pNodeChild->nRefs >= 0 ); - if ( pNodeChild->nRefs++ > 0 ) - continue; - if ( !Fpga_NodeIsAnd(pNodeChild) ) - { - aArea += pNodeChild->SwitchProb; - continue; - } - aArea += Fpga_CutRefSwitch( pMan, pNodeChild, pNodeChild->pCutBest, fFanouts ); - } - return aArea; -} - -/**function************************************************************* - - synopsis [Dereferences the cut.] - - description [This procedure is similar to the procedure NodeRecusiveDeref.] - - sideeffects [] - - seealso [] - -***********************************************************************/ -float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ) -{ - Fpga_Node_t * pNodeChild; - float aArea; - int i; - - // deref the fanouts -// if ( fFanouts ) -// Fpga_CutRemoveFanouts( pMan, pNode, pCut ); - - // start the area of this cut - aArea = pNode->SwitchProb; - // go through the children - for ( i = 0; i < pCut->nLeaves; i++ ) - { - pNodeChild = pCut->ppLeaves[i]; - assert( pNodeChild->nRefs > 0 ); - if ( --pNodeChild->nRefs > 0 ) - continue; - if ( !Fpga_NodeIsAnd(pNodeChild) ) - { - aArea += pNodeChild->SwitchProb; - continue; - } - aArea += Fpga_CutDerefSwitch( pMan, pNodeChild, pNodeChild->pCutBest, fFanouts ); - } - return aArea; -} - /**Function************************************************************* Synopsis [Sets the used cuts to be the currently selected ones.] diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h index 95203378..ec6057a7 100644 --- a/src/map/fpga/fpgaInt.h +++ b/src/map/fpga/fpgaInt.h @@ -120,12 +120,9 @@ struct Fpga_ManStruct_t_ // mapping parameters int nVarsMax; // the max number of variables -// int fTree; // the flag to enable tree mapping -// int fPower; // the flag to enable power optimization int fAreaRecovery; // the flag to use area flow as the first parameter int fVerbose; // the verbosiness flag -// int fRefCount; // enables reference counting -// int fSequential; // use sequential mapping + int fSwitching; // minimize the switching activity (instead of area) int nTravIds; // support of choice nodes @@ -137,7 +134,6 @@ struct Fpga_ManStruct_t_ // the supergate library Fpga_LutLib_t * pLutLib; // the current LUT library -// unsigned uTruths[6][2]; // the elementary truth tables // the memory managers Extra_MmFixed_t * mmNodes; // the memory manager for nodes @@ -215,7 +211,7 @@ struct Fpga_NodeStruct_t_ // the delay information float tRequired; // the best area flow float aEstFanouts; // the fanout estimation - float SwitchProb; // the probability of switching + float Switching; // the probability of switching int LValue; // the l-value of the node short nLatches1; // the number of latches on the first edge short nLatches2; // the number of latches on the second edge @@ -308,9 +304,6 @@ extern float Fpga_CutGetAreaRefed( Fpga_Man_t * pMan, Fpga_Cut_t * p extern float Fpga_CutGetAreaDerefed( Fpga_Man_t * pMan, Fpga_Cut_t * pCut ); extern float Fpga_CutRef( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); extern float Fpga_CutDeref( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); -extern float Fpga_CutGetSwitchDerefed( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ); -extern float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); -extern float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); extern float Fpga_CutGetAreaFlow( Fpga_Man_t * pMan, Fpga_Cut_t * pCut ); extern void Fpga_CutGetParameters( Fpga_Man_t * pMan, Fpga_Cut_t * pCut ); /*=== fraigFanout.c =============================================================*/ @@ -329,6 +322,11 @@ extern int Fpga_MappingMatchesSwitch( Fpga_Man_t * p ); /*=== fpgaShow.c =============================================================*/ extern void Fpga_MappingShow( Fpga_Man_t * pMan, char * pFileName ); extern void Fpga_MappingShowNodes( Fpga_Man_t * pMan, Fpga_Node_t ** ppRoots, int nRoots, char * pFileName ); +/*=== fpgaSwitch.c =============================================================*/ +extern float Fpga_CutGetSwitchDerefed( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ); +extern float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); +extern float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ); +extern float Fpga_MappingGetSwitching( Fpga_Man_t * pMan, Fpga_NodeVec_t * vMapping ); /*=== fpgaTime.c ===============================================================*/ extern float Fpga_TimeCutComputeArrival( Fpga_Man_t * pMan, Fpga_Cut_t * pCut ); extern float Fpga_TimeCutComputeArrival_rec( Fpga_Man_t * pMan, Fpga_Cut_t * pCut ); @@ -370,7 +368,6 @@ extern void Fpga_MappingSetupMask( unsigned uMask[], int nVarsMax ) extern void Fpga_MappingSortByLevel( Fpga_Man_t * pMan, Fpga_NodeVec_t * vNodes, int fIncreasing ); extern Fpga_NodeVec_t * Fpga_DfsLim( Fpga_Man_t * pMan, Fpga_Node_t * pNode, int nLevels ); extern Fpga_NodeVec_t * Fpga_MappingLevelize( Fpga_Man_t * pMan, Fpga_NodeVec_t * vNodes ); -extern float Fpga_MappingPrintSwitching( Fpga_Man_t * pMan ); extern int Fpga_MappingMaxLevel( Fpga_Man_t * pMan ); extern void Fpga_ManReportChoices( Fpga_Man_t * pMan ); extern void Fpga_MappingSetChoiceLevels( Fpga_Man_t * pMan ); diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c index 63ee682d..20444209 100644 --- a/src/map/fpga/fpgaMatch.c +++ b/src/map/fpga/fpgaMatch.c @@ -432,7 +432,7 @@ clk = clock(); if ( pNode->nRefs ) { pNode->pCutBest->aFlow = Fpga_CutRefSwitch( p, pNode, pNode->pCutBest, 0 ); - assert( pNode->pCutBest->aFlow <= aAreaCutBest ); + assert( pNode->pCutBest->aFlow <= aAreaCutBest + 0.001 ); // assert( pNode->tRequired < FPGA_FLOAT_LARGE ); } return 1; diff --git a/src/map/fpga/fpgaSwitch.c b/src/map/fpga/fpgaSwitch.c new file mode 100644 index 00000000..0d2ec3fc --- /dev/null +++ b/src/map/fpga/fpgaSwitch.c @@ -0,0 +1,176 @@ +/**CFile**************************************************************** + + FileName [fpgaSwitch.c] + + PackageName [MVSIS 1.3: Multi-valued logic synthesis system.] + + Synopsis [Generic technology mapping engine.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 8, 2003.] + + Revision [$Id: fpgaSwitch.h,v 1.0 2003/09/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fpgaInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static float Fpga_CutGetSwitching( Fpga_Cut_t * pCut ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**function************************************************************* + + synopsis [Computes the exact area associated with the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Fpga_CutGetSwitchDerefed( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ) +{ + float aResult, aResult2; + aResult2 = Fpga_CutRefSwitch( pMan, pNode, pCut, 0 ); + aResult = Fpga_CutDerefSwitch( pMan, pNode, pCut, 0 ); +// assert( aResult == aResult2 ); + return aResult; +} + +/**function************************************************************* + + synopsis [References the cut.] + + description [This procedure is similar to the procedure NodeReclaim.] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Fpga_CutRefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ) +{ + Fpga_Node_t * pNodeChild; + float aArea; + int i; + if ( pCut->nLeaves == 1 ) + return 0; + // start the area of this cut + aArea = Fpga_CutGetSwitching( pCut ); + // go through the children + for ( i = 0; i < pCut->nLeaves; i++ ) + { + pNodeChild = pCut->ppLeaves[i]; + assert( pNodeChild->nRefs >= 0 ); + if ( pNodeChild->nRefs++ > 0 ) + continue; + aArea += Fpga_CutRefSwitch( pMan, pNodeChild, pNodeChild->pCutBest, fFanouts ); + } + return aArea; +} + +/**function************************************************************* + + synopsis [Dereferences the cut.] + + description [This procedure is similar to the procedure NodeRecusiveDeref.] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Fpga_CutDerefSwitch( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Cut_t * pCut, int fFanouts ) +{ + Fpga_Node_t * pNodeChild; + float aArea; + int i; + if ( pCut->nLeaves == 1 ) + return 0; + // start the area of this cut + aArea = Fpga_CutGetSwitching( pCut ); + // go through the children + for ( i = 0; i < pCut->nLeaves; i++ ) + { + pNodeChild = pCut->ppLeaves[i]; + assert( pNodeChild->nRefs > 0 ); + if ( --pNodeChild->nRefs > 0 ) + continue; + aArea += Fpga_CutDerefSwitch( pMan, pNodeChild, pNodeChild->pCutBest, fFanouts ); + } + return aArea; +} + +/**function************************************************************* + + synopsis [Computes the exact area associated with the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Fpga_CutGetSwitching( Fpga_Cut_t * pCut ) +{ + float Result; + int i; + Result = 0.0; + for ( i = 0; i < pCut->nLeaves; i++ ) + Result += pCut->ppLeaves[i]->Switching; + return Result; +} + +/**Function************************************************************* + + Synopsis [Computes the array of mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Fpga_MappingGetSwitching( Fpga_Man_t * pMan, Fpga_NodeVec_t * vMapping ) +{ + Fpga_Node_t * pNode; + float Switch; + int i; + Switch = 0.0; + for ( i = 0; i < vMapping->nSize; i++ ) + { + pNode = vMapping->pArray[i]; + if ( !Fpga_NodeIsAnd(pNode) ) + continue; + // at least one phase has the best cut assigned + assert( pNode->pCutBest != NULL ); + // at least one phase is used in the mapping + assert( pNode->nRefs > 0 ); + // compute the array due to the supergate + Switch += pNode->Switching; + } + // add buffer for each CO driven by a CI + for ( i = 0; i < pMan->nOutputs; i++ ) + if ( Fpga_NodeIsVar(pMan->pOutputs[i]) && !Fpga_IsComplement(pMan->pOutputs[i]) ) + Switch += pMan->pOutputs[i]->Switching; + return Switch; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c index 89ef13dc..3ea1f2f1 100644 --- a/src/map/fpga/fpgaUtils.c +++ b/src/map/fpga/fpgaUtils.c @@ -779,43 +779,6 @@ Fpga_NodeVec_t * Fpga_MappingLevelize( Fpga_Man_t * pMan, Fpga_NodeVec_t * vNode } return vLevels; } -/**Function************************************************************* - - Synopsis [Prints the switching activity changes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float Fpga_MappingPrintSwitching( Fpga_Man_t * p ) -{ - Fpga_Node_t * pNode; - float SwitchTotal = 0.0; - int nNodes = 0; - int i; - for ( i = 0; i < p->vNodesAll->nSize; i++ ) - { - // skip primary inputs - pNode = p->vNodesAll->pArray[i]; -// if ( !Fpga_NodeIsAnd( pNode ) ) -// continue; - // skip a secondary node - if ( pNode->pRepr ) - continue; - // count the switching nodes - if ( pNode->nRefs > 0 ) - { - SwitchTotal += pNode->SwitchProb; - nNodes++; - } - } - if ( p->fVerbose ) - printf( "Total switching = %10.2f. Average switching = %6.4f.\n", SwitchTotal, SwitchTotal/nNodes ); - return SwitchTotal; -} /**Function************************************************************* diff --git a/src/map/fpga/module.make b/src/map/fpga/module.make index 409e4b54..cc3a6573 100644 --- a/src/map/fpga/module.make +++ b/src/map/fpga/module.make @@ -6,6 +6,7 @@ SRC += src/map/fpga/fpga.c \ src/map/fpga/fpgaFanout.c \ src/map/fpga/fpgaLib.c \ src/map/fpga/fpgaMatch.c \ + src/map/fpga/fpgaSwitch.c \ src/map/fpga/fpgaTime.c \ src/map/fpga/fpgaTruth.c \ src/map/fpga/fpgaUtils.c \ diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h index 1322cdfa..c3f1ce81 100644 --- a/src/map/mapper/mapper.h +++ b/src/map/mapper/mapper.h @@ -101,6 +101,7 @@ extern void Map_ManSetFanoutViolations( Map_Man_t * p, int nVio ); extern void Map_ManSetChoiceNodeNum( Map_Man_t * p, int nChoiceNodes ); extern void Map_ManSetChoiceNum( Map_Man_t * p, int nChoices ); extern void Map_ManSetVerbose( Map_Man_t * p, int fVerbose ); +extern void Map_ManSetSwitching( Map_Man_t * p, int fSwitching ); extern Map_Man_t * Map_NodeReadMan( Map_Node_t * p ); extern char * Map_NodeReadData( Map_Node_t * p, int fPhase ); @@ -113,6 +114,7 @@ extern Map_Node_t * Map_NodeReadTwo( Map_Node_t * p ); extern void Map_NodeSetData( Map_Node_t * p, int fPhase, char * pData ); extern void Map_NodeSetNextE( Map_Node_t * p, Map_Node_t * pNextE ); extern void Map_NodeSetRepr( Map_Node_t * p, Map_Node_t * pRepr ); +extern void Map_NodeSetSwitching( Map_Node_t * p, float Switching ); extern int Map_NodeIsConst( Map_Node_t * p ); extern int Map_NodeIsVar( Map_Node_t * p ); diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c index 16cbfd5c..629ba59d 100644 --- a/src/map/mapper/mapperCore.c +++ b/src/map/mapper/mapperCore.c @@ -46,9 +46,10 @@ ***********************************************************************/ int Map_Mapping( Map_Man_t * p ) { + int fShowSwitching = 0; int fUseAreaFlow = 1; - int fUseExactArea = 1; - int fUseExactAreaWithPhase = 1; + int fUseExactArea = !p->fSwitching; + int fUseExactAreaWithPhase = !p->fSwitching; int clk; ////////////////////////////////////////////////////////////////////// @@ -83,8 +84,10 @@ int Map_Mapping( Map_Man_t * p ) p->AreaBase = Map_MappingGetArea( p, p->vMapping ); if ( p->fVerbose ) { -printf( "Delay : Delay = %5.2f Flow = %11.1f Area = %11.1f %4.1f %% ", - p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 ); +printf( "Delay : %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 ); PRT( "Time", p->timeMatch ); } ////////////////////////////////////////////////////////////////////// @@ -97,7 +100,7 @@ PRT( "Time", p->timeMatch ); clk = clock(); if ( fUseAreaFlow ) { - // compute the required times and the fanouts + // compute the required times Map_TimeComputeRequiredGlobal( p ); // recover area flow p->fMappingMode = 1; @@ -107,8 +110,10 @@ PRT( "Time", p->timeMatch ); p->AreaFinal = Map_MappingGetArea( p, p->vMapping ); if ( p->fVerbose ) { -printf( "AreaFlow : Delay = %5.2f Flow = %11.1f Area = %11.1f %4.1f %% ", - p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaFinal, +printf( "AreaFlow : %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + Map_MappingGetAreaFlow(p), p->AreaFinal, 100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase ); PRT( "Time", clock() - clk ); } @@ -121,9 +126,9 @@ PRT( "Time", clock() - clk ); clk = clock(); if ( fUseExactArea ) { - // compute the required times and the fanouts + // compute the required times Map_TimeComputeRequiredGlobal( p ); - // recover area flow + // recover area p->fMappingMode = 2; Map_MappingMatches( p ); // compute the references and collect the nodes used in the mapping @@ -131,8 +136,10 @@ PRT( "Time", clock() - clk ); p->AreaFinal = Map_MappingGetArea( p, p->vMapping ); if ( p->fVerbose ) { -printf( "Area : Delay = %5.2f Flow = %11.1f Area = %11.1f %4.1f %% ", - p->fRequiredGlo, 0.0, p->AreaFinal, +printf( "Area : %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + 0.0, p->AreaFinal, 100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase ); PRT( "Time", clock() - clk ); } @@ -145,9 +152,9 @@ PRT( "Time", clock() - clk ); clk = clock(); if ( fUseExactAreaWithPhase ) { - // compute the required times and the fanouts + // compute the required times Map_TimeComputeRequiredGlobal( p ); - // recover area flow + // recover area p->fMappingMode = 3; Map_MappingMatches( p ); // compute the references and collect the nodes used in the mapping @@ -155,8 +162,54 @@ PRT( "Time", clock() - clk ); p->AreaFinal = Map_MappingGetArea( p, p->vMapping ); if ( p->fVerbose ) { -printf( "Area : Delay = %5.2f Flow = %11.1f Area = %11.1f %4.1f %% ", - p->fRequiredGlo, 0.0, p->AreaFinal, +printf( "Area : %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + 0.0, p->AreaFinal, + 100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase ); +PRT( "Time", clock() - clk ); +} + } + p->timeArea += clock() - clk; + ////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////// + // perform area recovery using exact area + clk = clock(); + if ( p->fSwitching ) + { + // compute the required times + Map_TimeComputeRequiredGlobal( p ); + // recover switching activity + p->fMappingMode = 4; + Map_MappingMatches( p ); + // compute the references and collect the nodes used in the mapping + Map_MappingSetRefs( p ); + p->AreaFinal = Map_MappingGetArea( p, p->vMapping ); +if ( p->fVerbose ) +{ +printf( "Switching: %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + 0.0, p->AreaFinal, + 100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase ); +PRT( "Time", clock() - clk ); +} + + // compute the required times + Map_TimeComputeRequiredGlobal( p ); + // recover switching activity + p->fMappingMode = 4; + Map_MappingMatches( p ); + // compute the references and collect the nodes used in the mapping + Map_MappingSetRefs( p ); + p->AreaFinal = Map_MappingGetArea( p, p->vMapping ); +if ( p->fVerbose ) +{ +printf( "Switching: %s = %8.2f Flow = %11.1f Area = %11.1f %4.1f %% ", + fShowSwitching? "Switch" : "Delay", + fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, + 0.0, p->AreaFinal, 100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase ); PRT( "Time", clock() - clk ); } diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c index 738d099c..31fbf0ea 100644 --- a/src/map/mapper/mapperCreate.c +++ b/src/map/mapper/mapperCreate.c @@ -69,6 +69,7 @@ void Map_ManSetFanoutViolations( Map_Man_t * p, int nVio ) { p->nFa void Map_ManSetChoiceNodeNum( Map_Man_t * p, int nChoiceNodes ) { p->nChoiceNodes = nChoiceNodes; } void Map_ManSetChoiceNum( Map_Man_t * p, int nChoices ) { p->nChoices = nChoices; } void Map_ManSetVerbose( Map_Man_t * p, int fVerbose ) { p->fVerbose = fVerbose; } +void Map_ManSetSwitching( Map_Man_t * p, int fSwitching ) { p->fSwitching = fSwitching; } /**Function************************************************************* @@ -90,8 +91,9 @@ Map_Cut_t * Map_NodeReadCutBest( Map_Node_t * p, int fPhase ) { return p Map_Node_t * Map_NodeReadOne( Map_Node_t * p ) { return p->p1; } Map_Node_t * Map_NodeReadTwo( Map_Node_t * p ) { return p->p2; } void Map_NodeSetData( Map_Node_t * p, int fPhase, char * pData ) { if (fPhase) p->pData1 = pData; else p->pData0 = pData; } -void Map_NodeSetNextE( Map_Node_t * p, Map_Node_t * pNextE ) { p->pNextE = pNextE; } -void Map_NodeSetRepr( Map_Node_t * p, Map_Node_t * pRepr ) { p->pRepr = pRepr; } +void Map_NodeSetNextE( Map_Node_t * p, Map_Node_t * pNextE ) { p->pNextE = pNextE; } +void Map_NodeSetRepr( Map_Node_t * p, Map_Node_t * pRepr ) { p->pRepr = pRepr; } +void Map_NodeSetSwitching( Map_Node_t * p, float Switching ) { p->Switching = Switching; } /**Function************************************************************* diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h index 7d63a804..0acca56c 100644 --- a/src/map/mapper/mapperInt.h +++ b/src/map/mapper/mapperInt.h @@ -117,6 +117,7 @@ struct Map_ManStruct_t_ bool fObeyFanoutLimits;// Should mapper try to obey fanout limits or not float DelayTarget; // the required times set by the user int nTravIds; // the traversal counter + bool fSwitching; // Should mapper try to obey fanout limits or not // the supergate library Map_SuperLib_t * pSuperLib; // the current supergate library @@ -184,6 +185,7 @@ struct Map_SuperLibStruct_t_ Mio_Gate_t * pGateInv; // the pointer to the intertor gate Map_Time_t tDelayInv; // the delay of the inverter float AreaInv; // the area of the inverter + float AreaBuf; // the area of the buffer Map_Super_t * pSuperInv; // the supergate representing the inverter // the memory manager for the internal table @@ -210,6 +212,7 @@ struct Map_NodeStruct_t_ unsigned NumTemp:10; // the level of the given node int nRefAct[3]; // estimated fanout for current covering phase, neg and pos and sum float nRefEst[3]; // actual fanout for previous covering phase, neg and pos and sum + float Switching; // the probability of switching // connectivity Map_Node_t * p1; // the first child @@ -378,6 +381,11 @@ extern int Map_MappingMatches( Map_Man_t * p ); extern float Map_MappingCombinePhases( Map_Man_t * p ); extern void Map_MatchClean( Map_Match_t * pMatch ); extern int Map_MatchCompare( Map_Man_t * pMan, Map_Match_t * pM1, Map_Match_t * pM2, int fDoingArea ); +/*=== mapperPower.c =============================================================*/ +extern float Map_SwitchCutGetDerefed( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ); +extern float Map_SwitchCutRef( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ); +extern float Map_SwitchCutDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ); +extern float Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping ); /*=== mapperRefs.c =============================================================*/ extern int Map_NodeReadRefPhaseAct( Map_Node_t * pNode, int fPhase ); extern float Map_NodeReadRefPhaseEst( Map_Node_t * pNode, int fPhase ); diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c index f9b280fe..5fea1f00 100644 --- a/src/map/mapper/mapperLib.c +++ b/src/map/mapper/mapperLib.c @@ -102,6 +102,7 @@ if ( fVerbose ) { p->tDelayInv.Fall = Mio_LibraryReadDelayInvFall( p->pGenlib ); p->tDelayInv.Worst = MAP_MAX( p->tDelayInv.Rise, p->tDelayInv.Fall ); p->AreaInv = Mio_LibraryReadAreaInv( p->pGenlib ); + p->AreaBuf = Mio_LibraryReadAreaBuf( p->pGenlib ); // assign the interver supergate p->pSuperInv = (Map_Super_t *)Extra_MmFixedEntryFetch( p->mmSupers ); diff --git a/src/map/mapper/mapperMatch.c b/src/map/mapper/mapperMatch.c index 5b72311c..ddb9ebb7 100644 --- a/src/map/mapper/mapperMatch.c +++ b/src/map/mapper/mapperMatch.c @@ -65,7 +65,7 @@ int Map_MappingMatches( Map_Man_t * p ) Map_Node_t * pNode; int i; - assert( p->fMappingMode >= 0 && p->fMappingMode <= 3 ); + assert( p->fMappingMode >= 0 && p->fMappingMode <= 4 ); // use the externally given PI arrival times if ( p->fMappingMode == 0 ) @@ -158,7 +158,7 @@ int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase ) // recompute the exact area of the current best match // because the exact area of the fanins may have changed // as a result of remapping fanins in the topological order - if ( p->fMappingMode >= 2 ) + if ( p->fMappingMode == 2 || p->fMappingMode == 3 ) { pMatch = pCutBest->M + fPhase; if ( pNode->nRefAct[fPhase] > 0 || @@ -167,6 +167,15 @@ int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase ) else pMatch->AreaFlow = Area1 = Map_CutGetAreaDerefed( pCutBest, fPhase ); } + else if ( p->fMappingMode == 4 ) + { + pMatch = pCutBest->M + fPhase; + if ( pNode->nRefAct[fPhase] > 0 || + (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0) ) + pMatch->AreaFlow = Area1 = Map_SwitchCutDeref( pNode, pCutBest, fPhase ); + else + pMatch->AreaFlow = Area1 = Map_SwitchCutGetDerefed( pNode, pCutBest, fPhase ); + } // save the old mapping if ( pCutBest ) @@ -210,7 +219,12 @@ int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase ) (pNode->nRefAct[fPhase] > 0 || (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0)) ) { - Area2 = Map_CutRef( pNode->pCutBest[fPhase], fPhase ); + if ( p->fMappingMode == 2 || p->fMappingMode == 3 ) + Area2 = Map_CutRef( pNode->pCutBest[fPhase], fPhase ); + else if ( p->fMappingMode == 4 ) + Area2 = Map_SwitchCutRef( pNode, pNode->pCutBest[fPhase], fPhase ); + else + assert( 0 ); assert( Area2 < Area1 + p->fEpsilon ); } @@ -273,9 +287,11 @@ int Map_MatchNodeCut( Map_Man_t * p, Map_Node_t * pNode, Map_Cut_t * pCut, int f else { // get the area (area flow) - if ( p->fMappingMode >= 2 ) + if ( p->fMappingMode == 2 || p->fMappingMode == 3 ) pMatch->AreaFlow = Map_CutGetAreaDerefed( pCut, fPhase ); - else + else if ( p->fMappingMode == 4 ) + pMatch->AreaFlow = Map_SwitchCutGetDerefed( pNode, pCut, fPhase ); + else pMatch->AreaFlow = Map_CutGetAreaFlow( pCut, fPhase ); // skip if the cut is too large if ( pMatch->AreaFlow > MatchBest.AreaFlow + p->fEpsilon ) @@ -304,9 +320,11 @@ int Map_MatchNodeCut( Map_Man_t * p, Map_Node_t * pNode, Map_Cut_t * pCut, int f if ( pMatch->pSuperBest ) { Map_TimeCutComputeArrival( pNode, pCut, fPhase, MAP_FLOAT_LARGE ); - if ( p->fMappingMode >= 2 ) + if ( p->fMappingMode == 2 || p->fMappingMode == 3 ) pMatch->AreaFlow = Map_CutGetAreaDerefed( pCut, fPhase ); - else + else if ( p->fMappingMode == 4 ) + pMatch->AreaFlow = Map_SwitchCutGetDerefed( pNode, pCut, fPhase ); + else pMatch->AreaFlow = Map_CutGetAreaFlow( pCut, fPhase ); } return 1; @@ -482,7 +500,7 @@ void Map_NodeTryDroppingOnePhase( Map_Man_t * p, Map_Node_t * pNode ) fUsePhase0 = (pNode->tRequired[1].Worst > tWorst1Using0 + 3*p->pSuperLib->tDelayInv.Worst + p->fEpsilon); fUsePhase1 = (pNode->tRequired[0].Worst > tWorst0Using1 + 3*p->pSuperLib->tDelayInv.Worst + p->fEpsilon); } - else if ( p->fMappingMode == 3 ) + else if ( p->fMappingMode == 3 || p->fMappingMode == 4 ) { fUsePhase0 = (pNode->tRequired[1].Worst > tWorst1Using0 + p->fEpsilon); fUsePhase1 = (pNode->tRequired[0].Worst > tWorst0Using1 + p->fEpsilon); diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c index e74bab9a..e4adadae 100644 --- a/src/map/mapper/mapperRefs.c +++ b/src/map/mapper/mapperRefs.c @@ -279,7 +279,7 @@ float Map_CutRef( Map_Cut_t * pCut, int fPhase ) /**function************************************************************* - synopsis [References the cut.] + synopsis [Dereferences the cut.] description [] @@ -298,8 +298,7 @@ float Map_CutDeref( Map_Cut_t * pCut, int fPhase ) synopsis [References or dereferences the cut.] description [This reference part is similar to Cudd_NodeReclaim(). - The dereference part is similar to Cudd_RecursiveDeref(). The - area of the inverter is not counted.] + The dereference part is similar to Cudd_RecursiveDeref().] sideeffects [] @@ -543,10 +542,10 @@ float Map_MappingGetArea( Map_Man_t * pMan, Map_NodeVec_t * vMapping ) (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) ) Area += pMan->pSuperLib->AreaInv; } - // add two inverters for each PO buffer + // add buffer for each CO driven by a CI for ( i = 0; i < pMan->nOutputs; i++ ) if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) ) - Area += 2 * pMan->pSuperLib->AreaInv; + Area += pMan->pSuperLib->AreaBuf; return Area; } diff --git a/src/map/mapper/mapperSwitch.c b/src/map/mapper/mapperSwitch.c new file mode 100644 index 00000000..02f38396 --- /dev/null +++ b/src/map/mapper/mapperSwitch.c @@ -0,0 +1,243 @@ +/**CFile**************************************************************** + + FileName [mapperSwitch.c] + + PackageName [MVSIS 1.3: Multi-valued logic synthesis system.] + + Synopsis [Generic technology mapping engine.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 8, 2003.] + + Revision [$Id: mapperSwitch.h,v 1.0 2003/09/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mapperInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, int fReference ); +static float Map_CutGetSwitching( Map_Cut_t * pCut ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**function************************************************************* + + synopsis [Computes the exact area associated with the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Map_SwitchCutGetDerefed( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ) +{ + float aResult, aResult2; +// assert( pNode->Switching > 0 ); + aResult2 = Map_SwitchCutRefDeref( pNode, pCut, fPhase, 1 ); // reference + aResult = Map_SwitchCutRefDeref( pNode, pCut, fPhase, 0 ); // dereference +// assert( aResult == aResult2 ); + return aResult; +} + +/**function************************************************************* + + synopsis [References the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Map_SwitchCutRef( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ) +{ + return Map_SwitchCutRefDeref( pNode, pCut, fPhase, 1 ); // reference +} + +/**function************************************************************* + + synopsis [References the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Map_SwitchCutDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ) +{ + return Map_SwitchCutRefDeref( pNode, pCut, fPhase, 0 ); // dereference +} + +/**function************************************************************* + + synopsis [References or dereferences the cut.] + + description [This reference part is similar to Cudd_NodeReclaim(). + The dereference part is similar to Cudd_RecursiveDeref().] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, int fReference ) +{ + Map_Node_t * pNodeChild; + Map_Cut_t * pCutChild; + float aSwitchActivity; + int i, fPhaseChild; + // consider the elementary variable + if ( pCut->nLeaves == 1 ) + return 0; + // start the area of this cut + aSwitchActivity = Map_CutGetSwitching( pCut ); + // go through the children + assert( pCut->M[fPhase].pSuperBest ); + for ( i = 0; i < pCut->nLeaves; i++ ) + { + pNodeChild = pCut->ppLeaves[i]; + fPhaseChild = Map_CutGetLeafPhase( pCut, fPhase, i ); + // get the reference counter of the child + + if ( fReference ) + { + if ( pNodeChild->pCutBest[0] && pNodeChild->pCutBest[1] ) // both phases are present + { + // if this phase of the node is referenced, there is no recursive call + pNodeChild->nRefAct[2]++; + if ( pNodeChild->nRefAct[fPhaseChild]++ > 0 ) + continue; + } + else // only one phase is present + { + // inverter should be added if the phase + // (a) has no reference and (b) is implemented using other phase + if ( pNodeChild->nRefAct[fPhaseChild]++ == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL ) + aSwitchActivity += pNodeChild->Switching; + // if the node is referenced, there is no recursive call + if ( pNodeChild->nRefAct[2]++ > 0 ) + continue; + } + } + else + { + if ( pNodeChild->pCutBest[0] && pNodeChild->pCutBest[1] ) // both phases are present + { + // if this phase of the node is referenced, there is no recursive call + --pNodeChild->nRefAct[2]; + if ( --pNodeChild->nRefAct[fPhaseChild] > 0 ) + continue; + } + else // only one phase is present + { + // inverter should be added if the phase + // (a) has no reference and (b) is implemented using other phase + if ( --pNodeChild->nRefAct[fPhaseChild] == 0 && pNodeChild->pCutBest[fPhaseChild] == NULL ) + aSwitchActivity += pNodeChild->Switching; + // if the node is referenced, there is no recursive call + if ( --pNodeChild->nRefAct[2] > 0 ) + continue; + } + assert( pNodeChild->nRefAct[fPhaseChild] >= 0 ); + } + + // get the child cut + pCutChild = pNodeChild->pCutBest[fPhaseChild]; + // if the child does not have this phase mapped, take the opposite phase + if ( pCutChild == NULL ) + { + fPhaseChild = !fPhaseChild; + pCutChild = pNodeChild->pCutBest[fPhaseChild]; + } + // reference and compute area recursively + aSwitchActivity += Map_SwitchCutRefDeref( pNodeChild, pCutChild, fPhaseChild, fReference ); + } + return aSwitchActivity; +} + +/**function************************************************************* + + synopsis [Computes the exact area associated with the cut.] + + description [] + + sideeffects [] + + seealso [] + +***********************************************************************/ +float Map_CutGetSwitching( Map_Cut_t * pCut ) +{ + float Result; + int i; + Result = 0.0; + for ( i = 0; i < pCut->nLeaves; i++ ) + Result += pCut->ppLeaves[i]->Switching; + return Result; +} + +/**Function************************************************************* + + Synopsis [Computes the array of mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping ) +{ + Map_Node_t * pNode; + float Switch; + int i; + Switch = 0.0; + for ( i = 0; i < vMapping->nSize; i++ ) + { + pNode = vMapping->pArray[i]; + // at least one phase has the best cut assigned + assert( pNode->pCutBest[0] != NULL || pNode->pCutBest[1] != NULL ); + // at least one phase is used in the mapping + assert( pNode->nRefAct[0] > 0 || pNode->nRefAct[1] > 0 ); + // compute the array due to the supergate + if ( Map_NodeIsAnd(pNode) ) + { + // count switching of the negative phase + if ( pNode->pCutBest[0] && (pNode->nRefAct[0] > 0 || pNode->pCutBest[1] == NULL) ) + Switch += pNode->Switching; + // count switching of the positive phase + if ( pNode->pCutBest[1] && (pNode->nRefAct[1] > 0 || pNode->pCutBest[0] == NULL) ) + Switch += pNode->Switching; + } + // count switching of the interver if we need to implement one phase with another phase + if ( (pNode->pCutBest[0] == NULL && pNode->nRefAct[0] > 0) || + (pNode->pCutBest[1] == NULL && pNode->nRefAct[1] > 0) ) + Switch += pNode->Switching; + } + // add buffer for each CO driven by a CI + for ( i = 0; i < pMan->nOutputs; i++ ) + if ( Map_NodeIsVar(pMan->pOutputs[i]) && !Map_IsComplement(pMan->pOutputs[i]) ) + Switch += pMan->pOutputs[i]->Switching; + return Switch; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/mapper/module.make b/src/map/mapper/module.make index 1d3b8867..bd6447d8 100644 --- a/src/map/mapper/module.make +++ b/src/map/mapper/module.make @@ -9,6 +9,7 @@ SRC += src/map/mapper/mapper.c \ src/map/mapper/mapperMatch.c \ src/map/mapper/mapperRefs.c \ src/map/mapper/mapperSuper.c \ + src/map/mapper/mapperSwitch.c \ src/map/mapper/mapperTable.c \ src/map/mapper/mapperTime.c \ src/map/mapper/mapperTree.c \ diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index 3347bba8..f9f4973d 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -90,6 +90,7 @@ extern float Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib ); extern float Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib ); extern float Mio_LibraryReadDelayNand2Max( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ); +extern float Mio_LibraryReadAreaBuf ( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ); extern char * Mio_GateReadName ( Mio_Gate_t * pGate ); extern char * Mio_GateReadOutName ( Mio_Gate_t * pGate ); diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c index 50d60fe9..a39c6288 100644 --- a/src/map/mio/mioApi.c +++ b/src/map/mio/mioApi.c @@ -46,14 +46,15 @@ Mio_Gate_t * Mio_LibraryReadInv ( Mio_Library_t * pLib ) { retur Mio_Gate_t * Mio_LibraryReadConst0 ( Mio_Library_t * pLib ) { return pLib->pGate0; } Mio_Gate_t * Mio_LibraryReadConst1 ( Mio_Library_t * pLib ) { return pLib->pGate1; } Mio_Gate_t * Mio_LibraryReadNand2 ( Mio_Library_t * pLib ) { return pLib->pGateNand2; } -float Mio_LibraryReadDelayInvRise ( Mio_Library_t * pLib ) { return (float)pLib->pGateInv->pPins->dDelayBlockRise; } -float Mio_LibraryReadDelayInvFall ( Mio_Library_t * pLib ) { return (float)pLib->pGateInv->pPins->dDelayBlockFall; } -float Mio_LibraryReadDelayInvMax ( Mio_Library_t * pLib ) { return (float)pLib->pGateInv->pPins->dDelayBlockMax; } -float Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib ) { return (float)pLib->pGateNand2->pPins->dDelayBlockRise; } -float Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib ) { return (float)pLib->pGateNand2->pPins->dDelayBlockFall; } -float Mio_LibraryReadDelayNand2Max ( Mio_Library_t * pLib ) { return (float)pLib->pGateNand2->pPins->dDelayBlockMax; } -float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ) { return (float)pLib->pGateInv->dArea; } -float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ) { return (float)pLib->pGateNand2->dArea; } +float Mio_LibraryReadDelayInvRise ( Mio_Library_t * pLib ) { return (float)(pLib->pGateInv? pLib->pGateInv->pPins->dDelayBlockRise : 0.0); } +float Mio_LibraryReadDelayInvFall ( Mio_Library_t * pLib ) { return (float)(pLib->pGateInv? pLib->pGateInv->pPins->dDelayBlockFall : 0.0); } +float Mio_LibraryReadDelayInvMax ( Mio_Library_t * pLib ) { return (float)(pLib->pGateInv? pLib->pGateInv->pPins->dDelayBlockMax : 0.0); } +float Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockRise : 0.0); } +float Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockFall : 0.0); } +float Mio_LibraryReadDelayNand2Max ( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockMax : 0.0); } +float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ) { return (float)(pLib->pGateInv? pLib->pGateInv->dArea : 0.0); } +float Mio_LibraryReadAreaBuf ( Mio_Library_t * pLib ) { return (float)(pLib->pGateBuf? pLib->pGateBuf->dArea : 0.0); } +float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->dArea : 0.0); } /**Function************************************************************* diff --git a/src/misc/mvc/module.make b/src/misc/mvc/module.make new file mode 100644 index 00000000..23735ca2 --- /dev/null +++ b/src/misc/mvc/module.make @@ -0,0 +1,16 @@ +SRC += src/misc/mvc/mvc.c \ + src/misc/mvc/mvcApi.c \ + src/misc/mvc/mvcCompare.c \ + src/misc/mvc/mvcContain.c \ + src/misc/mvc/mvcCover.c \ + src/misc/mvc/mvcCube.c \ + src/misc/mvc/mvcDivide.c \ + src/misc/mvc/mvcDivisor.c \ + src/misc/mvc/mvcList.c \ + src/misc/mvc/mvcLits.c \ + src/misc/mvc/mvcMan.c \ + src/misc/mvc/mvcOpAlg.c \ + src/misc/mvc/mvcOpBool.c \ + src/misc/mvc/mvcPrint.c \ + src/misc/mvc/mvcSort.c \ + src/misc/mvc/mvcUtils.c diff --git a/src/sop/mvc/mvc.c b/src/misc/mvc/mvc.c index 9430276c..9430276c 100644 --- a/src/sop/mvc/mvc.c +++ b/src/misc/mvc/mvc.c diff --git a/src/sop/mvc/mvc.h b/src/misc/mvc/mvc.h index ee8c31be..ee8c31be 100644 --- a/src/sop/mvc/mvc.h +++ b/src/misc/mvc/mvc.h diff --git a/src/sop/mvc/mvcApi.c b/src/misc/mvc/mvcApi.c index 1f51a235..1f51a235 100644 --- a/src/sop/mvc/mvcApi.c +++ b/src/misc/mvc/mvcApi.c diff --git a/src/sop/mvc/mvcCompare.c b/src/misc/mvc/mvcCompare.c index c7999d40..c7999d40 100644 --- a/src/sop/mvc/mvcCompare.c +++ b/src/misc/mvc/mvcCompare.c diff --git a/src/sop/mvc/mvcContain.c b/src/misc/mvc/mvcContain.c index 37b933b8..37b933b8 100644 --- a/src/sop/mvc/mvcContain.c +++ b/src/misc/mvc/mvcContain.c diff --git a/src/sop/mvc/mvcCover.c b/src/misc/mvc/mvcCover.c index bd9c4412..bd9c4412 100644 --- a/src/sop/mvc/mvcCover.c +++ b/src/misc/mvc/mvcCover.c diff --git a/src/sop/mvc/mvcCube.c b/src/misc/mvc/mvcCube.c index d02fa270..d02fa270 100644 --- a/src/sop/mvc/mvcCube.c +++ b/src/misc/mvc/mvcCube.c diff --git a/src/sop/mvc/mvcDivide.c b/src/misc/mvc/mvcDivide.c index 6aa3d58d..6aa3d58d 100644 --- a/src/sop/mvc/mvcDivide.c +++ b/src/misc/mvc/mvcDivide.c diff --git a/src/sop/mvc/mvcDivisor.c b/src/misc/mvc/mvcDivisor.c index e92c3a65..e92c3a65 100644 --- a/src/sop/mvc/mvcDivisor.c +++ b/src/misc/mvc/mvcDivisor.c diff --git a/src/sop/mvc/mvcList.c b/src/misc/mvc/mvcList.c index 678ae9fd..678ae9fd 100644 --- a/src/sop/mvc/mvcList.c +++ b/src/misc/mvc/mvcList.c diff --git a/src/sop/mvc/mvcLits.c b/src/misc/mvc/mvcLits.c index 98211719..98211719 100644 --- a/src/sop/mvc/mvcLits.c +++ b/src/misc/mvc/mvcLits.c diff --git a/src/sop/mvc/mvcMan.c b/src/misc/mvc/mvcMan.c index f2943e0c..f2943e0c 100644 --- a/src/sop/mvc/mvcMan.c +++ b/src/misc/mvc/mvcMan.c diff --git a/src/sop/mvc/mvcOpAlg.c b/src/misc/mvc/mvcOpAlg.c index befccb70..befccb70 100644 --- a/src/sop/mvc/mvcOpAlg.c +++ b/src/misc/mvc/mvcOpAlg.c diff --git a/src/sop/mvc/mvcOpBool.c b/src/misc/mvc/mvcOpBool.c index 57b1a968..57b1a968 100644 --- a/src/sop/mvc/mvcOpBool.c +++ b/src/misc/mvc/mvcOpBool.c diff --git a/src/sop/mvc/mvcPrint.c b/src/misc/mvc/mvcPrint.c index 3a31235b..3a31235b 100644 --- a/src/sop/mvc/mvcPrint.c +++ b/src/misc/mvc/mvcPrint.c diff --git a/src/sop/mvc/mvcSort.c b/src/misc/mvc/mvcSort.c index 1126b22a..1126b22a 100644 --- a/src/sop/mvc/mvcSort.c +++ b/src/misc/mvc/mvcSort.c diff --git a/src/sop/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c index 3fb57276..3fb57276 100644 --- a/src/sop/mvc/mvcUtils.c +++ b/src/misc/mvc/mvcUtils.c diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 793dd567..7556dd87 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -82,6 +82,26 @@ static inline Vec_Int_t * Vec_IntAlloc( int nCap ) /**Function************************************************************* + Synopsis [Allocates a vector with the given size and cleans it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Vec_IntStart( int nSize ) +{ + Vec_Int_t * p; + p = Vec_IntAlloc( nSize ); + p->nSize = nSize; + memset( p->pArray, 0, sizeof(int) * nSize ); + return p; +} + +/**Function************************************************************* + Synopsis [Creates the vector from an integer array of the given size.] Description [] @@ -437,6 +457,27 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + return 1; + Vec_IntPush( p, Entry ); + return 0; +} + +/**Function************************************************************* + Synopsis [Returns the last entry and removes it from the list.] Description [] diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 1d3e0633..b1776441 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -53,6 +53,8 @@ struct Vec_Ptr_t_ for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ ) #define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start ) \ for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ ) +#define Vec_PtrForEachEntryReverse( vVec, pEntry, i ) \ + for ( i = Vec_PtrSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i-- ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -83,6 +85,26 @@ static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap ) /**Function************************************************************* + Synopsis [Allocates a vector with the given size and cleans it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Ptr_t * Vec_PtrStart( int nSize ) +{ + Vec_Ptr_t * p; + p = Vec_PtrAlloc( nSize ); + p->nSize = nSize; + memset( p->pArray, 0, sizeof(void *) * nSize ); + return p; +} + +/**Function************************************************************* + Synopsis [Creates the vector from an integer array of the given size.] Description [] @@ -488,46 +510,6 @@ static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems ) /**Function************************************************************* - Synopsis [Frees the vector of vectors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_PtrFreeFree( Vec_Ptr_t * p ) -{ - Vec_Ptr_t * vVec; - int i; - Vec_PtrForEachEntry( p, vVec, i ) - Vec_PtrFree( vVec ); - Vec_PtrFree( p ); -} - -/**Function************************************************************* - - Synopsis [Frees the vector of vectors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_PtrSizeSize( Vec_Ptr_t * p ) -{ - Vec_Ptr_t * vVec; - int i, Counter = 0; - Vec_PtrForEachEntry( p, vVec, i ) - Counter += vVec->nSize; - return Counter; -} - -/**Function************************************************************* - Synopsis [Sorting the entries by their integer value.] Description [] diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 4b8e6a1c..311bda91 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -80,6 +80,26 @@ static inline Vec_Str_t * Vec_StrAlloc( int nCap ) /**Function************************************************************* + Synopsis [Allocates a vector with the given size and cleans it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Str_t * Vec_StrStart( int nSize ) +{ + Vec_Str_t * p; + p = Vec_StrAlloc( nSize ); + p->nSize = nSize; + memset( p->pArray, 0, sizeof(char) * nSize ); + return p; +} + +/**Function************************************************************* + Synopsis [Creates the vector from an integer array of the given size.] Description [] diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index af7ca571..0ad5fd1e 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -68,6 +68,9 @@ struct Vec_Vec_t_ #define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop ) \ for ( i = LevelStart; i <= LevelStop; i++ ) \ Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) +#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k ) \ + for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \ + Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make new file mode 100644 index 00000000..43d0a125 --- /dev/null +++ b/src/opt/sim/module.make @@ -0,0 +1,9 @@ +SRC += src/opt/sim/simMan.c \ + src/opt/sim/simSat.c \ + src/opt/sim/simSupp.c \ + src/opt/sim/simSwitch.c \ + src/opt/sim/simSym.c \ + src/opt/sim/simSymSat.c \ + src/opt/sim/simSymSim.c \ + src/opt/sim/simSymStr.c \ + src/opt/sim/simUtils.c diff --git a/src/sat/sim/sim.h b/src/opt/sim/sim.h index 7c4c50e3..9b4d9699 100644 --- a/src/sat/sim/sim.h +++ b/src/opt/sim/sim.h @@ -33,11 +33,52 @@ /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// +typedef struct Sym_Man_t_ Sym_Man_t; +struct Sym_Man_t_ +{ + // info about the network + Abc_Ntk_t * pNtk; // the network + Vec_Ptr_t * vNodes; // internal nodes in topological order + int nInputs; + int nOutputs; + // internal simulation information + int nSimWords; // the number of bits in simulation info + Vec_Ptr_t * vSim; // simulation info + // support information + Vec_Ptr_t * vSuppFun; // functional supports + // symmetry info for each output + Vec_Ptr_t * vMatrSymms; // symmetric pairs + Vec_Ptr_t * vMatrNonSymms; // non-symmetric pairs + Vec_Int_t * vPairsTotal; // total pairs + Vec_Int_t * vPairsSym; // symmetric pairs + Vec_Int_t * vPairsNonSym; // non-symmetric pairs + // temporary simulation info + unsigned * uPatRand; + unsigned * uPatCol; + unsigned * uPatRow; + // internal data structures + int nSatRuns; + int nSatRunsSat; + int nSatRunsUnsat; + // pairs + int nPairsSymm; + int nPairsSymmStr; + int nPairsNonSymm; + int nPairsTotal; + // runtime statistics + int timeSim; + int timeFraig; + int timeSat; + int timeTotal; +}; + typedef struct Sim_Man_t_ Sim_Man_t; struct Sim_Man_t_ { - // user specified parameters + // info about the network Abc_Ntk_t * pNtk; + int nInputs; + int nOutputs; // internal simulation information int nSimBits; // the number of bits in simulation info int nSimWords; // the number of words in simulation info @@ -48,25 +89,21 @@ struct Sim_Man_t_ int nSuppWords; // the number of words in support info Vec_Ptr_t * vSuppStr; // structural supports Vec_Ptr_t * vSuppFun; // functional supports - // unateness info - Vec_Ptr_t * vUnateVarsP; // unate variables - Vec_Ptr_t * vUnateVarsN; // unate variables - // symmtry info - Extra_BitMat_t * pMatSym; // symmetric pairs - Extra_BitMat_t * pMatNonSym; // non-symmetric pairs // simulation targets - Vec_Ptr_t * vSuppTargs; // support targets - Vec_Ptr_t * vUnateTargs; // unateness targets - Vec_Ptr_t * vSymmTargs; // symmetry targets + Vec_Vec_t * vSuppTargs; // support targets // internal data structures Extra_MmFixed_t * pMmPat; Vec_Ptr_t * vFifo; Vec_Int_t * vDiffs; + int nSatRuns; + int nSatRunsSat; + int nSatRunsUnsat; // runtime statistics - int time1; - int time2; - int time3; - int time4; + int timeSim; + int timeTrav; + int timeFraig; + int timeSat; + int timeTotal; }; typedef struct Sim_Pat_t_ Sim_Pat_t; @@ -84,6 +121,12 @@ struct Sim_Pat_t_ #define SIM_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0)) #define SIM_LAST_BITS(n) ((((n)%32) > 0)? (n)%32 : 32) +#define SIM_MASK_FULL (0xFFFFFFFF) +#define SIM_MASK_BEG(n) (SIM_MASK_FULL >> (32-n)) +#define SIM_MASK_END(n) (SIM_MASK_FULL << (n)) +#define SIM_SET_0_FROM(m,n) ((m) & ~SIM_MASK_BEG(n)) +#define SIM_SET_1_FROM(m,n) ((m) | SIM_MASK_END(n)) + // generating random unsigned (#define RAND_MAX 0x7fff) #define SIM_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())) @@ -93,40 +136,51 @@ struct Sim_Pat_t_ #define Sim_HasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0) // macros to get hold of the support info -#define Sim_SuppStrSetVar(pMan,pNode,v) Sim_SetBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v)) -#define Sim_SuppStrHasVar(pMan,pNode,v) Sim_HasBit((unsigned*)pMan->vSuppStr->pArray[(pNode)->Id],(v)) -#define Sim_SuppFunSetVar(pMan,Output,v) Sim_SetBit((unsigned*)pMan->vSuppFun->pArray[Output],(v)) -#define Sim_SuppFunHasVar(pMan,Output,v) Sim_HasBit((unsigned*)pMan->vSuppFun->pArray[Output],(v)) -#define Sim_SimInfoSetVar(pMan,pNode,v) Sim_SetBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v)) -#define Sim_SimInfoHasVar(pMan,pNode,v) Sim_HasBit((unsigned*)pMan->vSim0->pArray[(pNode)->Id],(v)) +#define Sim_SuppStrSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SuppStrHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SuppFunSetVar(vSupps,Output,v) Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v)) +#define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v)) +#define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== simMan.c ==========================================================*/ +extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ); +extern void Sym_ManStop( Sym_Man_t * p ); +extern void Sym_ManPrintStats( Sym_Man_t * p ); extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ); extern void Sim_ManStop( Sim_Man_t * p ); +extern void Sim_ManPrintStats( Sim_Man_t * p ); extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ); extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ); -extern void Sim_ManPrintStats( Sim_Man_t * p ); - /*=== simSupp.c ==========================================================*/ -extern Sim_Man_t * Sim_ComputeSupp( Abc_Ntk_t * pNtk ); - +extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ); +extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ); +/*=== simSym.c ==========================================================*/ +extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ); +/*=== simSymStr.c ==========================================================*/ +extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ); +/*=== simSymSim.c ==========================================================*/ +extern void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym ); /*=== simUtil.c ==========================================================*/ extern Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean ); extern void Sim_UtilInfoFree( Vec_Ptr_t * p ); extern void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords ); extern void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ); extern void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs ); -extern void Sim_UtilComputeStrSupp( Sim_Man_t * p ); -extern void Sim_UtilAssignRandom( Sim_Man_t * p ); -extern void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode ); -extern bool Sim_UtilCompareSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode ); +extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ); +extern bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ); extern void Sim_UtilSimulate( Sim_Man_t * p, bool fFirst ); extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 ); +extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ); +extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ); +extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ); +extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ); +extern int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/sim/simMan.c b/src/opt/sim/simMan.c index 1dd4053c..02d59343 100644 --- a/src/sat/sim/simMan.c +++ b/src/opt/sim/simMan.c @@ -40,14 +40,126 @@ SeeAlso [] ***********************************************************************/ +Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk ) +{ + Sym_Man_t * p; + int i; + // start the manager + p = ALLOC( Sym_Man_t, 1 ); + memset( p, 0, sizeof(Sym_Man_t) ); + p->pNtk = pNtk; + p->vNodes = Abc_NtkDfs( pNtk, 0 ); + p->nInputs = Abc_NtkCiNum(p->pNtk); + p->nOutputs = Abc_NtkCoNum(p->pNtk); + // internal simulation information + p->nSimWords = SIM_NUM_WORDS(p->nInputs); + p->vSim = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); + // symmetry info for each output + p->vMatrSymms = Vec_PtrStart( p->nOutputs ); + p->vMatrNonSymms = Vec_PtrStart( p->nOutputs ); + p->vPairsTotal = Vec_IntStart( p->nOutputs ); + p->vPairsSym = Vec_IntStart( p->nOutputs ); + p->vPairsNonSym = Vec_IntStart( p->nOutputs ); + for ( i = 0; i < p->nOutputs; i++ ) + { + p->vMatrSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs ); + p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs ); + } + // temporary patterns + p->uPatRand = ALLOC( unsigned, p->nSimWords ); + p->uPatCol = ALLOC( unsigned, p->nSimWords ); + p->uPatRow = ALLOC( unsigned, p->nSimWords ); + // compute supports + p->vSuppFun = Sim_ComputeFunSupp( pNtk ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sym_ManStop( Sym_Man_t * p ) +{ + int i; + Sym_ManPrintStats( p ); + if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); + if ( p->vSim ) Sim_UtilInfoFree( p->vSim ); + if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + for ( i = 0; i < p->nOutputs; i++ ) + { + Extra_BitMatrixStop( p->vMatrSymms->pArray[i] ); + Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] ); + } + Vec_PtrFree( p->vMatrSymms ); + Vec_PtrFree( p->vMatrNonSymms ); + Vec_IntFree( p->vPairsTotal ); + Vec_IntFree( p->vPairsSym ); + Vec_IntFree( p->vPairsNonSym ); + FREE( p->uPatRand ); + FREE( p->uPatCol ); + FREE( p->uPatRow ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prints the manager statisticis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sym_ManPrintStats( Sym_Man_t * p ) +{ + printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", + Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); +/* + printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); + printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); + printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); +*/ + printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); + PRT( "Simulation ", p->timeSim ); + PRT( "Fraiging ", p->timeFraig ); + PRT( "SAT ", p->timeSat ); + PRT( "TOTAL ", p->timeTotal ); +} + + + + +/**Function************************************************************* + + Synopsis [Starts the simulatin manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ) { Sim_Man_t * p; - int i; // start the manager p = ALLOC( Sim_Man_t, 1 ); memset( p, 0, sizeof(Sim_Man_t) ); p->pNtk = pNtk; + p->nInputs = Abc_NtkCiNum(p->pNtk); + p->nOutputs = Abc_NtkCoNum(p->pNtk); // internal simulation information p->nSimBits = 2048; p->nSimWords = SIM_NUM_WORDS(p->nSimBits); @@ -56,17 +168,14 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ) // support information p->nSuppBits = Abc_NtkCiNum(pNtk); p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits); - p->vSuppStr = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSuppWords, 1 ); + p->vSuppStr = Sim_ComputeStrSupp( pNtk ); p->vSuppFun = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk), p->nSuppWords, 1 ); // other data p->pMmPat = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); p->vFifo = Vec_PtrAlloc( 100 ); p->vDiffs = Vec_IntAlloc( 100 ); - // allocate support targets - p->vSuppTargs = Vec_PtrAlloc( p->nSuppBits ); - p->vSuppTargs->nSize = p->nSuppBits; - for ( i = 0; i < p->nSuppBits; i++ ) - p->vSuppTargs->pArray[i] = Vec_IntAlloc( 8 ); + // allocate support targets (array of unresolved outputs for each input) + p->vSuppTargs = Vec_VecStart( p->nInputs ); return p; } @@ -87,14 +196,8 @@ void Sim_ManStop( Sim_Man_t * p ) if ( p->vSim0 ) Sim_UtilInfoFree( p->vSim0 ); if ( p->vSim1 ) Sim_UtilInfoFree( p->vSim1 ); if ( p->vSuppStr ) Sim_UtilInfoFree( p->vSuppStr ); - if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); - if ( p->vUnateVarsP ) Sim_UtilInfoFree( p->vUnateVarsP ); - if ( p->vUnateVarsN ) Sim_UtilInfoFree( p->vUnateVarsN ); - if ( p->pMatSym ) Extra_BitMatrixStop( p->pMatSym ); - if ( p->pMatNonSym ) Extra_BitMatrixStop( p->pMatNonSym ); - if ( p->vSuppTargs ) Vec_PtrFreeFree( p->vSuppTargs ); - if ( p->vUnateTargs ) Vec_PtrFree( p->vUnateTargs ); - if ( p->vSymmTargs ) Vec_PtrFree( p->vSymmTargs ); +// if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); + if ( p->vSuppTargs ) Vec_VecFree( p->vSuppTargs ); if ( p->pMmPat ) Extra_MmFixedStop( p->pMmPat, 0 ); if ( p->vFifo ) Vec_PtrFree( p->vFifo ); if ( p->vDiffs ) Vec_IntFree( p->vDiffs ); @@ -103,7 +206,7 @@ void Sim_ManStop( Sim_Man_t * p ) /**Function************************************************************* - Synopsis [Returns one simulation pattern.] + Synopsis [Prints the manager statisticis.] Description [] @@ -112,16 +215,25 @@ void Sim_ManStop( Sim_Man_t * p ) SeeAlso [] ***********************************************************************/ -Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ) +void Sim_ManPrintStats( Sim_Man_t * p ) { - Sim_Pat_t * pPat; - pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat ); - pPat->Output = -1; - pPat->pData = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t)); - memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) ); - return pPat; + printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", + Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); + printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); + printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); + printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); + printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat ); + printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat ); + PRT( "Simulation ", p->timeSim ); + PRT( "Traversal ", p->timeTrav ); + PRT( "Fraiging ", p->timeFraig ); + PRT( "SAT ", p->timeSat ); + PRT( "TOTAL ", p->timeTotal ); } + + /**Function************************************************************* Synopsis [Returns one simulation pattern.] @@ -133,14 +245,19 @@ Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ) +Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ) { - Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat ); + Sim_Pat_t * pPat; + pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat ); + pPat->Output = -1; + pPat->pData = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t)); + memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) ); + return pPat; } /**Function************************************************************* - Synopsis [Prints the manager statisticis.] + Synopsis [Returns one simulation pattern.] Description [] @@ -149,14 +266,9 @@ void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ) SeeAlso [] ***********************************************************************/ -void Sim_ManPrintStats( Sim_Man_t * p ) +void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ) { - printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", - Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords ); - printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) ); - printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) ); - printf( "Total targets = %6d.\n", Vec_PtrSizeSize(p->vSuppTargs) ); - printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) ); + Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/sim/simSat.c b/src/opt/sim/simSat.c index b4e080fe..b4e080fe 100644 --- a/src/sat/sim/simSat.c +++ b/src/opt/sim/simSat.c diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c new file mode 100644 index 00000000..2f380866 --- /dev/null +++ b/src/opt/sim/simSupp.c @@ -0,0 +1,594 @@ +/**CFile**************************************************************** + + FileName [simSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine functional support.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ); +static int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ); +static void Sim_ComputeSuppSetTargets( Sim_Man_t * p ); + +static void Sim_UtilAssignRandom( Sim_Man_t * p ); +static void Sim_UtilAssignFromFifo( Sim_Man_t * p ); +static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters ); +static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ); + +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes structural supports.] + + Description [Supports are returned as an array of bit strings, one + for each CO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vSuppStr; + Abc_Obj_t * pNode; + unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; + int nSuppWords, i, k; + // allocate room for structural supports + nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) ); + vSuppStr = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 ); + // assign the structural support to the PIs + Abc_NtkForEachCi( pNtk, pNode, i ) + Sim_SuppStrSetVar( vSuppStr, pNode, i ); + // derive the structural supports of the internal nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + pSimmNode = vSuppStr->pArray[ pNode->Id ]; + pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; + pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ]; + for ( k = 0; k < nSuppWords; k++ ) + pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k]; + } + // set the structural supports of the PO nodes + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pSimmNode = vSuppStr->pArray[ pNode->Id ]; + pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; + for ( k = 0; k < nSuppWords; k++ ) + pSimmNode[k] = pSimmNode1[k]; + } + return vSuppStr; +} + +/**Function************************************************************* + + Synopsis [Compute functional supports.] + + Description [Supports are returned as an array of bit strings, one + for each CO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk ) +{ + Sim_Man_t * p; + Vec_Ptr_t * vResult; + int nSolved, i, clk = clock(); + +// srand( time(NULL) ); + srand( 0xABC ); + + // start the simulation manager + p = Sim_ManStart( pNtk ); + + // compute functional support using one round of random simulation + Sim_UtilAssignRandom( p ); + Sim_ComputeSuppRound( p, 0 ); + + // set the support targets + Sim_ComputeSuppSetTargets( p ); +printf( "Initial targets = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) ); + if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) + goto exit; + + for ( i = 0; i < 1; i++ ) + { + // compute patterns using one round of random simulation + Sim_UtilAssignRandom( p ); + nSolved = Sim_ComputeSuppRound( p, 1 ); +printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) ); + if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) + goto exit; + } + + + // simulate until saturation + while ( Vec_VecSizeSize(p->vSuppTargs) > 0 ) + { + // solve randomly a given number of targets + Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords ); + // compute additional functional support +// Sim_UtilAssignRandom( p ); + Sim_UtilAssignFromFifo( p ); + nSolved = Sim_ComputeSuppRound( p, 1 ); +printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n", + Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns ); + } + +exit: + vResult = p->vSuppFun; + // p->vSuppFun = NULL; + Sim_ManStop( p ); + return vResult; +} + +/**Function************************************************************* + + Synopsis [Computes functional support using one round of simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ) +{ + Vec_Int_t * vTargets; + Abc_Obj_t * pNode; + int i, Counter = 0; + int clk; + // perform one round of random simulation +clk = clock(); + Sim_UtilSimulate( p, 0 ); +p->timeSim += clock() - clk; + // iterate through the CIs and detect COs that depend on them + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + vTargets = p->vSuppTargs->pArray[i]; + if ( fUseTargets && vTargets->nSize == 0 ) + continue; + Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Computes functional support for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) +{ + int fVerbose = 0; + Sim_Pat_t * pPat; + Vec_Int_t * vTargets; + Vec_Vec_t * vNodesByLevel; + Abc_Obj_t * pNodeCi, * pNode; + int i, k, v, Output, LuckyPat, fType0, fType1; + int Counter = 0; + int fFirst = 1; + int clk; + // collect nodes by level in the TFO of the CI + // (this procedure increments TravId of the collected nodes) +clk = clock(); + pNodeCi = Abc_NtkCi( p->pNtk, iNumCi ); + vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 ); +p->timeTrav += clock() - clk; + // complement the simulation info of the selected CI + Sim_UtilInfoFlip( p, pNodeCi ); + // simulate the levelized structure of nodes + Vec_VecForEachEntry( vNodesByLevel, pNode, i, k ) + { + fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) ); + fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) ); +clk = clock(); + Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 ); +p->timeSim += clock() - clk; + } + // set the simulation info of the affected COs + if ( fUseTargets ) + { + vTargets = p->vSuppTargs->pArray[iNumCi]; + for ( i = vTargets->nSize - 1; i >= 0; i-- ) + { + // get the target output + Output = vTargets->pArray[i]; + // get the target node + pNode = Abc_NtkCo( p->pNtk, Output ); + // the output should be in the cone + assert( Abc_NodeIsTravIdCurrent(pNode) ); + + // simulate the node + Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); + + // skip if the simulation info is equal + if ( Sim_UtilInfoCompare( p, pNode ) ) + continue; + + // otherwise, we solved a new target + Vec_IntRemove( vTargets, Output ); +if ( fVerbose ) + printf( "(%d,%d) ", iNumCi, Output ); + Counter++; + // make sure this variable is not yet detected + assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ); + // set this variable + Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + + // detect the differences in the simulation info + Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs ); + // create new patterns + if ( !fFirst && p->vFifo->nSize > 1000 ) + continue; + + Vec_IntForEachEntry( p->vDiffs, LuckyPat, k ) + { + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = iNumCi; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) ) + Sim_SetBit( pPat->pData, v ); + Vec_PtrPush( p->vFifo, pPat ); + + fFirst = 0; + break; + } + } +if ( fVerbose && Counter ) +printf( "\n" ); + } + else + { + Abc_NtkForEachCo( p->pNtk, pNode, Output ) + { + if ( !Abc_NodeIsTravIdCurrent( pNode ) ) + continue; + Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); + if ( !Sim_UtilInfoCompare( p, pNode ) ) + { + if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ) + Counter++; + Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); + } + } + } + Vec_VecFree( vNodesByLevel ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Sets the simulation targets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_ComputeSuppSetTargets( Sim_Man_t * p ) +{ + Abc_Obj_t * pNode; + unsigned * pSuppStr, * pSuppFun; + int i, k, Num; + Abc_NtkForEachCo( p->pNtk, pNode, i ) + { + pSuppStr = p->vSuppStr->pArray[pNode->Id]; + pSuppFun = p->vSuppFun->pArray[i]; + // find vars in the structural support that are not in the functional support + Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs ); + Vec_IntForEachEntry( p->vDiffs, Num, k ) + Vec_VecPush( p->vSuppTargs, Num, (void *)i ); + } +} + +/**Function************************************************************* + + Synopsis [Assigns random simulation info to the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilAssignRandom( Sim_Man_t * p ) +{ + Abc_Obj_t * pNode; + unsigned * pSimInfo; + int i, k; + // assign the random/systematic simulation info to the PIs + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = p->vSim0->pArray[pNode->Id]; + for ( k = 0; k < p->nSimWords; k++ ) + pSimInfo[k] = SIM_RANDOM_UNSIGNED; + } +} + +/**Function************************************************************* + + Synopsis [Sets the new patterns from fifo.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilAssignFromFifo( Sim_Man_t * p ) +{ + int fUseOneWord = 0; + Abc_Obj_t * pNode; + Sim_Pat_t * pPat; + unsigned * pSimInfo; + int iWord, iWordLim, i, w; + int iBeg, iEnd; + int Counter = 0; + // go through the patterns and fill in the dist-1 minterms for each + for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim ) + { + ++Counter; + // get the pattern + pPat = Vec_PtrPop( p->vFifo ); + if ( fUseOneWord ) + { + // get the first word of the next series + iWordLim = iWord + 1; + // set the pattern for all PIs from iBit to iWord + p->nInputs + iBeg = ABC_MAX( 0, pPat->Input - 16 ); + iEnd = ABC_MIN( iBeg + 32, p->nInputs ); +// for ( i = iBeg; i < iEnd; i++ ) + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pNode = Abc_NtkCi(p->pNtk,i); + pSimInfo = p->vSim0->pArray[pNode->Id]; + if ( Sim_HasBit(pPat->pData, i) ) + pSimInfo[iWord] = SIM_MASK_FULL; + else + pSimInfo[iWord] = 0; + // flip one bit + if ( i >= iBeg && i < iEnd ) + Sim_XorBit( pSimInfo + iWord, i-iBeg ); + } + } + else + { + // get the first word of the next series + iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; + // set the pattern for all PIs from iBit to iWord + p->nInputs + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = p->vSim0->pArray[pNode->Id]; + if ( Sim_HasBit(pPat->pData, i) ) + { + for ( w = iWord; w < iWordLim; w++ ) + pSimInfo[w] = SIM_MASK_FULL; + } + else + { + for ( w = iWord; w < iWordLim; w++ ) + pSimInfo[w] = 0; + } + // flip one bit + Sim_XorBit( pSimInfo + iWord, i ); + } + } + Sim_ManPatFree( p, pPat ); + // stop if we ran out of room for patterns + if ( iWordLim == p->nSimWords ) + break; +// if ( Counter == 1 ) +// break; + } +} + +/**Function************************************************************* + + Synopsis [Get the given number of counter-examples using SAT.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) +{ + Fraig_Params_t Params; + Fraig_Man_t * pMan; + Abc_Obj_t * pNodeCi; + Abc_Ntk_t * pMiter; + Sim_Pat_t * pPat; + void * pEntry; + int * pModel; + int RetValue, Output, Input, k, v; + int Counter = 0; + int clk; + + p->nSatRuns = 0; + // put targets into one array + Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k ) + { + p->nSatRuns++; + Output = (int)pEntry; + // set up the miter for the two cofactors of this output w.r.t. this input + pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 ); + + // transform the target into a fraig + Fraig_ParamsSetDefault( &Params ); + Params.fInternal = 1; +clk = clock(); + pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); +p->timeFraig += clock() - clk; +clk = clock(); + Fraig_ManProveMiter( pMan ); +p->timeSat += clock() - clk; + + // analyze the result + RetValue = Fraig_ManCheckMiter( pMan ); + assert( RetValue >= 0 ); + if ( RetValue == 1 ) // unsat + { + p->nSatRunsUnsat++; + pModel = NULL; + Vec_PtrRemove( p->vSuppTargs->pArray[Input], pEntry ); + } + else // sat + { + p->nSatRunsSat++; + pModel = Fraig_ManReadModel( pMan ); + assert( pModel != NULL ); + assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) ); + +//printf( "Solved by SAT (%d,%d).\n", Input, Output ); + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = Input; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( pModel[v] ) + Sim_SetBit( pPat->pData, v ); + Vec_PtrPush( p->vFifo, pPat ); +/* + // set the new pattern + pPat = Sim_ManPatAlloc( p ); + pPat->Input = Input; + pPat->Output = Output; + Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) + if ( pModel[v] ) + Sim_SetBit( pPat->pData, v ); + Sim_XorBit( pPat->pData, Input ); // flip the given bit + Vec_PtrPush( p->vFifo, pPat ); +*/ + Counter++; + } + // delete the fraig manager + Fraig_ManFree( pMan ); + // delete the target + Abc_NtkDelete( pMiter ); + + // stop when we found enough patterns +// if ( Counter == Limit ) + if ( Counter == 1 ) + return; + // switch to the next input if we found one model + if ( pModel ) + break; + } +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode ) +{ + int Value0, Value1; + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return (int)pNode->pCopy; + Abc_NodeSetTravIdCurrent( pNode ); + Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) ); + Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) ); + if ( Abc_ObjFaninC0(pNode) ) + Value0 = ~Value0; + if ( Abc_ObjFaninC1(pNode) ) + Value1 = ~Value1; + pNode->pCopy = (Abc_Obj_t *)(Value0 & Value1); + return Value0 & Value1; +} + +/**Function************************************************************* + + Synopsis [Verifies that pModel proves the presence of Input in the support of Output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ) +{ + Abc_Obj_t * pNode; + int RetValue, i; + // set the PI values + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + { + Abc_NodeSetTravIdCurrent( pNode ); + if ( pNode == Abc_NtkCi(pNtk,Input) ) + pNode->pCopy = (Abc_Obj_t *)1; + else if ( pModel[i] == 1 ) + pNode->pCopy = (Abc_Obj_t *)3; + else + pNode->pCopy = NULL; + } + // perform the traversal + RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) ); + if ( RetValue == 0 || RetValue == 3 ) + { + int x = 0; + } +// assert( RetValue == 1 || RetValue == 2 ); + return RetValue == 1 || RetValue == 2; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c new file mode 100644 index 00000000..06b730fc --- /dev/null +++ b/src/opt/sim/simSwitch.c @@ -0,0 +1,107 @@ +/**CFile**************************************************************** + + FileName [simSwitch.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Computes switching activity of nodes in the ABC network.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); +static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes switching activity using simulation.] + + Description [Computes switching activity, which is understood as the + probability of switching under random simulation. Assigns the + random simulation information at the CI and propagates it through + the internal nodes of the AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) +{ + Vec_Int_t * vSwitching; + float * pSwitching; + Vec_Ptr_t * vNodes; + Vec_Ptr_t * vSimInfo; + Abc_Obj_t * pNode; + unsigned * pSimInfo; + int nSimWords, i; + + // allocate space for simulation info of all nodes + nSimWords = SIM_NUM_WORDS(nPatterns); + vSimInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSimWords, 0 ); + // assign the random simulation to the CIs + vSwitching = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); + pSwitching = (float *)vSwitching->pArray; + Abc_NtkForEachCi( pNtk, pNode, i ) + { + pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); + Sim_UtilGetRandom( pSimInfo, nSimWords ); + pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); + } + // simulate the internal nodes + vNodes = Abc_AigDfs( pNtk, 1, 0 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); + pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); + pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); + } + Vec_PtrFree( vNodes ); + Sim_UtilInfoFree( vSimInfo ); + return vSwitching; +} + +/**Function************************************************************* + + Synopsis [Computes switching activity of one node.] + + Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords ) +{ + int nOnes, nTotal; + nTotal = 32 * nSimWords; + nOnes = Sim_UtilCountOnes( pSimInfo, nSimWords ); + return (float)2.0 * nOnes * (nTotal - nOnes) / nTotal / nTotal; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c new file mode 100644 index 00000000..706b13dc --- /dev/null +++ b/src/opt/sim/simSym.c @@ -0,0 +1,93 @@ +/**CFile**************************************************************** + + FileName [simSym.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine two-variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes two variable symmetries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk ) +{ + Sym_Man_t * p; + Vec_Ptr_t * vResult; + int Result; + int i, clk = clock(); + +// srand( time(NULL) ); + srand( 0xABC ); + + // start the simulation manager + p = Sym_ManStart( pNtk ); + p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal ); + + // detect symmetries using circuit structure + Sim_SymmsStructCompute( pNtk, p->vMatrSymms ); + p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); + +printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + + // detect symmetries using simulation + for ( i = 1; i <= 1000; i++ ) + { + // generate random pattern + Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); + // simulate this pattern + Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); + if ( i % 100 != 0 ) + continue; + // count the number of pairs + p->nPairsSymm = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym ); + p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym ); + +printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n", + p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm ); + } + + Result = p->nPairsSymm; + vResult = p->vMatrSymms; + // p->vMatrSymms = NULL; + Sym_ManStop( p ); + return Result; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c new file mode 100644 index 00000000..88e33161 --- /dev/null +++ b/src/opt/sim/simSymSat.c @@ -0,0 +1,202 @@ +/**CFile**************************************************************** + + FileName [simSymSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Satisfiability to determine two variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ); +static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs the SAT based check.] + + Description [Given two bit matrices, with symm info and non-symm info, + checks the remaining pairs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym ) +{ + int VarsU[512], VarsV[512]; + int nVarsU, nVarsV; + int v, u, i, k; + int Counter = 0; + int satCalled = 0; + int satProved = 0; + double Density; + int clk = clock(); + + extern int symsSat; + extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); + + + // count undecided pairs + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) + continue; + Counter++; + } + // compute the density of 1's in the input space of the functions + Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32; + + printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", + p->vInputs->nSize, Counter, Density ); + + + // go through the remaining variable pairs + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) ) + continue; + symsSat++; + satCalled++; + + // collect the variables that are symmetric with each + nVarsU = nVarsV = 0; + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + if ( Extra_BitMatrixLookup1( pMatSym, u, i ) ) + VarsU[nVarsU++] = i; + if ( Extra_BitMatrixLookup1( pMatSym, v, i ) ) + VarsV[nVarsV++] = i; + } + + if ( Fraig_SymmsSatProveOne( p, v, u ) ) + { // update the symmetric variable info +//printf( "%d sym %d\n", v, u ); + for ( i = 0; i < nVarsU; i++ ) + for ( k = 0; k < nVarsV; k++ ) + { + Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 + Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1 + Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 2 + } + satProved++; + } + else + { // update the assymmetric variable info +//printf( "%d non-sym %d\n", v, u ); + for ( i = 0; i < nVarsU; i++ ) + for ( k = 0; k < nVarsV; k++ ) + { + Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 + Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3 + } + } +//Extra_BitMatrixPrint( pMatSym ); +//Extra_BitMatrixPrint( pMatNonSym ); + } +printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved ); +PRT( "Time", clock() - clk ); + + // make sure that the symmetry matrix contains only cliques + assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the variables are symmetric; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 ) +{ + Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2; + int RetValue; + int nSatRuns = p->nSatCalls; + int nSatProof = p->nSatProof; + + p->nBTLimit = 10; // set the backtrack limit + + pVar1 = p->vInputs->pArray[Var1]; + pVar2 = p->vInputs->pArray[Var2]; + pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) ); + pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 ); + +//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof ); + +// RetValue = (pCof01 == pCof10); +// RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 ); + RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [A sanity check procedure.] + + Description [Makes sure that the symmetry information in the matrix + is closed w.r.t. the relationship of transitivity (that is the symmetry + graph is composed of cliques).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat ) +{ + int v, u, i; + for ( v = 0; v < p->vInputs->nSize; v++ ) + for ( u = v+1; u < p->vInputs->nSize; u++ ) + { + if ( !Extra_BitMatrixLookup1( pMat, v, u ) ) + continue; + // v and u are symmetric + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + if ( i == v || i == u ) + continue; + // i is neither v nor u + // the symmetry status of i is the same w.r.t. to v and u + if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) ) + return 0; + } + } + return 1; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c new file mode 100644 index 00000000..53fc4ac2 --- /dev/null +++ b/src/opt/sim/simSymSim.c @@ -0,0 +1,159 @@ +/**CFile**************************************************************** + + FileName [simSymSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation to determine two-variable symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ); +static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detects non-symmetric pairs using one pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym ) +{ + Abc_Obj_t * pNode; + int i; + // create the simulation matrix + Sim_SymmsCreateSquare( p, pPat ); + // simulate each node in the DFS order + Vec_PtrForEachEntry( p->vNodes, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords ); + } + // collect info into the CO matrices + Abc_NtkForEachCo( p->pNtk, pNode, i ) + { + pNode = Abc_ObjFanin0(pNode); + if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) ) + continue; + if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) ) + continue; + Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i ); + } +} + +/**Function************************************************************* + + Synopsis [Creates the square matrix of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ) +{ + unsigned * pSimInfo; + Abc_Obj_t * pNode; + int i, w; + // for each PI var copy the pattern + Abc_NtkForEachCi( p->pNtk, pNode, i ) + { + pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id ); + if ( Sim_HasBit(pPat, i) ) + { + for ( w = 0; w < p->nSimWords; w++ ) + pSimInfo[w] = SIM_MASK_FULL; + } + else + { + for ( w = 0; w < p->nSimWords; w++ ) + pSimInfo[w] = 0; + } + // flip one bit + Sim_XorBit( pSimInfo, i ); + } +} + +/**Function************************************************************* + + Synopsis [Transfers the info to the POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output ) +{ + unsigned * pSuppInfo; + unsigned * pSimInfo; + int i, w; + // get the simuation info for the node + pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id ); + pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output ); + // generate vectors A1 and A2 + for ( w = 0; w < p->nSimWords; w++ ) + { + p->uPatCol[w] = pSuppInfo[w] & pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w]; + } + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatCol, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatRow ); + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatRow, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatCol ); + // generate vectors B1 and B2 + for ( w = 0; w < p->nSimWords; w++ ) + { + p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] & pSimInfo[w]; + p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w]; + } + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatCol, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatRow ); + // add two dimensions + for ( i = 0; i < p->nInputs; i++ ) + if ( Sim_HasBit( p->uPatRow, i ) ) + Extra_BitMatrixOr( pMat, i, p->uPatCol ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c new file mode 100644 index 00000000..c3059d84 --- /dev/null +++ b/src/opt/sim/simSymStr.c @@ -0,0 +1,481 @@ +/**CFile**************************************************************** + + FileName [simSymStr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Structural detection of symmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define SIM_READ_SYMMS(pNode) ((Vec_Int_t *)pNode->pCopy) +#define SIM_SET_SYMMS(pNode,vVect) (pNode->pCopy = (Abc_Obj_t *)(vVect)) + +static void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ); +static void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); +static void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ); +static void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ); +static void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ); +static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ); +static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ); +static void Sim_SymmsPrint( Vec_Int_t * vSymms ); +static void Sim_SymmsTrans( Vec_Int_t * vSymms ); +static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ); +static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes symmetries for a single output function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pTemp; + int * pMap, i; + + assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) ); + + // get the structural support + pNtk->vSupps = Sim_ComputeStrSupp( pNtk ); + // set elementary info for the CIs + Abc_NtkForEachCi( pNtk, pTemp, i ) + SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) ); + // create the map of CI ids into their numbers + pMap = Sim_SymmsCreateMap( pNtk ); + // collect the nodes in the TFI cone of this output + vNodes = Abc_NtkDfs( pNtk, 0 ); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + if ( Abc_NodeIsConst(pTemp) ) + continue; + Sim_SymmsStructComputeOne( pNtk, pTemp, pMap ); + } + // collect the results for the COs; + Abc_NtkForEachCo( pNtk, pTemp, i ) + { + pTemp = Abc_ObjFanin0(pTemp); + if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) + continue; + Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) ); + } + // clean the intermediate results + Sim_UtilInfoFree( pNtk->vSupps ); + pNtk->vSupps = NULL; + Abc_NtkForEachCi( pNtk, pTemp, i ) + Vec_IntFree( SIM_READ_SYMMS(pTemp) ); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + Vec_IntFree( SIM_READ_SYMMS(pTemp) ); + Vec_PtrFree( vNodes ); + free( pMap ); +} + +/**Function************************************************************* + + Synopsis [Recursively computes symmetries. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ) +{ + Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther; + Vec_Int_t * vSymms; + Abc_Obj_t * pTemp; + int i; + + // allocate the temporary arrays + vNodes = Vec_PtrAlloc( 10 ); + vNodesPi0 = Vec_PtrAlloc( 10 ); + vNodesPi1 = Vec_PtrAlloc( 10 ); + vNodesOther = Vec_PtrAlloc( 10 ); + + // collect the fanins of the implication supergate + Sim_SymmsBalanceCollect_rec( pNode, vNodes ); + + // sort the nodes in the implication supergate + Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther ); + + // start the resulting set + vSymms = Vec_IntAlloc( 10 ); + // generate symmetries from the groups + Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap ); + Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap ); + // add symmetries from other inputs + for ( i = 0; i < vNodesOther->nSize; i++ ) + { + pTemp = Abc_ObjRegular(vNodesOther->pArray[i]); + Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap ); + } + Vec_PtrFree( vNodes ); + Vec_PtrFree( vNodesPi0 ); + Vec_PtrFree( vNodesPi1 ); + Vec_PtrFree( vNodesOther ); + + // set the symmetry at the node + SIM_SET_SYMMS( pNode, vSymms ); +} + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + // if the new node is complemented, another gate begins + if ( Abc_ObjIsComplement(pNode) ) + { + Vec_PtrPushUnique( vNodes, pNode ); + return; + } + // if pNew is the PI node, return + if ( Abc_ObjIsCi(pNode) ) + { + Vec_PtrPushUnique( vNodes, pNode ); + return; + } + // go through the branches + Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes ); + Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes ); +} + +/**Function************************************************************* + + Synopsis [Divides PI variables into groups.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, + Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ) +{ + Abc_Obj_t * pNode; + int i; + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) ) + Vec_PtrPush( vNodesOther, pNode ); + else if ( Abc_ObjIsComplement(pNode) ) + Vec_PtrPush( vNodesPis0, pNode ); + else + Vec_PtrPush( vNodesPis1, pNode ); + } +} + +/**Function************************************************************* + + Synopsis [Makes the product of two partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ) +{ + Abc_Obj_t * pNode1, * pNode2; + unsigned uSymm; + int i, k; + + if ( vNodesPi->nSize == 0 ) + return; + + // go through the pairs + for ( i = 0; i < vNodesPi->nSize; i++ ) + for ( k = i+1; k < vNodesPi->nSize; k++ ) + { + // get the two PI nodes + pNode1 = Abc_ObjRegular(vNodesPi->pArray[i]); + pNode2 = Abc_ObjRegular(vNodesPi->pArray[k]); + assert( pMap[pNode1->Id] != pMap[pNode2->Id] ); + assert( pMap[pNode1->Id] >= 0 ); + assert( pMap[pNode2->Id] >= 0 ); + // generate symmetry + if ( pMap[pNode1->Id] < pMap[pNode2->Id] ) + uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]); + else + uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]); + // check if symmetry belongs + if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) ) + Vec_IntPushUnique( vSymms, (int)uSymm ); + } +} + +/**Function************************************************************* + + Synopsis [Add the filters symmetries from the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, + Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ) +{ + unsigned uSymm; + int i; + + if ( vSymms0->nSize == 0 ) + return; + + // go through the pairs + for ( i = 0; i < vSymms0->nSize; i++ ) + { + uSymm = (unsigned)vSymms0->pArray[i]; + // check if symmetry belongs + if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) && + Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) && + Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) ) + Vec_IntPushUnique( vSymms, (int)uSymm ); + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if symmetry is compatible with the group of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ) +{ + Vec_Int_t * vSymmsNode; + Abc_Obj_t * pNode; + int i, s, Ind1, Ind2, fIsVar1, fIsVar2; + + if ( vNodesOther->nSize == 0 ) + return 1; + + // get the indices of the PI variables + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + + // go through the nodes + // if they do not belong to a support, it is okay + // if one belongs, the other does not belong, quit + // if they belong, but are not part of symmetry, quit + for ( i = 0; i < vNodesOther->nSize; i++ ) + { + pNode = Abc_ObjRegular(vNodesOther->pArray[i]); + fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 ); + fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 ); + + if ( !fIsVar1 && !fIsVar2 ) + continue; + if ( fIsVar1 ^ fIsVar2 ) + return 0; + // both belong + // check if there is a symmetry + vSymmsNode = SIM_READ_SYMMS( pNode ); + for ( s = 0; s < vSymmsNode->nSize; s++ ) + if ( uSymm == (unsigned)vSymmsNode->pArray[s] ) + break; + if ( s == vSymmsNode->nSize ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if symmetry is compatible with the group of PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ) +{ + Abc_Obj_t * pNode; + int i, Ind1, Ind2, fHasVar1, fHasVar2; + + if ( vNodesPi->nSize == 0 ) + return 1; + + // get the indices of the PI variables + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + + // go through the PI nodes + fHasVar1 = fHasVar2 = 0; + for ( i = 0; i < vNodesPi->nSize; i++ ) + { + pNode = Abc_ObjRegular(vNodesPi->pArray[i]); + if ( pMap[pNode->Id] == Ind1 ) + fHasVar1 = 1; + else if ( pMap[pNode->Id] == Ind2 ) + fHasVar2 = 1; + } + return fHasVar1 == fHasVar2; +} + + + +/**Function************************************************************* + + Synopsis [Improvements due to transitivity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsTrans( Vec_Int_t * vSymms ) +{ + unsigned uSymm, uSymma, uSymmr; + int i, Ind1, Ind2; + int k, Ind1a, Ind2a; + int j; + int nTrans = 0; + + for ( i = 0; i < vSymms->nSize; i++ ) + { + uSymm = (unsigned)vSymms->pArray[i]; + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + // find other symmetries that have Ind1 + for ( k = i+1; k < vSymms->nSize; k++ ) + { + uSymma = (unsigned)vSymms->pArray[k]; + if ( uSymma == uSymm ) + continue; + Ind1a = (uSymma & 0xffff); + Ind2a = (uSymma >> 16); + if ( Ind1a == Ind1 ) + { + // find the symmetry (Ind2,Ind2a) + if ( Ind2 < Ind2a ) + uSymmr = ((Ind2 << 16) | Ind2a); + else + uSymmr = ((Ind2a << 16) | Ind2); + for ( j = 0; j < vSymms->nSize; j++ ) + if ( uSymmr == (unsigned)vSymms->pArray[j] ) + break; + if ( j == vSymms->nSize ) + nTrans++; + } + } + + } + printf( "Trans = %d.\n", nTrans ); +} + + +/**Function************************************************************* + + Synopsis [Transfers from the vector to the matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms ) +{ + int i, Ind1, Ind2, nInputs; + unsigned uSymm; + // add diagonal elements + nInputs = Extra_BitMatrixReadSize( pMatSymm ); + for ( i = 0; i < nInputs; i++ ) + Extra_BitMatrixInsert1( pMatSymm, i, i ); + // add non-diagonal elements + for ( i = 0; i < vSymms->nSize; i++ ) + { + uSymm = (unsigned)vSymms->pArray[i]; + Ind1 = (uSymm & 0xffff); + Ind2 = (uSymm >> 16); + Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 ); + Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 ); + } +} + +/**Function************************************************************* + + Synopsis [Mapping of indices into numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ) +{ + int * pMap; + Abc_Obj_t * pNode; + int i; + pMap = ALLOC( int, Abc_NtkObjNumMax(pNtk) ); + for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ ) + pMap[i] = -1; + Abc_NtkForEachCi( pNtk, pNode, i ) + pMap[pNode->Id] = i; + return pMap; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/sim/simUtils.c b/src/opt/sim/simUtils.c index 5f5708f2..5a57ca2d 100644 --- a/src/sat/sim/simUtils.c +++ b/src/opt/sim/simUtils.c @@ -25,6 +25,17 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -44,6 +55,7 @@ Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean ) { Vec_Ptr_t * vInfo; int i; + assert( nSize > 0 && nWords > 0 ); vInfo = Vec_PtrAlloc( nSize ); vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords ); if ( fClean ) @@ -137,71 +149,6 @@ void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, V /**Function************************************************************* - Synopsis [Computes structural supports.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sim_UtilComputeStrSupp( Sim_Man_t * p ) -{ - Abc_Obj_t * pNode; - unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; - int i, k; - // assign the structural support to the PIs - Abc_NtkForEachCi( p->pNtk, pNode, i ) - Sim_SuppStrSetVar( p, pNode, i ); - // derive the structural supports of the internal nodes - Abc_NtkForEachNode( p->pNtk, pNode, i ) - { - if ( Abc_NodeIsConst(pNode) ) - continue; - pSimmNode = p->vSuppStr->pArray[ pNode->Id ]; - pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; - pSimmNode2 = p->vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ]; - for ( k = 0; k < p->nSuppWords; k++ ) - pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k]; - } - // set the structural supports of the PO nodes - Abc_NtkForEachCo( p->pNtk, pNode, i ) - { - pSimmNode = p->vSuppStr->pArray[ pNode->Id ]; - pSimmNode1 = p->vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; - for ( k = 0; k < p->nSuppWords; k++ ) - pSimmNode[k] = pSimmNode1[k]; - } -} - -/**Function************************************************************* - - Synopsis [Assigns random simulation info to the PIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sim_UtilAssignRandom( Sim_Man_t * p ) -{ - Abc_Obj_t * pNode; - unsigned * pSimInfo; - int i, k; - // assign the random/systematic simulation info to the PIs - Abc_NtkForEachCi( p->pNtk, pNode, i ) - { - pSimInfo = p->vSim0->pArray[pNode->Id]; - for ( k = 0; k < p->nSimWords; k++ ) - pSimInfo[k] = SIM_RANDOM_UNSIGNED; - } -} - -/**Function************************************************************* - Synopsis [Flips the simulation info of the node.] Description [] @@ -211,12 +158,12 @@ void Sim_UtilAssignRandom( Sim_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode ) +void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ) { unsigned * pSimInfo1, * pSimInfo2; int k; - pSimInfo1 = p->vSim1->pArray[pNode->Id]; - pSimInfo2 = p->vSim0->pArray[pNode->Id]; + pSimInfo1 = p->vSim0->pArray[pNode->Id]; + pSimInfo2 = p->vSim1->pArray[pNode->Id]; for ( k = 0; k < p->nSimWords; k++ ) pSimInfo2[k] = ~pSimInfo1[k]; } @@ -232,12 +179,12 @@ void Sim_UtilFlipSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -bool Sim_UtilCompareSimInfo( Sim_Man_t * p, Abc_Obj_t * pNode ) +bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ) { unsigned * pSimInfo1, * pSimInfo2; int k; - pSimInfo1 = p->vSim1->pArray[pNode->Id]; - pSimInfo2 = p->vSim0->pArray[pNode->Id]; + pSimInfo1 = p->vSim0->pArray[pNode->Id]; + pSimInfo2 = p->vSim1->pArray[pNode->Id]; for ( k = 0; k < p->nSimWords; k++ ) if ( pSimInfo2[k] != pSimInfo1[k] ) return 0; @@ -343,6 +290,44 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT /**Function************************************************************* + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) +{ + unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; + int k, fComp1, fComp2; + // simulate the internal nodes + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsConst(pNode) ) + return; + pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id); + pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); + pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); + fComp1 = Abc_ObjFaninC0(pNode); + fComp2 = Abc_ObjFaninC1(pNode); + if ( fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k]; + else if ( fComp1 && !fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k] & pSimmNode2[k]; + else if ( !fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & ~pSimmNode2[k]; + else // if ( fComp1 && fComp2 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k] & pSimmNode2[k]; +} + +/**Function************************************************************* + Synopsis [Returns 1 if the simulation infos are equal.] Description [] @@ -361,13 +346,106 @@ int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ) { Abc_NtkForEachCo( p->pNtk, pNode, i ) Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) - Counter += Sim_SuppStrHasVar( p, pNode, v ); + Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v ); } else { Abc_NtkForEachCo( p->pNtk, pNode, i ) Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) - Counter += Sim_SuppFunHasVar( p, i, v ); + Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1's in the bitstring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) +{ + unsigned char * pBytes; + int nOnes, nBytes, i; + pBytes = (unsigned char *)pSimInfo; + nBytes = 4 * nSimWords; + nOnes = 0; + for ( i = 0; i < nBytes; i++ ) + nOnes += bit_count[ pBytes[i] ]; + return nOnes; +} + + +/**Function************************************************************* + + Synopsis [Returns the random pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + pPatRand[k] = SIM_RANDOM_UNSIGNED; +} + +/**Function************************************************************* + + Synopsis [Counts the total number of pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ) +{ + unsigned * pSupp; + int Counter, nOnes, nPairs, i; + Counter = 0; + Vec_PtrForEachEntry( vSuppFun, pSupp, i ) + { + nOnes = Sim_UtilCountOnes( pSupp, nSimWords ); + nPairs = nOnes * (nOnes - 1) / 2; + Vec_IntWriteEntry( vCounters, i, nPairs ); + Counter += nPairs; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of entries in the array of matrices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters ) +{ + Extra_BitMat_t * vMat; + int Counter, nPairs, i; + Counter = 0; + Vec_PtrForEachEntry( vMatrs, vMat, i ) + { + nPairs = Extra_BitMatrixCountOnesUpper( vMat ); + Vec_IntWriteEntry( vCounters, i, nPairs ); + Counter += nPairs; } return Counter; } diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 946ed56b..39c6fae8 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -50,6 +50,7 @@ struct Fraig_ParamsStruct_t_ int fTryProve; // tries to solve the final miter int fVerbose; // the verbosiness flag int fVerboseP; // the verbosiness flag (for proof reporting) + int fInternal; // is set to 1 for internal fraig calls }; //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index 0194f3b4..c9e6960c 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -164,10 +164,9 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i ) /**Function************************************************************* - Synopsis [Creates a new node.] + Synopsis [Creates a new PO node.] - Description [This procedure should be called to create the constant - node and the PI nodes first.] + Description [This procedure may take a complemented node.] SideEffects [] @@ -176,9 +175,8 @@ Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i ) ***********************************************************************/ void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode ) { -// assert( pNode->fNodePo == 0 ); // internal node may be a PO two times - pNode->fNodePo = 1; + Fraig_Regular(pNode)->fNodePo = 1; Fraig_NodeVecPush( p->vOutputs, pNode ); } diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c index b46f6c41..73640387 100644 --- a/src/sat/fraig/fraigFeed.c +++ b/src/sat/fraig/fraigFeed.c @@ -768,7 +768,80 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) /**Function************************************************************* - Synopsis [Doubles the size of simulation info.] + Synopsis [Generated trivial counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ) +{ + int * pModel; + pModel = ALLOC( int, p->vInputs->nSize ); + memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); + return pModel; +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManSimulateBitNode_rec( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + int Value0, Value1; + if ( Fraig_NodeIsTravIdCurrent( p, pNode ) ) + return pNode->fMark3; + Fraig_NodeSetTravIdCurrent( p, pNode ); + Value0 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p1) ); + Value1 = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode->p2) ); + Value0 ^= Fraig_IsComplement(pNode->p1); + Value1 ^= Fraig_IsComplement(pNode->p2); + pNode->fMark3 = Value0 & Value1; + return pNode->fMark3; +} + +/**Function************************************************************* + + Synopsis [Simulates one bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManSimulateBitNode( Fraig_Man_t * p, Fraig_Node_t * pNode, int * pModel ) +{ + int fCompl, RetValue, i; + // set the PI values + Fraig_ManIncrementTravId( p ); + for ( i = 0; i < p->vInputs->nSize; i++ ) + { + Fraig_NodeSetTravIdCurrent( p, p->vInputs->pArray[i] ); + p->vInputs->pArray[i]->fMark3 = pModel[i]; + } + // perform the traversal + fCompl = Fraig_IsComplement(pNode); + RetValue = Fraig_ManSimulateBitNode_rec( p, Fraig_Regular(pNode) ); + return fCompl ^ RetValue; +} + + +/**Function************************************************************* + + Synopsis [Saves the counter example.] Description [] @@ -779,33 +852,52 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p ) ***********************************************************************/ int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ) { - int * pModel = NULL; + int * pModel; int iPattern; - int i; + int i, fCompl; - iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 ); + // the node can be complemented + fCompl = Fraig_IsComplement(pNode); + // because we compare with constant 0, p->pConst1 should also be complemented + fCompl = !fCompl; + + // derive the model + pModel = Fraig_ManAllocCounterExample( p ); + iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->nWordsRand, 1 ); if ( iPattern >= 0 ) { - pModel = ALLOC( int, p->vInputs->nSize ); - memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); for ( i = 0; i < p->vInputs->nSize; i++ ) - if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) ) + if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) ) pModel[i] = 1; +/* +printf( "SAT solver's pattern:\n" ); +for ( i = 0; i < p->vInputs->nSize; i++ ) + printf( "%d", pModel[i] ); +printf( "\n" ); +*/ + assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); return pModel; } - iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 ); + iPattern = Fraig_FindFirstDiff( p->pConst1, Fraig_Regular(pNode), fCompl, p->iWordStart, 0 ); if ( iPattern >= 0 ) { - pModel = ALLOC( int, p->vInputs->nSize ); - memset( pModel, 0, sizeof(int) * p->vInputs->nSize ); for ( i = 0; i < p->vInputs->nSize; i++ ) - if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) ) + if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) ) pModel[i] = 1; +/* +printf( "SAT solver's pattern:\n" ); +for ( i = 0; i < p->vInputs->nSize; i++ ) + printf( "%d", pModel[i] ); +printf( "\n" ); +*/ + assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) ); return pModel; } - return pModel; + FREE( pModel ); + return NULL; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 5f8b3496..1c765c12 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -239,10 +239,11 @@ struct Fraig_NodeStruct_t_ unsigned fMark0 : 1; // the mark used for traversals unsigned fMark1 : 1; // the mark used for traversals unsigned fMark2 : 1; // the mark used for traversals + unsigned fMark3 : 1; // the mark used for traversals unsigned fFeedUse : 1; // the presence of the variable in the feedback unsigned fFeedVal : 1; // the value of the variable in the feedback unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many) - unsigned nOnes : 22; // the number of 1's in the random sim info + unsigned nOnes : 21; // the number of 1's in the random sim info // the children of the node Fraig_Node_t * p1; // the first child @@ -379,6 +380,7 @@ extern void Fraig_FeedBackInit( Fraig_Man_t * p ); extern void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); extern void Fraig_FeedBackTest( Fraig_Man_t * p ); extern int Fraig_FeedBackCompress( Fraig_Man_t * p ); +extern int * Fraig_ManAllocCounterExample( Fraig_Man_t * p ); extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ); /*=== fraigMem.c =============================================================*/ extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ); @@ -406,7 +408,7 @@ extern Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No extern void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); extern int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ); extern int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); -extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ); +extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand ); extern void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); extern void Fraig_TablePrintStatsS( Fraig_Man_t * pMan ); extern void Fraig_TablePrintStatsF( Fraig_Man_t * pMan ); @@ -416,10 +418,6 @@ extern int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEqu extern int Fraig_NodeCountPis( Msat_IntVec_t * vVars, int nVarsPi ); extern int Fraig_NodeCountSuppVars( Fraig_Man_t * p, Fraig_Node_t * pNode, int fSuppStr ); extern int Fraig_NodesCompareSupps( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); -extern void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ); -extern void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -extern int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); -extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); extern int Fraig_NodeAndSimpleCase_rec( Fraig_Node_t * pOld, Fraig_Node_t * pNew ); extern int Fraig_NodeIsExorType( Fraig_Node_t * pNode ); extern void Fraig_ManSelectBestChoice( Fraig_Man_t * p ); @@ -435,6 +433,10 @@ extern int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_No extern int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew ); extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux ); extern int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums ); +extern void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ); +extern void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); /*=== fraigVec.c ===============================================================*/ extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p ); diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 65716340..cfdba619 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -42,6 +42,7 @@ int timeAssign; ***********************************************************************/ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) { + memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info pParams->nBTLimit = 99; // the max number of backtracks to perform diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index da9e8e2b..17201e58 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -122,11 +122,23 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) ***********************************************************************/ int Fraig_ManCheckMiter( Fraig_Man_t * p ) { - if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) ) + Fraig_Node_t * pNode; + FREE( p->pModel ); + // get the output node (it can be complemented!) + pNode = p->vOutputs->pArray[0]; + // if the miter is constant 0, the problem is UNSAT + if ( pNode == Fraig_Not(p->pConst1) ) return 1; + // consider the special case when the miter is constant 1 + if ( pNode == p->pConst1 ) + { + // in this case, any counter example will do to distinquish it from constant 0 + // here we pick the counter example composed of all zeros + p->pModel = Fraig_ManAllocCounterExample( p ); + return 0; + } // save the counter example - FREE( p->pModel ); - p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) ); + p->pModel = Fraig_ManSaveCounterExample( p, pNode ); // if the model is not found, return undecided if ( p->pModel == NULL ) return -1; diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c index 4dc6afdc..7a8af749 100644 --- a/src/sat/fraig/fraigTable.c +++ b/src/sat/fraig/fraigTable.c @@ -382,28 +382,52 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor SeeAlso [] ***********************************************************************/ -int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ) +int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand ) { int i, v; assert( !Fraig_IsComplement(pNode1) ); assert( !Fraig_IsComplement(pNode2) ); - if ( fUseRand ) + // take into account possible internal complementation + fCompl ^= pNode1->fInv; + fCompl ^= pNode2->fInv; + // find the pattern + if ( fCompl ) { - // check the simulation info - for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) - for ( v = 0; v < 32; v++ ) - if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) ) - return i * 32 + v; + if ( fUseRand ) + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimR[i] != ~pNode2->puSimR[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimR[i] ^ ~pNode2->puSimR[i]) & (1 << v) ) + return i * 32 + v; + } + else + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimD[i] != ~pNode2->puSimD[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimD[i] ^ ~pNode2->puSimD[i]) & (1 << v) ) + return i * 32 + v; + } } else { - // check the simulation info - for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) - for ( v = 0; v < 32; v++ ) - if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) ) - return i * 32 + v; + if ( fUseRand ) + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) ) + return i * 32 + v; + } + else + { + for ( i = 0; i < iWordLast; i++ ) + if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) + for ( v = 0; v < 32; v++ ) + if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) ) + return i * 32 + v; + } } return -1; } diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c index 6b7431f2..2155c4a3 100644 --- a/src/sat/fraig/fraigUtil.c +++ b/src/sat/fraig/fraigUtil.c @@ -962,6 +962,71 @@ Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux ) return vSuper; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ) +{ + pMan->nTravIds2++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + pNode->TravId2 = pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2 - 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/sim/module.make b/src/sat/sim/module.make deleted file mode 100644 index ac887acf..00000000 --- a/src/sat/sim/module.make +++ /dev/null @@ -1,6 +0,0 @@ -SRC += src/sat/sim/simMan.c \ - src/sat/sim/simSat.c \ - src/sat/sim/simSupp.c \ - src/sat/sim/simSym.c \ - src/sat/sim/simUnate.c \ - src/sat/sim/simUtils.c diff --git a/src/sat/sim/simSupp.c b/src/sat/sim/simSupp.c deleted file mode 100644 index 570e8dc6..00000000 --- a/src/sat/sim/simSupp.c +++ /dev/null @@ -1,273 +0,0 @@ -/**CFile**************************************************************** - - FileName [simSupp.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Simulation to determine functional support.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "sim.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ); -static int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ); -static void Sim_ComputeSuppSetTargets( Sim_Man_t * p ); -static void Sim_UtilAssignFromFifo( Sim_Man_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Compute functional supports of the primary outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sim_Man_t * Sim_ComputeSupp( Abc_Ntk_t * pNtk ) -{ - Sim_Man_t * p; - int i, nSolved; - -// srand( time(NULL) ); - srand( 0xedfeedfe ); - - // start the simulation manager - p = Sim_ManStart( pNtk ); - Sim_UtilComputeStrSupp( p ); - - // compute functional support using one round of random simulation - Sim_UtilAssignRandom( p ); - Sim_ComputeSuppRound( p, 0 ); - - // set the support targets - Sim_ComputeSuppSetTargets( p ); -printf( "Initial targets = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs) ); - if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 ) - goto exit; - - // compute patterns using one round of random simulation - Sim_UtilAssignRandom( p ); - nSolved = Sim_ComputeSuppRound( p, 1 ); -printf( "First step targets = %5d. Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved ); - if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 ) - goto exit; - - // simulate until saturation - for ( i = 0; i < 10; i++ ) - { - // compute additional functional support -// Sim_UtilAssignFromFifo( p ); - Sim_UtilAssignRandom( p ); - nSolved = Sim_ComputeSuppRound( p, 1 ); -printf( "Next step targets = %5d. Solved = %5d.\n", Vec_PtrSizeSize(p->vSuppTargs), nSolved ); - if ( Vec_PtrSizeSize(p->vSuppTargs) == 0 ) - goto exit; - } - -exit: -// return p; - Sim_ManStop( p ); - return NULL; -} - -/**Function************************************************************* - - Synopsis [Computes functional support using one round of simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets ) -{ - Vec_Int_t * vTargets; - Abc_Obj_t * pNode; - int i, Counter = 0; - // perform one round of random simulation - Sim_UtilSimulate( p, 0 ); - // iterate through the CIs and detect COs that depend on them - Abc_NtkForEachCi( p->pNtk, pNode, i ) - { - vTargets = p->vSuppTargs->pArray[i]; - if ( fUseTargets && vTargets->nSize == 0 ) - continue; - Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets ); - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [Computes functional support for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets ) -{ - Sim_Pat_t * pPat; - Vec_Int_t * vTargets; - Vec_Vec_t * vNodesByLevel; - Abc_Obj_t * pNodeCi, * pNode; - int i, k, v, Output, LuckyPat, fType0, fType1; - int Counter = 0; - // collect nodes by level in the TFO of the CI - // (this procedure increments TravId of the collected nodes) - pNodeCi = Abc_NtkCi( p->pNtk, iNumCi ); - vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 ); - // complement the simulation info of the selected CI - Sim_UtilFlipSimInfo( p, pNodeCi ); - // simulate the levelized structure of nodes - Vec_VecForEachEntry( vNodesByLevel, pNode, i, k ) - { - fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) ); - fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) ); - Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 ); - } - // set the simulation info of the affected COs - if ( fUseTargets ) - { - vTargets = p->vSuppTargs->pArray[iNumCi]; - for ( i = vTargets->nSize - 1; i >= 0; i-- ) - { - // get the target output - Output = vTargets->pArray[i]; - // get the target node - pNode = Abc_NtkCo( p->pNtk, Output ); - // the output should be in the cone - assert( Abc_NodeIsTravIdCurrent(pNode) ); - - // simulate the node - Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); - - // skip if the simulation info is equal - if ( Sim_UtilCompareSimInfo( p, pNode ) ) - continue; - - // otherwise, we solved a new target - Vec_IntRemove( vTargets, Output ); - Counter++; - // make sure this variable is not yet detected - assert( !Sim_SuppFunHasVar(p, Output, iNumCi) ); - // set this variable - Sim_SuppFunSetVar( p, Output, iNumCi ); - - // detect the differences in the simulation info - Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs ); - // create new patterns - Vec_IntForEachEntry( p->vDiffs, LuckyPat, k ) - { - // set the new pattern - pPat = Sim_ManPatAlloc( p ); - pPat->Input = iNumCi; - pPat->Output = Output; - Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) - if ( Sim_SimInfoHasVar( p, pNodeCi, LuckyPat ) ) - Sim_SetBit( pPat->pData, v ); - Vec_PtrPush( p->vFifo, pPat ); - break; - } - } - } - else - { - Abc_NtkForEachCo( p->pNtk, pNode, Output ) - { - if ( !Abc_NodeIsTravIdCurrent( pNode ) ) - continue; - Sim_UtilSimulateNode( p, pNode, 1, 1, 1 ); - if ( !Sim_UtilCompareSimInfo( p, pNode ) ) - { - if ( !Sim_SuppFunHasVar(p, Output, iNumCi) ) - Counter++; - Sim_SuppFunSetVar( p, Output, iNumCi ); - } - } - } - Vec_VecFree( vNodesByLevel ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Sets the simulation targets.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sim_ComputeSuppSetTargets( Sim_Man_t * p ) -{ - Abc_Obj_t * pNode; - unsigned * pSuppStr, * pSuppFun; - int i, k, Num; - Abc_NtkForEachCo( p->pNtk, pNode, i ) - { - pSuppStr = p->vSuppStr->pArray[pNode->Id]; - pSuppFun = p->vSuppFun->pArray[i]; - // find vars in the structural support that are not in the functional support - Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs ); - Vec_IntForEachEntry( p->vDiffs, Num, k ) - Vec_IntPush( p->vSuppTargs->pArray[Num], i ); - } -} - -/**Function************************************************************* - - Synopsis [Sets the new patterns from fifo.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sim_UtilAssignFromFifo( Sim_Man_t * p ) -{ - Sim_Pat_t * pPat; - int i; - for ( i = 0; i < p->nSimBits; i++ ) - { - pPat = Vec_PtrPop( p->vFifo ); - - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/seq/module.make b/src/seq/module.make deleted file mode 100644 index d6d908e7..00000000 --- a/src/seq/module.make +++ /dev/null @@ -1 +0,0 @@ -SRC += diff --git a/src/sop/mvc/module.make b/src/sop/mvc/module.make deleted file mode 100644 index bdb5c5cf..00000000 --- a/src/sop/mvc/module.make +++ /dev/null @@ -1,16 +0,0 @@ -SRC += src/sop/mvc/mvc.c \ - src/sop/mvc/mvcApi.c \ - src/sop/mvc/mvcCompare.c \ - src/sop/mvc/mvcContain.c \ - src/sop/mvc/mvcCover.c \ - src/sop/mvc/mvcCube.c \ - src/sop/mvc/mvcDivide.c \ - src/sop/mvc/mvcDivisor.c \ - src/sop/mvc/mvcList.c \ - src/sop/mvc/mvcLits.c \ - src/sop/mvc/mvcMan.c \ - src/sop/mvc/mvcOpAlg.c \ - src/sop/mvc/mvcOpBool.c \ - src/sop/mvc/mvcPrint.c \ - src/sop/mvc/mvcSort.c \ - src/sop/mvc/mvcUtils.c |