| /**CFile**************************************************************** |
| |
| FileName [abcScorr.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Signal correspondence testing procedures.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: abcScorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "base/io/ioAbc.h" |
| #include "aig/saig/saig.h" |
| #include "proof/ssw/ssw.h" |
| #include "aig/gia/gia.h" |
| #include "proof/cec/cec.h" |
| #include "aig/gia/giaAig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Tst_Dat_t_ Tst_Dat_t; |
| struct Tst_Dat_t_ |
| { |
| Abc_Ntk_t * pNetlist; |
| Aig_Man_t * pAig; |
| Gia_Man_t * pGia; |
| Vec_Int_t * vId2Name; |
| char * pFileNameOut; |
| int fFlopOnly; |
| int fFfNdOnly; |
| int fDumpBmc; |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Abc_NtkMapGiaIntoNameId( Abc_Ntk_t * pNetlist, Aig_Man_t * pAig, Gia_Man_t * pGia ) |
| { |
| Vec_Int_t * vId2Name; |
| Abc_Obj_t * pNet, * pNode, * pAnd; |
| Aig_Obj_t * pObjAig; |
| int i; |
| vId2Name = Vec_IntAlloc( 0 ); |
| Vec_IntFill( vId2Name, pGia ? Gia_ManObjNum(pGia) : Aig_ManObjNumMax(pAig), ~0 ); |
| // copy all names |
| Abc_NtkForEachNet( pNetlist, pNet, i ) |
| { |
| pNode = Abc_ObjFanin0(pNet)->pCopy; |
| if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && |
| (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && |
| Aig_ObjType(pObjAig) != AIG_OBJ_NONE ) |
| { |
| if ( pGia == NULL ) |
| Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) ); |
| else |
| Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) ); |
| } |
| } |
| // overwrite CO names |
| Abc_NtkForEachCo( pNetlist, pNode, i ) |
| { |
| pNet = Abc_ObjFanin0(pNode); |
| pNode = pNode->pCopy; |
| if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && |
| (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && |
| Aig_ObjType(pObjAig) != AIG_OBJ_NONE ) |
| { |
| if ( pGia == NULL ) |
| Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) ); |
| else |
| Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) ); |
| } |
| } |
| // overwrite CI names |
| Abc_NtkForEachCi( pNetlist, pNode, i ) |
| { |
| pNet = Abc_ObjFanout0(pNode); |
| pNode = pNode->pCopy; |
| if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && |
| (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && |
| Aig_ObjType(pObjAig) != AIG_OBJ_NONE ) |
| { |
| if ( pGia == NULL ) |
| Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) ); |
| else |
| Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) ); |
| } |
| } |
| return vId2Name; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| char * Abc_NtkTestScorrGetName( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id ) |
| { |
| // Abc_Obj_t * pObj; |
| //printf( "trying to get name for %d\n", Id ); |
| if ( Vec_IntEntry(vId2Name, Id) == ~0 ) |
| return NULL; |
| // pObj = Abc_NtkObj( pNetlist, Vec_IntEntry(vId2Name, Id) ); |
| // pObj = Abc_ObjFanin0(pObj); |
| // assert( Abc_ObjIsCi(pObj) ); |
| return Nm_ManFindNameById( pNetlist->pManName, Vec_IntEntry(vId2Name, Id) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkTestScorrWriteEquivPair( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id1, int Id2, FILE * pFile, int fPol ) |
| { |
| char * pName1 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id1 ); |
| char * pName2 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id2 ); |
| if ( pName1 == NULL || pName2 == NULL ) |
| return 0; |
| fprintf( pFile, "%s=%s%s\n", pName1, fPol? "~": "", pName2 ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkTestScorrWriteEquivConst( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id1, FILE * pFile, int fPol ) |
| { |
| char * pName1 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id1 ); |
| if ( pName1 == NULL ) |
| return 0; |
| fprintf( pFile, "%s=%s%s\n", pName1, fPol? "~": "", "const0" ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| char * Abc_NtkBmcFileName( char * pName ) |
| { |
| static char Buffer[1000]; |
| char * pNameGeneric = Extra_FileNameGeneric( pName ); |
| sprintf( Buffer, "%s_bmc%s", pNameGeneric, pName + strlen(pNameGeneric) ); |
| ABC_FREE( pNameGeneric ); |
| return Buffer; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkTestScorrWriteEquivGia( Tst_Dat_t * pData ) |
| { |
| Abc_Ntk_t * pNetlist = pData->pNetlist; |
| Vec_Int_t * vId2Name = pData->vId2Name; |
| Gia_Man_t * pGia = pData->pGia; |
| char * pFileNameOut = pData->pFileNameOut; |
| FILE * pFile; |
| Gia_Obj_t * pObj, * pRepr; |
| int i, Counter = 0; |
| if ( pData->fDumpBmc ) |
| { |
| pData->fDumpBmc = 0; |
| pFileNameOut = Abc_NtkBmcFileName( pFileNameOut ); |
| } |
| pFile = fopen( pFileNameOut, "wb" ); |
| Gia_ManSetPhase( pGia ); |
| Gia_ManForEachObj( pGia, pObj, i ) |
| { |
| if ( !Gia_ObjHasRepr(pGia, i) ) |
| continue; |
| pRepr = Gia_ManObj( pGia,Gia_ObjRepr(pGia, i) ); |
| if ( pData->fFlopOnly ) |
| { |
| if ( !Gia_ObjIsRo(pGia, pObj) || !(Gia_ObjIsRo(pGia, pRepr)||Gia_ObjIsConst0(pRepr)) ) |
| continue; |
| } |
| else if ( pData->fFfNdOnly ) |
| { |
| if ( !Gia_ObjIsRo(pGia, pObj) && !(Gia_ObjIsRo(pGia, pRepr)||Gia_ObjIsConst0(pRepr)) ) |
| continue; |
| } |
| if ( Gia_ObjRepr(pGia, i) == 0 ) |
| Counter += Abc_NtkTestScorrWriteEquivConst( pNetlist, vId2Name, i, pFile, Gia_ObjPhase(pObj) ); |
| else |
| Counter += Abc_NtkTestScorrWriteEquivPair( pNetlist, vId2Name, Gia_ObjRepr(pGia, i), i, pFile, |
| Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); |
| } |
| fclose( pFile ); |
| printf( "%d pairs of sequentially equivalent nodes are written into file \"%s\".\n", Counter, pFileNameOut ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkTestScorrWriteEquivAig( Tst_Dat_t * pData ) |
| { |
| Abc_Ntk_t * pNetlist = pData->pNetlist; |
| Vec_Int_t * vId2Name = pData->vId2Name; |
| Aig_Man_t * pAig = pData->pAig; |
| char * pFileNameOut = pData->pFileNameOut; |
| FILE * pFile; |
| Aig_Obj_t * pObj, * pRepr; |
| int i, Counter = 0; |
| if ( pData->fDumpBmc ) |
| { |
| pData->fDumpBmc = 0; |
| pFileNameOut = Abc_NtkBmcFileName( pFileNameOut ); |
| } |
| pFile = fopen( pFileNameOut, "wb" ); |
| Aig_ManForEachObj( pAig, pObj, i ) |
| { |
| if ( (pRepr = Aig_ObjRepr(pAig, pObj)) == NULL ) |
| continue; |
| if ( pData->fFlopOnly ) |
| { |
| if ( !Saig_ObjIsLo(pAig, pObj) || !(Saig_ObjIsLo(pAig, pRepr)||pRepr==Aig_ManConst1(pAig)) ) |
| continue; |
| } |
| else if ( pData->fFfNdOnly ) |
| { |
| if ( !Saig_ObjIsLo(pAig, pObj) && !(Saig_ObjIsLo(pAig, pRepr)||pRepr==Aig_ManConst1(pAig)) ) |
| continue; |
| } |
| if ( pRepr == Aig_ManConst1(pAig) ) |
| Counter += Abc_NtkTestScorrWriteEquivConst( pNetlist, vId2Name, Aig_ObjId(pObj), pFile, Aig_ObjPhase(pObj) ); |
| else |
| Counter += Abc_NtkTestScorrWriteEquivPair( pNetlist, vId2Name, Aig_ObjId(pRepr), Aig_ObjId(pObj), pFile, |
| Aig_ObjPhase(pRepr) ^ Aig_ObjPhase(pObj) ); |
| } |
| fclose( pFile ); |
| printf( "%d pairs of sequentially equivalent nodes are written into file \"%s\".\n", Counter, pFileNameOut ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkTestScorr( char * pFileNameIn, char * pFileNameOut, int nStepsMax, int nBTLimit, int fNewAlgo, int fFlopOnly, int fFfNdOnly, int fVerbose ) |
| { |
| extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); |
| extern Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); |
| |
| FILE * pFile; |
| Tst_Dat_t Data, * pData = &Data; |
| Vec_Int_t * vId2Name; |
| Abc_Ntk_t * pNetlist, * pLogic, * pStrash, * pResult; |
| Aig_Man_t * pAig, * pTempAig; |
| Gia_Man_t * pGia, * pTempGia; |
| // int Counter = 0; |
| // check the files |
| pFile = fopen( pFileNameIn, "rb" ); |
| if ( pFile == NULL ) |
| { |
| printf( "Input file \"%s\" cannot be opened.\n", pFileNameIn ); |
| return NULL; |
| } |
| fclose( pFile ); |
| // check the files |
| pFile = fopen( pFileNameOut, "wb" ); |
| if ( pFile == NULL ) |
| { |
| printf( "Output file \"%s\" cannot be opened.\n", pFileNameOut ); |
| return NULL; |
| } |
| fclose( pFile ); |
| // derive AIG for signal correspondence |
| pNetlist = Io_ReadNetlist( pFileNameIn, Io_ReadFileType(pFileNameIn), 1 ); |
| if ( pNetlist == NULL ) |
| { |
| printf( "Reading input file \"%s\" has failed.\n", pFileNameIn ); |
| return NULL; |
| } |
| pLogic = Abc_NtkToLogic( pNetlist ); |
| if ( pLogic == NULL ) |
| { |
| Abc_NtkDelete( pNetlist ); |
| printf( "Deriving logic network from input file %s has failed.\n", pFileNameIn ); |
| return NULL; |
| } |
| if ( Extra_FileIsType( pFileNameIn, ".bench", ".BENCH", NULL ) ) |
| { |
| // get the init file name |
| char * pFileNameInit = Extra_FileNameGenericAppend( pLogic->pSpec, ".init" ); |
| pFile = fopen( pFileNameInit, "rb" ); |
| if ( pFile == NULL ) |
| { |
| printf( "Init file \"%s\" cannot be opened.\n", pFileNameInit ); |
| return NULL; |
| } |
| Io_ReadBenchInit( pLogic, pFileNameInit ); |
| Abc_NtkConvertDcLatches( pLogic ); |
| if ( fVerbose ) |
| printf( "Initial state was derived from file \"%s\".\n", pFileNameInit ); |
| } |
| pStrash = Abc_NtkStrash( pLogic, 0, 1, 0 ); |
| if ( pStrash == NULL ) |
| { |
| Abc_NtkDelete( pLogic ); |
| Abc_NtkDelete( pNetlist ); |
| printf( "Deriving strashed network from input file %s has failed.\n", pFileNameIn ); |
| return NULL; |
| } |
| pAig = Abc_NtkToDar( pStrash, 0, 1 ); // performs "zero" internally |
| // the newer computation (&scorr) |
| if ( fNewAlgo ) |
| { |
| Cec_ParCor_t CorPars, * pCorPars = &CorPars; |
| Cec_ManCorSetDefaultParams( pCorPars ); |
| pCorPars->nBTLimit = nBTLimit; |
| pCorPars->nStepsMax = nStepsMax; |
| pCorPars->fVerbose = fVerbose; |
| pCorPars->fUseCSat = 1; |
| pGia = Gia_ManFromAig( pAig ); |
| // prepare the data-structure |
| memset( pData, 0, sizeof(Tst_Dat_t) ); |
| pData->pNetlist = pNetlist; |
| pData->pAig = NULL; |
| pData->pGia = pGia; |
| pData->vId2Name = vId2Name = Abc_NtkMapGiaIntoNameId( pNetlist, pAig, pGia ); |
| pData->pFileNameOut = pFileNameOut; |
| pData->fFlopOnly = fFlopOnly; |
| pData->fFfNdOnly = fFfNdOnly; |
| pData->fDumpBmc = 1; |
| pCorPars->pData = pData; |
| pCorPars->pFunc = (void *)Abc_NtkTestScorrWriteEquivGia; |
| // call signal correspondence |
| pTempGia = Cec_ManLSCorrespondence( pGia, pCorPars ); |
| pTempAig = Gia_ManToAigSimple( pTempGia ); |
| Gia_ManStop( pTempGia ); |
| Gia_ManStop( pGia ); |
| } |
| // the older computation (scorr) |
| else |
| { |
| Ssw_Pars_t SswPars, * pSswPars = &SswPars; |
| Ssw_ManSetDefaultParams( pSswPars ); |
| pSswPars->nBTLimit = nBTLimit; |
| pSswPars->nStepsMax = nStepsMax; |
| pSswPars->fVerbose = fVerbose; |
| // preSswPare the data-structure |
| memset( pData, 0, sizeof(Tst_Dat_t) ); |
| pData->pNetlist = pNetlist; |
| pData->pAig = pAig; |
| pData->pGia = NULL; |
| pData->vId2Name = vId2Name = Abc_NtkMapGiaIntoNameId( pNetlist, pAig, NULL ); |
| pData->pFileNameOut = pFileNameOut; |
| pData->fFlopOnly = fFlopOnly; |
| pData->fFfNdOnly = fFfNdOnly; |
| pData->fDumpBmc = 1; |
| pSswPars->pData = pData; |
| pSswPars->pFunc = (void *)Abc_NtkTestScorrWriteEquivAig; |
| // call signal correspondence |
| pTempAig = Ssw_SignalCorrespondence( pAig, pSswPars ); |
| } |
| // create the resulting AIG |
| pResult = Abc_NtkFromDarSeqSweep( pStrash, pTempAig ); |
| // cleanup |
| Vec_IntFree( vId2Name ); |
| Aig_ManStop( pAig ); |
| Aig_ManStop( pTempAig ); |
| Abc_NtkDelete( pStrash ); |
| Abc_NtkDelete( pLogic ); |
| Abc_NtkDelete( pNetlist ); |
| return pResult; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
