Commands &fla_gla/&gla_fla to convert between flop-level and gate-level abstraction.

4 files changed, 263 insertions, 75 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 0d1c6ff1..e56e88aa 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -703,10 +703,6 @@ extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars,
 extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
 /*=== giaAbsVta.c ===========================================================*/
 extern void                Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
-extern Vec_Ptr_t *         Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
-extern Vec_Int_t *         Gia_VtaFramesToAbs( Vec_Vec_t * vFrames );
-extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
-extern Vec_Int_t *         Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
 extern int                 Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
@@ -942,6 +938,10 @@ extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
 extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
+extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
+extern Vec_Int_t *         Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
+extern Vec_Int_t *         Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
+extern Vec_Int_t *         Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index e762c112..e7e5e7a6 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -228,77 +228,6 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
 
 /**Function*************************************************************
 
-  Synopsis    [Converting VTA vector to GLA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
-{
-    Gia_Obj_t * pObj;
-    Vec_Int_t * vGla;
-    int nObjMask, nObjs = Gia_ManObjNum(p);
-    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
-    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
-    // get the bitmask
-    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
-    assert( nObjs <= nObjMask );
-    // go through objects
-    vGla = Vec_IntStart( nObjs );
-    Vec_IntWriteEntry( vGla, 0, 1 );
-    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
-    {
-        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
-        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
-        Vec_IntWriteEntry( vGla, (Entry &  nObjMask), 1 );
-    }
-    return vGla;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converting GLA vector to VTA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
-{
-    Vec_Int_t * vVta;
-    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
-    int i, k, j, Entry, Counter, nGlaSize;
-    //. get the GLA size
-    nGlaSize = Vec_IntSum(vGla);
-    // get the bitmask
-    nObjBits = Abc_Base2Log(nObjs);
-    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
-    assert( nObjs <= nObjMask );
-    // go through objects
-    vVta = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vVta, nFrames );
-    Counter = nFrames + 2;
-    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
-        Vec_IntPush( vVta, Counter );
-    for ( i = 0; i < nFrames; i++ )
-        for ( k = 0; k <= i; k++ )
-            Vec_IntForEachEntry( vGla, Entry, j )
-                if ( Entry ) 
-                    Vec_IntPush( vVta, (k << nObjBits) | j );
-    Counter = Vec_IntEntry(vVta, nFrames+1);
-    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
-    return vVta;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Detects how many frames are completed.]
 
   Description []
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 6f6bf0fa..1a6789b5 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1278,6 +1278,159 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Converting VTA vector to GLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vGla;
+    int nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+    // get the bitmask
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vGla = Vec_IntStart( nObjs );
+    Vec_IntWriteEntry( vGla, 0, 1 );
+    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
+    {
+        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
+        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
+        Vec_IntWriteEntry( vGla, (Entry &  nObjMask), 1 );
+    }
+    return vGla;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to VTA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
+{
+    Vec_Int_t * vVta;
+    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, k, j, Entry, Counter, nGlaSize;
+    //. get the GLA size
+    nGlaSize = Vec_IntSum(vGla);
+    // get the bitmask
+    nObjBits = Abc_Base2Log(nObjs);
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vVta = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vVta, nFrames );
+    Counter = nFrames + 2;
+    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
+        Vec_IntPush( vVta, Counter );
+    for ( i = 0; i < nFrames; i++ )
+        for ( k = 0; k <= i; k++ )
+            Vec_IntForEachEntry( vGla, Entry, j )
+                if ( Entry ) 
+                    Vec_IntPush( vVta, (k << nObjBits) | j );
+    Counter = Vec_IntEntry(vVta, nFrames+1);
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+    return vVta;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to FLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
+    if ( Gia_ObjIsRo(p, pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting FLA vector to GLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
+{
+    Vec_Int_t * vGla;
+    Gia_Obj_t * pObj;
+    int i;
+    // mark const0 and relevant CI objects
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
+    Gia_ManForEachPi( p, pObj, i )
+        Gia_ObjSetTravIdCurrent(p, pObj);
+    Gia_ManForEachRo( p, pObj, i )
+        if ( !Vec_IntEntry(vFla, i) )
+            Gia_ObjSetTravIdCurrent(p, pObj);
+    // label all objects reachable from the PO and selected flops
+    vGla = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_IntWriteEntry( vGla, 0, 1 );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    Gia_ManForEachRi( p, pObj, i )
+        if ( Vec_IntEntry(vFla, i) )
+            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    return vGla;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to FLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
+{
+    Vec_Int_t * vFla;
+    Gia_Obj_t * pObj;
+    int i;
+    vFla = Vec_IntStart( Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
+            Vec_IntWriteEntry( vFla, i, 1 );
+    return vFla;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5fdf5ace..5e74a943 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -353,6 +353,8 @@ static int Abc_CommandAbc9Gla                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Vta                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla2Vta            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Fla2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Gla2Fla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BackReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -799,6 +801,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_vta",      Abc_CommandAbc9Gla2Vta,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&fla_gla",      Abc_CommandAbc9Fla2Gla,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_fla",      Abc_CommandAbc9Gla2Fla,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&back_reach",   Abc_CommandAbc9BackReach,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
@@ -27862,6 +27866,108 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Fla2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, fVerbose = 0;
+    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_CommandAbc9Fla2Gla(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( pAbc->pGia->vFlopClasses == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no gate-level abstraction is defined.\n" );
+        return 1;
+    }
+    Vec_IntFreeP( &pAbc->pGia->vGateClasses );
+    pAbc->pGia->vGateClasses = Gia_FlaConvertToGla( pAbc->pGia, pAbc->pGia->vFlopClasses );
+    Vec_IntFreeP( &pAbc->pGia->vFlopClasses );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &fla_gla [-vh]\n" );
+    Abc_Print( -2, "\t          maps flop-level into gate-level abstraction\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");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Gla2Fla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, fVerbose = 0;
+    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_CommandAbc9Gla2Fla(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( pAbc->pGia->vGateClasses == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no gate-level abstraction is defined.\n" );
+        return 1;
+    }
+    Vec_IntFreeP( &pAbc->pGia->vFlopClasses );
+    pAbc->pGia->vFlopClasses = Gia_GlaConvertToFla( pAbc->pGia, pAbc->pGia->vGateClasses );
+    Vec_IntFreeP( &pAbc->pGia->vGateClasses );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_fla [-vh]\n" );
+    Abc_Print( -2, "\t          maps gate-level into flop-level abstraction\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");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;