diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-08-23 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-08-23 08:01:00 -0700 |
commit | 7b09d2d28aa81916f9c06f0993f2569a7ad18596 (patch) | |
tree | 7f9203d4a804fb4db2ae5d962166470360b1f27f /src/temp | |
parent | 956842d9cc321eee3907889b820132e6e2b5ec62 (diff) | |
download | abc-7b09d2d28aa81916f9c06f0993f2569a7ad18596.tar.gz abc-7b09d2d28aa81916f9c06f0993f2569a7ad18596.tar.bz2 abc-7b09d2d28aa81916f9c06f0993f2569a7ad18596.zip |
Version abc60823
Diffstat (limited to 'src/temp')
-rw-r--r-- | src/temp/aig/aig.h | 4 | ||||
-rw-r--r-- | src/temp/aig/aigUtil.c | 173 | ||||
-rw-r--r-- | src/temp/ver/ver.h | 7 | ||||
-rw-r--r-- | src/temp/ver/verCore.c | 157 | ||||
-rw-r--r-- | src/temp/ver/verFormula.c | 53 |
5 files changed, 336 insertions, 58 deletions
diff --git a/src/temp/aig/aig.h b/src/temp/aig/aig.h index e3e35b0c..e489d978 100644 --- a/src/temp/aig/aig.h +++ b/src/temp/aig/aig.h @@ -290,9 +290,11 @@ extern void Aig_TableProfile( Aig_Man_t * p ); /*=== aigUtil.c =========================================================*/ extern void Aig_ManIncrementTravId( Aig_Man_t * p ); extern void Aig_ManCleanData( Aig_Man_t * p ); -extern int Aig_ObjMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode ); +extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper ); extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj ); +extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 ); extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE ); +extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ); extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); diff --git a/src/temp/aig/aigUtil.c b/src/temp/aig/aigUtil.c index eb93cba1..99966e7d 100644 --- a/src/temp/aig/aigUtil.c +++ b/src/temp/aig/aigUtil.c @@ -73,6 +73,46 @@ void Aig_ManCleanData( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Detects multi-input gate rooted at this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) ) + { + Vec_PtrPushUnique(vSuper, pObj); + return; + } + Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper ); + Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper ); +} + +/**Function************************************************************* + + Synopsis [Detects multi-input gate rooted at this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper ) +{ + assert( !Aig_IsComplement(pRoot) ); + Vec_PtrClear( vSuper ); + Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper ); +} + +/**Function************************************************************* + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] Description [] @@ -106,6 +146,48 @@ int Aig_ObjIsMuxType( Aig_Obj_t * pNode ) (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1))); } + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are inputs of the EXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 ) +{ + Aig_Obj_t * p0, * p1; + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) ) + return 0; + if ( Aig_ObjIsExor(pObj) ) + { + *ppFan0 = Aig_ObjChild0(pObj); + *ppFan1 = Aig_ObjChild1(pObj); + return 1; + } + assert( Aig_ObjIsAnd(pObj) ); + p0 = Aig_ObjChild0(pObj); + p1 = Aig_ObjChild1(pObj); + if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) ) + return 0; + p0 = Aig_Regular(p0); + p1 = Aig_Regular(p1); + if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) ) + return 0; + if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) ) + return 0; + if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) ) + return 0; + *ppFan0 = Aig_ObjChild0(p0); + *ppFan1 = Aig_ObjChild1(p0); + return 1; +} + /**Function************************************************************* Synopsis [Recognizes what nodes are control and data inputs of a MUX.] @@ -198,6 +280,95 @@ Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Ob return NULL; } + +/**Function************************************************************* + + Synopsis [Prints Verilog formula for the AIG rooted at this node.] + + Description [The formula is in terms of PIs, which should have + their names assigned in pObj->pData fields.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ) +{ + Vec_Ptr_t * vSuper; + Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC; + int fCompl, i; + // store the complemented attribute + fCompl = Aig_IsComplement(pObj); + pObj = Aig_Regular(pObj); + // constant case + if ( Aig_ObjIsConst1(pObj) ) + { + fprintf( pFile, "%d", !fCompl ); + return; + } + // PI case + if ( Aig_ObjIsPi(pObj) ) + { + fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData ); + return; + } + // EXOR case + if ( Aig_ObjIsExor(pObj) ) + { + Vec_VecExpand( vLevels, Level ); + vSuper = Vec_VecEntry( vLevels, Level ); + Aig_ObjCollectMulti( pObj, vSuper ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 ); + if ( i < Vec_PtrSize(vSuper) - 1 ) + fprintf( pFile, " ^ " ); + } + fprintf( pFile, "%s", (Level==0? "" : ")") ); + return; + } + // MUX case + if ( Aig_ObjIsMuxType(pObj) ) + { + if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) ) + { + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 ); + fprintf( pFile, " ^ " ); + Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 ); + fprintf( pFile, "%s", (Level==0? "" : ")") ); + } + else + { + pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 ); + fprintf( pFile, " ? " ); + Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 ); + fprintf( pFile, " : " ); + Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 ); + fprintf( pFile, "%s", (Level==0? "" : ")") ); + } + return; + } + // AND case + Vec_VecExpand( vLevels, Level ); + vSuper = Vec_VecEntry(vLevels, Level); + Aig_ObjCollectMulti( pObj, vSuper ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 ); + if ( i < Vec_PtrSize(vSuper) - 1 ) + fprintf( pFile, " %s ", fCompl? "|" : "&" ); + } + fprintf( pFile, "%s", (Level==0? "" : ")") ); + return; +} + + /**Function************************************************************* Synopsis [Prints node in HAIG.] @@ -250,6 +421,8 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ) printf( "\n" ); } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h index 3e351840..c7c18f79 100644 --- a/src/temp/ver/ver.h +++ b/src/temp/ver/ver.h @@ -52,7 +52,9 @@ struct Ver_Man_t_ // current network and library Abc_Ntk_t * pNtkCur; // the network under construction Abc_Lib_t * pDesign; // the current design - Abc_Lib_t * pGateLib; // the current technology library + // parameters + int fUseMemMan; // allocate memory manager in the networks + int fCheck; // checks network for currectness // error recovery FILE * Output; int fTopLevel; @@ -77,10 +79,11 @@ struct Ver_Man_t_ //////////////////////////////////////////////////////////////////////// /*=== verCore.c ========================================================*/ -extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck ); +extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ); extern void Ver_ParsePrintErrorMessage( Ver_Man_t * p ); /*=== verFormula.c ========================================================*/ extern void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ); +extern void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage ); /*=== verParse.c ========================================================*/ extern int Ver_ParseSkipComments( Ver_Man_t * p ); extern char * Ver_ParseGetName( Ver_Man_t * p ); diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c index e868c4e3..99311c98 100644 --- a/src/temp/ver/verCore.c +++ b/src/temp/ver/verCore.c @@ -37,7 +37,7 @@ typedef enum { static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ); static void Ver_ParseStop( Ver_Man_t * p ); static void Ver_ParseFreeData( Ver_Man_t * p ); -static void Ver_ParseInternal( Ver_Man_t * p, int fCheck ); +static void Ver_ParseInternal( Ver_Man_t * p ); static int Ver_ParseModule( Ver_Man_t * p ); static int Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType ); static int Ver_ParseAssign( Ver_Man_t * p ); @@ -64,14 +64,16 @@ static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * SeeAlso [] ***********************************************************************/ -Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck ) +Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ) { Ver_Man_t * p; Abc_Lib_t * pDesign; // start the parser p = Ver_ParseStart( pFileName, pGateLib ); + p->fCheck = fCheck; + p->fUseMemMan = fUseMemMan; // parse the file - Ver_ParseInternal( p, fCheck ); + Ver_ParseInternal( p ); // save the result pDesign = p->pDesign; p->pDesign = NULL; @@ -98,13 +100,14 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) memset( p, 0, sizeof(Ver_Man_t) ); p->pFileName = pFileName; p->pReader = Ver_StreamAlloc( pFileName ); - p->pDesign = Abc_LibCreate( pFileName ); - p->pGateLib = pGateLib; p->Output = stdout; p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) ); p->vNames = Vec_PtrAlloc( 100 ); p->vStackFn = Vec_PtrAlloc( 100 ); p->vStackOp = Vec_IntAlloc( 100 ); + // create the design library and assign the technology library + p->pDesign = Abc_LibCreate( pFileName ); + p->pDesign->pLibrary = pGateLib; return p; } @@ -141,7 +144,7 @@ void Ver_ParseStop( Ver_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) +void Ver_ParseInternal( Ver_Man_t * pMan ) { char * pToken; while ( 1 ) @@ -162,7 +165,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) return; // check the network for correctness - if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) ) + if ( pMan->fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) ) { pMan->fTopLevel = 1; sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName ); @@ -177,6 +180,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) Ver_ParsePrintErrorMessage( pMan ); return; } + Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur ); st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur ); pMan->pNtkCur = NULL; } @@ -253,23 +257,19 @@ int Ver_ParseModule( Ver_Man_t * pMan ) // start the current network assert( pMan->pNtkCur == NULL ); - pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX ); - - pNtk->ntkFunc = ABC_FUNC_AIG; - assert( pNtk->pManFunc == NULL ); + pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan ); + pNtk->ntkFunc = ABC_FUNC_AIG; pNtk->pManFunc = pMan->pDesign->pManFunc; // get the network name pWord = Ver_ParseGetName( pMan ); pNtk->pName = Extra_UtilStrsav( pWord ); pNtk->pSpec = NULL; -/* - // create constant nodes and nets - pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); - Abc_ObjAddFanin( pNet, xxxx AigAbc_AigConst1(pNtk) ); - pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); - Abc_ObjAddFanin( pNet, Abc_AigConst1(pNtk) ); -*/ + + // create constant nets + Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); + Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); + // make sure we stopped at the opening paranthesis if ( Ver_StreamScanChar(p) != '(' ) { @@ -281,6 +281,7 @@ int Ver_ParseModule( Ver_Man_t * pMan ) // skip to the end of parantheses while ( 1 ) { + Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); Ver_StreamSkipToChars( p, ",/)" ); while ( Ver_StreamScanChar(p) == '/' ) { @@ -299,6 +300,7 @@ int Ver_ParseModule( Ver_Man_t * pMan ) // parse the inputs/outputs/registers/wires/inouts while ( 1 ) { + Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; @@ -329,12 +331,8 @@ int Ver_ParseModule( Ver_Man_t * pMan ) else if ( !strcmp( pWord, "initial" ) ) RetValue = Ver_ParseInitial( pMan ); else if ( !strcmp( pWord, "endmodule" ) ) - { - // if nothing is known, set the functionality to be black box - Abc_NtkFinalizeRead( pNtk ); break; - } - else if ( pMan->pGateLib && st_lookup(pMan->pGateLib->tModules, pWord, (char**)&pNtkTemp) ) // gate library + else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library RetValue = Ver_ParseGate( pMan, pNtkTemp ); else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design RetValue = Ver_ParseGate( pMan, pNtkTemp ); @@ -355,6 +353,22 @@ int Ver_ParseModule( Ver_Man_t * pMan ) if ( pWord == NULL ) return 0; } + + // check if constant 0 net is used + pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else + Abc_ObjAddFanin( pNet, Abc_NodeCreateConst0(pNtk) ); + // check if constant 1 net is used + pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); + if ( Abc_ObjFanoutNum(pNet) == 0 ) + Abc_NtkDeleteObj(pNet); + else + Abc_ObjAddFanin( pNet, Abc_NodeCreateConst1(pNtk) ); + + // fix the dangling nets + Abc_NtkFinalizeRead( pNtk ); return 1; } @@ -415,29 +429,46 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) Abc_Ntk_t * pNtk = pMan->pNtkCur; Abc_Obj_t * pNode, * pNet; char * pWord, * pName, * pEquation; - DdNode * bFunc; + Aig_Obj_t * pFunc; char Symbol; - int i, Length; + int i, Length, fReduction; // convert from the mapped netlist into the BDD netlist if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) { - pNtk->ntkFunc = ABC_FUNC_BDD; - pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + pNtk->ntkFunc = ABC_FUNC_AIG; + assert( pNtk->pManFunc == NULL ); + pNtk->pManFunc = pMan->pDesign->pManFunc; } - else if ( pNtk->ntkFunc != ABC_FUNC_BDD ) + else if ( pNtk->ntkFunc != ABC_FUNC_AIG ) { sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + while ( 1 ) { // get the name of the output signal pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; + // consider the case of reduction operations + fReduction = (pWord[0] == '{'); + if ( fReduction ) + { + pWord++; + pWord[strlen(pWord)-1] = 0; + } + // get the fanout net + pNet = Abc_NtkFindNet( 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 fanout net pNet = Abc_NtkFindNet( pNtk, pWord ); if ( pNet == NULL ) @@ -457,21 +488,27 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - pEquation = Ver_StreamGetWord( p, ",;" ); + if ( fReduction ) + pEquation = Ver_StreamGetWord( p, ";" ); + else + pEquation = Ver_StreamGetWord( p, ",;" ); if ( pEquation == NULL ) return 0; // parse the formula - bFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); - if ( bFunc == NULL ) + 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; } - Cudd_Ref( bFunc ); + // create the node with the given inputs pNode = Abc_NtkCreateNode( pMan->pNtkCur ); - pNode->pData = bFunc; + pNode->pData = pFunc; Abc_ObjAddFanin( pNet, pNode ); // connect to fanin nets for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) @@ -677,20 +714,8 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) Abc_Obj_t * pNetFormal, * pNetActual; Abc_Obj_t * pObj, * pNode; char * pWord, Symbol; - int i, fCompl; - - // convert from the mapped netlist into the BDD netlist - if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) - { - pNtk->ntkFunc = ABC_FUNC_MAP; - pNtk->pManFunc = pMan->pGateLib; - } - else if ( pNtk->ntkFunc != ABC_FUNC_MAP ) - { - sprintf( pMan->sError, "The network %s appears to contain both mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + int i, fCompl, fComplUsed = 0; + unsigned * pPolarity; // clean the PI/PO pointers Abc_NtkForEachPi( pNtkGate, pObj, i ) @@ -750,7 +775,12 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) // check if the name is complemented fCompl = (pWord[0] == '~'); if ( fCompl ) + { + fComplUsed = 1; pWord++; + if ( pMan->pNtkCur->pData == NULL ) + pMan->pNtkCur->pData = Extra_MmFlexStart(); + } // get the actual net pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord ); if ( pNetActual == NULL ) @@ -769,8 +799,8 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) } // process the pair - if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net - Abc_ObjFanin0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl ); + if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net (with polarity!) + Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl ); else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) ) // P0 net { assert( fCompl == 0 ); @@ -825,17 +855,38 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) return 0; } */ - // create a new node - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); + + // allocate memory to remember the phase + pPolarity = NULL; + if ( fComplUsed ) + { + int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) ); + pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes ); + memset( pPolarity, 0, nBytes ); + } + // create box to represent this gate + pNode = Abc_NtkCreateBox( pMan->pNtkCur ); + pNode->pNext = (Abc_Obj_t *)pPolarity; + pNode->pData = pNtkGate; // connect to fanin nets Abc_NtkForEachPi( pNtkGate, 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 ); + } // connect to fanout nets Abc_NtkForEachPo( pNtkGate, pObj, i ) + { if ( pObj->pCopy ) Abc_ObjAddFanin( pObj->pCopy, pNode ); - // set the functionality - pNode->pData = pNtkGate; + else + Abc_ObjAddFanin( Abc_NtkFindOrCreateNet(pNtk, NULL), pNode ); + } return 1; } diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c index cfeb3e5f..2c2881c0 100644 --- a/src/temp/ver/verFormula.c +++ b/src/temp/ver/verFormula.c @@ -277,7 +277,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_ break; } Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one - if ( Oper2 >= Oper1 ) + if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) ) { // if Oper2 precedence is higher or equal, execute it if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL ) { @@ -378,7 +378,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ) int nLength, nLength2, i; // find the end of the string delimited by other characters pTemp = pString; - while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && + while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && @@ -402,6 +402,55 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ) return i; } +/**Function************************************************************* + + Synopsis [Returns the AIG representation of the reduction formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage ) +{ + Aig_Obj_t * pRes; + int v, fCompl; + char Symbol; + + // get the operation + Symbol = *pFormula++; + fCompl = ( Symbol == '~' ); + if ( fCompl ) + Symbol = *pFormula++; + // check the operation + if ( Symbol != '&' && Symbol != '|' && Symbol != '^' ) + { + sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol ); + return NULL; + } + // skip the brace + while ( *pFormula++ != '{' ); + // parse the names + Vec_PtrClear( vNames ); + while ( *pFormula != '}' ) + { + v = Ver_FormulaParserFindVar( pFormula, vNames ); + pFormula += (int)Vec_PtrEntry( vNames, 2*v ); + while ( *pFormula == ' ' || *pFormula == ',' ) + pFormula++; + } + // compute the function + if ( Symbol == '&' ) + pRes = Aig_CreateAnd( pMan, Vec_PtrSize(vNames)/2 ); + else if ( Symbol == '|' ) + pRes = Aig_CreateOr( pMan, Vec_PtrSize(vNames)/2 ); + else if ( Symbol == '^' ) + pRes = Aig_CreateExor( pMan, Vec_PtrSize(vNames)/2 ); + return Aig_NotCond( pRes, fCompl ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |