From 32712ec9abb3f27e3bd00690838b054f5bdc0f77 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 9 Feb 2017 14:17:19 -0800 Subject: Making sure 'inv_out' can match flops by name. --- src/base/wlc/wlcAbc.c | 54 +++++++++++++++++++++++++++++++++++++++---------- src/base/wlc/wlcBlast.c | 11 +++++----- src/base/wlc/wlcCom.c | 4 ++-- 3 files changed, 51 insertions(+), 18 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c index 1f10d7b0..e19aaaec 100644 --- a/src/base/wlc/wlcAbc.c +++ b/src/base/wlc/wlcAbc.c @@ -185,8 +185,9 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs ) +Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia ) { + int nRegs = Gia_ManRegNum(pGia); Vec_Int_t * vRes = NULL; if ( Abc_NtkPoNum(pNtk) != 1 ) printf( "The number of outputs is other than 1.\n" ); @@ -194,26 +195,57 @@ Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs ) printf( "The number of internal nodes is other than 1.\n" ); else { - Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) ); + Abc_Nam_t * pNames = NULL; + Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) ); char * pName, * pCube, * pSop = (char *)pNode->pData; Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) ); - Abc_Obj_t * pFanin; int i, k, Value, nLits; + int i, k, Value, nLits, Counter = 0; + if ( pGia->vNamesIn ) + { + // hash the names + pNames = Abc_NamStart( 100, 16 ); + Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i ) + { + Value = Abc_NamStrFindOrAdd( pNames, pName, NULL ); + assert( Value == i+1 ); + //printf( "%s(%d) ", pName, i ); + } + //printf( "\n" ); + } Abc_ObjForEachFanin( pNode, pFanin, i ) { assert( Abc_ObjIsCi(pFanin) ); pName = Abc_ObjName(pFanin); - for ( k = (int)strlen(pName)-1; k >= 0; k-- ) - if ( pName[k] < '0' || pName[k] > '9' ) - break; - if ( k == (int)strlen(pName)-1 ) + if ( pNames ) + { + Value = Abc_NamStrFind(pNames, pName) - 1; + if ( Value == -1 ) + { + if ( Counter++ == 0 ) + printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i ); + Value = i; + } + } + else { - printf( "Cannot read input name of fanin %d.\n", i ); - Value = i; + for ( k = (int)strlen(pName)-1; k >= 0; k-- ) + if ( pName[k] < '0' || pName[k] > '9' ) + break; + if ( k == (int)strlen(pName)-1 ) + { + if ( Counter++ == 0 ) + printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i ); + Value = i; + } + else + Value = atoi(pName + k + 1); } - else - Value = atoi(pName + k + 1); Vec_IntPush( vFanins, Value ); } + if ( Counter ) + printf( "Cannot read names for %d inputs of the invariant.\n", Counter ); + if ( pNames ) + Abc_NamStop( pNames ); assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) ); vRes = Vec_IntAlloc( 1000 ); Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index b49c2dd7..67d7c902 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -872,6 +872,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { int fVerbose = 0; int fUseOldMultiplierBlasting = 0; + int fSkipBitRange = 0; Tim_Man_t * pManTime = NULL; Gia_Man_t * pTemp, * pNew, * pExtra = NULL; Wlc_Obj_t * pObj; @@ -1448,7 +1449,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1475,7 +1476,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1498,7 +1499,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1513,7 +1514,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) @@ -1532,7 +1533,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in { char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj)); nRange = Wlc_ObjRange( pObj ); - if ( nRange == 1 ) + if ( fSkipBitRange && nRange == 1 ) Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) ); else for ( k = 0; k < nRange; k++ ) diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 3bbe843f..cc69c636 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -1051,7 +1051,7 @@ usage: ******************************************************************************/ int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs ); + extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia ); Vec_Int_t * vInv = NULL; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c, fVerbose = 0; @@ -1080,7 +1080,7 @@ int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // derive the network - vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) ); + vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia ); if ( vInv ) Abc_FrameSetInv( vInv ); return 0; -- cgit v1.2.3