1 /**CFile****************************************************************
2
3 FileName [saig.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__saig__saig_h
22 #define ABC__aig__saig__saig_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/aig/aig.h"
30
31 ABC_NAMESPACE_HEADER_START
32
33 ////////////////////////////////////////////////////////////////////////
34 /// PARAMETERS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 ////////////////////////////////////////////////////////////////////////
38 /// BASIC TYPES ///
39 ////////////////////////////////////////////////////////////////////////
40
41 typedef struct Sec_MtrStatus_t_ Sec_MtrStatus_t;
42 struct Sec_MtrStatus_t_
43 {
44 int nInputs; // the total number of inputs
45 int nNodes; // the total number of nodes
46 int nOutputs; // the total number of outputs
47 int nUnsat; // the number of UNSAT outputs
48 int nSat; // the number of SAT outputs
49 int nUndec; // the number of undecided outputs
50 int iOut; // the satisfied output
51 };
52
53 typedef struct Saig_ParBbr_t_ Saig_ParBbr_t;
54 struct Saig_ParBbr_t_
55 {
56 int TimeLimit;
57 int nBddMax;
58 int nIterMax;
59 int fPartition;
60 int fReorder;
61 int fReorderImage;
62 int fVerbose;
63 int fSilent;
64 int fSkipOutCheck;// skip output checking
65 int iFrame; // explored up to this frame
66 };
67
68
69 ////////////////////////////////////////////////////////////////////////
70 /// MACRO DEFINITIONS ///
71 ////////////////////////////////////////////////////////////////////////
72
Saig_ManPiNum(Aig_Man_t * p)73 static inline int Saig_ManPiNum( Aig_Man_t * p ) { return p->nTruePis; }
Saig_ManPoNum(Aig_Man_t * p)74 static inline int Saig_ManPoNum( Aig_Man_t * p ) { return p->nTruePos; }
Saig_ManCiNum(Aig_Man_t * p)75 static inline int Saig_ManCiNum( Aig_Man_t * p ) { return p->nTruePis + p->nRegs; }
Saig_ManCoNum(Aig_Man_t * p)76 static inline int Saig_ManCoNum( Aig_Man_t * p ) { return p->nTruePos + p->nRegs; }
Saig_ManRegNum(Aig_Man_t * p)77 static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
Saig_ManConstrNum(Aig_Man_t * p)78 static inline int Saig_ManConstrNum( Aig_Man_t * p ) { return p->nConstrs; }
Saig_ManLo(Aig_Man_t * p,int i)79 static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+i); }
Saig_ManLi(Aig_Man_t * p,int i)80 static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+i); }
81
Saig_ObjIsPi(Aig_Man_t * p,Aig_Obj_t * pObj)82 static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) < Saig_ManPiNum(p); }
Saig_ObjIsPo(Aig_Man_t * p,Aig_Obj_t * pObj)83 static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) < Saig_ManPoNum(p); }
Saig_ObjIsLo(Aig_Man_t * p,Aig_Obj_t * pObj)84 static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPiNum(p); }
Saig_ObjIsLi(Aig_Man_t * p,Aig_Obj_t * pObj)85 static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPoNum(p); }
Saig_ObjLoToLi(Aig_Man_t * p,Aig_Obj_t * pObj)86 static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+Aig_ObjCioId(pObj)-Saig_ManPiNum(p)); }
Saig_ObjLiToLo(Aig_Man_t * p,Aig_Obj_t * pObj)87 static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+Aig_ObjCioId(pObj)-Saig_ManPoNum(p)); }
Saig_ObjRegId(Aig_Man_t * p,Aig_Obj_t * pObj)88 static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPoNum(p); else assert(0); return -1; }
89
90 // iterator over the primary inputs/outputs
91 #define Saig_ManForEachPi( p, pObj, i ) \
92 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Saig_ManPiNum(p) )
93 #define Saig_ManForEachPo( p, pObj, i ) \
94 Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Saig_ManPoNum(p) )
95 // iterator over the latch inputs/outputs
96 #define Saig_ManForEachLo( p, pObj, i ) \
97 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i+Saig_ManPiNum(p))), 1); i++ )
98 #define Saig_ManForEachLi( p, pObj, i ) \
99 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i+Saig_ManPoNum(p))), 1); i++ )
100 // iterator over the latch input and outputs
101 #define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) \
102 for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \
103 && (((pObjLo)=Saig_ManLo(p, i)), 1); i++ )
104
105 ////////////////////////////////////////////////////////////////////////
106 /// FUNCTION DECLARATIONS ///
107 ////////////////////////////////////////////////////////////////////////
108
109 /*=== saigCone.c ==========================================================*/
110 extern void Saig_ManPrintCones( Aig_Man_t * p );
111 /*=== saigConstr.c ==========================================================*/
112 extern Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig );
113 extern Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs );
114 extern int Saig_ManDetectConstrTest( Aig_Man_t * p );
115 extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
116 /*=== saigConstr2.c ==========================================================*/
117 extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
118 extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
119 // -- jlong -- begin
120 extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );
121 extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt);
122 // --jlong -- end
123
124 /*=== saigDual.c ==========================================================*/
125 extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne );
126 extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
127 /*=== saigDup.c ==========================================================*/
128 extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
129 extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs, int fAddOuts );
130 extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
131 extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
132 extern Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
133 extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
134 extern Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
135 extern Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos );
136 /*=== saigHaig.c ==========================================================*/
137 extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
138 /*=== saigInd.c ==========================================================*/
139 extern int Saig_ManInduction( Aig_Man_t * p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
140 /*=== saigIoa.c ==========================================================*/
141 extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
142 extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
143 /*=== saigIso.c ==========================================================*/
144 extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose );
145 extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose );
146 extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvCosEquivs, int fVerbose );
147 /*=== saigIsoFast.c ==========================================================*/
148 extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
149 /*=== saigMiter.c ==========================================================*/
150 extern Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p );
151 extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
152 extern Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
153 extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
154 extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames );
155 extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
156 extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
157 extern int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
158 extern int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose );
159 extern int Saig_ManDemiterNew( Aig_Man_t * pMan );
160 /*=== saigOutdec.c ==========================================================*/
161 extern Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose );
162 /*=== saigPhase.c ==========================================================*/
163 extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
164 /*=== saigRetFwd.c ==========================================================*/
165 extern void Saig_ManMarkAutonomous( Aig_Man_t * p );
166 extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
167 /*=== saigRetMin.c ==========================================================*/
168 extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
169 extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
170 /*=== saigRetStep.c ==========================================================*/
171 extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs );
172 /*=== saigScl.c ==========================================================*/
173 extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
174 /*=== saigSimMv.c ==========================================================*/
175 extern Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
176 /*=== saigStrSim.c ==========================================================*/
177 extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
178 /*=== saigSwitch.c ==========================================================*/
179 extern Vec_Int_t * Saig_ManComputeSwitchProb2s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
180 /*=== saigSynch.c ==========================================================*/
181 extern Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p );
182 /*=== saigTrans.c ==========================================================*/
183 extern Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose );
184 /*=== saigWnd.c ==========================================================*/
185 extern Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist );
186 extern Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd );
187 extern Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p );
188
189
190
191 ABC_NAMESPACE_HEADER_END
192
193
194
195 #endif
196
197 ////////////////////////////////////////////////////////////////////////
198 /// END OF FILE ///
199 ////////////////////////////////////////////////////////////////////////
200
201