utilBridge.c 14.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
/**CFile****************************************************************

  FileName    [utilBridge.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName []

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: utilBridge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
25
#if defined(LIN) || defined(LIN64)
26 27
#include <unistd.h>
#endif
28

29
#include "aig/gia/gia.h"
30 31 32 33 34 35 36

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

37 38 39 40 41 42 43 44 45 46 47 48
#define BRIDGE_TEXT_MESSAGE 999996

#define BRIDGE_ABORT        5
#define BRIDGE_PROGRESS     3
#define BRIDGE_RESULTS      101
#define BRIDGE_BAD_ABS      105
//#define BRIDGE_NETLIST      106
//#define BRIDGE_ABS_NETLIST  107

#define BRIDGE_VALUE_X 0
#define BRIDGE_VALUE_0 2
#define BRIDGE_VALUE_1 3
49 50


51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
66
Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
67
{
68
    Vec_Str_t * vStr;
69
    Gia_Obj_t * pObj;
70 71 72 73 74 75 76
    int i, uLit0, uLit1, nNodes;
    assert( Gia_ManPoNum(p) > 0 );

    // start with const1 node (number 1)
    nNodes = 1;
    // assign literals(!!!) to the value field
    Gia_ManConst0(p)->Value = Abc_Var2Lit( nNodes++, 1 );
77
    Gia_ManForEachCi( p, pObj, i )
78
        pObj->Value = Abc_Var2Lit( nNodes++, 0 );
79
    Gia_ManForEachAnd( p, pObj, i )
80 81 82 83
        pObj->Value = Abc_Var2Lit( nNodes++, 0 );

    // write header
    vStr = Vec_StrAlloc( 1000 );
84 85 86
    Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) );
    Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) );
    Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) );
87 88 89 90 91 92 93

    // write the nodes 
    Gia_ManForEachAnd( p, pObj, i )
    {
        uLit0 = Gia_ObjFanin0Copy( pObj );
        uLit1 = Gia_ObjFanin1Copy( pObj );
        assert( uLit0 != uLit1 );
94 95
        Gia_AigerWriteUnsigned( vStr, uLit0 << 1 );
        Gia_AigerWriteUnsigned( vStr, uLit1 );
96
    }
97 98 99 100

    // write latch drivers
    Gia_ManForEachRi( p, pObj, i )
    {
101
        uLit0 = Gia_ObjFanin0Copy( pObj );
102
        Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
103 104 105
    }

    // write PO drivers
106
    Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) );
107 108
    Gia_ManForEachPo( p, pObj, i )
    {
109 110
        uLit0 = Gia_ObjFanin0Copy( pObj );
        // complement property output!!!
111
        Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) );
112
    }
113
    return vStr;
114 115 116 117 118 119 120 121 122 123 124 125 126
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
127 128 129 130 131 132
void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer )
{
    fprintf( pFile, "%.6d", Type );
    fprintf( pFile, " " );
    fprintf( pFile, "%.16d", Size );
    fprintf( pFile, " " );
Alan Mishchenko committed
133 134 135
#if !defined(LIN) && !defined(LIN64)
    {
    int RetValue;
136
    RetValue = fwrite( pBuffer, Size, 1, pFile );
137
    assert( RetValue == 1 || Size == 0);
138
    fflush( pFile );
Alan Mishchenko committed
139 140
    }
#else
141 142 143 144 145 146 147 148 149 150 151 152
    fflush(pFile);
    int fd = fileno(pFile);

    ssize_t bytes_written = 0;
    while (bytes_written < Size){
        ssize_t n = write(fd, &pBuffer[bytes_written], Size - bytes_written);
        if (n < 0){
            fprintf(stderr, "BridgeMode: failed to send package; aborting\n"); fflush(stderr);
            _exit(255);
        }
        bytes_written += n;
    }
Alan Mishchenko committed
153
#endif
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer )
{
    Gia_CreateHeader( pFile, BRIDGE_TEXT_MESSAGE, Size, pBuffer );
    return 1;
}
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188


int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer )
{
    Gia_CreateHeader( pFile, BRIDGE_ABORT, Size, pBuffer );
    return 1;
}


int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer )
{
    Gia_CreateHeader( pFile, BRIDGE_PROGRESS, Size, pBuffer );
    return 1;
}


189
int Gia_ManToBridgeAbsNetlist( FILE * pFile, void * p, int pkg_type )
190 191
{
    Vec_Str_t * vBuffer;
192
    vBuffer = Gia_ManToBridgeVec( (Gia_Man_t *)p );
193
    Gia_CreateHeader( pFile, pkg_type, Vec_StrSize(vBuffer), (unsigned char *)Vec_StrArray(vBuffer) );
194
    Vec_StrFree( vBuffer );
195 196
    return 1;
}
197 198


199 200 201 202 203 204
int Gia_ManToBridgeBadAbs( FILE * pFile )
{
    Gia_CreateHeader( pFile, BRIDGE_BAD_ABS, 0, NULL );
    return 1;
}

Niklas Een committed
205 206 207 208 209 210 211 212 213 214 215 216 217

static int aigerNumSize( unsigned x )
{
    int sz = 1;
    while (x & ~0x7f)
    {
        sz++;
        x >>= 7;
    }
    return sz;
}


218 219 220 221 222 223 224 225 226 227 228
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
229
void Gia_ManFromBridgeHolds( FILE * pFile, int iPoProved )
230
{
231 232
    fprintf( pFile, "%.6d", 101 /*message type = Result*/);
    fprintf( pFile, " " );
Niklas Een committed
233
    fprintf( pFile, "%.16d", 3 + aigerNumSize(iPoProved) /*size in bytes*/);
234 235
    fprintf( pFile, " " );

236
    fputc( (char)BRIDGE_VALUE_1, pFile ); // true
237
    fputc( (char)1, pFile ); // size of vector (Armin's encoding)
238
    Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
239
    fputc( (char)0, pFile ); // no invariant
240
    fflush(pFile);
241
}
242
void Gia_ManFromBridgeUnknown( FILE * pFile, int iPoUnknown )
243
{
244 245
    fprintf( pFile, "%.6d", 101 /*message type = Result*/);
    fprintf( pFile, " " );
Niklas Een committed
246
    fprintf( pFile, "%.16d", 2 + aigerNumSize(iPoUnknown) /*size in bytes*/);
247 248
    fprintf( pFile, " " );

249
    fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
250
    fputc( (char)1, pFile ); // size of vector (Armin's encoding)
251
    Gia_AigerWriteUnsignedFile( pFile, iPoUnknown ); // number of the property (Armin's encoding)
252
    fflush(pFile);
253 254 255
}
void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
{
256
    int i, f, iBit;//, RetValue;
257
    Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
258
    Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
259
    Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
260
    Gia_AigerWriteUnsigned( vStr, pCex->iPo ); // number of the property (Armin's encoding)
261
    Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
262
    Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
263

264 265
    Gia_AigerWriteUnsigned( vStr, 1 ); // concrete
    Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
266 267 268
    iBit = pCex->nRegs;
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
269
        Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs
270 271
        for ( i = 0; i < pCex->nPis; i++, iBit++ )
            Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
272 273 274
    }
    assert( iBit == pCex->nBits );
    Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
275
    Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops
276
    for ( i = 0; i < pCex->nRegs; i++ )
277
        Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
278 279 280
//    RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
    Gia_CreateHeader(pFile, 101/*type=Result*/, Vec_StrSize(vStr), (unsigned char*)Vec_StrArray(vStr));

281
    Vec_StrFree( vStr );
282
    fflush(pFile);
283
}
284
int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved )
285 286 287 288
{
    if ( Result == 0 ) // sat
        Gia_ManFromBridgeCex( pFile, pCex );
    else if ( Result == 1 ) // unsat
289
        Gia_ManFromBridgeHolds( pFile, iPoProved );
290
    else if ( Result == -1 ) // undef
291
        Gia_ManFromBridgeUnknown( pFile, iPoProved );
292 293
    else assert( 0 );
    return 1;
294 295 296 297 298 299 300 301
}


/**Function*************************************************************

  Synopsis    []

  Description []
302

303 304 305 306 307 308 309 310 311 312 313 314 315 316
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_Int_t ** pvInits )
{
    int fHash = 0;
    Vec_Int_t * vLits, * vInits;
    Gia_Man_t * p = NULL;
    unsigned char * pBufferPivot, * pBufferEnd = pBuffer + Size;
    int i, nInputs, nFlops, nGates, nProps;
    unsigned iFan0, iFan1;

317 318 319
    nInputs = Gia_AigerReadUnsigned( &pBuffer );
    nFlops  = Gia_AigerReadUnsigned( &pBuffer );
    nGates  = Gia_AigerReadUnsigned( &pBuffer );
320 321

    vLits = Vec_IntAlloc( 1000 );
322
    Vec_IntPush( vLits, -999 );
323 324 325
    Vec_IntPush( vLits,  1 );

    // start the AIG package
326
    p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); // PI+FO+FI+AND+PO+1
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
    p->pName = Abc_UtilStrsav( "temp" );

    // create PIs
    for ( i = 0; i < nInputs; i++ )
        Vec_IntPush( vLits, Gia_ManAppendCi( p ) );

    // create flop outputs
    for ( i = 0; i < nFlops; i++ )
        Vec_IntPush( vLits, Gia_ManAppendCi( p ) );

    // create nodes
    if ( fHash )
        Gia_ManHashAlloc( p );
    for ( i = 0; i < nGates; i++ )
    {
342 343
        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
        iFan1 = Gia_AigerReadUnsigned( &pBuffer );
344
        assert( !(iFan0 & 1) );
345 346
        iFan0 >>= 1;
        iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
347
        iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan1 & 1 );
348 349
        if ( fHash )
            Vec_IntPush( vLits, Gia_ManHashAnd(p, iFan0, iFan1) );
350
        else
351 352 353 354 355 356 357 358
            Vec_IntPush( vLits, Gia_ManAppendAnd(p, iFan0, iFan1) );

    }
    if ( fHash )
        Gia_ManHashStop( p );

    // remember where flops begin
    pBufferPivot = pBuffer;
359
    // scroll through flops
360
    for ( i = 0; i < nFlops; i++ )
361
        Gia_AigerReadUnsigned( &pBuffer );
362 363

    // create POs
364
    nProps = Gia_AigerReadUnsigned( &pBuffer );
365
//    assert( nProps == 1 );
366 367
    for ( i = 0; i < nProps; i++ )
    {
368
        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
369
        iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
370 371
        // complement property output!!!
        Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
372 373 374 375 376 377 378 379 380
    }
    // make sure the end of buffer is reached
    assert( pBufferEnd == pBuffer );

    // resetting to flops
    pBuffer = pBufferPivot;
    vInits = Vec_IntAlloc( nFlops );
    for ( i = 0; i < nFlops; i++ )
    {
381
        iFan0 = Gia_AigerReadUnsigned( &pBuffer );
382
        assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
        Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
        iFan0 >>= 2;
        iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
        Gia_ManAppendCo( p, iFan0 );
    }
    Gia_ManSetRegNum( p, nFlops );
    Vec_IntFree( vLits );

    // remove wholes in the node list
    if ( fHash )
    {
        Gia_Man_t * pTemp;
        p = Gia_ManCleanup( pTemp = p );
        Gia_ManStop( pTemp );
    }

    // return
    if ( pvInits )
        *pvInits = vInits;
    else
        Vec_IntFree( vInits );
    return p;
}

407

408 409 410 411 412
/**Function*************************************************************

  Synopsis    []

  Description []
413

414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManFromBridgeReadPackage( FILE * pFile, int * pType, int * pSize, unsigned char ** ppBuffer )
{
    char Temp[24];
    int RetValue;
    RetValue = fread( Temp, 24, 1, pFile );
    if ( RetValue != 1 )
    {
        printf( "Gia_ManFromBridgeReadPackage();  Error 1: Something is wrong!\n" );
        return 0;
    }
    Temp[6] = 0;
    Temp[23]= 0;

    *pType = atoi( Temp );
    *pSize = atoi( Temp + 7 );

435
    *ppBuffer = ABC_ALLOC( unsigned char, *pSize );
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450
    RetValue = fread( *ppBuffer, *pSize, 1, pFile );
    if ( RetValue != 1 && *pSize != 0 )
    {
        ABC_FREE( *ppBuffer );
        printf( "Gia_ManFromBridgeReadPackage();  Error 2: Something is wrong!\n" );
        return 0;
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    []

  Description []
451

452 453 454 455 456 457 458 459 460 461 462 463 464 465
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit )
{
    unsigned char * pBuffer;
    int Type, Size, RetValue;
    Gia_Man_t * p = NULL;

    RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
    ABC_FREE( pBuffer );
    if ( !RetValue )
466
        return NULL;
467 468 469 470 471

    RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
    if ( !RetValue )
        return NULL;

472
    p = Gia_ManFromBridgeReadBody( Size, pBuffer, pvInit );
473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
    ABC_FREE( pBuffer );
    if ( p == NULL )
        return NULL;

    RetValue = Gia_ManFromBridgeReadPackage( pFile, &Type, &Size, &pBuffer );
    ABC_FREE( pBuffer );
    if ( !RetValue )
        return NULL;

    return p;
}

/*
    {
        extern void Gia_ManFromBridgeTest( char * pFileName );
        Gia_ManFromBridgeTest( "C:\\_projects\\abc\\_TEST\\bug\\65\\par.dump" );
    }
*/

/**Function*************************************************************

  Synopsis    []

  Description []
497

498 499 500 501 502
  SideEffects []

  SeeAlso     []

***********************************************************************/
503
void Gia_ManToBridgeAbsNetlistTest( char * pFileName, Gia_Man_t * p, int msg_type )
504 505 506 507 508 509 510
{
    FILE * pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open output file \"%s\".\n", pFileName );
        return;
    }
511
    Gia_ManToBridgeAbsNetlist( pFile, p, msg_type );
512 513 514 515 516 517 518 519
    fclose ( pFile );
}

/**Function*************************************************************

  Synopsis    []

  Description []
520

521 522 523 524 525
  SideEffects []

  SeeAlso     []

***********************************************************************/
526 527 528 529 530 531 532 533 534 535 536 537 538
void Gia_ManFromBridgeTest( char * pFileName )
{
    Gia_Man_t * p;
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open input file \"%s\".\n", pFileName );
        return;
    }

    p = Gia_ManFromBridge( pFile, NULL );
    fclose ( pFile );

539
    Gia_ManPrintStats( p, NULL );
540
    Gia_AigerWrite( p, "temp.aig", 0, 0 );
541

542
    Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
543 544 545
    Gia_ManStop( p );
}

546 547


548 549 550 551 552 553
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END