From bfe7333f4105442a7df530c68ed1cf1b7da7edda Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 21 Jul 2016 16:40:56 -0700 Subject: Adding new command 'dump_equiv'. --- src/base/abc/abcFunc.c | 11 +- src/base/abci/abc.c | 79 +++++++++++++- src/base/abci/abcDress3.c | 259 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 4 files changed, 343 insertions(+), 7 deletions(-) create mode 100644 src/base/abci/abcDress3.c (limited to 'src/base') diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index b44a272a..5d0261d7 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -980,7 +980,7 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple ) Vec_Int_t * vMapping = NULL; Vec_Ptr_t * vNodes; Abc_Obj_t * pNode, * pFanin; - int i, k, nObjs; + int i, k, nObjs, iGiaObj; assert( Abc_NtkIsAigLogic(p) ); pHopMan = (Hop_Man_t *)p->pManFunc; // create new manager @@ -1016,15 +1016,14 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple ) { assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) ); Abc_ConvertAigToGia( pNew, pHopObj ); - if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) ) - continue; - if ( vMapping && !Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) ) + iGiaObj = Abc_Lit2Var( pHopObj->iData ); + if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) ) { - Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) ); + Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) ); Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) ); Abc_ObjForEachFanin( pNode, pFanin, k ) Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) ); - Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) ); + Vec_IntPush( vMapping, iGiaObj ); } } pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ebd6c368..f19f8449 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -233,6 +233,7 @@ static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDumpEquiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRecStart3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRecStop3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -869,6 +870,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 ); + Cmd_CommandAdd( pAbc, "Fraiging", "dump_equiv", Abc_CommandDumpEquiv, 0 ); Cmd_CommandAdd( pAbc, "Choicing", "rec_start3", Abc_CommandRecStart3, 0 ); Cmd_CommandAdd( pAbc, "Choicing", "rec_stop3", Abc_CommandRecStop3, 0 ); @@ -14801,6 +14803,81 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose ); + FILE * pFile = NULL; + Abc_Ntk_t * pNtks[2] = {NULL}; + char * pFileName[2], * pFileNameOut; + int c, nConfs = 1000, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfs < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 3 ) + { + Abc_Print( -1, "Expecting three file names on the command line.\n" ); + goto usage; + } + pFileName[0] = argv[globalUtilOptind]; + pFileName[1] = argv[globalUtilOptind+1]; + pFileNameOut = argv[globalUtilOptind+2]; + for ( c = 0; c < 2; c++ ) + { + pNtks[c] = Io_Read( pFileName[c], Io_ReadFileType(pFileName[c]), 1, 0 ); + if ( pNtks[c] == NULL ) + goto usage; + Abc_NtkToAig( pNtks[c] ); + } + Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fVerbose ); + Abc_NtkDelete( pNtks[0] ); + Abc_NtkDelete( pNtks[1] ); + return 0; + +usage: + Abc_Print( -2, "usage: dump_equiv [-C num] [-vh] \n" ); + Abc_Print( -2, "\t computes equivalence classes of nodes in and \n" ); + Abc_Print( -2, "\t-C num : the maximum number of conflicts at each node [default = %d]\n", nConfs ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : first network whose nodes are considered\n" ); + Abc_Print( -2, "\t : second network whose nodes are considered\n" ); + Abc_Print( -2, "\t : text file with node equivalence classes\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -27022,7 +27099,7 @@ usage: Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" ); Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" ); Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" ); - Abc_Print( -2, "\t-c : toggles allowing simple GIA to be improved [default = %s]\n", fGiaSimple? "yes": "no" ); + Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" ); Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" ); Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" ); Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c new file mode 100644 index 00000000..ee7eb8e3 --- /dev/null +++ b/src/base/abci/abcDress3.c @@ -0,0 +1,259 @@ +/**CFile**************************************************************** + + FileName [abcDress3.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Transfers names from one netlist to the other.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcDress3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "base/abc/abc.h" +#include "base/io/ioAbc.h" +#include "proof/cec/cec.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Compute equivalence classes of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose ) +{ + Gia_Man_t * pTemp; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec_ManFraSetDefaultParams( pPars ); + pPars->fUseOrigIds = 1; + pPars->fSatSweeping = 1; + pPars->nBTLimit = nConfs; + pPars->fVerbose = fVerbose; + pTemp = Cec_ManSatSweeping( pGia, pPars, 0 ); + Gia_ManStop( pTemp ); + pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv ); + Gia_ManStop( pTemp ); +} + +/**Function************************************************************* + + Synopsis [Add logic from pNtk to the AIG manager p.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk ) +{ + extern int Abc_ConvertAigToGia( Gia_Man_t * p, Hop_Obj_t * pRoot ); + Hop_Man_t * pHopMan; + Hop_Obj_t * pHopObj; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode, * pFanin; + int i, k; + assert( Abc_NtkIsAigLogic(pNtk) ); + pHopMan = (Hop_Man_t *)pNtk->pManFunc; + Hop_ManConst1(pHopMan)->iData = 1; + // image primary inputs + Abc_NtkCleanCopy( pNtk ); + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->iTemp = Gia_ManCiLit(p, i); + // iterate through nodes used in the mapping + vNodes = Abc_NtkDfs( pNtk, 0 ); + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp; + pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData ); + assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) ); + if ( Hop_DagSize(pHopObj) > 0 ) + Abc_ConvertAigToGia( p, pHopObj ); + pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) ); + } + Vec_PtrFree( vNodes ); + // create primary outputs + Abc_NtkForEachCo( pNtk, pNode, i ) + Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp ); +} +Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +{ + Gia_Man_t * p; + Gia_Obj_t * pObj; + Abc_Obj_t * pNode; + int i; + assert( Abc_NtkIsAigLogic(pNtk1) ); + assert( Abc_NtkIsAigLogic(pNtk2) ); + // create new manager + p = Gia_ManStart( 10000 ); + p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) ); + p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) ); + Abc_NtkForEachCi( pNtk1, pNode, i ) + Gia_ManAppendCi(p); + // add logic + Gia_ManHashAlloc( p ); + Abc_NtkAigToGiaOne( p, pNtk1 ); + Abc_NtkAigToGiaOne( p, pNtk2 ); + Gia_ManHashStop( p ); + // add extra POs to dangling nodes + Gia_ManCreateValueRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + if ( pObj->Value == 0 ) + Gia_ManAppendCo( p, Abc_Var2Lit(i, 0) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Collect equivalence class information.] + + Description [Each class is represented as follows: + ... + where is nodeId with 1-bit for complement and 1-bit for network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_NtkCollectAddOne( int iNtk, int iObj, int iGiaLit, Gia_Man_t * pGia, Vec_Int_t * vGia2Cla, Vec_Int_t * vNexts[2] ) +{ + int iRepr = Gia_ObjReprSelf( pGia, Abc_Lit2Var(iGiaLit) ); + int Compl = Abc_LitIsCompl(iGiaLit) ^ Gia_ObjPhase(Gia_ManObj(pGia, iRepr)) ^ Gia_ObjPhase(Gia_ManObj(pGia, Abc_Lit2Var(iGiaLit))); + int Added = Abc_Var2Lit( Abc_Var2Lit(iObj, Compl), iNtk ); + int Entry = Vec_IntEntry( vGia2Cla, iRepr ); + Vec_IntWriteEntry( vNexts[iNtk], iObj, Entry ); + Vec_IntWriteEntry( vGia2Cla, iRepr, Added ); +} +Vec_Int_t * Abc_NtkCollectEquivClasses( Abc_Ntk_t * pNtks[2], Gia_Man_t * pGia ) +{ + Vec_Int_t * vClass = Vec_IntAlloc( 100 ); + Vec_Int_t * vClasses = Vec_IntAlloc( 1000 ); + Vec_Int_t * vGia2Cla = Vec_IntStartFull( Gia_ManObjNum(pGia) ); // mapping objId into classId + Vec_Int_t * vNexts[2] = { Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[0])), Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[1])) }; + Abc_Obj_t * pObj; + int n, i, k, Entry, fCompl; + Abc_NtkForEachCi( pNtks[0], pObj, i ) + Abc_NtkCollectAddOne( 0, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts ); + for ( n = 0; n < 2; n++ ) + Abc_NtkForEachNode( pNtks[n], pObj, i ) + Abc_NtkCollectAddOne( n, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts ); + Vec_IntForEachEntry( vGia2Cla, Entry, i ) + { + Vec_IntClear( vClass ); + for ( ; Entry >= 0; Entry = Vec_IntEntry(vNexts[Entry&1], Entry>>2) ) + Vec_IntPush( vClass, Entry ); + if ( Vec_IntSize(vClass) < 2 ) + continue; + Vec_IntReverseOrder( vClass ); + fCompl = 2 & Vec_IntEntry( vClass, 0 ); + Vec_IntForEachEntry( vClass, Entry, k ) + Vec_IntWriteEntry( vClass, k, Entry ^ fCompl ); + Vec_IntPush( vClasses, Vec_IntSize(vClass) ); + Vec_IntAppend( vClasses, vClass ); + } + Vec_IntFree( vGia2Cla ); + Vec_IntFree( vNexts[0] ); + Vec_IntFree( vNexts[1] ); + Vec_IntFree( vClass ); + return vClasses; +} + +/**Function************************************************************* + + Synopsis [Write the output file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * pNtks[2] ) +{ + int i, c, k, Entry; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { printf( "Cannot open file %s for writing.\n", pFileName ); return; } + fprintf( pFile, "# Node equivalences computed by ABC for networks \"%s\" and \"%s\" on %s\n\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), Extra_TimeStamp() ); + for ( i = c = 0; i < Vec_IntSize(vClasses); c++, i += 1 + Vec_IntEntry(vClasses, i) ) + { + Vec_IntForEachEntryStartStop( vClasses, Entry, k, i + 1, i + 1 + Vec_IntEntry(vClasses, i) ) + { + Abc_Ntk_t * pNtk = pNtks[Entry & 1]; + char * pObjName = Abc_ObjName( Abc_NtkObj(pNtk, Entry>>2) ); + fprintf( pFile, "%d:%s:%s%s\n", c+1, Abc_NtkName(pNtk), (Entry&2) ? "NOT:":"", pObjName ); + } + fprintf( pFile, "\n" ); + } + fclose( pFile ); +} + + +/**Function************************************************************* + + Synopsis [Compute and dump equivalent name classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose ) +{ + //abctime clk = Abc_Clock(); + Vec_Int_t * vClasses; + // derive shared AIG for the two networks + Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1] ); + if ( fVerbose ) + printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs ); + // compute equivalences in this AIG + Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose ); + //if ( fVerbose ) + // Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk ); + if ( fVerbose ) + Gia_ManPrintStats( pGia, NULL ); + // collect equivalence class information + vClasses = Abc_NtkCollectEquivClasses( pNtks, pGia ); + Gia_ManStop( pGia ); + // dump information into the output file + Abc_NtkDumpEquivFile( pFileName, vClasses, pNtks ); + Vec_IntFree( vClasses ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 492fc62a..b97f526f 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -15,6 +15,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDetect.c \ src/base/abci/abcDress.c \ src/base/abci/abcDress2.c \ + src/base/abci/abcDress3.c \ src/base/abci/abcDsd.c \ src/base/abci/abcExact.c \ src/base/abci/abcExtract.c \ -- cgit v1.2.3