ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sim.h
Go to the documentation of this file.
1
20
21#ifndef ABC__opt__sim__sim_h
22#define ABC__opt__sim__sim_h
23
24
25/*
26 The ideas realized in this package are described in the paper:
27 "Detecting Symmetries in Boolean Functions using Circuit Representation,
28 Simulation, and Satisfiability".
29*/
30
34
38
39
40
42
43
47
48typedef struct Sym_Man_t_ Sym_Man_t;
50{
51 // info about the network
52 Abc_Ntk_t * pNtk; // the network
53 Vec_Ptr_t * vNodes; // internal nodes in topological order
56 // internal simulation information
57 int nSimWords; // the number of bits in simulation info
58 Vec_Ptr_t * vSim; // simulation info
59 // support information
60 Vec_Ptr_t * vSuppFun; // bit representation
61 Vec_Vec_t * vSupports; // integer representation
62 // symmetry info for each output
63 Vec_Ptr_t * vMatrSymms; // symmetric pairs
64 Vec_Ptr_t * vMatrNonSymms; // non-symmetric pairs
65 Vec_Int_t * vPairsTotal; // total pairs
66 Vec_Int_t * vPairsSym; // symmetric pairs
67 Vec_Int_t * vPairsNonSym; // non-symmetric pairs
68 // temporary simulation info
69 unsigned * uPatRand;
70 unsigned * uPatCol;
71 unsigned * uPatRow;
72 // temporary
76 int iVar1;
77 int iVar2;
80 // internal data structures
84 // pairs
90 // runtime statistics
98};
99
100typedef struct Sim_Man_t_ Sim_Man_t;
102{
103 // info about the network
108 // internal simulation information
109 int nSimBits; // the number of bits in simulation info
110 int nSimWords; // the number of words in simulation info
111 Vec_Ptr_t * vSim0; // simulation info 1
112 Vec_Ptr_t * vSim1; // simulation info 2
113 // support information
114 int nSuppBits; // the number of bits in support info
115 int nSuppWords; // the number of words in support info
116 Vec_Ptr_t * vSuppStr; // structural supports
117 Vec_Ptr_t * vSuppFun; // functional supports
118 // simulation targets
119 Vec_Vec_t * vSuppTargs; // support targets
120 int iInput; // the input current processed
121 // internal data structures
128 // runtime statistics
134};
135
136typedef struct Sim_Pat_t_ Sim_Pat_t;
138{
139 int Input; // the input which it has detected
140 int Output; // the output for which it was collected
141 unsigned * pData; // the simulation data
142};
143
147
148#define SIM_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
149#define SIM_LAST_BITS(n) ((((n)&31) > 0)? (n)&31 : 32)
150
151#define SIM_MASK_FULL (0xFFFFFFFF)
152#define SIM_MASK_BEG(n) (SIM_MASK_FULL >> (32-n))
153#define SIM_MASK_END(n) (SIM_MASK_FULL << (n))
154#define SIM_SET_0_FROM(m,n) ((m) & ~SIM_MASK_BEG(n))
155#define SIM_SET_1_FROM(m,n) ((m) | SIM_MASK_END(n))
156
157// generating random unsigned (#define RAND_MAX 0x7fff)
158#define SIM_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
159
160// macros to get hold of bits in a bit string
161#define Sim_SetBit(p,i) ((p)[(i)>>5] |= (1<<((i) & 31)))
162#define Sim_XorBit(p,i) ((p)[(i)>>5] ^= (1<<((i) & 31)))
163#define Sim_HasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
164
165// macros to get hold of the support info
166#define Sim_SuppStrSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
167#define Sim_SuppStrHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
168#define Sim_SuppFunSetVar(vSupps,Output,v) Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))
169#define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
170#define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
171#define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
172#define Sim_SimInfoGet(vInfo,pNode) ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
173
177
178/*=== simMan.c ==========================================================*/
179extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
180extern void Sym_ManStop( Sym_Man_t * p );
181extern void Sym_ManPrintStats( Sym_Man_t * p );
182extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight );
183extern void Sim_ManStop( Sim_Man_t * p );
184extern void Sim_ManPrintStats( Sim_Man_t * p );
186extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
187/*=== simSeq.c ==========================================================*/
188extern Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
189extern Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
190/*=== simSupp.c ==========================================================*/
191extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
192extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
193/*=== simSym.c ==========================================================*/
194extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
195/*=== simSymSat.c ==========================================================*/
196extern int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
197/*=== simSymStr.c ==========================================================*/
198extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
199/*=== simSymSim.c ==========================================================*/
200extern void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
201/*=== simUtil.c ==========================================================*/
202extern Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, int fClean );
203extern void Sim_UtilInfoFree( Vec_Ptr_t * p );
204extern void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords );
205extern void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
206extern void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
207extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
208extern int Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
209extern void Sim_UtilSimulate( Sim_Man_t * p, int fFirst );
210extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, int fType, int fType1, int fType2 );
211extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
212extern void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
213extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
214extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
215extern Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
216extern void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
217extern void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
218extern void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
219extern int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
220extern int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
221extern int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
222extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
223extern void Sim_UtilCountPairsAll( Sym_Man_t * p );
224extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
225
226
227
229
230
231
232#endif
233
237
int nWords
Definition abcNpn.c:127
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
struct Extra_MmFixed_t_ Extra_MmFixed_t
Definition extra.h:147
void Sim_UtilInfoFree(Vec_Ptr_t *p)
Definition simUtils.c:84
struct Sim_Pat_t_ Sim_Pat_t
Definition sim.h:136
void Sim_UtilSetRandom(unsigned *pPatRand, int nSimWords)
Definition simUtils.c:448
int Sim_UtilInfoCompare(Sim_Man_t *p, Abc_Obj_t *pNode)
Definition simUtils.c:186
Vec_Ptr_t * Sim_SimulateSeqRandom(Abc_Ntk_t *pNtk, int nFrames, int nWords)
FUNCTION DEFINITIONS ///.
Definition simSeq.c:51
int Sim_UtilInfoIsImp(unsigned *pPats1, unsigned *pPats2, int nSimWords)
Definition simUtils.c:524
void Sim_SymmsStructCompute(Abc_Ntk_t *pNtk, Vec_Ptr_t *vMatrs, Vec_Ptr_t *vSuppFun)
FUNCTION DEFINITIONS ///.
Definition simSymStr.c:61
Vec_Ptr_t * Sim_UtilInfoAlloc(int nSize, int nWords, int fClean)
FUNCTION DEFINITIONS ///.
Definition simUtils.c:57
void Sim_ManPatFree(Sim_Man_t *p, Sim_Pat_t *pPat)
Definition simMan.c:282
Sim_Pat_t * Sim_ManPatAlloc(Sim_Man_t *p)
Definition simMan.c:261
void Sim_ManPrintStats(Sim_Man_t *p)
Definition simMan.c:233
Sym_Man_t * Sym_ManStart(Abc_Ntk_t *pNtk, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition simMan.c:46
int Sim_UtilInfoIsClause(unsigned *pPats1, unsigned *pPats2, int nSimWords)
Definition simUtils.c:544
void Sim_SymmsSimulate(Sym_Man_t *p, unsigned *pPatRand, Vec_Ptr_t *vMatrsNonSym)
FUNCTION DEFINITIONS ///.
Definition simSymSim.c:49
void Sim_UtilSimulateNodeOne(Abc_Obj_t *pNode, Vec_Ptr_t *vSimInfo, int nSimWords, int nOffset)
Definition simUtils.c:303
void Sim_UtilSetCompl(unsigned *pPatRand, int nSimWords)
Definition simUtils.c:466
void Sim_UtilInfoDetectNews(unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
Definition simUtils.c:142
int Sim_UtilCountOnes(unsigned *pSimInfo, int nSimWords)
Definition simUtils.c:403
int Sim_UtilMatrsAreDisjoint(Sym_Man_t *p)
Definition simUtils.c:704
struct Sim_Man_t_ Sim_Man_t
Definition sim.h:100
void Sim_UtilInfoFlip(Sim_Man_t *p, Abc_Obj_t *pNode)
Definition simUtils.c:165
void Sim_UtilTransferNodeOne(Abc_Obj_t *pNode, Vec_Ptr_t *vSimInfo, int nSimWords, int nOffset, int fShift)
Definition simUtils.c:342
Sim_Man_t * Sim_ManStart(Abc_Ntk_t *pNtk, int fLightweight)
Definition simMan.c:166
int Sim_UtilCountSuppSizes(Sim_Man_t *p, int fStruct)
Definition simUtils.c:372
void Sim_ManStop(Sim_Man_t *p)
Definition simMan.c:208
void Sym_ManStop(Sym_Man_t *p)
Definition simMan.c:98
void Sim_UtilSetConst(unsigned *pPatRand, int nSimWords, int fConst1)
Definition simUtils.c:484
int Sim_ComputeTwoVarSymms(Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition simSym.c:46
Vec_Int_t * Sim_UtilCountOnesArray(Vec_Ptr_t *vInfo, int nSimWords)
Definition simUtils.c:426
void Sim_UtilInfoAdd(unsigned *pInfo1, unsigned *pInfo2, int nWords)
Definition simUtils.c:101
void Sim_UtilSimulate(Sim_Man_t *p, int fFirst)
Definition simUtils.c:209
void Sim_UtilSimulateNode(Sim_Man_t *p, Abc_Obj_t *pNode, int fType, int fType1, int fType2)
Definition simUtils.c:232
Vec_Ptr_t * Sim_ComputeStrSupp(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition simSupp.c:57
int Sim_SymmsGetPatternUsingSat(Sym_Man_t *p, unsigned *pPattern)
FUNCTION DEFINITIONS ///.
Definition simSymSat.c:51
void Sim_UtilInfoDetectDiffs(unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
Definition simUtils.c:119
Vec_Ptr_t * Sim_ComputeFunSupp(Abc_Ntk_t *pNtk, int fVerbose)
Definition simSupp.c:103
Vec_Ptr_t * Sim_SimulateSeqModel(Abc_Ntk_t *pNtk, int nFrames, int *pModel)
Definition simSeq.c:92
void Sym_ManPrintStats(Sym_Man_t *p)
Definition simMan.c:135
int Sim_UtilCountAllPairs(Vec_Ptr_t *vSuppFun, int nSimWords, Vec_Int_t *vCounters)
Definition simUtils.c:564
int Sim_UtilInfoIsEqual(unsigned *pPats1, unsigned *pPats2, int nSimWords)
Definition simUtils.c:504
typedefABC_NAMESPACE_HEADER_START struct Sym_Man_t_ Sym_Man_t
INCLUDES ///.
Definition sim.h:48
void Sim_UtilCountPairsAll(Sym_Man_t *p)
Definition simUtils.c:660
Vec_Ptr_t * vSuppStr
Definition sim.h:116
abctime timeTrav
Definition sim.h:130
int nOutputs
Definition sim.h:106
abctime timeSim
Definition sim.h:129
int nSimWords
Definition sim.h:110
int nInputs
Definition sim.h:105
Vec_Ptr_t * vSim1
Definition sim.h:112
int nSuppBits
Definition sim.h:114
Vec_Vec_t * vSuppTargs
Definition sim.h:119
Abc_Ntk_t * pNtk
Definition sim.h:104
int nSuppWords
Definition sim.h:115
abctime timeFraig
Definition sim.h:131
int nSatRunsUnsat
Definition sim.h:127
Extra_MmFixed_t * pMmPat
Definition sim.h:122
int iInput
Definition sim.h:120
Vec_Ptr_t * vSim0
Definition sim.h:111
int nSimBits
Definition sim.h:109
int nSatRuns
Definition sim.h:125
abctime timeTotal
Definition sim.h:133
Vec_Ptr_t * vFifo
Definition sim.h:123
int nSatRunsSat
Definition sim.h:126
Vec_Int_t * vDiffs
Definition sim.h:124
abctime timeSat
Definition sim.h:132
int fLightweight
Definition sim.h:107
Vec_Ptr_t * vSuppFun
Definition sim.h:117
int Output
Definition sim.h:140
int Input
Definition sim.h:139
unsigned * pData
Definition sim.h:141
abctime timeTotal
Definition sim.h:97
int iVar2Old
Definition sim.h:79
int iVar1Old
Definition sim.h:78
abctime timeStruct
Definition sim.h:91
unsigned * uPatRow
Definition sim.h:71
int nSimWords
Definition sim.h:57
unsigned * uPatCol
Definition sim.h:70
int nPairsSymmStr
Definition sim.h:86
unsigned * uPatRand
Definition sim.h:69
int nInputs
Definition sim.h:54
abctime timeSat
Definition sim.h:96
Vec_Ptr_t * vSuppFun
Definition sim.h:60
Vec_Ptr_t * vMatrSymms
Definition sim.h:63
abctime timeFraig
Definition sim.h:95
Vec_Vec_t * vSupports
Definition sim.h:61
Vec_Int_t * vPairsNonSym
Definition sim.h:67
int nSatRunsSat
Definition sim.h:82
int nPairsRem
Definition sim.h:88
abctime timeCount
Definition sim.h:92
Vec_Ptr_t * vNodes
Definition sim.h:53
Vec_Int_t * vVarsV
Definition sim.h:74
Vec_Int_t * vPairsTotal
Definition sim.h:65
int nPairsNonSymm
Definition sim.h:87
int nOutputs
Definition sim.h:55
Vec_Ptr_t * vMatrNonSymms
Definition sim.h:64
int iOutput
Definition sim.h:75
int iVar1
Definition sim.h:76
Vec_Ptr_t * vSim
Definition sim.h:58
abctime timeSim
Definition sim.h:94
Vec_Int_t * vPairsSym
Definition sim.h:66
int iVar2
Definition sim.h:77
Vec_Int_t * vVarsU
Definition sim.h:73
int nSatRuns
Definition sim.h:81
int nPairsSymm
Definition sim.h:85
abctime timeMatr
Definition sim.h:93
int nSatRunsUnsat
Definition sim.h:83
int nPairsTotal
Definition sim.h:89
Abc_Ntk_t * pNtk
Definition sim.h:52
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42