1 /**CFile****************************************************************
2
3 FileName [wlc.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - August 22, 2014.]
16
17 Revision [$Id: wlc.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__base__wlc__wlc_h
22 #define ABC__base__wlc__wlc_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/gia/gia.h"
30 #include "misc/extra/extra.h"
31 #include "misc/util/utilNam.h"
32 #include "misc/mem/mem.h"
33 #include "misc/extra/extra.h"
34 #include "misc/util/utilTruth.h"
35 #include "base/main/mainInt.h"
36
37 ////////////////////////////////////////////////////////////////////////
38 /// PARAMETERS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 ABC_NAMESPACE_HEADER_START
42
43 // object types
44 typedef enum {
45 WLC_OBJ_NONE = 0, // 00: unknown
46 WLC_OBJ_PI, // 01: primary input
47 WLC_OBJ_PO, // 02: primary output
48 WLC_OBJ_FO, // 03: flop output
49 WLC_OBJ_FI, // 04: flop input (unused)
50 WLC_OBJ_FF, // 05: flop
51 WLC_OBJ_CONST, // 06: constant
52 WLC_OBJ_BUF, // 07: buffer
53 WLC_OBJ_MUX, // 08: multiplexer
54 WLC_OBJ_SHIFT_R, // 09: shift right
55 WLC_OBJ_SHIFT_RA, // 10: shift right (arithmetic)
56 WLC_OBJ_SHIFT_L, // 11: shift left
57 WLC_OBJ_SHIFT_LA, // 12: shift left (arithmetic)
58 WLC_OBJ_ROTATE_R, // 13: rotate right
59 WLC_OBJ_ROTATE_L, // 14: rotate left
60 WLC_OBJ_BIT_NOT, // 15: bitwise NOT
61 WLC_OBJ_BIT_AND, // 16: bitwise AND
62 WLC_OBJ_BIT_OR, // 17: bitwise OR
63 WLC_OBJ_BIT_XOR, // 18: bitwise XOR
64 WLC_OBJ_BIT_NAND, // 19: bitwise NAND
65 WLC_OBJ_BIT_NOR, // 20: bitwise OR
66 WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR
67 WLC_OBJ_BIT_SELECT, // 22: bit selection
68 WLC_OBJ_BIT_CONCAT, // 23: bit concatenation
69 WLC_OBJ_BIT_ZEROPAD, // 24: zero padding
70 WLC_OBJ_BIT_SIGNEXT, // 25: sign extension
71 WLC_OBJ_LOGIC_NOT, // 26: logic NOT
72 WLC_OBJ_LOGIC_IMPL, // 27: logic implication
73 WLC_OBJ_LOGIC_AND, // 28: logic AND
74 WLC_OBJ_LOGIC_OR, // 29: logic OR
75 WLC_OBJ_LOGIC_XOR, // 30: logic XOR
76 WLC_OBJ_COMP_EQU, // 31: compare equal
77 WLC_OBJ_COMP_NOTEQU, // 32: compare not equal
78 WLC_OBJ_COMP_LESS, // 33: compare less
79 WLC_OBJ_COMP_MORE, // 34: compare more
80 WLC_OBJ_COMP_LESSEQU, // 35: compare less or equal
81 WLC_OBJ_COMP_MOREEQU, // 36: compare more or equal
82 WLC_OBJ_REDUCT_AND, // 37: reduction AND
83 WLC_OBJ_REDUCT_OR, // 38: reduction OR
84 WLC_OBJ_REDUCT_XOR, // 39: reduction XOR
85 WLC_OBJ_REDUCT_NAND, // 40: reduction NAND
86 WLC_OBJ_REDUCT_NOR, // 41: reduction NOR
87 WLC_OBJ_REDUCT_NXOR, // 42: reduction NXOR
88 WLC_OBJ_ARI_ADD, // 43: arithmetic addition
89 WLC_OBJ_ARI_SUB, // 44: arithmetic subtraction
90 WLC_OBJ_ARI_MULTI, // 45: arithmetic multiplier
91 WLC_OBJ_ARI_DIVIDE, // 46: arithmetic division
92 WLC_OBJ_ARI_REM, // 47: arithmetic remainder
93 WLC_OBJ_ARI_MODULUS, // 48: arithmetic modulus
94 WLC_OBJ_ARI_POWER, // 49: arithmetic power
95 WLC_OBJ_ARI_MINUS, // 50: arithmetic minus
96 WLC_OBJ_ARI_SQRT, // 51: integer square root
97 WLC_OBJ_ARI_SQUARE, // 52: integer square
98 WLC_OBJ_TABLE, // 53: bit table
99 WLC_OBJ_READ, // 54: read port
100 WLC_OBJ_WRITE, // 55: write port
101 WLC_OBJ_ARI_ADDSUB, // 56: adder-subtractor
102 WLC_OBJ_SEL, // 57: positionally encoded selector
103 WLC_OBJ_DEC, // 58: decoder
104 WLC_OBJ_LUT, // 59: lookup table
105 WLC_OBJ_NUMBER // 59: unused
106 } Wlc_ObjType_t;
107 // when adding new types, remember to update table Wlc_Names in "wlcNtk.c"
108
109
110 // Unlike AIG managers and logic networks in ABC, this network treats POs and FIs
111 // as attributes of internal nodes and *not* as separate types of objects.
112
113
114 ////////////////////////////////////////////////////////////////////////
115 /// BASIC TYPES ///
116 ////////////////////////////////////////////////////////////////////////
117
118 typedef struct Wlc_Obj_t_ Wlc_Obj_t;
119 struct Wlc_Obj_t_ // 24 bytes
120 {
121 unsigned Type : 6; // node type
122 unsigned Signed : 1; // signed
123 unsigned Mark : 1; // user mark
124 unsigned Mark2 : 1; // user mark
125 unsigned fIsPo : 1; // this is PO
126 unsigned fIsFi : 1; // this is FI
127 unsigned fXConst : 1; // this is X-valued constant
128 unsigned nFanins; // fanin count
129 int End; // range end
130 int Beg; // range begin
131 union { int Fanins[2]; // fanin IDs
132 int * pFanins[1]; };
133 };
134
135 typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
136 struct Wlc_Ntk_t_
137 {
138 char * pName; // model name
139 char * pSpec; // input file name
140 Vec_Int_t vPis; // primary inputs
141 Vec_Int_t vPos; // primary outputs
142 Vec_Int_t vCis; // combinational inputs
143 Vec_Int_t vCos; // combinational outputs
144 Vec_Int_t vFfs; // flops
145 Vec_Int_t vFfs2; // flops
146 Vec_Int_t * vArsts; // async resets
147 Vec_Int_t * vInits; // initial values
148 char * pInits; // initial values
149 int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
150 int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
151 int fSmtLib; // the network comes from an SMT-LIB file
152 int fAsyncRst; // the network has asynchronous reset
153 int fMemPorts; // the network contains memory ports
154 int fEasyFfs; // the network contains simple flops
155 int nAssert; // the number of asserts
156 // memory for objects
157 Wlc_Obj_t * pObjs;
158 int iObj;
159 int nObjsAlloc;
160 Mem_Flex_t * pMemFanin;
161 Mem_Flex_t * pMemTable;
162 Vec_Ptr_t * vTables;
163 Vec_Wrd_t * vLutTruths;
164 // object names
165 Abc_Nam_t * pManName; // object names
166 Vec_Int_t vNameIds; // object name IDs
167 Vec_Int_t vValues; // value objects
168 // object attributes
169 int nTravIds; // counter of traversal IDs
170 Vec_Int_t vTravIds; // trav IDs of the objects
171 Vec_Int_t vCopies; // object first bits
172 Vec_Int_t vBits; // object mapping into AIG nodes
173 Vec_Int_t vLevels; // object levels
174 Vec_Int_t vRefs; // object reference counters
175 Vec_Int_t vPoPairs; // pairs of primary outputs
176 };
177
178 typedef struct Wlc_Par_t_ Wlc_Par_t;
179 struct Wlc_Par_t_
180 {
181 int nBitsAdd; // adder bit-width
182 int nBitsMul; // multiplier bit-widht
183 int nBitsMux; // MUX bit-width
184 int nBitsFlop; // flop bit-width
185 int nIterMax; // the max number of iterations
186 int nLimit; // the max number of signals
187 int fXorOutput; // XOR outputs of word-level miter
188 int fCheckClauses; // Check clauses in the reloaded trace
189 int fPushClauses; // Push clauses in the reloaded trace
190 int fMFFC; // Refine the entire MFFC of a PPI
191 int fPdra; // Use pdr -nct
192 int fLoadTrace; // Load previous traces if any
193 int fProofRefine; // Use proof-based refinement
194 int fHybrid; // Use a hybrid of CBR and PBR
195 int fCheckCombUnsat; // Check if ABS becomes comb. unsat
196 int fAbs2; // Use UFAR style createAbs
197 int fProofUsePPI; // Use PPI values in PBR
198 int fUseBmc3; // Run BMC3 in parallel
199 int fShrinkAbs; // Shrink Abs with BMC
200 int fShrinkScratch; // Restart pdr from scratch after shrinking
201 int fVerbose; // verbose output
202 int fPdrVerbose; // verbose output
203 int RunId; // id in this run
204 int (*pFuncStop)(int); // callback to terminate
205 };
206
207 typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
208 struct Wlc_BstPar_t_
209 {
210 int iOutput;
211 int nOutputRange;
212 int nAdderLimit;
213 int nMultLimit;
214 int fGiaSimple;
215 int fAddOutputs;
216 int fMulti;
217 int fBooth;
218 int fNonRest;
219 int fCla;
220 int fNoCleanup;
221 int fCreateMiter;
222 int fCreateWordMiter;
223 int fDecMuxes;
224 int fSaveFfNames;
225 int fVerbose;
226 Vec_Int_t * vBoxIds;
227 };
228
Wlc_BstParDefault(Wlc_BstPar_t * pPar)229 static inline void Wlc_BstParDefault( Wlc_BstPar_t * pPar )
230 {
231 memset( pPar, 0, sizeof(Wlc_BstPar_t) );
232 pPar->iOutput = -1;
233 pPar->nOutputRange = 0;
234 pPar->nAdderLimit = 0;
235 pPar->nMultLimit = 0;
236 pPar->fGiaSimple = 0;
237 pPar->fAddOutputs = 0;
238 pPar->fMulti = 0;
239 pPar->fBooth = 0;
240 pPar->fCla = 0;
241 pPar->fCreateMiter = 0;
242 pPar->fCreateWordMiter = 0;
243 pPar->fDecMuxes = 0;
244 pPar->fVerbose = 0;
245 }
246
247 typedef struct Wla_Man_t_ Wla_Man_t;
248 struct Wla_Man_t_
249 {
250 Wlc_Ntk_t * p;
251 Wlc_Par_t * pPars;
252 Vec_Vec_t * vClauses;
253 Vec_Int_t * vBlacks;
254 Vec_Int_t * vSignals;
255 Abc_Cex_t * pCex;
256 Gia_Man_t * pGia;
257 Vec_Bit_t * vUnmark;
258 void * pPdrPars;
259 void * pThread;
260
261 int iCexFrame;
262 int fNewAbs;
263
264 int nIters;
265 int nTotalCla;
266 int nDisj;
267 int nNDisj;
268
269 abctime tPdr;
270 abctime tCbr;
271 abctime tPbr;
272 };
273
Wlc_NtkObjNum(Wlc_Ntk_t * p)274 static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; }
Wlc_NtkObjNumMax(Wlc_Ntk_t * p)275 static inline int Wlc_NtkObjNumMax( Wlc_Ntk_t * p ) { return p->iObj; }
Wlc_NtkPiNum(Wlc_Ntk_t * p)276 static inline int Wlc_NtkPiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPis); }
Wlc_NtkPoNum(Wlc_Ntk_t * p)277 static inline int Wlc_NtkPoNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPos); }
Wlc_NtkCiNum(Wlc_Ntk_t * p)278 static inline int Wlc_NtkCiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vCis); }
Wlc_NtkCoNum(Wlc_Ntk_t * p)279 static inline int Wlc_NtkCoNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vCos); }
Wlc_NtkFfNum(Wlc_Ntk_t * p)280 static inline int Wlc_NtkFfNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vCis) - Vec_IntSize(&p->vPis); }
281
Wlc_NtkObj(Wlc_Ntk_t * p,int Id)282 static inline Wlc_Obj_t * Wlc_NtkObj( Wlc_Ntk_t * p, int Id ) { assert(Id > 0 && Id < p->nObjsAlloc); return p->pObjs + Id; }
Wlc_NtkPi(Wlc_Ntk_t * p,int i)283 static inline Wlc_Obj_t * Wlc_NtkPi( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPis, i) ); }
Wlc_NtkPo(Wlc_Ntk_t * p,int i)284 static inline Wlc_Obj_t * Wlc_NtkPo( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPos, i) ); }
Wlc_NtkCi(Wlc_Ntk_t * p,int i)285 static inline Wlc_Obj_t * Wlc_NtkCi( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCis, i) ); }
Wlc_NtkCo(Wlc_Ntk_t * p,int i)286 static inline Wlc_Obj_t * Wlc_NtkCo( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCos, i) ); }
Wlc_NtkFf(Wlc_Ntk_t * p,int i)287 static inline Wlc_Obj_t * Wlc_NtkFf( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vFfs, i) ); }
Wlc_NtkFf2(Wlc_Ntk_t * p,int i)288 static inline Wlc_Obj_t * Wlc_NtkFf2( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj( p, Vec_IntEntry(&p->vFfs2, i) ); }
289
Wlc_ObjIsPi(Wlc_Obj_t * p)290 static inline int Wlc_ObjIsPi( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_PI; }
Wlc_ObjIsPo(Wlc_Obj_t * p)291 static inline int Wlc_ObjIsPo( Wlc_Obj_t * p ) { return p->fIsPo; }
Wlc_ObjIsCi(Wlc_Obj_t * p)292 static inline int Wlc_ObjIsCi( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO; }
Wlc_ObjIsCo(Wlc_Obj_t * p)293 static inline int Wlc_ObjIsCo( Wlc_Obj_t * p ) { return p->fIsPo || p->fIsFi; }
Wlc_ObjIsRead(Wlc_Obj_t * p)294 static inline int Wlc_ObjIsRead( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_READ; }
Wlc_ObjIsWrite(Wlc_Obj_t * p)295 static inline int Wlc_ObjIsWrite( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_WRITE; }
Wlc_ObjIsMux(Wlc_Obj_t * p)296 static inline int Wlc_ObjIsMux( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_MUX; }
Wlc_ObjIsBuf(Wlc_Obj_t * p)297 static inline int Wlc_ObjIsBuf( Wlc_Obj_t * p ) { return p->Type == WLC_OBJ_BUF; }
Wlc_ObjIsFf(Wlc_Ntk_t * p,int i)298 static inline int Wlc_ObjIsFf( Wlc_Ntk_t * p, int i ) { return Wlc_NtkObj(p, i)->Type == WLC_OBJ_FF; }
299
Wlc_ObjId(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)300 static inline int Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return pObj - p->pObjs; }
Wlc_ObjCiId(Wlc_Obj_t * p)301 static inline int Wlc_ObjCiId( Wlc_Obj_t * p ) { assert( Wlc_ObjIsCi(p) ); return p->Fanins[1]; }
Wlc_ObjType(Wlc_Obj_t * pObj)302 static inline int Wlc_ObjType( Wlc_Obj_t * pObj ) { return pObj->Type; }
Wlc_ObjFaninNum(Wlc_Obj_t * p)303 static inline int Wlc_ObjFaninNum( Wlc_Obj_t * p ) { return p->nFanins; }
Wlc_ObjHasArray(Wlc_Obj_t * p)304 static inline int Wlc_ObjHasArray( Wlc_Obj_t * p ) { return p->nFanins > 2 || p->Type == WLC_OBJ_CONST || p->Type == WLC_OBJ_BIT_SELECT; }
Wlc_ObjFanins(Wlc_Obj_t * p)305 static inline int * Wlc_ObjFanins( Wlc_Obj_t * p ) { return Wlc_ObjHasArray(p) ? p->pFanins[0] : p->Fanins; }
Wlc_ObjFaninId(Wlc_Obj_t * p,int i)306 static inline int Wlc_ObjFaninId( Wlc_Obj_t * p, int i ) { return Wlc_ObjFanins(p)[i]; }
Wlc_ObjFaninId0(Wlc_Obj_t * p)307 static inline int Wlc_ObjFaninId0( Wlc_Obj_t * p ) { return Wlc_ObjFanins(p)[0]; }
Wlc_ObjFaninId1(Wlc_Obj_t * p)308 static inline int Wlc_ObjFaninId1( Wlc_Obj_t * p ) { return Wlc_ObjFanins(p)[1]; }
Wlc_ObjFaninId2(Wlc_Obj_t * p)309 static inline int Wlc_ObjFaninId2( Wlc_Obj_t * p ) { return Wlc_ObjFanins(p)[2]; }
Wlc_ObjFanin(Wlc_Ntk_t * p,Wlc_Obj_t * pObj,int i)310 static inline Wlc_Obj_t * Wlc_ObjFanin( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int i ) { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, i) ); }
Wlc_ObjFanin0(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)311 static inline Wlc_Obj_t * Wlc_ObjFanin0( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 0) ); }
Wlc_ObjFanin1(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)312 static inline Wlc_Obj_t * Wlc_ObjFanin1( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 1) ); }
Wlc_ObjFanin2(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)313 static inline Wlc_Obj_t * Wlc_ObjFanin2( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 2) ); }
314
Wlc_ObjRange(Wlc_Obj_t * p)315 static inline int Wlc_ObjRange( Wlc_Obj_t * p ) { return 1 + (p->End >= p->Beg ? p->End - p->Beg : p->Beg - p->End); }
Wlc_ObjRangeEnd(Wlc_Obj_t * p)316 static inline int Wlc_ObjRangeEnd( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->pFanins[0][1]; }
Wlc_ObjRangeBeg(Wlc_Obj_t * p)317 static inline int Wlc_ObjRangeBeg( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->pFanins[0][2]; }
Wlc_ObjRangeIsReversed(Wlc_Obj_t * p)318 static inline int Wlc_ObjRangeIsReversed( Wlc_Obj_t * p ) { return p->End < p->Beg; }
319
Wlc_ObjIsSigned(Wlc_Obj_t * p)320 static inline int Wlc_ObjIsSigned( Wlc_Obj_t * p ) { return p->Signed; }
Wlc_ObjIsSignedFanin01(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)321 static inline int Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : (Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed); }
Wlc_ObjIsSignedFanin0(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)322 static inline int Wlc_ObjIsSignedFanin0( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : Wlc_ObjFanin0(p, pObj)->Signed; }
Wlc_ObjIsSignedFanin1(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)323 static inline int Wlc_ObjIsSignedFanin1( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : Wlc_ObjFanin1(p, pObj)->Signed; }
Wlc_ObjSign(Wlc_Obj_t * p)324 static inline int Wlc_ObjSign( Wlc_Obj_t * p ) { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjIsSigned(p) ); }
Wlc_ObjConstValue(Wlc_Obj_t * p)325 static inline int * Wlc_ObjConstValue( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_CONST); return Wlc_ObjFanins(p); }
Wlc_ObjTableId(Wlc_Obj_t * p)326 static inline int Wlc_ObjTableId( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_TABLE); return p->Fanins[1]; }
Wlc_ObjTable(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)327 static inline word * Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) ); }
Wlc_ObjLevelId(Wlc_Ntk_t * p,int iObj)328 static inline int Wlc_ObjLevelId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); }
Wlc_ObjLevel(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)329 static inline int Wlc_ObjLevel( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_ObjLevelId( p, Wlc_ObjId(p, pObj) ); }
330
Wlc_NtkCleanCopy(Wlc_Ntk_t * p)331 static inline void Wlc_NtkCleanCopy( Wlc_Ntk_t * p ) { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 ); }
Wlc_NtkHasCopy(Wlc_Ntk_t * p)332 static inline int Wlc_NtkHasCopy( Wlc_Ntk_t * p ) { return Vec_IntSize( &p->vCopies ) > 0; }
Wlc_ObjSetCopy(Wlc_Ntk_t * p,int iObj,int i)333 static inline void Wlc_ObjSetCopy( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vCopies, iObj, i ); }
Wlc_ObjCopy(Wlc_Ntk_t * p,int iObj)334 static inline int Wlc_ObjCopy( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vCopies, iObj ); }
Wlc_ObjCopyObj(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Wlc_Obj_t * pObj)335 static inline Wlc_Obj_t * Wlc_ObjCopyObj(Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj) {return Wlc_NtkObj(pNew, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj))); }
336
Wlc_NtkCleanNameId(Wlc_Ntk_t * p)337 static inline void Wlc_NtkCleanNameId( Wlc_Ntk_t * p ) { Vec_IntFill( &p->vNameIds, p->nObjsAlloc, 0 ); }
Wlc_NtkHasNameId(Wlc_Ntk_t * p)338 static inline int Wlc_NtkHasNameId( Wlc_Ntk_t * p ) { return Vec_IntSize( &p->vNameIds ) > 0; }
Wlc_ObjSetNameId(Wlc_Ntk_t * p,int iObj,int i)339 static inline void Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vNameIds, iObj, i ); }
Wlc_ObjNameId(Wlc_Ntk_t * p,int iObj)340 static inline int Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vNameIds, iObj ); }
341
Wlc_ObjFo2Fi(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)342 static inline Wlc_Obj_t * Wlc_ObjFo2Fi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkPoNum(p) + Wlc_ObjCiId(pObj) - Wlc_NtkPiNum(p)); }
Wlc_ObjCo2PoFo(Wlc_Ntk_t * p,int iCoId)343 static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) { return iCoId < Wlc_NtkPoNum(p) ? Wlc_NtkPo(p, iCoId) : Wlc_NtkCi(p, Wlc_NtkPiNum(p) + iCoId - Wlc_NtkPoNum(p)); }
344
345 ////////////////////////////////////////////////////////////////////////
346 /// MACRO DEFINITIONS ///
347 ////////////////////////////////////////////////////////////////////////
348
349 ////////////////////////////////////////////////////////////////////////
350 /// ITERATORS ///
351 ////////////////////////////////////////////////////////////////////////
352
353 #define Wlc_NtkForEachObj( p, pObj, i ) \
354 for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )
355 #define Wlc_NtkForEachObjReverse( p, pObj, i ) \
356 for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- )
357 #define Wlc_NtkForEachObjVec( vVec, p, pObj, i ) \
358 for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )
359 #define Wlc_NtkForEachPi( p, pPi, i ) \
360 for ( i = 0; (i < Wlc_NtkPiNum(p)) && (((pPi) = Wlc_NtkPi(p, i)), 1); i++ )
361 #define Wlc_NtkForEachPo( p, pPo, i ) \
362 for ( i = 0; (i < Wlc_NtkPoNum(p)) && (((pPo) = Wlc_NtkPo(p, i)), 1); i++ )
363 #define Wlc_NtkForEachCi( p, pCi, i ) \
364 for ( i = 0; (i < Wlc_NtkCiNum(p)) && (((pCi) = Wlc_NtkCi(p, i)), 1); i++ )
365 #define Wlc_NtkForEachCo( p, pCo, i ) \
366 for ( i = 0; (i < Wlc_NtkCoNum(p)) && (((pCo) = Wlc_NtkCo(p, i)), 1); i++ )
367 #define Wlc_NtkForEachFf( p, pFf, i ) \
368 for ( i = 0; (i < Vec_IntSize(&p->vFfs)) && (((pFf) = Wlc_NtkFf(p, i)), 1); i++ )
369 #define Wlc_NtkForEachFf2( p, pFf, i ) \
370 for ( i = 0; (i < Vec_IntSize(&p->vFfs2)) && (((pFf) = Wlc_NtkFf2(p, i)), 1); i++ )
371
372 #define Wlc_ObjForEachFanin( pObj, iFanin, i ) \
373 for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )
374 #define Wlc_ObjForEachFaninObj( p, pObj, pFanin, i ) \
375 for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((pFanin) = Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, i))), 1); i++ )
376 #define Wlc_ObjForEachFaninReverse( pObj, iFanin, i ) \
377 for ( i = Wlc_ObjFaninNum(pObj) - 1; (i >= 0) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i-- )
378
379
380 ////////////////////////////////////////////////////////////////////////
381 /// FUNCTION DECLARATIONS ///
382 ////////////////////////////////////////////////////////////////////////
383
384 /*=== wlcAbs.c ========================================================*/
385 extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
386 extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
387 /*=== wlcAbs2.c ========================================================*/
388 extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
389 /*=== wlcBlast.c ========================================================*/
390 extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
391 /*=== wlcCom.c ========================================================*/
392 extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
393 /*=== wlcMem.c ========================================================*/
394 extern Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p, int fClean );
395 extern void Wlc_NtkPrintMemory( Wlc_Ntk_t * p );
396 extern Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p );
397 extern int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose );
398 extern Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose );
399 /*=== wlcNdr.c ========================================================*/
400 extern Wlc_Ntk_t * Wlc_ReadNdr( char * pFileName );
401 extern void Wlc_WriteNdr( Wlc_Ntk_t * pNtk, char * pFileName );
402 extern Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData );
403 extern void * Wlc_NtkToNdr( Wlc_Ntk_t * pNtk );
404 /*=== wlcNtk.c ========================================================*/
405 extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
406 extern char * Wlc_ObjTypeName( Wlc_Obj_t * p );
407 extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc );
408 extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
409 extern int Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins );
410 extern void Wlc_ObjSetCi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
411 extern void Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput );
412 extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
413 extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
414 extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
415 extern int Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins );
416 extern void Wlc_NtkFree( Wlc_Ntk_t * p );
417 extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
418 extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
419 extern int Wlc_NtkRemapLevels( Wlc_Ntk_t * p, Vec_Int_t * vObjs, int nLevels );
420 extern int Wlc_NtkCountRealPis( Wlc_Ntk_t * p );
421 extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
422 extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
423 extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
424 extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
425 extern void Wlc_NtkPrintObjects( Wlc_Ntk_t * p );
426 extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
427 extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
428 extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
429 extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
430 extern Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p );
431 extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
432 extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
433 extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p );
434 extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
435 extern void Wlc_NtkShortNames( Wlc_Ntk_t * p );
436 extern int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p );
437 extern void Wlc_NtkSetRefs( Wlc_Ntk_t * p );
438 extern int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew );
439 /*=== wlcReadSmt.c ========================================================*/
440 extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
441 extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
442 /*=== wlcSim.c ========================================================*/
443 extern Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int nFrames );
444 extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
445 /*=== wlcStdin.c ========================================================*/
446 extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
447 /*=== wlcReadVer.c ========================================================*/
448 extern char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p );
449 extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
450 /*=== wlcUif.c ========================================================*/
451 extern Vec_Int_t * Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM );
452 extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
453 extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
454 extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
455 extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
456 extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
457 /*=== wlcWin.c =============================================================*/
458 extern void Wlc_WinProfileArith( Wlc_Ntk_t * p );
459 /*=== wlcWriteVer.c ========================================================*/
460 extern void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops );
461
462
463 ABC_NAMESPACE_HEADER_END
464
465 #endif
466
467 ////////////////////////////////////////////////////////////////////////
468 /// END OF FILE ///
469 ////////////////////////////////////////////////////////////////////////
470
471