/**CFile****************************************************************
FileName [sim.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Simulation package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__opt__sim__sim_h
#define ABC__opt__sim__sim_h
/*
The ideas realized in this package are described in the paper:
"Detecting Symmetries in Boolean Functions using Circuit Representation,
Simulation, and Satisfiability".
*/
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// 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; // bit representation
Vec_Vec_t * vSupports; // integer representation
// 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;
// temporary
Vec_Int_t * vVarsU;
Vec_Int_t * vVarsV;
int iOutput;
int iVar1;
int iVar2;
int iVar1Old;
int iVar2Old;
// internal data structures
int nSatRuns;
int nSatRunsSat;
int nSatRunsUnsat;
// pairs
int nPairsSymm;
int nPairsSymmStr;
int nPairsNonSymm;
int nPairsRem;
int nPairsTotal;
// runtime statistics
abctime timeStruct;
abctime timeCount;
abctime timeMatr;
abctime timeSim;
abctime timeFraig;
abctime timeSat;
abctime timeTotal;
};
typedef struct Sim_Man_t_ Sim_Man_t;
struct Sim_Man_t_
{
// info about the network
Abc_Ntk_t * pNtk;
int nInputs;
int nOutputs;
int fLightweight;
// internal simulation information
int nSimBits; // the number of bits in simulation info
int nSimWords; // the number of words in simulation info
Vec_Ptr_t * vSim0; // simulation info 1
Vec_Ptr_t * vSim1; // simulation info 2
// support information
int nSuppBits; // the number of bits in support info
int nSuppWords; // the number of words in support info
Vec_Ptr_t * vSuppStr; // structural supports
Vec_Ptr_t * vSuppFun; // functional supports
// simulation targets
Vec_Vec_t * vSuppTargs; // support targets
int iInput; // the input current processed
// internal data structures
Extra_MmFixed_t * pMmPat;
Vec_Ptr_t * vFifo;
Vec_Int_t * vDiffs;
int nSatRuns;
int nSatRunsSat;
int nSatRunsUnsat;
// runtime statistics
abctime timeSim;
abctime timeTrav;
abctime timeFraig;
abctime timeSat;
abctime timeTotal;
};
typedef struct Sim_Pat_t_ Sim_Pat_t;
struct Sim_Pat_t_
{
int Input; // the input which it has detected
int Output; // the output for which it was collected
unsigned * pData; // the simulation data
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define SIM_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
#define SIM_LAST_BITS(n) ((((n)&31) > 0)? (n)&31 : 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()))
// macros to get hold of bits in a bit string
#define Sim_SetBit(p,i) ((p)[(i)>>5] |= (1<<((i) & 31)))
#define Sim_XorBit(p,i) ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define Sim_HasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
// macros to get hold of the support info
#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))
#define Sim_SimInfoGet(vInfo,pNode) ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== simMan.c ==========================================================*/
extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
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, int fLightweight );
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 );
/*=== simSeq.c ==========================================================*/
extern Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
extern Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
/*=== simSupp.c ==========================================================*/
extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
/*=== simSym.c ==========================================================*/
extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
/*=== simSymSat.c ==========================================================*/
extern int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
/*=== simSymStr.c ==========================================================*/
extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
/*=== 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, int 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_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
extern int Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
extern void Sim_UtilSimulate( Sim_Man_t * p, int fFirst );
extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, int fType, int fType1, int fType2 );
extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
extern void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
extern Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
extern void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
extern void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
extern void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
extern int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
extern void Sim_UtilCountPairsAll( Sym_Man_t * p );
extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////