/**CFile****************************************************************

  FileName    [saigSynch.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Computation of synchronizing sequence.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "saig.h"

ABC_NAMESPACE_IMPL_START


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

//        0  1  x
//       00 01 11
// 0  00 00 00 00
// 1  01 00 01 11
// x  11 00 11 11

static inline unsigned Saig_SynchNot( unsigned w )
{
    return w^((~(w&(w>>1)))&0x55555555);
}
static inline unsigned Saig_SynchAnd( unsigned u, unsigned w )
{
    return (u&w)|((((u&(u>>1)&w&~(w>>1))|(w&(w>>1)&u&~(u>>1)))&0x55555555)<<1);
}
static inline unsigned Saig_SynchRandomBinary() 
{ 
    return Aig_ManRandom(0) & 0x55555555;               
}
static inline unsigned Saig_SynchRandomTernary() 
{ 
    unsigned w = Aig_ManRandom(0);
    return w^((~w)&(w>>1)&0x55555555);        
}
static inline unsigned Saig_SynchTernary( int v ) 
{
    assert( v == 0 || v == 1 || v == 3 );
    return v? ((v==1)? 0x55555555 : 0xffffffff) : 0;
}


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

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

  Synopsis    [Initializes registers to the ternary state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchSetConstant1( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int w;
    pObj = Aig_ManConst1( pAig );
    pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
    for ( w = 0; w < nWords; w++ )
        pSim[w] = 0x55555555;
}

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

  Synopsis    [Initializes registers to the ternary state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchInitRegsTernary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int i, w;
    Saig_ManForEachLo( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = 0xffffffff;
    }
}

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

  Synopsis    [Initializes registers to the given binary state.]

  Description [The binary state is stored in pObj->fMarkA.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchInitRegsBinary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int i, w;
    Saig_ManForEachLo( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = Saig_SynchTernary( pObj->fMarkA );
    }
}

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

  Synopsis    [Initializes random binary primary inputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchInitPisRandom( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int i, w;
    Saig_ManForEachPi( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = Saig_SynchRandomBinary();
    }
}

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

  Synopsis    [Initializes random binary primary inputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchInitPisGiven( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, char * pValues )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int i, w;
    Saig_ManForEachPi( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = Saig_SynchTernary( pValues[i] );
    }
}

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

  Synopsis    [Performs ternary simulation of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchTernarySimulate( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObj;
    unsigned * pSim0, * pSim1, * pSim;
    int i, w;
    // simulate nodes
    Aig_ManForEachNode( pAig, pObj, i )
    {
        pSim  = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId1(pObj) );
        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), Saig_SynchNot(pSim1[w]) );
        }
        else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = Saig_SynchAnd( pSim0[w], Saig_SynchNot(pSim1[w]) );
        }
        else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), pSim1[w] );
        }
        else // if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = Saig_SynchAnd( pSim0[w], pSim1[w] );
        }
    }
    // transfer values to register inputs
    Saig_ManForEachLi( pAig, pObj, i )
    {
        pSim  = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
        if ( Aig_ObjFaninC0(pObj) )
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = Saig_SynchNot( pSim0[w] );
        }
        else
        {
            for ( w = 0; w < nWords; w++ )
                pSim[w] = pSim0[w];
        }
    }
}

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

  Synopsis    [Performs ternary simulation of the nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_SynchTernaryTransferState( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
{
    Aig_Obj_t * pObjLi, * pObjLo;
    unsigned * pSim0, * pSim1;
    int i, w;
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
    {
        pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLi->Id );
        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLo->Id );
        for ( w = 0; w < nWords; w++ )
            pSim1[w] = pSim0[w];
    }
}

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

  Synopsis    [Returns the number of Xs in the smallest ternary pattern.]

  Description [Returns the number of this pattern.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * piPat )
{
    Aig_Obj_t * pObj;
    unsigned * pSim;
    int * pCounters, i, w, b;
    int iPatBest, iTernMin;
    // count the number of ternary values in each pattern
    pCounters = ABC_CALLOC( int, nWords * 16 );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        for ( w = 0; w < nWords; w++ )
            for ( b = 0; b < 16; b++ )
                if ( ((pSim[w] >> (b << 1)) & 3) == 3 )
                    pCounters[16 * w + b]++;
    }
    // get the best pattern
    iPatBest = -1;
    iTernMin = 1 + Saig_ManRegNum(pAig);
    for ( b = 0; b < 16 * nWords; b++ )
        if ( iTernMin > pCounters[b] )
        {
            iTernMin = pCounters[b];
            iPatBest = b;
            if ( iTernMin == 0 )
                break;
        }
    ABC_FREE( pCounters );
    *piPat = iPatBest;
    return iTernMin;
}

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

  Synopsis    [Saves the best pattern found and initializes the registers.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_SynchSavePattern( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int iPat, Vec_Str_t * vSequence )
{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    unsigned * pSim;
    int Counter, Value, i, w;
    assert( iPat < 16 * nWords );
    Saig_ManForEachPi( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
        Vec_StrPush( vSequence, (char)Value );
//        printf( "%d ", Value );
    }
//    printf( "\n" );
    Counter = 0;
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLi->Id );
        Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
        Counter += (Value == 3);
        // save patern in the same register
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLo->Id );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = Saig_SynchTernary( Value );
    }
    return Counter;
}

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

  Synopsis    [Implement synchronizing sequence.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_SynchSequenceRun( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, Vec_Str_t * vSequence, int fTernary )
{
    unsigned * pSim;
    Aig_Obj_t * pObj;
    int Counter, nIters, Value, i;
    assert( Vec_StrSize(vSequence) % Saig_ManPiNum(pAig) == 0 );
    nIters = Vec_StrSize(vSequence) / Saig_ManPiNum(pAig);
    Saig_SynchSetConstant1( pAig, vSimInfo, 1 );
    if ( fTernary )
        Saig_SynchInitRegsTernary( pAig, vSimInfo, 1 ); 
    else
        Saig_SynchInitRegsBinary( pAig, vSimInfo, 1 ); 
    for ( i = 0; i < nIters; i++ )
    {
        Saig_SynchInitPisGiven( pAig, vSimInfo, 1, Vec_StrArray(vSequence) + i * Saig_ManPiNum(pAig) );
        Saig_SynchTernarySimulate( pAig, vSimInfo, 1 );
        Saig_SynchTernaryTransferState( pAig, vSimInfo, 1 );
    }
    // save the resulting state in the registers
    Counter = 0;
    Saig_ManForEachLo( pAig, pObj, i )
    {
        pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
        Value = pSim[0] & 3;
        assert( Value != 2 );
        Counter += (Value == 3);
        pObj->fMarkA = Value;
    }
    return Counter;
}

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

  Synopsis    [Determines synchronizing sequence using ternary simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Str_t * Saig_SynchSequence( Aig_Man_t * pAig, int nWords )
{
    int nStepsMax = 100;  // the maximum number of simulation steps
    int nTriesMax = 100;  // the maximum number of attempts at each step
    int fVerify   =   1;  // verify the resulting pattern
    Vec_Str_t * vSequence;
    Vec_Ptr_t * vSimInfo;
    int nTerPrev, nTerCur = 0, nTerCur2;
    int iPatBest, RetValue, s, t;
    assert( Saig_ManRegNum(pAig) > 0 );
    // reset random numbers
    Aig_ManRandom( 1 );
    // start the sequence
    vSequence = Vec_StrAlloc( 20 * Saig_ManRegNum(pAig) );
    // create sim info and init registers
    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
    Saig_SynchSetConstant1( pAig, vSimInfo, nWords );
    // iterate over the timeframes
    nTerPrev = Saig_ManRegNum(pAig);
    Saig_SynchInitRegsTernary( pAig, vSimInfo, nWords );
    for ( s = 0; s < nStepsMax && nTerPrev > 0; s++ )
    {
        for ( t = 0; t < nTriesMax; t++ )
        {
            Saig_SynchInitPisRandom( pAig, vSimInfo, nWords );
            Saig_SynchTernarySimulate( pAig, vSimInfo, nWords );
            nTerCur = Saig_SynchCountX( pAig, vSimInfo, nWords, &iPatBest );
            if ( nTerCur < nTerPrev )
                break;
        }
        if ( t == nTriesMax )
            break;
        nTerCur2 = Saig_SynchSavePattern( pAig, vSimInfo, nWords, iPatBest, vSequence );
        assert( nTerCur == nTerCur2 );
        nTerPrev = nTerCur;
    }
    if ( nTerPrev > 0 )
    {
        printf( "Count not initialize %d registers.\n", nTerPrev );
        Vec_PtrFree( vSimInfo );
        Vec_StrFree( vSequence );
        return NULL;
    }
    // verify that the sequence is correct
    if ( fVerify )
    {
        RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
        assert( RetValue == 0 );
        Aig_ManCleanMarkA( pAig );
    }
    Vec_PtrFree( vSimInfo );
    return vSequence;
}

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

  Synopsis    [Duplicates the AIG to have constant-0 initial state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Saig_ManForEachPi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    Saig_ManForEachLo( p, pObj, i )
        pObj->pData = Aig_NotCond( Aig_ObjCreateCi( pNew ), pObj->fMarkA );
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Saig_ManForEachPo( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Saig_ManForEachLi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) );
    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
    assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) );
    return pNew;
}

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

  Synopsis    [Determines synchronizing sequence using ternary simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose )
{
    Aig_Man_t * pAigZero;
    Vec_Str_t * vSequence;
    Vec_Ptr_t * vSimInfo;
    int RetValue;
    abctime clk;

clk = Abc_Clock();
    // derive synchronization sequence
    vSequence = Saig_SynchSequence( pAig, nWords );
    if ( vSequence == NULL )
        printf( "Design 1: Synchronizing sequence is not found. " );
    else if ( fVerbose )
        printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) );
    if ( fVerbose )
    {
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    else
        printf( "\n" );
    if ( vSequence == NULL )
    {
        printf( "Quitting synchronization.\n" );
        return NULL;
    }

    // apply synchronization sequence
    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), 1 );
    RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
    assert( RetValue == 0 );
    // duplicate 
    pAigZero = Saig_ManDupInitZero( pAig );
    // cleanup
    Vec_PtrFree( vSimInfo );
    Vec_StrFree( vSequence );
    Aig_ManCleanMarkA( pAig );
    return pAigZero;
}

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

  Synopsis    [Creates SEC miter for two designs without initial state.]

  Description [The designs (pAig1 and pAig2) are assumed to have ternary 
  initial state. Determines synchronizing sequences using ternary simulation.
  Simulates the sequences on both designs to come up with equivalent binary 
  initial states. Create seq miter for the designs starting in these states.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose )
{
    Aig_Man_t * pAig1z, * pAig2z, * pMiter;
    Vec_Str_t * vSeq1, * vSeq2;
    Vec_Ptr_t * vSimInfo;
    int RetValue;
    abctime clk;
/*
    {
        unsigned u = Saig_SynchRandomTernary();
        unsigned w = Saig_SynchRandomTernary();
        unsigned x = Saig_SynchNot( u );
        unsigned y = Saig_SynchNot( w );
        unsigned z = Saig_SynchAnd( x, y );

        Extra_PrintBinary( stdout, &u, 32 );  printf( "\n" );
        Extra_PrintBinary( stdout, &w, 32 );  printf( "\n" );  printf( "\n" );
        Extra_PrintBinary( stdout, &x, 32 );  printf( "\n" );
        Extra_PrintBinary( stdout, &y, 32 );  printf( "\n" );  printf( "\n" );
        Extra_PrintBinary( stdout, &z, 32 );  printf( "\n" );
    }
*/
    // report statistics
    if ( fVerbose )
    {
        printf( "Design 1: " );
        Aig_ManPrintStats( pAig1 );
        printf( "Design 2: " );
        Aig_ManPrintStats( pAig2 );
    }

    // synchronize the first design
    clk = Abc_Clock();
    vSeq1 = Saig_SynchSequence( pAig1, nWords );
    if ( vSeq1 == NULL )
        printf( "Design 1: Synchronizing sequence is not found. " );
    else if ( fVerbose )
        printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) );
    if ( fVerbose )
    {
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    else
        printf( "\n" );

    // synchronize the first design
    clk = Abc_Clock();
    vSeq2 = Saig_SynchSequence( pAig2, nWords );
    if ( vSeq2 == NULL )
        printf( "Design 2: Synchronizing sequence is not found. " );
    else if ( fVerbose )
        printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) );
    if ( fVerbose )
    {
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    else
        printf( "\n" );

    // quit if one of the designs cannot be synchronized
    if ( vSeq1 == NULL || vSeq2 == NULL )
    {
        printf( "Quitting synchronization.\n" );
        if ( vSeq1 ) Vec_StrFree( vSeq1 );
        if ( vSeq2 ) Vec_StrFree( vSeq2 );
        return NULL;
    }
    clk = Abc_Clock();
    vSimInfo = Vec_PtrAllocSimInfo( Abc_MaxInt( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );

    // process Design 1
    RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );
    assert( RetValue == 0 );
    RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq2, 0 );
    assert( RetValue == 0 );

    // process Design 2
    RetValue = Saig_SynchSequenceRun( pAig2, vSimInfo, vSeq2, 1 );
    assert( RetValue == 0 );

    // duplicate designs
    pAig1z = Saig_ManDupInitZero( pAig1 );
    pAig2z = Saig_ManDupInitZero( pAig2 );
    pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
    Aig_ManCleanup( pMiter );
    Aig_ManStop( pAig1z );
    Aig_ManStop( pAig2z );

    // cleanup
    Vec_PtrFree( vSimInfo );
    Vec_StrFree( vSeq1 );
    Vec_StrFree( vSeq2 );
    Aig_ManCleanMarkA( pAig1 );
    Aig_ManCleanMarkA( pAig2 );

    if ( fVerbose )
    {
        printf( "Miter of the synchronized designs is constructed.         " );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    return pMiter;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END