ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaAigerExt.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/st/st.h"
23#include "map/mio/mio.h"
24#include "map/mio/mioInt.h"
25
27
28
32
36
48Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize )
49{
50 Gia_Rpr_t * pReprs;
51 unsigned char * pStop;
52 int i, Item, fProved, iRepr, iNode;
53 pStop = *ppPos;
54 pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
55 pReprs = ABC_CALLOC( Gia_Rpr_t, nSize );
56 for ( i = 0; i < nSize; i++ )
57 pReprs[i].iRepr = GIA_VOID;
58 iRepr = iNode = 0;
59 while ( *ppPos < pStop )
60 {
61 Item = Gia_AigerReadUnsigned( ppPos );
62 if ( Item & 1 )
63 {
64 iRepr += (Item >> 1);
65 iNode = iRepr;
66 continue;
67 }
68 Item >>= 1;
69 fProved = (Item & 1);
70 Item >>= 1;
71 iNode += Item;
72 pReprs[iNode].fProved = fProved;
73 pReprs[iNode].iRepr = iRepr;
74 assert( iRepr < iNode );
75 }
76 return pReprs;
77}
78unsigned char * Gia_WriteEquivClassesInt( Gia_Man_t * p, int * pEquivSize )
79{
80 unsigned char * pBuffer;
81 int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos;
82 assert( p->pReprs && p->pNexts );
83 // count the number of entries to be written
84 nItems = 0;
85 for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ )
86 {
87 nItems += Gia_ObjIsConst( p, iRepr );
88 if ( !Gia_ObjIsHead(p, iRepr) )
89 continue;
90 Gia_ClassForEachObj( p, iRepr, iNode )
91 nItems++;
92 }
93 pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) );
94 // write constant class
95 iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, 4, Abc_Var2Lit(0, 1) );
96 iPrevNode = 0;
97 for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
98 if ( Gia_ObjIsConst(p, iNode) )
99 {
100 iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
101 iPrevNode = iNode;
102 iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
103 }
104 // write non-constant classes
105 iPrevRepr = 0;
106 Gia_ManForEachClass( p, iRepr )
107 {
108 iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
109 iPrevRepr = iPrevNode = iRepr;
110 Gia_ClassForEachObj1( p, iRepr, iNode )
111 {
112 iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
113 iPrevNode = iNode;
114 iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
115 }
116 }
117 Gia_AigerWriteInt( pBuffer, iPos );
118 *pEquivSize = iPos;
119 return pBuffer;
120}
122{
123 int nEquivSize;
124 unsigned char * pBuffer = Gia_WriteEquivClassesInt( p, &nEquivSize );
125 return Vec_StrAllocArray( (char *)pBuffer, nEquivSize );
126}
127
139static inline unsigned Gia_AigerReadDiffValue( unsigned char ** ppPos, int iPrev )
140{
141 int Item = Gia_AigerReadUnsigned( ppPos );
142 if ( Item & 1 )
143 return iPrev + (Item >> 1);
144 return iPrev - (Item >> 1);
145}
146int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize )
147{
148 int * pMapping;
149 unsigned char * pStop;
150 int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize;
151 pStop = *ppPos;
152 pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
153 nAlloc = nSize + pStop - *ppPos;
154 pMapping = ABC_CALLOC( int, nAlloc );
155 while ( *ppPos < pStop )
156 {
157 k = iOffset;
158 pMapping[k++] = nFanins = Gia_AigerReadUnsigned( ppPos );
159 for ( j = 0; j <= nFanins; j++ )
160 pMapping[k++] = iNode = Gia_AigerReadDiffValue( ppPos, iNode );
161 pMapping[iNode] = iOffset;
162 iOffset = k;
163 }
164 assert( iOffset <= nAlloc );
165 return pMapping;
166}
167static inline int Gia_AigerWriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
168{
169 if ( iPrev < iThis )
170 return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
171 return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
172}
173unsigned char * Gia_AigerWriteMappingInt( Gia_Man_t * p, int * pMapSize )
174{
175 unsigned char * pBuffer;
176 int i, k, iPrev, iFan, nItems, iPos = 4;
177 assert( Gia_ManHasMapping(p) );
178 // count the number of entries to be written
179 nItems = 0;
180 Gia_ManForEachLut( p, i )
181 nItems += 2 + Gia_ObjLutSize( p, i );
182 pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
183 // write non-constant classes
184 iPrev = 0;
185 Gia_ManForEachLut( p, i )
186 {
187//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) );
188 iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Gia_ObjLutSize(p, i) );
189 Gia_LutForEachFanin( p, i, iFan, k )
190 {
191//printf( "Fan = %d ", iFan );
192 iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, iFan );
193 iPrev = iFan;
194 }
195 iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, i );
196 iPrev = i;
197//printf( "Node = %d ", i );
198 }
199//printf( "\n" );
200 Gia_AigerWriteInt( pBuffer, iPos );
201 *pMapSize = iPos;
202 return pBuffer;
203}
205{
206 int nMapSize;
207 unsigned char * pBuffer = Gia_AigerWriteMappingInt( p, &nMapSize );
208 return Vec_StrAllocArray( (char *)pBuffer, nMapSize );
209}
210
222int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize )
223{
224 int * pMapping = ABC_ALLOC( int, (size_t)nSize/4 );
225 memcpy( pMapping, *ppPos, nSize );
226 assert( nSize % 4 == 0 );
227 return pMapping;
228}
230{
231 unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*Vec_IntSize(p->vMapping) );
232 memcpy( pBuffer, Vec_IntArray(p->vMapping), (size_t)4*Vec_IntSize(p->vMapping) );
233 assert( Vec_IntSize(p->vMapping) >= Gia_ManObjNum(p) );
234 return Vec_StrAllocArray( (char *)pBuffer, 4*Vec_IntSize(p->vMapping) );
235}
236
248Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs )
249{
250 int * pMapping, nLuts, LutSize, iRoot, nFanins, i, k, nOffset;
251 nLuts = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
252 LutSize = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
253 pMapping = ABC_CALLOC( int, nObjs + (LutSize + 2) * nLuts );
254 nOffset = nObjs;
255 for ( i = 0; i < nLuts; i++ )
256 {
257 iRoot = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
258 nFanins = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
259 pMapping[iRoot] = nOffset;
260 // write one
261 pMapping[ nOffset++ ] = nFanins;
262 for ( k = 0; k < nFanins; k++ )
263 {
264 pMapping[ nOffset++ ] = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
265 }
266 pMapping[ nOffset++ ] = iRoot;
267 }
268 return Vec_IntAllocArray( pMapping, nOffset );
269}
271{
272 unsigned char * pBuffer;
273 int i, k, iFan, nLuts = 0, LutSize = 0, nSize = 2, nSize2 = 0;
274 Gia_ManForEachLut( p, i )
275 {
276 nLuts++;
277 nSize += Gia_ObjLutSize(p, i) + 2;
278 LutSize = Abc_MaxInt( LutSize, Gia_ObjLutSize(p, i) );
279 }
280 pBuffer = ABC_ALLOC( unsigned char, 4 * nSize );
281 Gia_AigerWriteInt( pBuffer + 4 * nSize2++, nLuts );
282 Gia_AigerWriteInt( pBuffer + 4 * nSize2++, LutSize );
283 Gia_ManForEachLut( p, i )
284 {
285 Gia_AigerWriteInt( pBuffer + 4 * nSize2++, i );
286 Gia_AigerWriteInt( pBuffer + 4 * nSize2++, Gia_ObjLutSize(p, i) );
287 Gia_LutForEachFanin( p, i, iFan, k )
288 Gia_AigerWriteInt( pBuffer + 4 * nSize2++, iFan );
289 }
290 assert( nSize2 == nSize );
291 return Vec_StrAllocArray( (char *)pBuffer, 4*nSize );
292}
293
294int Gia_AigerWriteCellMappingInstance( Gia_Man_t * p, unsigned char * pBuffer, int nSize2, int i )
295{
296 int k, iFan;
297 if ( !Gia_ObjIsCellInv(p, i) ) {
298 Gia_AigerWriteInt( pBuffer + nSize2, Gia_ObjCellId(p, i) ); nSize2 += 4;
299 Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4;
300 Gia_CellForEachFanin( p, i, iFan, k )
301 {
302 Gia_AigerWriteInt( pBuffer + nSize2, iFan );
303 nSize2 += 4;
304 }
305 } else {
306 Gia_AigerWriteInt( pBuffer + nSize2, 3 ); nSize2 += 4;
307 Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4;
308 Gia_AigerWriteInt( pBuffer + nSize2, Abc_LitNot(i) ); nSize2 += 4;
309 }
310
311 return nSize2;
312}
313
315{
316 unsigned char * pBuffer;
317 int i, nCells = 0, nInstances = 0, nSize = 8, nSize2 = 0;
318 Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
319 assert( pCells );
320
321 for (int i = 0; i < nCells; i++)
322 {
323 Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate;
324 Mio_Pin_t *pPin;
325 nSize += strlen(Mio_GateReadName(pGate)) + 1;
326 nSize += strlen(Mio_GateReadOutName(pGate)) + 1 + 4;
327 Mio_GateForEachPin( pGate, pPin )
328 nSize += strlen(Mio_PinReadName(pPin)) + 1;
329 }
330
332 {
333 assert ( !Gia_ObjIsCellBuf(p, i) ); // not implemented
334 nInstances++;
335 if ( Gia_ObjIsCellInv(p, i) )
336 nSize += 12;
337 else
338 nSize += Gia_ObjCellSize(p, i) * 4 + 8;
339 }
340
341 pBuffer = ABC_ALLOC( unsigned char, nSize );
342 Gia_AigerWriteInt( pBuffer + nSize2, nCells ); nSize2 += 4;
343 Gia_AigerWriteInt( pBuffer + nSize2, nInstances ); nSize2 += 4;
344
345 for (int i = 0; i < nCells; i++)
346 {
347 int nPins = 0;
348 Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate;
349 Mio_Pin_t *pPin;
350
351 strcpy((char *) pBuffer + nSize2, Mio_GateReadName(pGate));
352 nSize2 += strlen(Mio_GateReadName(pGate)) + 1;
353 strcpy((char *) pBuffer + nSize2, Mio_GateReadOutName(pGate));
354 nSize2 += strlen(Mio_GateReadOutName(pGate)) + 1;
355
356 Mio_GateForEachPin( pGate, pPin )
357 nPins++;
358 Gia_AigerWriteInt( pBuffer + nSize2, nPins ); nSize2 += 4;
359
360 Mio_GateForEachPin( pGate, pPin )
361 {
362 strcpy((char *) pBuffer + nSize2, Mio_PinReadName(pPin));
363 nSize2 += strlen(Mio_PinReadName(pPin)) + 1;
364 }
365 }
366
368 {
369 if ( Gia_ObjIsCellBuf(p, i) )
370 continue;
371
372 if ( Gia_ObjIsCellInv(p, i) && !Abc_LitIsCompl(i) ) {
373 // swap the order so that the inverter is after the driver
374 // of the inverter's input
375 nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, Abc_LitNot(i) );
376 nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i );
377 i += 1;
378 continue;
379 }
380
381 nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i );
382 }
383
384 assert( nSize2 == nSize );
385 ABC_FREE( pCells );
386 return Vec_StrAllocArray( (char *)pBuffer, nSize );
387}
388
400Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize )
401{
402 Vec_Int_t * vPacking = Vec_IntAlloc( nSize/4 );
403 int i;
404 assert( nSize % 4 == 0 );
405 for ( i = 0; i < nSize/4; i++, *ppPos += 4 )
406 Vec_IntPush( vPacking, Gia_AigerReadInt( *ppPos ) );
407 return vPacking;
408}
410{
411 unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*Vec_IntSize(vPacking) );
412 int i, Entry, nSize = 0;
413 Vec_IntForEachEntry( vPacking, Entry, i )
414 Gia_AigerWriteInt( pBuffer + 4 * nSize++, Entry );
415 return Vec_StrAllocArray( (char *)pBuffer, 4*Vec_IntSize(vPacking) );
416}
417
421
422
424
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Cube * p
Definition exorList.c:222
Vec_Str_t * Gia_AigerWriteMappingSimple(Gia_Man_t *p)
unsigned char * Gia_AigerWriteMappingInt(Gia_Man_t *p, int *pMapSize)
Vec_Str_t * Gia_AigerWriteMapping(Gia_Man_t *p)
unsigned char * Gia_WriteEquivClassesInt(Gia_Man_t *p, int *pEquivSize)
Definition giaAigerExt.c:78
Vec_Str_t * Gia_WritePacking(Vec_Int_t *vPacking)
ABC_NAMESPACE_IMPL_START Gia_Rpr_t * Gia_AigerReadEquivClasses(unsigned char **ppPos, int nSize)
DECLARATIONS ///.
Definition giaAigerExt.c:48
int * Gia_AigerReadMappingSimple(unsigned char **ppPos, int nSize)
int Gia_AigerWriteCellMappingInstance(Gia_Man_t *p, unsigned char *pBuffer, int nSize2, int i)
Vec_Int_t * Gia_AigerReadMappingDoc(unsigned char **ppPos, int nObjs)
Vec_Str_t * Gia_AigerWriteCellMappingDoc(Gia_Man_t *p)
int * Gia_AigerReadMapping(unsigned char **ppPos, int nSize)
Vec_Int_t * Gia_AigerReadPacking(unsigned char **ppPos, int nSize)
Vec_Str_t * Gia_AigerWriteMappingDoc(Gia_Man_t *p)
Vec_Str_t * Gia_WriteEquivClasses(Gia_Man_t *p)
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
#define Gia_ManForEachCell(p, i)
Definition gia.h:1181
#define Gia_ClassForEachObj1(p, i, iObj)
Definition gia.h:1109
#define Gia_ManForEachLut(p, i)
Definition gia.h:1157
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition gia.h:1161
#define Gia_ClassForEachObj(p, i, iObj)
Definition gia.h:1107
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
#define Gia_ManForEachClass(p, i)
Definition gia.h:1101
#define Gia_CellForEachFanin(p, i, iFanLit, k)
Definition gia.h:1183
#define GIA_VOID
Definition gia.h:46
Mio_Cell2_t * Mio_CollectRootsNewDefault2(int nInputs, int *pnGates, int fVerbose)
Definition mioUtils.c:877
struct Mio_Cell2_t_ Mio_Cell2_t
Definition mio.h:57
char * Mio_PinReadName(Mio_Pin_t *pPin)
Definition mioApi.c:208
char * Mio_GateReadName(Mio_Gate_t *pGate)
Definition mioApi.c:169
struct Mio_PinStruct_t_ Mio_Pin_t
Definition mio.h:44
char * Mio_GateReadOutName(Mio_Gate_t *pGate)
Definition mioApi.c:170
#define Mio_GateForEachPin(Gate, Pin)
Definition mio.h:92
struct Mio_GateStruct_t_ Mio_Gate_t
Definition mio.h:43
unsigned fProved
Definition gia.h:61
unsigned iRepr
Definition gia.h:60
#define assert(ex)
Definition util_old.h:213
char * memcpy()
int strlen()
char * strcpy()
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54