diff options
Diffstat (limited to 'src/base/wlc/wlcAbc.c')
-rw-r--r-- | src/base/wlc/wlcAbc.c | 353 |
1 files changed, 237 insertions, 116 deletions
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c index 12425b0..1836f4e 100644 --- a/src/base/wlc/wlcAbc.c +++ b/src/base/wlc/wlcAbc.c @@ -18,8 +18,8 @@ ***********************************************************************/ -#include "wlc.h"
-#include "base/abc/abc.h"
+#include "wlc.h" +#include "base/abc/abc.h" ABC_NAMESPACE_IMPL_START @@ -30,120 +30,241 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
-{
- Wlc_Obj_t * pObj;
- int i, k, nNum, nRange, nBits = 0;
- Wlc_NtkForEachCi( pNtk, pObj, i )
- {
- if ( pObj->Type != WLC_OBJ_FO )
- continue;
- nRange = Wlc_ObjRange(pObj);
- for ( k = 0; k < nRange; k++ )
- {
- nNum = Vec_IntEntry(vInv, nBits + k);
- if ( nNum )
- break;
- }
- if ( k == nRange )
- {
- nBits += nRange;
- continue;
- }
- printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
- for ( k = 0; k < nRange; k++ )
- {
- nNum = Vec_IntEntry( vInv, nBits + k );
- if ( nNum == 0 )
- continue;
- printf( " [%d] -> %d", k, nNum );
- }
- printf( "\n");
- nBits += nRange;
- }
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
-{
- Wlc_Obj_t * pObj;
- int i, k, nNum, nRange, nBits = 0;
- Abc_Ntk_t * pMainNtk = NULL;
- Abc_Obj_t * pMainObj, * pMainTemp;
- char Buffer[5000];
- // start the network
- pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
- // duplicate the name and the spec
- pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
- // create primary inputs
- Wlc_NtkForEachCi( pNtk, pObj, i )
- {
- if ( pObj->Type != WLC_OBJ_FO )
- continue;
- nRange = Wlc_ObjRange(pObj);
- for ( k = 0; k < nRange; k++ )
- {
- nNum = Vec_IntEntry(vInv, nBits + k);
- if ( nNum )
- break;
- }
- if ( k == nRange )
- {
- nBits += nRange;
- continue;
- }
- //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
- for ( k = 0; k < nRange; k++ )
- {
- nNum = Vec_IntEntry( vInv, nBits + k );
- if ( nNum == 0 )
- continue;
- //printf( " [%d] -> %d", k, nNum );
- pMainObj = Abc_NtkCreatePi( pMainNtk );
- sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
- Abc_ObjAssignName( pMainObj, Buffer, NULL );
-
- }
- //printf( "\n");
- nBits += nRange;
- }
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
- // create node
- pMainObj = Abc_NtkCreateNode( pMainNtk );
- Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
- Abc_ObjAddFanin( pMainObj, pMainTemp );
- pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
- // create PO
- pMainTemp = Abc_NtkCreatePo( pMainNtk );
- Abc_ObjAddFanin( pMainTemp, pMainObj );
- Abc_ObjAssignName( pMainTemp, "inv", NULL );
- return pMainNtk;
-}
+ +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose ) +{ + Wlc_Obj_t * pObj; + int i, k, nNum, nRange, nBits = 0; + Wlc_NtkForEachCi( pNtk, pObj, i ) + { + if ( pObj->Type != WLC_OBJ_FO ) + continue; + nRange = Wlc_ObjRange(pObj); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry(vCounts, nBits + k); + if ( nNum ) + break; + } + if ( k == nRange ) + { + nBits += nRange; + continue; + } + printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry( vCounts, nBits + k ); + if ( nNum == 0 ) + continue; + printf( " [%d] -> %d", k, nNum ); + } + printf( "\n"); + nBits += nRange; + } + //printf( "%d %d\n", Vec_IntSize(vCounts), nBits ); + assert( Vec_IntSize(vCounts) == nBits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ) +{ + extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ); + extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ); + + Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); + Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts ); + + Wlc_Obj_t * pObj; + int i, k, nNum, nRange, nBits = 0; + Abc_Ntk_t * pMainNtk = NULL; + Abc_Obj_t * pMainObj, * pMainTemp; + char Buffer[5000]; + // start the network + pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); + // duplicate the name and the spec + pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv"); + // create primary inputs + if ( pNtk == NULL ) + { + int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) ); + Vec_IntForEachEntry( vCounts, Entry, i ) + { + if ( Entry == 0 ) + continue; + pMainObj = Abc_NtkCreatePi( pMainNtk ); + sprintf( Buffer, "pi%d", i ); + Abc_ObjAssignName( pMainObj, Buffer, NULL ); + } + if ( Abc_NtkPiNum(pMainNtk) != nInputs ) + { + printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" ); + Abc_NtkDelete( pMainNtk ); + return NULL; + } + } + else + { + Wlc_NtkForEachCi( pNtk, pObj, i ) + { + if ( pObj->Type != WLC_OBJ_FO ) + continue; + nRange = Wlc_ObjRange(pObj); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry(vCounts, nBits + k); + if ( nNum ) + break; + } + if ( k == nRange ) + { + nBits += nRange; + continue; + } + //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry( vCounts, nBits + k ); + if ( nNum == 0 ) + continue; + //printf( " [%d] -> %d", k, nNum ); + pMainObj = Abc_NtkCreatePi( pMainNtk ); + sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k ); + Abc_ObjAssignName( pMainObj, Buffer, NULL ); + + } + //printf( "\n"); + nBits += nRange; + } + } + //printf( "%d %d\n", Vec_IntSize(vCounts), nBits ); + assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits ); + // create node + pMainObj = Abc_NtkCreateNode( pMainNtk ); + Abc_NtkForEachPi( pMainNtk, pMainTemp, i ) + Abc_ObjAddFanin( pMainObj, pMainTemp ); + pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) ); + Vec_IntFree( vCounts ); + Vec_StrFree( vSop ); + // create PO + pMainTemp = Abc_NtkCreatePo( pMainNtk ); + Abc_ObjAddFanin( pMainTemp, pMainObj ); + Abc_ObjAssignName( pMainTemp, "inv", NULL ); + return pMainNtk; +} + +/**Function************************************************************* + + Synopsis [Translate current network into an invariant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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" ); + else if ( Abc_NtkNodeNum(pNtk) != 1 ) + printf( "The number of internal nodes is other than 1.\n" ); + else + { + 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) ); + 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); + if ( pNames ) + { + Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia); + if ( Value < 0 ) + { + if ( Counter++ == 0 ) + printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i ); + Value = i; + } + } + else + { + 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); + } + 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) ); + Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube ) + { + nLits = 0; + Abc_CubeForEachVar( pCube, Value, k ) + if ( Value != '-' ) + nLits++; + Vec_IntPush( vRes, nLits ); + Abc_CubeForEachVar( pCube, Value, k ) + if ( Value != '-' ) + Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') ); + } + Vec_IntPush( vRes, nRegs ); + Vec_IntFree( vFanins ); + } + return vRes; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |