ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
wlnRead.c
Go to the documentation of this file.
1
20
21#include "wln.h"
22#include "proof/cec/cec.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
30#define MAX_LINE 1000000
31
32#define MAX_MAP 32
33#define CELL_NUM 8
34#define WIRE_NUM 5
35#define TEMP_NUM 5
36#define CONST_SHIFT 99
37
38//typedef struct Rtl_Lib_t_ Rtl_Lib_t;
39struct Rtl_Lib_t_
40{
41 char * pSpec; // input file name
42 Vec_Ptr_t * vNtks; // modules
43 Abc_Nam_t * pManName; // object names
44 Vec_Int_t vConsts; // constants
45 Vec_Int_t vSlices; // selections
46 Vec_Int_t vConcats; // concatenations
47 FILE * pFile; // temp file
48 Vec_Int_t * vTokens; // temp tokens
49 int pMap[MAX_MAP]; // temp map
50 Vec_Int_t * vMap; // mapping NameId into wires
51 Vec_Int_t * vDirects; // direct equivalences
52 Vec_Int_t * vInverses; // inverse equivalences
53 Vec_Int_t vAttrTemp; // temp
54 Vec_Int_t vTemp[TEMP_NUM]; // temp
55};
56
57typedef struct Rtl_Ntk_t_ Rtl_Ntk_t;
58struct Rtl_Ntk_t_
59{
60 int NameId; // model name
61 int nInputs; // word-level inputs
62 int nOutputs; // word-level outputs
63 Vec_Int_t vWires; // wires (name{upto,signed,in,out}+width+offset+number)
64 Vec_Int_t vCells; // instances ([0]type+[1]name+[2]mod+[3]ins+[4]nattr+[5]nparams+[6]nconns+[7]mark+(attr+params+conns))
65 Vec_Int_t vConns; // connection pairs
66 Vec_Int_t vStore; // storage for cells
67 Vec_Int_t vAttrs; // attributes
68 Rtl_Lib_t * pLib; // parent
69 Vec_Int_t vOrder; // topological order
70 Vec_Int_t vLits; // bit-level view
71 Vec_Int_t vDrivers; // bit-level view
72 Vec_Int_t vBitTemp; // storage for bits
73 Vec_Int_t vBitTemp2; // storage for bits
74 Gia_Man_t * pGia; // derived by bit-blasting
75 int Slice0; // first slice
76 int Slice1; // last slice
77 int iCopy; // place in array
78 int fRoot; // denote root network
79};
80
81static inline int Rtl_LibNtkNum( Rtl_Lib_t * pLib ) { return Vec_PtrSize(pLib->vNtks); }
82static inline Rtl_Ntk_t * Rtl_LibNtk( Rtl_Lib_t * pLib, int i ) { return (Rtl_Ntk_t *)Vec_PtrEntry(pLib->vNtks, i); }
83static inline Rtl_Ntk_t * Rtl_LibTop( Rtl_Lib_t * pLib ) { return Rtl_LibNtk( pLib, Rtl_LibNtkNum(pLib)-1 ); }
84static inline char * Rtl_LibStr( Rtl_Lib_t * pLib, int h ) { return Abc_NamStr(pLib->pManName, h); }
85static inline int Rtl_LibStrId( Rtl_Lib_t * pLib, char * s ) { return Abc_NamStrFind(pLib->pManName, s); }
86
87static inline Rtl_Ntk_t * Rtl_NtkModule( Rtl_Ntk_t * p, int i ) { return Rtl_LibNtk( p->pLib, i ); }
88
89static inline int Rtl_NtkStrId( Rtl_Ntk_t * p, char * s ) { return Abc_NamStrFind(p->pLib->pManName, s); }
90static inline char * Rtl_NtkStr( Rtl_Ntk_t * p, int h ) { return Abc_NamStr(p->pLib->pManName, h); }
91static inline char * Rtl_NtkName( Rtl_Ntk_t * p ) { return Rtl_NtkStr(p, p->NameId); }
92
93static inline FILE * Rtl_NtkFile( Rtl_Ntk_t * p ) { return p->pLib->pFile; }
94static inline int Rtl_NtkTokId( Rtl_Ntk_t * p, int i ) { return i < Vec_IntSize(p->pLib->vTokens) ? Vec_IntEntry(p->pLib->vTokens, i) : -1; }
95static inline char * Rtl_NtkTokStr( Rtl_Ntk_t * p, int i ) { return i < Vec_IntSize(p->pLib->vTokens) ? Rtl_NtkStr(p, Vec_IntEntry(p->pLib->vTokens, i)) : NULL; }
96static inline int Rtl_NtkTokCheck( Rtl_Ntk_t * p, int i, int Tok ) { return i == p->pLib->pMap[Tok]; }
97static inline int Rtl_NtkPosCheck( Rtl_Ntk_t * p, int i, int Tok ) { return Vec_IntEntry(p->pLib->vTokens, i) == p->pLib->pMap[Tok]; }
98
99static inline int Rtl_NtkInputNum( Rtl_Ntk_t * p ) { return p->nInputs; }
100static inline int Rtl_NtkOutputNum( Rtl_Ntk_t * p ) { return p->nOutputs; }
101static inline int Rtl_NtkAttrNum( Rtl_Ntk_t * p ) { return Vec_IntSize(&p->vAttrs)/2; }
102static inline int Rtl_NtkWireNum( Rtl_Ntk_t * p ) { return Vec_IntSize(&p->vWires)/WIRE_NUM; }
103static inline int Rtl_NtkCellNum( Rtl_Ntk_t * p ) { return Vec_IntSize(&p->vCells); }
104static inline int Rtl_NtkConNum( Rtl_Ntk_t * p ) { return Vec_IntSize(&p->vConns)/2; }
105static inline int Rtl_NtkObjNum( Rtl_Ntk_t * p ) { return p->nInputs + p->nOutputs + Rtl_NtkCellNum(p) + Rtl_NtkConNum(p); }
106
107static inline int * Rtl_NtkWire( Rtl_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vWires, WIRE_NUM*i); }
108static inline int * Rtl_NtkCell( Rtl_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vStore, Vec_IntEntry(&p->vCells, i)); }
109static inline int * Rtl_NtkCon( Rtl_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vConns, 2*i); }
110
111static inline int Rtl_WireName( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i) >> 4; }
112static inline char * Rtl_WireNameStr( Rtl_Ntk_t * p, int i ) { return Rtl_NtkStr(p, Rtl_WireName(p, i)); }
113static inline int Rtl_WireFirst( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i); }
114static inline int Rtl_WireWidth( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i+1); }
115static inline int Rtl_WireOffset( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i+2); }
116static inline int Rtl_WireNumber( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i+3); }
117static inline int Rtl_WireBitStart( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vWires, WIRE_NUM*i+4); }
118static inline int Rtl_WireMapNameToId( Rtl_Ntk_t * p, int i ) { return Vec_IntEntry(p->pLib->vMap, i); }
119
120static inline int Rtl_CellType( int * pCell ) { return pCell[0]; }
121static inline int Rtl_CellName( int * pCell ) { return pCell[1]; }
122static inline int Rtl_CellModule( int * pCell ) { return pCell[2]; }
123static inline int Rtl_CellInputNum( int * pCell ) { return pCell[3]; }
124static inline int Rtl_CellOutputNum( int * pCell ) { return pCell[6]-pCell[3]; }
125static inline int Rtl_CellAttrNum( int * pCell ) { return pCell[4]; }
126static inline int Rtl_CellParamNum( int * pCell ) { return pCell[5]; }
127static inline int Rtl_CellConNum( int * pCell ) { return pCell[6]; }
128static inline int Rtl_CellMark( int * pCell ) { return pCell[7]; }
129static inline Rtl_Ntk_t * Rtl_CellNtk( Rtl_Ntk_t * p, int * pCell ) { return Rtl_CellModule(pCell) >= ABC_INFINITY ? Rtl_NtkModule(p, Rtl_CellModule(pCell)-ABC_INFINITY) : NULL; }
130
131static inline char * Rtl_CellTypeStr( Rtl_Ntk_t * p, int * pCell ) { return Rtl_NtkStr(p, Rtl_CellType(pCell)); }
132static inline char * Rtl_CellNameStr( Rtl_Ntk_t * p, int * pCell ) { return Rtl_NtkStr(p, Rtl_CellName(pCell)); }
133
134static inline int Rtl_SigIsNone( int s ) { return (s & 0x3) == 0; }
135static inline int Rtl_SigIsConst( int s ) { return (s & 0x3) == 1; }
136static inline int Rtl_SigIsSlice( int s ) { return (s & 0x3) == 2; }
137static inline int Rtl_SigIsConcat( int s ) { return (s & 0x3) == 3; }
138
139#define Rtl_NtkForEachAttr( p, Par, Val, i ) \
140 for ( i = 0; i < Rtl_NtkAttrNum(p) && (Par = Vec_IntEntry(&p->vAttrs, 2*i)) && (Val = Vec_IntEntry(&p->vAttrs, 2*i+1)); i++ )
141#define Rtl_NtkForEachWire( p, pWire, i ) \
142 for ( i = 0; i < Rtl_NtkWireNum(p) && (pWire = Vec_IntEntryP(&p->vWires, WIRE_NUM*i)); i++ )
143#define Rtl_NtkForEachCell( p, pCell, i ) \
144 for ( i = 0; i < Rtl_NtkCellNum(p) && (pCell = Rtl_NtkCell(p, i)); i++ )
145#define Rtl_NtkForEachCon( p, pCon, i ) \
146 for ( i = 0; i < Rtl_NtkConNum(p) && (pCon = Vec_IntEntryP(&p->vConns, 2*i)); i++ )
147
148#define Rtl_CellForEachAttr( p, pCell, Par, Val, i ) \
149 for ( i = 0; i < pCell[4] && (Par = pCell[CELL_NUM+2*i]) && (Val = pCell[CELL_NUM+2*i+1]); i++ )
150#define Rtl_CellForEachParam( p, pCell, Par, Val, i ) \
151 for ( i = 0; i < pCell[5] && (Par = pCell[CELL_NUM+2*(pCell[4]+i)]) && (Val = pCell[CELL_NUM+2*(pCell[4]+i)+1]); i++ )
152#define Rtl_CellForEachConnect( p, pCell, Par, Val, i ) \
153 for ( i = 0; i < pCell[6] && (Par = pCell[CELL_NUM+2*(pCell[4]+pCell[5]+i)]) && (Val = pCell[CELL_NUM+2*(pCell[4]+pCell[5]+i)+1]); i++ )
154
155#define Rtl_CellForEachInput( p, pCell, Par, Val, i ) \
156 Rtl_CellForEachConnect( p, pCell, Par, Val, i ) if ( i >= Rtl_CellInputNum(pCell) ) continue; else
157#define Rtl_CellForEachOutput( p, pCell, Par, Val, i ) \
158 Rtl_CellForEachConnect( p, pCell, Par, Val, i ) if ( i < Rtl_CellInputNum(pCell) ) continue; else
159
160extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
161extern int Abc_NtkFromGiaCollapse( Gia_Man_t * pGia );
162extern int Wln_ReadFindToken( char * pToken, Abc_Nam_t * p );
163
167
179Rtl_Ntk_t * Rtl_NtkAlloc( Rtl_Lib_t * pLib )
180{
181 Rtl_Ntk_t * p = ABC_CALLOC( Rtl_Ntk_t, 1 );
182 Vec_IntGrow( &p->vWires, 4 );
183 Vec_IntGrow( &p->vCells, 4 );
184 Vec_IntGrow( &p->vConns, 4 );
185 Vec_IntGrow( &p->vStore, 8 );
186 Vec_IntGrow( &p->vAttrs, 8 );
187 Vec_PtrPush( pLib->vNtks, (void *)p );
188 p->pLib = pLib;
189 return p;
190}
191void Rtl_NtkFree( Rtl_Ntk_t * p )
192{
193 Gia_ManStopP( &p->pGia );
194 ABC_FREE( p->vWires.pArray );
195 ABC_FREE( p->vCells.pArray );
196 ABC_FREE( p->vConns.pArray );
197 ABC_FREE( p->vStore.pArray );
198 ABC_FREE( p->vAttrs.pArray );
199 ABC_FREE( p->vOrder.pArray );
200 ABC_FREE( p->vLits.pArray );
201 ABC_FREE( p->vDrivers.pArray );
202 ABC_FREE( p->vBitTemp.pArray );
203 ABC_FREE( p->vBitTemp2.pArray );
204 ABC_FREE( p );
205}
206void Rtl_NtkCountPio( Rtl_Ntk_t * p, int Counts[4] )
207{
208 int i, * pWire;
209 Rtl_NtkForEachWire( p, pWire, i )
210 {
211 if ( pWire[0] & 1 ) // PI
212 Counts[0]++, Counts[1] += pWire[1];
213 if ( pWire[0] & 2 ) // PO
214 Counts[2]++, Counts[3] += pWire[1];
215 }
216 assert( p->nInputs == Counts[0] );
217 assert( p->nOutputs == Counts[2] );
218}
219void Rtl_NtkPrintOpers( Rtl_Ntk_t * p )
220{
221 int i, * pCell, nBlack = 0, nUser = 0, Counts[ABC_OPER_LAST] = {0};
222 if ( Rtl_NtkCellNum(p) == 0 )
223 return;
224 Rtl_NtkForEachCell( p, pCell, i )
225 if ( Rtl_CellModule(pCell) < ABC_OPER_LAST )
226 Counts[Rtl_CellModule(pCell)]++;
227 else if ( Rtl_CellModule(pCell) == ABC_OPER_LAST-1 )
228 nBlack++;
229 else
230 nUser++;
231 printf( "There are %d instances in this network:\n", Rtl_NtkCellNum(p) );
232 if ( nBlack )
233 printf( " %s (%d)", "blackbox", nBlack );
234 if ( nUser )
235 printf( " %s (%d)", "user", nUser );
236 for ( i = 0; i < ABC_OPER_LAST; i++ )
237 if ( Counts[i] )
238 printf( " %s (%d)", Abc_OperName(i), Counts[i] );
239 printf( "\n" );
240}
241void Rtl_NtkPrintStats( Rtl_Ntk_t * p, int nNameSymbs )
242{
243 int Counts[4] = {0}; Rtl_NtkCountPio( p, Counts );
244 printf( "%*s : ", nNameSymbs, Rtl_NtkName(p) );
245 printf( "PI = %5d (%5d) ", Counts[0], Counts[1] );
246 printf( "PO = %5d (%5d) ", Counts[2], Counts[3] );
247 printf( "Wire = %6d ", Rtl_NtkWireNum(p) );
248 printf( "Cell = %6d ", Rtl_NtkCellNum(p) );
249 printf( "Con = %6d", Rtl_NtkConNum(p) );
250 printf( "\n" );
251 //Rtl_NtkPrintOpers( p );
252}
253
265void Rtl_NtkPrintHieStats( Rtl_Ntk_t * p, int nOffset )
266{
267 Vec_Int_t * vFound = Vec_IntAlloc( 100 );
268 int i, * pCell;
269 for ( i = 0; i < 5*(nOffset-1); i++ )
270 printf( " " );
271 if ( nOffset )
272 printf( "|--> " );
273 printf( "%s\n", Rtl_NtkName(p) );
274 Rtl_NtkForEachCell( p, pCell, i )
275 if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
276 {
277 Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
278 assert( pCell[6] == pModel->nInputs+pModel->nOutputs );
279 if ( Vec_IntFind(vFound, pModel->NameId) >= 0 )
280 continue;
281 Vec_IntPush( vFound, pModel->NameId );
282 Rtl_NtkPrintHieStats( pModel, nOffset+1 );
283 }
284 Vec_IntFree( vFound );
285}
286void Rtl_LibPrintHieStats( Rtl_Lib_t * p )
287{
288 Rtl_Ntk_t * pNtk; int i;
289 printf( "Hierarchy found in \"%s\":\n", p->pSpec );
290 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
291 {
292 printf( "\n" );
293 printf( "MODULE %d: ", i );
294 Rtl_NtkPrintHieStats( pNtk, 0 );
295 }
296}
297
309Rtl_Lib_t * Rtl_LibAlloc()
310{
311 Rtl_Lib_t * p = ABC_CALLOC( Rtl_Lib_t, 1 );
312 p->vNtks = Vec_PtrAlloc( 100 );
313 Vec_IntGrow( &p->vConsts, 1000 );
314 Vec_IntGrow( &p->vSlices, 1000 );
315 Vec_IntGrow( &p->vConcats, 1000 );
316 return p;
317}
318void Rtl_LibFree( Rtl_Lib_t * p )
319{
320 Rtl_Ntk_t * pNtk; int i;
321 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
322 Rtl_NtkFree( pNtk );
323 ABC_FREE( p->vConsts.pArray );
324 ABC_FREE( p->vSlices.pArray );
325 ABC_FREE( p->vConcats.pArray );
326 ABC_FREE( p->vAttrTemp.pArray );
327 for ( i = 0; i < TEMP_NUM; i++ )
328 ABC_FREE( p->vTemp[i].pArray );
329 Vec_IntFreeP( &p->vMap );
330 Vec_IntFreeP( &p->vDirects );
331 Vec_IntFreeP( &p->vInverses );
332 Vec_IntFreeP( &p->vTokens );
333 Abc_NamStop( p->pManName );
334 Vec_PtrFree( p->vNtks );
335 ABC_FREE( p->pSpec );
336 ABC_FREE( p );
337}
338int Rtl_LibFindModule( Rtl_Lib_t * p, int NameId )
339{
340 Rtl_Ntk_t * pNtk; int i;
341 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
342 if ( pNtk->NameId == NameId )
343 return i;
344 return -1;
345}
346int Rtl_LibFindModule2( Rtl_Lib_t * p, int NameId, int iNtk0 )
347{
348 char * pName = Rtl_LibStr( p, NameId );
349 Rtl_Ntk_t * pNtk0 = Rtl_LibNtk( p, iNtk0 );
350 Rtl_Ntk_t * pNtk; int i;
351 int Counts0[4] = {0}; Rtl_NtkCountPio( pNtk0, Counts0 );
352 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
353 if ( strstr(Rtl_NtkName(pNtk), pName+1) )
354 {
355 int Counts[4] = {0}; Rtl_NtkCountPio( pNtk, Counts );
356 if ( Counts[1] == Counts0[1] && Counts[3] == Counts0[3] )
357 return i;
358 }
359 return -1;
360}
361int Rtl_LibFindTwoModules( Rtl_Lib_t * p, int Name1, int Name2 )
362{
363 int iNtk1 = Rtl_LibFindModule( p, Name1 );
364 if ( Name2 == -1 )
365 return (iNtk1 << 16) | iNtk1;
366 else if ( iNtk1 == -1 )
367 return -1;
368 else
369 {
370 int Counts1[4] = {0}, Counts2[4] = {0};
371 int iNtk2 = Rtl_LibFindModule( p, Name2 );
372 if ( iNtk2 == -1 )
373 return -1;
374 else
375 {
376 Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
377 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
378 Rtl_NtkCountPio( pNtk1, Counts1 );
379 Rtl_NtkCountPio( pNtk2, Counts2 );
380 if ( Counts1[1] != Counts2[1] || Counts1[3] != Counts2[3] )
381 iNtk1 = Rtl_LibFindModule2( p, Name1, iNtk2 );
382 return (iNtk1 << 16) | iNtk2;
383 }
384 }
385}
386void Rtl_LibPrintStats( Rtl_Lib_t * p )
387{
388 Rtl_Ntk_t * pNtk; int i, nSymbs = 0;
389 printf( "Modules found in \"%s\":\n", p->pSpec );
390 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
391 nSymbs = Abc_MaxInt( nSymbs, strlen(Rtl_NtkName(pNtk)) );
392 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
393 Rtl_NtkPrintStats( pNtk, nSymbs + 2 );
394}
395
396
408typedef enum {
409 RTL_NONE = 0, // 0: unused
410 RTL_MODULE, // 1: "module"
411 RTL_END, // 2: "end"
412 RTL_INPUT, // 3: "input"
413 RTL_OUTPUT, // 4: "output"
414 RTL_INOUT, // 5: "inout"
415 RTL_UPTO, // 6: "upto"
416 RTL_SIGNED, // 7: "signed"
417 RTL_OFFSET, // 8: "offset"
418 RTL_PARAMETER, // 9: "parameter"
419 RTL_WIRE, // 10: "wire"
420 RTL_CONNECT, // 11: "connect"
421 RTL_CELL, // 12: "cell"
422 RTL_WIDTH, // 13: "width"
423 RTL_ATTRIBUTE, // 14: "attribute"
424 RTL_UNUSED // 15: unused
425} Rtl_Type_t;
426
427static inline char * Rtl_Num2Name( int i )
428{
429 if ( i == 1 ) return "module";
430 if ( i == 2 ) return "end";
431 if ( i == 3 ) return "input";
432 if ( i == 4 ) return "output";
433 if ( i == 5 ) return "inout";
434 if ( i == 6 ) return "upto";
435 if ( i == 7 ) return "signed";
436 if ( i == 8 ) return "offset";
437 if ( i == 9 ) return "parameter";
438 if ( i == 10 ) return "wire";
439 if ( i == 11 ) return "connect";
440 if ( i == 12 ) return "cell";
441 if ( i == 13 ) return "width";
442 if ( i == 14 ) return "attribute";
443 return NULL;
444}
445
446static inline void Rtl_LibDeriveMap( Rtl_Lib_t * p )
447{
448 int i;
449 p->pMap[0] = -1;
450 for ( i = 1; i < RTL_UNUSED; i++ )
451 p->pMap[i] = Abc_NamStrFind( p->pManName, Rtl_Num2Name(i) );
452}
453
454
455
467int Rtl_LibReadType( char * pType )
468{
469 if ( !strcmp(pType, "$not") ) return ABC_OPER_BIT_INV; // Y = ~A $not
470 if ( !strcmp(pType, "$pos") ) return ABC_OPER_BIT_BUF; // Y = +A $pos
471 if ( !strcmp(pType, "$neg") ) return ABC_OPER_ARI_MIN; // Y = -A $neg
472 if ( !strcmp(pType, "$reduce_and") ) return ABC_OPER_RED_AND; // Y = &A $reduce_and
473 if ( !strcmp(pType, "$reduce_or") ) return ABC_OPER_RED_OR; // Y = |A $reduce_or
474 if ( !strcmp(pType, "$reduce_xor") ) return ABC_OPER_RED_XOR; // Y = ^A $reduce_xor
475 if ( !strcmp(pType, "$reduce_xnor") ) return ABC_OPER_RED_NXOR; // Y = ~^A $reduce_xnor
476 if ( !strcmp(pType, "$reduce_bool") ) return ABC_OPER_RED_OR; // Y = |A $reduce_bool
477 if ( !strcmp(pType, "$logic_not") ) return ABC_OPER_LOGIC_NOT; // Y = !A $logic_not
478
479 if ( !strcmp(pType, "$and") ) return ABC_OPER_BIT_AND; // Y = A & B $and
480 if ( !strcmp(pType, "$or") ) return ABC_OPER_BIT_OR; // Y = A | B $or
481 if ( !strcmp(pType, "$xor") ) return ABC_OPER_BIT_XOR; // Y = A ^ B $xor
482 if ( !strcmp(pType, "$xnor") ) return ABC_OPER_BIT_NXOR; // Y = A ~^ B $xnor
483
484 if ( !strcmp(pType, "$shl") ) return ABC_OPER_SHIFT_L; // Y = A << B $shl
485 if ( !strcmp(pType, "$shr") ) return ABC_OPER_SHIFT_R; // Y = A >> B $shr
486 if ( !strcmp(pType, "$sshl") ) return ABC_OPER_SHIFT_LA; // Y = A <<< B $sshl
487 if ( !strcmp(pType, "$sshr") ) return ABC_OPER_SHIFT_RA; // Y = A >>> B $sshr
488
489 if ( !strcmp(pType, "$shiftx") ) return ABC_OPER_SHIFT_R; // Y = A << B $shl <== temporary
490
491 if ( !strcmp(pType, "$logic_and") ) return ABC_OPER_LOGIC_AND; // Y = A && B $logic_and
492 if ( !strcmp(pType, "$logic_or") ) return ABC_OPER_LOGIC_OR; // Y = A || B $logic_or
493
494 if ( !strcmp(pType, "$lt") ) return ABC_OPER_COMP_LESS; // Y = A < B $lt
495 if ( !strcmp(pType, "$le") ) return ABC_OPER_COMP_LESSEQU; // Y = A <= B $le
496 if ( !strcmp(pType, "$ge") ) return ABC_OPER_COMP_MOREEQU; // Y = A >= B $ge
497 if ( !strcmp(pType, "$gt") ) return ABC_OPER_COMP_MORE; // Y = A > B $gt
498 if ( !strcmp(pType, "$eq") ) return ABC_OPER_COMP_EQU; // Y = A == B $eq
499 if ( !strcmp(pType, "$ne") ) return ABC_OPER_COMP_NOTEQU; // Y = A != B $ne
500 if ( !strcmp(pType, "$eqx") ) return ABC_OPER_COMP_EQU; // Y = A === B $eqx
501 if ( !strcmp(pType, "$nex") ) return ABC_OPER_COMP_NOTEQU; // Y = A !== B $nex
502
503 if ( !strcmp(pType, "$add") ) return ABC_OPER_ARI_ADD; // Y = A + B $add
504 if ( !strcmp(pType, "$sub") ) return ABC_OPER_ARI_SUB; // Y = A - B $sub
505 if ( !strcmp(pType, "$mul") ) return ABC_OPER_ARI_MUL; // Y = A * B $mul
506 if ( !strcmp(pType, "$div") ) return ABC_OPER_ARI_DIV; // Y = A / B $div
507 if ( !strcmp(pType, "$mod") ) return ABC_OPER_ARI_MOD; // Y = A % B $mod
508 if ( !strcmp(pType, "$pow") ) return ABC_OPER_ARI_POW; // Y = A ** B $pow
509
510 if ( !strcmp(pType, "$modfoor") ) return ABC_OPER_NONE; // [N/A] $modfoor
511 if ( !strcmp(pType, "$divfloor") ) return ABC_OPER_NONE; // [N/A] $divfloor
512
513 if ( !strcmp(pType, "$mux") ) return ABC_OPER_SEL_NMUX; // $mux
514 if ( !strcmp(pType, "$pmux") ) return ABC_OPER_SEL_SEL; // $pmux
515
516 if ( !strcmp(pType, "$dff") ) return ABC_OPER_DFF;
517 if ( !strcmp(pType, "$adff") ) return ABC_OPER_DFF;
518 if ( !strcmp(pType, "$sdff") ) return ABC_OPER_DFF;
519 assert( 0 );
520 return -1;
521}
522int Rtl_NtkReadType( Rtl_Ntk_t * p, int Type )
523{
524 extern int Rtl_LibFindModule( Rtl_Lib_t * p, int NameId );
525 char * pType = Rtl_NtkStr( p, Type );
526 if ( pType[0] == '$' && strncmp(pType,"$paramod",strlen("$paramod")) )
527 return Rtl_LibReadType( pType );
528 return ABC_INFINITY + Rtl_LibFindModule( p->pLib, Type );
529}
530
542int Rtl_NtkRangeWires( Rtl_Ntk_t * p )
543{
544 int i, * pWire, nBits = 0;
545 Rtl_NtkForEachWire( p, pWire, i )
546 {
547 //printf( "%s -> %d\n", Rtl_WireNameStr(p, i), nBits );
548 pWire[4] = nBits, nBits += Rtl_WireWidth(p, i);
549 }
550 return nBits;
551}
552void Rtl_NtkMapWires( Rtl_Ntk_t * p, int fUnmap )
553{
554 int i, Value;
555 assert( Vec_IntSize(p->pLib->vMap) == Abc_NamObjNumMax(p->pLib->pManName) );
556 for ( i = 0; i < Rtl_NtkWireNum(p); i++ )
557 {
558 int NameId = Rtl_WireName( p, i );
559 assert( Vec_IntEntry(p->pLib->vMap, NameId) == (fUnmap ? i : -1) );
560 Vec_IntWriteEntry( p->pLib->vMap, NameId, fUnmap ? -1 : i );
561 }
562 if ( fUnmap )
563 Vec_IntForEachEntry( p->pLib->vMap, Value, i )
564 assert( Value == -1 );
565}
566void Rtl_NtkNormRanges( Rtl_Ntk_t * p )
567{
568 int i, * pWire;
569 Rtl_NtkMapWires( p, 0 );
570 for ( i = p->Slice0; i < p->Slice1; i += 3 )
571 {
572 int NameId = Vec_IntEntry( &p->pLib->vSlices, i );
573 int Left = Vec_IntEntry( &p->pLib->vSlices, i+1 );
574 int Right = Vec_IntEntry( &p->pLib->vSlices, i+2 );
575 int Wire = Rtl_WireMapNameToId( p, NameId );
576 int Offset = Rtl_WireOffset( p, Wire );
577 int First = Rtl_WireFirst( p, Wire );
578 assert( First >> 4 == NameId );
579 if ( Offset )
580 {
581 Left -= Offset;
582 Right -= Offset;
583 }
584 if ( First & 8 ) // upto
585 {
586 Vec_IntWriteEntry( &p->pLib->vSlices, i+1, Right );
587 Vec_IntWriteEntry( &p->pLib->vSlices, i+2, Left );
588 }
589 }
590 Rtl_NtkForEachWire( p, pWire, i )
591 {
592 Vec_IntWriteEntry( &p->vWires, WIRE_NUM*i+0, Rtl_WireFirst(p, i) & ~0x8 ); // upto
593 Vec_IntWriteEntry( &p->vWires, WIRE_NUM*i+2, 0 ); // offset
594 }
595 Rtl_NtkMapWires( p, 1 );
596}
597void Rtl_LibNormRanges( Rtl_Lib_t * pLib )
598{
599 Rtl_Ntk_t * p; int i;
600 if ( pLib->vMap == NULL )
601 pLib->vMap = Vec_IntStartFull( Abc_NamObjNumMax(pLib->pManName) );
602 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
603 Rtl_NtkNormRanges( p );
604}
605
606
618int * Rlt_NtkFindIOPerm( Rtl_Ntk_t * p )
619{
620 Vec_Int_t * vCost = Vec_IntAlloc( 100 );
621 int i, * pWire, * pPerm = NULL, Count = 0;
622 Rtl_NtkForEachWire( p, pWire, i )
623 {
624 int First = Rtl_WireFirst( p, i );
625 int Number = Rtl_WireNumber( p, i );
626 int fIsPi = (int)((First & 1) > 0);
627 int fIsPo = (int)((First & 2) > 0);
628 assert( (fIsPi || fIsPo) == (Number > 0) );
629 if ( fIsPi || fIsPo )
630 Vec_IntPush( vCost, fIsPo*ABC_INFINITY + Number );
631 else
632 Vec_IntPush( vCost, 2*ABC_INFINITY + Count++ );
633 }
634 pPerm = Abc_MergeSortCost( Vec_IntArray(vCost), Vec_IntSize(vCost) );
635 Vec_IntFree( vCost );
636 return pPerm;
637}
638void Rtl_NtkOrderWires( Rtl_Ntk_t * p )
639{
640 Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(&p->vWires) );
641 int i, k, * pWire, * pPerm = Rlt_NtkFindIOPerm( p );
642 Rtl_NtkForEachWire( p, pWire, i )
643 {
644 pWire = Vec_IntEntryP( &p->vWires, WIRE_NUM*pPerm[i] );
645 for ( k = 0; k < WIRE_NUM; k++ )
646 Vec_IntPush( vTemp, pWire[k] );
647 }
648 ABC_FREE( pPerm );
649 assert( Vec_IntSize(&p->vWires) == Vec_IntSize(vTemp) );
650 ABC_SWAP( Vec_Int_t, p->vWires, *vTemp );
651 Vec_IntFree( vTemp );
652}
653void Rtl_LibUpdateInstances( Rtl_Ntk_t * p )
654{
655 Vec_Int_t * vMap = p->pLib->vMap;
656 Vec_Int_t * vTemp = &p->pLib->vTemp[2];
657 int i, k, Par, Val, * pCell, Value;
658 Rtl_NtkForEachCell( p, pCell, i )
659 if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
660 {
661 Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
662 assert( pCell[6] == pModel->nInputs+pModel->nOutputs );
663 Rtl_CellForEachConnect( p, pCell, Par, Val, k )
664 Vec_IntWriteEntry( vMap, Par >> 2, k );
665 Vec_IntClear( vTemp );
666 for ( k = 0; k < pCell[6]; k++ )
667 {
668 int Perm = Vec_IntEntry( vMap, Rtl_WireName(pModel, k) );
669 int Par = pCell[CELL_NUM+2*(pCell[4]+pCell[5]+Perm)];
670 int Val = pCell[CELL_NUM+2*(pCell[4]+pCell[5]+Perm)+1];
671 assert( (Par >> 2) == Rtl_WireName(pModel, k) );
672 Vec_IntWriteEntry( vMap, Par >> 2, -1 );
673 Vec_IntPushTwo( vTemp, Par, Val );
674 assert( Perm >= 0 );
675 }
676 memcpy( pCell+CELL_NUM+2*(pCell[4]+pCell[5]), Vec_IntArray(vTemp), sizeof(int)*Vec_IntSize(vTemp) );
677 }
678 Vec_IntForEachEntry( p->pLib->vMap, Value, i )
679 assert( Value == -1 );
680}
681void Rtl_LibOrderWires( Rtl_Lib_t * pLib )
682{
683 Rtl_Ntk_t * p; int i;
684 if ( pLib->vMap == NULL )
685 pLib->vMap = Vec_IntStartFull( Abc_NamObjNumMax(pLib->pManName) );
686 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
687 Rtl_NtkOrderWires( p );
688 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
689 Rtl_LibUpdateInstances( p );
690}
691
692
704extern int Rtl_NtkCountSignalRange( Rtl_Ntk_t * p, int Sig );
705
706int Rtl_NtkCountWireRange( Rtl_Ntk_t * p, int NameId )
707{
708 int Wire = Rtl_WireMapNameToId( p, NameId );
709 int Width = Rtl_WireWidth( p, Wire );
710 return Width;
711}
712int Rtl_NtkCountSliceRange( Rtl_Ntk_t * p, int * pSlice )
713{
714 return pSlice[1] - pSlice[2] + 1;
715}
716int Rtl_NtkCountConcatRange( Rtl_Ntk_t * p, int * pConcat )
717{
718 int i, nBits = 0;
719 for ( i = 1; i <= pConcat[0]; i++ )
720 nBits += Rtl_NtkCountSignalRange( p, pConcat[i] );
721 return nBits;
722}
723int Rtl_NtkCountSignalRange( Rtl_Ntk_t * p, int Sig )
724{
725 if ( Rtl_SigIsNone(Sig) )
726 return Rtl_NtkCountWireRange( p, Sig >> 2 );
727 if ( Rtl_SigIsSlice(Sig) )
728 return Rtl_NtkCountSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
729 if ( Rtl_SigIsConcat(Sig) )
730 return Rtl_NtkCountConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
731 if ( Rtl_SigIsConst(Sig) )
732 assert( 0 );
733 return ABC_INFINITY;
734}
735
747extern int Rtl_NtkCheckSignalRange( Rtl_Ntk_t * p, int Sig );
748
749int Rtl_NtkCheckWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right )
750{
751 int Wire = Rtl_WireMapNameToId( p, NameId );
752 int First = Rtl_WireBitStart( p, Wire );
753 int Width = Rtl_WireWidth( p, Wire ), i;
754 Left = Left == -1 ? Width-1 : Left;
755 Right = Right == -1 ? 0 : Right;
756 assert ( Right <= Left && Right >= 0 );
757 for ( i = Right; i <= Left; i++ )
758 if ( Vec_IntEntry(&p->vLits, First+i) == -1 )
759 return 0;
760 return 1;
761}
762int Rtl_NtkCheckSliceRange( Rtl_Ntk_t * p, int * pSlice )
763{
764 return Rtl_NtkCheckWireRange( p, pSlice[0], pSlice[1], pSlice[2] );
765}
766int Rtl_NtkCheckConcatRange( Rtl_Ntk_t * p, int * pConcat )
767{
768 int i;
769 for ( i = 1; i <= pConcat[0]; i++ )
770 if ( !Rtl_NtkCheckSignalRange( p, pConcat[i] ) )
771 return 0;
772 return 1;
773}
774int Rtl_NtkCheckSignalRange( Rtl_Ntk_t * p, int Sig )
775{
776 if ( Rtl_SigIsNone(Sig) )
777 return Rtl_NtkCheckWireRange( p, Sig >> 2, -1, -1 );
778 else if ( Rtl_SigIsConst(Sig) )
779 return 1;
780 else if ( Rtl_SigIsSlice(Sig) )
781 return Rtl_NtkCheckSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
782 else if ( Rtl_SigIsConcat(Sig) )
783 return Rtl_NtkCheckConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
784 else assert( 0 );
785 return -1;
786}
787
788
789extern void Rtl_NtkSetSignalRange( Rtl_Ntk_t * p, int Sig, int Value );
790
791void Rtl_NtkSetWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right, int Value )
792{
793 //char * pName = Rtl_NtkStr( p, NameId );
794 int Wire = Rtl_WireMapNameToId( p, NameId );
795 int First = Rtl_WireBitStart( p, Wire );
796 int Width = Rtl_WireWidth( p, Wire ), i;
797 Left = Left == -1 ? Width-1 : Left;
798 Right = Right == -1 ? 0 : Right;
799 assert ( Right <= Left && Right >= 0 );
800 for ( i = Right; i <= Left; i++ )
801 {
802 assert( Vec_IntEntry(&p->vLits, First+i) == -1 );
803 Vec_IntWriteEntry(&p->vLits, First+i, Value );
804 }
805 //printf( "Finished setting wire %s\n", Rtl_NtkStr(p, NameId) );
806}
807void Rtl_NtkSetSliceRange( Rtl_Ntk_t * p, int * pSlice, int Value )
808{
809 Rtl_NtkSetWireRange( p, pSlice[0], pSlice[1], pSlice[2], Value );
810}
811void Rtl_NtkSetConcatRange( Rtl_Ntk_t * p, int * pConcat, int Value )
812{
813 int i;
814 for ( i = 1; i <= pConcat[0]; i++ )
815 Rtl_NtkSetSignalRange( p, pConcat[i], Value );
816}
817void Rtl_NtkSetSignalRange( Rtl_Ntk_t * p, int Sig, int Value )
818{
819 if ( Rtl_SigIsNone(Sig) )
820 Rtl_NtkSetWireRange( p, Sig >> 2, -1, -1, Value );
821 else if ( Rtl_SigIsSlice(Sig) )
822 Rtl_NtkSetSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2), Value );
823 else if ( Rtl_SigIsConcat(Sig) )
824 Rtl_NtkSetConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2), Value );
825 else if ( Rtl_SigIsConst(Sig) )
826 assert( 0 );
827}
828
829
830void Rtl_NtkInitInputs( Rtl_Ntk_t * p )
831{
832 int b, i;
833 for ( i = 0; i < p->nInputs; i++ )
834 {
835 int First = Rtl_WireBitStart( p, i );
836 int Width = Rtl_WireWidth( p, i );
837 for ( b = 0; b < Width; b++ )
838 {
839 assert( Vec_IntEntry(&p->vLits, First+b) == -1 );
840 Vec_IntWriteEntry( &p->vLits, First+b, Vec_IntSize(&p->vOrder) );
841 }
842 Vec_IntPush( &p->vOrder, i );
843 //printf( "Finished setting input %s\n", Rtl_WireNameStr(p, i) );
844 }
845}
846Vec_Int_t * Rtl_NtkCollectOutputs( Rtl_Ntk_t * p )
847{
848 //char * pNtkName = Rtl_NtkName(p);
849 int b, i;
850 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
851 for ( i = 0; i < p->nOutputs; i++ )
852 {
853 //char * pName = Rtl_WireNameStr(p, p->nInputs + i);
854 int First = Rtl_WireBitStart( p, p->nInputs + i );
855 int Width = Rtl_WireWidth( p, p->nInputs + i );
856 for ( b = 0; b < Width; b++ )
857 {
858 assert( Vec_IntEntry(&p->vLits, First+b) != -1 );
859 Vec_IntPush( vRes, Vec_IntEntry(&p->vLits, First+b) );
860 }
861 }
862 return vRes;
863}
864int Rtl_NtkReviewCells( Rtl_Ntk_t * p )
865{
866 int i, k, Par, Val, * pCell, RetValue = 0;
867 Rtl_NtkForEachCell( p, pCell, i )
868 {
869 if ( pCell[7] )
870 continue;
871 Rtl_CellForEachInput( p, pCell, Par, Val, k )
872 if ( !Rtl_NtkCheckSignalRange( p, Val ) )
873 break;
874 if ( k < Rtl_CellInputNum(pCell) )
875 continue;
876 Rtl_CellForEachOutput( p, pCell, Par, Val, k )
877 Rtl_NtkSetSignalRange( p, Val, Vec_IntSize(&p->vOrder) );
878 Vec_IntPush( &p->vOrder, p->nInputs + i );
879 pCell[7] = 1;
880 RetValue = 1;
881 //printf( "Setting cell %s as propagated.\n", Rtl_CellNameStr(p, pCell) );
882 }
883 return RetValue;
884}
885int Rtl_NtkReviewConnections( Rtl_Ntk_t * p )
886{
887 int i, * pCon, RetValue = 0;
888 Rtl_NtkForEachCon( p, pCon, i )
889 {
890 int Status0 = Rtl_NtkCheckSignalRange( p, pCon[0] );
891 int Status1 = Rtl_NtkCheckSignalRange( p, pCon[1] );
892 if ( Status0 == Status1 )
893 continue;
894 if ( !Status0 && Status1 )
895 ABC_SWAP( int, pCon[0], pCon[1] )
896 Rtl_NtkSetSignalRange( p, pCon[1], Vec_IntSize(&p->vOrder) );
897 Vec_IntPush( &p->vOrder, p->nInputs + Rtl_NtkCellNum(p) + i );
898 RetValue = 1;
899 }
900 return RetValue;
901}
902void Rtl_NtkPrintCellOrder( Rtl_Ntk_t * p )
903{
904 int i, iCell;
905 Vec_IntForEachEntry( &p->vOrder, iCell, i )
906 {
907 printf( "%4d : ", i );
908 printf( "Cell %4d ", iCell );
909 if ( iCell < p->nInputs )
910 printf( "Type Input " );
911 else if ( iCell < p->nInputs + Rtl_NtkCellNum(p) )
912 {
913 int * pCell = Rtl_NtkCell( p, iCell - p->nInputs );
914 printf( "Type %4d ", Rtl_CellType(pCell) );
915 printf( "%16s ", Rtl_CellTypeStr(p, pCell) );
916 printf( "%16s ", Rtl_CellNameStr(p, pCell) );
917 }
918 else
919 printf( "Type Connection " );
920 printf( "\n" );
921 }
922}
923void Rtl_NtkPrintUnusedCells( Rtl_Ntk_t * p )
924{
925 int i, * pCell;
926 printf( "\n*** Printing unused cells:\n" );
927 Rtl_NtkForEachCell( p, pCell, i )
928 {
929 if ( pCell[7] )
930 continue;
931 printf( "Unused cell %s %s\n", Rtl_CellTypeStr(p, pCell), Rtl_CellNameStr(p, pCell) );
932 }
933 printf( "\n" );
934}
935void Rtl_NtkOrderCells( Rtl_Ntk_t * p )
936{
937 Vec_Int_t * vRes;
938 int nBits = Rtl_NtkRangeWires( p );
939 Vec_IntFill( &p->vLits, nBits, -1 );
940
941 Vec_IntClear( &p->vOrder );
942 Vec_IntGrow( &p->vOrder, Rtl_NtkObjNum(p) );
943 Rtl_NtkInitInputs( p );
944
945 Rtl_NtkMapWires( p, 0 );
946//Vec_IntPrint(&p->vLits);
947
948 Rtl_NtkReviewConnections( p );
949 while ( Rtl_NtkReviewCells(p) | Rtl_NtkReviewConnections(p) );
950 Rtl_NtkMapWires( p, 1 );
951
952 vRes = Rtl_NtkCollectOutputs( p );
953 Vec_IntFree( vRes );
954
955 //Rtl_NtkPrintCellOrder( p );
956}
957void Rtl_LibOrderCells( Rtl_Lib_t * pLib )
958{
959 Rtl_Ntk_t * p; int i;
960 if ( pLib->vMap == NULL )
961 pLib->vMap = Vec_IntStartFull( Abc_NamObjNumMax(pLib->pManName) );
962 assert( Vec_IntSize(pLib->vMap) == Abc_NamObjNumMax(pLib->pManName) );
963 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
964 Rtl_NtkOrderCells( p );
965}
966
967
979void Rtl_TokenUnspace( char * p )
980{
981 int i, Length = strlen(p), Quote = 0;
982 for ( i = 0; i < Length; i++ )
983 if ( p[i] == '\"' )
984 Quote ^= 1;
985 else if ( Quote && p[i] == ' ' )
986 p[i] = '\"';
987}
988void Rtl_TokenRespace( char * p )
989{
990 int i, Length = strlen(p);
991 assert( p[0] == '\"' && p[Length-1] == '\"' );
992 for ( i = 1; i < Length-1; i++ )
993 if ( p[i] == '\"' )
994 p[i] = ' ';
995}
996Vec_Int_t * Rtl_NtkReadFile( char * pFileName, Abc_Nam_t * p )
997{
998 Vec_Int_t * vTokens;
999 char * pTemp, * pBuffer;
1000 FILE * pFile = fopen( pFileName, "rb" );
1001 if ( pFile == NULL )
1002 {
1003 printf( "Cannot open file \"%s\" for reading.\n", pFileName );
1004 return NULL;
1005 }
1006 pBuffer = ABC_ALLOC( char, MAX_LINE );
1007 Abc_NamStrFindOrAdd( p, "module", NULL );
1008 assert( Abc_NamObjNumMax(p) == 2 );
1009 vTokens = Vec_IntAlloc( 1000 );
1010 while ( fgets( pBuffer, MAX_LINE, pFile ) != NULL )
1011 {
1012 if ( pBuffer[0] == '#' )
1013 continue;
1014 Rtl_TokenUnspace( pBuffer );
1015 pTemp = strtok( pBuffer, " \t\r\n" );
1016 if ( pTemp == NULL )
1017 continue;
1018 while ( pTemp )
1019 {
1020 if ( *pTemp == '\"' ) Rtl_TokenRespace( pTemp );
1021 Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pTemp, NULL) );
1022 pTemp = strtok( NULL, " \t\r\n" );
1023 }
1024 Vec_IntPush( vTokens, -1 );
1025 }
1026 ABC_FREE( pBuffer );
1027 fclose( pFile );
1028 return vTokens;
1029}
1030
1031
1032
1033
1045extern void Rtl_NtkPrintSig( Rtl_Ntk_t * p, int Sig );
1046
1047void Rtl_NtkPrintConst( Rtl_Ntk_t * p, int * pConst )
1048{
1049 int i;
1050 if ( pConst[0] == -1 )
1051 {
1052 fprintf( Rtl_NtkFile(p), " %d", pConst[1] );
1053 return;
1054 }
1055 fprintf( Rtl_NtkFile(p), " %d\'", pConst[0] );
1056 for ( i = pConst[0] - 1; i >= 0; i-- )
1057 fprintf( Rtl_NtkFile(p), "%d", Abc_InfoHasBit((unsigned *)pConst+1,i) );
1058}
1059void Rtl_NtkPrintSlice( Rtl_Ntk_t * p, int * pSlice )
1060{
1061 fprintf( Rtl_NtkFile(p), " %s", Rtl_NtkStr(p, pSlice[0]) );
1062 if ( pSlice[1] == pSlice[2] )
1063 fprintf( Rtl_NtkFile(p), " [%d]", pSlice[1] );
1064 else
1065 fprintf( Rtl_NtkFile(p), " [%d:%d]", pSlice[1], pSlice[2] );
1066}
1067void Rtl_NtkPrintConcat( Rtl_Ntk_t * p, int * pConcat )
1068{
1069 int i;
1070 fprintf( Rtl_NtkFile(p), " {" );
1071 for ( i = 1; i <= pConcat[0]; i++ )
1072 Rtl_NtkPrintSig( p, pConcat[i] );
1073 fprintf( Rtl_NtkFile(p), " }" );
1074}
1075void Rtl_NtkPrintSig( Rtl_Ntk_t * p, int Sig )
1076{
1077 if ( Rtl_SigIsNone(Sig) )
1078 fprintf( Rtl_NtkFile(p), " %s", Rtl_NtkStr(p, Sig >> 2) );
1079 else if ( Rtl_SigIsConst(Sig) )
1080 Rtl_NtkPrintConst( p, Vec_IntEntryP(&p->pLib->vConsts, Sig >> 2) );
1081 else if ( Rtl_SigIsSlice(Sig) )
1082 Rtl_NtkPrintSlice( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
1083 else if ( Rtl_SigIsConcat(Sig) )
1084 Rtl_NtkPrintConcat( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
1085 else assert( 0 );
1086}
1087void Rtl_NtkPrintWire( Rtl_Ntk_t * p, int * pWire )
1088{
1089 fprintf( Rtl_NtkFile(p), " wire" );
1090 if ( pWire[1] != 1 ) fprintf( Rtl_NtkFile(p), " width %d", pWire[1] );
1091 if ( pWire[2] != 0 ) fprintf( Rtl_NtkFile(p), " offset %d", pWire[2] );
1092 if ( pWire[0] & 8 ) fprintf( Rtl_NtkFile(p), " upto" );
1093 if ( pWire[0] & 1 ) fprintf( Rtl_NtkFile(p), " input %d", pWire[3] );
1094 if ( pWire[0] & 2 ) fprintf( Rtl_NtkFile(p), " output %d", pWire[3] );
1095 if ( pWire[0] & 4 ) fprintf( Rtl_NtkFile(p), " signed" );
1096 fprintf( Rtl_NtkFile(p), " %s\n", Rtl_NtkStr(p, pWire[0] >> 4) );
1097}
1098void Rtl_NtkPrintCell( Rtl_Ntk_t * p, int * pCell )
1099{
1100 int i, Par, Val;
1101 Rtl_CellForEachAttr( p, pCell, Par, Val, i ) {
1102 fprintf( Rtl_NtkFile(p), " attribute %s %s\n", Rtl_NtkStr(p, Par), Rtl_NtkStr(p, Val) ); }
1103 fprintf( Rtl_NtkFile(p), " cell %s %s\n", Rtl_NtkStr(p, Rtl_CellType(pCell)), Rtl_NtkStr(p, pCell[1]) );
1104 Rtl_CellForEachParam( p, pCell, Par, Val, i )
1105 fprintf( Rtl_NtkFile(p), " parameter" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" );
1106 Rtl_CellForEachConnect( p, pCell, Par, Val, i ) {
1107 fprintf( Rtl_NtkFile(p), " connect" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" ); }
1108 fprintf( Rtl_NtkFile(p), " end\n" );
1109}
1110void Rtl_NtkPrintConnection( Rtl_Ntk_t * p, int * pCon )
1111{
1112 fprintf( Rtl_NtkFile(p), " connect" );
1113 Rtl_NtkPrintSig( p, pCon[0] );
1114 Rtl_NtkPrintSig( p, pCon[1] );
1115 fprintf( Rtl_NtkFile(p), "\n" );
1116}
1117void Rtl_NtkPrint( Rtl_Ntk_t * p )
1118{
1119 int i, Par, Val, * pWire, * pCell, * pCon;
1120 fprintf( Rtl_NtkFile(p), "\n" );
1121 Rtl_NtkForEachAttr( p, Par, Val, i )
1122 fprintf( Rtl_NtkFile(p), "attribute %s %s\n", Rtl_NtkStr(p, Par), Rtl_NtkStr(p, Val) );
1123 fprintf( Rtl_NtkFile(p), "module %s\n", Rtl_NtkName(p) );
1124 Rtl_NtkForEachWire( p, pWire, i )
1125 Rtl_NtkPrintWire( p, pWire );
1126 Rtl_NtkForEachCell( p, pCell, i )
1127 Rtl_NtkPrintCell( p, pCell );
1128 Rtl_NtkForEachCon( p, pCon, i )
1129 Rtl_NtkPrintConnection( p, pCon );
1130 fprintf( Rtl_NtkFile(p), "end\n" );
1131}
1132void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p )
1133{
1134 p->pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
1135 if ( p->pFile == NULL )
1136 {
1137 printf( "Cannot open output file \"%s\".\n", pFileName );
1138 return;
1139 }
1140 else
1141 {
1142 Rtl_Ntk_t * pNtk; int i;
1143 fprintf( p->pFile, "\n" );
1144 fprintf( p->pFile, "# Generated by ABC on %s\n", Extra_TimeStamp() );
1145 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
1146 Rtl_NtkPrint( pNtk );
1147 if ( p->pFile != stdout )
1148 fclose( p->pFile );
1149 p->pFile = NULL;
1150 }
1151}
1152
1153
1165extern int Rtl_NtkReadSig( Rtl_Ntk_t * p, int * pPos );
1166
1167int Rtl_NtkReadConst( Rtl_Ntk_t * p, char * pConst )
1168{
1169 Vec_Int_t * vConst = &p->pLib->vConsts;
1170 int RetVal = Vec_IntSize( vConst );
1171 int Width = atoi( pConst );
1172 assert( pConst[0] >= '0' && pConst[0] <= '9' );
1173 if ( strstr(pConst, "\'") )
1174 {
1175 int Length = strlen(pConst);
1176 int nWords = (Width + 31) / 32;
1177 int i, * pArray;
1178 Vec_IntPush( vConst, Width );
1179 Vec_IntFillExtra( vConst, Vec_IntSize(vConst) + nWords, 0 );
1180 pArray = Vec_IntEntryP( vConst, RetVal + 1 );
1181 for ( i = Length-1; i >= Length-Width; i-- )
1182 if ( pConst[i] == '1' )
1183 Abc_InfoSetBit( (unsigned *)pArray, Length-1-i );
1184 }
1185 else
1186 {
1187 Vec_IntPush( vConst, -1 );
1188 Vec_IntPush( vConst, Width );
1189 }
1190 return (RetVal << 2) | 1;
1191}
1192int Rtl_NtkReadSlice( Rtl_Ntk_t * p, char * pSlice, int NameId )
1193{
1194 Vec_Int_t * vSlice = &p->pLib->vSlices;
1195 int RetVal = Vec_IntSize( vSlice );
1196 int Left = atoi( pSlice+1 );
1197 char * pTwo = strstr( pSlice, ":" );
1198 int Right = pTwo ? atoi( pTwo+1 ) : Left;
1199 assert( pSlice[0] == '[' && pSlice[strlen(pSlice)-1] == ']' );
1200 Vec_IntPush( vSlice, NameId );
1201 Vec_IntPush( vSlice, Left );
1202 Vec_IntPush( vSlice, Right );
1203 return (RetVal << 2) | 2;
1204}
1205int Rtl_NtkReadConcat( Rtl_Ntk_t * p, int * pPos )
1206{
1207 Vec_Int_t * vConcat = &p->pLib->vConcats;
1208 int RetVal = Vec_IntSize( vConcat ); char * pTok;
1209 Vec_IntPush( vConcat, ABC_INFINITY );
1210 do {
1211 int Sig = Rtl_NtkReadSig( p, pPos );
1212 Vec_IntPush( vConcat, Sig );
1213 pTok = Rtl_NtkTokStr( p, *pPos );
1214 }
1215 while ( pTok[0] != '}' );
1216 Vec_IntWriteEntry( vConcat, RetVal, Vec_IntSize(vConcat) - RetVal - 1 );
1217 assert( pTok[0] == '}' );
1218 (*pPos)++;
1219 return (RetVal << 2) | 3;
1220}
1221int Rtl_NtkReadSig( Rtl_Ntk_t * p, int * pPos )
1222{
1223 int NameId = Rtl_NtkTokId( p, *pPos );
1224 char * pSig = Rtl_NtkTokStr( p, (*pPos)++ );
1225 if ( pSig[0] >= '0' && pSig[0] <= '9' )
1226 return Rtl_NtkReadConst( p, pSig );
1227 if ( pSig[0] == '{' )
1228 return Rtl_NtkReadConcat( p, pPos );
1229 else
1230 {
1231 char * pNext = Rtl_NtkTokStr( p, *pPos );
1232 if ( pNext && pNext[0] == '[' )
1233 {
1234 (*pPos)++;
1235 return Rtl_NtkReadSlice( p, pNext, NameId );
1236 }
1237 else
1238 return NameId << 2;
1239 }
1240}
1241int Rtl_NtkReadWire( Rtl_Ntk_t * p, int iPos )
1242{
1243 int i, Entry, Prev = -1;
1244 int Width = 1, Upto = 0, Offset = 0, Out = 0, In = 0, Number = 0, Signed = 0;
1245 assert( Rtl_NtkPosCheck(p, iPos-1, RTL_WIRE) );
1246 Vec_IntClear( &p->pLib->vAttrTemp );
1247 Vec_IntForEachEntryStart( p->pLib->vTokens, Entry, i, iPos )
1248 {
1249 //char * pTok = Rtl_NtkTokStr(p, i);
1250 if ( Entry == -1 )
1251 break;
1252 else if ( Rtl_NtkTokCheck(p, Entry, RTL_WIDTH) )
1253 Width = atoi( Rtl_NtkTokStr(p, ++i) );
1254 else if ( Rtl_NtkTokCheck(p, Entry, RTL_OFFSET) )
1255 Offset = atoi( Rtl_NtkTokStr(p, ++i) );
1256 else if ( Rtl_NtkTokCheck(p, Entry, RTL_INPUT) )
1257 Number = atoi( Rtl_NtkTokStr(p, ++i) ), In = 1, p->nInputs++;
1258 else if ( Rtl_NtkTokCheck(p, Entry, RTL_OUTPUT) )
1259 Number = atoi( Rtl_NtkTokStr(p, ++i) ), Out = 1, p->nOutputs++;
1260 else if ( Rtl_NtkTokCheck(p, Entry, RTL_SIGNED) )
1261 Signed = 1;
1262 else if ( Rtl_NtkTokCheck(p, Entry, RTL_UPTO) )
1263 Upto = 1;
1264 Prev = Entry;
1265 }
1266 // add WIRE_NUM=5 entries
1267 Vec_IntPush( &p->vWires, (Prev << 4) | (Upto << 3) | (Signed << 2) | (Out << 1) | (In << 0) );
1268 Vec_IntPush( &p->vWires, Width );
1269 Vec_IntPush( &p->vWires, Offset );
1270 Vec_IntPush( &p->vWires, Number );
1271 Vec_IntPush( &p->vWires, -1 );
1272 assert( Rtl_NtkPosCheck(p, i, RTL_NONE) );
1273 return i;
1274}
1275int Rtl_NtkReadAttribute( Rtl_Ntk_t * p, int iPos )
1276{
1277//char * pTok1 = Rtl_NtkTokStr(p, iPos-1);
1278//char * pTok2 = Rtl_NtkTokStr(p, iPos);
1279//char * pTok3 = Rtl_NtkTokStr(p, iPos+1);
1280 assert( Rtl_NtkPosCheck(p, iPos-1, RTL_ATTRIBUTE) );
1281 Vec_IntPush( &p->pLib->vAttrTemp, Rtl_NtkTokId(p, iPos++) );
1282 Vec_IntPush( &p->pLib->vAttrTemp, Rtl_NtkTokId(p, iPos++) );
1283 assert( Rtl_NtkPosCheck(p, iPos, RTL_NONE) );
1284 return iPos;
1285}
1286int Rtl_NtkReadAttribute2( Rtl_Lib_t * p, int iPos )
1287{
1288//char * pTok1 = Abc_NamStr(p->pManName, Vec_IntEntry(p->vTokens, iPos-1));
1289//char * pTok2 = Abc_NamStr(p->pManName, Vec_IntEntry(p->vTokens, iPos) );
1290//char * pTok3 = Abc_NamStr(p->pManName, Vec_IntEntry(p->vTokens, iPos+1));
1291 assert( Vec_IntEntry(p->vTokens, iPos-1) == p->pMap[RTL_ATTRIBUTE] );
1292 Vec_IntPush( &p->vAttrTemp, Vec_IntEntry(p->vTokens, iPos++) );
1293 Vec_IntPush( &p->vAttrTemp, Vec_IntEntry(p->vTokens, iPos++) );
1294 assert( Vec_IntEntry(p->vTokens, iPos) == p->pMap[RTL_NONE] );
1295 return iPos;
1296}
1297int Rtl_NtkReadConnect( Rtl_Ntk_t * p, int iPos )
1298{
1299//char * pTok1 = Rtl_NtkTokStr(p, iPos-1);
1300//char * pTok2 = Rtl_NtkTokStr(p, iPos);
1301//char * pTok3 = Rtl_NtkTokStr(p, iPos+1);
1302 assert( Rtl_NtkPosCheck(p, iPos-1, RTL_CONNECT) );
1303 Vec_IntPush( &p->vConns, Rtl_NtkReadSig(p, &iPos) );
1304 Vec_IntPush( &p->vConns, Rtl_NtkReadSig(p, &iPos) );
1305 assert( Rtl_NtkPosCheck(p, iPos, RTL_NONE) );
1306 return iPos;
1307}
1308int Rtl_NtkReadCell( Rtl_Ntk_t * p, int iPos )
1309{
1310 Vec_Int_t * vAttrs = &p->pLib->vAttrTemp;
1311 int iPosPars, iPosCons, Par, Val, i, Entry;
1312 assert( Rtl_NtkPosCheck(p, iPos-1, RTL_CELL) );
1313 Vec_IntPush( &p->vCells, Vec_IntSize(&p->vStore) );
1314 Vec_IntPush( &p->vStore, Rtl_NtkTokId(p, iPos++) ); // 0
1315 Vec_IntPush( &p->vStore, Rtl_NtkTokId(p, iPos++) ); // 1
1316 Vec_IntPush( &p->vStore, -1 );
1317 Vec_IntPush( &p->vStore, -1 );
1318 assert( Vec_IntSize(vAttrs) % 2 == 0 );
1319 Vec_IntPush( &p->vStore, Vec_IntSize(vAttrs)/2 );
1320 iPosPars = Vec_IntSize(&p->vStore);
1321 Vec_IntPush( &p->vStore, 0 ); // 5
1322 iPosCons = Vec_IntSize(&p->vStore);
1323 Vec_IntPush( &p->vStore, 0 ); // 6
1324 Vec_IntPush( &p->vStore, 0 ); // 7
1325 assert( Vec_IntSize(&p->vStore) == Vec_IntEntryLast(&p->vCells)+CELL_NUM );
1326 Vec_IntAppend( &p->vStore, vAttrs );
1327 Vec_IntClear( vAttrs );
1328 Vec_IntForEachEntryStart( p->pLib->vTokens, Entry, i, iPos )
1329 {
1330 if ( Rtl_NtkTokCheck(p, Entry, RTL_END) )
1331 break;
1332 if ( Rtl_NtkTokCheck(p, Entry, RTL_PARAMETER) || Rtl_NtkTokCheck(p, Entry, RTL_CONNECT) )
1333 {
1334 int iPosCount = Rtl_NtkTokCheck(p, Entry, RTL_PARAMETER) ? iPosPars : iPosCons;
1335 Vec_IntAddToEntry( &p->vStore, iPosCount, 1 );
1336 i++;
1337 Par = Rtl_NtkReadSig(p, &i);
1338 Val = Rtl_NtkReadSig(p, &i);
1339 Vec_IntPushTwo( &p->vStore, Par, Val );
1340 }
1341 assert( Rtl_NtkPosCheck(p, i, RTL_NONE) );
1342 }
1343 assert( Rtl_NtkPosCheck(p, i, RTL_END) );
1344 i++;
1345 assert( Rtl_NtkPosCheck(p, i, RTL_NONE) );
1346 return i;
1347}
1348int Wln_ReadMatchEnd( Rtl_Ntk_t * p, int Mod )
1349{
1350 int i, Entry, Count = 0;
1351 Vec_IntForEachEntryStart( p->pLib->vTokens, Entry, i, Mod )
1352 if ( Rtl_NtkTokCheck(p, Entry, RTL_CELL) )
1353 Count++;
1354 else if ( Rtl_NtkTokCheck(p, Entry, RTL_END) )
1355 {
1356 if ( Count == 0 )
1357 return i;
1358 Count--;
1359 }
1360 assert( 0 );
1361 return -1;
1362}
1363int Rtl_NtkReadNtk( Rtl_Lib_t * pLib, int Mod )
1364{
1365 Rtl_Ntk_t * p = Rtl_NtkAlloc( pLib );
1366 Vec_Int_t * vAttrs = &p->pLib->vAttrTemp;
1367 int End = Wln_ReadMatchEnd( p, Mod ), i, Entry;
1368 assert( Rtl_NtkPosCheck(p, Mod-1, RTL_MODULE) );
1369 assert( Rtl_NtkPosCheck(p, End, RTL_END) );
1370 p->NameId = Rtl_NtkTokId( p, Mod );
1371 p->Slice0 = Vec_IntSize( &pLib->vSlices );
1372 Vec_IntAppend( &p->vAttrs, vAttrs );
1373 Vec_IntClear( vAttrs );
1374 Vec_IntForEachEntryStartStop( pLib->vTokens, Entry, i, Mod, End )
1375 {
1376 if ( Rtl_NtkTokCheck(p, Entry, RTL_WIRE) )
1377 i = Rtl_NtkReadWire( p, i+1 );
1378 else if ( Rtl_NtkTokCheck(p, Entry, RTL_ATTRIBUTE) )
1379 i = Rtl_NtkReadAttribute( p, i+1 );
1380 else if ( Rtl_NtkTokCheck(p, Entry, RTL_CELL) )
1381 i = Rtl_NtkReadCell( p, i+1 );
1382 else if ( Rtl_NtkTokCheck(p, Entry, RTL_CONNECT) )
1383 i = Rtl_NtkReadConnect( p, i+1 );
1384 }
1385 p->Slice1 = Vec_IntSize( &pLib->vSlices );
1386 assert( Vec_IntSize(&p->vWires) % WIRE_NUM == 0 );
1387 return End;
1388}
1389void Rtl_NtkReportUndefs( Rtl_Ntk_t * p )
1390{
1391 Vec_Int_t * vNames, * vCounts;
1392 int i, iName, * pCell;
1393 vNames = Vec_IntAlloc( 10 );
1394 vCounts = Vec_IntAlloc( 10 );
1395 Rtl_NtkForEachCell( p, pCell, i )
1396 if ( Rtl_CellModule(pCell) == ABC_INFINITY-1 )
1397 {
1398 iName = Vec_IntFind(vNames, Rtl_CellType(pCell));
1399 if ( iName == -1 )
1400 {
1401 iName = Vec_IntSize(vNames);
1402 Vec_IntPush( vNames, Rtl_CellType(pCell) );
1403 Vec_IntPush( vCounts, 0 );
1404 }
1405 Vec_IntAddToEntry( vCounts, iName, 1 );
1406 }
1407 Vec_IntForEachEntry( vNames, iName, i )
1408 printf( " %s (%d)", Rtl_NtkStr(p, iName), Vec_IntEntry(vCounts, i) );
1409 printf( "\n" );
1410 Vec_IntFree( vNames );
1411 Vec_IntFree( vCounts );
1412}
1413int Rtl_NtkSetParents( Rtl_Ntk_t * p )
1414{
1415 int i, * pCell, nUndef = 0;
1416 Rtl_NtkForEachCell( p, pCell, i )
1417 {
1418 pCell[2] = Rtl_NtkReadType( p, Rtl_CellType(pCell) );
1419 if ( Rtl_CellModule(pCell) == ABC_INFINITY-1 )
1420 nUndef++;
1421 else
1422 pCell[3] = Rtl_CellModule(pCell) < ABC_INFINITY ? pCell[6]-1 : Rtl_NtkModule(p, Rtl_CellModule(pCell)-ABC_INFINITY)->nInputs;
1423 }
1424 if ( !nUndef )
1425 return 0;
1426 printf( "Module \"%s\" has %d blackbox instances: ", Rtl_NtkName(p), nUndef );
1427 Rtl_NtkReportUndefs( p );
1428 return nUndef;
1429}
1430void Rtl_LibSetParents( Rtl_Lib_t * p )
1431{
1432 Rtl_Ntk_t * pNtk; int i;
1433 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
1434 Rtl_NtkSetParents( pNtk );
1435}
1436void Rtl_LibReorderModules_rec( Rtl_Ntk_t * p, Vec_Ptr_t * vNew )
1437{
1438 int i, * pCell;
1439 Rtl_NtkForEachCell( p, pCell, i )
1440 {
1441 Rtl_Ntk_t * pMod = Rtl_CellNtk( p, pCell );
1442 if ( pMod && pMod->iCopy == -1 )
1443 Rtl_LibReorderModules_rec( pMod, vNew );
1444 }
1445 assert( p->iCopy == -1 );
1446 p->iCopy = Vec_PtrSize(vNew);
1447 Vec_PtrPush( vNew, p );
1448}
1449int Rtl_LibCountInsts( Rtl_Lib_t * p, Rtl_Ntk_t * pOne )
1450{
1451 Rtl_Ntk_t * pNtk; int n, i, * pCell, Count = 0;
1452 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, n )
1453 Rtl_NtkForEachCell( pNtk, pCell, i )
1454 {
1455 Rtl_Ntk_t * pMod = Rtl_CellNtk( pNtk, pCell );
1456 if ( pMod && pMod == pOne )
1457 Count++;
1458 }
1459 return Count;
1460}
1461void Rtl_NtkUpdateBoxes( Rtl_Ntk_t * p )
1462{
1463 int i, * pCell;
1464 Rtl_NtkForEachCell( p, pCell, i )
1465 {
1466 Rtl_Ntk_t * pMod = Rtl_CellNtk( p, pCell );
1467 if ( pMod && pMod->iCopy >= 0 )
1468 pCell[2] = ABC_INFINITY + pMod->iCopy;
1469 }
1470}
1471void Rtl_LibUpdateBoxes( Rtl_Lib_t * p )
1472{
1473 Rtl_Ntk_t * pNtk; int i;
1474 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
1475 Rtl_NtkUpdateBoxes( pNtk );
1476}
1477void Rtl_LibReorderModules( Rtl_Lib_t * p )
1478{
1479 Vec_Ptr_t * vNew = Vec_PtrAlloc( Vec_PtrSize(p->vNtks) );
1480 Rtl_Ntk_t * pNtk; int i;
1481 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
1482 pNtk->iCopy = -1;
1483 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
1484 if ( pNtk->iCopy == -1 )
1485 Rtl_LibReorderModules_rec( pNtk, vNew );
1486 assert( Vec_PtrSize(p->vNtks) == Vec_PtrSize(vNew) );
1487 Rtl_LibUpdateBoxes( p );
1488 Vec_PtrClear( p->vNtks );
1489 Vec_PtrAppend( p->vNtks, vNew );
1490 Vec_PtrFree( vNew );
1491}
1492Rtl_Lib_t * Rtl_LibReadFile( char * pFileName, char * pFileSpec )
1493{
1494 Rtl_Lib_t * p = Rtl_LibAlloc(); int i, Entry;
1495 p->pSpec = Abc_UtilStrsav( pFileSpec );
1496 p->pManName = Abc_NamStart( 1000, 50 );
1497 p->vTokens = Rtl_NtkReadFile( pFileName, p->pManName );
1498 Rtl_LibDeriveMap( p );
1499 Vec_IntClear( &p->vAttrTemp );
1500 Vec_IntForEachEntry( p->vTokens, Entry, i )
1501 if ( Entry == p->pMap[RTL_MODULE] )
1502 i = Rtl_NtkReadNtk( p, i+1 );
1503 else if ( Entry == p->pMap[RTL_ATTRIBUTE] )
1504 i = Rtl_NtkReadAttribute2( p, i+1 );
1505 Rtl_LibSetParents( p );
1506 Rtl_LibReorderModules( p );
1507 Rtl_LibOrderWires( p );
1508 return p;
1509}
1510
1511
1523extern int Rtl_NtkMapSignalRange( Rtl_Ntk_t * p, int Sig, int iCell, int iBit );
1524
1525int Rtl_NtkMapWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right, int iCell, int iBit )
1526{
1527 //char * pName = Rtl_NtkStr( p, NameId );
1528 int Wire = Rtl_WireMapNameToId( p, NameId );
1529 int First = Rtl_WireBitStart( p, Wire );
1530 int Width = Rtl_WireWidth( p, Wire ), i;
1531 Left = Left == -1 ? Width-1 : Left;
1532 Right = Right == -1 ? 0 : Right;
1533 assert ( Right >= 0 && Right <= Left );
1534 for ( i = Right; i <= Left; i++ )
1535 {
1536 assert( Vec_IntEntry(&p->vDrivers, 2*(First+i)) == -4 );
1537 Vec_IntWriteEntry(&p->vDrivers, 2*(First+i)+0, iCell );
1538 Vec_IntWriteEntry(&p->vDrivers, 2*(First+i)+1, iBit + (i - Right) );
1539 }
1540 return Left - Right + 1;
1541}
1542int Rtl_NtkMapSliceRange( Rtl_Ntk_t * p, int * pSlice, int iCell, int iBit )
1543{
1544 return Rtl_NtkMapWireRange( p, pSlice[0], pSlice[1], pSlice[2], iCell, iBit );
1545}
1546int Rtl_NtkMapConcatRange( Rtl_Ntk_t * p, int * pConcat, int iCell, int iBit )
1547{
1548 int i, k = 0;
1549 for ( i = 1; i <= pConcat[0]; i++ )
1550 k += Rtl_NtkMapSignalRange( p, pConcat[i], iCell, iBit+k );
1551 return k;
1552}
1553int Rtl_NtkMapSignalRange( Rtl_Ntk_t * p, int Sig, int iCell, int iBit )
1554{
1555 int nBits = ABC_INFINITY;
1556 if ( Rtl_SigIsNone(Sig) )
1557 nBits = Rtl_NtkMapWireRange( p, Sig >> 2, -1, -1, iCell, iBit );
1558 if ( Rtl_SigIsSlice(Sig) )
1559 nBits = Rtl_NtkMapSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2), iCell, iBit );
1560 if ( Rtl_SigIsConcat(Sig) )
1561 nBits = Rtl_NtkMapConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2), iCell, iBit );
1562 if ( Rtl_SigIsConst(Sig) )
1563 assert( 0 );
1564 return nBits;
1565}
1566
1567
1579extern void Rtl_NtkCollectSignalInfo( Rtl_Ntk_t * p, int Sig );
1580
1581void Rtl_NtkCollectWireInfo( Rtl_Ntk_t * p, int NameId, int Left, int Right )
1582{
1583 int Wire = Rtl_WireMapNameToId( p, NameId );
1584 int First = Rtl_WireBitStart( p, Wire );
1585 int Width = Rtl_WireWidth( p, Wire ), i;
1586 Left = Left == -1 ? Width-1 : Left;
1587 Right = Right == -1 ? 0 : Right;
1588 assert ( Right >= 0 && Right <= Left );
1589 for ( i = Right; i <= Left; i++ )
1590 Vec_IntPush( &p->vBitTemp, First+i );
1591}
1592void Rtl_NtkCollectConstInfo( Rtl_Ntk_t * p, int * pConst )
1593{
1594 int i, nLimit = pConst[0];
1595 if ( nLimit == -1 )
1596 nLimit = 32;
1597 for ( i = 0; i < nLimit; i++ )
1598 Vec_IntPush( &p->vBitTemp, Abc_InfoHasBit((unsigned *)pConst+1,i)-CONST_SHIFT );
1599}
1600void Rtl_NtkCollectSliceInfo( Rtl_Ntk_t * p, int * pSlice )
1601{
1602 Rtl_NtkCollectWireInfo( p, pSlice[0], pSlice[1], pSlice[2] );
1603}
1604void Rtl_NtkCollectConcatInfo( Rtl_Ntk_t * p, int * pConcat )
1605{
1606 int i;
1607 for ( i = pConcat[0]; i >= 1; i-- )
1608 Rtl_NtkCollectSignalInfo( p, pConcat[i] );
1609}
1610void Rtl_NtkCollectSignalInfo( Rtl_Ntk_t * p, int Sig )
1611{
1612 if ( Rtl_SigIsNone(Sig) )
1613 Rtl_NtkCollectWireInfo( p, Sig >> 2, -1, -1 );
1614 else if ( Rtl_SigIsConst(Sig) )
1615 Rtl_NtkCollectConstInfo( p, Vec_IntEntryP(&p->pLib->vConsts, Sig >> 2) );
1616 else if ( Rtl_SigIsSlice(Sig) )
1617 Rtl_NtkCollectSliceInfo( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
1618 else if ( Rtl_SigIsConcat(Sig) )
1619 Rtl_NtkCollectConcatInfo( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
1620 else assert( 0 );
1621}
1622
1634extern void Rtl_NtkCollectSignalRange( Rtl_Ntk_t * p, int Sig );
1635
1636void Rtl_NtkCollectWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right )
1637{
1638 int Wire = Rtl_WireMapNameToId( p, NameId );
1639 int First = Rtl_WireBitStart( p, Wire );
1640 int Width = Rtl_WireWidth( p, Wire ), i;
1641 Left = Left == -1 ? Width-1 : Left;
1642 Right = Right == -1 ? 0 : Right;
1643 assert ( Right >= 0 && Right <= Left );
1644 for ( i = Right; i <= Left; i++ )
1645 {
1646 assert( Vec_IntEntry(&p->vLits, First+i) != -1 );
1647 Vec_IntPush( &p->vBitTemp, Vec_IntEntry(&p->vLits, First+i) );
1648 }
1649}
1650void Rtl_NtkCollectConstRange( Rtl_Ntk_t * p, int * pConst )
1651{
1652 int i, nLimit = pConst[0];
1653 if ( nLimit == -1 )
1654 nLimit = 32;
1655 for ( i = 0; i < nLimit; i++ )
1656 Vec_IntPush( &p->vBitTemp, Abc_InfoHasBit((unsigned *)pConst+1,i) );
1657}
1658void Rtl_NtkCollectSliceRange( Rtl_Ntk_t * p, int * pSlice )
1659{
1660 Rtl_NtkCollectWireRange( p, pSlice[0], pSlice[1], pSlice[2] );
1661}
1662void Rtl_NtkCollectConcatRange( Rtl_Ntk_t * p, int * pConcat )
1663{
1664 int i;
1665 for ( i = pConcat[0]; i >= 1; i-- )
1666 Rtl_NtkCollectSignalRange( p, pConcat[i] );
1667}
1668void Rtl_NtkCollectSignalRange( Rtl_Ntk_t * p, int Sig )
1669{
1670 if ( Rtl_SigIsNone(Sig) )
1671 Rtl_NtkCollectWireRange( p, Sig >> 2, -1, -1 );
1672 else if ( Rtl_SigIsConst(Sig) )
1673 Rtl_NtkCollectConstRange( p, Vec_IntEntryP(&p->pLib->vConsts, Sig >> 2) );
1674 else if ( Rtl_SigIsSlice(Sig) )
1675 Rtl_NtkCollectSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
1676 else if ( Rtl_SigIsConcat(Sig) )
1677 Rtl_NtkCollectConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
1678 else assert( 0 );
1679}
1680
1681
1682extern int Rtl_NtkInsertSignalRange( Rtl_Ntk_t * p, int Sig, int * pLits, int nLits );
1683
1684int Rtl_NtkInsertWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right, int * pLits, int nLits )
1685{
1686 //char * pName = Rtl_NtkStr( p, NameId );
1687 int Wire = Rtl_WireMapNameToId( p, NameId );
1688 int First = Rtl_WireBitStart( p, Wire );
1689 int Width = Rtl_WireWidth( p, Wire ), i, k = 0;
1690 Left = Left == -1 ? Width-1 : Left;
1691 Right = Right == -1 ? 0 : Right;
1692 assert ( Right >= 0 && Right <= Left );
1693 for ( i = Right; i <= Left; i++ )
1694 {
1695 assert( Vec_IntEntry(&p->vLits, First+i) == -1 );
1696 Vec_IntWriteEntry(&p->vLits, First+i, pLits[k++] );
1697 }
1698 assert( k <= nLits );
1699 return k;
1700}
1701int Rtl_NtkInsertSliceRange( Rtl_Ntk_t * p, int * pSlice, int * pLits, int nLits )
1702{
1703 return Rtl_NtkInsertWireRange( p, pSlice[0], pSlice[1], pSlice[2], pLits, nLits );
1704}
1705int Rtl_NtkInsertConcatRange( Rtl_Ntk_t * p, int * pConcat, int * pLits, int nLits )
1706{
1707 int i, k = 0;
1708 for ( i = 1; i <= pConcat[0]; i++ )
1709 k += Rtl_NtkInsertSignalRange( p, pConcat[i], pLits+k, nLits-k );
1710 assert( k <= nLits );
1711 return k;
1712}
1713int Rtl_NtkInsertSignalRange( Rtl_Ntk_t * p, int Sig, int * pLits, int nLits )
1714{
1715 int nBits = ABC_INFINITY;
1716 if ( Rtl_SigIsNone(Sig) )
1717 nBits = Rtl_NtkInsertWireRange( p, Sig >> 2, -1, -1, pLits, nLits );
1718 if ( Rtl_SigIsSlice(Sig) )
1719 nBits = Rtl_NtkInsertSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2), pLits, nLits );
1720 if ( Rtl_SigIsConcat(Sig) )
1721 nBits = Rtl_NtkInsertConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2), pLits, nLits );
1722 if ( Rtl_SigIsConst(Sig) )
1723 assert( 0 );
1724 assert( nBits == nLits );
1725 return nBits;
1726}
1727
1739Vec_Int_t * Rtl_NtkRevPermInput( Rtl_Ntk_t * p )
1740{
1741 Vec_Int_t * vNew = Vec_IntAlloc( 100 ); int b, i, Count = 0;
1742 for ( i = 0; i < p->nInputs; i++ )
1743 {
1744 int Width = Rtl_WireWidth( p, i );
1745 for ( b = 0; b < Width; b++ )
1746 Vec_IntPush( vNew, Count + Width-1-b );
1747 Count += Width;
1748 }
1749 return vNew;
1750}
1751Vec_Int_t * Rtl_NtkRevPermOutput( Rtl_Ntk_t * p )
1752{
1753 Vec_Int_t * vNew = Vec_IntAlloc( 100 ); int b, i, Count = 0;
1754 for ( i = 0; i < p->nOutputs; i++ )
1755 {
1756 int Width = Rtl_WireWidth( p, p->nInputs + i );
1757 for ( b = 0; b < Width; b++ )
1758 Vec_IntPush( vNew, Count + Width-1-b );
1759 Count += Width;
1760 }
1761 return vNew;
1762}
1763
1775void Rtl_NtkBlastInputs( Gia_Man_t * pNew, Rtl_Ntk_t * p )
1776{
1777 int b, i;
1778 for ( i = 0; i < p->nInputs; i++ )
1779 {
1780 int First = Rtl_WireBitStart( p, i );
1781 int Width = Rtl_WireWidth( p, i );
1782 for ( b = 0; b < Width; b++ )
1783 {
1784 assert( Vec_IntEntry(&p->vLits, First+b) == -1 );
1785 Vec_IntWriteEntry( &p->vLits, First+b, Gia_ManAppendCi(pNew) );
1786 }
1787 }
1788}
1789void Rtl_NtkBlastOutputs( Gia_Man_t * pNew, Rtl_Ntk_t * p )
1790{
1791 int b, i;
1792 for ( i = 0; i < p->nOutputs; i++ )
1793 {
1794 int First = Rtl_WireBitStart( p, p->nInputs + i );
1795 int Width = Rtl_WireWidth( p, p->nInputs + i );
1796 for ( b = 0; b < Width; b++ )
1797 {
1798 assert( Vec_IntEntry(&p->vLits, First+b) != -1 );
1799 Gia_ManAppendCo( pNew, Vec_IntEntry(&p->vLits, First+b) );
1800 }
1801 }
1802}
1803void Rtl_NtkBlastConnect( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCon )
1804{
1805 int nBits;
1806 Vec_IntClear( &p->vBitTemp );
1807 Rtl_NtkCollectSignalRange( p, pCon[0] );
1808 nBits = Rtl_NtkInsertSignalRange( p, pCon[1], Vec_IntArray(&p->vBitTemp), Vec_IntSize(&p->vBitTemp) );
1809 assert( nBits == Vec_IntSize(&p->vBitTemp) );
1810 //printf( "Finished blasting connection (Value = %d).\n", Vec_IntEntry(&p->vBitTemp, 0) );
1811}
1812void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
1813{
1814 extern void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs );
1815 extern Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p );
1816 extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
1817 extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
1818 Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
1819 int nIns = 0, nOuts = 0, nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
1820 int k, Par, Val, iThis = -1, nBits = 0;
1821 //int fFound = 0;
1822 int fFound = p->pLib->vInverses && (iThis = Vec_IntFind(p->pLib->vInverses, pModel->NameId)) >= 0;
1823 //int iThat = fFound ? Vec_IntEntry( p->pLib->vInverses, iThis ^ 1 ) : -1;
1824 Vec_IntClear( &p->vBitTemp );
1825 Rtl_CellForEachInput( p, pCell, Par, Val, k )
1826 Rtl_NtkCollectSignalRange( p, Val );
1827 assert( pModel->pGia );
1828 if ( fFound )
1829 {
1830 nIns = nOuts1;
1831 Vec_IntForEachEntry( &p->vBitTemp, Val, k )
1832 Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
1833 Vec_IntPush( pNew->vBarBufs, (nIns << 16) | Abc_Var2Lit(pModel->NameId, 0) );
1834 }
1835 else if ( pModel->fRoot )
1836 {
1837 nIns = Vec_IntSize(&p->vBitTemp);
1838 Vec_IntForEachEntry( &p->vBitTemp, Val, k )
1839 //Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
1840 Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
1841 Vec_IntPush( pNew->vBarBufs, (nIns << 16) | Abc_Var2Lit(pModel->NameId, 0) );
1842 }
1843 if ( fFound || pModel->fRoot )
1844 Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, 0 );
1845 else
1846 {
1847 Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, 1 );
1848 Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
1849 }
1850 if ( pModel->fRoot || fFound )
1851 {
1852 nOuts = Vec_IntSize(&p->vBitTemp);
1853 Vec_IntForEachEntry( &p->vBitTemp, Val, k )
1854 Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
1855 Vec_IntPush( pNew->vBarBufs, (nOuts << 16) | Abc_Var2Lit(pModel->NameId, 1) );
1856 printf( "Added %d input buffers and %d output buffers for module %s.\n", nIns, nOuts, Rtl_NtkName(pModel) );
1857 }
1858 Rtl_CellForEachOutput( p, pCell, Par, Val, k )
1859 nBits += Rtl_NtkInsertSignalRange( p, Val, Vec_IntArray(&p->vBitTemp)+nBits, Vec_IntSize(&p->vBitTemp)-nBits );
1860 assert( nBits == Vec_IntSize(&p->vBitTemp) );
1861}
1862
1863int Rtl_NtkCellParamValue( Rtl_Ntk_t * p, int * pCell, char * pParam )
1864{
1865 int ParamId = Rtl_NtkStrId( p, pParam );
1866 int i, Par, Val, ValOut = ABC_INFINITY, * pConst;
1867// p->pLib->pFile = stdout;
1868// Rtl_CellForEachParam( p, pCell, Par, Val, i )
1869// fprintf( Rtl_NtkFile(p), " parameter" ), Rtl_NtkPrintSig(p, Par), Rtl_NtkPrintSig(p, Val), printf( "\n" );
1870 Rtl_CellForEachParam( p, pCell, Par, Val, i )
1871 if ( (Par >> 2) == ParamId )
1872 {
1873 assert( Rtl_SigIsConst(Val) );
1874 pConst = Vec_IntEntryP( &p->pLib->vConsts, Val >> 2 );
1875 assert( pConst[0] < 32 );
1876 ValOut = pConst[1];
1877 }
1878 return ValOut;
1879}
1880void Rtl_NtkBlastOperator( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
1881{
1882 extern void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas, int nRange, int fSign0, int fSign1 );
1883 Vec_Int_t * vRes = &p->pLib->vTemp[3];
1884 int i, Par, Val, ValOut = -1, nBits = 0, nRange = -1;
1885 int fSign0 = Rtl_NtkCellParamValue( p, pCell, "\\A_SIGNED" );
1886 int fSign1 = Rtl_NtkCellParamValue( p, pCell, "\\B_SIGNED" );
1887 Rtl_CellForEachOutput( p, pCell, Par, ValOut, i )
1888 nRange = Rtl_NtkCountSignalRange( p, ValOut );
1889 assert( nRange > 0 );
1890 for ( i = 0; i < TEMP_NUM; i++ )
1891 Vec_IntClear( &p->pLib->vTemp[i] );
1892 //printf( "Starting blasting cell %s.\n", Rtl_CellNameStr(p, pCell) );
1893 Rtl_CellForEachInput( p, pCell, Par, Val, i )
1894 {
1895 Vec_IntClear( &p->vBitTemp );
1896 Rtl_NtkCollectSignalRange( p, Val );
1897 Vec_IntAppend( &p->pLib->vTemp[i], &p->vBitTemp );
1898 }
1899 Rtl_NtkBlastNode( pNew, Rtl_CellModule(pCell), Rtl_CellInputNum(pCell), p->pLib->vTemp, nRange, fSign0, fSign1 );
1900 assert( Vec_IntSize(vRes) > 0 );
1901 nBits = Rtl_NtkInsertSignalRange( p, ValOut, Vec_IntArray(vRes)+nBits, Vec_IntSize(vRes)-nBits );
1902 assert( nBits == Vec_IntSize(vRes) );
1903 //printf( "Finished blasting cell %s (Value = %d).\n", Rtl_CellNameStr(p, pCell), Vec_IntEntry(vRes, 0) );
1904}
1905char * Rtl_ShortenName( char * pName, int nSize )
1906{
1907 static char Buffer[1000];
1908 if ( (int)strlen(pName) <= nSize )
1909 return pName;
1910 Buffer[0] = 0;
1911 strcat( Buffer, pName );
1912 //Buffer[nSize-4] = ' ';
1913 Buffer[nSize-3] = '.';
1914 Buffer[nSize-2] = '.';
1915 Buffer[nSize-1] = '.';
1916 Buffer[nSize-0] = 0;
1917 return Buffer;
1918}
1919void Rtl_NtkPrintBufOne( Rtl_Lib_t * p, int Lit )
1920{
1921 printf( "%s (%c%d) ", Rtl_LibStr(p, Abc_Lit2Var(Lit&0xFFFF)), Abc_LitIsCompl(Lit)? 'o' : 'i', Lit >> 16 );
1922}
1923void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs )
1924{
1925 int i, Lit;
1926 if ( Vec_IntSize(vBufs) )
1927 printf( "Found %d buffers (%d groups): ", p->pGia->nBufs, Vec_IntSize(vBufs) );
1928 Vec_IntForEachEntry( vBufs, Lit, i )
1929 Rtl_NtkPrintBufOne( p->pLib, Lit );
1930 if ( Vec_IntSize(vBufs) )
1931 printf( "\n" );
1932}
1933Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p )
1934{
1935 int fDump = 0;
1936 Gia_Man_t * pTemp, * pNew = Gia_ManStart( 1000 );
1937 int i, iObj, * pCell, nBits = Rtl_NtkRangeWires( p );
1938 Vec_IntFill( &p->vLits, nBits, -1 );
1939 Rtl_NtkMapWires( p, 0 );
1940 Rtl_NtkBlastInputs( pNew, p );
1941 Gia_ManHashAlloc( pNew );
1942 Vec_IntForEachEntry( &p->vOrder, iObj, i )
1943 {
1944 iObj -= Rtl_NtkInputNum(p);
1945 if ( iObj < 0 )
1946 continue;
1947 if ( iObj >= Rtl_NtkCellNum(p) )
1948 {
1949 Rtl_NtkBlastConnect( pNew, p, Rtl_NtkCon(p, iObj - Rtl_NtkCellNum(p)) );
1950 continue;
1951 }
1952 pCell = Rtl_NtkCell(p, iObj);
1953 if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
1954 Rtl_NtkBlastHierarchy( pNew, p, pCell );
1955 else if ( Rtl_CellModule(pCell) < ABC_OPER_LAST )
1956 Rtl_NtkBlastOperator( pNew, p, pCell );
1957 else
1958 printf( "Cannot blast black box %s in module %s.\n", Rtl_NtkStr(p, Rtl_CellType(pCell)), Rtl_NtkName(p) );
1959 }
1960 Gia_ManHashStop( pNew );
1961 Rtl_NtkBlastOutputs( pNew, p );
1962 Rtl_NtkMapWires( p, 1 );
1963 pNew = Gia_ManCleanup( pTemp = pNew );
1964 Gia_ManStop( pTemp );
1965 if ( fDump )
1966 {
1967 char Buffer[100]; static int counter = 0;
1968 sprintf( Buffer, "old%02d.aig", counter++ );
1969 Gia_AigerWrite( pNew, Buffer, 0, 0, 0 );
1970 printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rtl_NtkName(p), 20) );
1971 }
1972 else
1973 printf( "Derived AIG for module %-20s : ", Rtl_ShortenName(Rtl_NtkName(p), 20) );
1974 Gia_ManPrintStats( pNew, NULL );
1975 return pNew;
1976}
1977void Rtl_LibBlast( Rtl_Lib_t * pLib )
1978{
1979 Rtl_Ntk_t * p; int i;
1980 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
1981 if ( p->pGia == NULL )
1982 p->pGia = Rtl_NtkBlast( p );
1983}
1984
1996// -4 unassigned
1997// -3 other bit
1998// -2 constant
1999// -1 primary input
2000// 0+ cell
2001int Rtl_NtkBlastCons( Rtl_Ntk_t * p )
2002{
2003 int c, i, iBit0, iBit1, * pCon, * pDri0, * pDri1, nChanges = 0;
2004 Rtl_NtkForEachCon( p, pCon, c )
2005 {
2006 Vec_IntClear( &p->vBitTemp );
2007 Rtl_NtkCollectSignalInfo( p, pCon[1] );
2008 Vec_IntClearAppend( &p->vBitTemp2, &p->vBitTemp );
2009
2010 Vec_IntClear( &p->vBitTemp );
2011 Rtl_NtkCollectSignalInfo( p, pCon[0] );
2012 assert( Vec_IntSize(&p->vBitTemp2) == Vec_IntSize(&p->vBitTemp) );
2013
2014 Vec_IntForEachEntryTwo( &p->vBitTemp, &p->vBitTemp2, iBit0, iBit1, i )
2015 {
2016 pDri0 = iBit0 >= 0 ? Vec_IntEntryP(&p->vDrivers, 2*iBit0) : NULL;
2017 pDri1 = iBit1 >= 0 ? Vec_IntEntryP(&p->vDrivers, 2*iBit1) : NULL;
2018 assert( iBit0 >= 0 || iBit1 >= 0 );
2019 if ( iBit0 < 0 )
2020 {
2021 if ( pDri1[0] == -4 )
2022 {
2023 assert( pDri1[1] == -4 );
2024 pDri1[0] = -2;
2025 pDri1[1] = iBit0+CONST_SHIFT;
2026 nChanges++;
2027 }
2028 continue;
2029 }
2030 if ( iBit1 < 0 )
2031 {
2032 if ( pDri0[0] == -4 )
2033 {
2034 assert( pDri0[1] == -4 );
2035 pDri0[0] = -2;
2036 pDri0[1] = iBit1+CONST_SHIFT;
2037 nChanges++;
2038 }
2039 continue;
2040 }
2041 if ( pDri0[0] == -4 && pDri1[0] != -4 )
2042 {
2043 assert( pDri0[1] == -4 );
2044 pDri0[0] = -3;
2045 pDri0[1] = iBit1;
2046 nChanges++;
2047 continue;
2048 }
2049 if ( pDri1[0] == -4 && pDri0[0] != -4 )
2050 {
2051 assert( pDri1[1] == -4 );
2052 pDri1[0] = -3;
2053 pDri1[1] = iBit0;
2054 nChanges++;
2055 continue;
2056 }
2057 }
2058 }
2059 //printf( "Changes %d\n", nChanges );
2060 return nChanges;
2061}
2062void Rtl_NtkBlastMap( Rtl_Ntk_t * p, int nBits )
2063{
2064 int i, k, Par, Val, * pCell, iBit = 0;
2065 Vec_IntFill( &p->vDrivers, 2*nBits, -4 );
2066 for ( i = 0; i < p->nInputs; i++ )
2067 {
2068 int First = Rtl_WireBitStart( p, i );
2069 int Width = Rtl_WireWidth( p, i );
2070 for ( k = 0; k < Width; k++ )
2071 {
2072 assert( Vec_IntEntry(&p->vDrivers, 2*(First+k)) == -4 );
2073 Vec_IntWriteEntry(&p->vDrivers, 2*(First+k)+0, -1 );
2074 Vec_IntWriteEntry(&p->vDrivers, 2*(First+k)+1, iBit++ );
2075 }
2076 }
2077 Rtl_NtkForEachCell( p, pCell, i )
2078 {
2079 int iBit = 0;
2080 Rtl_CellForEachOutput( p, pCell, Par, Val, k )
2081 iBit += Rtl_NtkMapSignalRange( p, Val, i, iBit );
2082 }
2083 for ( i = 0; i < 100; i++ )
2084 if ( !Rtl_NtkBlastCons(p) )
2085 break;
2086 if ( i == 100 )
2087 printf( "Mapping connections did not succeed after %d iterations.\n", i );
2088// else
2089// printf( "Mapping connections converged after %d iterations.\n", i );
2090}
2091int Rtl_NtkCollectOrComputeBit( Rtl_Ntk_t * p, int iBit )
2092{
2093 extern void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver );
2094 if ( Vec_IntEntry(&p->vLits, iBit) == -1 )
2095 {
2096 int * pDriver = Vec_IntEntryP(&p->vDrivers, 2*iBit);
2097 assert( pDriver[0] != -4 );
2098 Rtl_NtkBlast2_rec( p, iBit, pDriver );
2099 }
2100 assert( Vec_IntEntry(&p->vLits, iBit) >= 0 );
2101 return Vec_IntEntry(&p->vLits, iBit);
2102}
2103int Rtl_NtkBlast2Spec( Rtl_Ntk_t * p, int * pCell, int iInput )
2104{
2105 int i, Par, Val, pLits[3] = {-1, -1, -1}, iBit;
2106 Rtl_CellForEachInput( p, pCell, Par, Val, i )
2107 {
2108 Vec_Int_t * vTemp;
2109 Vec_IntClear( &p->vBitTemp );
2110 Rtl_NtkCollectSignalInfo( p, Val );
2111 vTemp = Vec_IntDup( &p->vBitTemp );
2112 iBit = Vec_IntEntry( vTemp, i==2 ? 0 : iInput );
2113 if ( iBit >= 0 )
2114 pLits[i] = Rtl_NtkCollectOrComputeBit( p, iBit );
2115 else
2116 pLits[i] = iBit+CONST_SHIFT;
2117 assert( pLits[i] >= 0 );
2118 Vec_IntFree( vTemp );
2119 }
2120 return Gia_ManHashMux(p->pGia, pLits[2], pLits[1], pLits[0]);
2121}
2122void Rtl_NtkBlastPrepareInputs( Rtl_Ntk_t * p, int * pCell )
2123{
2124 int i, k, Par, Val, iBit;
2125 Rtl_CellForEachInput( p, pCell, Par, Val, i )
2126 {
2127 Vec_Int_t * vTemp;
2128 Vec_IntClear( &p->vBitTemp );
2129 Rtl_NtkCollectSignalInfo( p, Val );
2130 vTemp = Vec_IntDup( &p->vBitTemp );
2131 Vec_IntForEachEntry( vTemp, iBit, k )
2132 if ( iBit >= 0 )
2133 Rtl_NtkCollectOrComputeBit( p, iBit );
2134 Vec_IntFree( vTemp );
2135 }
2136}
2137void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver )
2138{
2139 //char * pName = Rtl_NtkName(p);
2140 assert( pDriver[0] != -1 );
2141 if ( pDriver[0] == -3 )
2142 {
2143 int * pDriver1 = Vec_IntEntryP( &p->vDrivers, 2*pDriver[1] );
2144 if ( Vec_IntEntry(&p->vLits, pDriver[1]) == -1 )
2145 Rtl_NtkBlast2_rec( p, pDriver[1], pDriver1 );
2146 assert( Vec_IntEntry(&p->vLits, pDriver[1]) >= 0 );
2147 Vec_IntWriteEntry( &p->vLits, iBit, Vec_IntEntry(&p->vLits, pDriver[1]) );
2148 return;
2149 }
2150 if ( pDriver[0] == -2 )
2151 {
2152 Vec_IntWriteEntry( &p->vLits, iBit, pDriver[1] );
2153 return;
2154 }
2155 else
2156 {
2157 int * pCell = Rtl_NtkCell(p, pDriver[0]);
2158 assert( pDriver[0] >= 0 );
2159 if ( Rtl_CellModule(pCell) == ABC_OPER_SEL_NMUX ) // special case
2160 {
2161 int iLit = Rtl_NtkBlast2Spec( p, pCell, pDriver[1] );
2162 Vec_IntWriteEntry( &p->vLits, iBit, iLit );
2163 return;
2164 }
2165 Rtl_NtkBlastPrepareInputs( p, pCell );
2166 if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
2167 Rtl_NtkBlastHierarchy( p->pGia, p, pCell );
2168 else if ( Rtl_CellModule(pCell) < ABC_OPER_LAST )
2169 Rtl_NtkBlastOperator( p->pGia, p, pCell );
2170 else
2171 printf( "Cannot blast black box %s in module %s.\n", Rtl_NtkStr(p, Rtl_CellType(pCell)), Rtl_NtkName(p) );
2172 }
2173}
2174Gia_Man_t * Rtl_NtkBlast2( Rtl_Ntk_t * p )
2175{
2176 int fDump = 0;
2177 Gia_Man_t * pTemp;
2178 int i, b, nBits = Rtl_NtkRangeWires( p );
2179 Vec_IntFill( &p->vLits, nBits, -1 );
2180printf( "Blasting %s...\r", Rtl_NtkName(p) );
2181 Rtl_NtkMapWires( p, 0 );
2182 Rtl_NtkBlastMap( p, nBits );
2183 assert( p->pGia == NULL );
2184 p->pGia = Gia_ManStart( 1000 );
2185 p->pGia->vBarBufs = Vec_IntAlloc( 1000 );
2186 Rtl_NtkBlastInputs( p->pGia, p );
2187 Gia_ManHashAlloc( p->pGia );
2188 for ( i = 0; i < p->nOutputs; i++ )
2189 {
2190 int First = Rtl_WireBitStart( p, p->nInputs + i );
2191 int Width = Rtl_WireWidth( p, p->nInputs + i );
2192 for ( b = 0; b < Width; b++ )
2193 Rtl_NtkCollectOrComputeBit( p, First+b );
2194 }
2195 Gia_ManHashStop( p->pGia );
2196 Rtl_NtkBlastOutputs( p->pGia, p );
2197 Rtl_NtkMapWires( p, 1 );
2198 p->pGia = Gia_ManCleanup( pTemp = p->pGia );
2199 ABC_SWAP( Vec_Int_t *, p->pGia->vBarBufs, pTemp->vBarBufs );
2200 Gia_ManStop( pTemp );
2201// if ( p->fRoot )
2202// Rtl_NtkPrintBufs( p, p->pGia->vBarBufs );
2203 if ( fDump )
2204 {
2205 char Buffer[100]; static int counter = 0;
2206 sprintf( Buffer, "old%02d.aig", counter++ );
2207 Gia_AigerWrite( p->pGia, Buffer, 0, 0, 0 );
2208 printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rtl_NtkName(p), 20) );
2209 }
2210 else
2211 printf( "Derived AIG for module %-20s : ", Rtl_ShortenName(Rtl_NtkName(p), 20) );
2212 Gia_ManPrintStats( p->pGia, NULL );
2213 return p->pGia;
2214}
2215void Rtl_LibMark_rec( Rtl_Ntk_t * pNtk )
2216{
2217 int i, * pCell;
2218 if ( pNtk->iCopy == -1 )
2219 return;
2220 Rtl_NtkForEachCell( pNtk, pCell, i )
2221 {
2222 Rtl_Ntk_t * pMod = Rtl_CellNtk( pNtk, pCell );
2223 if ( pMod )
2224 Rtl_LibMark_rec( pMod );
2225 }
2226 assert( pNtk->iCopy == -2 );
2227 pNtk->iCopy = -1;
2228}
2229void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots, int fInv )
2230{
2231 Rtl_Ntk_t * pNtk; int i, iNtk;
2232 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
2233 pNtk->iCopy = -1;
2234 if ( vRoots )
2235 {
2236 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
2237 pNtk->iCopy = -2;//, pNtk->fRoot = 0;
2238 Vec_IntForEachEntry( vRoots, iNtk, i )
2239 {
2240 Rtl_Ntk_t * pNtk = Rtl_LibNtk(pLib, iNtk);
2241 //pNtk->fRoot = fInv;
2242 Rtl_LibMark_rec( pNtk );
2243 }
2244 }
2245 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
2246 if ( pNtk->iCopy == -1 && pNtk->pGia == NULL )
2247 pNtk->pGia = Rtl_NtkBlast2( pNtk );
2248// Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
2249// if ( pNtk->iCopy == -2 )
2250// printf( "Skipping network \"%s\" during bit-blasting.\n", Rtl_NtkName(pNtk) );
2251 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
2252 pNtk->iCopy = -1;
2253}
2254void Rtl_LibBlastClean( Rtl_Lib_t * p )
2255{
2256 Rtl_Ntk_t * pNtk; int i;
2257 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
2258 Gia_ManStopP( &pNtk->pGia );
2259}
2260void Rtl_LibSetReplace( Rtl_Lib_t * p, Vec_Wec_t * vGuide )
2261{
2262 Vec_Int_t * vLevel; int i, iNtk1, iNtk2;
2263 Rtl_Ntk_t * pNtk, * pNtk1, * pNtk2;
2264 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
2265 pNtk->iCopy = -1;
2266 Vec_WecForEachLevel( vGuide, vLevel, i )
2267 {
2268 int Type = Vec_IntEntry( vLevel, 1 );
2269 int Name1 = Vec_IntEntry( vLevel, 2 );
2270 int Name2 = Vec_IntEntry( vLevel, 3 );
2271 int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 );
2272 if ( iNtk == -1 )
2273 {
2274 printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) );
2275 break;
2276 }
2277 if ( Type != Rtl_LibStrId(p, "equal") )
2278 continue;
2279 iNtk1 = iNtk >> 16;
2280 iNtk2 = iNtk & 0xFFFF;
2281 pNtk1 = Rtl_LibNtk(p, iNtk1);
2282 pNtk2 = Rtl_LibNtk(p, iNtk2);
2283 pNtk1->iCopy = iNtk2;
2284 if ( iNtk1 == iNtk2 )
2285 printf( "Preparing to prove \"%s\".\n", Rtl_NtkName(pNtk1) );
2286 else
2287 printf( "Preparing to replace \"%s\" by \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
2288 }
2289}
2290
2291
2303void Rtl_LibPreprocess( Rtl_Lib_t * pLib )
2304{
2305 abctime clk = Abc_Clock();
2306 Rtl_Ntk_t * p1 = NULL, * p2 = NULL, * p;
2307 int i, k, Status, fFound = 0;
2308 printf( "Performing preprocessing for verification.\n" );
2309 // find similar modules
2310 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p1, i )
2311 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p2, k )
2312 {
2313 if ( i >= k )
2314 continue;
2315 if ( Gia_ManCiNum(p1->pGia) != Gia_ManCiNum(p2->pGia) ||
2316 Gia_ManCoNum(p1->pGia) != Gia_ManCoNum(p2->pGia) )
2317 continue;
2318 // two similar modules
2319 Status = Cec_ManVerifyTwo( p1->pGia, p2->pGia, 0 );
2320 if ( Status != 1 )
2321 continue;
2322 printf( "Proved equivalent modules: %s == %s\n", Rtl_NtkName(p1), Rtl_NtkName(p2) );
2323 // inline
2324 if ( Gia_ManAndNum(p1->pGia) > Gia_ManAndNum(p2->pGia) )
2325 ABC_SWAP( Gia_Man_t *, p1->pGia, p2->pGia );
2326 assert( Gia_ManAndNum(p1->pGia) <= Gia_ManAndNum(p2->pGia) );
2327 Gia_ManStopP( &p2->pGia );
2328 p2->pGia = Gia_ManDup( p1->pGia );
2329 fFound = 1;
2330 goto finish;
2331 }
2332finish:
2333 if ( fFound == 0 )
2334 printf( "Preprocessing not succeded.\n" );
2335 Abc_PrintTime( 1, "Preprocessing time", Abc_Clock() - clk );
2336 // blast AIGs again
2337 Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
2338 if ( p != p1 && p != p2 )
2339 Gia_ManStopP( &p->pGia );
2340 //Rtl_LibBlast( pLib );
2341 Rtl_LibBlast2( pLib, NULL, 0 );
2342}
2343void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
2344{
2345 extern Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p );
2346 abctime clk = Abc_Clock(); int Status;
2347 Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
2348 Gia_Man_t * pGia2 = Gia_ManReduceBuffers( pLib, pTop->pGia );
2349 Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pGia2, 1000000, 0 );
2350 int RetValue = Gia_ManAndNum(pSwp);
2351 char * pFileName = "miter_to_solve.aig";
2352 printf( "Dumped the miter into file \"%s\".\n", pFileName );
2353 Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
2354 Gia_ManStop( pSwp );
2355 Gia_ManStop( pGia2 );
2356 if ( RetValue == 0 )
2357 printf( "Verification problem solved after SAT sweeping! " );
2358 else
2359 {
2360 Gia_Man_t * pCopy = Gia_ManDup( pTop->pGia );
2361 Gia_ManInvertPos( pCopy );
2362 Gia_ManAppendCo( pCopy, 0 );
2363 Status = Cec_ManVerifySimple( pCopy );
2364 Gia_ManStop( pCopy );
2365 if ( Status == 1 )
2366 printf( "Verification problem solved after CEC! " );
2367 else
2368 printf( "Verification problem is NOT solved (miter has %d nodes)! ", RetValue );
2369 }
2370 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2371}
2372
2373
2385void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
2386{
2387 abctime clk = Abc_Clock();
2388 Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
2389 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
2390 printf( "\nProving equivalence of \"%s\" and \"%s\"...\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
2391 if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) ||
2392 Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) )
2393 {
2394 printf( "The number of inputs/outputs does not match.\n" );
2395 }
2396 else if ( 1 )
2397 {
2398 Gia_Man_t * pGia = Gia_ManMiter( pNtk1->pGia, pNtk2->pGia, 0, 0, 0, 0, 0 );
2399 if ( Abc_NtkFromGiaCollapse( pGia ) )
2400 Abc_Print( 1, "Networks are equivalent after collapsing. " );
2401 else
2402 {
2403 Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
2404 //printf( "Miter %d -> %d\n", Gia_ManAndNum(pGia), Gia_ManAndNum(pNew) );
2405 if ( Gia_ManAndNum(pNew) == 0 )
2406 Abc_Print( 1, "Networks are equivalent. " );
2407 else
2408 Abc_Print( 1, "Networks are UNDECIDED. " );
2409 Gia_ManStopP( &pNew );
2410 Gia_ManStopP( &pGia );
2411 }
2412 }
2413 else
2414 {
2415 int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 );
2416 if ( Status == 1 )
2417 printf( "The networks are equivalent. " );
2418 else
2419 printf( "The networks are NOT equivalent. " );
2420 }
2421 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2422}
2423int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts )
2424{
2425 int i, * pWire, Counts[4] = {0}, nBits = 0;
2426 assert( p->nOutputs == 1 );
2427 Rtl_NtkForEachWire( p, pWire, i )
2428 {
2429 if ( pWire[0] & 1 ) // PI
2430 Counts[0]++, Counts[1] += pWire[1];
2431 if ( pWire[0] & 2 ) // PO
2432 Counts[2]++, Counts[3] += pWire[1];
2433 }
2434 assert( p->nInputs == Counts[0] );
2435 assert( p->nOutputs == Counts[2] );
2436 *pnOuts = Counts[3];
2437 Rtl_NtkForEachWire( p, pWire, i )
2438 {
2439 if ( pWire[0] & 1 ) // PI
2440 {
2441 if ( pWire[1] == Counts[3] )
2442 return nBits;
2443 nBits += pWire[1];
2444 }
2445 }
2446 return -1;
2447}
2448Gia_Man_t * Gia_ManMoveSharedFirst( Gia_Man_t * pGia, int iFirst, int nBits )
2449{
2450 Vec_Int_t * vPiPerm = Vec_IntAlloc( Gia_ManPiNum(pGia) );
2451 Gia_Man_t * pTemp; int i, n;
2452 for ( n = 0; n < 2; n++ )
2453 for ( i = 0; i < Gia_ManPiNum(pGia); i++ )
2454 if ( n == (i >= iFirst && i < iFirst + nBits) )
2455 Vec_IntPush( vPiPerm, i );
2456 pTemp = Gia_ManDupPerm( pGia, vPiPerm );
2457 if ( pGia->vBarBufs )
2458 pTemp->vBarBufs = Vec_IntDup( pGia->vBarBufs );
2459 Vec_IntFree( vPiPerm );
2460 return pTemp;
2461}
2462Vec_Int_t * Gia_ManCollectBufs( Gia_Man_t * p, int iFirst, int nBufs )
2463{
2464 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
2465 Gia_Obj_t * pObj; int i, iBuf = 0;
2466 assert( iFirst >= 0 && iFirst + nBufs < p->nBufs );
2467 Gia_ManForEachAnd( p, pObj, i )
2468 {
2469 if ( Gia_ObjIsBuf(pObj) && iBuf >= iFirst && iBuf < iFirst + nBufs )
2470 Vec_IntPush( vRes, i );
2471 iBuf += Gia_ObjIsBuf(pObj);
2472 }
2473 assert( iBuf == p->nBufs );
2474 return vRes;
2475}
2476Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p )
2477{
2478 Gia_Man_t * pNew;
2479 Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
2480 Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0, 64 );
2481 Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280-64, 64 );
2482 //Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0, 1280/2 );
2483 //Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280/2, 1280/2 );
2484 int i, One, Two;
2485 printf( "Reducing %d buffers... Size(vOne) = %d. Size(vTwo) = %d. \n", p->nBufs, Vec_IntSize(vOne), Vec_IntSize(vTwo) );
2486 assert( p->nBufs == 1280 );
2487 Vec_IntForEachEntryTwo( vOne, vTwo, One, Two, i )
2488 Vec_IntWriteEntry( vMap, Two, One );
2489 Vec_IntFree( vOne );
2490 Vec_IntFree( vTwo );
2491Gia_ManPrintStats( p, NULL );
2492 //pNew = Gia_ManDupNoBuf( p );
2493 pNew = Gia_ManDupMap( p, vMap );
2494Gia_ManPrintStats( pNew, NULL );
2495 Vec_IntFree( vMap );
2496 //Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
2497 //printf( "Found %d buffers.\n", p->nBufs );
2498 return pNew;
2499}
2500void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
2501{
2502 abctime clk = Abc_Clock();
2503 Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
2504 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
2505 int Res = printf( "\nProving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
2506 int nOuts1, iFirst1 = Gia_ManFindFirst( pNtk1, &nOuts1 );
2507 int nOuts2, iFirst2 = Gia_ManFindFirst( pNtk2, &nOuts2 );
2508 Gia_Man_t * pGia1 = Gia_ManMoveSharedFirst( pNtk1->pGia, iFirst1, nOuts1 );
2509 Gia_Man_t * pGia2 = Gia_ManMoveSharedFirst( pNtk2->pGia, iFirst2, nOuts2 );
2510 if ( 1 )
2511 {
2512 char * pFileName = "inv_miter.aig";
2513 Gia_Man_t * pGia = Gia_ManMiterInverse( pGia1, pGia2, 0, 0 );
2514 //Gia_Man_t * pGia2 = Gia_ManReduceBuffers( p, pGia );
2515 Gia_Man_t * pGia2 = Gia_ManDupNoBuf( pGia );
2516 printf( "Dumping inverse miter into file \"%s\".\n", pFileName );
2517 Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
2518 printf( "Dumped the miter into file \"%s\".\n", pFileName );
2519 if ( Abc_NtkFromGiaCollapse( pGia2 ) )
2520 Abc_Print( 1, "Networks are equivalent after collapsing. " );
2521 else
2522 {
2523 Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia2, 10000000, 0 );
2524 Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
2525 //printf( "Miter %d -> %d\n", Gia_ManAndNum(pGia), Gia_ManAndNum(pNew) );
2526 if ( Gia_ManAndNum(pNew) == 0 )
2527 Abc_Print( 1, "Networks are equivalent. " );
2528 else
2529 Abc_Print( 1, "Networks are UNDECIDED. " );
2530 Gia_ManStopP( &pNew );
2531 }
2532 Gia_ManStopP( &pGia2 );
2533 Gia_ManStopP( &pGia );
2534 }
2535 else
2536 {
2537 int Status = Cec_ManVerifyTwoInv( pGia1, pGia2, 0 );
2538 if ( Status == 1 )
2539 printf( "The networks are equivalent. " );
2540 else
2541 printf( "The networks are NOT equivalent. " );
2542 }
2543 Res = 0;
2544 Gia_ManStopP( &pGia1 );
2545 Gia_ManStopP( &pGia2 );
2546 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2547}
2548void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
2549{
2550 Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
2551 printf( "\nProving property \"%s\".\n", Rtl_NtkName(pNtk) );
2552 Rtl_NtkPrintBufs( pNtk, pNtk->pGia->vBarBufs );
2553 Rtl_LibSolve( p, pNtk );
2554}
2555Vec_Int_t * Wln_ReadNtkRoots( Rtl_Lib_t * p, Vec_Wec_t * vGuide )
2556{
2557 Vec_Int_t * vLevel; int i;
2558 Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
2559 Vec_WecForEachLevel( vGuide, vLevel, i )
2560 {
2561 int Name1 = Vec_IntEntry( vLevel, 2 );
2562 int Name2 = Vec_IntEntry( vLevel, 3 );
2563 int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 );
2564 if ( iNtk == -1 )
2565 {
2566 printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) );
2567 break;
2568 }
2569/*
2570 else
2571 {
2572 Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk >> 16 );
2573 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk & 0xFFFF );
2574 printf( "Matching \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
2575 }
2576*/
2577 Vec_IntPushTwo( vRoots, iNtk >> 16, iNtk & 0xFFFF );
2578 }
2579 return vRoots;
2580}
2581void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
2582{
2583 extern Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
2584 Vec_Wec_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName );
2585 Vec_Int_t * vRoots, * vLevel; int i, iNtk1, iNtk2, fInv = 0;
2586 Vec_WecForEachLevel( vGuide, vLevel, i )
2587 if ( Vec_IntEntry( vLevel, 1 ) == Rtl_LibStrId(p, "inverse") )
2588 fInv = 1;
2589 Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
2590 Rtl_LibSetReplace( p, vGuide );
2591 Rtl_LibUpdateBoxes( p );
2592 Rtl_LibReorderModules( p );
2593 vRoots = Wln_ReadNtkRoots( p, vGuide );
2594 Rtl_LibBlast2( p, vRoots, fInv );
2595 Vec_WecForEachLevel( vGuide, vLevel, i )
2596 {
2597 int Prove = Vec_IntEntry( vLevel, 0 );
2598 int Type = Vec_IntEntry( vLevel, 1 );
2599 int Name1 = Vec_IntEntry( vLevel, 2 );
2600 int Name2 = Vec_IntEntry( vLevel, 3 );
2601 int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 );
2602 if ( iNtk == -1 )
2603 {
2604 printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) );
2605 break;
2606 }
2607 iNtk1 = iNtk >> 16;
2608 iNtk2 = iNtk & 0xFFFF;
2609 if ( Prove != Rtl_LibStrId(p, "prove") )
2610 printf( "Unknown task in line %d.\n", i );
2611 //else if ( iNtk1 == -1 )
2612 // printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) );
2613 else
2614 {
2615 if ( Type == Rtl_LibStrId(p, "equal") )
2616 Wln_SolveEqual( p, iNtk1, iNtk2 );
2617 else if ( Type == Rtl_LibStrId(p, "inverse") )
2618 Wln_SolveInverse( p, iNtk1, iNtk2 );
2619 else if ( Type == Rtl_LibStrId(p, "property") )
2620 Wln_SolveProperty( p, iNtk1 );
2621 continue;
2622 }
2623 break;
2624 }
2625 Rtl_LibBlastClean( p );
2626 Vec_WecFree( vGuide );
2627 Vec_IntFree( vRoots );
2628}
2629
2641
2642static inline void Gia_ManPatchBufDriver( Gia_Man_t * p, int iObj, int iLit0 )
2643{
2644 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
2645 assert( iObj > Abc_Lit2Var(iLit0) );
2646 pObj->iDiff0 = pObj->iDiff1 = iObj - Abc_Lit2Var(iLit0);
2647 pObj->fCompl0 = pObj->fCompl1 = Abc_LitIsCompl(iLit0);
2648}
2649
2650Gia_Man_t * Rtl_ReduceInverse( Rtl_Lib_t * pLib, Gia_Man_t * p )
2651{
2652 int fVerbose = 1;
2653 Gia_Man_t * pNew = NULL;
2654 Vec_Wec_t * vBufs = Vec_WecStart( Vec_IntSize(p->vBarBufs) );
2655 Vec_Int_t * vPairs = Vec_IntAlloc( 10 );
2656 Vec_Int_t * vTypes = Vec_IntAlloc( p->nBufs );
2657 Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
2658 Gia_Obj_t * pObj; int i, k = 0, Entry, Buf0, Buf1, fChange = 1;
2659 Vec_IntForEachEntry( p->vBarBufs, Entry, i )
2660 Vec_IntFillExtra( vTypes, Vec_IntSize(vTypes) + (Entry >> 16), i );
2661 assert( Vec_IntSize(vTypes) == p->nBufs );
2662 Gia_ManForEachAnd( p, pObj, i )
2663 if ( Gia_ObjIsBuf(pObj) )
2664 {
2665 Vec_WecPush( vBufs, Vec_IntEntry(vTypes, k), i );
2666 Vec_IntWriteEntry( vMap, i, Vec_IntEntry(vTypes, k++) );
2667 }
2668 assert( k == p->nBufs );
2669 Gia_ManForEachAnd( p, pObj, i )
2670 if ( Gia_ObjIsBuf(pObj) && Gia_ObjIsBuf(Gia_ObjFanin0(pObj)) )
2671 Vec_IntPushUnique( vPairs, (Vec_IntEntry(vMap, Gia_ObjFaninId0(pObj, i)) << 16) | (Vec_IntEntry(vMap, i) & 0xFFFF) );
2672 if ( fVerbose )
2673 {
2674 printf( "Connected boundaries:\n" );
2675 Vec_IntForEachEntry( vPairs, Entry, i )
2676 {
2677 printf( "%2d -> %2d : ", Entry >> 16, Entry & 0xFFFF );
2678 Rtl_NtkPrintBufOne( pLib, Vec_IntEntry(p->vBarBufs, Entry >> 16) );
2679 printf( " -> " );
2680 Rtl_NtkPrintBufOne( pLib, Vec_IntEntry(p->vBarBufs, Entry & 0xFFFF) );
2681 printf( "\n" );
2682 }
2683 }
2684 while ( fChange )
2685 {
2686 int Entry1, Entry2, j;
2687 fChange = 0;
2688 Vec_IntForEachEntryDouble( vPairs, Entry1, Entry2, j )
2689 if ( (Entry1 & 0xFFFF) + 1 == (Entry2 >> 16) )
2690 {
2691 Vec_IntWriteEntry( vPairs, j, ((Entry1 >> 16) << 16) | (Entry2 & 0xFFFF) );
2692 Vec_IntDrop( vPairs, j+1 );
2693 fChange = 1;
2694 break;
2695 }
2696 }
2697// printf( "Before:\n" );
2698// Vec_IntForEachEntry( vPairs, Entry, i )
2699// printf( "%d %d\n", Entry >> 16, Entry & 0xFFFF );
2700 Vec_IntForEachEntry( vPairs, Entry, i )
2701 Vec_IntWriteEntry( vPairs, i, (((Entry >> 16) - 1) << 16) | ((Entry & 0xFFFF) + 1) );
2702// printf( "After:\n" );
2703// Vec_IntForEachEntry( vPairs, Entry, i )
2704// printf( "%d %d\n", Entry >> 16, Entry & 0xFFFF );
2705 if ( fVerbose )
2706 {
2707 printf( "Transformed boundaries:\n" );
2708 Vec_IntForEachEntry( vPairs, Entry, i )
2709 {
2710 printf( "%2d -> %2d : ", Entry >> 16, Entry & 0xFFFF );
2711 Rtl_NtkPrintBufOne( pLib, Vec_IntEntry(p->vBarBufs, Entry >> 16) );
2712 printf( " -> " );
2713 Rtl_NtkPrintBufOne( pLib, Vec_IntEntry(p->vBarBufs, Entry & 0xFFFF) );
2714 printf( "\n" );
2715 }
2716 }
2717 Vec_IntForEachEntry( vPairs, Entry, i )
2718 {
2719 Vec_Int_t * vLevel0 = Vec_WecEntry( vBufs, Entry >> 16 );
2720 Vec_Int_t * vLevel1 = Vec_WecEntry( vBufs, Entry & 0xFFFF );
2721 Vec_IntForEachEntryTwo( vLevel0, vLevel1, Buf0, Buf1, k )
2722 Gia_ManPatchBufDriver( p, Buf1, Gia_ObjFaninLit0(Gia_ManObj(p, Buf0), Buf0) );
2723 }
2724 pNew = Gia_ManRehash( p, 0 );
2725 Vec_IntFree( vPairs );
2726 Vec_IntFree( vTypes );
2727 Vec_IntFree( vMap );
2728 Vec_WecFree( vBufs );
2729 return pNew;
2730}
2731
2743Gia_Man_t * Gia_ManDupPermIO( Gia_Man_t * p, Vec_Int_t * vPermI, Vec_Int_t * vPermO )
2744{
2745 Gia_Man_t * pNew;
2746 Gia_Obj_t * pObj;
2747 int i;
2748 assert( Vec_IntSize(vPermI) == Gia_ManCiNum(p) );
2749 assert( Vec_IntSize(vPermO) == Gia_ManCoNum(p) );
2750 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2751 pNew->pName = Abc_UtilStrsav(p->pName);
2752 Gia_ManConst0(p)->Value = 0;
2753 Gia_ManForEachCi( p, pObj, i )
2754 Gia_ManCi(p, Vec_IntEntry(vPermI, i))->Value = Gia_ManAppendCi(pNew);
2755 Gia_ManForEachAnd( p, pObj, i )
2756 {
2757 if ( Gia_ObjIsBuf(pObj) )
2758 pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
2759 else
2760 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2761 assert( Abc_Lit2Var(pObj->Value) == i );
2762 }
2763 Gia_ManForEachCo( p, pObj, i )
2764 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, Vec_IntEntry(vPermO, i))) );
2765 return pNew;
2766}
2767
2779int Rtl_LibReturnNtk( Rtl_Lib_t * p, char * pModule )
2780{
2781 int NameId = Wln_ReadFindToken( pModule, p->pManName );
2782 int iNtk = NameId ? Rtl_LibFindModule( p, NameId ) : -1;
2783 if ( iNtk == -1 )
2784 {
2785 printf( "Cannot find module \"%s\" in the current design.\n", pModule );
2786 return -1;
2787 }
2788 return iNtk;
2789}
2790Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose )
2791{
2792 Gia_Man_t * pGia = NULL;
2793 int NameId = Wln_ReadFindToken( pTopModule, p->pManName );
2794 int iNtk = NameId ? Rtl_LibFindModule( p, NameId ) : -1;
2795 if ( iNtk == -1 )
2796 {
2797 printf( "Cannot find top module \"%s\".\n", pTopModule );
2798 return NULL;
2799 }
2800 else
2801 {
2802 abctime clk = Abc_Clock();
2803 Rtl_Ntk_t * pTop = Rtl_LibNtk(p, iNtk);
2804 Vec_Int_t * vRoots = Vec_IntAlloc( 1 );
2805 Vec_IntPush( vRoots, iNtk );
2806 Rtl_LibBlast2( p, vRoots, 1 );
2807 pGia = Gia_ManDup( pTop->pGia );
2808 if ( fRev )
2809 {
2810 Gia_Man_t * pTemp;
2811 Vec_Int_t * vPermI = Rtl_NtkRevPermInput( pTop );
2812 Vec_Int_t * vPermO = Rtl_NtkRevPermOutput( pTop );
2813 pGia = Gia_ManDupPermIO( pTemp = pGia, vPermI, vPermO );
2814 Vec_IntFree( vPermI );
2815 Vec_IntFree( vPermO );
2816 Gia_ManStop( pTemp );
2817 }
2818 //Gia_AigerWrite( pGia, "temp_miter.aig", 0, 0, 0 );
2819 if ( pTop->pGia->vBarBufs )
2820 pGia->vBarBufs = Vec_IntDup( pTop->pGia->vBarBufs );
2821 printf( "Derived global AIG for the top module \"%s\". ", Rtl_NtkStr(pTop, NameId) );
2822 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
2823 Rtl_NtkPrintBufs( pTop, pGia->vBarBufs );
2824 Rtl_LibBlastClean( p );
2825 Vec_IntFree( vRoots );
2826 if ( p->vInverses )
2827 {
2828 Gia_Man_t * pTemp;
2829 pGia = Rtl_ReduceInverse( p, pTemp = pGia );
2830 Gia_ManStop( pTemp );
2831 }
2832 }
2833 return pGia;
2834}
2835
2847void Wln_LibGraftOne( Rtl_Lib_t * p, char ** pModules, int nModules, int fInv, int fVerbose )
2848{
2849 if ( nModules == 0 )
2850 {
2851 Rtl_Ntk_t * pNtk; int i;
2852 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
2853 pNtk->iCopy = -1;
2854 Vec_IntFreeP( &p->vInverses );
2855 if ( p->vDirects )
2856 {
2857 int iName1, iName2;
2858 Vec_IntForEachEntryDouble( p->vDirects, iName1, iName2, i )
2859 {
2860 int iNtk1 = Rtl_LibFindModule(p, iName1);
2861 int iNtk2 = Rtl_LibFindModule(p, iName2);
2862 //Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
2863 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
2864 pNtk2->iCopy = iNtk1;
2865 }
2866 Rtl_LibUpdateBoxes( p );
2867 Rtl_LibReorderModules( p );
2868 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
2869 pNtk->iCopy = -1;
2870 Vec_IntFreeP( &p->vDirects );
2871 }
2872 }
2873 else
2874 {
2875 int Name1 = Wln_ReadFindToken( pModules[0], p->pManName );
2876 int Name2 = Wln_ReadFindToken( pModules[1], p->pManName );
2877 int iNtk = Rtl_LibFindTwoModules( p, Name1, Name2 );
2878 if ( iNtk == -1 )
2879 {
2880 printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) );
2881 return;
2882 }
2883 else
2884 {
2885 int iNtk1 = iNtk >> 16;
2886 int iNtk2 = iNtk & 0xFFFF;
2887 Rtl_Ntk_t * pNtk1 = Rtl_LibNtk(p, iNtk1);
2888 Rtl_Ntk_t * pNtk2 = Rtl_LibNtk(p, iNtk2);
2889 assert( iNtk1 != iNtk2 );
2890 if ( fInv )
2891 {
2892 printf( "Setting \"%s\" (appearing %d times) and \"%s\" (appearing %d times) as inverse-equivalent.\n",
2893 Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
2894 if ( p->vInverses == NULL )
2895 p->vInverses = Vec_IntAlloc( 10 );
2896 Vec_IntPushTwo( p->vInverses, pNtk1->NameId, pNtk2->NameId );
2897 }
2898 else
2899 {
2900 printf( "Replacing \"%s\" (appearing %d times) by \"%s\" (appearing %d times).\n",
2901 Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
2902 pNtk1->iCopy = iNtk2;
2903 // Rtl_LibSetReplace( p, vGuide );
2904 Rtl_LibUpdateBoxes( p );
2905 Rtl_LibReorderModules( p );
2906 if ( p->vDirects == NULL )
2907 p->vDirects = Vec_IntAlloc( 10 );
2908 Vec_IntPushTwo( p->vDirects, pNtk1->NameId, pNtk2->NameId );
2909 }
2910 }
2911 }
2912}
2913
2925void Wln_LibMarkHierarchy( Rtl_Lib_t * p, char ** ppModule, int nModules, int fVerbose )
2926{
2927 Rtl_Ntk_t * pNtk; int i;
2928 if ( nModules == 0 ) // clean labels
2929 Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
2930 pNtk->fRoot = 0;
2931 for ( i = 0; i < nModules; i++ )
2932 {
2933 int iNtk = Rtl_LibReturnNtk( p, ppModule[i] );
2934 if ( iNtk == -1 )
2935 continue;
2936 pNtk = Rtl_LibNtk( p, iNtk );
2937 pNtk->fRoot = 1;
2938 printf( "Marking module \"%s\" (appearing %d times in the hierarchy).\n", ppModule[i], Rtl_LibCountInsts(p, pNtk) );
2939 }
2940}
2941
2945
2946
2947ABC_NAMESPACE_IMPL_END
2948
nWords
int nWords
Definition abcNpn.c:127
ABC_OPER_DFF
@ ABC_OPER_DFF
Definition abcOper.h:142
ABC_OPER_COMP_LESS
@ ABC_OPER_COMP_LESS
Definition abcOper.h:112
ABC_OPER_LOGIC_OR
@ ABC_OPER_LOGIC_OR
Definition abcOper.h:86
ABC_OPER_RED_XOR
@ ABC_OPER_RED_XOR
Definition abcOper.h:80
ABC_OPER_COMP_EQU
@ ABC_OPER_COMP_EQU
Definition abcOper.h:116
ABC_OPER_ARI_MUL
@ ABC_OPER_ARI_MUL
Definition abcOper.h:101
ABC_OPER_SEL_NMUX
@ ABC_OPER_SEL_NMUX
Definition abcOper.h:91
ABC_OPER_SHIFT_RA
@ ABC_OPER_SHIFT_RA
Definition abcOper.h:122
ABC_OPER_BIT_XOR
@ ABC_OPER_BIT_XOR
Definition abcOper.h:61
ABC_OPER_COMP_MORE
@ ABC_OPER_COMP_MORE
Definition abcOper.h:115
ABC_OPER_NONE
@ ABC_OPER_NONE
Definition abcOper.h:42
ABC_OPER_RED_NXOR
@ ABC_OPER_RED_NXOR
Definition abcOper.h:81
ABC_OPER_SHIFT_L
@ ABC_OPER_SHIFT_L
Definition abcOper.h:119
ABC_OPER_LAST
@ ABC_OPER_LAST
Definition abcOper.h:157
ABC_OPER_LOGIC_NOT
@ ABC_OPER_LOGIC_NOT
Definition abcOper.h:83
ABC_OPER_ARI_DIV
@ ABC_OPER_ARI_DIV
Definition abcOper.h:103
ABC_OPER_RED_AND
@ ABC_OPER_RED_AND
Definition abcOper.h:76
ABC_OPER_RED_OR
@ ABC_OPER_RED_OR
Definition abcOper.h:78
ABC_OPER_SEL_SEL
@ ABC_OPER_SEL_SEL
Definition abcOper.h:92
ABC_OPER_ARI_POW
@ ABC_OPER_ARI_POW
Definition abcOper.h:106
ABC_OPER_COMP_LESSEQU
@ ABC_OPER_COMP_LESSEQU
Definition abcOper.h:113
ABC_OPER_LOGIC_AND
@ ABC_OPER_LOGIC_AND
Definition abcOper.h:84
ABC_OPER_COMP_MOREEQU
@ ABC_OPER_COMP_MOREEQU
Definition abcOper.h:114
ABC_OPER_ARI_MOD
@ ABC_OPER_ARI_MOD
Definition abcOper.h:104
ABC_OPER_SHIFT_R
@ ABC_OPER_SHIFT_R
Definition abcOper.h:120
ABC_OPER_SHIFT_LA
@ ABC_OPER_SHIFT_LA
Definition abcOper.h:121
ABC_OPER_BIT_INV
@ ABC_OPER_BIT_INV
Definition abcOper.h:56
ABC_OPER_BIT_AND
@ ABC_OPER_BIT_AND
Definition abcOper.h:57
ABC_OPER_COMP_NOTEQU
@ ABC_OPER_COMP_NOTEQU
Definition abcOper.h:117
ABC_OPER_BIT_OR
@ ABC_OPER_BIT_OR
Definition abcOper.h:59
ABC_OPER_BIT_BUF
@ ABC_OPER_BIT_BUF
Definition abcOper.h:55
ABC_OPER_ARI_SUB
@ ABC_OPER_ARI_SUB
Definition abcOper.h:100
ABC_OPER_BIT_NXOR
@ ABC_OPER_BIT_NXOR
Definition abcOper.h:62
ABC_OPER_ARI_MIN
@ ABC_OPER_ARI_MIN
Definition abcOper.h:107
ABC_OPER_ARI_ADD
@ ABC_OPER_ARI_ADD
Definition abcOper.h:99
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Abc_MergeSortCost
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition utilSort.c:442
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cec_ManVerifyTwoInv
int Cec_ManVerifyTwoInv(Gia_Man_t *p0, Gia_Man_t *p1, int fVerbose)
Definition cecCec.c:468
Cec_ManVerifySimple
int Cec_ManVerifySimple(Gia_Man_t *p)
Definition cecCec.c:432
Cec_ManVerifyTwo
int Cec_ManVerifyTwo(Gia_Man_t *p0, Gia_Man_t *p1, int fVerbose)
Definition cecCec.c:453
p
Cube * p
Definition exorList.c:222
Extra_TimeStamp
char * Extra_TimeStamp()
Definition extraUtilFile.c:465
Gia_ManDupRebuild
void Gia_ManDupRebuild(Gia_Man_t *pNew, Gia_Man_t *p, Vec_Int_t *vLits, int fBufs)
Definition giaDup.c:1215
MAX_LINE
#define MAX_LINE
DECLARATIONS ///.
Definition giaGig.c:32
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition giaMan.c:224
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManRehash
Gia_Man_t * Gia_ManRehash(Gia_Man_t *p, int fAddStrash)
Definition giaHash.c:739
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManDupPerm
Gia_Man_t * Gia_ManDupPerm(Gia_Man_t *p, Vec_Int_t *vPiPerm)
Definition giaDup.c:929
Gia_ManInvertPos
void Gia_ManInvertPos(Gia_Man_t *pAig)
Definition giaUtil.c:1651
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManDupMap
Gia_Man_t * Gia_ManDupMap(Gia_Man_t *p, Vec_Int_t *vMap)
Definition giaDup.c:846
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManDupNoBuf
Gia_Man_t * Gia_ManDupNoBuf(Gia_Man_t *p)
Definition giaDup.c:823
Gia_ManMiterInverse
Gia_Man_t * Gia_ManMiterInverse(Gia_Man_t *pBot, Gia_Man_t *pTop, int fDualOut, int fVerbose)
Definition giaDup.c:3130
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition giaDup.c:2983
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Gia_Man_t_::vBarBufs
Vec_Int_t * vBarBufs
Definition gia.h:163
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::iDiff1
unsigned iDiff1
Definition gia.h:84
Gia_Obj_t_::fCompl1
unsigned fCompl1
Definition gia.h:85
Gia_Obj_t_::fCompl0
unsigned fCompl0
Definition gia.h:80
Gia_Obj_t_::iDiff0
unsigned iDiff0
Definition gia.h:79
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Rtl_Lib_t_
Definition wlnRead.c:40
Rtl_Lib_t_::pFile
FILE * pFile
Definition wlnRead.c:47
Rtl_Lib_t_::vInverses
Vec_Int_t * vInverses
Definition wlnRead.c:52
Rtl_Lib_t_::vAttrTemp
Vec_Int_t vAttrTemp
Definition wlnRead.c:53
Rtl_Lib_t_::vConcats
Vec_Int_t vConcats
Definition wlnRead.c:46
Rtl_Lib_t_::vMap
Vec_Int_t * vMap
Definition wlnRead.c:50
Rtl_Lib_t_::vSlices
Vec_Int_t vSlices
Definition wlnRead.c:45
Rtl_Lib_t_::vNtks
Vec_Ptr_t * vNtks
Definition wlnRead.c:42
Rtl_Lib_t_::vDirects
Vec_Int_t * vDirects
Definition wlnRead.c:51
Rtl_Lib_t_::vTemp
Vec_Int_t vTemp[TEMP_NUM]
Definition wlnRead.c:54
Rtl_Lib_t_::pManName
Abc_Nam_t * pManName
Definition wlnRead.c:43
Rtl_Lib_t_::pMap
int pMap[MAX_MAP]
Definition wlnRead.c:49
Rtl_Lib_t_::pSpec
char * pSpec
Definition wlnRead.c:41
Rtl_Lib_t_::vConsts
Vec_Int_t vConsts
Definition wlnRead.c:44
Rtl_Lib_t_::vTokens
Vec_Int_t * vTokens
Definition wlnRead.c:48
Rtl_Ntk_t_
Definition wlnRead.c:59
Rtl_Ntk_t_::nOutputs
int nOutputs
Definition wlnRead.c:62
Rtl_Ntk_t_::vStore
Vec_Int_t vStore
Definition wlnRead.c:66
Rtl_Ntk_t_::vOrder
Vec_Int_t vOrder
Definition wlnRead.c:69
Rtl_Ntk_t_::nInputs
int nInputs
Definition wlnRead.c:61
Rtl_Ntk_t_::vCells
Vec_Int_t vCells
Definition wlnRead.c:64
Rtl_Ntk_t_::vConns
Vec_Int_t vConns
Definition wlnRead.c:65
Rtl_Ntk_t_::fRoot
int fRoot
Definition wlnRead.c:78
Rtl_Ntk_t_::pGia
Gia_Man_t * pGia
Definition wlnRead.c:74
Rtl_Ntk_t_::vAttrs
Vec_Int_t vAttrs
Definition wlnRead.c:67
Rtl_Ntk_t_::vBitTemp2
Vec_Int_t vBitTemp2
Definition wlnRead.c:73
Rtl_Ntk_t_::vLits
Vec_Int_t vLits
Definition wlnRead.c:70
Rtl_Ntk_t_::vBitTemp
Vec_Int_t vBitTemp
Definition wlnRead.c:72
Rtl_Ntk_t_::iCopy
int iCopy
Definition wlnRead.c:77
Rtl_Ntk_t_::vDrivers
Vec_Int_t vDrivers
Definition wlnRead.c:71
Rtl_Ntk_t_::pLib
Rtl_Lib_t * pLib
Definition wlnRead.c:68
Rtl_Ntk_t_::NameId
int NameId
Definition wlnRead.c:60
Rtl_Ntk_t_::Slice1
int Slice1
Definition wlnRead.c:76
Rtl_Ntk_t_::Slice0
int Slice0
Definition wlnRead.c:75
Rtl_Ntk_t_::vWires
Vec_Int_t vWires
Definition wlnRead.c:63
counter
Definition walk.c:35
Abc_NamStrFind
int Abc_NamStrFind(Abc_Nam_t *p, char *pStr)
Definition utilNam.c:433
Abc_NamStop
void Abc_NamStop(Abc_Nam_t *p)
Definition utilNam.c:112
Abc_NamStrFindOrAdd
int Abc_NamStrFindOrAdd(Abc_Nam_t *p, char *pStr, int *pfFound)
Definition utilNam.c:453
Abc_NamObjNumMax
int Abc_NamObjNumMax(Abc_Nam_t *p)
Definition utilNam.c:231
Abc_NamStart
Abc_Nam_t * Abc_NamStart(int nObjs, int nAveSize)
FUNCTION DEFINITIONS ///.
Definition utilNam.c:80
Abc_NamStr
char * Abc_NamStr(Abc_Nam_t *p, int NameId)
Definition utilNam.c:555
Abc_Nam_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Nam_t_ Abc_Nam_t
INCLUDES ///.
Definition utilNam.h:39
assert
#define assert(ex)
Definition util_old.h:213
strncmp
int strncmp()
memcpy
char * memcpy()
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strtok
char * strtok()
strstr
char * strstr()
strcat
char * strcat()
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryTwo
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition vecInt.h:66
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition vecInt.h:60
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Rtl_NtkBlastNode
void Rtl_NtkBlastNode(Gia_Man_t *pNew, int Type, int nIns, Vec_Int_t *vDatas, int nRange, int fSign0, int fSign1)
Definition wlnBlast.c:61
Wln_ReadGuidance
Vec_Wec_t * Wln_ReadGuidance(char *pFileName, Abc_Nam_t *p)
Definition wlnGuide.c:61
Gia_ManMoveSharedFirst
Gia_Man_t * Gia_ManMoveSharedFirst(Gia_Man_t *pGia, int iFirst, int nBits)
Definition wlnRead.c:2448
Rtl_NtkReadConst
int Rtl_NtkReadConst(Rtl_Ntk_t *p, char *pConst)
Definition wlnRead.c:1167
Rtl_NtkPrintSig
void Rtl_NtkPrintSig(Rtl_Ntk_t *p, int Sig)
Definition wlnRead.c:1075
Rtl_NtkRevPermOutput
Vec_Int_t * Rtl_NtkRevPermOutput(Rtl_Ntk_t *p)
Definition wlnRead.c:1751
Rtl_LibFree
void Rtl_LibFree(Rtl_Lib_t *p)
Definition wlnRead.c:318
Rtl_NtkReadType
int Rtl_NtkReadType(Rtl_Ntk_t *p, int Type)
Definition wlnRead.c:522
Rtl_NtkAlloc
Rtl_Ntk_t * Rtl_NtkAlloc(Rtl_Lib_t *pLib)
FUNCTION DEFINITIONS ///.
Definition wlnRead.c:179
Rtl_NtkPrintCell
void Rtl_NtkPrintCell(Rtl_Ntk_t *p, int *pCell)
Definition wlnRead.c:1098
Rtl_NtkForEachAttr
#define Rtl_NtkForEachAttr(p, Par, Val, i)
Definition wlnRead.c:139
Rtl_NtkPrintConst
void Rtl_NtkPrintConst(Rtl_Ntk_t *p, int *pConst)
Definition wlnRead.c:1047
Rtl_NtkBlastMap
void Rtl_NtkBlastMap(Rtl_Ntk_t *p, int nBits)
Definition wlnRead.c:2062
Rtl_NtkInsertSignalRange
int Rtl_NtkInsertSignalRange(Rtl_Ntk_t *p, int Sig, int *pLits, int nLits)
Definition wlnRead.c:1713
Rtl_Type_t
Rtl_Type_t
Definition wlnRead.c:408
RTL_SIGNED
@ RTL_SIGNED
Definition wlnRead.c:416
RTL_PARAMETER
@ RTL_PARAMETER
Definition wlnRead.c:418
RTL_UNUSED
@ RTL_UNUSED
Definition wlnRead.c:424
RTL_CONNECT
@ RTL_CONNECT
Definition wlnRead.c:420
RTL_END
@ RTL_END
Definition wlnRead.c:411
RTL_INOUT
@ RTL_INOUT
Definition wlnRead.c:414
RTL_OFFSET
@ RTL_OFFSET
Definition wlnRead.c:417
RTL_WIDTH
@ RTL_WIDTH
Definition wlnRead.c:422
RTL_CELL
@ RTL_CELL
Definition wlnRead.c:421
RTL_ATTRIBUTE
@ RTL_ATTRIBUTE
Definition wlnRead.c:423
RTL_OUTPUT
@ RTL_OUTPUT
Definition wlnRead.c:413
RTL_MODULE
@ RTL_MODULE
Definition wlnRead.c:410
RTL_NONE
@ RTL_NONE
Definition wlnRead.c:409
RTL_INPUT
@ RTL_INPUT
Definition wlnRead.c:412
RTL_UPTO
@ RTL_UPTO
Definition wlnRead.c:415
RTL_WIRE
@ RTL_WIRE
Definition wlnRead.c:419
Abc_NtkFromGiaCollapse
int Abc_NtkFromGiaCollapse(Gia_Man_t *pGia)
Definition abcDar.c:676
Rtl_CellForEachParam
#define Rtl_CellForEachParam(p, pCell, Par, Val, i)
Definition wlnRead.c:150
MAX_MAP
#define MAX_MAP
Definition wlnRead.c:32
Rlt_NtkFindIOPerm
int * Rlt_NtkFindIOPerm(Rtl_Ntk_t *p)
Definition wlnRead.c:618
Rtl_NtkCountSliceRange
int Rtl_NtkCountSliceRange(Rtl_Ntk_t *p, int *pSlice)
Definition wlnRead.c:712
Rtl_LibFindTwoModules
int Rtl_LibFindTwoModules(Rtl_Lib_t *p, int Name1, int Name2)
Definition wlnRead.c:361
Rtl_LibOrderCells
void Rtl_LibOrderCells(Rtl_Lib_t *pLib)
Definition wlnRead.c:957
Rtl_LibSolve
void Rtl_LibSolve(Rtl_Lib_t *pLib, void *pNtk)
Definition wlnRead.c:2343
Rtl_NtkPrintHieStats
void Rtl_NtkPrintHieStats(Rtl_Ntk_t *p, int nOffset)
Definition wlnRead.c:265
Rtl_NtkPrintWire
void Rtl_NtkPrintWire(Rtl_Ntk_t *p, int *pWire)
Definition wlnRead.c:1087
Rtl_NtkInsertConcatRange
int Rtl_NtkInsertConcatRange(Rtl_Ntk_t *p, int *pConcat, int *pLits, int nLits)
Definition wlnRead.c:1705
Rtl_TokenUnspace
void Rtl_TokenUnspace(char *p)
Definition wlnRead.c:979
Rtl_NtkBlastOutputs
void Rtl_NtkBlastOutputs(Gia_Man_t *pNew, Rtl_Ntk_t *p)
Definition wlnRead.c:1789
Rtl_NtkSetWireRange
void Rtl_NtkSetWireRange(Rtl_Ntk_t *p, int NameId, int Left, int Right, int Value)
Definition wlnRead.c:791
Rtl_LibCollapse
Gia_Man_t * Rtl_LibCollapse(Rtl_Lib_t *p, char *pTopModule, int fRev, int fVerbose)
Definition wlnRead.c:2790
Rtl_NtkCollectConstInfo
void Rtl_NtkCollectConstInfo(Rtl_Ntk_t *p, int *pConst)
Definition wlnRead.c:1592
Rtl_LibPrintHieStats
void Rtl_LibPrintHieStats(Rtl_Lib_t *p)
Definition wlnRead.c:286
Rtl_NtkSetSliceRange
void Rtl_NtkSetSliceRange(Rtl_Ntk_t *p, int *pSlice, int Value)
Definition wlnRead.c:807
CELL_NUM
#define CELL_NUM
Definition wlnRead.c:33
Rtl_NtkCountConcatRange
int Rtl_NtkCountConcatRange(Rtl_Ntk_t *p, int *pConcat)
Definition wlnRead.c:716
Rtl_CellForEachAttr
#define Rtl_CellForEachAttr(p, pCell, Par, Val, i)
Definition wlnRead.c:148
Rtl_LibMark_rec
void Rtl_LibMark_rec(Rtl_Ntk_t *pNtk)
Definition wlnRead.c:2215
Rtl_NtkMapSignalRange
int Rtl_NtkMapSignalRange(Rtl_Ntk_t *p, int Sig, int iCell, int iBit)
Definition wlnRead.c:1553
Rtl_NtkForEachWire
#define Rtl_NtkForEachWire(p, pWire, i)
Definition wlnRead.c:141
Rtl_NtkReadAttribute2
int Rtl_NtkReadAttribute2(Rtl_Lib_t *p, int iPos)
Definition wlnRead.c:1286
Rtl_LibBlastClean
void Rtl_LibBlastClean(Rtl_Lib_t *p)
Definition wlnRead.c:2254
Rtl_NtkBlast
Gia_Man_t * Rtl_NtkBlast(Rtl_Ntk_t *p)
Definition wlnRead.c:1933
Rtl_NtkCollectSignalRange
void Rtl_NtkCollectSignalRange(Rtl_Ntk_t *p, int Sig)
Definition wlnRead.c:1668
Rtl_NtkCollectWireInfo
void Rtl_NtkCollectWireInfo(Rtl_Ntk_t *p, int NameId, int Left, int Right)
Definition wlnRead.c:1581
Rtl_NtkUpdateBoxes
void Rtl_NtkUpdateBoxes(Rtl_Ntk_t *p)
Definition wlnRead.c:1461
Rtl_NtkCheckWireRange
int Rtl_NtkCheckWireRange(Rtl_Ntk_t *p, int NameId, int Left, int Right)
Definition wlnRead.c:749
Rtl_NtkReviewConnections
int Rtl_NtkReviewConnections(Rtl_Ntk_t *p)
Definition wlnRead.c:885
Rtl_NtkSetSignalRange
void Rtl_NtkSetSignalRange(Rtl_Ntk_t *p, int Sig, int Value)
Definition wlnRead.c:817
Rtl_NtkCollectSignalInfo
void Rtl_NtkCollectSignalInfo(Rtl_Ntk_t *p, int Sig)
Definition wlnRead.c:1610
Gia_ManReduceBuffers
Gia_Man_t * Gia_ManReduceBuffers(Rtl_Lib_t *pLib, Gia_Man_t *p)
Definition wlnRead.c:2476
Rtl_NtkCountWireRange
int Rtl_NtkCountWireRange(Rtl_Ntk_t *p, int NameId)
Definition wlnRead.c:706
Rtl_NtkCellParamValue
int Rtl_NtkCellParamValue(Rtl_Ntk_t *p, int *pCell, char *pParam)
Definition wlnRead.c:1863
Gia_ManCollectBufs
Vec_Int_t * Gia_ManCollectBufs(Gia_Man_t *p, int iFirst, int nBufs)
Definition wlnRead.c:2462
Rtl_LibUpdateBoxes
void Rtl_LibUpdateBoxes(Rtl_Lib_t *p)
Definition wlnRead.c:1471
Rtl_NtkReadCell
int Rtl_NtkReadCell(Rtl_Ntk_t *p, int iPos)
Definition wlnRead.c:1308
Rtl_NtkBlastConnect
void Rtl_NtkBlastConnect(Gia_Man_t *pNew, Rtl_Ntk_t *p, int *pCon)
Definition wlnRead.c:1803
Rtl_NtkOrderWires
void Rtl_NtkOrderWires(Rtl_Ntk_t *p)
Definition wlnRead.c:638
Rtl_LibPreprocess
void Rtl_LibPreprocess(Rtl_Lib_t *pLib)
Definition wlnRead.c:2303
Rtl_NtkBlast2Spec
int Rtl_NtkBlast2Spec(Rtl_Ntk_t *p, int *pCell, int iInput)
Definition wlnRead.c:2103
Rtl_NtkBlastHierarchy
void Rtl_NtkBlastHierarchy(Gia_Man_t *pNew, Rtl_Ntk_t *p, int *pCell)
Definition wlnRead.c:1812
Rtl_NtkReadWire
int Rtl_NtkReadWire(Rtl_Ntk_t *p, int iPos)
Definition wlnRead.c:1241
Rtl_NtkCollectSliceInfo
void Rtl_NtkCollectSliceInfo(Rtl_Ntk_t *p, int *pSlice)
Definition wlnRead.c:1600
Rtl_NtkBlast2
Gia_Man_t * Rtl_NtkBlast2(Rtl_Ntk_t *p)
Definition wlnRead.c:2174
Rtl_NtkBlastPrepareInputs
void Rtl_NtkBlastPrepareInputs(Rtl_Ntk_t *p, int *pCell)
Definition wlnRead.c:2122
Rtl_LibUpdateInstances
void Rtl_LibUpdateInstances(Rtl_Ntk_t *p)
Definition wlnRead.c:653
CONST_SHIFT
#define CONST_SHIFT
Definition wlnRead.c:36
WIRE_NUM
#define WIRE_NUM
Definition wlnRead.c:34
Rtl_NtkPrintBufOne
void Rtl_NtkPrintBufOne(Rtl_Lib_t *p, int Lit)
Definition wlnRead.c:1919
Rtl_NtkReadSlice
int Rtl_NtkReadSlice(Rtl_Ntk_t *p, char *pSlice, int NameId)
Definition wlnRead.c:1192
Rtl_NtkPrintSlice
void Rtl_NtkPrintSlice(Rtl_Ntk_t *p, int *pSlice)
Definition wlnRead.c:1059
Rtl_LibBlast2
void Rtl_LibBlast2(Rtl_Lib_t *pLib, Vec_Int_t *vRoots, int fInv)
Definition wlnRead.c:2229
Rtl_NtkCollectConcatInfo
void Rtl_NtkCollectConcatInfo(Rtl_Ntk_t *p, int *pConcat)
Definition wlnRead.c:1604
Rtl_NtkBlastCons
int Rtl_NtkBlastCons(Rtl_Ntk_t *p)
Definition wlnRead.c:2001
Rtl_CellForEachConnect
#define Rtl_CellForEachConnect(p, pCell, Par, Val, i)
Definition wlnRead.c:152
Rtl_LibBlast
void Rtl_LibBlast(Rtl_Lib_t *pLib)
Definition wlnRead.c:1977
Rtl_LibAlloc
Rtl_Lib_t * Rtl_LibAlloc()
Definition wlnRead.c:309
Wln_SolveEqual
void Wln_SolveEqual(Rtl_Lib_t *p, int iNtk1, int iNtk2)
Definition wlnRead.c:2385
Rtl_LibSetParents
void Rtl_LibSetParents(Rtl_Lib_t *p)
Definition wlnRead.c:1430
Rtl_LibNormRanges
void Rtl_LibNormRanges(Rtl_Lib_t *pLib)
Definition wlnRead.c:597
Rtl_NtkCountSignalRange
int Rtl_NtkCountSignalRange(Rtl_Ntk_t *p, int Sig)
Definition wlnRead.c:723
Rtl_NtkMapConcatRange
int Rtl_NtkMapConcatRange(Rtl_Ntk_t *p, int *pConcat, int iCell, int iBit)
Definition wlnRead.c:1546
TEMP_NUM
#define TEMP_NUM
Definition wlnRead.c:35
Rtl_NtkCountPio
void Rtl_NtkCountPio(Rtl_Ntk_t *p, int Counts[4])
Definition wlnRead.c:206
Rtl_NtkForEachCell
#define Rtl_NtkForEachCell(p, pCell, i)
Definition wlnRead.c:143
Rtl_LibCountInsts
int Rtl_LibCountInsts(Rtl_Lib_t *p, Rtl_Ntk_t *pOne)
Definition wlnRead.c:1449
Rtl_LibSetReplace
void Rtl_LibSetReplace(Rtl_Lib_t *p, Vec_Wec_t *vGuide)
Definition wlnRead.c:2260
Rtl_LibFindModule2
int Rtl_LibFindModule2(Rtl_Lib_t *p, int NameId, int iNtk0)
Definition wlnRead.c:346
Rtl_LibReorderModules_rec
void Rtl_LibReorderModules_rec(Rtl_Ntk_t *p, Vec_Ptr_t *vNew)
Definition wlnRead.c:1436
Rtl_LibPrintStats
void Rtl_LibPrintStats(Rtl_Lib_t *p)
Definition wlnRead.c:386
Rtl_TokenRespace
void Rtl_TokenRespace(char *p)
Definition wlnRead.c:988
Gia_ManFindFirst
int Gia_ManFindFirst(Rtl_Ntk_t *p, int *pnOuts)
Definition wlnRead.c:2423
Rtl_NtkCollectOutputs
Vec_Int_t * Rtl_NtkCollectOutputs(Rtl_Ntk_t *p)
Definition wlnRead.c:846
Rtl_NtkPrintStats
void Rtl_NtkPrintStats(Rtl_Ntk_t *p, int nNameSymbs)
Definition wlnRead.c:241
Rtl_NtkInitInputs
void Rtl_NtkInitInputs(Rtl_Ntk_t *p)
Definition wlnRead.c:830
Rtl_LibPrint
void Rtl_LibPrint(char *pFileName, Rtl_Lib_t *p)
Definition wlnRead.c:1132
Rtl_NtkCollectOrComputeBit
int Rtl_NtkCollectOrComputeBit(Rtl_Ntk_t *p, int iBit)
Definition wlnRead.c:2091
Rtl_NtkBlastOperator
void Rtl_NtkBlastOperator(Gia_Man_t *pNew, Rtl_Ntk_t *p, int *pCell)
Definition wlnRead.c:1880
Rtl_NtkBlastInputs
void Rtl_NtkBlastInputs(Gia_Man_t *pNew, Rtl_Ntk_t *p)
Definition wlnRead.c:1775
Rtl_NtkReadConcat
int Rtl_NtkReadConcat(Rtl_Ntk_t *p, int *pPos)
Definition wlnRead.c:1205
Rtl_Ntk_t
struct Rtl_Ntk_t_ Rtl_Ntk_t
Definition wlnRead.c:57
Rtl_NtkFree
void Rtl_NtkFree(Rtl_Ntk_t *p)
Definition wlnRead.c:191
Rtl_NtkPrintBufs
void Rtl_NtkPrintBufs(Rtl_Ntk_t *p, Vec_Int_t *vBufs)
Definition wlnRead.c:1923
Rtl_NtkPrintUnusedCells
void Rtl_NtkPrintUnusedCells(Rtl_Ntk_t *p)
Definition wlnRead.c:923
Rtl_NtkCollectConstRange
void Rtl_NtkCollectConstRange(Rtl_Ntk_t *p, int *pConst)
Definition wlnRead.c:1650
Rtl_NtkCollectConcatRange
void Rtl_NtkCollectConcatRange(Rtl_Ntk_t *p, int *pConcat)
Definition wlnRead.c:1662
Rtl_NtkReadFile
Vec_Int_t * Rtl_NtkReadFile(char *pFileName, Abc_Nam_t *p)
Definition wlnRead.c:996
Rtl_NtkNormRanges
void Rtl_NtkNormRanges(Rtl_Ntk_t *p)
Definition wlnRead.c:566
Rtl_CellForEachInput
#define Rtl_CellForEachInput(p, pCell, Par, Val, i)
Definition wlnRead.c:155
Wln_ReadMatchEnd
int Wln_ReadMatchEnd(Rtl_Ntk_t *p, int Mod)
Definition wlnRead.c:1348
Rtl_NtkMapSliceRange
int Rtl_NtkMapSliceRange(Rtl_Ntk_t *p, int *pSlice, int iCell, int iBit)
Definition wlnRead.c:1542
Rtl_NtkPrintConcat
void Rtl_NtkPrintConcat(Rtl_Ntk_t *p, int *pConcat)
Definition wlnRead.c:1067
Cec4_ManSimulateTest3
Gia_Man_t * Cec4_ManSimulateTest3(Gia_Man_t *p, int nBTLimit, int fVerbose)
Definition cecSatG2.c:2077
Rtl_NtkForEachCon
#define Rtl_NtkForEachCon(p, pCon, i)
Definition wlnRead.c:145
Rtl_NtkCollectSliceRange
void Rtl_NtkCollectSliceRange(Rtl_Ntk_t *p, int *pSlice)
Definition wlnRead.c:1658
Rtl_NtkPrintConnection
void Rtl_NtkPrintConnection(Rtl_Ntk_t *p, int *pCon)
Definition wlnRead.c:1110
Rtl_NtkCheckSignalRange
int Rtl_NtkCheckSignalRange(Rtl_Ntk_t *p, int Sig)
Definition wlnRead.c:774
Rtl_NtkReadNtk
int Rtl_NtkReadNtk(Rtl_Lib_t *pLib, int Mod)
Definition wlnRead.c:1363
Rtl_NtkMapWireRange
int Rtl_NtkMapWireRange(Rtl_Ntk_t *p, int NameId, int Left, int Right, int iCell, int iBit)
Definition wlnRead.c:1525
Rtl_NtkSetParents
int Rtl_NtkSetParents(Rtl_Ntk_t *p)
Definition wlnRead.c:1413
Rtl_LibReorderModules
void Rtl_LibReorderModules(Rtl_Lib_t *p)
Definition wlnRead.c:1477
Rtl_NtkCheckSliceRange
int Rtl_NtkCheckSliceRange(Rtl_Ntk_t *p, int *pSlice)
Definition wlnRead.c:762
Gia_ManDupPermIO
Gia_Man_t * Gia_ManDupPermIO(Gia_Man_t *p, Vec_Int_t *vPermI, Vec_Int_t *vPermO)
Definition wlnRead.c:2743
Rtl_ShortenName
char * Rtl_ShortenName(char *pName, int nSize)
Definition wlnRead.c:1905
Wln_LibGraftOne
void Wln_LibGraftOne(Rtl_Lib_t *p, char **pModules, int nModules, int fInv, int fVerbose)
Definition wlnRead.c:2847
Rtl_NtkReadConnect
int Rtl_NtkReadConnect(Rtl_Ntk_t *p, int iPos)
Definition wlnRead.c:1297
Wln_ReadNtkRoots
Vec_Int_t * Wln_ReadNtkRoots(Rtl_Lib_t *p, Vec_Wec_t *vGuide)
Definition wlnRead.c:2555
Wln_LibMarkHierarchy
void Wln_LibMarkHierarchy(Rtl_Lib_t *p, char **ppModule, int nModules, int fVerbose)
Definition wlnRead.c:2925
Rtl_NtkPrintCellOrder
void Rtl_NtkPrintCellOrder(Rtl_Ntk_t *p)
Definition wlnRead.c:902
Rtl_NtkCheckConcatRange
int Rtl_NtkCheckConcatRange(Rtl_Ntk_t *p, int *pConcat)
Definition wlnRead.c:766
Rtl_NtkReviewCells
int Rtl_NtkReviewCells(Rtl_Ntk_t *p)
Definition wlnRead.c:864
Wln_SolveWithGuidance
void Wln_SolveWithGuidance(char *pFileName, Rtl_Lib_t *p)
Definition wlnRead.c:2581
Rtl_NtkRevPermInput
Vec_Int_t * Rtl_NtkRevPermInput(Rtl_Ntk_t *p)
Definition wlnRead.c:1739
Rtl_NtkCollectWireRange
void Rtl_NtkCollectWireRange(Rtl_Ntk_t *p, int NameId, int Left, int Right)
Definition wlnRead.c:1636
Rtl_NtkOrderCells
void Rtl_NtkOrderCells(Rtl_Ntk_t *p)
Definition wlnRead.c:935
Rtl_NtkInsertWireRange
int Rtl_NtkInsertWireRange(Rtl_Ntk_t *p, int NameId, int Left, int Right, int *pLits, int nLits)
Definition wlnRead.c:1684
Rtl_NtkPrint
void Rtl_NtkPrint(Rtl_Ntk_t *p)
Definition wlnRead.c:1117
Rtl_NtkBlast2_rec
void Rtl_NtkBlast2_rec(Rtl_Ntk_t *p, int iBit, int *pDriver)
Definition wlnRead.c:2137
Rtl_LibReadFile
Rtl_Lib_t * Rtl_LibReadFile(char *pFileName, char *pFileSpec)
Definition wlnRead.c:1492
Rtl_LibFindModule
int Rtl_LibFindModule(Rtl_Lib_t *p, int NameId)
Definition wlnRead.c:338
Rtl_LibOrderWires
void Rtl_LibOrderWires(Rtl_Lib_t *pLib)
Definition wlnRead.c:681
Rtl_NtkMapWires
void Rtl_NtkMapWires(Rtl_Ntk_t *p, int fUnmap)
Definition wlnRead.c:552
Rtl_NtkReadAttribute
int Rtl_NtkReadAttribute(Rtl_Ntk_t *p, int iPos)
Definition wlnRead.c:1275
Rtl_NtkReportUndefs
void Rtl_NtkReportUndefs(Rtl_Ntk_t *p)
Definition wlnRead.c:1389
Rtl_NtkInsertSliceRange
int Rtl_NtkInsertSliceRange(Rtl_Ntk_t *p, int *pSlice, int *pLits, int nLits)
Definition wlnRead.c:1701
Rtl_NtkRangeWires
int Rtl_NtkRangeWires(Rtl_Ntk_t *p)
Definition wlnRead.c:542
Wln_SolveInverse
void Wln_SolveInverse(Rtl_Lib_t *p, int iNtk1, int iNtk2)
Definition wlnRead.c:2500
Rtl_NtkSetConcatRange
void Rtl_NtkSetConcatRange(Rtl_Ntk_t *p, int *pConcat, int Value)
Definition wlnRead.c:811
Rtl_CellForEachOutput
#define Rtl_CellForEachOutput(p, pCell, Par, Val, i)
Definition wlnRead.c:157
Rtl_ReduceInverse
Gia_Man_t * Rtl_ReduceInverse(Rtl_Lib_t *pLib, Gia_Man_t *p)
Definition wlnRead.c:2650
Wln_ReadFindToken
int Wln_ReadFindToken(char *pToken, Abc_Nam_t *p)
DECLARATIONS ///.
Definition wlnGuide.c:44
Rtl_NtkPrintOpers
void Rtl_NtkPrintOpers(Rtl_Ntk_t *p)
Definition wlnRead.c:219
Wln_SolveProperty
void Wln_SolveProperty(Rtl_Lib_t *p, int iNtk)
Definition wlnRead.c:2548
Rtl_NtkReadSig
int Rtl_NtkReadSig(Rtl_Ntk_t *p, int *pPos)
Definition wlnRead.c:1221
Rtl_LibReadType
int Rtl_LibReadType(char *pType)
Definition wlnRead.c:467
Rtl_LibReturnNtk
int Rtl_LibReturnNtk(Rtl_Lib_t *p, char *pModule)
Definition wlnRead.c:2779
Rtl_Lib_t
struct Rtl_Lib_t_ Rtl_Lib_t
Definition wln.h:255