diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 22:58:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 22:58:23 -0700 |
| commit | cfa7be1a07e3102195b2395f379f50e556dbf4e3 (patch) | |
| tree | a53bddabc1d9554eae9d03cb6f6363c5edd2d478 /src/opt | |
| parent | 38e577f5dfeb30379c0f97c246b4cc9428ba3db3 (diff) | |
| download | abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.tar.gz abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.tar.bz2 abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.zip | |
Integrating synthesis into the new BMC engine.
Diffstat (limited to 'src/opt')
| -rw-r--r-- | src/opt/dau/dau.h | 2 | ||||
| -rw-r--r-- | src/opt/dau/dauGia.c | 19 |
2 files changed, 16 insertions, 5 deletions
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index a928fecf..92641b71 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -89,7 +89,7 @@ extern int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ); /*=== dauGia.c ==========================================================*/ extern int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover ); -extern void * Dsm_ManDeriveGia( void * p ); +extern void * Dsm_ManDeriveGia( void * p, int fUseMuxes ); /*=== dauMerge.c ==========================================================*/ extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c index a714f622..2712effc 100644 --- a/src/opt/dau/dauGia.c +++ b/src/opt/dau/dauGia.c @@ -68,7 +68,10 @@ int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVa return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars ); t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars ); t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); - return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 ); + if ( pGia->pMuxes ) + return Gia_ManHashMuxReal( pGia, pFanins[nVars], t1, t0 ); + else + return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 ); } /**Function************************************************************* @@ -110,7 +113,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, for ( (*p)++; *p < q; (*p)++ ) { Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); - Res = Gia_ManHashXor( pGia, Res, Lit ); + if ( pGia->pMuxes ) + Res = Gia_ManHashXorReal( pGia, Res, Lit ); + else + Res = Gia_ManHashXor( pGia, Res, Lit ); } assert( *p == q ); return Abc_LitNotCond( Res, fCompl ); @@ -156,7 +162,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, assert( **p == '{' && *q == '}' ); *p = q; } - Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] ); + if ( pGia->pMuxes ) + Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] ); + else + Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] ); return Abc_LitNotCond( Res, fCompl ); } if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) @@ -250,7 +259,7 @@ void Dsm_ManReportStats() SeeAlso [] ***********************************************************************/ -void * Dsm_ManDeriveGia( void * pGia ) +void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes ) { Gia_Man_t * p = (Gia_Man_t *)pGia; Gia_Man_t * pNew, * pTemp; @@ -263,6 +272,8 @@ void * Dsm_ManDeriveGia( void * pGia ) pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + if ( fUseMuxes ) + pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc ); // map primary inputs Gia_ManFillValue(p); Gia_ManConst0(p)->Value = 0; |