Experiments with simulation patterns.

2 files changed, 570 insertions, 1 deletions

diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 88e94156..cb10507e 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -1222,6 +1222,348 @@ int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
 }
 
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords )
+{
+    Vec_Wrd_t * vSims = Vec_WrdAlloc( nWords ); int i;
+    for ( i = 0; i < nWords; i++ )
+        Vec_WrdPush( vSims, Gia_ManRandomW(0) );
+    return vSims;
+}
+void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn )
+{
+    int i, Id;
+    assert( Vec_WrdSize(vSims)   == nWords * Gia_ManObjNum(p) );
+    assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) );
+    Gia_ManForEachCiId( p, Id, i )
+        memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords );
+}
+static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
+{
+    word pComps[2] = { 0, ~(word)0 };
+    word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
+    word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
+    word * pSims  = Vec_WrdArray(vSims);
+    word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i);
+    word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i);
+    word * pSims2 = pSims + nWords*i; int w;
+    for ( w = 0; w < nWords; w++ )
+        pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
+}
+static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
+{
+    word pComps[2] = { 0, ~(word)0 };
+    word Diff0     = pComps[Gia_ObjFaninC0(pObj)];
+    word * pSims   = Vec_WrdArray(vSims);
+    word * pSims0  = pSims + nWords*Gia_ObjFaninId0(pObj, i);
+    word * pSims2  = pSims + nWords*i; int w;
+    for ( w = 0; w < nWords; w++ )
+        pSims2[w] = (pSims0[w] ^ Diff0);
+}
+Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
+{
+    Gia_Obj_t * pObj;
+    int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
+    Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
+    assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
+    Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi );
+    Gia_ManForEachAnd( pGia, pObj, i ) 
+        Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims );
+    Gia_ManForEachCo( pGia, pObj, i )
+        Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
+    return vSims;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/\
+Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse )
+{
+    int nWordsBase  = Vec_WrdSize(vBase)  / nInputs;
+    int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w;
+    Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) );
+    assert( Vec_WrdSize(vBase)  % nInputs == 0 );
+    assert( Vec_WrdSize(vAddOn) % nInputs == 0 );
+    assert( nWordsUse <= nWordsAddOn );
+    for ( i = 0; i < nInputs; i++ )
+    {
+        word * pSimsB = Vec_WrdEntryP( vBase,  i * nWordsBase );
+        word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn );
+        for ( w = 0; w < nWordsBase; w++ )
+            Vec_WrdPush( vSimsIn, pSimsB[w] );
+        for ( w = 0; w < nWordsUse; w++ )
+            Vec_WrdPush( vSimsIn, pSimsA[w] );
+    }
+    assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) );
+    return vSimsIn;
+}
+int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits )
+{
+    word * pSimsI, * pSimsC; int i, k;
+    for ( i = 0; i < iPat; i++ )
+    {
+        for ( k = 0; k < nLits; k++ )
+        {
+            int iVar = Abc_Lit2Var( pLits[k] );
+            pSimsI = Vec_WrdEntryP( vSimsIn,   nWords * iVar );
+            pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
+            if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) )
+                break;
+        }
+        if ( k == nLits )
+            break;
+    }
+    for ( k = 0; k < nLits; k++ )
+    {
+        int iVar = Abc_Lit2Var( pLits[k] );
+        pSimsI = Vec_WrdEntryP( vSimsIn,   nWords * iVar );
+        pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
+        if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) )
+            Abc_TtXorBit( pSimsI, i );
+        Abc_TtSetBit( pSimsC, i );
+        assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) );
+    }
+    return (int)(i == iPat);
+}
+Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes )
+{
+    int c, iCur = 0, iPat = 0;
+    int nWordsMax = Abc_Bit6WordNum( nCexes ); 
+    Vec_Wrd_t * vSimsIn   = Gia_ManSimPatGenRandom( Gia_ManCiNum(p) * nWordsMax );
+    Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax );
+    Vec_Wrd_t * vSimsRes  = NULL;
+    for ( c = 0; c < nCexes; c++ )
+    {
+        int Out  = Vec_IntEntry( vCexStore, iCur++ );
+        int Size = Vec_IntEntry( vCexStore, iCur++ );
+        iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
+        iCur += Size;
+        assert( iPat <= nCexes );
+    }
+    printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
+    assert( iCur == Vec_IntSize(vCexStore) );
+    vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) );
+    printf( "Combined %d words of the original info with %d words of additional info.\n", 
+        Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) );
+    Vec_WrdFree( vSimsIn );
+    Vec_WrdFree( vSimsCare );
+    return vSimsRes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 )
+{
+    Gia_Obj_t * pObj; 
+    int i, nUnique;
+    Vec_Mem_t * vStore;
+    vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
+    Vec_MemHashAlloc( vStore, 1 << 12 );
+    Gia_ManForEachCand( p, pObj, i )
+    {
+        word * pSim = Vec_WrdEntryP(vSims, i*nWords);
+        if ( pnC0 && Abc_TtIsConst0(pSim, nWords) )
+            (*pnC0)++;
+        if ( pnC1 && Abc_TtIsConst1(pSim, nWords) )
+            (*pnC1)++;
+        Vec_MemHashInsert( vStore, pSim );
+    }
+    nUnique = Vec_MemEntryNum( vStore );
+    Vec_MemHashFree( vStore );
+    Vec_MemFree( vStore );
+    return nUnique;
+}
+Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p);
+    pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) );
+    Gia_ManHashStart( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        word * pSim = Vec_WrdEntryP(vSims, i*nWords);
+        if ( Abc_TtIsConst0(pSim, nWords) )
+            Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) );
+        if ( Abc_TtIsConst1(pSim, nWords) )
+            Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) );
+    }
+    Gia_ManHashStop( pNew );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords )
+{
+    int k, Digit, nDigits = nWords*16;
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'A' + Digit-10 );
+    }
+    fprintf( pFile, "\n" );
+}
+void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
+{
+    int i, nNodes = Vec_WrdSize(vSimsIn) / nWords;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
+    for ( i = 0; i < nNodes; i++ )
+        Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
+    fclose( pFile );
+    printf( "Written %d words of simulation data.\n", nWords );
+}
+int Gia_ManSimPatReadOne( char c )
+{
+    int Digit = 0;
+    if ( c >= '0' && c <= '9' )
+        Digit = c - '0';
+    else if ( c >= 'A' && c <= 'F' )
+        Digit = c - 'A' + 10;
+    else if ( c >= 'a' && c <= 'f' )
+        Digit = c - 'a' + 10;
+    else assert( 0 );
+    assert( Digit >= 0 && Digit < 16 );
+    return Digit;
+}
+Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
+{
+    Vec_Wrd_t * vSimsIn = NULL; 
+    int c, nWords = -1, nChars = 0; word Num = 0;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    vSimsIn = Vec_WrdAlloc( 1000 );
+    while ( (c = fgetc(pFile)) != EOF )
+    {
+        if ( c == '\n' && nWords == -1 )
+            nWords = Vec_WrdSize(vSimsIn);
+        if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' )
+            continue;
+        Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4);
+        if ( ++nChars < 16 )
+            continue;
+        Vec_WrdPush( vSimsIn, Num );
+        nChars = 0; 
+        Num = 0;
+    }
+    assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
+    fclose( pFile );
+    printf( "Read %d words of simulation data.\n", nWords );
+    return vSimsIn;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSimProfile( Gia_Man_t * pGia )
+{
+    Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
+    int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
+    int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
+    printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", 
+        nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
+    Vec_WrdFree( vSims );
+}
+void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
+{
+    extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+    int i, Status, Counts[3] = {0};
+    Gia_Man_t * pGia;
+    Vec_Wrd_t * vSimsIn = NULL;
+    Vec_Str_t * vStatus = NULL;
+    Vec_Int_t * vCexStore = NULL;
+    Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
+    Gia_ManSimProfile( p );
+    pGia  = Gia_ManSimPatGenMiter( p, vSims );
+    vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 );
+    Gia_ManStop( pGia );
+    Vec_StrForEachEntry( vStatus, Status, i )
+    {
+        assert( Status >= -1 && Status <= 1 );
+        Counts[Status+1]++;
+    }
+    printf( "Total = %d : SAT = %d.  UNSAT = %d.  UNDEC = %d.\n", Gia_ManCoNum(p), Counts[1], Counts[2], Counts[0] );
+    if ( Counts[1] == 0 )
+        printf( "There are no counter-examples.  No need for more simulation.\n" );
+    else
+    {
+        vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] );
+        Vec_WrdFreeP( &p->vSimsPi );
+        p->vSimsPi = vSimsIn;
+        Gia_ManSimProfile( p );
+    }
+    Vec_StrFree( vStatus );
+    Vec_IntFree( vCexStore );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 48be4f55..f6fc7ea6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -411,6 +411,9 @@ static int Abc_CommandAbc9Trim               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Dfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sim                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sim3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReadSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9WriteSim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SimPat             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Resim              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SpecI              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Equiv              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1120,6 +1123,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&dfs",          Abc_CommandAbc9Dfs,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sim",          Abc_CommandAbc9Sim,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sim3",         Abc_CommandAbc9Sim3,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&read_sim",     Abc_CommandAbc9ReadSim,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&write_sim",    Abc_CommandAbc9WriteSim,     0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&simpat",       Abc_CommandAbc9SimPat,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&resim",        Abc_CommandAbc9Resim,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&speci",        Abc_CommandAbc9SpecI,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&equiv",        Abc_CommandAbc9Equiv,        0 );
@@ -22653,7 +22659,6 @@ usage:
     return 1;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -31307,6 +31312,7 @@ usage:
     return 1;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -32474,6 +32480,227 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords );
+    extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName );
+    int c, nWords = 4, fVerbose = 0;
+    char ** pArgvNew;
+    int nArgcNew;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReadSim(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReadSim(): This command works only for combinational AIGs.\n" );
+        return 0;
+    }
+    Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew == 0 )
+    {
+        Gia_ManRandom( 1 );
+        pAbc->pGia->vSimsPi = Gia_ManSimPatGenRandom( Gia_ManCiNum(pAbc->pGia) * nWords );
+        printf( "Generated %d random patterns (%d 64-bit words) for each input of the AIG.\n", 64*nWords, nWords );
+        return 0;
+    }
+    if ( nArgcNew != 1 )
+    {
+        Abc_Print( -1, "File name is not given on the command line.\n" );
+        return 1;
+    }
+    pAbc->pGia->vSimsPi = Gia_ManSimPatRead( pArgvNew[0] );
+    if ( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) != 0 )
+    {
+        Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
+        Abc_Print( -1, "File size (%d words) does not match the number of AIG inputs (%d %% %d = %d).\n", 
+            Vec_WrdSize(pAbc->pGia->vSimsPi), Vec_WrdSize(pAbc->pGia->vSimsPi), Gia_ManCiNum(pAbc->pGia), 
+            Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) );
+        return 1;
+    }
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &read_sim [-W num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t         reads simulation patterns from file\n" );
+    Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t<file> : file to store the simulation info\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords );
+    int c, fVerbose = 0;
+    char ** pArgvNew;
+    int nArgcNew;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9WriteSim(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9WriteSim(): This command works only for combinational AIGs.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vSimsPi == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9WriteSim(): Does not have simulation information available.\n" );
+        return 0;
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        Abc_Print( -1, "File name is not given on the command line.\n" );
+        return 1;
+    }
+    assert( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) == 0 );
+    Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPi, Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia) );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &write_sim [-vh] <file>\n" );
+    Abc_Print( -2, "\t         writes simulation patterns into a file\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t<file> : file to store the simulation info\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManSimPat( Gia_Man_t * pGia, int nWords, int fVerbose );
+    int c, nWords = 4, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SimPat(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SimPat(): This command works only for combinational AIGs.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vSimsPi == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9WriteSim(): Does not have simulation information available.\n" );
+        return 0;
+    }
+    Gia_ManSimPat( pAbc->pGia, nWords, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &simpat [-W num] [-vh]\n" );
+    Abc_Print( -2, "\t         performs simulation of the AIG\n" );
+    Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 /**Function*************************************************************