1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
/**CFile****************************************************************
FileName [ssw.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __SSW_H__
#define __SSW_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// choicing parameters
typedef struct Ssw_Pars_t_ Ssw_Pars_t;
struct Ssw_Pars_t_
{
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
int fConstrs; // treat the last nConstrs POs as seq constraints
int fMergeFull; // enables full merge when constraints are used
int nMaxLevs; // the max number of levels of nodes to consider
int nBTLimit; // conflict limit at a node
int nBTLimitGlobal;// conflict limit for multiple runs
int nMinDomSize; // min clock domain considered for optimization
int nItersStop; // stop after the given number of iterations
int fDumpSRInit; // dumps speculative reduction
int nResimDelta; // the number of nodes to resimulate
int nStepsMax; // (scorr only) the max number of induction steps
int TimeLimit; // time out in seconds
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
int fConstCorr; // perform constant correspondence
int fOutputCorr; // perform 'PO correspondence'
int fSemiFormal; // enable semiformal filtering
// int fUniqueness; // enable uniqueness constraints
int fDynamic; // enable dynamic addition of constraints
int fLocalSim; // enable local simulation simulation
int fPartSigCorr; // uses partial signal correspondence
int nIsleDist; // extends islands by the given distance
int fScorrGia; // new signal correspondence implementation
int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
int fEquivDump; // enables dumping equivalences
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
// optimized signal correspondence
int nSatVarMax2; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
int nRecycleCalls2;// calls to perform before recycling SAT solver (optimized latch corr only)
// internal parameters
int nIters; // the number of iterations performed
int nConflicts; // the total number of conflicts performed
// callback
void * pData;
void * pFunc;
};
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswBmc.c ==========================================================*/
extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
/*=== sswConstr.c ==========================================================*/
extern int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswIslands.c ==========================================================*/
extern int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars );
extern int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars );
/*=== sswMiter.c ===================================================*/
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswRarity.c ===================================================*/
extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
/*=== sswSim.c ===================================================*/
extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern void Ssw_SmlUnnormalize( Ssw_Sml_t * p );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit );
extern int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p );
extern Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
