New code since Dec 2010.

2 files changed, 904 insertions, 0 deletions

diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
new file mode 100644
index 00000000..4131f942
--- /dev/null
+++ b/src/aig/gia/giaSim2.c
@@ -0,0 +1,705 @@
+/**CFile****************************************************************
+
+  FileName    [giaSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Fast sequential simulator.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Gia_Sim2_t_ Gia_Sim2_t;
+struct Gia_Sim2_t_
+{
+    Gia_Man_t *    pAig;
+    Gia_ParSim_t * pPars; 
+    int            nWords;
+    unsigned *     pDataSim; 
+    Vec_Int_t *    vClassOld;
+    Vec_Int_t *    vClassNew;
+};
+
+static inline unsigned * Gia_Sim2Data( Gia_Sim2_t * p, int i )    { return p->pDataSim + i * p->nWords;    }
+
+extern void Gia_ManResetRandom( Gia_ParSim_t * pPars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_Sim2Delete( Gia_Sim2_t * p )
+{
+    Vec_IntFreeP( &p->vClassOld );
+    Vec_IntFreeP( &p->vClassNew );
+    ABC_FREE( p->pDataSim );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fast simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Sim2_t * Gia_Sim2Create( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
+{
+    Gia_Sim2_t * p;
+    Gia_Obj_t * pObj;
+    int i;
+    p = ABC_CALLOC( Gia_Sim2_t, 1 );
+    p->pAig      = pAig;
+    p->pPars     = pPars;
+    p->nWords    = pPars->nWords;
+    p->pDataSim  = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
+    if ( !p->pDataSim  )
+    { 
+        Abc_Print( 1, "Simulator could not allocate %.2f Gb for simulation info.\n", 
+            4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
+        Gia_Sim2Delete( p );
+        return NULL;
+    }
+    p->vClassOld = Vec_IntAlloc( 100 );
+    p->vClassNew = Vec_IntAlloc( 100 );
+    if ( pPars->fVerbose )
+        Abc_Print( 1, "Memory: AIG = %7.2f Mb.  SimInfo = %7.2f Mb.\n", 
+            12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
+    // prepare AIG
+    Gia_ManSetPhase( pAig );
+    Gia_ManForEachObj( pAig, pObj, i )
+        pObj->Value = i;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoRandom( Gia_Sim2_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = Gia_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoZero( Gia_Sim2_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoOne( Gia_Sim2_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = ~0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoCopy( Gia_Sim2_t * p, unsigned * pInfo, unsigned * pInfo0 )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateCo( Gia_Sim2_t * p, Gia_Obj_t * pObj )
+{
+    unsigned * pInfo  = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
+    unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
+    int w;
+    if ( Gia_ObjFaninC0(pObj) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = ~pInfo0[w];
+    else 
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateNode( Gia_Sim2_t * p, Gia_Obj_t * pObj )
+{
+    unsigned * pInfo  = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
+    unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
+    unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
+    int w;
+    if ( Gia_ObjFaninC0(pObj) )
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = p->nWords-1; w >= 0; w-- )
+                pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
+        else 
+            for ( w = p->nWords-1; w >= 0; w-- )
+                pInfo[w] = ~pInfo0[w] & pInfo1[w];
+    }
+    else 
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = p->nWords-1; w >= 0; w-- )
+                pInfo[w] = pInfo0[w] & ~pInfo1[w];
+        else 
+            for ( w = p->nWords-1; w >= 0; w-- )
+                pInfo[w] = pInfo0[w] & pInfo1[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2InfoTransfer( Gia_Sim2_t * p )
+{
+    Gia_Obj_t * pObjRo, * pObjRi;
+    unsigned * pInfo0, * pInfo1;
+    int i;
+    Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
+    {
+        pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
+        pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
+        Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_Sim2SimulateRound( Gia_Sim2_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    pObj = Gia_ManConst0(p->pAig);
+    assert( Gia_ObjValue(pObj) == 0 );
+    Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+    Gia_ManForEachPi( p->pAig, pObj, i )
+        Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+    Gia_ManForEachAnd( p->pAig, pObj, i )
+    {
+        assert( Gia_ObjValue(pObj) == i );
+        Gia_Sim2SimulateNode( p, pObj );
+    }
+    Gia_ManForEachCo( p->pAig, pObj, i )
+        Gia_Sim2SimulateCo( p, pObj );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compares simulation info of two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_Sim2CompareEqual( unsigned * p0, unsigned * p1, int nWords, int fCompl )
+{
+    int w;
+    if ( !fCompl )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != p1[w] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != ~p1[w] )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares simulation info of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_Sim2CompareZero( unsigned * p0, int nWords, int fCompl )
+{
+    int w;
+    if ( !fCompl )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != 0 )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != ~0 )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_Sim2ClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
+{
+    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
+    assert( Vec_IntSize(vClass) > 0 );
+    Vec_IntForEachEntry( vClass, Ent, i )
+    {
+        if ( i == 0 )
+        {
+            Repr = Ent;
+            Gia_ObjSetRepr( p, Ent, GIA_VOID );
+            EntPrev = Ent;
+        }
+        else
+        {
+            assert( Repr < Ent );
+            Gia_ObjSetRepr( p, Ent, Repr );
+            Gia_ObjSetNext( p, EntPrev, Ent );
+            EntPrev = Ent;
+        }
+    }
+    Gia_ObjSetNext( p, EntPrev, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_Sim2ClassRefineOne( Gia_Sim2_t * p, int i )
+{
+    Gia_Obj_t * pObj0, * pObj1;
+    unsigned * pSim0, * pSim1;
+    int Ent;
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Vec_IntPush( p->vClassOld, i );
+    pObj0 = Gia_ManObj( p->pAig, i );
+    pSim0 = Gia_Sim2Data( p, i );
+    Gia_ClassForEachObj1( p->pAig, i, Ent )
+    {
+        pObj1 = Gia_ManObj( p->pAig, Ent );
+        pSim1 = Gia_Sim2Data( p, Ent );
+        if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
+            Vec_IntPush( p->vClassOld, Ent );
+        else
+            Vec_IntPush( p->vClassNew, Ent );
+    }
+    if ( Vec_IntSize( p->vClassNew ) == 0 )
+        return 0;
+    Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
+    Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
+    if ( Vec_IntSize(p->vClassNew) > 1 )
+        return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash key of the simuation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_Sim2HashKey( unsigned * pSim, int nWords, int nTableSize )
+{
+    static int s_Primes[16] = { 
+        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
+        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+    unsigned uHash = 0;
+    int i;
+    if ( pSim[0] & 1 )
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
+    else
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= pSim[i] * s_Primes[i & 0xf];
+    return (int)(uHash % nTableSize);
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines nodes belonging to candidate constant class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
+{
+    unsigned * pSim;
+    int * pTable, nTableSize, i, k, Key;
+    if ( Vec_IntSize(vRefined) == 0 )
+        return;
+    nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    Vec_IntForEachEntry( vRefined, i, k )
+    {
+        pSim = Gia_Sim2Data( p, i );
+        Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
+        if ( pTable[Key] == 0 )
+        {
+            assert( Gia_ObjRepr(p->pAig, i) == 0 );
+            assert( Gia_ObjNext(p->pAig, i) == 0 );
+            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+        }
+        else
+        {
+            Gia_ObjSetNext( p->pAig, pTable[Key], i );
+            Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
+            if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
+                Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
+            assert( Gia_ObjRepr(p->pAig, i) > 0 );
+        }
+        pTable[Key] = i;
+    }
+/*
+    Vec_IntForEachEntry( vRefined, i, k )
+    {
+        if ( Gia_ObjIsHead( p->pAig, i ) )
+            Gia_Sim2ClassRefineOne( p, i );
+    }
+*/
+    ABC_FREE( pTable );
+}
+/**Function*************************************************************
+
+  Synopsis    [Refines equivalences after one simulation round.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_Sim2InfoRefineEquivs( Gia_Sim2_t * p )
+{
+    Vec_Int_t * vRefined;
+    Gia_Obj_t * pObj;
+    unsigned * pSim;
+    int i, Count = 0;
+    // process constant candidates
+    vRefined = Vec_IntAlloc( 100 );
+    Gia_ManForEachObj1( p->pAig, pObj, i )
+    {
+        if ( !Gia_ObjIsConst(p->pAig, i) )
+            continue;
+        pSim = Gia_Sim2Data( p, i );
+//Extra_PrintBinary( stdout, pSim, 32 * p->nWords );  printf( "\n" );
+        if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
+        {
+            Vec_IntPush( vRefined, i );
+            Count++;
+        }
+    }
+    Gia_Sim2ProcessRefined( p, vRefined );
+    Vec_IntFree( vRefined );
+    // process other classes
+    Gia_ManForEachClass( p->pAig, i )
+        Count += Gia_Sim2ClassRefineOne( p, i );
+//    if ( Count )
+//        printf( "Refined %d times.\n", Count );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns index of the first pattern that failed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_Sim2InfoIsZero( Gia_Sim2_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( pInfo[w] )
+            return 32*w + Gia_WordFindFirstBit( pInfo[w] );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns index of the PO and pattern that failed it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_Sim2CheckPos( Gia_Sim2_t * p, int * piPo, int * piPat )
+{
+    Gia_Obj_t * pObj;
+    int i, iPat;
+    Gia_ManForEachPo( p->pAig, pObj, i )
+    {
+        iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
+        if ( iPat >= 0 )
+        {
+            *piPo = i;
+            *piPat = iPat;
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat )
+{
+    Abc_Cex_t * p;
+    unsigned * pData;
+    int f, i, w, Counter;
+    p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+    p->iFrame = iFrame;
+    p->iPo = iOut;
+    // fill in the binary data
+    Counter = p->nRegs;
+    pData = ABC_ALLOC( unsigned, nWords );
+    for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+    for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
+    {
+        for ( w = nWords-1; w >= 0; w-- )
+            pData[w] = Gia_ManRandom( 0 );
+        if ( Gia_InfoHasBit( pData, iPat ) )
+            Gia_InfoSetBit( p->pData, Counter + i );
+    }
+    ABC_FREE( pData );
+    return p;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation to refine equivalence classes.]
+
+  Description [Returns 1 if counter-example is detected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
+{
+    Gia_Sim2_t * p;
+    Gia_Obj_t * pObj;
+    int i, clkTotal = clock();
+    int RetValue = 0, iOut, iPat;
+    assert( pAig->pReprs && pAig->pNexts );
+    ABC_FREE( pAig->pCexSeq );
+    p = Gia_Sim2Create( pAig, pPars );
+    Gia_ManResetRandom( pPars );
+    Gia_ManForEachRo( p->pAig, pObj, i )
+        Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
+    for ( i = 0; i < pPars->nIters; i++ )
+    {
+        Gia_Sim2SimulateRound( p );
+        if ( pPars->fVerbose )
+        {
+            Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
+            if ( pAig->pReprs && pAig->pNexts )
+                Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
+            Abc_Print( 1, "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
+        }
+        if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
+        {
+            Gia_ManResetRandom( pPars );
+            pPars->iOutFail = iOut;
+            pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
+            Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
+            if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+            {
+//                Abc_Print( 1, "\n" );
+                Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
+//                Abc_Print( 1, "\n" );
+            }
+            else
+            {
+//                Abc_Print( 1, "\n" );
+//                if ( pPars->fVerbose )
+//                Abc_Print( 1, "\nGenerated counter-example is verified correctly.         " );
+//                Abc_Print( 1, "\n" );
+            }
+            RetValue = 1;
+            break;
+        }
+        if ( pAig->pReprs && pAig->pNexts )
+            Gia_Sim2InfoRefineEquivs( p );
+        if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+        {
+            i++;
+            break;
+        }
+        if ( i < pPars->nIters - 1 )
+            Gia_Sim2InfoTransfer( p );
+    }
+    Gia_Sim2Delete( p );
+    if ( pAig->pCexSeq == NULL )
+        Abc_Print( 1, "No bug detected after simulating %d frames with %d words.  ", i, pPars->nWords );
+    Abc_PrintTime( 1, "Time", clock() - clkTotal );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
new file mode 100644
index 00000000..80bde75c
--- /dev/null
+++ b/src/aig/saig/saigTempor.c
@@ -0,0 +1,199 @@
+/**CFile****************************************************************
+
+  FileName    [saigTempor.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Temporal decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initialized timeframes for temporal decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    // start the frames package
+    Aig_ManCleanData( pAig );
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    // initiliaze the flops
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0(pFrames);
+    // for each timeframe
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi(pFrames);
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        Aig_ManForEachPo( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    // create POs for the flop inputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pFrames, pObj->pData );
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pAigNew, * pFrames;
+    Aig_Obj_t * pObj, * pReset;
+    int i;
+    if ( pAig->nConstrs > 0 )
+    {
+        printf( "The AIG manager should have no constraints.\n" );
+        return NULL;
+    }
+    // create initialized timeframes
+    pFrames = Saig_ManTemporFrames( pAig, nFrames );
+    assert( Aig_ManPoNum(pFrames) == Aig_ManRegNum(pAig) );
+
+    // start the new manager
+    Aig_ManCleanData( pAig );
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+    // map the constant node and primary inputs
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    Saig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+
+    // insert initialization logic
+    Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
+    Aig_ManForEachPi( pFrames, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    Aig_ManForEachNode( pFrames, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Aig_ManForEachPo( pFrames, pObj, i )
+        pObj->pData = Aig_ObjChild0Copy(pObj);
+
+    // create reset latch (the first one among the latches)
+    pReset = Aig_ObjCreatePi( pAigNew );
+
+    // create flop output values
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), Aig_ManPo(pFrames, i)->pData );
+    Aig_ManStop( pFrames );
+
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create primary outputs
+    Saig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+
+    // create reset latch (the first one among the latches)
+    Aig_ObjCreatePo( pAigNew, Aig_ManConst1(pAigNew) );
+    // create latch inputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+
+    // finalize
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
+    return pAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
+{ 
+    extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose );
+    int RetValue, nFramesFinished = -1;
+    assert( nFrames >= 0 ); 
+    if ( nFrames == 0 )
+    {
+        nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose );
+        if ( nFrames == 1 )
+        {
+            printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
+            return NULL;
+        }
+        Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
+    }
+    else
+        Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
+    // run BMC2
+    if ( fUseBmc )
+    {
+        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+        if ( RetValue == 0 )
+        {
+            printf( "A cex found in the first %d frames.\n", nFrames );
+            return NULL;
+        }
+        if ( nFramesFinished < nFrames )
+        {
+            printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
+            return NULL;
+        }
+    }
+    return Saig_ManTemporDecompose( pAig, nFrames );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
+