From 81fae91a95b8b51d7a10d3884df92dc89eb266bf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 25 Feb 2007 08:01:00 -0800 Subject: Version abc70225 --- src/base/abc/abc.h | 20 +- src/base/abc/abcBlifMv.c | 970 ++++++++++++++++++++++++++ src/base/abc/abcCheck.c | 128 ++++ src/base/abc/abcDfs.c | 9 +- src/base/abc/abcFunc.c | 16 + src/base/abc/abcHie.c | 294 +------- src/base/abc/abcLib.c | 46 ++ src/base/abc/abcNetlist.c | 11 +- src/base/abc/abcNtk.c | 45 +- src/base/abc/abcObj.c | 9 +- src/base/abc/abcSop.c | 133 ++++ src/base/abc/abcUtil.c | 43 -- src/base/abc/module.make | 1 + src/base/abci/abc.c | 98 ++- src/base/abci/abcIf.c | 20 +- src/base/abci/abcRenode.c | 93 ++- src/base/cmd/cmd.c | 6 +- src/base/io/io.h | 3 +- src/base/io/ioReadBlifMv.c | 209 ++++-- src/base/io/ioReadVerilog.c | 35 +- src/base/io/ioUtil.c | 194 ++---- src/base/io/ioWriteAiger.c | 4 +- src/base/io/ioWriteBlif.c | 16 +- src/base/io/ioWriteBlifMv.c | 81 +-- src/base/io/ioWriteDot.c | 4 +- src/base/ver/ver.h | 2 + src/base/ver/verCore.c | 1583 +++++++++++++++++++++++++++++++++---------- src/base/ver/verCore.zip | Bin 0 -> 13275 bytes src/base/ver/verFormula.c | 4 +- 29 files changed, 3027 insertions(+), 1050 deletions(-) create mode 100644 src/base/abc/abcBlifMv.c create mode 100644 src/base/ver/verCore.zip (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index f638097f..c375a34e 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -316,6 +316,7 @@ static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Ab static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI ); } static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BO ); } static inline Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_ASSERT ); } +static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); } static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NODE ); } static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_LATCH ); } static inline Abc_Obj_t * Abc_NtkCreateWhitebox( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_WHITEBOX ); } @@ -535,6 +536,15 @@ extern void Abc_AigUpdateStop( Abc_Aig_t * pMan ); extern void Abc_AigUpdateReset( Abc_Aig_t * pMan ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); +/*=== abcBlifMv.c ==========================================================*/ +extern void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ); +extern void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ); +extern void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues ); +extern Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic ); +extern int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk ); +extern char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ); +extern int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ); /*=== abcBalance.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel ); /*=== abcCheck.c ==========================================================*/ @@ -544,6 +554,9 @@ extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb ); extern int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk ); +extern int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk ); +extern int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk ); +extern int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ); /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ); /*=== abcCut.c ==========================================================*/ @@ -616,6 +629,7 @@ extern void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk ); extern void Abc_LibPrint( Abc_Lib_t * pLib ); extern int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName ); +extern int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib ); extern Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib ); /*=== abcMiter.c ==========================================================*/ extern int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk ); @@ -682,7 +696,7 @@ extern void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); /*=== abcNetlist.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect ); +extern Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk ); /*=== abcNtbdd.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi ); @@ -783,6 +797,10 @@ extern int Abc_SopIsExorType( char * pSop ); extern bool Abc_SopCheck( char * pSop, int nFanins ); extern char * Abc_SopFromTruthBin( char * pTruth ); extern char * Abc_SopFromTruthHex( char * pTruth ); +extern char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues ); +extern char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues ); +extern char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues ); +extern char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues ); /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ); extern Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ); diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c new file mode 100644 index 00000000..48ec58c0 --- /dev/null +++ b/src/base/abc/abcBlifMv.c @@ -0,0 +1,970 @@ +/**CFile**************************************************************** + + FileName [abcBlifMv.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Procedures to process BLIF-MV networks and AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcBlifMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the Mv-Var manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ) +{ + Vec_Att_t * pAttMan; + assert( Abc_NtkMvVar(pNtk) == NULL ); + pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL ); + Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan ); +//printf( "allocing attr\n" ); +} + +/**Function************************************************************* + + Synopsis [Stops the Mv-Var manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) +{ + void * pUserMan; + pUserMan = Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); + Extra_MmFlexStop( pUserMan ); +} + +/**Function************************************************************* + + Synopsis [Duplicate the MV variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues ) +{ + Extra_MmFlex_t * pFlex; + struct temp + { + int nValues; + char ** pNames; + } * pVarStruct; + assert( nValues > 1 ); + // skip binary signals + if ( nValues == 2 ) + return; + // skip already assigned signals + if ( Abc_ObjMvVar(pObj) != NULL ) + return; + // create the structure + pFlex = Abc_NtkMvVarMan( pObj->pNtk ); + pVarStruct = (void *)Extra_MmFlexEntryFetch( pFlex, sizeof(struct temp) ); + pVarStruct->nValues = nValues; + pVarStruct->pNames = NULL; + Abc_ObjSetMvVar( pObj, pVarStruct ); +} + +/**Function************************************************************* + + Synopsis [Strashes the BLIF-MV netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_StringGetNumber( char ** ppStr ) +{ + char * pStr = *ppStr; + int Number = 0; + assert( *pStr >= '0' && *pStr <= '9' ); + for ( ; *pStr >= '0' && *pStr <= '9'; pStr++ ) + Number = 10 * Number + *pStr - '0'; + *ppStr = pStr; + return Number; +} + +/**Function************************************************************* + + Synopsis [Strashes one node in the BLIF-MV netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) +{ + char * pSop; + Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2; + Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet; + int k, v, Def, DefIndex, Index, nValues, nValuesF, nValuesF2; + + // start the output values + assert( Abc_ObjIsNode(pObj) ); + pNet = Abc_ObjFanout0(pObj); + nValues = Abc_ObjMvVarNum(pNet); + pValues = ALLOC( Abc_Obj_t *, nValues ); + for ( k = 0; k < nValues; k++ ) + pValues[k] = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); + + // get the BLIF-MV formula + pSop = pObj->pData; + // skip the value line +// while ( *pSop++ != '\n' ); + + // handle the constant + if ( Abc_ObjFaninNum(pObj) == 0 ) + { + // skip the default if present + if ( *pSop == 'd' ) + while ( *pSop++ != '\n' ); + // skip space if present + if ( *pSop == ' ' ) + pSop++; + Index = Abc_StringGetNumber( &pSop ); + assert( Index < nValues ); + pValues[Index] = Abc_AigConst1(pNtkNew); + // save the values in the fanout net + pNet->pCopy = (Abc_Obj_t *)pValues; + return 1; + } + + // parse the default line + Def = DefIndex = -1; + if ( *pSop == 'd' ) + { + pSop++; + if ( *pSop == '=' ) + { + pSop++; + DefIndex = Abc_StringGetNumber( &pSop ); + assert( DefIndex < Abc_ObjFaninNum(pObj) ); + } + else if ( *pSop == '-' ) + { + pSop++; + Def = 0; + } + else + { + Def = Abc_StringGetNumber( &pSop ); + assert( Def < nValues ); + } + assert( *pSop == '\n' ); + pSop++; + } + + // convert the values + while ( *pSop ) + { + // extract the values for each cube + pTemp = Abc_AigConst1(pNtkNew); + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + if ( *pSop == '-' ) + { + pSop += 2; + continue; + } + if ( *pSop == '!' ) + { + printf( "Abc_NodeStrashBlifMv(): Cannot handle complement in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) ); + return 0; + } + if ( *pSop == '{' ) + { + printf( "Abc_NodeStrashBlifMv(): Cannot handle braces in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) ); + return 0; + } + // get the value set + nValuesF = Abc_ObjMvVarNum(pFanin); + pValuesF = (Abc_Obj_t **)pFanin->pCopy; + if ( *pSop == '(' ) + { + pSop++; + pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); + while ( *pSop != ')' ) + { + Index = Abc_StringGetNumber( &pSop ); + assert( Index < nValuesF ); + pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, pValuesF[Index] ); + assert( *pSop == ')' || *pSop == ',' ); + if ( *pSop == ',' ) + pSop++; + } + assert( *pSop == ')' ); + pSop++; + } + else if ( *pSop == '=' ) + { + pSop++; + // get the fanin index + Index = Abc_StringGetNumber( &pSop ); + assert( Index < Abc_ObjFaninNum(pObj) ); + assert( Index != k ); + // get the fanin + pFanin2 = Abc_ObjFanin( pObj, Index ); + nValuesF2 = Abc_ObjMvVarNum(pFanin2); + pValuesF2 = (Abc_Obj_t **)pFanin2->pCopy; + // create the sum of products of values + assert( nValuesF == nValuesF2 ); + pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); + for ( v = 0; v < nValues; v++ ) + pTemp2 = Abc_AigOr( pNtkNew->pManFunc, pTemp2, Abc_AigAnd(pNtkNew->pManFunc, pValuesF[v], pValuesF2[v]) ); + } + else + { + Index = Abc_StringGetNumber( &pSop ); + assert( Index < nValuesF ); + pTemp2 = pValuesF[Index]; + } + // compute the compute + pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, pTemp2 ); + // advance the reading point + assert( *pSop == ' ' ); + pSop++; + } + // check if the output value is an equal construct + if ( *pSop == '=' ) + { + pSop++; + // get the output value + Index = Abc_StringGetNumber( &pSop ); + assert( Index < Abc_ObjFaninNum(pObj) ); + // add values of the given fanin with the given cube + pFanin = Abc_ObjFanin( pObj, Index ); + nValuesF = Abc_ObjMvVarNum(pFanin); + pValuesF = (Abc_Obj_t **)pFanin->pCopy; + assert( nValuesF == nValues ); // should be guaranteed by the parser + for ( k = 0; k < nValuesF; k++ ) + pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) ); + } + else + { + // get the output value + Index = Abc_StringGetNumber( &pSop ); + assert( Index < nValues ); + pValues[Index] = Abc_AigOr( pNtkNew->pManFunc, pValues[Index], pTemp ); + } + // advance the reading point + assert( *pSop == '\n' ); + pSop++; + } + + // compute the default value + if ( Def >= 0 || DefIndex >= 0 ) + { + pTemp = Abc_AigConst1(pNtkNew); + for ( k = 0; k < nValues; k++ ) + { + if ( k == Def ) + continue; + pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, Abc_ObjNot(pValues[k]) ); + } + + // assign the default value + if ( Def >= 0 ) + pValues[Def] = pTemp; + else + { + assert( DefIndex >= 0 ); + // add values of the given fanin with the given cube + pFanin = Abc_ObjFanin( pObj, DefIndex ); + nValuesF = Abc_ObjMvVarNum(pFanin); + pValuesF = (Abc_Obj_t **)pFanin->pCopy; + assert( nValuesF == nValues ); // should be guaranteed by the parser + for ( k = 0; k < nValuesF; k++ ) + pValues[k] = Abc_AigOr( pNtkNew->pManFunc, pValues[k], Abc_AigAnd(pNtkNew->pManFunc, pTemp, pValuesF[k]) ); + } + + } + + // save the values in the fanout net + pNet->pCopy = (Abc_Obj_t *)pValues; + return 1; +} + +/**Function************************************************************* + + Synopsis [Assigns name with index.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index ) +{ + char Suffix[16]; + assert( Abc_ObjIsTerm(pObj) ); + assert( Abc_ObjIsNet(pNet) ); + sprintf( Suffix, "[%d]", Index ); + Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix ); +} + +/**Function************************************************************* + + Synopsis [Strashes the BLIF-MV netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) +{ + int fUsePositional = 0; + Vec_Ptr_t * vNodes; + Abc_Obj_t ** pBits; + Abc_Obj_t ** pValues; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pTemp, * pBit, * pNet; + int i, k, v, nValues, nValuesMax, nBits; + + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_NtkHasBlifMv(pNtk) ); + assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); + assert( Abc_NtkBlackboxNum(pNtk) == 0 ); + + // get the largest number of values + nValuesMax = 2; + Abc_NtkForEachNet( pNtk, pObj, i ) + { + nValues = Abc_ObjMvVarNum(pObj); + if ( nValuesMax < nValues ) + nValuesMax = nValues; + } + nBits = Extra_Base2Log( nValuesMax ); + pBits = ALLOC( Abc_Obj_t *, nBits ); + + // clean the node copy fields + Abc_NtkCleanCopy( pNtk ); + // collect the nodes + vNodes = Abc_NtkDfs( pNtk, 0 ); + + // start the network + pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + // duplicate the name and the spec + pNtkNew->pName = Extra_UtilStrsav( pNtk->pName ); +// pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName ); + + // encode the CI nets + Abc_NtkIncrementTravId( pNtk ); + if ( fUsePositional ) + { + Abc_NtkForEachCi( pNtk, pObj, i ) + { + pNet = Abc_ObjFanout0(pObj); + nValues = Abc_ObjMvVarNum(pNet); + pValues = ALLOC( Abc_Obj_t *, nValues ); + // create PIs for the values + for ( v = 0; v < nValues; v++ ) + { + pValues[v] = Abc_NtkCreatePi( pNtkNew ); + Abc_NtkConvertAssignName( pValues[v], pNet, v ); + } + // save the values in the fanout net + pNet->pCopy = (Abc_Obj_t *)pValues; + // mark the net + Abc_NodeSetTravIdCurrent( pNet ); + } + } + else + { + Abc_NtkForEachCi( pNtk, pObj, i ) + { + pNet = Abc_ObjFanout0(pObj); + nValues = Abc_ObjMvVarNum(pNet); + pValues = ALLOC( Abc_Obj_t *, nValues ); + // create PIs for the encoding bits + nBits = Extra_Base2Log( nValues ); + for ( k = 0; k < nBits; k++ ) + { + pBits[k] = Abc_NtkCreatePi( pNtkNew ); + Abc_NtkConvertAssignName( pBits[k], pNet, k ); + } + // encode the values + for ( v = 0; v < nValues; v++ ) + { + pValues[v] = Abc_AigConst1(pNtkNew); + for ( k = 0; k < nBits; k++ ) + { + pBit = Abc_ObjNotCond( pBits[k], (v&(1<pManFunc, pValues[v], pBit ); + } + } + // save the values in the fanout net + pNet->pCopy = (Abc_Obj_t *)pValues; + // mark the net + Abc_NodeSetTravIdCurrent( pNet ); + } + } + + // process nodes in the topological order + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( !Abc_NodeStrashBlifMv( pNtkNew, pObj ) ) + { + Abc_NtkDelete( pNtkNew ); + return NULL; + } + Vec_PtrFree( vNodes ); + + // encode the CO nets + if ( fUsePositional ) + { + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNet = Abc_ObjFanin0(pObj); + // skip marked nets + if ( Abc_NodeIsTravIdCurrent(pNet) ) + continue; + Abc_NodeSetTravIdCurrent( pNet ); + nValues = Abc_ObjMvVarNum(pNet); + pValues = (Abc_Obj_t **)pNet->pCopy; + for ( v = 0; v < nValues; v++ ) + { + pTemp = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pTemp, pValues[v] ); + Abc_NtkConvertAssignName( pTemp, pNet, v ); + } + } + } + else + { + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNet = Abc_ObjFanin0(pObj); + // skip marked nets + if ( Abc_NodeIsTravIdCurrent(pNet) ) + continue; + Abc_NodeSetTravIdCurrent( pNet ); + nValues = Abc_ObjMvVarNum(pNet); + pValues = (Abc_Obj_t **)pNet->pCopy; + nBits = Extra_Base2Log( nValues ); + for ( k = 0; k < nBits; k++ ) + { + pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); + for ( v = 0; v < nValues; v++ ) + if ( v & (1<pManFunc, pBit, pValues[v] ); + pTemp = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pTemp, pBit ); + Abc_NtkConvertAssignName( pTemp, pNet, k ); + } + } + } + + // cleanup + free( pBits ); + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( pObj->pCopy ) + free( pObj->pCopy ); + + // remove dangling nodes + i = Abc_AigCleanup(pNtkNew->pManFunc); +// printf( "Cleanup removed %d nodes.\n", i ); +// Abc_NtkReassignIds( pNtkNew ); + + // check integrity + if ( !Abc_NtkCheck( pNtkNew ) ) + { + fprintf( stdout, "Abc_NtkStrashBlifMv(): Network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Extract the MV-skeleton of the BLIF-MV network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk ) +{ + int fUsePositional = 0; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pNet, * pNetNew, * pNodeNew, * pTermNew, * pBoxNew; + int i, k, v, nValues, nBits; + + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_NtkHasBlifMv(pNtk) ); + assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); + assert( Abc_NtkBlackboxNum(pNtk) == 0 ); + + // clean the node copy fields + Abc_NtkCleanCopy( pNtk ); + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); + // duplicate the name and the spec + pNtkNew->pName = Extra_UtilStrsav( pNtk->pName ); + pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName ); + // create the internal box (it is important to put it first!) + pBoxNew = Abc_NtkCreateWhitebox( pNtkNew ); + // create PIs and their nets + Abc_NtkForEachPi( pNtk, pObj, i ) + { + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + pNet = Abc_ObjFanout0(pObj); + Abc_NtkDupObj( pNtkNew, pNet, 1 ); + Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy ); + } + // create POs and their nets + Abc_NtkForEachPo( pNtk, pObj, i ) + { + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + pNet = Abc_ObjFanin0(pObj); + if ( pNet->pCopy == NULL ) + Abc_NtkDupObj( pNtkNew, pNet, 1 ); + Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy ); + } + // create latches + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + Abc_NtkDupBox( pNtkNew, pObj, 0 ); + // latch outputs + pNet = Abc_ObjFanout0(Abc_ObjFanout0(pObj)); + assert( pNet->pCopy == NULL ); + Abc_NtkDupObj( pNtkNew, pNet, 1 ); + Abc_ObjAddFanin( pNet->pCopy, Abc_ObjFanout0(pObj)->pCopy ); + // latch inputs + pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj)); + if ( pNet->pCopy == NULL ) + Abc_NtkDupObj( pNtkNew, pNet, 1 ); + Abc_ObjAddFanin( Abc_ObjFanin0(pObj)->pCopy, pNet->pCopy ); + } + + // encode the CI nets + Abc_NtkIncrementTravId( pNtk ); + if ( fUsePositional ) + { + Abc_NtkForEachCi( pNtk, pObj, i ) + { + pNet = Abc_ObjFanout0(pObj); + nValues = Abc_ObjMvVarNum(pNet); + for ( v = 0; v < nValues; v++ ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopEncoderPos( pNtkNew->pManFunc, v, nValues ); + pNetNew = Abc_NtkCreateNet( pNtkNew ); + pTermNew = Abc_NtkCreateBi( pNtkNew ); + Abc_ObjAddFanin( pNodeNew, pNet->pCopy ); + Abc_ObjAddFanin( pNetNew, pNodeNew ); + Abc_ObjAddFanin( pTermNew, pNetNew ); + Abc_ObjAddFanin( pBoxNew, pTermNew ); + } + // mark the net + Abc_NodeSetTravIdCurrent( pNet ); + } + } + else + { + Abc_NtkForEachCi( pNtk, pObj, i ) + { + pNet = Abc_ObjFanout0(pObj); + nValues = Abc_ObjMvVarNum(pNet); + nBits = Extra_Base2Log( nValues ); + for ( k = 0; k < nBits; k++ ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopEncoderLog( pNtkNew->pManFunc, k, nValues ); + pNetNew = Abc_NtkCreateNet( pNtkNew ); + pTermNew = Abc_NtkCreateBi( pNtkNew ); + Abc_ObjAddFanin( pNodeNew, pNet->pCopy ); + Abc_ObjAddFanin( pNetNew, pNodeNew ); + Abc_ObjAddFanin( pTermNew, pNetNew ); + Abc_ObjAddFanin( pBoxNew, pTermNew ); + } + // mark the net + Abc_NodeSetTravIdCurrent( pNet ); + } + } + + // encode the CO nets + if ( fUsePositional ) + { + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNet = Abc_ObjFanin0(pObj); + // skip marked nets + if ( Abc_NodeIsTravIdCurrent(pNet) ) + continue; + Abc_NodeSetTravIdCurrent( pNet ); + nValues = Abc_ObjMvVarNum(pNet); + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopDecoderPos( pNtkNew->pManFunc, nValues ); + for ( v = 0; v < nValues; v++ ) + { + pTermNew = Abc_NtkCreateBo( pNtkNew ); + pNetNew = Abc_NtkCreateNet( pNtkNew ); + Abc_ObjAddFanin( pTermNew, pBoxNew ); + Abc_ObjAddFanin( pNetNew, pTermNew ); + Abc_ObjAddFanin( pNodeNew, pNetNew ); + } + Abc_ObjAddFanin( pNet->pCopy, pNodeNew ); + } + } + else + { + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNet = Abc_ObjFanin0(pObj); + // skip marked nets + if ( Abc_NodeIsTravIdCurrent(pNet) ) + continue; + Abc_NodeSetTravIdCurrent( pNet ); + nValues = Abc_ObjMvVarNum(pNet); + nBits = Extra_Base2Log( nValues ); + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopDecoderLog( pNtkNew->pManFunc, nValues ); + for ( k = 0; k < nBits; k++ ) + { + pTermNew = Abc_NtkCreateBo( pNtkNew ); + pNetNew = Abc_NtkCreateNet( pNtkNew ); + Abc_ObjAddFanin( pTermNew, pBoxNew ); + Abc_ObjAddFanin( pNetNew, pTermNew ); + Abc_ObjAddFanin( pNodeNew, pNetNew ); + } + Abc_ObjAddFanin( pNet->pCopy, pNodeNew ); + } + } + + // if it is a BLIF-MV netlist transfer the values of all nets + if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) ) + { + if ( Abc_NtkMvVar( pNtkNew ) == NULL ) + Abc_NtkStartMvVars( pNtkNew ); + Abc_NtkForEachNet( pNtk, pObj, i ) + if ( pObj->pCopy ) + Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) ); + } + + // check integrity + if ( !Abc_NtkCheck( pNtkNew ) ) + { + fprintf( stdout, "Abc_NtkSkeletonBlifMv(): Network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Inserts processed network into original base MV network.] + + Description [The original network remembers the interface of combinational + logic (PIs/POs/latches names and values). The processed network may + be binary or multi-valued (currently, multi-value is not supported). + The resulting network has the same interface as the original network + while the internal logic is the same as that of the processed network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic ) +{ + Abc_Ntk_t * pNtkSkel, * pNtkNew; + Abc_Obj_t * pBox; + + assert( Abc_NtkIsNetlist(pNtkBase) ); + assert( Abc_NtkHasBlifMv(pNtkBase) ); + assert( Abc_NtkWhiteboxNum(pNtkBase) == 0 ); + assert( Abc_NtkBlackboxNum(pNtkBase) == 0 ); + + assert( Abc_NtkIsNetlist(pNtkLogic) ); + assert( Abc_NtkHasBlifMv(pNtkLogic) ); + assert( Abc_NtkWhiteboxNum(pNtkLogic) == 0 ); + assert( Abc_NtkBlackboxNum(pNtkLogic) == 0 ); + + // extract the skeleton of the old network + pNtkSkel = Abc_NtkSkeletonBlifMv( pNtkBase ); + + // set the implementation of the box to be the same as the processed network + assert( Abc_NtkWhiteboxNum(pNtkSkel) == 1 ); + pBox = Abc_NtkBox( pNtkSkel, 0 ); + assert( Abc_ObjIsWhitebox(pBox) ); + assert( pBox->pData == NULL ); + assert( Abc_ObjFaninNum(pBox) == Abc_NtkPiNum(pNtkLogic) ); + assert( Abc_ObjFanoutNum(pBox) == Abc_NtkPoNum(pNtkLogic) ); + pBox->pData = pNtkLogic; + + // flatten the hierarchy to insert the processed network + pNtkNew = Abc_NtkFlattenLogicHierarchy( pNtkSkel ); + pBox->pData = NULL; + Abc_NtkDelete( pNtkSkel ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts SOP netlist into BLIF-MV netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk ) +{ + Extra_MmFlex_t * pMmFlex; + Abc_Obj_t * pNode; + Vec_Str_t * vCube; + char * pSop0, * pSop1, * pBlifMv, * pCube, * pCur; + int Value, nCubes, nSize, i, k; + + assert( Abc_NtkIsNetlist(pNtk) ); + if ( !Abc_NtkToBdd(pNtk) ) + { + printf( "Converting logic functions to BDDs has failed.\n" ); + return 0; + } + + pMmFlex = Extra_MmFlexStart(); + vCube = Vec_StrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + // convert BDD into cubes for on-set and off-set + Abc_NodeBddToCnf( pNode, pMmFlex, vCube, 0, &pSop0, &pSop1 ); + // allocate room for the MV-SOP + nCubes = Abc_SopGetCubeNum(pSop0) + Abc_SopGetCubeNum(pSop1); + nSize = nCubes*(2*Abc_ObjFaninNum(pNode) + 2)+1; + pBlifMv = Extra_MmFlexEntryFetch( pMmFlex, nSize ); + // add the cubes + pCur = pBlifMv; + Abc_SopForEachCube( pSop0, Abc_ObjFaninNum(pNode), pCube ) + { + Abc_CubeForEachVar( pCube, Value, k ) + { + *pCur++ = Value; + *pCur++ = ' '; + } + *pCur++ = '0'; + *pCur++ = '\n'; + } + Abc_SopForEachCube( pSop1, Abc_ObjFaninNum(pNode), pCube ) + { + Abc_CubeForEachVar( pCube, Value, k ) + { + *pCur++ = Value; + *pCur++ = ' '; + } + *pCur++ = '1'; + *pCur++ = '\n'; + } + *pCur++ = 0; + assert( pCur - pBlifMv == nSize ); + // update the node representation + Cudd_RecursiveDeref( pNtk->pManFunc, pNode->pData ); + pNode->pData = pBlifMv; + } + + // update the functionality type + pNtk->ntkFunc = ABC_FUNC_BLIFMV; + Cudd_Quit( pNtk->pManFunc ); + pNtk->pManFunc = pMmFlex; + + Vec_StrFree( vCube ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Converts SOP into MV-SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ) +{ + char * pMvSop, * pCur; + unsigned uCube; + int nCubes, nSize, Value, i, k; + // consider the case of the constant node + if ( Vec_IntSize(vSop0) == 0 || Vec_IntSize(vSop1) == 0 ) + { + // (temporary) create a tautology cube + pMvSop = ALLOC( char, nVars + 3 ); + for ( k = 0; k < nVars; k++ ) + pMvSop[k] = '-'; + pMvSop[nVars] = '0' + (int)(Vec_IntSize(vSop1) > 0); + pMvSop[nVars+1] = '\n'; + pMvSop[nVars+2] = 0; + return pMvSop; + } + // find the total number of cubes + nCubes = Vec_IntSize(vSop0) + Vec_IntSize(vSop1); + // find the size of the MVSOP represented as a C-string + // (each cube has nVars variables + one output literal + end-of-line, + // and the string is zero-terminated) + nSize = nCubes * (nVars + 2) + 1; + // allocate memory + pMvSop = pCur = ALLOC( char, nSize ); + // fill in the negative polarity cubes + Vec_IntForEachEntry( vSop0, uCube, i ) + { + for ( k = 0; k < nVars; k++ ) + { + Value = (uCube >> (2*k)) & 3; + if ( Value == 1 ) + *pCur++ = '0'; + else if ( Value == 2 ) + *pCur++ = '1'; + else if ( Value == 0 ) + *pCur++ = '-'; + else + assert( 0 ); + } + *pCur++ = '0'; + *pCur++ = '\n'; + } + // fill in the positive polarity cubes + Vec_IntForEachEntry( vSop1, uCube, i ) + { + for ( k = 0; k < nVars; k++ ) + { + Value = (uCube >> (2*k)) & 3; + if ( Value == 1 ) + *pCur++ = '0'; + else if ( Value == 2 ) + *pCur++ = '1'; + else if ( Value == 0 ) + *pCur++ = '-'; + else + assert( 0 ); + } + *pCur++ = '1'; + *pCur++ = '\n'; + } + *pCur++ = 0; + assert( pCur - pMvSop == nSize ); + return pMvSop; +} + + +/**Function************************************************************* + + Synopsis [A prototype of internal cost evaluation procedure.] + + Description [This procedure takes the number of variables (nVars), + the array of values of the inputs and the output (pVarValues) + (note that this array has nVars+1 entries), and an MV-SOP represented + as a C-string with one charater for each literal, including inputs + and output. Each cube is terminated with the new-line character ('\n'). + The string is zero-terminated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeEvalMvCostInternal( int nVars, int * pVarValues, char * pMvSop ) +{ + // for now, return the number of cubes in the MV-SOP + int Counter = 0; + while ( *pMvSop ) Counter += (*pMvSop++ == '\n'); + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the cost of the cut.] + + Description [The Boolean function of the cut is specified by two SOPs, + which represent the negative/positive polarities of the cut function. + Converts these two SOPs into a mutually-agreed-upon representation + to be passed to the internal cost-evaluation procedure (see the above + prototype Abc_NodeEvalMvCostInternal).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 ) +{ + char * pMvSop; + int * pVarValues; + int i, RetValue; + // collect the input and output values (currently, they are binary) + pVarValues = ALLOC( int, nVars + 1 ); + for ( i = 0; i <= nVars; i++ ) + pVarValues[i] = 2; + // prepare MV-SOP for evaluation + pMvSop = Abc_NodeConvertSopToMvSop( nVars, vSop0, vSop1 ); + // have a look at the MV-SOP: +// printf( "%s\n", pMvSop ); + // get the result of internal cost evaluation + RetValue = Abc_NodeEvalMvCostInternal( nVars, pVarValues, pMvSop ); + // cleanup + free( pVarValues ); + free( pMvSop ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index e159bcab..24f10475 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -277,6 +277,19 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk ) } } Vec_IntFree( vNameIds ); + + // make sure the CI names are unique + if ( !Abc_NtkCheckUniqueCiNames(pNtk) ) + return 0; + + // make sure the CO names are unique + if ( !Abc_NtkCheckUniqueCoNames(pNtk) ) + return 0; + + // make sure that if a CO has the same name as a CI, they point directly + if ( !Abc_NtkCheckUniqueCioNames(pNtk) ) + return 0; + return 1; } @@ -804,6 +817,121 @@ int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk ) return RetValue; } +/**Function************************************************************* + + Synopsis [Returns 0 if CI names are repeated.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkNamesCompare( char ** pName1, char ** pName2 ) +{ + return strcmp( *pName1, *pName2 ); +} + +/**Function************************************************************* + + Synopsis [Returns 0 if CI names are repeated.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNames; + Abc_Obj_t * pObj; + int i, fRetValue = 1; + assert( !Abc_NtkIsNetlist(pNtk) ); + vNames = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + Vec_PtrPush( vNames, Abc_ObjName(pObj) ); + Vec_PtrSort( vNames, Abc_NtkNamesCompare ); + for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ ) + if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) ) + { + printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ); + fRetValue = 0; + } + Vec_PtrFree( vNames ); + return fRetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 0 if CO names are repeated.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNames; + Abc_Obj_t * pObj; + int i, fRetValue = 1; + assert( !Abc_NtkIsNetlist(pNtk) ); + vNames = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Vec_PtrPush( vNames, Abc_ObjName(pObj) ); + Vec_PtrSort( vNames, Abc_NtkNamesCompare ); + for ( i = 1; i < Abc_NtkCoNum(pNtk); i++ ) + { +// printf( "%s\n", Vec_PtrEntry(vNames,i) ); + if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) ) + { + printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ); + fRetValue = 0; + } + } + Vec_PtrFree( vNames ); + return fRetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 0 if there is a pair of CI/CO with the same name and logic in between.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj, * pObjCi; + int i, nCiId, fRetValue = 1; + assert( !Abc_NtkIsNetlist(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI ); + if ( nCiId == -1 ) + nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_BO ); + if ( nCiId == -1 ) + continue; + pObjCi = Abc_NtkObj( pNtk, nCiId ); + assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) ); + if ( Abc_ObjFanin0(pObj) != pObjCi ) + { + printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) ); + fRetValue = 0; + } + } + return fRetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index da4617ca..3dd9a132 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -884,7 +884,8 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode ) if ( pNode->Level < (unsigned)Level ) pNode->Level = Level; } - pNode->Level++; + if ( Abc_ObjFaninNum(pNode) > 0 ) + pNode->Level++; return pNode->Level; } @@ -975,8 +976,8 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ) if ( Abc_NodeIsTravIdCurrent(pNode) ) { fprintf( stdout, "Network \"%s\" contains combinational loop!\n", Abc_NtkName(pNtk) ); - fprintf( stdout, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(pNode) ); - fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(pNode) : Abc_NtkName(pNode->pData) ); + fprintf( stdout, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(Abc_ObjFanout0(pNode)) : Abc_NtkName(pNode->pData) ); return 0; } // mark this node as a node on the current path @@ -1041,7 +1042,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ) if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) ) continue; // stop as soon as the first loop is detected - fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) ); + fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(Abc_ObjFanout0(pNode)) ); break; } return fAcyclic; diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 0947b58a..7a271338 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -878,6 +878,22 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ) return 1; } +/**Function************************************************************* + + Synopsis [Converts SOP functions into BLIF-MV functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk ) +{ + return 1; +} + /**Function************************************************************* Synopsis [Convers logic network to the SOP form.] diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c index b38afb59..9e9d921b 100644 --- a/src/base/abc/abcHie.c +++ b/src/base/abc/abcHie.c @@ -146,6 +146,15 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in // call recursively Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter ); } + + // if it is a BLIF-MV netlist transfer the values of all nets + if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) ) + { + if ( Abc_NtkMvVar( pNtkNew ) == NULL ) + Abc_NtkStartMvVars( pNtkNew ); + Abc_NtkForEachNet( pNtk, pObj, i ) + Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) ); + } } /**Function************************************************************* @@ -198,12 +207,15 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", Counter, Abc_NtkBlackboxNum(pNtkNew) ); - // pass the design - assert( Vec_PtrEntry(pNtk->pDesign->vModules, 0) == pNtk ); - pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew ); - // update the pointers - Abc_NtkForEachBlackbox( pNtkNew, pTerm, i ) - pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy; + if ( pNtk->pDesign ) + { + // pass on the design + assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk ); + pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew ); + // update the pointers + Abc_NtkForEachBlackbox( pNtkNew, pTerm, i ) + pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy; + } // copy the timing information // Abc_ManTimeDup( pNtk, pNtkNew ); @@ -473,276 +485,6 @@ Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL ) return pNtkNew; } -/**Function************************************************************* - - Synopsis [Assigns name with index.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index ) -{ - char Suffix[16]; - assert( Abc_ObjIsTerm(pObj) ); - assert( Abc_ObjIsNet(pNet) ); - sprintf( Suffix, "[%d]", Index ); - Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix ); -} - -/**Function************************************************************* - - Synopsis [Strashes the BLIF-MV netlist.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkConvertBlifMv( Abc_Ntk_t * pNtk ) -{ - char * pSop; - Vec_Ptr_t * vNodes; - Abc_Obj_t * pBits[16]; - Abc_Obj_t ** pValues, ** pValuesF; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pTemp, * pBit, * pFanin, * pNet; - int fUsePositional = 0; - int i, k, v, nValues, Val, Index, Len, nBits, Def; - - assert( Abc_NtkIsNetlist(pNtk) ); - assert( Abc_NtkHasBlifMv(pNtk) ); - - // clean the node copy fields - Abc_NtkCleanCopy( pNtk ); - - // start the network - pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - // duplicate the name and the spec - pNtkNew->pName = Extra_UtilStrsav( pNtk->pName ); -// pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName ); - - // check temporary assumptions - Abc_NtkForEachNet( pNtk, pObj, i ) - assert( Abc_ObjMvVarNum(pObj) < 10 ); - - // encode the CI nets - if ( fUsePositional ) - { - Abc_NtkForEachCi( pNtk, pObj, i ) - { - pNet = Abc_ObjFanout0(pObj); - nValues = Abc_ObjMvVarNum(pNet); - pValues = ALLOC( Abc_Obj_t *, nValues ); - // create PIs for the values - for ( v = 0; v < nValues; v++ ) - { - pValues[v] = Abc_NtkCreatePi( pNtkNew ); - Abc_NtkConvertAssignName( pValues[v], pNet, v ); - } - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - } - } - else - { - Abc_NtkForEachCi( pNtk, pObj, i ) - { - pNet = Abc_ObjFanout0(pObj); - nValues = Abc_ObjMvVarNum(pNet); - pValues = ALLOC( Abc_Obj_t *, nValues ); - // create PIs for the encoding bits - nBits = Extra_Base2Log( nValues ); - for ( k = 0; k < nBits; k++ ) - { - pBits[k] = Abc_NtkCreatePi( pNtkNew ); - Abc_NtkConvertAssignName( pBits[k], pNet, k ); - } - // encode the values - for ( v = 0; v < nValues; v++ ) - { - pValues[v] = Abc_AigConst1(pNtkNew); - for ( k = 0; k < nBits; k++ ) - { - pBit = Abc_ObjNotCond( pBits[k], (v&(1<pManFunc, pValues[v], pBit ); - } - } - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - } - } - - // process nodes in the topological order - vNodes = Abc_NtkDfs( pNtk, 0 ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - { - assert( Abc_ObjIsNode(pObj) ); - pNet = Abc_ObjFanout0(pObj); - nValues = Abc_ObjMvVarNum(pNet); - pValues = ALLOC( Abc_Obj_t *, nValues ); - for ( v = 0; v < nValues; v++ ) - pValues[v] = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - // get the BLIF-MV formula - pSop = pObj->pData; - // skip the value line - while ( *pSop++ != '\n' ); - - // handle the constant - if ( Abc_ObjFaninNum(pObj) == 0 ) - { - Index = *pSop-'0'; - pValues[Index] = Abc_AigConst1(pNtkNew); - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - continue; - } -/* - // handle the mux - if ( *pSop != 'd' ) - { - assert( Abc_ObjFaninNum(pObj) == 3 ); - pValuesF = (Abc_Obj_t **)Abc_ObjFanin(pObj,1)->pCopy; - for ( v = 0; v < nValues; v++ ) - pValues[v] = pValuesF[v]; - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - continue; - } -*/ - // detect muxes - Len = strlen(pSop); - for ( k = 0; k < Len; k++ ) - if ( *(pSop+k) == '=' ) - break; - if ( k < Len ) - { - assert( Abc_ObjFaninNum(pObj) == 3 ); - pValuesF = (Abc_Obj_t **)Abc_ObjFanin(pObj,1)->pCopy; - for ( v = 0; v < nValues; v++ ) - pValues[v] = pValuesF[v]; - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - continue; - } - - // skip the default line -// assert( *pSop == 'd' ); - if ( *pSop == 'd' ) - { - Def = *(pSop+1) - '0'; - while ( *pSop++ != '\n' ); - } - else - Def = -1; - // convert the values - while ( *pSop ) - { - // encode the values - pTemp = Abc_AigConst1(pNtkNew); - Abc_ObjForEachFanin( pObj, pFanin, k ) - { - if ( *pSop == '-' ) - { - pSop += 2; - continue; - } - Val = Abc_ObjMvVarNum(pFanin); - pValuesF = (Abc_Obj_t **)pFanin->pCopy; - Index = *pSop-'0'; - assert( Index >= 0 && Index <= 9 && Index < Val ); - pTemp = Abc_AigAnd( pNtkNew->pManFunc, pTemp, pValuesF[Index] ); - pSop += 2; - } - // get the output value - Index = *pSop-'0'; - assert( Index >= 0 && Index <= 9 ); - pValues[Index] = Abc_AigOr( pNtkNew->pManFunc, pValues[Index], pTemp ); - pSop++; - assert( *pSop == '\n' ); - pSop++; - } - // compute the default value -// Def = 0; - if ( Def >= 0 ) - { - assert( pValues[Def] == Abc_ObjNot( Abc_AigConst1(pNtkNew) ) ); - pValues[Def] = Abc_AigConst1(pNtkNew); - for ( v = 0; v < nValues; v++ ) - { - if ( v == Def ) - continue; - pValues[Def] = Abc_AigAnd( pNtkNew->pManFunc, pValues[Def], Abc_ObjNot(pValues[v]) ); - } - // experiment - // if ( nValues > 2 ) - // pValues[Def] = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - } - - // save the values in the fanout net - pNet->pCopy = (Abc_Obj_t *)pValues; - } - Vec_PtrFree( vNodes ); - - // encode the CO nets - if ( fUsePositional ) - { - Abc_NtkForEachCo( pNtk, pObj, i ) - { - pNet = Abc_ObjFanin0(pObj); - nValues = Abc_ObjMvVarNum(pNet); - pValues = (Abc_Obj_t **)pNet->pCopy; - for ( v = 0; v < nValues; v++ ) - { - pTemp = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pTemp, pValues[v] ); - Abc_NtkConvertAssignName( pTemp, pNet, v ); - } - } - } - else - { - Abc_NtkForEachCo( pNtk, pObj, i ) - { - pNet = Abc_ObjFanin0(pObj); - nValues = Abc_ObjMvVarNum(pNet); - pValues = (Abc_Obj_t **)pNet->pCopy; - nBits = Extra_Base2Log( nValues ); - for ( k = 0; k < nBits; k++ ) - { - pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - for ( v = 0; v < nValues; v++ ) - if ( v & (1<pManFunc, pBit, pValues[v] ); - pTemp = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pTemp, pBit ); - Abc_NtkConvertAssignName( pTemp, pNet, k ); - } - } - } - - // cleanup - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( pObj->pCopy ) - free( pObj->pCopy ); - - Abc_AigCleanup(pNtkNew->pManFunc); - - // check integrity - if ( !Abc_NtkCheck( pNtkNew ) ) - { - fprintf( stdout, "Abc_NtkConvertBlifMv(): Network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c index 1f741ca8..d9d8bce9 100644 --- a/src/base/abc/abcLib.c +++ b/src/base/abc/abcLib.c @@ -108,8 +108,11 @@ Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave ) Abc_Lib_t * pLibNew; Abc_Ntk_t * pNtkTemp; int i; + assert( Vec_PtrSize(pLib->vTops) > 0 ); + assert( Vec_PtrSize(pLib->vModules) > 1 ); pLibNew = Abc_LibCreate( pLib->pName ); // pLibNew->pManFunc = pNtkSave->pManFunc; + Vec_PtrPush( pLibNew->vTops, pNtkSave ); Vec_PtrPush( pLibNew->vModules, pNtkSave ); Vec_PtrForEachEntry( pLib->vModules, pNtkTemp, i ) if ( Abc_NtkHasBlackbox( pNtkTemp ) ) @@ -215,7 +218,50 @@ Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib ) return pNtk; } +/**Function************************************************************* + + Synopsis [Detects the top-level models.] + + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib ) +{ + Abc_Ntk_t * pNtk, * pNtkBox; + Abc_Obj_t * pObj; + int i, k; + assert( Vec_PtrSize( pLib->vModules ) > 0 ); + // clear the models + Vec_PtrForEachEntry( pLib->vModules, pNtk, i ) + pNtk->fHieVisited = 0; + // mark all the models reachable from other models + Vec_PtrForEachEntry( pLib->vModules, pNtk, i ) + { + Abc_NtkForEachBox( pNtk, pObj, k ) + { + if ( Abc_ObjIsLatch(pObj) ) + continue; + if ( pObj->pData == NULL ) + continue; + pNtkBox = pObj->pData; + pNtkBox->fHieVisited = 1; + } + } + // collect the models that are not marked + Vec_PtrClear( pLib->vTops ); + Vec_PtrForEachEntry( pLib->vModules, pNtk, i ) + { + if ( pNtk->fHieVisited == 0 ) + Vec_PtrPush( pLib->vTops, pNtk ); + else + pNtk->fHieVisited = 0; + } + return Vec_PtrSize( pLib->vTops ); +} /**Function************************************************************* diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index f57bcc21..26b88c68 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk ) return Abc_NtkAigToLogicSop( pNtk ); assert( Abc_NtkIsNetlist(pNtk) ); // consider simple case when there is hierarchy - assert( pNtk->pDesign == NULL ); +// assert( pNtk->pDesign == NULL ); assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); assert( Abc_NtkBlackboxNum(pNtk) == 0 ); // start the network @@ -90,7 +90,7 @@ Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk, int fDirect ) +Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew, * pNtkTemp; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); @@ -151,6 +151,11 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) // remove dangling nodes Abc_NtkCleanup( pNtk, 0 ); + // make sure the CO names are unique + Abc_NtkCheckUniqueCiNames( pNtk ); + Abc_NtkCheckUniqueCoNames( pNtk ); + Abc_NtkCheckUniqueCioNames( pNtk ); + // assert( Abc_NtkLogicHasSimpleCos(pNtk) ); if ( !Abc_NtkLogicHasSimpleCos(pNtk) ) { @@ -213,7 +218,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc, 0 ); + pNtkNew->pExdc = Abc_NtkToNetlist( pNtk->pExdc ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkLogicToNetlist(): Network check has failed.\n" ); return pNtkNew; diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index deddb712..e0773e3f 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -264,18 +264,23 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) assert( Abc_NtkIsNetlist(pNtk) ); // check if constant 0 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else if ( Abc_ObjFaninNum(pNet) == 0 ) - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) ); + pNet = Abc_NtkFindNet( pNtk, "1\'b0" ); + if ( pNet ) + { + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else if ( Abc_ObjFaninNum(pNet) == 0 ) + Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) ); + } // check if constant 1 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else if ( Abc_ObjFaninNum(pNet) == 0 ) - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) ); - + pNet = Abc_NtkFindNet( pNtk, "1\'b1" ); + if ( pNet ) + { + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else if ( Abc_ObjFaninNum(pNet) == 0 ) + Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) ); + } // fix the net drivers Abc_NtkFixNonDrivenNets( pNtk ); @@ -872,7 +877,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // free node attributes Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i ) if ( pAttrMan ) + { +//printf( "deleting attr\n" ); Vec_AttFree( pAttrMan, 1 ); + } Vec_PtrFree( pNtk->vAttrs ); FREE( pNtk->pName ); FREE( pNtk->pSpec ); @@ -892,16 +900,12 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) { - char Buffer[10]; Vec_Ptr_t * vNets; Abc_Obj_t * pNet, * pNode; int i; if ( Abc_NtkNodeNum(pNtk) == 0 ) - { -// pNtk->ntkFunc = ABC_FUNC_BLACKBOX; return; - } // check for non-driven nets vNets = Vec_PtrAlloc( 100 ); @@ -910,14 +914,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) if ( Abc_ObjFaninNum(pNet) > 0 ) continue; // add the constant 0 driver - if ( Abc_NtkHasBlifMv(pNtk) ) - { - pNode = Abc_NtkCreateNode( pNtk ); - sprintf( Buffer, "%d\n0\n", Abc_ObjMvVarNum(pNet) ); - pNode->pData = Abc_SopRegister( pNtk->pManFunc, Buffer ); - } - else - pNode = Abc_NtkCreateNodeConst0( pNtk ); + pNode = Abc_NtkCreateNodeConst0( pNtk ); // add the fanout net Abc_ObjAddFanin( pNet, pNode ); // add the net to those for which the warning will be printed @@ -927,7 +924,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) // print the warning if ( vNets->nSize > 0 ) { - printf( "Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pNtk->pName ); + printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pNtk->pName ); Vec_PtrForEachEntry( vNets, pNet, i ) { printf( "%s%s", (i? ", ": ""), Abc_ObjName(pNet) ); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 4931f238..0425d984 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -349,7 +349,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName { if ( Abc_NtkIsStrash(pNtkNew) ) {} - else if ( Abc_NtkHasSop(pNtkNew) ) + else if ( Abc_NtkHasSop(pNtkNew) || Abc_NtkHasBlifMv(pNtkNew) ) pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData ); else if ( Abc_NtkHasBdd(pNtkNew) ) pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData); @@ -558,8 +558,9 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ) assert( Abc_NtkIsNetlist(pNtk) ); if ( pName && (pNet = Abc_NtkFindNet( pNtk, pName )) ) return pNet; +//printf( "Creating net %s.\n", pName ); // create a new net - pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + pNet = Abc_NtkCreateNet( pNtk ); if ( pName ) Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pNet->Type, pName, NULL ); return pNet; @@ -581,7 +582,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNode; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) ); pNode = Abc_NtkCreateNode( pNtk ); - if ( Abc_NtkHasSop(pNtk) ) + if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) ) pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 0\n" ); else if ( Abc_NtkHasBdd(pNtk) ) pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData ); @@ -610,7 +611,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNode; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) ); pNode = Abc_NtkCreateNode( pNtk ); - if ( Abc_NtkHasSop(pNtk) ) + if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) ) pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" ); else if ( Abc_NtkHasBdd(pNtk) ) pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData ); diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index 0836bb89..a39bd7bf 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -933,6 +933,139 @@ char * Abc_SopFromTruthHex( char * pTruth ) return pSopCover; } +/**Function************************************************************* + + Synopsis [Creates one encoder node.] + + Description [Produces MV-SOP for BLIF-MV representation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues ) +{ + char Buffer[32]; + assert( iValue < nValues ); + sprintf( Buffer, "d0\n%d 1\n", iValue ); + return Abc_SopRegister( pMan, Buffer ); +} + +/**Function************************************************************* + + Synopsis [Creates one encoder node.] + + Description [Produces MV-SOP for BLIF-MV representation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues ) +{ + char * pResult; + Vec_Str_t * vSop; + int v, Counter, fFirst = 1, nBits = Extra_Base2Log(nValues); + assert( iBit < nBits ); + // count the number of literals + Counter = 0; + for ( v = 0; v < nValues; v++ ) + Counter += ( (v & (1 << iBit)) > 0 ); + // create the cover + vSop = Vec_StrAlloc( 100 ); + Vec_StrPrintStr( vSop, "d0\n" ); + if ( Counter > 1 ) + Vec_StrPrintStr( vSop, "(" ); + for ( v = 0; v < nValues; v++ ) + if ( v & (1 << iBit) ) + { + if ( fFirst ) + fFirst = 0; + else + Vec_StrPush( vSop, ',' ); + Vec_StrPrintNum( vSop, v ); + } + if ( Counter > 1 ) + Vec_StrPrintStr( vSop, ")" ); + Vec_StrPrintStr( vSop, " 1\n" ); + Vec_StrPush( vSop, 0 ); + pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) ); + Vec_StrFree( vSop ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the decoder node.] + + Description [Produces MV-SOP for BLIF-MV representation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues ) +{ + char * pResult; + Vec_Str_t * vSop; + int i, k; + assert( nValues > 1 ); + vSop = Vec_StrAlloc( 100 ); + for ( i = 0; i < nValues; i++ ) + { + for ( k = 0; k < nValues; k++ ) + { + if ( k == i ) + Vec_StrPrintStr( vSop, "1 " ); + else + Vec_StrPrintStr( vSop, "- " ); + } + Vec_StrPrintNum( vSop, i ); + Vec_StrPush( vSop, '\n' ); + } + Vec_StrPush( vSop, 0 ); + pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) ); + Vec_StrFree( vSop ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the decover node.] + + Description [Produces MV-SOP for BLIF-MV representation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues ) +{ + char * pResult; + Vec_Str_t * vSop; + int i, b, nBits = Extra_Base2Log(nValues); + assert( nValues > 1 && nValues <= (1< 0) ); + Vec_StrPush( vSop, ' ' ); + } + Vec_StrPrintNum( vSop, i ); + Vec_StrPush( vSop, '\n' ); + } + Vec_StrPush( vSop, 0 ); + pResult = Abc_SopRegister( pMan, Vec_StrArray(vSop) ); + Vec_StrFree( vSop ); + return pResult; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 353bf046..84952019 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -53,43 +53,6 @@ void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan ) return pUserMan; } -/**Function************************************************************* - - Synopsis [Starts the Mv-Var manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk ) -{ - Vec_Att_t * pAttMan; - assert( Abc_NtkMvVar(pNtk) == NULL ); - pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL ); - Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan ); -} - -/**Function************************************************************* - - Synopsis [Stops the Mv-Var manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) -{ - void * pUserMan; - pUserMan = Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); - Extra_MmFlexStop( pUserMan ); -} - /**Function************************************************************* Synopsis [Increments the current traversal ID of the network.] @@ -754,12 +717,6 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ) Abc_NtkIncrementTravId( pNtk ); Abc_NtkForEachCo( pNtk, pNode, i ) { -/* - if ( strcmp( Abc_ObjName(pNode), "g704" ) == 0 ) - { - int s = 1; - } -*/ // if the driver is complemented, this is an error pDriver = Abc_ObjFanin0(pNode); if ( Abc_ObjFaninC0(pNode) ) diff --git a/src/base/abc/module.make b/src/base/abc/module.make index 5edf9000..7b34d8f6 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -1,4 +1,5 @@ SRC += src/base/abc/abcAig.c \ + src/base/abc/abcBlifMv.c \ src/base/abc/abcCheck.c \ src/base/abc/abcDfs.c \ src/base/abc/abcFanio.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cf7cc0e9..dc185302 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -46,6 +46,7 @@ static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -187,6 +188,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "print_kmap", Abc_CommandPrintKMap, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_xcut", Abc_CommandPrintXCut, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show", Abc_CommandShow, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); @@ -1394,6 +1396,64 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPrintXCut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fUseLibrary; + + extern int Abc_NtkCrossCut( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fUseLibrary = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) + { + switch ( c ) + { + case 'l': + fUseLibrary ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + Abc_NtkCrossCut( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: print_xcut [-h]\n" ); + fprintf( pErr, "\t prints the size of the cross cut of the current network\n" ); +// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* Synopsis [] @@ -2057,8 +2117,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) int fUseBdds; int fUseSops; int fUseCnfs; + int fUseMv; int fVerbose; - extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -2066,16 +2127,17 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nLutSize = 8; - nCutsMax = 5; + nCutsMax = 4; nFlowIters = 1; nAreaIters = 1; fArea = 0; fUseBdds = 0; fUseSops = 0; fUseCnfs = 0; + fUseMv = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscivh" ) ) != EOF ) { switch ( c ) { @@ -2135,6 +2197,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fUseCnfs ^= 1; break; + case 'i': + fUseMv ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -2145,7 +2210,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( fUseBdds && fUseSops || fUseBdds && fUseCnfs || fUseSops && fUseCnfs ) + if ( fUseBdds + fUseSops + fUseCnfs + fUseMv > 1 ) { fprintf( pErr, "Cannot optimize two parameters at the same time.\n" ); return 1; @@ -2157,7 +2222,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( nCutsMax < 2 || nCutsMax >= (1<<12) ) + if ( nCutsMax < 1 || nCutsMax >= (1<<12) ) { fprintf( pErr, "Incorrect number of cuts.\n" ); return 1; @@ -2175,7 +2240,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fVerbose ); + pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fUseMv, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Renoding has failed.\n" ); @@ -2186,16 +2251,17 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbcav]\n" ); + fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbciav]\n" ); fprintf( pErr, "\t transforms the AIG into a logic network with larger nodes\n" ); fprintf( pErr, "\t while minimizing the number of FF literals of the node SOPs\n" ); fprintf( pErr, "\t-K num : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize ); - fprintf( pErr, "\t-C num : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax ); + fprintf( pErr, "\t-C num : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCutsMax ); fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters ); fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters ); fprintf( pErr, "\t-s : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" ); fprintf( pErr, "\t-b : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" ); fprintf( pErr, "\t-c : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" ); + fprintf( pErr, "\t-i : toggles minimizing MV-SOP instead of FF lits [default = %s]\n", fUseMv? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" ); fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -2706,7 +2772,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fVeryVerbose = 0; fPlaceEnable = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwph" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwh" ) ) != EOF ) { switch ( c ) { @@ -2766,13 +2832,13 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: rewrite [-lzvwph]\n" ); + fprintf( pErr, "usage: rewrite [-lzvwh]\n" ); fprintf( pErr, "\t performs technology-independent rewriting of the AIG\n" ); fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" ); - fprintf( pErr, "\t-p : toggle placement-aware rewriting [default = %s]\n", fPlaceEnable? "yes": "no" ); +// fprintf( pErr, "\t-p : toggle placement-aware rewriting [default = %s]\n", fPlaceEnable? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -8074,13 +8140,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nFlowIters = 1; pPars->nAreaIters = 2; pPars->DelayTarget = -1; - pPars->fPreprocess = 1; + pPars->fPreprocess = 1;// pPars->fArea = 0; pPars->fFancy = 0; - pPars->fExpRed = 1; + pPars->fExpRed = 1;// pPars->fLatchPaths = 0; pPars->fSeqMap = 0; - pPars->fVerbose = 0; + pPars->fVerbose = 0;// // internal parameters pPars->fTruth = 0; pPars->nLatches = pNtk? Abc_NtkLatchNum(pNtk) : 0; @@ -8206,7 +8272,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( pPars->nCutsMax < 2 || pPars->nCutsMax >= (1<<12) ) + if ( pPars->nCutsMax < 1 || pPars->nCutsMax >= (1<<12) ) { fprintf( pErr, "Incorrect number of cuts.\n" ); return 1; @@ -8279,7 +8345,7 @@ usage: fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" ); fprintf( pErr, "\t performs FPGA technology mapping of the network\n" ); fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); - fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); + fprintf( pErr, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters ); fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters ); fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer ); diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 887f6cc9..00861e1b 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -125,9 +125,9 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) pIfMan = If_ManStart( pPars ); // print warning about excessive memory usage - if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30) > 0.5 ) - printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", - 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30), pPars->nCutsMax ); + if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30) > 1.0 ) + printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", + 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30), Abc_NtkObjNum(pNtk) ); // create PIs and remember them in the old nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan ); @@ -184,7 +184,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) Vec_Int_t * vCover; int i, nDupGates; // create the new network - if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs ) + if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); else if ( pIfMan->pPars->fUseSops ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); @@ -214,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) Abc_NtkDeleteObj( pNodeNew ); // minimize the node - if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseBdds ) + if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) Abc_NtkSweep( pNtkNew, 0 ); if ( pIfMan->pPars->fUseBdds ) Abc_NtkBddReorder( pNtkNew, 0 ); @@ -251,7 +251,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); - if ( pIfMan->pPars->fUseCnfs ) + if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); @@ -269,7 +269,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // transform truth table into the BDD pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 ); Cudd_Ref(pNodeNew->pData); } - else if ( pIfMan->pPars->fUseCnfs ) + else if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { // transform truth table into the BDD pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 ); Cudd_Ref(pNodeNew->pData); @@ -329,7 +329,7 @@ Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_ If_Cut_t * pCut; Hop_Obj_t * gFunc, * gFunc0, * gFunc1; // get the best cut - pCut = If_ObjCutTriv(pIfObj); + pCut = If_ObjCutBest(pIfObj); // if the cut is visited, return the result if ( If_CutData(pCut) ) return If_CutData(pCut); @@ -367,14 +367,14 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * assert( pCut->nLeaves > 1 ); // set the leaf variables If_CutForEachLeaf( pIfMan, pCut, pLeaf, i ) - If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) ); + If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) ); // recursively compute the function while collecting visited cuts Vec_PtrClear( pIfMan->vTemp ); gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); // printf( "%d ", Vec_PtrSize(p->vTemp) ); // clean the cuts If_CutForEachLeaf( pIfMan, pCut, pLeaf, i ) - If_CutSetData( If_ObjCutTriv(pLeaf), NULL ); + If_CutSetData( If_ObjCutBest(pLeaf), NULL ); Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i ) If_CutSetData( pCut, NULL ); return gFunc; diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index af3f55cf..17db7ed9 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -27,14 +27,16 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ); -static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ); +static int Abc_NtkRenodeEvalMv( If_Cut_t * pCut ); -static reo_man * s_pReo = NULL; -static DdManager * s_pDd = NULL; -static Vec_Int_t * s_vMemory = NULL; +static reo_man * s_pReo = NULL; +static DdManager * s_pDd = NULL; +static Vec_Int_t * s_vMemory = NULL; +static Vec_Int_t * s_vMemory2 = NULL; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -51,7 +53,7 @@ static Vec_Int_t * s_vMemory = NULL; SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ) +Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose ) { extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); If_Par_t Pars, * pPars = &Pars; @@ -85,6 +87,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF pPars->fUseBdds = fUseBdds; pPars->fUseSops = fUseSops; pPars->fUseCnfs = fUseCnfs; + pPars->fUseMv = fUseMv; if ( fUseBdds ) pPars->pFuncCost = Abc_NtkRenodeEvalBdd; else if ( fUseSops ) @@ -94,6 +97,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF pPars->fArea = 1; pPars->pFuncCost = Abc_NtkRenodeEvalCnf; } + else if ( fUseMv ) + pPars->pFuncCost = Abc_NtkRenodeEvalMv; else pPars->pFuncCost = Abc_NtkRenodeEvalAig; @@ -108,7 +113,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF else { assert( s_vMemory == NULL ); - s_vMemory = Vec_IntAlloc( 1 << 16 ); + s_vMemory = Vec_IntAlloc( 1 << 16 ); + s_vMemory2 = Vec_IntAlloc( 1 << 16 ); } // perform mapping/renoding @@ -125,12 +131,43 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF else { Vec_IntFree( s_vMemory ); + Vec_IntFree( s_vMemory2 ); s_vMemory = NULL; + s_vMemory2 = NULL; } return pNtkNew; } +/**Function************************************************************* + + Synopsis [Computes the cost based on the factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ) +{ + Kit_Graph_t * pGraph; + int i, nNodes; + pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory ); + if ( pGraph == NULL ) + { + for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) + pCut->pPerm[i] = 100; + return IF_COST_MAX; + } + nNodes = Kit_GraphNodeNum( pGraph ); + for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) + pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) ); + Kit_GraphFree( pGraph ); + return nNodes; +} + /**Function************************************************************* Synopsis [Computes the cost based on the BDD size after reordering.] @@ -178,7 +215,7 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ) pCut->pPerm[i] = 1; RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 ); if ( RetValue == -1 ) - return ABC_INFINITY; + return IF_COST_MAX; assert( RetValue == 0 || RetValue == 1 ); return Vec_IntSize( s_vMemory ); } @@ -197,12 +234,13 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ) int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) { int i, RetValue, nClauses; + // set internal mapper parameters for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) pCut->pPerm[i] = 1; // compute ISOP for the positive phase RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); if ( RetValue == -1 ) - return ABC_INFINITY; + return IF_COST_MAX; assert( RetValue == 0 || RetValue == 1 ); nClauses = Vec_IntSize( s_vMemory ); // compute ISOP for the negative phase @@ -210,7 +248,7 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); if ( RetValue == -1 ) - return ABC_INFINITY; + return IF_COST_MAX; assert( RetValue == 0 || RetValue == 1 ); nClauses += Vec_IntSize( s_vMemory ); return nClauses; @@ -218,7 +256,7 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) /**Function************************************************************* - Synopsis [Computes the cost based on the factored form.] + Synopsis [Computes the cost of MV-SOP of the cut function.] Description [] @@ -227,22 +265,29 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) SeeAlso [] ***********************************************************************/ -int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ) +int Abc_NtkRenodeEvalMv( If_Cut_t * pCut ) { - Kit_Graph_t * pGraph; - int i, nNodes; - pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory ); - if ( pGraph == NULL ) - { - for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) - pCut->pPerm[i] = 100; - return ABC_INFINITY; - } - nNodes = Kit_GraphNodeNum( pGraph ); + int i, RetValue; + // set internal mapper parameters for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) - pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) ); - Kit_GraphFree( pGraph ); - return nNodes; + pCut->pPerm[i] = 1; + // compute ISOP for the positive phase + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); + if ( RetValue == -1 ) + return IF_COST_MAX; + assert( RetValue == 0 || RetValue == 1 ); + // compute ISOP for the negative phase + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory2, 0 ); + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + if ( RetValue == -1 ) + return IF_COST_MAX; + assert( RetValue == 0 || RetValue == 1 ); + // return the cost of the cut + RetValue = Abc_NodeEvalMvCost( If_CutLeaveNum(pCut), s_vMemory, s_vMemory2 ); + if ( RetValue >= IF_COST_MAX ) + return IF_COST_MAX; + return RetValue; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 92691d6c..845f9d77 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1265,7 +1265,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); @@ -1406,7 +1406,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); @@ -1552,7 +1552,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv ) } // write out the current network - pNetlist = Abc_NtkToNetlist(pNtk,0); + pNetlist = Abc_NtkToNetlist(pNtk); if ( pNetlist == NULL ) { fprintf( pErr, "Cannot produce the intermediate network.\n" ); diff --git a/src/base/io/io.h b/src/base/io/io.h index 472e7b2d..7e23b6e4 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -95,8 +95,7 @@ extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ); /*=== abcWriteBlifMv.c ==========================================================*/ -extern void Io_WriteBlifMvDesign( Abc_Lib_t * pLib, char * FileName ); -extern void Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileName ); +extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteBench.c =========================================================*/ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteCnf.c ===========================================================*/ diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 3e09caf0..dc72c591 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -62,11 +62,13 @@ struct Io_MvMan_t_ { // general info about file int fBlifMv; // the file is BLIF-MV + int fUseReset; // the reset circuitry is added char * pFileName; // the name of the file char * pBuffer; // the contents of the file Vec_Ptr_t * vLines; // the line beginnings // the results of reading Abc_Lib_t * pDesign; // the design under construction + int nNDnodes; // the counter of ND nodes // intermediate storage for models Vec_Ptr_t * vModels; // vector of models Io_MvMod_t * pLatest; // the current model @@ -99,6 +101,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine ); static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset ); static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine ); static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens ); +static Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar ); static int Io_MvCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; } static int Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!'; } @@ -127,7 +130,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) Abc_Ntk_t * pNtk; Abc_Lib_t * pDesign; char * pDesignName; - int i; + int RetValue, i; // check that the file is available pFile = fopen( pFileName, "rb" ); @@ -141,6 +144,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) // start the file reader p = Io_MvAlloc(); p->fBlifMv = fBlifMv; + p->fUseReset = 0; p->pFileName = pFileName; p->pBuffer = Io_MvLoadFile( pFileName ); if ( p->pBuffer == NULL ) @@ -152,6 +156,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) pDesignName = Extra_FileNameGeneric( pFileName ); p->pDesign = Abc_LibCreate( pDesignName ); free( pDesignName ); + // free the HOP manager + Hop_ManStop( p->pDesign->pManFunc ); + p->pDesign->pManFunc = NULL; // prepare the file for parsing Io_MvReadPreparse( p ); // parse interfaces of each network @@ -163,6 +170,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) if ( pDesign == NULL ) return NULL; Io_MvFree( p ); +// pDesign should be linked to all models of the design // make sure that everything is okay with the network structure if ( fCheck ) @@ -177,11 +185,19 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) } } } -// pDesign should be linked to all models of the design + +//Abc_LibPrint( pDesign ); + + // detect top-level model + RetValue = Abc_LibFindTopLevelModels( pDesign ); + pNtk = Vec_PtrEntry( pDesign->vTops, 0 ); + if ( RetValue > 1 ) + printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n", + Vec_PtrSize(pDesign->vTops), pNtk->pName ); // extract the master network - pNtk = Vec_PtrEntry( pDesign->vModules, 0 ); pNtk->pDesign = pDesign; + pDesign->pManFunc = NULL; // verify the design for cyclic dependence assert( Vec_PtrSize(pDesign->vModules) > 0 ); @@ -195,10 +211,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) else Abc_NtkIsAcyclicHierarchy( pNtk ); -//Io_WriteBlifMvDesign( pDesign, "_temp_.mv" ); -//Abc_LibPrint( pDesign ); -//Abc_LibFree( pDesign ); -//return NULL; +//Io_WriteBlifMv( pNtk, "_temp_.mv" ); return pNtk; } @@ -691,16 +704,18 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p ) return NULL; } // create binary latch with 1-data and 0-init - pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv ); + if ( p->fUseReset ) + pMod->pResetLatch = Io_ReadCreateResetLatch( pMod->pNtk, p->fBlifMv ); } // parse the latches Vec_PtrForEachEntry( pMod->vLatches, pLine, k ) if ( !Io_MvParseLineLatch( pMod, pLine ) ) return NULL; // parse the reset lines - Vec_PtrForEachEntry( pMod->vResets, pLine, k ) - if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) ) - return NULL; + if ( p->fUseReset ) + Vec_PtrForEachEntry( pMod->vResets, pLine, k ) + if ( !Io_MvParseLineNamesMv( pMod, pLine, 1 ) ) + return NULL; // parse the nodes if ( p->fBlifMv ) { @@ -721,6 +736,9 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p ) // finalize the network Abc_NtkFinalizeRead( pMod->pNtk ); } + if ( p->nNDnodes ) +// printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes ); + printf( "Warning: The parser added %d constant 0 nodes to replace non-deterministic nodes.\n", p->nNDnodes ); // return the network pDesign = p->pDesign; p->pDesign = NULL; @@ -822,7 +840,7 @@ static int Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine ) static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; - Abc_Obj_t * pObj, * pMux, * pNet; + Abc_Obj_t * pObj, * pNet; char * pToken; int Init; Io_MvSplitIntoTokens( vTokens, pLine, '\0' ); @@ -838,33 +856,35 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine ) { pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Vec_PtrEntry(vTokens,2) ); // get initial value - if ( Vec_PtrSize(vTokens) > 3 ) - Init = atoi( Vec_PtrEntry(vTokens,3) ); + if ( p->pMan->fBlifMv ) + Abc_LatchSetInit0( pObj ); else - Init = 2; - if ( Init < 0 || Init > 2 ) { - sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); - return 0; + if ( Vec_PtrSize(vTokens) > 3 ) + Init = atoi( Vec_PtrEntry(vTokens,3) ); + else + Init = 2; + if ( Init < 0 || Init > 2 ) + { + sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); + return 0; + } + if ( Init == 0 ) + Abc_LatchSetInit0( pObj ); + else if ( Init == 1 ) + Abc_LatchSetInit1( pObj ); + else // if ( Init == 2 ) + Abc_LatchSetInitDc( pObj ); } - if ( Init == 0 ) - Abc_LatchSetInit0( pObj ); - else if ( Init == 1 ) - Abc_LatchSetInit1( pObj ); - else // if ( Init == 2 ) - Abc_LatchSetInitDc( pObj ); } else { - // get the net corresponding to output of reset latch - pNet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch)); - assert( Abc_ObjIsNet(pNet) ); - // create mux - pMux = Io_ReadCreateResetMux( p->pNtk, Abc_ObjName(pNet), Vec_PtrEntry(vTokens,1), p->pMan->fBlifMv ); - // get the net of mux output - pNet = Abc_ObjFanout0(pMux); + // get the net corresponding to the output of the latch + pNet = Abc_NtkFindOrCreateNet( p->pNtk, Vec_PtrEntry(vTokens,2) ); + // get the net corresponding to the latch output (feeding into reset MUX) + pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") ); // create latch - pObj = Io_ReadCreateLatch( p->pNtk, Abc_ObjName(pNet), Vec_PtrEntry(vTokens,2) ); + pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) ); Abc_LatchSetInit0( pObj ); } return 1; @@ -1180,7 +1200,7 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * // prepare the place for the cover Vec_StrClear( vFunc ); // write the number of values - Io_MvWriteValues( pNode, vFunc ); +// Io_MvWriteValues( pNode, vFunc ); // get the first token pFirst = Vec_PtrEntry( vTokens2, 0 ); if ( pFirst[0] == '.' ) @@ -1215,6 +1235,60 @@ static char * Io_MvParseTableMv( Io_MvMod_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * return Vec_StrArray( vFunc ); } +/**Function************************************************************* + + Synopsis [Adds reset circuitry corresponding to latch with pName.] + + Description [Returns the reset node's net.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName ) +{ + char Buffer[50]; + Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pOutNet; + Io_MvVar_t * pVar; + // make sure the reset latch exists + assert( p->pResetLatch != NULL ); + // get the reset net + pResetLONet = Abc_ObjFanout0(Abc_ObjFanout0(p->pResetLatch)); + // get the output net + pOutNet = Abc_NtkFindOrCreateNet( p->pNtk, pName ); + // get the data nets + pData0Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_reset") ); + pData1Net = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pOutNet, "_out") ); + // duplicate MV variables + if ( Abc_NtkMvVar(p->pNtk) ) + { + pVar = Abc_ObjMvVar( pOutNet ); + Abc_ObjSetMvVar( pData0Net, Abc_NtkMvVarDup(p->pNtk, pVar) ); + Abc_ObjSetMvVar( pData1Net, Abc_NtkMvVarDup(p->pNtk, pVar) ); + } + // create the node + pNode = Abc_NtkCreateNode( p->pNtk ); + // create the output net + Abc_ObjAddFanin( pOutNet, pNode ); + // create the function + if ( p->pMan->fBlifMv ) + { +// Vec_Att_t * p = Abc_NtkMvVar( pNtk ); + int nValues = Abc_ObjMvVarNum(pOutNet); +// sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues ); + sprintf( Buffer, "1 - - =1\n0 - - =2\n" ); + pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, Buffer ); + } + else + pNode->pData = Abc_SopCreateMux( p->pNtk->pManFunc ); + // add nets + Abc_ObjAddFanin( pNode, pResetLONet ); + Abc_ObjAddFanin( pNode, pData1Net ); + Abc_ObjAddFanin( pNode, pData0Net ); + return pData0Net; +} + /**Function************************************************************* Synopsis [Parses the nodes line.] @@ -1241,19 +1315,15 @@ static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Pt sprintf( p->pMan->sError, "Line %d: Latch with output signal \"%s\" does not exist.", Io_MvGetLine(p->pMan, pName), pName ); return 0; } +/* if ( !Abc_ObjIsBo(Abc_ObjFanin0(pNet)) ) { sprintf( p->pMan->sError, "Line %d: Reset line \"%s\" defines signal that is not a latch output.", Io_MvGetLine(p->pMan, pName), pName ); return 0; } - // get the latch input - pNode = Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(pNet))); - assert( Abc_ObjIsBi(pNode) ); - // get the MUX feeding into the latch - pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNode)); - assert( Abc_ObjFaninNum(pNode) == 3 ); - // get the corresponding fanin net - pNet = Abc_ObjFanin( pNode, 2 ); +*/ + // construct the reset circuit and get the reset net feeding into it + pNet = Io_MvParseAddResetCircuit( p, pName ); // create fanins pNode = Io_ReadCreateNode( p->pNtk, Abc_ObjName(pNet), (char **)(vTokens->pArray + 1), nInputs ); assert( nInputs == Vec_PtrSize(vTokens) - 2 ); @@ -1292,6 +1362,7 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; Vec_Ptr_t * vTokens2 = p->pMan->vTokens2; + Abc_Obj_t * pNet; char * pName, * pFirst, * pArrow; int nInputs, nOutputs, nLiterals, nLines, i; assert( p->pMan->fBlifMv ); @@ -1341,27 +1412,23 @@ static int Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset ) nLines = nLiterals / (nInputs + nOutputs); if ( nInputs == 0 && nLines > 1 ) { - Abc_Obj_t * pNode, * pNet; // add the outputs to the PIs for ( i = 0; i < nOutputs; i++ ) { pName = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - nOutputs + i ); - fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName ); // get the net corresponding to this node pNet = Abc_NtkFindOrCreateNet(p->pNtk, pName); if ( fReset ) { - // get the latch input - pNode = Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(pNet))); - assert( Abc_ObjIsBi(pNode) ); - // get the MUX feeding into the latch - pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNode)); - assert( Abc_ObjFaninNum(pNode) == 3 ); - // get the corresponding fanin net - pNet = Abc_ObjFanin( pNode, 2 ); + assert( p->pResetLatch != NULL ); + // construct the reset circuit and get the reset net feeding into it + pNet = Io_MvParseAddResetCircuit( p, pName ); } -// Io_ReadCreatePi( p->pNtk, pName ); - Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) ); + // add the new PI node +// Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(p->pNtk) ); +// fprintf( stdout, "Io_ReadBlifMv(): Adding PI for internal non-deterministic node \"%s\".\n", pName ); + p->pMan->nNDnodes++; + Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(p->pNtk) ); } return 1; } @@ -1437,7 +1504,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins ) sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity ); return NULL; } - // parse one product product + // parse one product Vec_StrAppend( vFunc, pProduct ); Vec_StrPush( vFunc, ' ' ); Vec_StrPush( vFunc, pOutput[0] ); @@ -1487,6 +1554,40 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine ) return 1; } +/**Function************************************************************* + + Synopsis [Duplicate the MV variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar ) +{ + Extra_MmFlex_t * pFlex; + Io_MvVar_t * pVarDup; + int i; + if ( pVar == NULL ) + return NULL; + pFlex = Abc_NtkMvVarMan( pNtk ); + assert( pFlex != NULL ); + pVarDup = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) ); + pVarDup->nValues = pVar->nValues; + pVarDup->pNames = NULL; + if ( pVar->pNames == NULL ) + return pVarDup; + pVarDup->pNames = (char **)Extra_MmFlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues ); + for ( i = 0; i < pVar->nValues; i++ ) + { + pVarDup->pNames[i] = (char *)Extra_MmFlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 ); + strcpy( pVarDup->pNames[i], pVar->pNames[i] ); + } + return pVarDup; +} + #include "mio.h" #include "main.h" diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c index 090cf254..c64e330c 100644 --- a/src/base/io/ioReadVerilog.c +++ b/src/base/io/ioReadVerilog.c @@ -45,14 +45,21 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ) { Abc_Ntk_t * pNtk; Abc_Lib_t * pDesign; + int RetValue; // parse the verilog file pDesign = Ver_ParseFile( pFileName, NULL, fCheck, 1 ); if ( pDesign == NULL ) return NULL; -/* + + // detect top-level model + RetValue = Abc_LibFindTopLevelModels( pDesign ); + pNtk = Vec_PtrEntry( pDesign->vTops, 0 ); + if ( RetValue > 1 ) + printf( "Warning: The design has %d root-level modules. The first one (%s) will be used.\n", + Vec_PtrSize(pDesign->vTops), pNtk->pName ); + // extract the master network - pNtk = Vec_PtrEntryLast( pDesign->vModules ); pNtk->pDesign = pDesign; pDesign->pManFunc = NULL; @@ -67,35 +74,11 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ) } else { - // bring the root model to the beginning - for ( i = Vec_PtrSize(pDesign->vModules) - 2; i >= 0; i-- ) - Vec_PtrWriteEntry(pDesign->vModules, i+1, Vec_PtrEntry(pDesign->vModules, i) ); - Vec_PtrWriteEntry(pDesign->vModules, 0, pNtk ); // check that there is no cyclic dependency Abc_NtkIsAcyclicHierarchy( pNtk ); } -*/ - // extract the master network - pNtk = Vec_PtrEntry( pDesign->vModules, 0 ); - pNtk->pDesign = pDesign; - pDesign->pManFunc = NULL; //Io_WriteVerilog( pNtk, "_temp.v" ); - - // verify the design for cyclic dependence - assert( Vec_PtrSize(pDesign->vModules) > 0 ); - if ( Vec_PtrSize(pDesign->vModules) == 1 ) - { -// printf( "Warning: The design is not hierarchical.\n" ); - Abc_LibFree( pDesign, pNtk ); - pNtk->pDesign = NULL; - pNtk->pSpec = Extra_UtilStrsav( pFileName ); - } - else - { - // check that there is no cyclic dependency - Abc_NtkIsAcyclicHierarchy( pNtk ); - } return pNtk; } diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 0ac3181a..9845fbab 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -173,27 +173,6 @@ Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck ) return NULL; if ( !Abc_NtkIsNetlist(pNtk) ) return pNtk; - // consider the case of BLIF-MV - if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) - { - extern Abc_Ntk_t * Abc_NtkConvertBlifMv( Abc_Ntk_t * pNtk ); -Abc_NtkPrintStats( stdout, pNtk, 0 ); -/* -{ - FILE * pFile = fopen( "_temp_.mv", "w" ); - Io_NtkWriteBlifMv( pFile, pNtk ); - fclose( pFile ); -} -*/ - pNtk = Abc_NtkConvertBlifMv( pTemp = pNtk ); - Abc_NtkDelete( pTemp ); - if ( pNtk == NULL ) - { - fprintf( stdout, "Converting BLIF-MV has failed.\n" ); - return NULL; - } - return pNtk; - } // flatten logic hierarchy assert( Abc_NtkIsNetlist(pNtk) ); if ( Abc_NtkWhiteboxNum(pNtk) > 0 ) @@ -218,69 +197,19 @@ Abc_NtkPrintStats( stdout, pNtk, 0 ); return NULL; } } - // convert the netlist into the logic network - pNtk = Abc_NtkToLogic( pTemp = pNtk ); - Abc_NtkDelete( pTemp ); - if ( pNtk == NULL ) - { - fprintf( stdout, "Converting netlist to logic network after reading has failed.\n" ); - return NULL; - } - return pNtk; -} - -/**Function************************************************************* - - Synopsis [Read the network from a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Io_ReadHie( char * pFileName, Io_FileType_t FileType, int fCheck ) -{ - Abc_Ntk_t * pNtk, * pTemp; - // detect the file type - if ( Io_ReadFileType(pFileName) == IO_FILE_BLIF ) - pNtk = Io_ReadBlifMv( pFileName, 0, fCheck ); -// else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) -// pNtk = Io_ReadBlifMv( pFileName, 1, fCheck ); - else if ( Io_ReadFileType(pFileName) == IO_FILE_VERILOG ) - pNtk = Io_ReadVerilog( pFileName, fCheck ); - else - { - printf( "Wrong file type.\n" ); - return NULL; - } - if ( pNtk == NULL ) - return NULL; -// printf( "\n" ); - // flatten logic hierarchy - assert( Abc_NtkIsNetlist(pNtk) ); - if ( Abc_NtkWhiteboxNum(pNtk) > 0 ) - { - pNtk = Abc_NtkFlattenLogicHierarchy( pTemp = pNtk ); - Abc_NtkDelete( pTemp ); - if ( pNtk == NULL ) - { - fprintf( stdout, "Flattening logic hierarchy has failed.\n" ); - return NULL; - } - } - // convert blackboxes - if ( Abc_NtkBlackboxNum(pNtk) > 0 ) + // consider the case of BLIF-MV + if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) { - printf( "Hierarchy reader converted %d instances of blackboxes.\n", Abc_NtkBlackboxNum(pNtk) ); - pNtk = Abc_NtkConvertBlackboxes( pTemp = pNtk ); +//Abc_NtkPrintStats( stdout, pNtk, 0 ); +// Io_WriteBlifMv( pNtk, "_temp_.mv" ); + pNtk = Abc_NtkStrashBlifMv( pTemp = pNtk ); Abc_NtkDelete( pTemp ); if ( pNtk == NULL ) { - fprintf( stdout, "Converting blackboxes has failed.\n" ); + fprintf( stdout, "Converting BLIF-MV to AIG has failed.\n" ); return NULL; } + return pNtk; } // convert the netlist into the logic network pNtk = Abc_NtkToLogic( pTemp = pNtk ); @@ -349,7 +278,13 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) Io_WriteGml( pNtk, pFileName ); return; } - +/* + if ( FileType == IO_FILE_BLIFMV ) + { + Io_WriteBlifMv( pNtk, pFileName ); + return; + } +*/ // convert logic network into netlist if ( FileType == IO_FILE_PLA ) { @@ -359,15 +294,17 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) return; } if ( Abc_NtkIsComb(pNtk) ) - pNtkTemp = Abc_NtkToNetlist( pNtk, 1 ); + pNtkTemp = Abc_NtkToNetlist( pNtk ); else { fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" ); pNtkCopy = Abc_NtkDup( pNtk ); Abc_NtkMakeComb( pNtkCopy ); - pNtkTemp = Abc_NtkToNetlist( pNtk, 1 ); + pNtkTemp = Abc_NtkToNetlist( pNtk ); Abc_NtkDelete( pNtkCopy ); } + if ( !Abc_NtkToSop( pNtk, 1 ) ) + return; } else if ( FileType == IO_FILE_BENCH ) { @@ -379,7 +316,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) pNtkTemp = Abc_NtkToNetlistBench( pNtk ); } else - pNtkTemp = Abc_NtkToNetlist( pNtk, 0 ); + pNtkTemp = Abc_NtkToNetlist( pNtk ); if ( pNtkTemp == NULL ) { @@ -393,6 +330,12 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) Abc_NtkToSop( pNtkTemp, 0 ); Io_WriteBlif( pNtkTemp, pFileName, 1 ); } + else if ( FileType == IO_FILE_BLIFMV ) + { + if ( !Abc_NtkConvertToBlifMv( pNtkTemp ) ) + return; + Io_WriteBlifMv( pNtkTemp, pFileName ); + } else if ( FileType == IO_FILE_BENCH ) Io_WriteBench( pNtkTemp, pFileName ); else if ( FileType == IO_FILE_PLA ) @@ -439,6 +382,8 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) ); if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIF ) pNtkBase = Io_ReadBlifMv( pBaseName, 0, 1 ); + else if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV ) + pNtkBase = Io_ReadBlifMv( pBaseName, 1, 1 ); else if ( Io_ReadFileType(pBaseName) == IO_FILE_VERILOG ) pNtkBase = Io_ReadVerilog( pBaseName, 1 ); else @@ -446,6 +391,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) if ( pNtkBase == NULL ) return; + // flatten logic hierarchy if present if ( Abc_NtkWhiteboxNum(pNtkBase) > 0 ) { pNtkBase = Abc_NtkFlattenLogicHierarchy( pNtkTemp = pNtkBase ); @@ -455,10 +401,27 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) } // reintroduce the boxes into the netlist - if ( Abc_NtkBlackboxNum(pNtkBase) > 0 ) + if ( Io_ReadFileType(pBaseName) == IO_FILE_BLIFMV ) + { + if ( Abc_NtkBlackboxNum(pNtkBase) > 0 ) + { + printf( "Hierarchy writer does not support BLIF-MV with blackboxes.\n" ); + Abc_NtkDelete( pNtkBase ); + return; + } + // convert the current network to BLIF-MV + assert( !Abc_NtkIsNetlist(pNtk) ); + pNtkResult = Abc_NtkToNetlist( pNtk ); + if ( !Abc_NtkConvertToBlifMv( pNtkResult ) ) + return; + // reintroduce the network + pNtkResult = Abc_NtkInsertBlifMv( pNtkBase, pNtkTemp = pNtkResult ); + Abc_NtkDelete( pNtkTemp ); + } + else if ( Abc_NtkBlackboxNum(pNtkBase) > 0 ) { // derive the netlist - pNtkResult = Abc_NtkToNetlist( pNtk, 0 ); + pNtkResult = Abc_NtkToNetlist( pNtk ); pNtkResult = Abc_NtkInsertNewLogic( pNtkBase, pNtkTemp = pNtkResult ); Abc_NtkDelete( pNtkTemp ); if ( pNtkResult ) @@ -467,7 +430,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) else { printf( "Warning: The output network does not contain blackboxes.\n" ); - pNtkResult = Abc_NtkToNetlist( pNtk, 0 ); + pNtkResult = Abc_NtkToNetlist( pNtk ); } Abc_NtkDelete( pNtkBase ); if ( pNtkResult == NULL ) @@ -486,6 +449,10 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) Abc_NtkToAig( pNtkResult ); Io_WriteVerilog( pNtkResult, pFileName ); } + else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) + { + Io_WriteBlifMv( pNtkResult, pFileName ); + } else fprintf( stderr, "Unknown output file format.\n" ); @@ -614,59 +581,24 @@ Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ) Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv ) { Abc_Obj_t * pLatch, * pNode; + Abc_Obj_t * pNetLI, * pNetLO; // create latch with 0 init value - pLatch = Io_ReadCreateLatch( pNtk, "_resetLI_", "_resetLO_" ); +// pLatch = Io_ReadCreateLatch( pNtk, "_resetLI_", "_resetLO_" ); + pNetLI = Abc_NtkCreateNet( pNtk ); + pNetLO = Abc_NtkCreateNet( pNtk ); + Abc_ObjAssignName( pNetLI, Abc_ObjName(pNetLI), NULL ); + Abc_ObjAssignName( pNetLO, Abc_ObjName(pNetLO), NULL ); + pLatch = Io_ReadCreateLatch( pNtk, Abc_ObjName(pNetLI), Abc_ObjName(pNetLO) ); + // set the initial value Abc_LatchSetInit0( pLatch ); // feed the latch with constant1- node - pNode = Abc_NtkCreateNode( pNtk ); - pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" ); +// pNode = Abc_NtkCreateNode( pNtk ); +// pNode->pData = Abc_SopRegister( pNtk->pManFunc, "2\n1\n" ); + pNode = Abc_NtkCreateNodeConst1( pNtk ); Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pNode ); return pLatch; } -/**Function************************************************************* - - Synopsis [Create a latch with the given input/output.] - - Description [By default, the latch value is unknown (ABC_INIT_NONE).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv ) -{ - char Buffer[50]; - Abc_Obj_t * pNode, * pData0Net, * pData1Net, * pResetLONet, * pLINet; - // get the reset output net - pResetLONet = Abc_NtkFindNet( pNtk, pResetLO ); - assert( pResetLONet ); - // get the latch input net - pData1Net = Abc_NtkFindOrCreateNet( pNtk, pDataLI ); - // create Data0 net (coming from reset node) - pData0Net = Abc_NtkFindOrCreateNet( pNtk, Abc_ObjNameSuffix(pData1Net, "_reset") ); - // create the node - pNode = Abc_NtkCreateNode( pNtk ); - if ( fBlifMv ) - { -// Vec_Att_t * p = Abc_NtkMvVar( pNtk ); - int nValues = Abc_ObjMvVarNum(pData1Net); - sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues ); - pNode->pData = Abc_SopRegister( pNtk->pManFunc, Buffer ); - } - else - pNode->pData = Abc_SopCreateMux( pNtk->pManFunc ); - // add nets - Abc_ObjAddFanin( pNode, pResetLONet ); - Abc_ObjAddFanin( pNode, pData1Net ); - Abc_ObjAddFanin( pNode, pData0Net ); - // create the output net - pLINet = Abc_NtkFindOrCreateNet( pNtk, Abc_ObjNameSuffix(pData1Net, "_mux") ); - Abc_ObjAddFanin( pLINet, pNode ); - return pNode; -} - /**Function************************************************************* Synopsis [Create node and the net driven by it.] diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 3b7d78ca..00768356 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -225,7 +225,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName ) // write the buffer fwrite( pBuffer, 1, Pos, pFile ); free( pBuffer ); - +/* // write the symbol table // write PIs Abc_NtkForEachPi( pNtk, pObj, i ) @@ -236,7 +236,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName ) // write POs Abc_NtkForEachPo( pNtk, pObj, i ) fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); - +*/ // write the comment fprintf( pFile, "c\n" ); fprintf( pFile, "%s\n", pNtk->pName ); diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index 417fe2a3..c0c29d65 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -56,7 +56,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) { Abc_Ntk_t * pNtkTemp; // derive the netlist - pNtkTemp = Abc_NtkToNetlist(pNtk,0); + pNtkTemp = Abc_NtkToNetlist(pNtk); if ( pNtkTemp == NULL ) { fprintf( stdout, "Writing BLIF has failed.\n" ); @@ -80,6 +80,8 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) { FILE * pFile; + Abc_Ntk_t * pNtkTemp; + int i; assert( Abc_NtkIsNetlist(pNtk) ); // start writing the file pFile = fopen( FileName, "w" ); @@ -96,18 +98,6 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ) // write the hierarchy if present if ( Abc_NtkBlackboxNum(pNtk) > 0 ) { - Abc_Ntk_t * pNtkTemp; - int i; -/* - Abc_Obj_t * pObj; - Abc_NtkForEachBlackbox( pNtk, pObj, i ) - { - pNtkTemp = pObj->pData; - assert( pNtkTemp != NULL && Abc_NtkHasBlackbox(pNtkTemp) ); - fprintf( pFile, "\n\n" ); - Io_NtkWrite( pFile, pNtkTemp, fWriteLatches ); - } -*/ Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i ) { if ( pNtkTemp == pNtk ) diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c index 597ca945..775a2e07 100644 --- a/src/base/io/ioWriteBlifMv.c +++ b/src/base/io/ioWriteBlifMv.c @@ -26,7 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -void Io_NtkWriteBlifMv( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteBlifMv( FILE * pFile, Abc_Ntk_t * pNtk ); static void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk ); static void Io_NtkWriteBlifMvPis( FILE * pFile, Abc_Ntk_t * pNtk ); static void Io_NtkWriteBlifMvPos( FILE * pFile, Abc_Ntk_t * pNtk ); @@ -52,49 +52,34 @@ static void Io_NtkWriteBlifMvValues( FILE * pFile, Abc_Obj_t * pNode ); SeeAlso [] ***********************************************************************/ -void Io_WriteBlifMvDesign( Abc_Lib_t * pLib, char * FileName ) +void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ) { FILE * pFile; - Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtkTemp; int i; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_NtkHasBlifMv(pNtk) ); // start writing the file pFile = fopen( FileName, "w" ); if ( pFile == NULL ) { - fprintf( stdout, "Io_WriteBlifMvDesign(): Cannot open the output file.\n" ); - return; - } - fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pLib->pName, Extra_TimeStamp() ); - // write the master network - Vec_PtrForEachEntry( pLib->vModules, pNtk, i ) - Io_NtkWriteBlifMv( pFile, pNtk ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Write the network into a BLIF file with the given name.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileName ) -{ - FILE * pFile; - // start writing the file - pFile = fopen( FileName, "w" ); - if ( pFile == NULL ) - { - fprintf( stdout, "Io_WriteMvNetlist(): Cannot open the output file.\n" ); + fprintf( stdout, "Io_WriteBlifMv(): Cannot open the output file.\n" ); return; } fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); // write the master network Io_NtkWriteBlifMv( pFile, pNtk ); + // write the remaining networks + if ( pNtk->pDesign ) + { + Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i ) + { + if ( pNtkTemp == pNtk ) + continue; + fprintf( pFile, "\n\n" ); + Io_NtkWriteBlifMv( pFile, pNtkTemp ); + } + } fclose( pFile ); } @@ -185,7 +170,7 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk ) Io_NtkWriteBlifMvLatch( pFile, pLatch ); fprintf( pFile, "\n" ); } - +/* // write the subcircuits assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); if ( Abc_NtkBlackboxNum(pNtk) > 0 ) @@ -195,6 +180,18 @@ void Io_NtkWriteBlifMvOne( FILE * pFile, Abc_Ntk_t * pNtk ) Io_NtkWriteBlifMvSubckt( pFile, pNode ); fprintf( pFile, "\n" ); } +*/ + if ( Abc_NtkBlackboxNum(pNtk) > 0 || Abc_NtkWhiteboxNum(pNtk) > 0 ) + { + fprintf( pFile, "\n" ); + Abc_NtkForEachBox( pNtk, pNode, i ) + { + if ( Abc_ObjIsLatch(pNode) ) + continue; + Io_NtkWriteBlifMvSubckt( pFile, pNode ); + } + fprintf( pFile, "\n" ); + } // write each internal node pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); @@ -414,26 +411,32 @@ void Io_NtkWriteBlifMvNode( FILE * pFile, Abc_Obj_t * pNode ) Abc_Obj_t * pFanin; char * pCur; int nValues, iFanin, i; - fprintf( pFile, "\n" ); + // write .mv directives for the fanins - pCur = Abc_ObjData(pNode); + fprintf( pFile, "\n" ); Abc_ObjForEachFanin( pNode, pFanin, i ) { - nValues = atoi(pCur); +// nValues = atoi(pCur); + nValues = Abc_ObjMvVarNum( pFanin ); if ( nValues > 2 ) fprintf( pFile, ".mv %s %d\n", Abc_ObjName(pFanin), nValues ); - while ( *pCur++ != ' ' ); +// while ( *pCur++ != ' ' ); } + // write .mv directives for the node - nValues = atoi(pCur); +// nValues = atoi(pCur); + nValues = Abc_ObjMvVarNum( Abc_ObjFanout0(pNode) ); if ( nValues > 2 ) fprintf( pFile, ".mv %s %d\n", Abc_ObjName(Abc_ObjFanout0(pNode)), nValues ); - while ( *pCur++ != '\n' ); +// while ( *pCur++ != '\n' ); + // write the .names line fprintf( pFile, ".table" ); Io_NtkWriteBlifMvNodeFanins( pFile, pNode ); fprintf( pFile, "\n" ); + // write the cubes + pCur = Abc_ObjData(pNode); if ( *pCur == 'd' ) { fprintf( pFile, ".default " ); diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index d8bb1855..8ae3cc42 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -277,6 +277,8 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho { if ( (int)pNode->Level != Level ) continue; + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; // fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); if ( Abc_NtkIsStrash(pNtk) ) pSopString = ""; @@ -313,7 +315,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho // check if the costant node is present if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 ) { - fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id ); + fprintf( pFile, " Node%d [label = \"Const%d\"", pNode->Id, Abc_NtkIsStrash(pNode->pNtk) || Abc_NodeIsConst1(pNode) ); fprintf( pFile, ", shape = ellipse" ); if ( pNode->fMarkB ) fprintf( pFile, ", style = filled" ); diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h index 0ba081db..cf2b7497 100644 --- a/src/base/ver/ver.h +++ b/src/base/ver/ver.h @@ -56,6 +56,7 @@ struct Ver_Man_t_ ProgressBar * pProgress; // current design Abc_Lib_t * pDesign; + st_table * tName2Suffix; // error handling FILE * Output; int fTopLevel; @@ -67,6 +68,7 @@ struct Ver_Man_t_ Vec_Int_t * vStackOp; }; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index 6c036288..89f9a689 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -61,18 +61,29 @@ static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateT static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ); static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ); static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ); -static int Vec_ParseAttachBoxes( Ver_Man_t * pMan ); +static int Ver_ParseAttachBoxes( Ver_Man_t * pMan ); static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO ); static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ); +static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan ); + static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); } static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); } +//static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); } + int glo_fMapped = 0; // this is bad! +typedef struct Ver_Bundle_t_ Ver_Bundle_t; +struct Ver_Bundle_t_ +{ + char * pNameFormal; // the name of the formal net + Vec_Ptr_t * vNetsActual; // the vector of actual nets (MSB to LSB) +}; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -201,7 +212,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) } // process defined and undefined boxes - if ( !Vec_ParseAttachBoxes( pMan ) ) + if ( !Ver_ParseAttachBoxes( pMan ) ) return; // connect the boxes and check @@ -213,7 +224,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) ) { pMan->fTopLevel = 1; - sprintf( pMan->sError, "The network check has failed.", pNtk->pName ); + sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName ); Ver_ParsePrintErrorMessage( pMan ); return; } @@ -391,7 +402,7 @@ int Ver_ParseModule( Ver_Man_t * pMan ) // make sure we stopped at the opening paranthesis if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName ); + sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -406,7 +417,12 @@ int Ver_ParseModule( Ver_Man_t * pMan ) if ( !Ver_ParseSkipComments( pMan ) ) return 0; Symbol = Ver_StreamPopChar(p); - assert( Symbol == ';' ); + if ( Symbol != ';' ) + { + sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } // parse the inputs/outputs/registers/wires/inouts while ( 1 ) @@ -508,12 +524,141 @@ int Ver_ParseModule( Ver_Man_t * pMan ) } } } + + // remove the table if needed + Ver_ParseRemoveSuffixTable( pMan ); return 1; } + /**Function************************************************************* - Synopsis [Parses one directive.] + Synopsis [Lookups the suffix of the signal of the form [m:n].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseLookupSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb ) +{ + unsigned Value; + *pnMsb = *pnLsb = -1; + if ( pMan->tName2Suffix == NULL ) + return 1; + if ( !st_lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) ) + return 1; + *pnMsb = (Value >> 8) & 0xff; + *pnLsb = Value & 0xff; + return 1; +} + +/**Function************************************************************* + + Synopsis [Lookups the suffix of the signal of the form [m:n].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb ) +{ + unsigned Value; + if ( pMan->tName2Suffix == NULL ) + pMan->tName2Suffix = st_init_table( strcmp, st_strhash ); + if ( st_is_member( pMan->tName2Suffix, pWord ) ) + return 1; + assert( nMsb >= 0 && nMsb < 128 ); + assert( nLsb >= 0 && nLsb < 128 ); + Value = (nMsb << 8) | nLsb; + st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Lookups the suffic of the signal of the form [m:n].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan ) +{ + st_generator * gen; + char * pKey, * pValue; + if ( pMan->tName2Suffix == NULL ) + return; + st_foreach_item( pMan->tName2Suffix, gen, (char **)&pKey, (char **)&pValue ) + free( pKey ); + st_free_table( pMan->tName2Suffix ); + pMan->tName2Suffix = NULL; +} + +/**Function************************************************************* + + Synopsis [Determine signal prefix of the form [Beg:End].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb ) +{ + char * pWord = *ppWord; + int nMsb, nLsb; + assert( pWord[0] == '[' ); + // get the beginning + nMsb = atoi( pWord + 1 ); + // find the splitter + while ( *pWord && *pWord != ':' && *pWord != ']' ) + pWord++; + if ( *pWord == 0 ) + { + sprintf( pMan->sError, "Cannot find closing bracket in this line." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + if ( *pWord == ']' ) + nLsb = nMsb; + else + { + assert( *pWord == ':' ); + nLsb = atoi( pWord + 1 ); + // find the closing paranthesis + while ( *pWord && *pWord != ']' ) + pWord++; + if ( *pWord == 0 ) + { + sprintf( pMan->sError, "Cannot find closing bracket in this line." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + assert( *pWord == ']' ); + pWord++; + } + assert( nMsb >= 0 && nLsb >= 0 ); + // return + *ppWord = pWord; + *pnMsb = nMsb; + *pnLsb = nLsb; + return 1; +} + +/**Function************************************************************* + + Synopsis [Determine signal suffix of the form [m:n].] Description [] @@ -521,17 +666,120 @@ int Ver_ParseModule( Ver_Man_t * pMan ) SeeAlso [] +***********************************************************************/ +int Ver_ParseSignalSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb ) +{ + char * pCur; + int Length; + Length = strlen(pWord); + assert( pWord[Length-1] == ']' ); + // walk backward + for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- ) + if ( *pCur == ':' || *pCur == '[' ) + break; + if ( pCur == pWord ) + { + sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + if ( *pCur == '[' ) + { + *pnMsb = *pnLsb = atoi(pCur+1); + *pCur = 0; + return 1; + } + assert( *pCur == ':' ); + // get the end of the interval + *pnLsb = atoi(pCur+1); + // find the beginning + for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- ) + if ( *pCur == '[' ) + break; + if ( pCur == pWord ) + { + sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + assert( *pCur == '[' ); + // get the beginning of the interval + *pnMsb = atoi(pCur+1); + // cut the word + *pCur = 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns the values of constant bits.] + + Description [The resulting bits are in MSB to LSB order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord ) +{ + int nBits, i; + assert( pWord[0] >= '1' && pWord[1] <= '9' ); + nBits = atoi(pWord); + // find the next symbol \' + while ( *pWord && *pWord != '\'' ) + pWord++; + if ( *pWord == 0 ) + { + sprintf( pMan->sError, "Cannot find symbol \' in the constant." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + assert( *pWord == '\'' ); + pWord++; + if ( *pWord != 'b' ) + { + sprintf( pMan->sError, "Currently can only handle binary constants." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + pWord++; + // scan the bits + Vec_PtrClear( pMan->vNames ); + for ( i = 0; i < nBits; i++ ) + { + if ( pWord[i] != '0' && pWord[i] != '1' ) + { + sprintf( pMan->sError, "Having problem parsing the binary constant." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') ); + } + return 1; +} + + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [The signals are added in the order from LSB to MSB.] + + SideEffects [] + + SeeAlso [] + ***********************************************************************/ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType ) { Ver_Stream_t * p = pMan->pReader; - char Buffer[1000]; - int Lower, Upper, i; - char * pWord; - char Symbol; - Lower = Upper = 0; + char Buffer[1000], Symbol, * pWord; + int nMsb, nLsb, Bit, Limit, i; + nMsb = nLsb = -1; while ( 1 ) { + // get the next word pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; @@ -539,38 +787,10 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp // check if the range is specified if ( pWord[0] == '[' && !pMan->fNameLast ) { - Lower = atoi( pWord + 1 ); - // find the splitter - while ( *pWord && *pWord != ':' && *pWord != ']' ) - pWord++; + assert( nMsb == -1 && nLsb == -1 ); + Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb ); + // check the case when there is space between bracket and the next word if ( *pWord == 0 ) - { - sprintf( pMan->sError, "Cannot find closing bracket in this line." ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - if ( *pWord == ']' ) - Upper = Lower; - else - { - Upper = atoi( pWord + 1 ); - if ( Lower > Upper ) - i = Lower, Lower = Upper, Upper = i; - // find the closing paranthesis - while ( *pWord && *pWord != ']' ) - pWord++; - if ( *pWord == 0 ) - { - sprintf( pMan->sError, "Cannot find closing bracket in this line." ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - assert( *pWord == ']' ); - } - // check the case of no space between bracket and the next word - if ( *(pWord+1) != 0 ) - pWord++; - else { // get the signal name pWord = Ver_ParseGetName( pMan ); @@ -580,7 +800,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp } // create signals - if ( Lower == 0 && Upper == 0 ) + if ( nMsb == -1 && nLsb == -1 ) { if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT ) Ver_ParseCreatePi( pNtk, pWord ); @@ -591,9 +811,14 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp } else { - for ( i = Lower; i <= Upper; i++ ) + assert( nMsb >= 0 && nLsb >= 0 ); + // add to the hash table + Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb ); + // add signals from Lsb to Msb + Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1; + for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 ) { - sprintf( Buffer, "%s[%d]", pWord, i ); + sprintf( Buffer, "%s[%d]", pWord, Bit ); if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT ) Ver_ParseCreatePi( pNtk, Buffer ); if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT ) @@ -823,12 +1048,14 @@ int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) ***********************************************************************/ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { + char Buffer[1000], Buffer2[1000]; Ver_Stream_t * p = pMan->pReader; Abc_Obj_t * pNode, * pNet; char * pWord, * pName, * pEquation; Hop_Obj_t * pFunc; char Symbol; - int i, Length, fReduction; + int i, Bit, Limit, Length, fReduction; + int nMsb, nLsb; // if ( Ver_StreamGetLineNumber(p) == 2756 ) // { @@ -845,102 +1072,171 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // consider the case of reduction operations - fReduction = 0; - if ( pWord[0] == '{' && !pMan->fNameLast ) - fReduction = 1; - if ( fReduction ) - { - pWord++; - pWord[strlen(pWord)-1] = 0; - assert( pWord[0] != '\\' ); - } - // get the fanout net - pNet = Ver_ParseFindNet( pNtk, pWord ); - if ( pNet == NULL ) - { - sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - // get the equality sign - if ( Ver_StreamPopChar(p) != '=' ) - { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - // skip the comments - if ( !Ver_ParseSkipComments( pMan ) ) + // check for vector-inputs + if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) ) return 0; - // get the second name - if ( fReduction ) - pEquation = Ver_StreamGetWord( p, ";" ); - else - pEquation = Ver_StreamGetWord( p, ",;" ); - if ( pEquation == NULL ) + // handle special case of constant assignment + if ( nMsb >= 0 && nLsb >= 0 ) { - sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + // save the fanout name + strcpy( Buffer, pWord ); + // get the equality sign + if ( Ver_StreamPopChar(p) != '=' ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // get the constant + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // check if it is indeed a constant + if ( !(pWord[0] >= '0' && pWord[0] <= '9') ) + { + sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } - // consider the case of mapped network - if ( pMan->fMapped ) - { - Vec_PtrClear( pMan->vNames ); - if ( !strcmp( pEquation, "1\'b0" ) ) - pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen()); - else if ( !strcmp( pEquation, "1\'b1" ) ) - pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); - else + // set individual bits of the constant + if ( !Ver_ParseConstant( pMan, pWord ) ) + return 0; + // check that the constant has the same size + Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1; + if ( Limit != Vec_PtrSize(pMan->vNames) ) + { + sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).", + Vec_PtrSize(pMan->vNames), Buffer, Limit ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // iterate through the bits + for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 ) { - if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) + // get the fanin net + if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) ) + pNet = Ver_ParseFindNet( pNtk, "1\'b1" ); + else + pNet = Ver_ParseFindNet( pNtk, "1\'b0" ); + assert( pNet != NULL ); + + // create the buffer + pNode = Abc_NtkCreateNodeBuf( pNtk, pNet ); + + // get the fanout net + sprintf( Buffer2, "%s[%d]", Buffer, Bit ); + pNet = Ver_ParseFindNet( pNtk, Buffer2 ); + if ( pNet == NULL ) { - sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) ); - Vec_PtrPush( pMan->vNames, pEquation ); - // get the buffer - pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen()); + Abc_ObjAddFanin( pNet, pNode ); } + // go to the end of the line + Ver_ParseSkipComments( pMan ); } else { - // parse the formula + // consider the case of reduction operations + fReduction = 0; + if ( pWord[0] == '{' && !pMan->fNameLast ) + fReduction = 1; if ( fReduction ) - pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); - else - pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); - if ( pFunc == NULL ) { + pWord++; + pWord[strlen(pWord)-1] = 0; + assert( pWord[0] != '\\' ); + } + // get the fanout net + pNet = Ver_ParseFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - } - - // create the node with the given inputs - pNode = Abc_NtkCreateNode( pNtk ); - pNode->pData = pFunc; - Abc_ObjAddFanin( pNet, pNode ); - // connect to fanin nets - for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) - { - // get the name of this signal - Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); - pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); - pName[Length] = 0; - // find the corresponding net - pNet = Ver_ParseFindNet( pNtk, pName ); - if ( pNet == NULL ) + // get the equality sign + if ( Ver_StreamPopChar(p) != '=' ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - Abc_ObjAddFanin( pNode, pNet ); + // skip the comments + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + // get the second name + if ( fReduction ) + pEquation = Ver_StreamGetWord( p, ";" ); + else + pEquation = Ver_StreamGetWord( p, ",;" ); + if ( pEquation == NULL ) + { + sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // consider the case of mapped network + if ( pMan->fMapped ) + { + Vec_PtrClear( pMan->vNames ); + if ( !strcmp( pEquation, "1\'b0" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen()); + else if ( !strcmp( pEquation, "1\'b1" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); + else + { + if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) + { + sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) ); + Vec_PtrPush( pMan->vNames, pEquation ); + // get the buffer + pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen()); + } + } + else + { + // parse the formula + if ( fReduction ) + pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); + else + pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); + if ( pFunc == NULL ) + { + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + + // create the node with the given inputs + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = pFunc; + Abc_ObjAddFanin( pNet, pNode ); + // connect to fanin nets + for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) + { + // get the name of this signal + Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); + pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); + pName[Length] = 0; + // find the corresponding net + pNet = Ver_ParseFindNet( pNtk, pName ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Abc_ObjAddFanin( pNode, pNet ); + } } Symbol = Ver_StreamPopChar(p); @@ -1229,19 +1525,21 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) ***********************************************************************/ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) { + char Buffer[1000]; Ver_Stream_t * p = pMan->pReader; - Vec_Ptr_t * vNetPairs; - Abc_Obj_t * pNetFormal, * pNetActual; + Ver_Bundle_t * pBundle; + Vec_Ptr_t * vBundles; + Abc_Obj_t * pNetActual; Abc_Obj_t * pNode; char * pWord, Symbol; - int fCompl; + int fCompl, fFormalIsGiven; - // parse the directive and set the pointers to the PIs/POs of the gate + // gate the name of the box pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // create box to represent this gate + // create a box with this name pNode = Abc_NtkCreateBlackbox( pNtk ); pNode->pData = pNtkBox; Abc_ObjAssignName( pNode, pWord, NULL ); @@ -1253,50 +1551,174 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) Ver_ParsePrintErrorMessage( pMan ); return 0; } - + Ver_ParseSkipComments( pMan ); + // parse pairs of formal/actural inputs - vNetPairs = Vec_PtrAlloc( 16 ); - pNode->pCopy = (Abc_Obj_t *)vNetPairs; + vBundles = Vec_PtrAlloc( 16 ); + pNode->pCopy = (Abc_Obj_t *)vBundles; while ( 1 ) { + // allocate the bundle (formal name + array of actual nets) + pBundle = ALLOC( Ver_Bundle_t, 1 ); + pBundle->pNameFormal = NULL; + pBundle->vNetsActual = Vec_PtrAlloc( 4 ); + Vec_PtrPush( vBundles, pBundle ); + // process one pair of formal/actual parameters - if ( Ver_StreamPopChar(p) != '.' ) + fFormalIsGiven = 0; + if ( Ver_StreamScanChar(p) == '.' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + fFormalIsGiven = 1; + if ( Ver_StreamPopChar(p) != '.' ) + { + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } - // parse the formal name - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - // get the formal net - pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord ); - Vec_PtrPush( vNetPairs, pNetFormal ); + // parse the formal name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; - // open the paranthesis - if ( Ver_StreamPopChar(p) != '(' ) - { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + // save the name + pBundle->pNameFormal = Extra_UtilStrsav( pWord ); + + // open the paranthesis + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); } - // parse the actual name - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - // consider the case of empty name - fCompl = 0; - if ( pWord[0] == 0 ) + // check if this is the beginning of {} expression + Symbol = Ver_StreamScanChar(p); + + // consider the case of vector-inputs + if ( Symbol == '{' ) { - // remove the formal net -// Vec_PtrPop( vNetPairs ); - pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + int i, k, Bit, Limit, nMsb, nLsb, fQuit; + + // skip this char + Ver_ParseSkipComments( pMan ); + Ver_StreamPopChar(p); + + // read actual names + i = 0; + fQuit = 0; + while ( 1 ) + { + // parse the formal name + Ver_ParseSkipComments( pMan ); + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + + // check if the last char is a closing brace + if ( pWord[strlen(pWord)-1] == '}' ) + { + pWord[strlen(pWord)-1] = 0; + fQuit = 1; + } + if ( pWord[0] == 0 ) + break; + + // check for constant + if ( pWord[0] >= '1' && pWord[0] <= '9' ) + { + if ( !Ver_ParseConstant( pMan, pWord ) ) + return 0; + // add constant MSB to LSB + for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ ) + { + // get the actual net + sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) ); + pNetActual = Ver_ParseFindNet( pNtk, Buffer ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + } + else + { + // get the suffix of the form [m:n] + if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast ) + Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb ); + else + Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ); + + // generate signals + if ( nMsb == -1 && nLsb == -1 ) + { + // get the actual net + pNetActual = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + i++; + } + else + { + // go from MSB to LSB + assert( nMsb >= 0 && nLsb >= 0 ); + Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1; + for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ ) + { + // get the actual net + sprintf( Buffer, "%s[%d]", pWord, Bit ); + pNetActual = Ver_ParseFindNet( pNtk, Buffer ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + } + } + + if ( fQuit ) + break; + + // skip comma + Ver_ParseSkipComments( pMan ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol == '}' ) + break; + if ( Symbol != ',' ) + { + sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } } else { + // get the next word + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // consider the case of empty name + fCompl = 0; + if ( pWord[0] == 0 ) + { + pNetActual = Abc_NtkCreateNet( pNtk ); + } + else + { /* // check if the name is complemented fCompl = (pWord[0] == '~'); @@ -1307,34 +1729,39 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNtk->pData = Extra_MmFlexStart(); } */ - // get the actual net - pNetActual = Ver_ParseFindNet( pNtk, pWord ); - if ( pNetActual == NULL ) - { - sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + // get the actual net + pNetActual = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } + Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } - Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) ); - // close the paranthesis - if ( Ver_StreamPopChar(p) != ')' ) + if ( fFormalIsGiven ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + // close the paranthesis + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ')' ) + { + sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); } // check if it is the end of gate - Ver_ParseSkipComments( pMan ); Symbol = Ver_StreamPopChar(p); if ( Symbol == ')' ) break; // skip comma if ( Symbol != ',' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); + sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -1353,6 +1780,24 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) return 1; } +/**Function************************************************************* + + Synopsis [Connects one box to the network] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParseFreeBundle( Ver_Bundle_t * pBundle ) +{ + FREE( pBundle->pNameFormal ); + Vec_PtrFree( pBundle->vNetsActual ); + free( pBundle ); +} + /**Function************************************************************* Synopsis [Connects one box to the network] @@ -1366,256 +1811,693 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) ***********************************************************************/ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) { - Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy; + Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy; Abc_Ntk_t * pNtk = pBox->pNtk; Abc_Ntk_t * pNtkBox = pBox->pData; - Abc_Obj_t * pNet, * pTerm, * pTermNew; - int i; + Abc_Obj_t * pTerm, * pTermNew, * pNetAct; + Ver_Bundle_t * pBundle; + char * pNameFormal; + int i, k, j, iBundle, Length; assert( !Ver_ObjIsConnected(pBox) ); assert( Ver_NtkIsDefined(pNtkBox) ); assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 ); - +/* // clean the PI/PO nets Abc_NtkForEachPi( pNtkBox, pTerm, i ) Abc_ObjFanout0(pTerm)->pCopy = NULL; Abc_NtkForEachPo( pNtkBox, pTerm, i ) Abc_ObjFanin0(pTerm)->pCopy = NULL; - - // map formal nets into actual nets - Vec_PtrForEachEntry( vNetPairs, pNet, i ) +*/ + // check if some of them do not have formal names + Vec_PtrForEachEntry( vBundles, pBundle, k ) + if ( pBundle->pNameFormal == NULL ) + break; + if ( k < Vec_PtrSize(vBundles) ) { - // get the actual net corresponding to this formal net (pNet) - pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i ); - // make sure the actual net is not complemented (otherwise need to use polarity) - assert( !Abc_ObjIsComplement(pNet->pCopy) ); + printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) ); + // add all actual nets in the bundles + iBundle = 0; + Vec_PtrForEachEntry( vBundles, pBundle, j ) + iBundle += Vec_PtrSize(pBundle->vNetsActual); + + // check the number of actual nets is the same as the number of formal nets + if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) ) + { + sprintf( pMan->sError, "The number of actual IOs (%d) is different from the number of formal IOs (%d) when instantiating network %s in box %s.", + Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // connect bundles in the natural order + iBundle = 0; + Abc_NtkForEachPi( pNtkBox, pTerm, i ) + { + pBundle = Vec_PtrEntry( vBundles, iBundle++ ); + // the bundle is found - add the connections - using order LSB to MSB + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k ) + { + pTermNew = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, pNetAct ); + i++; + } + i--; + } + // create fanins of the box + Abc_NtkForEachPo( pNtkBox, pTerm, i ) + { + pBundle = Vec_PtrEntry( vBundles, iBundle++ ); + // the bundle is found - add the connections - using order LSB to MSB + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k ) + { + pTermNew = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( pTermNew, pBox ); + Abc_ObjAddFanin( pNetAct, pTermNew ); + i++; + } + i--; + } + + // free the bundling + Vec_PtrForEachEntry( vBundles, pBundle, k ) + Ver_ParseFreeBundle( pBundle ); + Vec_PtrFree( vBundles ); + pBox->pCopy = NULL; + return 1; } - // make sure all PI nets are assigned + // bundles arrive in any order - but inside each bundle the order is MSB to LSB + // make sure every formal PI has a corresponding net Abc_NtkForEachPi( pNtkBox, pTerm, i ) { - if ( Abc_ObjFanout0(pTerm)->pCopy == NULL ) + // get the name of this formal net + pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) ); + // try to find the bundle with this formal net + pBundle = NULL; + Vec_PtrForEachEntry( vBundles, pBundle, k ) + if ( !strcmp(pBundle->pNameFormal, pNameFormal) ) + break; + assert( pBundle != NULL ); + // if the bundle is not found, try without parantheses + if ( k == Vec_PtrSize(vBundles) ) { - sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.", - Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + pBundle = NULL; + Length = strlen(pNameFormal); + if ( pNameFormal[Length-1] == ']' ) + { + // find the opening brace + for ( Length--; Length >= 0; Length-- ) + if ( pNameFormal[Length] == '[' ) + break; + // compare names before brace + if ( Length > 0 ) + { + Vec_PtrForEachEntry( vBundles, pBundle, j ) + if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) ) + break; + if ( j == Vec_PtrSize(vBundles) ) + pBundle = NULL; + } + } + if ( pBundle == NULL ) + { + sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.", + pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + // the bundle is found - add the connections - using order LSB to MSB + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k ) + { + pTermNew = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, pNetAct ); + i++; } - pTermNew = Abc_NtkCreateBi( pNtk ); - Abc_ObjAddFanin( pBox, pTermNew ); - Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy ); + i--; } - // create fanins of the box + // connect those formal POs that do have nets Abc_NtkForEachPo( pNtkBox, pTerm, i ) { - if ( Abc_ObjFanin0(pTerm)->pCopy == NULL ) - Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); - pTermNew = Abc_NtkCreateBo( pNtk ); - Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew ); - Abc_ObjAddFanin( pTermNew, pBox ); + // get the name of this PI + pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) ); + // try to find this formal net in the bundle + pBundle = NULL; + Vec_PtrForEachEntry( vBundles, pBundle, k ) + if ( !strcmp(pBundle->pNameFormal, pNameFormal) ) + break; + assert( pBundle != NULL ); + // if the name is not found, try without parantheses + if ( k == Vec_PtrSize(vBundles) ) + { + pBundle = NULL; + Length = strlen(pNameFormal); + if ( pNameFormal[Length-1] == ']' ) + { + // find the opening brace + for ( Length--; Length >= 0; Length-- ) + if ( pNameFormal[Length] == '[' ) + break; + // compare names before brace + if ( Length > 0 ) + { + Vec_PtrForEachEntry( vBundles, pBundle, j ) + if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) ) + break; + if ( j == Vec_PtrSize(vBundles) ) + pBundle = NULL; + } + } + if ( pBundle == NULL ) + { + printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", + pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); + continue; + } + } + // the bundle is found - add the connections + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k ) + { + if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") ) + { + sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.", + pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + pTermNew = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( pTermNew, pBox ); + Abc_ObjAddFanin( pNetAct, pTermNew ); + i++; + } + i--; } - // free the mapping - Vec_PtrFree( vNetPairs ); + // free the bundling + Vec_PtrForEachEntry( vBundles, pBundle, k ) + Ver_ParseFreeBundle( pBundle ); + Vec_PtrFree( vBundles ); pBox->pCopy = NULL; return 1; } + /**Function************************************************************* - Synopsis [Attaches the boxes to the network.] + Synopsis [Connects the defined boxes.] - Description [Makes sure that the undefined boxes are connected correctly.] + Description [Returns 2 if there are any undef boxes.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Vec_ParseAttachBoxes( Ver_Man_t * pMan ) +int Ver_ParseConnectDefBoxes( Ver_Man_t * pMan ) { - Abc_Ntk_t * pNtk, * pNtkBox; - Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots; - Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct; - int i, k, m, nBoxes; - - // connect defined boxes + Abc_Ntk_t * pNtk; + Abc_Obj_t * pBox; + int i, k, RetValue = 1; + // go through all the modules Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) { - Abc_NtkForEachBlackbox( pNtk, pBox, k ) + // go through all the boxes of this module + Abc_NtkForEachBox( pNtk, pBox, k ) { - if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) ) - if ( !Ver_ParseConnectBox( pMan, pBox ) ) - return 0; + if ( Abc_ObjIsLatch(pBox) ) + continue; + // skip internal boxes of the blackboxes + if ( pBox->pData == NULL ) + continue; + // if the network is undefined, it will be connected later + if ( !Ver_NtkIsDefined(pBox->pData) ) + { + RetValue = 2; + continue; + } + // connect the box + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + // if the network is a true blackbox, skip + if ( Abc_NtkHasBlackbox(pBox->pData) ) + continue; + // convert the box to the whitebox + Abc_ObjBlackboxToWhitebox( pBox ); } } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Collects the undef boxes and maps them into their instances.] + + Description [] + + SideEffects [] - // convert blackboxes to whiteboxes + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Ver_ParseCollectUndefBoxes( Ver_Man_t * pMan ) +{ + Vec_Ptr_t * vUndefs; + Abc_Ntk_t * pNtk, * pNtkBox; + Abc_Obj_t * pBox; + int i, k; + // clear the module structures + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + pNtk->pData = NULL; + // go through all the blackboxes + vUndefs = Vec_PtrAlloc( 16 ); Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { Abc_NtkForEachBlackbox( pNtk, pBox, k ) { pNtkBox = pBox->pData; if ( pNtkBox == NULL ) continue; - - if ( !strcmp( pNtkBox->pName, "ADDHX1" ) ) + if ( Ver_NtkIsDefined(pNtkBox) ) + continue; + if ( pNtkBox->pData == NULL ) { - int x = 0; + // save the box + Vec_PtrPush( vUndefs, pNtkBox ); + pNtkBox->pData = Vec_PtrAlloc( 16 ); } + // save the instance + Vec_PtrPush( pNtkBox->pData, pBox ); + } + } + return vUndefs; +} - if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) ) - Abc_ObjBlackboxToWhitebox( pBox ); - } +/**Function************************************************************* + Synopsis [Reports how many times each type of undefined box occurs.] - // search for undefined boxes - nBoxes = 0; - Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) - nBoxes += !Ver_NtkIsDefined(pNtk); - // quit if no undefined boxes are found - if ( nBoxes == 0 ) - return 1; + Description [] + + SideEffects [] - // count how many times each box occurs + SeeAlso [] + +***********************************************************************/ +void Ver_ParseReportUndefBoxes( Ver_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk; + Abc_Obj_t * pBox; + int i, k, nBoxes; + // clean + nBoxes = 0; Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) { - assert( pNtk->pData == NULL ); - pNtk->pData = NULL; + pNtk->fHiePath = 0; + if ( !Ver_NtkIsDefined(pNtk) ) + nBoxes++; } + // count Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) Abc_NtkForEachBlackbox( pNtk, pBox, k ) - { - if ( pBox->pData == NULL ) - continue; - pNtkBox = pBox->pData; - pNtkBox->pData = (void *)((int)pNtkBox->pData + 1); - } - - // print the boxes + if ( pBox->pData && !Ver_NtkIsDefined(pBox->pData) ) + ((Abc_Ntk_t *)pBox->pData)->fHiePath++; + // print the stats printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes ); Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) if ( !Ver_NtkIsDefined(pNtk) ) - printf( "%s (%d) ", Abc_NtkName(pNtk), (int)pNtk->pData ); + printf( "%s (%d) ", Abc_NtkName(pNtk), pNtk->fHiePath ); printf( "\n" ); - - // clean the boxes + // clean Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) - pNtk->pData = NULL; + pNtk->fHiePath = 0; +} +/**Function************************************************************* - // map actual nets into formal nets belonging to the undef boxes - vPivots = Vec_PtrAlloc( 100 ); - Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) - { - Abc_NtkForEachBlackbox( pNtk, pBox, k ) - { - if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) ) - continue; - vNetPairs = (Vec_Ptr_t *)pBox->pCopy; - Vec_PtrForEachEntry( vNetPairs, pNet, m ) - { - pNetAct = Vec_PtrEntry( vNetPairs, ++m ); - // skip already driven nets and constants - if ( Abc_ObjFaninNum(pNetAct) == 1 ) - continue; - if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant - continue; - // add this net - if ( pNetAct->pData == NULL ) + Synopsis [Returns 1 if there are non-driven nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs ) +{ + Abc_Ntk_t * pNtk; + Ver_Bundle_t * pBundle; + Abc_Obj_t * pBox, * pNet; + int i, k, j, m; + // go through undef box types + Vec_PtrForEachEntry( vUndefs, pNtk, i ) + // go through instances of this type + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + // go through the bundles of this instance + Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) + // go through the actual nets of this bundle + if ( pBundle ) + Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m ) { - pNetAct->pData = Vec_PtrAlloc( 16 ); - Vec_PtrPush( vPivots, pNetAct ); + char * pName = Abc_ObjName(pNet); + if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven + if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const + return 1; } - vEnvoys = pNetAct->pData; - Vec_PtrPush( vEnvoys, pNet ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Checks if formal nets with the given name are driven in any of the instances of undef boxes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal ) +{ + Ver_Bundle_t * pBundle; + Abc_Obj_t * pBox, * pNet; + int k, j, m; + // go through instances of this type + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + { + // find a bundle with the given name in this instance + Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) + if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) ) + break; + // skip non-driven bundles + if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) ) + continue; + // check if all nets are driven in this bundle + Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m ) + if ( Abc_ObjFaninNum(pNet) > 0 ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns the non-driven bundle that is given distance from the end.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ver_Bundle_t * Ver_ParseGetNondrivenBundle( Abc_Ntk_t * pNtk, int Counter ) +{ + Ver_Bundle_t * pBundle; + Abc_Obj_t * pBox, * pNet; + int k, m; + // go through instances of this type + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + { + if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) ) + continue; + // get the bundle given distance away + pBundle = Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter ); + if ( pBundle == NULL ) + continue; + // go through the actual nets of this bundle + Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m ) + if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven + return pBundle; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Drives the bundle in the given undef box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 ) +{ + char Buffer[200]; + char * pName; + Ver_Bundle_t * pBundle; + Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal; + int k, j, m; + + // drive this net in the undef box + Vec_PtrForEachEntry( pBundle0->vNetsActual, pNetAct, m ) + { + // create the formal net + if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 ) + sprintf( Buffer, "%s", pBundle0->pNameFormal ); + else + sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m ); + assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL ); + pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer ); + // connect it to the box + pTerm = Abc_NtkCreateBo( pNtk ); + assert( Abc_NtkBoxNum(pNtk) <= 1 ); + pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk); + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal ); + Abc_ObjAddFanin( pNetFormal, pTerm ); + Abc_ObjAddFanin( pTerm, pBox ); + } + + // go through instances of this type + pName = Extra_UtilStrsav(pBundle0->pNameFormal); + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + { + // find a bundle with the given name in this instance + Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) + if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) ) + break; + // skip non-driven bundles + if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) ) + continue; + // check if any nets are driven in this bundle + Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m ) + if ( Abc_ObjFaninNum(pNetAct) > 0 ) + { + sprintf( pMan->sError, "Internal error while trying to connect undefined boxes. It is likely that the algorithm currently used has its limitations." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } + // drive the nets by the undef box + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m ) + { + pTermNew = Abc_NtkCreateBo( pNetAct->pNtk ); + Abc_ObjAddFanin( pTermNew, pBox ); + Abc_ObjAddFanin( pNetAct, pTermNew ); } + // remove the bundle + Ver_ParseFreeBundle( pBundle ); + Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL ); } + free( pName ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Drives the bundle in the given undef box.] + + Description [] + + SideEffects [] + + SeeAlso [] - // for each pivot net, find the driver - Vec_PtrForEachEntry( vPivots, pNetAct, i ) +***********************************************************************/ +int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs ) +{ + char Buffer[200]; + Ver_Bundle_t * pBundle; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct; + int i, k, j, m, CountCur, CountTotal = -1; + // iterate through the undef boxes + Vec_PtrForEachEntry( vUndefs, pNtk, i ) { - char * pName = Abc_ObjName(pNetAct); -/* - if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) ) + // count the number of unconnected bundles for instances of this type of box + CountTotal = -1; + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) { - int x = 0; + CountCur = 0; + Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) + CountCur += (pBundle != NULL); + if ( CountTotal == -1 ) + CountTotal = CountCur; + else if ( CountTotal != CountCur ) + { + sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.", + CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } -*/ - assert( Abc_ObjFaninNum(pNetAct) == 0 ); - assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") ); - vEnvoys = pNetAct->pData; pNetAct->pData = NULL; - // find the driver starting from the last nets - pNetDr = NULL; - for ( m = 0; m < 64; m++ ) + + // create formals + pBox = Vec_PtrEntry( pNtk->pData, 0 ); + Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) { - Vec_PtrForEachEntry( vEnvoys, pNet, k ) + if ( pBundle == NULL ) + continue; + Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m ) { - if ( Abc_ObjId(pNet) == 0 ) + // find create the formal net + if ( Vec_PtrSize(pBundle->vNetsActual) == 1 ) + sprintf( Buffer, "%s", pBundle->pNameFormal ); + else + sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m ); + assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL ); + pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer ); + // connect + pTerm = Abc_NtkCreateBi( pNtk ); + assert( Abc_NtkBoxNum(pNtk) <= 1 ); + pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk); + Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) ); + Abc_ObjAddFanin( pTerm, pNetFormal ); + Abc_ObjAddFanin( pBox2, pTerm ); + } + } + + // go through all the boxes + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + { + // go through all the bundles + Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j ) + { + if ( pBundle == NULL ) continue; - if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m ) + // drive the nets by the undef box + Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m ) { - pNetDr = pNet; - break; + pTermNew = Abc_NtkCreateBi( pNetAct->pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, pNetAct ); } + // remove the bundle + Ver_ParseFreeBundle( pBundle ); + Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL ); } - if ( pNetDr ) - break; + + // free the bundles + Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy ); + pBox->pCopy = NULL; } - assert( pNetDr != NULL ); - Vec_PtrWriteEntry( vPivots, i, pNetDr ); - Vec_PtrFree( vEnvoys ); } + return 1; +} - // for each pivot net, create driver - Vec_PtrForEachEntry( vPivots, pNetDr, i ) - { - if ( pNetDr == NULL ) - continue; - assert( Abc_ObjFaninNum(pNetDr) <= 1 ); - if ( Abc_ObjFaninNum(pNetDr) == 1 ) - continue; - // drive this net with the box - pTerm = Abc_NtkCreateBo( pNetDr->pNtk ); - assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 ); - pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk); - Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr ); - Abc_ObjAddFanin( pNetDr, pTerm ); - Abc_ObjAddFanin( pTerm, pBox ); - } - Vec_PtrFree( vPivots ); - // connect the remaining boxes - Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) +/**Function************************************************************* + + Synopsis [Returns the max size of any undef box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs ) +{ + Abc_Ntk_t * pNtk; + Abc_Obj_t * pBox; + int i, k, nMaxSize = 0; + // go through undef box types + Vec_PtrForEachEntry( vUndefs, pNtk, i ) + // go through instances of this type + Vec_PtrForEachEntry( pNtk->pData, pBox, k ) + // check the number of bundles of this instance + if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) ) + nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy); + return nMaxSize; +} + + +/**Function************************************************************* + + Synopsis [Attaches the boxes to the network.] + + Description [This procedure is called after the design is parsed. + At that point, all the defined models have their PIs present. + They are connected first. Next undef boxes are processed (if present). + Iteratively, one bundle is selected to be driven by the undef boxes in such + a way that there is no conflict (if it is driven by an instance of the box, + no other net will be driven twice by the same formal net of some other instance + of the same box). In the end, all the remaining nets that cannot be driven + by the undef boxes are connected to the undef boxes as inputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseAttachBoxes( Ver_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk; + Ver_Bundle_t * pBundle; + Vec_Ptr_t * vUndefs; + int i, RetValue, Counter, nMaxBoxSize; + + // connect defined boxes + RetValue = Ver_ParseConnectDefBoxes( pMan ); + if ( RetValue < 2 ) + return RetValue; + + // report the boxes + Ver_ParseReportUndefBoxes( pMan ); + + // collect undef box types and their actual instances + vUndefs = Ver_ParseCollectUndefBoxes( pMan ); + assert( Vec_PtrSize( vUndefs ) > 0 ); + + // go through all undef box types + Counter = 0; + nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs ); + while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize ) { - if ( Abc_NtkPiNum(pNtk) ) - continue; - Abc_NtkForEachNet( pNtk, pNet, k ) + // go through undef box types + pBundle = NULL; + Vec_PtrForEachEntry( vUndefs, pNtk, i ) + if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) ) + break; + if ( pBundle == NULL ) { - if ( Abc_ObjFaninNum(pNet) ) - continue; - // drive this net - pTerm = Abc_NtkCreateBi( pNet->pNtk ); - assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 ); - pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk); - Abc_ObjAddFanin( pBox, pTerm ); - Abc_ObjAddFanin( pTerm, pNet ); - Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) ); + Counter++; + continue; } + // drive this bundle by this box + if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) ) + return 0; } - // connect the remaining boxes - Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + // make all the remaining bundles the drivers of undefs + if ( !Ver_ParseDriveInputs( pMan, vUndefs ) ) + return 0; + + // cleanup + Vec_PtrForEachEntry( vUndefs, pNtk, i ) { - Abc_NtkForEachBlackbox( pNtk, pBox, k ) - { - char * pName = Abc_ObjName(pBox); - if ( !Ver_ObjIsConnected(pBox) ) - if ( !Ver_ParseConnectBox( pMan, pBox ) ) - return 0; - } + Vec_PtrFree( pNtk->pData ); + pNtk->pData = NULL; } + Vec_PtrFree( vUndefs ); return 1; } @@ -1716,55 +2598,12 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ) { Abc_Obj_t * pObj; pObj = Abc_NtkCreateNodeInv( pNtk, pNet ); - pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + pNet = Abc_NtkCreateNet( pNtk ); Abc_ObjAddFanin( pNet, pObj ); return pNet; } - -/* - // allocate memory to remember the phase - pPolarity = NULL; - if ( fComplUsed ) - { - int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) ); - pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes ); - memset( pPolarity, 0, nBytes ); - } - // create box to represent this gate - if ( Abc_NtkHasBlackbox(pNtkBox) ) - pNode = Abc_NtkCreateBlackbox( pNtk ); - else - pNode = Abc_NtkCreateWhitebox( pNtk ); - pNode->pNext = (Abc_Obj_t *)pPolarity; - pNode->pData = pNtkBox; - // connect to fanin nets - Abc_NtkForEachPi( pNtkBox, pObj, i ) - { - if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) - { - Abc_InfoSetBit( pPolarity, i ); - pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); - } - assert( !Abc_ObjIsComplement(pObj->pCopy) ); -// Abc_ObjAddFanin( pNode, pObj->pCopy ); - pTerm = Abc_NtkCreateBi( pNtk ); - Abc_ObjAddFanin( pTerm, pObj->pCopy ); - Abc_ObjAddFanin( pNode, pTerm ); - } - // connect to fanout nets - Abc_NtkForEachPo( pNtkBox, pObj, i ) - { - if ( pObj->pCopy == NULL ) - pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL); -// Abc_ObjAddFanin( pObj->pCopy, pNode ); - pTerm = Abc_NtkCreateBo( pNtk ); - Abc_ObjAddFanin( pTerm, pNode ); - Abc_ObjAddFanin( pObj->pCopy, pTerm ); - } -*/ - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip new file mode 100644 index 00000000..481f7e6a Binary files /dev/null and b/src/base/ver/verCore.zip differ diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c index 253754ae..19a2c523 100644 --- a/src/base/ver/verFormula.c +++ b/src/base/ver/verFormula.c @@ -120,7 +120,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_ case '\r': case '\n': continue; - +/* // treat Constant 0 as a variable case VER_PARSE_SYM_CONST0: Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( Hop_ManConst0(pMan) ); @@ -144,7 +144,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_ } Flag = VER_PARSE_FLAG_VAR; break; - +*/ case VER_PARSE_SYM_NEGBEF1: case VER_PARSE_SYM_NEGBEF2: if ( Flag == VER_PARSE_FLAG_VAR ) -- cgit v1.2.3