From b949436f4c99157397e16b23c3693fb5a99bd557 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 Jul 2015 16:49:06 -0700 Subject: Adding new Python API 'is_func_iso'. --- src/base/abc/abc.h | 1 + src/base/abc/abcDfs.c | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/proof/cec/cec.h | 1 + src/proof/cec/cecCec.c | 21 ++++++++++++ src/python/pyabc.i | 14 ++++++++ 5 files changed, 129 insertions(+) (limited to 'src') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e4136810..ae7c02a5 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -626,6 +626,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsWithBoxes( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); extern ABC_DLL Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo ); +extern ABC_DLL int Abc_NtkFunctionalIso( Abc_Ntk_t * pNtk, int iCo1, int iCo2 ); extern ABC_DLL Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos ); extern ABC_DLL Vec_Ptr_t * Abc_AigDfsMap( Abc_Ntk_t * pNtk ); extern ABC_DLL Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, int fTfi ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 8017ce95..9bca1e64 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abc.h" +#include "proof/cec/cec.h" ABC_NAMESPACE_IMPL_START @@ -955,6 +956,97 @@ Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo ) return vNodes; } +/**Function************************************************************* + + Synopsis [Derives GIA comparing two outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFunctionalIsoGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) +{ + int iLit0, iLit1; + if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 ) + return pNode->iTemp; + assert( Abc_ObjIsNode( pNode ) ); + Abc_NodeSetTravIdCurrent( pNode ); + iLit0 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit1 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin1(pNode) ); + iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); + iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); + return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1)); +} +Gia_Man_t * Abc_NtkFunctionalIsoGia( Abc_Ntk_t * pNtk, int iCo1, int iCo2 ) +{ + Gia_Man_t * pNew = NULL, * pTemp; + Vec_Int_t * vSupp1 = Abc_NtkNodeSupportInt( pNtk, iCo1 ); + Vec_Int_t * vSupp2 = Abc_NtkNodeSupportInt( pNtk, iCo2 ); + if ( Vec_IntSize(vSupp1) == Vec_IntSize(vSupp2) ) + { + Abc_Obj_t * pObj; + int i, iCi, iLit1, iLit2; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pNtk->pName ); + pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); + Gia_ManHashStart( pNew ); + // primary inputs + Abc_AigConst1(pNtk)->iTemp = 1; + Vec_IntForEachEntry( vSupp1, iCi, i ) + Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManAppendCi(pNew); + // create the first cone + Abc_NtkIncrementTravId( pNtk ); + pObj = Abc_NtkCo( pNtk, iCo1 ); + iLit1 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pObj) ); + iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC0(pObj) ); + // primary inputs + Vec_IntForEachEntry( vSupp2, iCi, i ) + Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManCiLit(pNew, i); + // create the second cone + Abc_NtkIncrementTravId( pNtk ); + pObj = Abc_NtkCo( pNtk, iCo2 ); + iLit2 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pObj) ); + iLit2 = Abc_LitNotCond( iLit2, Abc_ObjFaninC0(pObj) ); + Gia_ManAppendCo( pNew, iLit1 ); + Gia_ManAppendCo( pNew, iLit2 ); + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + } + Vec_IntFree( vSupp1 ); + Vec_IntFree( vSupp2 ); + return pNew; +} +int Abc_NtkFunctionalIsoInt( Abc_Ntk_t * pNtk, int iCo1, int iCo2 ) +{ + Gia_Man_t * pGia; int Value; + assert( Abc_NtkIsStrash(pNtk) ); + if ( iCo1 < 0 || iCo1 >= Abc_NtkCoNum(pNtk) ) + return 0; + if ( iCo2 < 0 || iCo2 >= Abc_NtkCoNum(pNtk) ) + return 0; + pGia = Abc_NtkFunctionalIsoGia( pNtk, iCo1, iCo2 ); + if ( pGia == NULL ) + return 0; + Value = Cec_ManVerifySimple( pGia ); + Gia_ManStop( pGia ); + return (int)(Value == 1); +} +int Abc_NtkFunctionalIso( Abc_Ntk_t * pNtk, int iCo1, int iCo2 ) +{ + Abc_Ntk_t * pNtkNew; int Result; + if ( Abc_NtkIsStrash(pNtk) ) + return Abc_NtkFunctionalIsoInt( pNtk, iCo1, iCo2 ); + pNtkNew = Abc_NtkStrash( pNtk, 0, 0, 0 ); + Result = Abc_NtkFunctionalIsoInt( pNtkNew, iCo1, iCo2 ); + Abc_NtkDelete( pNtkNew ); + return Result; +} + + /**Function************************************************************* Synopsis [Computes support size of the node.] diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 805a5d73..a0b92b52 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -197,6 +197,7 @@ struct Cec_ParSeq_t_ /*=== cecCec.c ==========================================================*/ extern int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ); extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ); +extern int Cec_ManVerifySimple( Gia_Man_t * p ); /*=== cecChoice.c ==========================================================*/ extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ); /*=== cecCorr.c ==========================================================*/ diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index 1465a721..77a6ed4a 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -413,6 +413,27 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) return RetValue; } +/**Function************************************************************* + + Synopsis [Simple SAT run to check equivalence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifySimple( Gia_Man_t * p ) +{ + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Cec_ManCecSetDefaultParams( pPars ); + pPars->fSilent = 1; + assert( Gia_ManCoNum(p) == 2 ); + assert( Gia_ManRegNum(p) == 0 ); + return Cec_ManVerify( p, pPars ); +} + /**Function************************************************************* Synopsis [New CEC engine applied to two circuits.] diff --git a/src/python/pyabc.i b/src/python/pyabc.i index 208235a4..e3bad4bc 100644 --- a/src/python/pyabc.i +++ b/src/python/pyabc.i @@ -384,6 +384,19 @@ PyObject* co_supp( int iCo ) return co_supp; } +int is_func_iso( int iCo1, int iCo2 ) +{ + Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + + if ( !pNtk ) + { + return 0; + } + + return Abc_NtkFunctionalIso( pNtk, iCo1, iCo2 ); +} + void _pyabc_array_clear() { Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); @@ -741,6 +754,7 @@ int _cex_get_frame(Abc_Cex_t* pCex); PyObject* eq_classes(); PyObject* co_supp(int iCo); +int is_func_iso(int iCo1, int iCo2); void _pyabc_array_clear(); void _pyabc_array_push(int i); -- cgit v1.2.3