ioReadBlifMv.c 77.9 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**CFile****************************************************************

  FileName    [ioReadBlifMv.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Command processing package.]

  Synopsis    [Procedures to read BLIF-MV file.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 8, 2007.]

  Revision    [$Id: ioReadBlifMv.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $]

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

21 22
#include "misc/zlib/zlib.h"
#include "misc/bzlib/bzlib.h"
23 24
#include "base/abc/abc.h"
#include "misc/vec/vecPtr.h"
Alan Mishchenko committed
25
#include "ioAbc.h"
Alan Mishchenko committed
26

27 28
ABC_NAMESPACE_IMPL_START

Alan Mishchenko committed
29 30 31 32 33
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

#define IO_BLIFMV_MAXVALUES 256
Alan Mishchenko committed
34
//#define IO_VERBOSE_OUTPUT
Alan Mishchenko committed
35 36 37 38 39

typedef struct Io_MvVar_t_ Io_MvVar_t; // parsing var
typedef struct Io_MvMod_t_ Io_MvMod_t; // parsing model
typedef struct Io_MvMan_t_ Io_MvMan_t; // parsing manager

40 41
Vec_Ptr_t *vGlobalLtlArray;

Alan Mishchenko committed
42 43 44 45 46 47 48 49 50 51 52 53 54
struct Io_MvVar_t_
{
    int                  nValues;      // the number of values 
    char **              pNames;       // the value names
};

struct Io_MvMod_t_
{
    // file lines
    char *               pName;        // .model line
    Vec_Ptr_t *          vInputs;      // .inputs lines
    Vec_Ptr_t *          vOutputs;     // .outputs lines
    Vec_Ptr_t *          vLatches;     // .latch lines
55
    Vec_Ptr_t *          vFlops;       // .flop lines
Alan Mishchenko committed
56 57 58
    Vec_Ptr_t *          vResets;      // .reset lines
    Vec_Ptr_t *          vNames;       // .names lines
    Vec_Ptr_t *          vSubckts;     // .subckt lines
Alan Mishchenko committed
59
    Vec_Ptr_t *          vShorts;      // .short lines
Alan Mishchenko committed
60
    Vec_Ptr_t *          vOnehots;     // .onehot lines
Alan Mishchenko committed
61
    Vec_Ptr_t *          vMvs;         // .mv lines
62 63
    Vec_Ptr_t *          vConstrs;     // .constraint lines
    Vec_Ptr_t *             vLtlProperties;
Alan Mishchenko committed
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
    int                  fBlackBox;    // indicates blackbox model
    // the resulting network
    Abc_Ntk_t *          pNtk;   
    Abc_Obj_t *          pResetLatch; 
    // the parent manager
    Io_MvMan_t *         pMan;         
};

struct Io_MvMan_t_
{
    // general info about file
    int                  fBlifMv;      // the file is BLIF-MV
    int                  fUseReset;    // the reset circuitry is added
    char *               pFileName;    // the name of the file
    char *               pBuffer;      // the contents of the file
    Vec_Ptr_t *          vLines;       // the line beginnings
    // the results of reading
81
    Abc_Des_t *          pDesign;      // the design under construction
Alan Mishchenko committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
    int                  nNDnodes;     // the counter of ND nodes
    // intermediate storage for models
    Vec_Ptr_t *          vModels;      // vector of models
    Io_MvMod_t *         pLatest;      // the current model
    // current processing info
    Vec_Ptr_t *          vTokens;      // the current tokens
    Vec_Ptr_t *          vTokens2;     // the current tokens
    Vec_Str_t *          vFunc;        // the local function
    // error reporting
    char                 sError[512];  // the error string generated during parsing
    // statistics 
    int                  nTablesRead;  // the number of processed tables
    int                  nTablesLeft;  // the number of dangling tables
};

// static functions
static Io_MvMan_t *      Io_MvAlloc();
static void              Io_MvFree( Io_MvMan_t * p );
static Io_MvMod_t *      Io_MvModAlloc();
static void              Io_MvModFree( Io_MvMod_t * p );
static char *            Io_MvLoadFile( char * pFileName );
static void              Io_MvReadPreparse( Io_MvMan_t * p );
Alan Mishchenko committed
104
static int               Io_MvReadInterfaces( Io_MvMan_t * p );
105
static Abc_Des_t *       Io_MvParse( Io_MvMan_t * p );
Alan Mishchenko committed
106 107 108
static int               Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
static int               Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
static int               Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
109
static int               Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
110
static int               Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine );
111
static int               Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
112
static int               Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
113
static Vec_Int_t *       Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
114 115 116
static int               Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
static int               Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
static int               Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
117
static int               Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine );
118
static int                 Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine );
Alan Mishchenko committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
static int               Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens );
static Io_MvVar_t *      Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar );

static int               Io_MvCharIsSpace( char s )  { return s == ' ' || s == '\t' || s == '\r' || s == '\n';  }
static int               Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!';  }

extern void              Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Reads the network from the BLIF or BLIF-MV file.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
{
    FILE * pFile;
    Io_MvMan_t * p;
146
    Abc_Ntk_t * pNtk, * pExdc;
147
    Abc_Des_t * pDesign = NULL; 
Alan Mishchenko committed
148 149
    char * pDesignName;
    int RetValue, i;
150
    char * pLtlProp;
Alan Mishchenko committed
151 152 153 154 155 156 157 158 159 160 161 162 163

    // check that the file is available
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Io_ReadBlifMv(): The file is unavailable (absent or open).\n" );
        return 0;
    }
    fclose( pFile );

    // start the file reader
    p = Io_MvAlloc();
    p->fBlifMv   = fBlifMv;
Alan Mishchenko committed
164
    p->fUseReset = 1;
Alan Mishchenko committed
165 166 167 168 169 170 171 172 173
    p->pFileName = pFileName;
    p->pBuffer   = Io_MvLoadFile( pFileName );
    if ( p->pBuffer == NULL )
    {
        Io_MvFree( p );
        return NULL;
    }
    // set the design name
    pDesignName  = Extra_FileNameGeneric( pFileName );
174
    p->pDesign   = Abc_DesCreate( pDesignName );
Alan Mishchenko committed
175
    ABC_FREE( pDesignName );
Alan Mishchenko committed
176
    // free the HOP manager
177
    Hop_ManStop( (Hop_Man_t *)p->pDesign->pManFunc );
Alan Mishchenko committed
178 179 180
    p->pDesign->pManFunc = NULL;
    // prepare the file for parsing
    Io_MvReadPreparse( p );
Alan Mishchenko committed
181 182 183
    // parse interfaces of each network and construct the network
    if ( Io_MvReadInterfaces( p ) )
        pDesign = Io_MvParse( p );
Alan Mishchenko committed
184 185 186 187 188 189 190 191 192 193
    if ( p->sError[0] )
        fprintf( stdout, "%s\n", p->sError );
    Io_MvFree( p );
    if ( pDesign == NULL )
        return NULL;
// pDesign should be linked to all models of the design

    // make sure that everything is okay with the network structure
    if ( fCheck )
    {
194
        Vec_PtrForEachEntry( Abc_Ntk_t *, pDesign->vModules, pNtk, i )
Alan Mishchenko committed
195 196 197
        {
            if ( !Abc_NtkCheckRead( pNtk ) )
            {
Alan Mishchenko committed
198
                printf( "Io_ReadBlifMv: The network check has failed for model %s.\n", pNtk->pName );
199
                Abc_DesFree( pDesign, NULL );
Alan Mishchenko committed
200 201 202 203 204
                return NULL;
            }
        }
    }

205
//Abc_DesPrint( pDesign );
Alan Mishchenko committed
206

207 208 209 210 211
    // check if there is an EXDC network
    if ( Vec_PtrSize(pDesign->vModules) > 1 )
    {
        pNtk = (Abc_Ntk_t *)Vec_PtrEntry(pDesign->vModules, 0);
        Vec_PtrForEachEntryStart( Abc_Ntk_t *, pDesign->vModules, pExdc, i, 1 )
212
            if ( !strcmp(pExdc->pName, "EXDC") )
213 214 215 216 217 218 219 220 221 222 223
            {
                assert( pNtk->pExdc == NULL );
                pNtk->pExdc = pExdc;
                Vec_PtrRemove(pDesign->vModules, pExdc);
                pExdc->pDesign = NULL;
                i--;
            }
            else
                pNtk = pExdc;
    }

Alan Mishchenko committed
224
    // detect top-level model
225
    RetValue = Abc_DesFindTopLevelModels( pDesign );
226
    pNtk = (Abc_Ntk_t *)Vec_PtrEntry( pDesign->vTops, 0 );
Alan Mishchenko committed
227 228 229 230 231 232 233 234 235 236 237 238 239
    if ( RetValue > 1 )
        printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n",
            Vec_PtrSize(pDesign->vTops), pNtk->pName );

    // extract the master network
    pNtk->pDesign = pDesign;
    pDesign->pManFunc = NULL;

    // verify the design for cyclic dependence
    assert( Vec_PtrSize(pDesign->vModules) > 0 );
    if ( Vec_PtrSize(pDesign->vModules) == 1 )
    {
//        printf( "Warning: The design is not hierarchical.\n" );
240
        Abc_DesFree( pDesign, pNtk );
Alan Mishchenko committed
241 242 243 244 245 246 247 248 249
        pNtk->pDesign = NULL;
        pNtk->pSpec = Extra_UtilStrsav( pFileName );
    }
    else
        Abc_NtkIsAcyclicHierarchy( pNtk );

//Io_WriteBlifMv( pNtk, "_temp_.mv" );
    if ( pNtk->pSpec == NULL )
        pNtk->pSpec = Extra_UtilStrsav( pFileName );
250

Alan Mishchenko committed
251
    vGlobalLtlArray = Vec_PtrAlloc( 100 );
252 253
    Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
        Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
254
    Vec_PtrFreeP( &vGlobalLtlArray );
Alan Mishchenko committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
    return pNtk;
}

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

  Synopsis    [Allocates the BLIF parsing structure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static Io_MvMan_t * Io_MvAlloc()
{
    Io_MvMan_t * p;
Alan Mishchenko committed
272
    p = ABC_ALLOC( Io_MvMan_t, 1 );
Alan Mishchenko committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
    memset( p, 0, sizeof(Io_MvMan_t) );
    p->vLines   = Vec_PtrAlloc( 512 );
    p->vModels  = Vec_PtrAlloc( 512 );
    p->vTokens  = Vec_PtrAlloc( 512 );
    p->vTokens2 = Vec_PtrAlloc( 512 );
    p->vFunc    = Vec_StrAlloc( 512 );
    return p;
}

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

  Synopsis    [Frees the BLIF parsing structure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvFree( Io_MvMan_t * p )
{
    Io_MvMod_t * pMod;
    int i;
    if ( p->pDesign )
298
        Abc_DesFree( p->pDesign, NULL );
Alan Mishchenko committed
299
    if ( p->pBuffer )  
Alan Mishchenko committed
300
        ABC_FREE( p->pBuffer );
Alan Mishchenko committed
301 302 303 304
    if ( p->vLines )
        Vec_PtrFree( p->vLines  );
    if ( p->vModels )
    {
305
        Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
Alan Mishchenko committed
306 307 308 309 310 311
            Io_MvModFree( pMod );
        Vec_PtrFree( p->vModels );
    }
    Vec_PtrFree( p->vTokens );
    Vec_PtrFree( p->vTokens2 );
    Vec_StrFree( p->vFunc );
Alan Mishchenko committed
312
    ABC_FREE( p );
Alan Mishchenko committed
313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
}

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

  Synopsis    [Allocates the BLIF parsing structure for one model.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static Io_MvMod_t * Io_MvModAlloc()
{
    Io_MvMod_t * p;
Alan Mishchenko committed
329
    p = ABC_ALLOC( Io_MvMod_t, 1 );
Alan Mishchenko committed
330 331 332 333
    memset( p, 0, sizeof(Io_MvMod_t) );
    p->vInputs  = Vec_PtrAlloc( 512 );
    p->vOutputs = Vec_PtrAlloc( 512 );
    p->vLatches = Vec_PtrAlloc( 512 );
334
    p->vFlops   = Vec_PtrAlloc( 512 );
Alan Mishchenko committed
335 336 337
    p->vResets  = Vec_PtrAlloc( 512 );
    p->vNames   = Vec_PtrAlloc( 512 );
    p->vSubckts = Vec_PtrAlloc( 512 );
Alan Mishchenko committed
338
    p->vShorts  = Vec_PtrAlloc( 512 );
Alan Mishchenko committed
339
    p->vOnehots = Vec_PtrAlloc( 512 );
Alan Mishchenko committed
340
    p->vMvs     = Vec_PtrAlloc( 512 );
341 342
    p->vConstrs = Vec_PtrAlloc( 512 );
    p->vLtlProperties = Vec_PtrAlloc( 512 );
Alan Mishchenko committed
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
    return p;
}

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

  Synopsis    [Allocates the BLIF parsing structure for one model.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvModFree( Io_MvMod_t * p )
{
//    if ( p->pNtk )
//        Abc_NtkDelete( p->pNtk );
Alan Mishchenko committed
361
    Vec_PtrFree( p->vLtlProperties );
Alan Mishchenko committed
362 363 364
    Vec_PtrFree( p->vInputs );
    Vec_PtrFree( p->vOutputs );
    Vec_PtrFree( p->vLatches );
365
    Vec_PtrFree( p->vFlops );
Alan Mishchenko committed
366 367 368
    Vec_PtrFree( p->vResets );
    Vec_PtrFree( p->vNames );
    Vec_PtrFree( p->vSubckts );
Alan Mishchenko committed
369
    Vec_PtrFree( p->vShorts );
Alan Mishchenko committed
370
    Vec_PtrFree( p->vOnehots );
Alan Mishchenko committed
371
    Vec_PtrFree( p->vMvs );
372
    Vec_PtrFree( p->vConstrs );
Alan Mishchenko committed
373
    ABC_FREE( p );
Alan Mishchenko committed
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527
}



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

  Synopsis    [Counts the number of given chars.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvCountChars( char * pLine, char Char )
{
    char * pCur;
    int Counter = 0;
    for ( pCur = pLine; *pCur; pCur++ )
        if ( *pCur == Char )
            Counter++;
    return Counter;
}

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

  Synopsis    [Returns the place where the arrow is hiding.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Io_MvFindArrow( char * pLine )
{
    char * pCur;
    for ( pCur = pLine; *(pCur+1); pCur++ )
        if ( *pCur == '-' && *(pCur+1) == '>' )
        {
            *pCur = ' ';
            *(pCur+1) = ' ';
            return pCur;
        }
    return NULL;
}

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

  Synopsis    [Collects the already split tokens.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput )
{
    char * pCur;
    Vec_PtrClear( vTokens );
    for ( pCur = pInput; pCur < pOutput; pCur++ )
    {
        if ( *pCur == 0 )
            continue;
        Vec_PtrPush( vTokens, pCur );
        while ( *++pCur );
    }
}

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

  Synopsis    [Splits the line into tokens.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop )
{
    char * pCur;
    // clear spaces
    for ( pCur = pLine; *pCur != Stop; pCur++ )
        if ( Io_MvCharIsSpace(*pCur) )
            *pCur = 0;
    // collect tokens
    Io_MvCollectTokens( vTokens, pLine, pCur );
}

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

  Synopsis    [Splits the line into tokens when .default may be present.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvSplitIntoTokensMv( Vec_Ptr_t * vTokens, char * pLine )
{
    char * pCur;
    // clear spaces
    for ( pCur = pLine; *pCur != '.' || *(pCur+1) == 'd'; pCur++ )
        if ( Io_MvCharIsSpace(*pCur) )
            *pCur = 0;
    // collect tokens
    Io_MvCollectTokens( vTokens, pLine, pCur );
}

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

  Synopsis    [Splits the line into tokens.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char )
{
    char * pCur;
    // clear spaces
    for ( pCur = pLine; *pCur != Stop; pCur++ )
        if ( Io_MvCharIsSpace(*pCur) || *pCur == Char )
            *pCur = 0;
    // collect tokens
    Io_MvCollectTokens( vTokens, pLine, pCur );
}

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

  Synopsis    [Returns the 1-based number of the line in which the token occurs.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvGetLine( Io_MvMan_t * p, char * pToken )
{
    char * pLine;
    int i;
528
    Vec_PtrForEachEntry( char *, p->vLines, pLine, i )
Alan Mishchenko committed
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544
        if ( pToken < pLine )
            return i;
    return -1;
}

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

  Synopsis    [Reads the file into a character buffer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
545 546 547 548 549 550
typedef struct buflist {
  char buf[1<<20];
  int nBuf;
  struct buflist * next;
} buflist;

551
char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize )
552 553 554 555 556
{
    FILE    * pFile;
    int       nFileSize = 0;
    char    * pContents;
    BZFILE  * b;
Alan Mishchenko committed
557
    int       bzError, RetValue;
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
    struct buflist * pNext;
    buflist * bufHead = NULL, * buf = NULL;

    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        Abc_Print( -1, "Io_MvLoadFileBz2(): The file is unavailable (absent or open).\n" );
        return NULL;
    }
    b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0);
    if (bzError != BZ_OK) {
        Abc_Print( -1, "Io_MvLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError );
        return NULL;
    }
    do {
        if (!bufHead)
            buf = bufHead = ABC_ALLOC( buflist, 1 );
        else
            buf = buf->next = ABC_ALLOC( buflist, 1 );
        nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20);
        buf->next = NULL;
    } while (bzError == BZ_OK);
    if (bzError == BZ_STREAM_END) {
        // we're okay
        char * p;
        int nBytes = 0;
        BZ2_bzReadClose(&bzError,b);
        p = pContents = ABC_ALLOC( char, nFileSize + 10 );
        buf = bufHead;
        do {
            memcpy(p+nBytes,buf->buf,buf->nBuf);
            nBytes += buf->nBuf;
//        } while((buf = buf->next));
            pNext = buf->next;
            ABC_FREE( buf );
        } while((buf = pNext));
    } else if (bzError == BZ_DATA_ERROR_MAGIC) {
        // not a BZIP2 file
        BZ2_bzReadClose(&bzError,b);
        fseek( pFile, 0, SEEK_END );
        nFileSize = ftell( pFile );
        if ( nFileSize == 0 )
        {
            Abc_Print( -1, "Io_MvLoadFileBz2(): The file is empty.\n" );
            return NULL;
        }
        pContents = ABC_ALLOC( char, nFileSize + 10 );
        rewind( pFile );
Alan Mishchenko committed
606
        RetValue = fread( pContents, nFileSize, 1, pFile );
607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
    } else { 
        // Some other error.
        Abc_Print( -1, "Io_MvLoadFileBz2(): Unable to read the compressed BLIF.\n" );
        return NULL;
    }
    fclose( pFile );
    // finish off the file with the spare .end line
    // some benchmarks suddenly break off without this line
    strcpy( pContents + nFileSize, "\n.end\n" );
    *pnFileSize = nFileSize;
    return pContents;
}

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

  Synopsis    [Reads the file into a character buffer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Io_MvLoadFileGz( char * pFileName, int * pnFileSize )
{
    const int READ_BLOCK_SIZE = 100000;
    gzFile pFile;
    char * pContents;
    int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
    pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
    pContents = ABC_ALLOC( char, nFileSize );        
    readBlock = 0;
    while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
        //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
        nFileSize += READ_BLOCK_SIZE;
        pContents = ABC_REALLOC(char, pContents, nFileSize);
        ++readBlock;
    }
    //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
    assert( amtRead != -1 ); // indicates a zlib error
    nFileSize -= (READ_BLOCK_SIZE - amtRead);
    gzclose(pFile);
    *pnFileSize = nFileSize;
    return pContents;
}

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

  Synopsis    [Reads the file into a character buffer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
665 666 667 668 669
static char * Io_MvLoadFile( char * pFileName )
{
    FILE * pFile;
    int nFileSize;
    char * pContents;
670
    int RetValue;
671 672 673 674
    if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
        return Io_MvLoadFileBz2( pFileName, &nFileSize );
    if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
        return Io_MvLoadFileGz( pFileName, &nFileSize );
Alan Mishchenko committed
675 676 677 678 679 680 681 682 683 684
    pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Io_MvLoadFile(): The file is unavailable (absent or open).\n" );
        return NULL;
    }
    fseek( pFile, 0, SEEK_END );  
    nFileSize = ftell( pFile ); 
    if ( nFileSize == 0 )
    {
685
        fclose( pFile );
Alan Mishchenko committed
686 687 688
        printf( "Io_MvLoadFile(): The file is empty.\n" );
        return NULL;
    }
Alan Mishchenko committed
689
    pContents = ABC_ALLOC( char, nFileSize + 10 );
Alan Mishchenko committed
690
    rewind( pFile );
691
    RetValue = fread( pContents, nFileSize, 1, pFile );
Alan Mishchenko committed
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
    fclose( pFile );
    // finish off the file with the spare .end line
    // some benchmarks suddenly break off without this line
    strcpy( pContents + nFileSize, "\n.end\n" );
    return pContents;
}

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

  Synopsis    [Prepares the parsing.]

  Description [Performs several preliminary operations:
  - Cuts the file buffer into separate lines.
  - Removes comments and line extenders.
  - Sorts lines by directives.
  - Estimates the number of objects.
  - Allocates room for the objects.
  - Allocates room for the hash table.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Io_MvReadPreparse( Io_MvMan_t * p )
{
    char * pCur, * pPrev;
    int i, fComment = 0;
    // parse the buffer into lines and remove comments
    Vec_PtrPush( p->vLines, p->pBuffer );
    for ( pCur = p->pBuffer; *pCur; pCur++ )
    {
        if ( *pCur == '\n' )
        {
            *pCur = 0;
//            if ( *(pCur-1) == '\r' )
//                *(pCur-1) = 0;
            fComment = 0;
            Vec_PtrPush( p->vLines, pCur + 1 );
        }
        else if ( *pCur == '#' )
            fComment = 1;
        // remove comments
        if ( fComment )
            *pCur = 0;
    }

    // unfold the line extensions and sort lines by directive
740
    Vec_PtrForEachEntry( char *, p->vLines, pCur, i )
Alan Mishchenko committed
741 742 743 744 745 746 747 748
    {
        if ( *pCur == 0 )
            continue;
        // find previous non-space character
        for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- )
            if ( !Io_MvCharIsSpace(*pPrev) )
                break;
        // if it is the line extender, overwrite it with spaces
749
        if ( pPrev >= p->pBuffer && *pPrev == '\\' )
Alan Mishchenko committed
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764
        {
            for ( ; *pPrev; pPrev++ )
                *pPrev = ' ';
            *pPrev = ' ';
            continue;
        }
        // skip spaces at the beginning of the line
        while ( Io_MvCharIsSpace(*pCur++) );
        // parse directives
        if ( *(pCur-1) != '.' )
            continue;
        if ( !strncmp(pCur, "names", 5) || !strncmp(pCur, "table", 5) || !strncmp(pCur, "gate", 4) )
            Vec_PtrPush( p->pLatest->vNames, pCur );
        else if ( p->fBlifMv && (!strncmp(pCur, "def ", 4) || !strncmp(pCur, "default ", 8)) )
            continue;
765 766
        else if ( !strncmp( pCur, "ltlformula", 10 ) )
            Vec_PtrPush( p->pLatest->vLtlProperties, pCur );
Alan Mishchenko committed
767 768
        else if ( !strncmp(pCur, "latch", 5) )
            Vec_PtrPush( p->pLatest->vLatches, pCur );
769 770
        else if ( !strncmp(pCur, "flop", 4) )
            Vec_PtrPush( p->pLatest->vFlops, pCur );
Alan Mishchenko committed
771 772 773 774 775 776 777 778
        else if ( !strncmp(pCur, "r ", 2) || !strncmp(pCur, "reset ", 6) )
            Vec_PtrPush( p->pLatest->vResets, pCur );
        else if ( !strncmp(pCur, "inputs", 6) )
            Vec_PtrPush( p->pLatest->vInputs, pCur );
        else if ( !strncmp(pCur, "outputs", 7) )
            Vec_PtrPush( p->pLatest->vOutputs, pCur );
        else if ( !strncmp(pCur, "subckt", 6) )
            Vec_PtrPush( p->pLatest->vSubckts, pCur );
Alan Mishchenko committed
779 780
        else if ( !strncmp(pCur, "short", 5) )
            Vec_PtrPush( p->pLatest->vShorts, pCur );
Alan Mishchenko committed
781 782
        else if ( !strncmp(pCur, "onehot", 6) )
            Vec_PtrPush( p->pLatest->vOnehots, pCur );
Alan Mishchenko committed
783 784
        else if ( p->fBlifMv && !strncmp(pCur, "mv", 2) )
            Vec_PtrPush( p->pLatest->vMvs, pCur );
785 786
        else if ( !strncmp(pCur, "constraint", 10) )
            Vec_PtrPush( p->pLatest->vConstrs, pCur );
Alan Mishchenko committed
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802
        else if ( !strncmp(pCur, "blackbox", 8) )
            p->pLatest->fBlackBox = 1;
        else if ( !strncmp(pCur, "model", 5) ) 
        {
            p->pLatest = Io_MvModAlloc();
            p->pLatest->pName = pCur;
            p->pLatest->pMan = p;
        }
        else if ( !strncmp(pCur, "end", 3) )
        {
            if ( p->pLatest )
                Vec_PtrPush( p->vModels, p->pLatest );
            p->pLatest = NULL;
        }
        else if ( !strncmp(pCur, "exdc", 4) )
        {
803 804
//            fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) );
            fprintf( stdout, "Warning: The design contains EXDC network.\n" );
805 806
            if ( p->pLatest )
                Vec_PtrPush( p->vModels, p->pLatest );
807 808 809
            p->pLatest = Io_MvModAlloc();
            p->pLatest->pName = NULL;
            p->pLatest->pMan = p;
Alan Mishchenko committed
810
        }
Alan Mishchenko committed
811 812
        else if ( !strncmp(pCur, "attrib", 6) )
        {}
Alan Mishchenko committed
813 814
        else if ( !strncmp(pCur, "delay", 5) )
        {}
Alan Mishchenko committed
815 816 817
        else if ( !strncmp(pCur, "input_", 6) )
        {}
        else if ( !strncmp(pCur, "output_", 7) )
Alan Mishchenko committed
818
        {}
Alan Mishchenko committed
819
        else if ( !strncmp(pCur, "no_merge", 8) )
Alan Mishchenko committed
820
        {}
821 822
        else if ( !strncmp(pCur, "wd", 2) )
        {}
Alan Mishchenko committed
823 824
//        else if ( !strncmp(pCur, "inouts", 6) )
//        {}
Alan Mishchenko committed
825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845
        else
        {
            pCur--;
            if ( pCur[strlen(pCur)-1] == '\r' )
                pCur[strlen(pCur)-1] = 0;
            fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Io_MvGetLine(p, pCur), pCur );
        }
    }
}

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

  Synopsis    [Parses interfaces of the models.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
846
static int Io_MvReadInterfaces( Io_MvMan_t * p )
Alan Mishchenko committed
847 848 849
{
    Io_MvMod_t * pMod;
    char * pLine;
850
    int i, k, nOutsOld;
Alan Mishchenko committed
851
    // iterate through the models
852
    Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
Alan Mishchenko committed
853 854 855
    {
        // parse the model
        if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
Alan Mishchenko committed
856
            return 0;
Alan Mishchenko committed
857
        // add model to the design
858
        if ( !Abc_DesAddModel( p->pDesign, pMod->pNtk ) )
Alan Mishchenko committed
859 860
        {
            sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName );
Alan Mishchenko committed
861
            return 0;
Alan Mishchenko committed
862 863
        }
        // parse the inputs
864
        Vec_PtrForEachEntry( char *, pMod->vInputs, pLine, k )
Alan Mishchenko committed
865
            if ( !Io_MvParseLineInputs( pMod, pLine ) )
Alan Mishchenko committed
866
                return 0;
Alan Mishchenko committed
867
        // parse the outputs
868
        Vec_PtrForEachEntry( char *, pMod->vOutputs, pLine, k )
Alan Mishchenko committed
869
            if ( !Io_MvParseLineOutputs( pMod, pLine ) )
Alan Mishchenko committed
870
                return 0;
871 872 873 874 875 876 877 878 879
        // parse the constraints
        nOutsOld = Abc_NtkPoNum(pMod->pNtk);
        Vec_PtrForEachEntry( char *, pMod->vConstrs, pLine, k )
            if ( !Io_MvParseLineConstrs( pMod, pLine ) )
                return 0;
        pMod->pNtk->nConstrs = Abc_NtkPoNum(pMod->pNtk) - nOutsOld;
        Vec_PtrForEachEntry( char *, pMod->vLtlProperties, pLine, k )
            if ( !Io_MvParseLineLtlProperty( pMod, pLine ) )
                return 0;
880 881
        // report the results
#ifdef IO_VERBOSE_OUTPUT
882 883 884 885
        if ( Vec_PtrSize(p->vModels) > 1 )
            printf( "Parsed %-32s: PI =%6d  PO =%6d  ND =%8d  FF =%6d  B =%6d\n", 
                pMod->pNtk->pName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkPoNum(pMod->pNtk),
                Vec_PtrSize(pMod->vNames), Vec_PtrSize(pMod->vLatches), Vec_PtrSize(pMod->vSubckts) );
886
#endif
Alan Mishchenko committed
887
    }
Alan Mishchenko committed
888
    return 1;
Alan Mishchenko committed
889 890 891 892 893 894 895 896 897 898 899 900 901 902
}


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

  Synopsis    []

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
903
static Abc_Des_t * Io_MvParse( Io_MvMan_t * p )
Alan Mishchenko committed
904
{
905
    Abc_Des_t * pDesign;
Alan Mishchenko committed
906 907 908 909
    Io_MvMod_t * pMod;
    char * pLine;
    int i, k;
    // iterate through the models
910
    Vec_PtrForEachEntry( Io_MvMod_t *, p->vModels, pMod, i )
Alan Mishchenko committed
911
    { 
912
#ifdef IO_VERBOSE_OUTPUT
913 914
        if ( Vec_PtrSize(p->vModels) > 1 )
            printf( "Parsing model %s...\n", pMod->pNtk->pName );
915 916
#endif

Alan Mishchenko committed
917 918 919 920
        // check if there any MV lines
        if ( Vec_PtrSize(pMod->vMvs) > 0 )
            Abc_NtkStartMvVars( pMod->pNtk );
        // parse the mv lines
921
        Vec_PtrForEachEntry( char *, pMod->vMvs, pLine, k )
Alan Mishchenko committed
922 923 924 925 926 927 928 929 930 931 932 933 934 935 936
            if ( !Io_MvParseLineMv( pMod, pLine ) )
                return NULL;
        // if reset lines are used there should be the same number of them as latches
        if ( Vec_PtrSize(pMod->vResets) > 0 )
        {
            if ( Vec_PtrSize(pMod->vLatches) != Vec_PtrSize(pMod->vResets) )
            {
                sprintf( p->sError, "Line %d: Model %s has different number of latches (%d) and reset nodes (%d).", 
                    Io_MvGetLine(p, pMod->pName), Abc_NtkName(pMod->pNtk), Vec_PtrSize(pMod->vLatches), Vec_PtrSize(pMod->vResets) );
                return NULL;
            }
            // create binary latch with 1-data and 0-init
            if ( p->fUseReset ) 
                pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv );
        }
937 938 939 940
        // parse the flops
        Vec_PtrForEachEntry( char *, pMod->vFlops, pLine, k )
            if ( !Io_MvParseLineFlop( pMod, pLine ) )
                return NULL;
Alan Mishchenko committed
941
        // parse the latches
942
        Vec_PtrForEachEntry( char *, pMod->vLatches, pLine, k )
Alan Mishchenko committed
943 944 945 946
            if ( !Io_MvParseLineLatch( pMod, pLine ) )
                return NULL;
        // parse the reset lines
        if ( p->fUseReset )
947
            Vec_PtrForEachEntry( char *, pMod->vResets, pLine, k )
Alan Mishchenko committed
948 949 950 951 952
                if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) )
                    return NULL;
        // parse the nodes
        if ( p->fBlifMv )
        {
953
            Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
Alan Mishchenko committed
954 955 956 957 958
                if ( !Io_MvParseLineNamesMv( pMod, pLine, 0 ) )
                    return NULL;
        }
        else
        {
959
            Vec_PtrForEachEntry( char *, pMod->vNames, pLine, k )
Alan Mishchenko committed
960 961
                if ( !Io_MvParseLineNamesBlif( pMod, pLine ) )
                    return NULL;
962
            Vec_PtrForEachEntry( char *, pMod->vShorts, pLine, k )
Alan Mishchenko committed
963 964
                if ( !Io_MvParseLineShortBlif( pMod, pLine ) )
                    return NULL;
Alan Mishchenko committed
965 966
        }
        // parse the subcircuits
967
        Vec_PtrForEachEntry( char *, pMod->vSubckts, pLine, k )
Alan Mishchenko committed
968 969
            if ( !Io_MvParseLineSubckt( pMod, pLine ) )
                return NULL;
Alan Mishchenko committed
970 971

        // allow for blackboxes without .blackbox line
Alan Mishchenko committed
972
        if ( Abc_NtkLatchNum(pMod->pNtk) == 0 && Abc_NtkNodeNum(pMod->pNtk) == 0 && Abc_NtkBoxNum(pMod->pNtk) == 0 )
Alan Mishchenko committed
973 974
        {
            if ( pMod->pNtk->ntkFunc == ABC_FUNC_SOP )
Alan Mishchenko committed
975
            {
976
                Mem_FlexStop( (Mem_Flex_t *)pMod->pNtk->pManFunc, 0 );
Alan Mishchenko committed
977
                pMod->pNtk->pManFunc = NULL;
Alan Mishchenko committed
978
                pMod->pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
Alan Mishchenko committed
979
            }
Alan Mishchenko committed
980 981
        }

Alan Mishchenko committed
982 983
        // finalize the network
        Abc_NtkFinalizeRead( pMod->pNtk );
Alan Mishchenko committed
984 985 986 987 988 989 990
        // read the one-hotness lines
        if ( Vec_PtrSize(pMod->vOnehots) > 0 )
        {
            Vec_Int_t * vLine; 
            Abc_Obj_t * pObj;
            // set register numbers
            Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
Alan Mishchenko committed
991
                pObj->pNext = (Abc_Obj_t *)(ABC_PTRINT_T)k;
Alan Mishchenko committed
992 993
            // derive register
            pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
994
            Vec_PtrForEachEntry( char *, pMod->vOnehots, pLine, k )
Alan Mishchenko committed
995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006
            {
                vLine = Io_MvParseLineOnehot( pMod, pLine );
                if ( vLine == NULL )
                    return NULL;
                Vec_PtrPush( pMod->pNtk->vOnehots, vLine );
//                printf( "Parsed %d one-hot registers.\n", Vec_IntSize(vLine) );
            }
            // reset register numbers
            Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
                pObj->pNext = NULL;
            // print the result
            printf( "Parsed %d groups of 1-hot registers: { ", Vec_PtrSize(pMod->pNtk->vOnehots) );
1007
            Vec_PtrForEachEntry( Vec_Int_t *, pMod->pNtk->vOnehots, vLine, k )
Alan Mishchenko committed
1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019
                printf( "%d ", Vec_IntSize(vLine) );
            printf( "}\n" );
            printf( "The total number of 1-hot registers = %d. (%.2f %%)\n", 
                Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ), 
                100.0 * Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ) / Abc_NtkLatchNum(pMod->pNtk) );
            {
                extern void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots );
                char * pFileName = Extra_FileNameGenericAppend( pMod->pMan->pFileName, "_1h.blif" );
                Abc_GenOneHotIntervals( pFileName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkLatchNum(pMod->pNtk), pMod->pNtk->vOnehots );
                printf( "One-hotness condition is written into file \"%s\".\n", pFileName );
            }
        }
1020 1021 1022 1023 1024 1025
        if ( Vec_PtrSize(pMod->vFlops) )
        {
            printf( "Warning: The parser converted %d .flop lines into .latch lines\n", Vec_PtrSize(pMod->vFlops) );
            printf( "(information about set, reset, enable of the flops may be lost).\n" );
        }

Alan Mishchenko committed
1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049
    }
    if ( p->nNDnodes )
//        printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
        printf( "Warning: The parser added %d constant 0 nodes to replace non-deterministic nodes.\n", p->nNDnodes );
    // return the network
    pDesign = p->pDesign;
    p->pDesign = NULL;
    return pDesign;
}

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

  Synopsis    [Parses the model line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
Alan Mishchenko committed
1050
    char * pToken, * pPivot;
1051 1052 1053
    if ( pLine == NULL )
    {
        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
1054
        p->pNtk->pName = Extra_UtilStrsav( "EXDC" );
1055 1056
        return 1;
    }
Alan Mishchenko committed
1057
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1058
    pToken = (char *)Vec_PtrEntry( vTokens, 0 );
Alan Mishchenko committed
1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070
    assert( !strcmp(pToken, "model") );
    if ( Vec_PtrSize(vTokens) != 2 )
    {
        sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
        return 0;
    }
    if ( p->fBlackBox )
        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, 1 );
    else if ( p->pMan->fBlifMv )
        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLIFMV, 1 );
    else 
        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
Alan Mishchenko committed
1071 1072 1073
//    for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
//        if ( *pToken == '/' || *pToken == '\\' )
//            pPivot = pToken+1;
1074
    pPivot = pToken = (char *)Vec_PtrEntry(vTokens, 1);
Alan Mishchenko committed
1075
    p->pNtk->pName = Extra_UtilStrsav( pPivot );
Alan Mishchenko committed
1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095
    return 1;
}

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

  Synopsis    [Parses the inputs line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    char * pToken;
    int i;
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1096
    pToken = (char *)Vec_PtrEntry(vTokens, 0);
Alan Mishchenko committed
1097
    assert( !strcmp(pToken, "inputs") );
1098
    Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
Alan Mishchenko committed
1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119
        Io_ReadCreatePi( p->pNtk, pToken );
    return 1;
}

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

  Synopsis    [Parses the outputs line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    char * pToken;
    int i;
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1120
    pToken = (char *)Vec_PtrEntry(vTokens, 0);
Alan Mishchenko committed
1121
    assert( !strcmp(pToken, "outputs") );
1122
    Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
Alan Mishchenko committed
1123 1124 1125 1126 1127 1128
        Io_ReadCreatePo( p->pNtk, pToken );
    return 1;
}

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

1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195
  Synopsis    [Parses the outputs line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineConstrs( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    char * pToken;
    int i;
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
    pToken = (char *)Vec_PtrEntry(vTokens, 0);
    assert( !strcmp(pToken, "constraint") );
    Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
        Io_ReadCreatePo( p->pNtk, pToken );
    return 1;
}

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

  Synopsis    [Parses the LTL property line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineLtlProperty( Io_MvMod_t * p, char * pLine )
{
    int i, j;
    int quoteBegin, quoteEnd;
    char keyWordLtlFormula[11];
    char *actualLtlFormula;

    //checking if the line begins with the keyword "ltlformula" and
    //progressing the pointer forword
    for( i=0; i<10; i++ )
        keyWordLtlFormula[i] = pLine[i];
    quoteBegin = i;
    keyWordLtlFormula[10] = '\0';
    assert( strcmp( "ltlformula", keyWordLtlFormula ) == 0 );
    while( pLine[i] != '"' )
        i++;
    quoteBegin = i;
    i = strlen( pLine );
    while( pLine[i] != '"' )
        i--;
    quoteEnd = i;
    actualLtlFormula = (char *)malloc( sizeof(char) * (quoteEnd - quoteBegin) );
    //printf("\nThe input ltl formula = ");
    for( i = quoteBegin + 1, j = 0; i<quoteEnd; i++, j++ )
        //printf("%c", pLine[i] );
        actualLtlFormula[j] = pLine[i];
    actualLtlFormula[j] = '\0';
    Vec_PtrPush( vGlobalLtlArray, actualLtlFormula );
    return 1;
}


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

Alan Mishchenko committed
1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211
  Synopsis    [Parses the latches line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Obj_t * pObj, * pNet;
    char * pToken;
    int Init;
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
1212
    pToken = (char *)Vec_PtrEntry(vTokens,0);
Alan Mishchenko committed
1213 1214 1215 1216 1217 1218 1219 1220 1221
    assert( !strcmp(pToken, "latch") );
    if ( Vec_PtrSize(vTokens) < 3 )
    {
        sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Io_MvGetLine(p->pMan, pToken) );
        return 0;
    }
    // create latch
    if ( p->pResetLatch == NULL )
    {
1222
        pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), (char *)Vec_PtrEntry(vTokens,2) );
Alan Mishchenko committed
1223 1224 1225 1226 1227
        // get initial value
        if ( p->pMan->fBlifMv )
            Abc_LatchSetInit0( pObj );
        else
        {
Alan Mishchenko committed
1228 1229 1230
            if ( Vec_PtrSize(vTokens) > 6 )
                printf( "Warning: Line %d has .latch directive with unrecognized entries (the total of %d entries).\n", 
                    Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); 
Alan Mishchenko committed
1231
            if ( Vec_PtrSize(vTokens) > 3 )
1232
                Init = atoi( (char *)Vec_PtrEntryLast(vTokens) );
Alan Mishchenko committed
1233 1234
            else
                Init = 2;
1235
            if ( Init < 0 || Init > 3 )
Alan Mishchenko committed
1236
            {
Alan Mishchenko committed
1237
                sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
Alan Mishchenko committed
1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250
                return 0;
            }
            if ( Init == 0 )
                Abc_LatchSetInit0( pObj );
            else if ( Init == 1 )
                Abc_LatchSetInit1( pObj );
            else // if ( Init == 2 )
                Abc_LatchSetInitDc( pObj );
        }
    }
    else
    {
        // get the net corresponding to the output of the latch
1251
        pNet = Abc_NtkFindOrCreateNet( p->pNtk, (char *)Vec_PtrEntry(vTokens,2) );
Alan Mishchenko committed
1252 1253 1254
        // get the net corresponding to the latch output (feeding into reset MUX)
        pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") );
        // create latch
1255
        pObj = Io_ReadCreateLatch( p->pNtk, (char *)Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) );
Alan Mishchenko committed
1256
//        Abc_LatchSetInit0( pObj );
Alan Mishchenko committed
1257 1258 1259 1260 1261 1262 1263
        Abc_LatchSetInit0( pObj );
    }
    return 1;
}

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

1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338
  Synopsis    [Parses the latches line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineFlop( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Obj_t * pObj;
    char * pToken, * pOutput, * pInput;
    int i, Init = 2;
    assert( !p->pMan->fBlifMv );
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
    pToken = (char *)Vec_PtrEntry(vTokens,0);
    assert( !strcmp(pToken, "flop") );
    // get flop output
    Vec_PtrForEachEntry( char *, vTokens, pToken, i )
        if ( pToken[0] == 'Q' && pToken[1] == '=' )
            break;
    if ( i == Vec_PtrSize(vTokens) )
    {
        sprintf( p->pMan->sError, "Line %d: Cannot find flop output.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
        return 0;
    }
    pOutput = pToken+2;
    // get flop input
    Vec_PtrForEachEntry( char *, vTokens, pToken, i )
        if ( pToken[0] == 'D' && pToken[1] == '=' )
            break;
    if ( i == Vec_PtrSize(vTokens) )
    {
        sprintf( p->pMan->sError, "Line %d: Cannot find flop input.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
        return 0;
    }
    pInput = pToken+2;
    // create latch
    pObj = Io_ReadCreateLatch( p->pNtk, pInput, pOutput );
    // get the init value
    Vec_PtrForEachEntry( char *, vTokens, pToken, i )
    {
        if ( !strncmp( pToken, "init=", 5 ) )
        {
            Init = 0;
            if ( pToken[5] == '1' )
                Init = 1;
            else if ( pToken[5] == '2' )
                Init = 2;
            else if ( pToken[5] != '0' )
            {
                sprintf( p->pMan->sError, "Line %d: Cannot read flop init value %s.", Io_MvGetLine(p->pMan, pToken), pToken );
                return 0;
            }
            break;
        }
    }
    if ( Init < 0 || Init > 2 )
    {
        sprintf( p->pMan->sError, "Line %d: Initial state of the flop is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
        return 0;
    }
    if ( Init == 0 )
        Abc_LatchSetInit0( pObj );
    else if ( Init == 1 )
        Abc_LatchSetInit1( pObj );
    else // if ( Init == 2 )
        Abc_LatchSetInitDc( pObj );
    return 1;
}

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

Alan Mishchenko committed
1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352
  Synopsis    [Parses the subckt line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Ntk_t * pModel;
    Abc_Obj_t * pBox, * pNet, * pTerm;
1353 1354
    char * pToken, * pName, * pName2, ** ppNames;
    int nEquals, Last, i, k;
Alan Mishchenko committed
1355 1356 1357 1358

    // split the line into tokens
    nEquals = Io_MvCountChars( pLine, '=' );
    Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
1359
    pToken = (char *)Vec_PtrEntry(vTokens,0);
Alan Mishchenko committed
1360
    assert( !strcmp(pToken, "subckt") );
1361
//printf( "%d ", nEquals );
Alan Mishchenko committed
1362 1363

    // get the model for this box
1364 1365 1366 1367 1368 1369 1370 1371 1372
    pName = (char *)Vec_PtrEntry(vTokens,1);
    // skip instance name for now
    for ( pToken = pName; *pToken; pToken++ )
        if ( *pToken == '|' )
        {
            *pToken = 0;
            break;
        }
    // find the model
1373
    pModel = Abc_DesFindModelByName( p->pMan->pDesign, pName );
Alan Mishchenko committed
1374 1375 1376 1377 1378
    if ( pModel == NULL )
    {
        sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Io_MvGetLine(p->pMan, pToken), pName );
        return 0;
    }
Alan Mishchenko committed
1379
/*
Alan Mishchenko committed
1380 1381 1382 1383 1384 1385 1386
    // check if the number of tokens is correct
    if ( nEquals != Abc_NtkPiNum(pModel) + Abc_NtkPoNum(pModel) )
    {
        sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).", 
            Io_MvGetLine(p->pMan, pToken), nEquals, Abc_NtkPiNum(pModel) + Abc_NtkPoNum(pModel) );
        return 0;
    }
Alan Mishchenko committed
1387
*/
Alan Mishchenko committed
1388 1389 1390 1391 1392 1393 1394 1395 1396 1397
    // get the names
    ppNames = (char **)Vec_PtrArray(vTokens) + 2 + p->pMan->fBlifMv;

    // create the box with these terminals
    if ( Abc_NtkHasBlackbox(pModel) )
        pBox = Abc_NtkCreateBlackbox( p->pNtk );
    else
        pBox = Abc_NtkCreateWhitebox( p->pNtk );
    pBox->pData = pModel;
    if ( p->pMan->fBlifMv )
1398
        Abc_ObjAssignName( pBox, (char *)Vec_PtrEntry(vTokens,2), NULL );
Alan Mishchenko committed
1399
    // go through formal inputs
1400
    Last = 0;
Alan Mishchenko committed
1401
    Abc_NtkForEachPi( pModel, pTerm, i )
Alan Mishchenko committed
1402 1403
    { 
        // find this terminal among the actual inputs of the subcircuit
1404
        pName2 = NULL;
Alan Mishchenko committed
1405 1406
        pName = Abc_ObjName(Abc_ObjFanout0(pTerm));
        for ( k = 0; k < nEquals; k++ )
1407 1408 1409 1410
            if ( !strcmp( ppNames[2*((k+Last)%nEquals)], pName ) )
            {
                pName2 = ppNames[2*((k+Last)%nEquals)+1];
                Last = k+Last+1;
Alan Mishchenko committed
1411
                break;
1412
            }
Alan Mishchenko committed
1413
/*
Alan Mishchenko committed
1414 1415 1416 1417 1418 1419
        if ( k == nEquals )
        {
            sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.", 
                Io_MvGetLine(p->pMan, pToken), pName, Abc_NtkName(pModel) );
            return 0;
        }
Alan Mishchenko committed
1420
*/
1421
        if ( pName2 == NULL )
Alan Mishchenko committed
1422 1423
        {
            Abc_Obj_t * pNode = Abc_NtkCreateNode( p->pNtk );
1424
            pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, " 0\n" );
Alan Mishchenko committed
1425 1426 1427 1428 1429 1430 1431
            pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNode, "abc") );
            Abc_ObjAddFanin( pNet, pNode );
            pTerm = Abc_NtkCreateBi( p->pNtk );
            Abc_ObjAddFanin( pBox, pTerm );
            Abc_ObjAddFanin( pTerm, pNet );
            continue;
        }
1432 1433
        assert( pName2 != NULL );
  
Alan Mishchenko committed
1434
        // create the BI with the actual name
1435
        pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName2 );
Alan Mishchenko committed
1436 1437 1438 1439
        pTerm = Abc_NtkCreateBi( p->pNtk );
        Abc_ObjAddFanin( pBox, pTerm );
        Abc_ObjAddFanin( pTerm, pNet );
    }
Alan Mishchenko committed
1440
    // go through formal outputs
1441
    Last = 0;
Alan Mishchenko committed
1442 1443
    Abc_NtkForEachPo( pModel, pTerm, i )
    {
Alan Mishchenko committed
1444
        // find this terminal among the actual outputs of the subcircuit
1445
        pName2 = NULL;
Alan Mishchenko committed
1446 1447
        pName = Abc_ObjName(Abc_ObjFanin0(pTerm));
        for ( k = 0; k < nEquals; k++ )
1448 1449 1450 1451
            if ( !strcmp( ppNames[2*((k+Last)%nEquals)], pName ) )
            {
                pName2 = ppNames[2*((k+Last)%nEquals)+1];
                Last = k+Last+1;
Alan Mishchenko committed
1452
                break;
1453
            }
Alan Mishchenko committed
1454
/*
Alan Mishchenko committed
1455 1456 1457 1458 1459 1460
        if ( k == nEquals )
        {
            sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the modell \"%s\" as a formal output of the subcircuit.", 
                Io_MvGetLine(p->pMan, pToken), pName, Abc_NtkName(pModel) );
            return 0;
        }
Alan Mishchenko committed
1461
*/
1462

Alan Mishchenko committed
1463 1464
        // create the BI with the actual name
        pTerm = Abc_NtkCreateBo( p->pNtk );
1465
        pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName2 == NULL  ? Abc_ObjNameSuffix(pTerm, "abc") : pName2 );
Alan Mishchenko committed
1466 1467 1468 1469 1470 1471
        Abc_ObjAddFanin( pNet, pTerm );
        Abc_ObjAddFanin( pTerm, pBox );
    }
    return 1;
}

Alan Mishchenko committed
1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494
/**Function*************************************************************

  Synopsis    [Parses the subckt line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
//    Vec_Ptr_t * vResult;
    Vec_Int_t * vResult;
    Abc_Obj_t * pNet, * pTerm;
    char * pToken;
    int nEquals, i;

    // split the line into tokens
    nEquals = Io_MvCountChars( pLine, '=' );
    Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
1495
    pToken = (char *)Vec_PtrEntry(vTokens,0);
Alan Mishchenko committed
1496 1497 1498 1499 1500
    assert( !strcmp(pToken, "onehot") );

    // iterate through the register names
//    vResult = Vec_PtrAlloc( Vec_PtrSize(vTokens) );
    vResult = Vec_IntAlloc( Vec_PtrSize(vTokens) );
1501
    Vec_PtrForEachEntryStart( char *, vTokens, pToken, i, 1 )
Alan Mishchenko committed
1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520
    {
        // check if this register exists
        pNet = Abc_NtkFindNet( p->pNtk, pToken );
        if ( pNet == NULL )
        {
            sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" does not exist in the model \"%s\".", 
                Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
            return NULL;
        }
        // check if this is register output net
        pTerm = Abc_ObjFanin0( pNet );
        if ( pTerm == NULL || Abc_ObjFanin0(pTerm) == NULL || !Abc_ObjIsLatch(Abc_ObjFanin0(pTerm)) )
        {
            sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" is not a register in the model \"%s\".", 
                Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
            return NULL;
        }
        // save register name
//        Vec_PtrPush( vResult, Abc_ObjName(pNet) );
Alan Mishchenko committed
1521
        Vec_IntPush( vResult, (int)(ABC_PTRINT_T)Abc_ObjFanin0(pTerm)->pNext );
Alan Mishchenko committed
1522
//        printf( "%d(%d) ", (int)Abc_ObjFanin0(pTerm)->pNext, ((int)Abc_ObjFanin0(pTerm)->pData) -1 );
Alan Mishchenko committed
1523
        printf( "%d", ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pTerm)->pData)-1 );
Alan Mishchenko committed
1524 1525 1526 1527 1528
    }
    printf( "\n" );
    return vResult;
}

Alan Mishchenko committed
1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544

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

  Synopsis    [Parses the mv line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Obj_t * pObj;
Alan Mishchenko committed
1545
    Io_MvVar_t * pVar = NULL;
1546
    Mem_Flex_t * pFlex;
Alan Mishchenko committed
1547 1548 1549 1550 1551
    char * pName;
    int nCommas, nValues, i, k;
    // count commas and get the tokens
    nCommas = Io_MvCountChars( pLine, ',' );
    Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', ',' );
1552
    pName = (char *)Vec_PtrEntry(vTokens,0);
Alan Mishchenko committed
1553 1554 1555 1556
    assert( !strcmp(pName, "mv") );
    // get the number of values
    if ( Vec_PtrSize(vTokens) <= nCommas + 2 )
    {
Alan Mishchenko committed
1557
        sprintf( p->pMan->sError, "Line %d: The number of values in not specified in .mv line.", Io_MvGetLine(p->pMan, pName) );
Alan Mishchenko committed
1558 1559
        return 0;
    }
1560
    nValues = atoi( (char *)Vec_PtrEntry(vTokens,nCommas+2) );
Alan Mishchenko committed
1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576
    if ( nValues < 2 || nValues > IO_BLIFMV_MAXVALUES )
    {
        sprintf( p->pMan->sError, "Line %d: The number of values (%d) is incorrect (should be >= 2 and <= %d).", 
            Io_MvGetLine(p->pMan, pName), nValues, IO_BLIFMV_MAXVALUES );
        return 0;
    }
    // if there is no symbolic values, quit
    if ( nValues == 2 && Vec_PtrSize(vTokens) == nCommas + 3 )
        return 1;
    if ( Vec_PtrSize(vTokens) > nCommas + 3 && Vec_PtrSize(vTokens) - (nCommas + 3) != nValues )
    {
        sprintf( p->pMan->sError, "Line %d: Wrong number (%d) of symbolic value names (should be %d).", 
            Io_MvGetLine(p->pMan, pName), Vec_PtrSize(vTokens) - (nCommas + 3), nValues );
        return 0;
    }
    // go through variables
1577
    pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( p->pNtk );
Alan Mishchenko committed
1578 1579
    for ( i = 0; i <= nCommas; i++ )
    {
1580
        pName = (char *)Vec_PtrEntry( vTokens, i+1 );
Alan Mishchenko committed
1581 1582
        pObj = Abc_NtkFindOrCreateNet( p->pNtk, pName );
        // allocate variable
1583
        pVar = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
Alan Mishchenko committed
1584 1585 1586 1587 1588
        pVar->nValues = nValues;
        pVar->pNames = NULL;
        // create names
        if ( Vec_PtrSize(vTokens) > nCommas + 3 )
        {
1589
            pVar->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * nValues );
1590
            Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nCommas + 3 )
Alan Mishchenko committed
1591
            {
1592
                pVar->pNames[k-(nCommas + 3)] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pName) + 1 );
Alan Mishchenko committed
1593 1594 1595 1596 1597 1598 1599
                strcpy( pVar->pNames[k-(nCommas + 3)], pName );
            }
        }
        // save the variable
        Abc_ObjSetMvVar( pObj, pVar );
    }
    // make sure the names are unique
Alan Mishchenko committed
1600
    assert(pVar);
Alan Mishchenko committed
1601 1602 1603 1604 1605 1606
    if ( pVar->pNames )
    {
        for ( i = 0; i < nValues; i++ )
        for ( k = i+1; k < nValues; k++ )
            if ( !strcmp(pVar->pNames[i], pVar->pNames[k]) )
            {
1607
                pName = (char *)Vec_PtrEntry(vTokens,0);
Alan Mishchenko committed
1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635
                sprintf( p->pMan->sError, "Line %d: Symbolic value name \"%s\" is repeated in .mv line.", 
                    Io_MvGetLine(p->pMan, pName), pVar->pNames[i] );
                return 0;
            }
    }
    return 1;
}

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

  Synopsis    [Writes the values into the BLIF-MV representation for the node.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvWriteValues( Abc_Obj_t * pNode, Vec_Str_t * vFunc )
{
    char Buffer[10];
    Abc_Obj_t * pFanin;
    int i;
    // add the fanin number of values
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
        sprintf( Buffer, "%d", Abc_ObjMvVarNum(pFanin) );
1636
        Vec_StrPrintStr( vFunc, Buffer );
Alan Mishchenko committed
1637 1638 1639 1640
        Vec_StrPush( vFunc, ' ' );
    }
    // add the node number of values
    sprintf( Buffer, "%d", Abc_ObjMvVarNum(Abc_ObjFanout0(pNode)) );
1641
    Vec_StrPrintStr( vFunc, Buffer );
Alan Mishchenko committed
1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678
    Vec_StrPush( vFunc, '\n' );
    return 1;
}

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

  Synopsis    [Translated one literal.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLiteralMv( Io_MvMod_t * p, Abc_Obj_t * pNode, char * pToken, Vec_Str_t * vFunc, int iLit )
{
    char Buffer[10];
    Io_MvVar_t * pVar;
    Abc_Obj_t * pFanin, * pNet;
    char * pCur, * pNext;
    int i;
    // consider the equality literal
    if ( pToken[0] == '=' )
    {
        // find the fanins
        Abc_ObjForEachFanin( pNode, pFanin, i )
            if ( !strcmp( Abc_ObjName(pFanin), pToken + 1 ) )
                break;
        if ( i == Abc_ObjFaninNum(pNode) )
        {
            sprintf( p->pMan->sError, "Line %d: Node name in the table \"%s\" cannot be found on .names line.", 
                Io_MvGetLine(p->pMan, pToken), pToken + 1 );
            return 0;
        }
        Vec_StrPush( vFunc, '=' );
        sprintf( Buffer, "%d", i );
1679
        Vec_StrPrintStr( vFunc, Buffer );
Alan Mishchenko committed
1680 1681 1682 1683 1684 1685
        Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
        return 1;
    }
    // consider regular literal
    assert( iLit < Abc_ObjFaninNum(pNode) );
    pNet = iLit >= 0 ? Abc_ObjFanin(pNode, iLit) : Abc_ObjFanout0(pNode);
1686
    pVar = (Io_MvVar_t *)Abc_ObjMvVar( pNet );
Alan Mishchenko committed
1687 1688 1689
    // if the var is absent or has no symbolic values quit
    if ( pVar == NULL || pVar->pNames == NULL )
    {
1690
        Vec_StrPrintStr( vFunc, pToken );
Alan Mishchenko committed
1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718
        Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
        return 1;
    }
    // parse the literal using symbolic values
    for ( pCur = pToken; *pCur; pCur++ )
    {
        if ( Io_MvCharIsMvSymb(*pCur) )
        {
            Vec_StrPush( vFunc, *pCur );
            continue;
        }
        // find the next MvSymb char
        for ( pNext = pCur+1; *pNext; pNext++ )
            if ( Io_MvCharIsMvSymb(*pNext) )
                break;
        // look for the value name
        for ( i = 0; i < pVar->nValues; i++ )
            if ( !strncmp( pVar->pNames[i], pCur, pNext-pCur ) )
                break;
        if ( i == pVar->nValues )
        {
            *pNext = 0;
            sprintf( p->pMan->sError, "Line %d: Cannot find value name \"%s\" among the value names of variable \"%s\".", 
                Io_MvGetLine(p->pMan, pToken), pCur, Abc_ObjName(pNet) );
            return 0;
        }
        // value name is found
        sprintf( Buffer, "%d", i );
1719
        Vec_StrPrintStr( vFunc, Buffer );
Alan Mishchenko committed
1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747
        // update the pointer
        pCur = pNext - 1;
    }
    Vec_StrPush( vFunc, (char)((iLit == -1)? '\n' : ' ') );
    return 1;
}

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

  Synopsis    [Constructs the MV-SOP cover from the file parsing info.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vTokens2, int nInputs, int nOutputs, int iOut )
{
    Vec_Str_t * vFunc = p->pMan->vFunc;
    char * pFirst, * pToken;
    int iStart, i;
    // prepare the place for the cover
    Vec_StrClear( vFunc );
    // write the number of values
//    Io_MvWriteValues( pNode, vFunc );
    // get the first token
1748
    pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
Alan Mishchenko committed
1749 1750 1751 1752
    if ( pFirst[0] == '.' )
    {
        // write the default literal
        Vec_StrPush( vFunc, 'd' );
1753
        pToken = (char *)Vec_PtrEntry(vTokens2, 1 + iOut);
Alan Mishchenko committed
1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765
        if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
            return NULL;
        iStart = 1 + nOutputs;
    }
    else
        iStart = 0;
    // write the remaining literals
    while ( iStart < Vec_PtrSize(vTokens2) )
    {
        // input literals
        for ( i = 0; i < nInputs; i++ )
        {
1766
            pToken = (char *)Vec_PtrEntry( vTokens2, iStart + i );
Alan Mishchenko committed
1767 1768 1769 1770
            if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, i ) )
                return NULL;
        }
        // output literal
1771
        pToken = (char *)Vec_PtrEntry( vTokens2, iStart + nInputs + iOut );
Alan Mishchenko committed
1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808
        if ( !Io_MvParseLiteralMv( p, pNode, pToken, vFunc, -1 ) )
            return NULL;
        // update the counter
        iStart += nInputs + nOutputs;
    }       
    Vec_StrPush( vFunc, '\0' );
    return Vec_StrArray( vFunc );
}

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

  Synopsis    [Adds reset circuitry corresponding to latch with pName.]

  Description [Returns the reset node's net.]
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
{
    char Buffer[50];
    Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pOutNet;
    Io_MvVar_t * pVar;
    // make sure the reset latch exists
    assert( p->pResetLatch != NULL );
    // get the reset net
    pResetLONet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch));
    // get the output net
    pOutNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
    // get the data nets
    pData0Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_reset") );
    pData1Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_out") );
    // duplicate MV variables
    if ( Abc_NtkMvVar(p->pNtk) )
    {
1809
        pVar = (Io_MvVar_t *)Abc_ObjMvVar( pOutNet );
Alan Mishchenko committed
1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820
        Abc_ObjSetMvVar( pData0Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
        Abc_ObjSetMvVar( pData1Net, Abc_NtkMvVarDup(p->pNtk, pVar) );
    }
    // create the node
    pNode = Abc_NtkCreateNode( p->pNtk );
    // create the output net
    Abc_ObjAddFanin( pOutNet, pNode );
    // create the function
    if ( p->pMan->fBlifMv )
    {
//        Vec_Att_t * p = Abc_NtkMvVar( pNtk );
Alan Mishchenko committed
1821
//        int nValues = Abc_ObjMvVarNum(pOutNet);
Alan Mishchenko committed
1822 1823
//        sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
        sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
1824
        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, Buffer );
Alan Mishchenko committed
1825 1826
    }
    else
1827
        pNode->pData = Abc_SopCreateMux( (Mem_Flex_t *)p->pNtk->pManFunc );
Alan Mishchenko committed
1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850
    // add nets
    Abc_ObjAddFanin( pNode, pResetLONet );
    Abc_ObjAddFanin( pNode, pData1Net );
    Abc_ObjAddFanin( pNode, pData0Net );
    return pData0Net;
}

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

  Synopsis    [Parses the nodes line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Ptr_t * vTokens2, int nInputs, int nOutputs, int iOut, int fReset )
{
    Abc_Obj_t * pNet, * pNode;
    char * pName;
    // get the output name
1851
    pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + iOut );
Alan Mishchenko committed
1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887
    // create the node
    if ( fReset )
    {
        pNet = Abc_NtkFindNet( p->pNtk, pName );
        if ( pNet == NULL )
        {
            sprintf( p->pMan->sError, "Line %d: Latch with output signal \"%s\" does not exist.", Io_MvGetLine(p->pMan, pName), pName );
            return 0;
        }
/*
        if ( !Abc_ObjIsBo(Abc_ObjFanin0(pNet)) )
        {
            sprintf( p->pMan->sError, "Line %d: Reset line \"%s\" defines signal that is not a latch output.", Io_MvGetLine(p->pMan, pName), pName );
            return 0;
        }
*/
        // construct the reset circuit and get the reset net feeding into it
        pNet = Io_MvParseAddResetCircuit( p, pName );
        // create fanins
        pNode = Io_ReadCreateNode( p->pNtk, Abc_ObjName(pNet), (char **)(vTokens->pArray + 1), nInputs );
        assert( nInputs == Vec_PtrSize(vTokens) - 2 );
    }
    else
    {
        pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
        if ( Abc_ObjFaninNum(pNet) > 0 )
        {
            sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
            return 0;
        }
        pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), nInputs );
    }
    // create the cover
    pNode->pData = Io_MvParseTableMv( p, pNode, vTokens2, nInputs, nOutputs, iOut );
    if ( pNode->pData == NULL )
        return 0;
1888
    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
Alan Mishchenko committed
1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921
//printf( "Finished parsing node \"%s\" with table:\n%s\n", pName, pNode->pData );
    return 1;
}

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

  Synopsis    [Parses the nodes line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Vec_Ptr_t * vTokens2 = p->pMan->vTokens2;
    Abc_Obj_t * pNet;
    char * pName, * pFirst, * pArrow;
    int nInputs, nOutputs, nLiterals, nLines, i;
    assert( p->pMan->fBlifMv );
    // get the arrow if it is present
    pArrow = Io_MvFindArrow( pLine );
    if ( !p->pMan->fBlifMv && pArrow ) 
    {
        sprintf( p->pMan->sError, "Line %d: Multi-output node symbol (->) in binary BLIF file.", Io_MvGetLine(p->pMan, pLine) );
        return 0;
    }
    // split names line into tokens
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
    if ( fReset )
1922
        assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "r") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "reset") );
Alan Mishchenko committed
1923
    else
1924
        assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") || !strcmp((char *)Vec_PtrEntry(vTokens,0), "table") );
Alan Mishchenko committed
1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937
    // find the number of inputs and outputs
    nInputs  = Vec_PtrSize(vTokens) - 2;
    nOutputs = 1;
    if ( pArrow != NULL )
    {
        for ( i = Vec_PtrSize(vTokens) - 2; i >= 1; i-- )
            if ( pArrow < (char*)Vec_PtrEntry(vTokens,i) )
            {
                nInputs--;
                nOutputs++;
            }
    }
    // split table into tokens
1938
    pName = (char *)Vec_PtrEntryLast( vTokens );
Alan Mishchenko committed
1939
    Io_MvSplitIntoTokensMv( vTokens2, pName + strlen(pName) );
1940
    pFirst = (char *)Vec_PtrEntry( vTokens2, 0 );
Alan Mishchenko committed
1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960
    if ( pFirst[0] == '.' )
    {
        assert( pFirst[1] == 'd' );
        nLiterals = Vec_PtrSize(vTokens2) - 1 - nOutputs;
    }
    else
        nLiterals = Vec_PtrSize(vTokens2);
    // check the number of lines
    if ( nLiterals % (nInputs + nOutputs) != 0 )
    {
        sprintf( p->pMan->sError, "Line %d: Wrong number of literals in the table of node \"%s\". (Spaces inside literals are not allowed.)", Io_MvGetLine(p->pMan, pFirst), pName );
        return 0;
    }
    // check for the ND table
    nLines = nLiterals / (nInputs + nOutputs);
    if ( nInputs == 0 && nLines > 1 )
    {
        // add the outputs to the PIs
        for ( i = 0; i < nOutputs; i++ )
        {
1961
            pName = (char *)Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i );
Alan Mishchenko committed
1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002
            // get the net corresponding to this node
            pNet = Abc_NtkFindOrCreateNet(p->pNtk, pName);
            if ( fReset )
            {
                assert( p->pResetLatch != NULL );
                // construct the reset circuit and get the reset net feeding into it
                pNet = Io_MvParseAddResetCircuit( p, pName );
            }
            // add the new PI node
//            Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) );
//            fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName );
            p->pMan->nNDnodes++;
            Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(p->pNtk) );
        }
        return 1;
    }
    // iterate through the outputs
    for ( i = 0; i < nOutputs; i++ )
    {
        if ( !Io_MvParseLineNamesMvOne( p, vTokens, vTokens2, nInputs, nOutputs, i, fReset ) )
            return 0;
    }
    return 1;
}


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

  Synopsis    [Constructs the SOP cover from the file parsing info.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Vec_Str_t * vFunc = p->pMan->vFunc;
Alan Mishchenko committed
2003
    char * pProduct, * pOutput, c;
Alan Mishchenko committed
2004 2005 2006 2007 2008 2009
    int i, Polarity = -1;

    p->pMan->nTablesRead++;
    // get the tokens
    Io_MvSplitIntoTokens( vTokens, pTable, '.' );
    if ( Vec_PtrSize(vTokens) == 0 )
2010
        return Abc_SopCreateConst0( (Mem_Flex_t *)p->pNtk->pManFunc );
Alan Mishchenko committed
2011 2012
    if ( Vec_PtrSize(vTokens) == 1 )
    {
2013
        pOutput = (char *)Vec_PtrEntry( vTokens, 0 );
Alan Mishchenko committed
2014 2015
        c = pOutput[0];
        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
Alan Mishchenko committed
2016 2017 2018 2019
        {
            sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
            return NULL;
        }
2020
        return pOutput[0] == '0' ? Abc_SopCreateConst0((Mem_Flex_t *)p->pNtk->pManFunc) : Abc_SopCreateConst1((Mem_Flex_t *)p->pNtk->pManFunc);
Alan Mishchenko committed
2021
    }
2022
    pProduct = (char *)Vec_PtrEntry( vTokens, 0 );
Alan Mishchenko committed
2023 2024 2025 2026 2027 2028 2029 2030 2031
    if ( Vec_PtrSize(vTokens) % 2 == 1 )
    {
        sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Io_MvGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
        return NULL;
    }
    // parse the table
    Vec_StrClear( vFunc );
    for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
    {
2032 2033
        pProduct = (char *)Vec_PtrEntry( vTokens, 2*i + 0 );
        pOutput  = (char *)Vec_PtrEntry( vTokens, 2*i + 1 );
Alan Mishchenko committed
2034 2035 2036 2037 2038
        if ( strlen(pProduct) != (unsigned)nFanins )
        {
            sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Io_MvGetLine(p->pMan, pProduct), pProduct, nFanins );
            return NULL;
        }
Alan Mishchenko committed
2039 2040
        c = pOutput[0];
        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
Alan Mishchenko committed
2041 2042 2043 2044 2045
        {
            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Io_MvGetLine(p->pMan, pProduct), pOutput );
            return NULL;
        }
        if ( Polarity == -1 )
Alan Mishchenko committed
2046 2047
            Polarity = (c=='1' || c=='x');
        else if ( Polarity != (c=='1' || c=='x') )
Alan Mishchenko committed
2048 2049 2050 2051 2052
        {
            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity );
            return NULL;
        }
        // parse one product 
2053
        Vec_StrPrintStr( vFunc, pProduct );
Alan Mishchenko committed
2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080
        Vec_StrPush( vFunc, ' ' );
        Vec_StrPush( vFunc, pOutput[0] );
        Vec_StrPush( vFunc, '\n' );
    }
    Vec_StrPush( vFunc, '\0' );
    return Vec_StrArray( vFunc );
}

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

  Synopsis    [Parses the nodes line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Obj_t * pNet, * pNode;
    char * pName;
    assert( !p->pMan->fBlifMv );
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
    // parse the mapped node
2081
    if ( !strcmp((char *)Vec_PtrEntry(vTokens,0), "gate") )
Alan Mishchenko committed
2082 2083
        return Io_MvParseLineGateBlif( p, vTokens );
    // parse the regular name line
2084 2085
    assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "names") );
    pName = (char *)Vec_PtrEntryLast( vTokens );
Alan Mishchenko committed
2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097
    pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
    if ( Abc_ObjFaninNum(pNet) > 0 )
    {
        sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
        return 0;
    }
    // create fanins
    pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), Vec_PtrSize(vTokens) - 2 );
    // parse the table of this node
    pNode->pData = Io_MvParseTableBlif( p, pName + strlen(pName), Abc_ObjFaninNum(pNode) );
    if ( pNode->pData == NULL )
        return 0;
2098
    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
Alan Mishchenko committed
2099 2100 2101
    return 1;
}

2102 2103 2104 2105 2106 2107 2108 2109
ABC_NAMESPACE_IMPL_END

#include "map/mio/mio.h"
#include "base/main/main.h"

ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
2110 2111
/**Function*************************************************************

Alan Mishchenko committed
2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129
  Synopsis    [Parses the nodes line.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
{
    Vec_Ptr_t * vTokens = p->pMan->vTokens;
    Abc_Obj_t * pNet, * pNode;
    char * pName;
    assert( !p->pMan->fBlifMv );
    Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
    if ( Vec_PtrSize(vTokens) != 3 )
    {
2130
        sprintf( p->pMan->sError, "Line %d: Expecting three entries in the .short line.", Io_MvGetLine(p->pMan, (char *)Vec_PtrEntry(vTokens,0)) );
Alan Mishchenko committed
2131 2132 2133
        return 0;
    }
    // parse the regular name line
2134 2135
    assert( !strcmp((char *)Vec_PtrEntry(vTokens,0), "short") );
    pName = (char *)Vec_PtrEntryLast( vTokens );
Alan Mishchenko committed
2136 2137 2138 2139 2140 2141 2142 2143 2144
    pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName );
    if ( Abc_ObjFaninNum(pNet) > 0 )
    {
        sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Io_MvGetLine(p->pMan, pName), pName );
        return 0;
    }
    // create fanins
    pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), 1 );
    // parse the table of this node
2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 2166
    if ( p->pNtk->ntkFunc == ABC_FUNC_MAP )
    {
        Mio_Library_t * pGenlib; 
        Mio_Gate_t * pGate;
        // check that the library is available
        pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
        if ( pGenlib == NULL )
        {
            sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
            return 0;
        }
        // get the gate
        pGate = Mio_LibraryReadBuf( pGenlib );
        if ( pGate == NULL )
        {
            sprintf( p->pMan->sError, "Line %d: Cannot find buffer gate in the library.", Io_MvGetLine(p->pMan, pName) );
            return 0;
        }
        Abc_ObjSetData( pNode, pGate );
    }
    else
        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, "1 1\n" );
Alan Mishchenko committed
2167 2168 2169 2170 2171
    return 1;
}

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

Alan Mishchenko committed
2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182
  Synopsis    [Duplicate the MV variable.]

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
{
2183
    Mem_Flex_t * pFlex;
Alan Mishchenko committed
2184 2185 2186 2187
    Io_MvVar_t * pVarDup;
    int i;
    if ( pVar == NULL )
        return NULL;
2188
    pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( pNtk );
Alan Mishchenko committed
2189
    assert( pFlex != NULL );
2190
    pVarDup = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
Alan Mishchenko committed
2191 2192 2193 2194
    pVarDup->nValues = pVar->nValues;
    pVarDup->pNames = NULL;
    if ( pVar->pNames == NULL )
        return pVarDup;
2195
    pVarDup->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues );
Alan Mishchenko committed
2196 2197
    for ( i = 0; i < pVar->nValues; i++ )
    {
2198
        pVarDup->pNames[i] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 );
Alan Mishchenko committed
2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237
        strcpy( pVarDup->pNames[i], pVar->pNames[i] );
    }
    return pVarDup;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static char * Io_ReadBlifCleanName( char * pName )
{
    int i, Length;
    Length = strlen(pName);
    for ( i = 0; i < Length; i++ )
        if ( pName[i] == '=' )
            return pName + i + 1;
    return NULL;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
{
2238
    extern int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_Gate_t * pTwin );
Alan Mishchenko committed
2239 2240 2241 2242 2243 2244
    Mio_Library_t * pGenlib; 
    Mio_Gate_t * pGate;
    Abc_Obj_t * pNode;
    char ** ppNames, * pName;
    int i, nNames;

2245
    pName = (char *)vTokens->pArray[0];
Alan Mishchenko committed
2246 2247

    // check that the library is available
2248
    pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
Alan Mishchenko committed
2249 2250 2251 2252 2253 2254 2255 2256 2257 2258 2259 2260 2261 2262
    if ( pGenlib == NULL )
    {
        sprintf( p->pMan->sError, "Line %d: The current library is not available.", Io_MvGetLine(p->pMan, pName) );
        return 0;
    }

    // create a new node and add it to the network
    if ( vTokens->nSize < 2 )
    {
        sprintf( p->pMan->sError, "Line %d: The .gate line has less than two tokens.", Io_MvGetLine(p->pMan, pName) );
        return 0;
    }

    // get the gate
2263
    pGate = Mio_LibraryReadGateByName( pGenlib, (char *)vTokens->pArray[1], NULL );
Alan Mishchenko committed
2264 2265
    if ( pGate == NULL )
    {
Alan Mishchenko committed
2266
        sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
Alan Mishchenko committed
2267 2268 2269 2270 2271 2272 2273 2274
        return 0;
    }

    // if this is the first line with gate, update the network type
    if ( Abc_NtkNodeNum(p->pNtk) == 0 )
    {
        assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
        p->pNtk->ntkFunc = ABC_FUNC_MAP;
2275
        Mem_FlexStop( (Mem_Flex_t *)p->pNtk->pManFunc, 0 );
Alan Mishchenko committed
2276 2277 2278
        p->pNtk->pManFunc = pGenlib;
    }

Alan Mishchenko committed
2279
    // reorder the formal inputs to be in the same order as in the gate
2280
    if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate, Mio_GateReadTwin(pGate) ) )
Alan Mishchenko committed
2281 2282 2283 2284 2285
    {
        sprintf( p->pMan->sError, "Line %d: Mismatch in the fanins of gate \"%s\".", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
        return 0;
    }

Alan Mishchenko committed
2286 2287 2288
    // remove the formal parameter names
    for ( i = 2; i < vTokens->nSize; i++ )
    {
2289 2290
        if ( vTokens->pArray[i] == NULL )
            continue;
2291
        vTokens->pArray[i] = Io_ReadBlifCleanName( (char *)vTokens->pArray[i] );
Alan Mishchenko committed
2292 2293 2294 2295 2296 2297 2298 2299
        if ( vTokens->pArray[i] == NULL )
        {
            sprintf( p->pMan->sError, "Line %d: Invalid gate input assignment.", Io_MvGetLine(p->pMan, pName) );
            return 0;
        }
    }

    // create the node
2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322
    if ( Mio_GateReadTwin(pGate) == NULL )
    {
        nNames  = vTokens->nSize - 3;
        ppNames = (char **)vTokens->pArray + 2;
        pNode   = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
        Abc_ObjSetData( pNode, pGate );
    }
    else
    {
        nNames  = vTokens->nSize - 4;
        ppNames = (char **)vTokens->pArray + 2;
        assert( ppNames[nNames] != NULL || ppNames[nNames+1] != NULL );
        if ( ppNames[nNames] )
        {
            pNode   = Io_ReadCreateNode( p->pNtk, ppNames[nNames], ppNames, nNames );
            Abc_ObjSetData( pNode, pGate );
        }
        if ( ppNames[nNames+1] )
        {
            pNode   = Io_ReadCreateNode( p->pNtk, ppNames[nNames+1], ppNames, nNames );
            Abc_ObjSetData( pNode, Mio_GateReadTwin(pGate) );
        }
    }
Alan Mishchenko committed
2323 2324 2325 2326

    return 1;
}

2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356
/**Function*************************************************************

  Synopsis    [Box mapping procedures.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Abc_MapBoxSetPrevNext( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
{
    Abc_Obj_t * pNode;
    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
    Vec_IntWriteEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
    Vec_IntWriteEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
}
static inline int Abc_MapBox2Next( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
{
    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
    return Vec_IntEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
}
static inline int Abc_MapBox2Prev( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
{
    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
    return Vec_IntEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
}

Alan Mishchenko committed
2357 2358 2359 2360 2361
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


2362 2363
ABC_NAMESPACE_IMPL_END