1 /**CFile****************************************************************
2
3 FileName [utilBridge.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName []
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: utilBridge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include <string.h>
23 #include <stdlib.h>
24 #include <assert.h>
25
26 #include <misc/util/abc_global.h>
27
28 #if defined(LIN) || defined(LIN64)
29 #include <unistd.h>
30 #endif
31
32 #include "aig/gia/gia.h"
33
34 ABC_NAMESPACE_IMPL_START
35
36 ////////////////////////////////////////////////////////////////////////
37 /// DECLARATIONS ///
38 ////////////////////////////////////////////////////////////////////////
39
40 #define BRIDGE_TEXT_MESSAGE 999996
41
42 #define BRIDGE_ABORT 5
43 #define BRIDGE_PROGRESS 3
44 #define BRIDGE_RESULTS 101
45 #define BRIDGE_BAD_ABS 105
46 //#define BRIDGE_NETLIST 106
47 //#define BRIDGE_ABS_NETLIST 107
48
49 #define BRIDGE_VALUE_X 0
50 #define BRIDGE_VALUE_0 2
51 #define BRIDGE_VALUE_1 3
52
53
54 ////////////////////////////////////////////////////////////////////////
55 /// FUNCTION DEFINITIONS ///
56 ////////////////////////////////////////////////////////////////////////
57
58 /**Function*************************************************************
59
60 Synopsis []
61
62 Description []
63
64 SideEffects []
65
66 SeeAlso []
67
68 ***********************************************************************/
Gia_ManToBridgeVec(Gia_Man_t * p)69 Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
70 {
71 Vec_Str_t * vStr;
72 Gia_Obj_t * pObj;
73 int i, uLit0, uLit1, nNodes;
74 assert( Gia_ManPoNum(p) > 0 );
75
76 // start with const1 node (number 1)
77 nNodes = 1;
78 // assign literals(!!!) to the value field
79 Gia_ManConst0(p)->Value = Abc_Var2Lit( nNodes++, 1 );
80 Gia_ManForEachCi( p, pObj, i )
81 pObj->Value = Abc_Var2Lit( nNodes++, 0 );
82 Gia_ManForEachAnd( p, pObj, i )
83 pObj->Value = Abc_Var2Lit( nNodes++, 0 );
84
85 // write header
86 vStr = Vec_StrAlloc( 1000 );
87 Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) );
88 Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) );
89 Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) );
90
91 // write the nodes
92 Gia_ManForEachAnd( p, pObj, i )
93 {
94 uLit0 = Gia_ObjFanin0Copy( pObj );
95 uLit1 = Gia_ObjFanin1Copy( pObj );
96 assert( uLit0 != uLit1 );
97 Gia_AigerWriteUnsigned( vStr, uLit0 << 1 );
98 Gia_AigerWriteUnsigned( vStr, uLit1 );
99 }
100
101 // write latch drivers
102 Gia_ManForEachRi( p, pObj, i )
103 {
104 uLit0 = Gia_ObjFanin0Copy( pObj );
105 Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
106 }
107
108 // write PO drivers
109 Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) );
110 Gia_ManForEachPo( p, pObj, i )
111 {
112 uLit0 = Gia_ObjFanin0Copy( pObj );
113 // complement property output!!!
114 Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) );
115 }
116 return vStr;
117 }
118
119 /**Function*************************************************************
120
121 Synopsis []
122
123 Description []
124
125 SideEffects []
126
127 SeeAlso []
128
129 ***********************************************************************/
Gia_CreateHeader(FILE * pFile,int Type,int Size,unsigned char * pBuffer)130 void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer )
131 {
132 fprintf( pFile, "%.6d", Type );
133 fprintf( pFile, " " );
134 fprintf( pFile, "%.16d", Size );
135 fprintf( pFile, " " );
136 #if !defined(LIN) && !defined(LIN64)
137 {
138 int RetValue;
139 RetValue = fwrite( pBuffer, Size, 1, pFile );
140 assert( RetValue == 1 || Size == 0);
141 fflush( pFile );
142 }
143 #else
144 fflush(pFile);
145 int fd = fileno(pFile);
146
147 ssize_t bytes_written = 0;
148 while (bytes_written < Size){
149 ssize_t n = write(fd, &pBuffer[bytes_written], Size - bytes_written);
150 if (n < 0){
151 fprintf(stderr, "BridgeMode: failed to send package; aborting\n"); fflush(stderr);
152 _exit(255);
153 }
154 bytes_written += n;
155 }
156 #endif
157 }
158
159
160 /**Function*************************************************************
161
162 Synopsis []
163
164 Description []
165
166 SideEffects []
167
168 SeeAlso []
169
170 ***********************************************************************/
Gia_ManToBridgeText(FILE * pFile,int Size,unsigned char * pBuffer)171 int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer )
172 {
173 Gia_CreateHeader( pFile, BRIDGE_TEXT_MESSAGE, Size, pBuffer );
174 return 1;
175 }
176
177
Gia_ManToBridgeAbort(FILE * pFile,int Size,unsigned char * pBuffer)178 int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer )
179 {
180 Gia_CreateHeader( pFile, BRIDGE_ABORT, Size, pBuffer );
181 return 1;
182 }
183
184
Gia_ManToBridgeProgress(FILE * pFile,int Size,unsigned char * pBuffer)185 int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer )
186 {
187 Gia_CreateHeader( pFile, BRIDGE_PROGRESS, Size, pBuffer );
188 return 1;
189 }
190
191
Gia_ManToBridgeAbsNetlist(FILE * pFile,void * p,int pkg_type)192 int Gia_ManToBridgeAbsNetlist( FILE * pFile, void * p, int pkg_type )
193 {
194 Vec_Str_t * vBuffer;
195 vBuffer = Gia_ManToBridgeVec( (Gia_Man_t *)p );
196 Gia_CreateHeader( pFile, pkg_type, Vec_StrSize(vBuffer), (unsigned char *)Vec_StrArray(vBuffer) );
197 Vec_StrFree( vBuffer );
198 return 1;
199 }
200
201
Gia_ManToBridgeBadAbs(FILE * pFile)202 int Gia_ManToBridgeBadAbs( FILE * pFile )
203 {
204 Gia_CreateHeader( pFile, BRIDGE_BAD_ABS, 0, NULL );
205 return 1;
206 }
207
208
aigerNumSize(unsigned x)209 static int aigerNumSize( unsigned x )
210 {
211 int sz = 1;
212 while (x & ~0x7f)
213 {
214 sz++;
215 x >>= 7;
216 }
217 return sz;
218 }
219
220
221 /**Function*************************************************************
222
223 Synopsis []
224
225 Description []
226
227 SideEffects []
228
229 SeeAlso []
230
231 ***********************************************************************/
Gia_ManFromBridgeHolds(FILE * pFile,int iPoProved)232 void Gia_ManFromBridgeHolds( FILE * pFile, int iPoProved )
233 {
234 fprintf( pFile, "%.6d", 101 /*message type = Result*/);
235 fprintf( pFile, " " );
236 fprintf( pFile, "%.16d", 3 + aigerNumSize(iPoProved) /*size in bytes*/);
237 fprintf( pFile, " " );
238
239 fputc( (char)BRIDGE_VALUE_1, pFile ); // true
240 fputc( (char)1, pFile ); // size of vector (Armin's encoding)
241 Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
242 fputc( (char)0, pFile ); // no invariant
243 fflush(pFile);
244 }
Gia_ManFromBridgeUnknown(FILE * pFile,int iPoUnknown)245 void Gia_ManFromBridgeUnknown( FILE * pFile, int iPoUnknown )
246 {
247 fprintf( pFile, "%.6d", 101 /*message type = Result*/);
248 fprintf( pFile, " " );
249 fprintf( pFile, "%.16d", 2 + aigerNumSize(iPoUnknown) /*size in bytes*/);
250 fprintf( pFile, " " );
251
252 fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
253 fputc( (char)1, pFile ); // size of vector (Armin's encoding)
254 Gia_AigerWriteUnsignedFile( pFile, iPoUnknown ); // number of the property (Armin's encoding)
255 fflush(pFile);
256 }
Gia_ManFromBridgeCex(FILE * pFile,Abc_Cex_t * pCex)257 void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
258 {
259 int i, f, iBit;//, RetValue;
260 Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
261 Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
262 Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
263 Gia_AigerWriteUnsigned( vStr, pCex->iPo ); // number of the property (Armin's encoding)
264 Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
265 Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
266
267 Gia_AigerWriteUnsigned( vStr, 1 ); // concrete
268 Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
269 iBit = pCex->nRegs;
270 for ( f = 0; f <= pCex->iFrame; f++ )
271 {
272 Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs
273 for ( i = 0; i < pCex->nPis; i++, iBit++ )
274 Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
275 }
276 assert( iBit == pCex->nBits );
277 Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
278 Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops
279 for ( i = 0; i < pCex->nRegs; i++ )
280 Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
281 // RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
282 Gia_CreateHeader(pFile, 101/*type=Result*/, Vec_StrSize(vStr), (unsigned char*)Vec_StrArray(vStr));
283
284 Vec_StrFree( vStr );
285 fflush(pFile);
286 }
Gia_ManToBridgeResult(FILE * pFile,int Result,Abc_Cex_t * pCex,int iPoProved)287 int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved )
288 {
289 if ( Result == 0 ) // sat
290 Gia_ManFromBridgeCex( pFile, pCex );
291 else if ( Result == 1 ) // unsat
292 Gia_ManFromBridgeHolds( pFile, iPoProved );
293 else if ( Result == -1 ) // undef
294 Gia_ManFromBridgeUnknown( pFile, iPoProved );
295 else assert( 0 );
296 return 1;
297 }
298
299
300 /**Function*************************************************************
301
302 Synopsis []
303
304 Description []
305
306 SideEffects []
307
308 SeeAlso []
309
310 ***********************************************************************/
Gia_ManFromBridgeReadBody(int Size,unsigned char * pBuffer,Vec_Int_t ** pvInits)311 Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_Int_t ** pvInits )
312 {
313 int fHash = 0;
314 Vec_Int_t * vLits, * vInits;
315 Gia_Man_t * p = NULL;
316 unsigned char * pBufferPivot, * pBufferEnd = pBuffer + Size;
317 int i, nInputs, nFlops, nGates, nProps;
318 int verFairness, nFairness, nConstraints;
319 unsigned iFan0, iFan1;
320
321 nInputs = Gia_AigerReadUnsigned( &pBuffer );
322 nFlops = Gia_AigerReadUnsigned( &pBuffer );
323 nGates = Gia_AigerReadUnsigned( &pBuffer );
324
325 vLits = Vec_IntAlloc( 1000 );
326 Vec_IntPush( vLits, -999 );
327 Vec_IntPush( vLits, 1 );
328
329 // start the AIG package
330 p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); // PI+FO+FI+AND+PO+1
331 p->pName = Abc_UtilStrsav( "temp" );
332
333 // create PIs
334 for ( i = 0; i < nInputs; i++ )
335 Vec_IntPush( vLits, Gia_ManAppendCi( p ) );
336
337 // create flop outputs
338 for ( i = 0; i < nFlops; i++ )
339 Vec_IntPush( vLits, Gia_ManAppendCi( p ) );
340
341 // create nodes
342 if ( fHash )
343 Gia_ManHashAlloc( p );
344 for ( i = 0; i < nGates; i++ )
345 {
346 iFan0 = Gia_AigerReadUnsigned( &pBuffer );
347 iFan1 = Gia_AigerReadUnsigned( &pBuffer );
348 assert( !(iFan0 & 1) );
349 iFan0 >>= 1;
350 iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
351 iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan1 & 1 );
352 if ( fHash )
353 Vec_IntPush( vLits, Gia_ManHashAnd(p, iFan0, iFan1) );
354 else
355 Vec_IntPush( vLits, Gia_ManAppendAnd(p, iFan0, iFan1) );
356
357 }
358 if ( fHash )
359 Gia_ManHashStop( p );
360
361 // remember where flops begin
362 pBufferPivot = pBuffer;
363 // scroll through flops
364 for ( i = 0; i < nFlops; i++ )
365 Gia_AigerReadUnsigned( &pBuffer );
366
367 // create POs
368 nProps = Gia_AigerReadUnsigned( &pBuffer );
369 // assert( nProps == 1 );
370 for ( i = 0; i < nProps; i++ )
371 {
372 iFan0 = Gia_AigerReadUnsigned( &pBuffer );
373 iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
374 // complement property output!!!
375 Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
376 }
377
378 verFairness = Gia_AigerReadUnsigned( &pBuffer );
379 assert( verFairness == 1 );
380
381 nFairness = Gia_AigerReadUnsigned( &pBuffer );
382 assert( nFairness == 0 );
383
384 nConstraints = Gia_AigerReadUnsigned( &pBuffer );
385 assert( nConstraints == 0);
386
387 // make sure the end of buffer is reached
388 assert( pBufferEnd == pBuffer );
389
390 // resetting to flops
391 pBuffer = pBufferPivot;
392 vInits = Vec_IntAlloc( nFlops );
393 for ( i = 0; i < nFlops; i++ )
394 {
395 iFan0 = Gia_AigerReadUnsigned( &pBuffer );
396 assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
397 Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
398 iFan0 >>= 2;
399 iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
400 Gia_ManAppendCo( p, iFan0 );
401 }
402 Gia_ManSetRegNum( p, nFlops );
403 Vec_IntFree( vLits );
404
405 // remove wholes in the node list
406 if ( fHash )
407 {
408 Gia_Man_t * pTemp;
409 p = Gia_ManCleanup( pTemp = p );
410 Gia_ManStop( pTemp );
411 }
412
413 // return
414 if ( pvInits )
415 *pvInits = vInits;
416 else
417 Vec_IntFree( vInits );
418 return p;
419 }
420
421
422 /**Function*************************************************************
423
424 Synopsis []
425
426 Description []
427
428 SideEffects []
429
430 SeeAlso []
431
432 ***********************************************************************/
Gia_ManFromBridgeReadPackage(FILE * pFile,int * pType,int * pSize,unsigned char ** ppBuffer)433 int Gia_ManFromBridgeReadPackage( FILE * pFile, int * pType, int * pSize, unsigned char ** ppBuffer )
434 {
435 char Temp[24];
436 int RetValue;
437 RetValue = fread( Temp, 24, 1, pFile );
438 if ( RetValue != 1 )
439 {
440 printf( "Gia_ManFromBridgeReadPackage(); Error 1: Something is wrong!\n" );
441 return 0;
442 }
443 Temp[6] = 0;
444 Temp[23]= 0;
445
446 *pType = atoi( Temp );
447 *pSize = atoi( Temp + 7 );
448
449 *ppBuffer = ABC_ALLOC( unsigned char, *pSize );
450 RetValue = fread( *ppBuffer, *pSize, 1, pFile );
451 if ( RetValue != 1 && *pSize != 0 )
452 {
453 ABC_FREE( *ppBuffer );
454 printf( "Gia_ManFromBridgeReadPackage(); Error 2: Something is wrong!\n" );
455 return 0;
456 }
457 return 1;
458 }
459
460 /**Function*************************************************************
461
462 Synopsis []
463
464 Description []
465
466 SideEffects []
467
468 SeeAlso []
469
470 ***********************************************************************/
Gia_ManFromBridge(FILE * pFile,Vec_Int_t ** pvInit)471 Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit )
472 {
473 unsigned char * pBuffer;
474 int Type, Size, RetValue;
475 Gia_Man_t * p = NULL;
476
477 RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
478 ABC_FREE( pBuffer );
479 if ( !RetValue )
480 return NULL;
481
482 RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
483 if ( !RetValue )
484 return NULL;
485
486 p = Gia_ManFromBridgeReadBody( Size, pBuffer, pvInit );
487 ABC_FREE( pBuffer );
488 if ( p == NULL )
489 return NULL;
490
491 RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
492 ABC_FREE( pBuffer );
493 if ( !RetValue )
494 return NULL;
495
496 return p;
497 }
498
499 /*
500 {
501 extern void Gia_ManFromBridgeTest( char * pFileName );
502 Gia_ManFromBridgeTest( "C:\\_projects\\abc\\_TEST\\bug\\65\\par.dump" );
503 }
504 */
505
506 /**Function*************************************************************
507
508 Synopsis []
509
510 Description []
511
512 SideEffects []
513
514 SeeAlso []
515
516 ***********************************************************************/
Gia_ManToBridgeAbsNetlistTest(char * pFileName,Gia_Man_t * p,int msg_type)517 void Gia_ManToBridgeAbsNetlistTest( char * pFileName, Gia_Man_t * p, int msg_type )
518 {
519 FILE * pFile = fopen( pFileName, "wb" );
520 if ( pFile == NULL )
521 {
522 printf( "Cannot open output file \"%s\".\n", pFileName );
523 return;
524 }
525 Gia_ManToBridgeAbsNetlist( pFile, p, msg_type );
526 fclose ( pFile );
527 }
528
529 /**Function*************************************************************
530
531 Synopsis []
532
533 Description []
534
535 SideEffects []
536
537 SeeAlso []
538
539 ***********************************************************************/
Gia_ManFromBridgeTest(char * pFileName)540 void Gia_ManFromBridgeTest( char * pFileName )
541 {
542 Gia_Man_t * p;
543 FILE * pFile = fopen( pFileName, "rb" );
544 if ( pFile == NULL )
545 {
546 printf( "Cannot open input file \"%s\".\n", pFileName );
547 return;
548 }
549
550 p = Gia_ManFromBridge( pFile, NULL );
551 fclose ( pFile );
552
553 Gia_ManPrintStats( p, NULL );
554 Gia_AigerWrite( p, "temp.aig", 0, 0, 0 );
555
556 Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
557 Gia_ManStop( p );
558 }
559
560
561
562 ////////////////////////////////////////////////////////////////////////
563 /// END OF FILE ///
564 ////////////////////////////////////////////////////////////////////////
565
566
567 ABC_NAMESPACE_IMPL_END
568