| /**CFile**************************************************************** |
| |
| FileName [wlcAbc.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Verilog parser.] |
| |
| Synopsis [Parses several flavors of word-level Verilog.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - August 22, 2014.] |
| |
| Revision [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "wlc.h" |
| #include "base/abc/abc.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
