luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Deriving equivalent nets from proved equivalences.

This commit is contained in:
Alan Mishchenko 2020-12-09 21:59:49 -10:00
parent 5b8e56b2e5
commit 901560bb23
1 changed files with 28 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/base/abci/abcDress2.c
View File

@ -21,6 +21,7 @@
#include "base/abc/abc.h" #include "base/abc/abc.h"
#include "aig/aig/aig.h" #include "aig/aig/aig.h"
#include "proof/dch/dch.h" #include "proof/dch/dch.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
@ -272,6 +273,32 @@ Vec_Ptr_t * Abc_NtkDressMapIds( Aig_Man_t * pMiter, Abc_Ntk_t * pNtk1, Abc_Ntk_t
return vRes; return vRes;
} }
/**Function*************************************************************
Synopsis [Alternative way to compute equivalences.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ComputeEquivalences2( Aig_Man_t * pMiter, Dch_Pars_t * pPars )
{
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Gia_Man_t * pGia = Gia_ManFromAigSimple(pMiter);
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, pPars->nBTLimit, pPars->fVerbose );
int i, k;
ABC_FREE( pMiter->pReprs );
pMiter->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMiter) );
Gia_ManForEachClass( pGia, i )
Gia_ClassForEachObj1( pGia, i, k )
pMiter->pReprs[k] = Aig_ManObj( pMiter, i );
Gia_ManStop( pGia );
Gia_ManStop( pNew );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes equivalence classes of objects in pNtk1 and pNtk2.] Synopsis [Computes equivalence classes of objects in pNtk1 and pNtk2.]
@ -307,7 +334,7 @@ Vec_Ptr_t * Abc_NtkDressComputeEquivs( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int
pPars->nBTLimit = nConflictLimit; pPars->nBTLimit = nConflictLimit;
pPars->fVerbose = fVerbose; pPars->fVerbose = fVerbose;
// perform SAT sweeping // perform SAT sweeping
Dch_ComputeEquivalences( pMiter, pPars ); Dch_ComputeEquivalences2( pMiter, pPars );
// now, pMiter is annotated with the equivl class info // now, pMiter is annotated with the equivl class info
// convert this info into the resulting array // convert this info into the resulting array
vRes = Abc_NtkDressMapIds( pMiter, pNtk1, pNtk2 ); vRes = Abc_NtkDressMapIds( pMiter, pNtk1, pNtk2 );