Version abc80516

1 files changed, 422 insertions, 0 deletions

diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
new file mode 100644
index 00000000..b0039276
--- /dev/null
+++ b/src/aig/saig/saigTrans.c
@@ -0,0 +1,422 @@
+/**CFile****************************************************************
+
+  FileName    [saigTrans.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Dynamic simplication of the transition relation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigTrans.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+/* 
+    A similar approach is presented in the his paper:
+    A. Kuehlmann. Dynamic transition relation simplification for 
+    bounded property checking. ICCAD'04, pp. 50-57.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Maps a node/frame into a node of a different manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Saig_ManStartMap1( Aig_Man_t * p, int nFrames )
+{
+    Vec_Int_t * vMap;
+    int i;
+    assert( p->pData == NULL );
+    vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames );
+    for ( i = 0; i < vMap->nCap; i++ )
+        vMap->pArray[i] = -1;
+    vMap->nSize = vMap->nCap;
+    p->pData = vMap;
+}
+static inline void Saig_ManStopMap1( Aig_Man_t * p )
+{
+    assert( p->pData != NULL );
+    Vec_IntFree( p->pData );
+    p->pData = NULL;
+}
+static inline int Saig_ManHasMap1( Aig_Man_t * p )
+{
+    return (int)(p->pData != NULL);
+}
+static inline void Saig_ManSetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew ) 
+{
+    Vec_Int_t * vMap = p->pData;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    assert( !Aig_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    Vec_IntWriteEntry( vMap, nOffset, pNew->Id );
+}
+static inline int Saig_ManGetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1 )
+{
+    Vec_Int_t * vMap = p->pData;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    return Vec_IntEntry( vMap, nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps a node/frame into a node/frame of a different manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Saig_ManStartMap2( Aig_Man_t * p, int nFrames )
+{
+    Vec_Int_t * vMap;
+    int i;
+    assert( p->pData2 == NULL );
+    vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames * 2 );
+    for ( i = 0; i < vMap->nCap; i++ )
+        vMap->pArray[i] = -1;
+    vMap->nSize = vMap->nCap;
+    p->pData2 = vMap;
+}
+static inline void Saig_ManStopMap2( Aig_Man_t * p )
+{
+    assert( p->pData2 != NULL );
+    Vec_IntFree( p->pData2 );
+    p->pData2 = NULL;
+}
+static inline int Saig_ManHasMap2( Aig_Man_t * p )
+{
+    return (int)(p->pData2 != NULL);
+}
+static inline void Saig_ManSetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew, int f2 ) 
+{
+    Vec_Int_t * vMap = p->pData2;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    assert( !Aig_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    Vec_IntWriteEntry( vMap, 2*nOffset + 0, pNew->Id );
+    Vec_IntWriteEntry( vMap, 2*nOffset + 1, f2 );
+}
+static inline int Saig_ManGetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, int * pf2 )
+{
+    Vec_Int_t * vMap = p->pData2;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    *pf2 = Vec_IntEntry( vMap, 2*nOffset + 1 );
+    return Vec_IntEntry( vMap, 2*nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create mapping for the first nFrames timeframes of pAig.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCreateMapping( Aig_Man_t * pAig, Aig_Man_t * pFrames, int nFrames )
+{
+    Aig_Obj_t * pObj, * pObjFrame, * pObjRepr;
+    int i, f, iNum, iFrame;
+    assert( pFrames->pReprs != NULL ); // mapping from nodes into their representatives
+    // start step mapping for both orignal manager and fraig
+    Saig_ManStartMap2( pAig, nFrames );
+    Saig_ManStartMap2( pFrames, 1 );
+    // for each object in each frame
+    for ( f = 0; f < nFrames; f++ )
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        // get the frame object
+        iNum = Saig_ManGetMap1( pAig, pObj, f );
+        pObjFrame = Aig_ManObj( pFrames, iNum );
+        // if the node has no prototype, map it into itself
+        if ( pObjFrame == NULL )
+        {
+            Saig_ManSetMap2( pAig, pObj, f, pObj, f );
+            continue;
+        }
+        // get the representative object
+        pObjRepr = Aig_ObjRepr( pFrames, pObjFrame );
+        if ( pObjRepr == NULL )
+            pObjRepr = pObjFrame;
+        // check if this is the first time this object is reached
+        if ( Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ) == -1 )
+            Saig_ManSetMap2( pFrames, pObjRepr, 0, pObj, f );
+        // set the map for the main object
+        iNum = Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame );
+        Saig_ManSetMap2( pAig, pObj, f, Aig_ManObj(pAig, iNum), iFrame );
+    }
+    Saig_ManStopMap2( pFrames );
+    assert( Saig_ManHasMap2(pAig) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unroll without initialization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesNonInitial( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start node map
+    Saig_ManStartMap1( pAig, nFrames ); 
+    // start the new manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // save the mapping
+        Aig_ManForEachObj( pAig, pObj, i )
+        {
+            assert( pObj->pData != NULL );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // quit if the last frame
+        if ( f == nFrames - 1 )
+            break;
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    // remember register outputs
+    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+        Aig_ObjCreatePo( pFrames, pObjLi->pData );
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unroll with initialization and mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pRepr;
+    int i, f, iNum1, iNum2, iFrame2;
+    assert( nFrames <= nFramesMax );
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start node map
+    Saig_ManStartMap1( pAig, nFramesMax );
+    // start the new manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFramesMax );
+    // create variables for register outputs
+    if ( fInit )
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ManConst0( pFrames );
+            Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+        }
+    }
+    else
+    {
+        // create PIs first
+        for ( f = 0; f < nFramesMax; f++ )
+            Saig_ManForEachPi( pAig, pObj, i )
+                Aig_ObjCreatePi( pFrames );
+        // create registers second
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+            Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+        }
+    }
+    // add timeframes
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        // map the constant node
+        pObj = Aig_ManConst1(pAig);
+        pObj->pData = Aig_ManConst1( pFrames );
+        Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+        {
+            if ( fInit )
+                pObj->pData = Aig_ObjCreatePi( pFrames );
+            else
+                pObj->pData = Aig_ManPi( pFrames, f * Saig_ManPiNum(pAig) + i );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+            if ( !Saig_ManHasMap2(pAig) )
+                continue;
+            if ( f < nFrames )
+            {
+                // get the mapping for this node
+                iNum2 = Saig_ManGetMap2( pAig, pObj, f, &iFrame2 );
+            }
+            else
+            {
+                // get the mapping for this node
+                iNum2 = Saig_ManGetMap2( pAig, pObj, nFrames-1, &iFrame2 );
+                iFrame2 += f - (nFrames-1);
+            }
+            assert( iNum2 != -1 );
+            assert( f >= iFrame2 );
+            // get the corresponding frames node
+            iNum1 = Saig_ManGetMap1( pAig, Aig_ManObj(pAig, iNum2), iFrame2 );
+            pRepr = Aig_ManObj( pFrames, iNum1 );
+            // compare the phases of these nodes
+            pObj->pData = Aig_NotCond( pRepr, pRepr->fPhase ^ Aig_ObjPhaseReal(pObj->pData) );
+        }
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // quit if the last frame
+        if ( f == nFramesMax - 1 )
+            break;
+        // transfer to register outputs
+        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            if ( !fInit )
+                Saig_ManSetMap1( pAig, pObjLo, f+1, Aig_Regular(pObjLo->pData) );
+        }
+    }
+    if ( !fInit )
+    {
+        // create registers
+        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+            Aig_ObjCreatePo( pFrames, pObjLi->pData );
+        // set register number
+        Aig_ManSetRegNum( pFrames, pAig->nRegs );
+    }
+    Aig_ManCleanup( pFrames );
+    Saig_ManStopMap1( pAig );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements dynamic simplification.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose )
+{
+    extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
+    Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
+    int clk, clkTotal = clock();
+    // create uninitialized timeframes with map1
+    pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
+    // perform fraiging for the unrolled timeframes
+clk = clock();
+    pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
+    // report the results
+    if ( fVerbose )
+    {
+        Aig_ManPrintStats( pFrames );
+        Aig_ManPrintStats( pFraig );
+PRT( "Fraiging", clock() - clk );
+    }
+    Aig_ManStop( pFraig );
+    assert( pFrames->pReprs != NULL );
+    // create AIG with map2
+    Saig_ManCreateMapping( pAig, pFrames, nFrames );
+    Aig_ManStop( pFrames );
+    Saig_ManStopMap1( pAig );
+    // create reduced initialized timeframes
+clk = clock();
+    pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Mapped", clock() - clk );
+    // free mapping
+    Saig_ManStopMap2( pAig );
+clk = clock();
+    pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Normal", clock() - clk );
+    // report the results
+    if ( fVerbose )
+    {
+        Aig_ManPrintStats( pRes1 );
+        Aig_ManPrintStats( pRes2 );
+    }
+    Aig_ManStop( pRes1 );
+    assert( !Saig_ManHasMap1(pAig) );
+    assert( !Saig_ManHasMap2(pAig) );
+    return pRes2;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+