From 940cf7f98b6de040cb984b1d9ee356a232647648 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 27 Sep 2013 13:30:36 -0700 Subject: Generation of plain AIG after mapping. --- abclib.dsp | 4 + src/aig/gia/gia.h | 1 + src/aig/gia/giaJf.c | 82 +++++++++++++++++- src/base/abci/abc.c | 11 ++- src/opt/dau/dau.h | 3 + src/opt/dau/dauDsd.c | 2 +- src/opt/dau/dauGia.c | 225 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/dau/module.make | 1 + 8 files changed, 323 insertions(+), 6 deletions(-) create mode 100644 src/opt/dau/dauGia.c diff --git a/abclib.dsp b/abclib.dsp index 9efdb000..848b2c8a 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -2071,6 +2071,10 @@ SOURCE=.\src\opt\dau\dauEnum.c # End Source File # Begin Source File +SOURCE=.\src\opt\dau\dauGia.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\dau\dauInt.h # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5a6148d0..eef8675f 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -248,6 +248,7 @@ struct Jf_Par_t_ int fCutMin; int fUseTts; int fGenCnf; + int fPureAig; int fVerbose; int fVeryVerbose; int nLutSizeMax; diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 87a05f2b..8ca16f29 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -24,6 +24,7 @@ #include "misc/extra/extra.h" #include "bool/kit/kit.h" #include "misc/util/utilTruth.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START @@ -1426,6 +1427,82 @@ void Jf_ManDeriveMapping( Jf_Man_t * p ) // Gia_ManMappingVerify( p->pGia ); } +/**Function************************************************************* + + Synopsis [Derive GIA without mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) ); + Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 ); + Vec_Int_t * vLeaves = Vec_IntAlloc( 16 ); + int i, k, iLit, Class, * pCut; + word uTruth; + assert( p->pPars->fCutMin ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) ); + pNew->pName = Abc_UtilStrsav( p->pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec ); + // map primary inputs + Vec_IntWriteEntry( vCopies, 0, 0 ); + Gia_ManForEachCi( p->pGia, pObj, i ) + Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) ); + // iterate through nodes used in the mapping + Gia_ManHashStart( pNew ); + Gia_ManForEachAnd( p->pGia, pObj, i ) + { + if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 ) + continue; + pCut = Jf_ObjCutBest( p, i ); +// printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut); + Class = Jf_CutFuncClass( pCut ); + uTruth = p->pPars->fUseTts ? *Vec_MemReadEntry(p->vTtMem, Class) : Sdm_ManReadDsdTruth(p->pDsd, Class); + assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) ); + if ( Jf_CutSize(pCut) == 0 ) + { + assert( Class == 0 ); + Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) ); + continue; + } + if ( Jf_CutSize(pCut) == 1 ) + { + assert( Class == 1 ); + iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) ); + iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit ); + Vec_IntWriteEntry( vCopies, i, iLit ); + continue; + } + // collect leaves + Vec_IntClear( vLeaves ); + Jf_CutForEachLit( pCut, iLit, k ) + Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) ); + // create GIA + iLit = Dsm_ManDeriveGia( pNew, uTruth, vLeaves, vCover ); + iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) ); + Vec_IntWriteEntry( vCopies, i, iLit ); + } + Gia_ManForEachCo( p->pGia, pObj, i ) + { + iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) ); + } + Vec_IntFree( vCopies ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCover ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) ); + return pNew; +} + /**Function************************************************************* Synopsis [] @@ -1451,6 +1528,7 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars ) pPars->fCutMin = 0; pPars->fUseTts = 0; pPars->fGenCnf = 0; + pPars->fPureAig = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; pPars->nLutSizeMax = JF_LEAF_MAX; @@ -1491,7 +1569,9 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " ); Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " ); } - if ( p->pPars->fCutMin ) + if ( p->pPars->fPureAig ) + pNew = Jf_ManDeriveGia(p); + else if ( p->pPars->fCutMin ) pNew = Jf_ManDeriveMappingGia(p); else Jf_ManDeriveMapping(p); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 30be411f..10b9e72e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29874,11 +29874,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv ) { char Buffer[200]; Jf_Par_t Pars, * pPars = &Pars; - Gia_Man_t * pNew; - int c; + Gia_Man_t * pNew; int c; Jf_ManSetDefaultPars( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcgvwh" ) ) != EOF ) { switch ( c ) { @@ -29961,6 +29960,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': pPars->fGenCnf ^= 1; break; + case 'g': + pPars->fPureAig ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -29999,7 +30001,7 @@ usage: sprintf(Buffer, "best possible" ); else sprintf(Buffer, "%d", pPars->DelayTarget ); - Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcvwh]\n" ); + Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcgvwh]\n" ); Abc_Print( -2, "\t performs technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum ); @@ -30012,6 +30014,7 @@ usage: Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" ); Abc_Print( -2, "\t-t : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" ); Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" ); + Abc_Print( -2, "\t-g : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n"); diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 0f332b26..0ee50007 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -87,6 +87,9 @@ extern int Dau_DsdCountAnds( char * pDsd ); extern void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR ); extern int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ); +/*=== dauGia.c ==========================================================*/ +extern int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover ); + /*=== dauMerge.c ==========================================================*/ extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars ); diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index 2aeeb958..05cfc485 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -1021,7 +1021,7 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nNonDecSize; // compose the result Dau_DsdWriteString( p, "<" ); - Dau_DsdWriteVar( p, pVars[vBest], 0 ); + Dau_DsdWriteVar( p, vBest, 0 ); // split decomposition Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest ); nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes ); diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c new file mode 100644 index 00000000..4ced55e6 --- /dev/null +++ b/src/opt/dau/dauGia.c @@ -0,0 +1,225 @@ +/**CFile**************************************************************** + + FileName [dauGia.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware unmapping.] + + Synopsis [Coverting DSD into GIA.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: dauGia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dauInt.h" +#include "aig/gia/gia.h" +#include "misc/util/utilTruth.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives GIA for the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVars ) +{ + int t0, t1; + if ( Func == 0 ) + return 0; + if ( Func == ~(word)0 ) + return 1; + assert( nVars > 0 ); + if ( --nVars == 0 ) + { + assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] ); + return Abc_LitNotCond( pFanins[0], (int)(Func == s_Truths6Neg[0]) ); + } + if ( !Abc_Tt6HasVar(Func, nVars) ) + 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 ); +} + +/**Function************************************************************* + + Synopsis [Derives GIA for the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, int * pLits, Vec_Int_t * vCover ) +{ + int fCompl = 0; + if ( **p == '!' ) + (*p)++, fCompl = 1; + if ( **p >= 'a' && **p <= 'f' ) // var + { + assert( **p - 'a' >= 0 && **p - 'a' < 6 ); + return Abc_LitNotCond( pLits[**p - 'a'], fCompl ); + } + if ( **p == '(' ) // and/or + { + char * q = pStr + pMatches[ *p - pStr ]; + int Res = 1, Lit; + assert( **p == '(' && *q == ')' ); + for ( (*p)++; *p < q; (*p)++ ) + { + Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); + Res = Gia_ManHashAnd( pGia, Res, Lit ); + } + assert( *p == q ); + return Abc_LitNotCond( Res, fCompl ); + } + if ( **p == '[' ) // xor + { + char * q = pStr + pMatches[ *p - pStr ]; + int Res = 0, Lit; + assert( **p == '[' && *q == ']' ); + for ( (*p)++; *p < q; (*p)++ ) + { + Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); + Res = Gia_ManHashXor( pGia, Res, Lit ); + } + assert( *p == q ); + return Abc_LitNotCond( Res, fCompl ); + } + if ( **p == '<' ) // mux + { + int nVars = 0; + int Temp[3], * pTemp = Temp, Res; + int Fanins[6], * pLits2; + char * pOld = *p; + char * q = pStr + pMatches[ *p - pStr ]; + // read fanins + if ( *(q+1) == '{' ) + { + char * q2; + *p = q+1; + q2 = pStr + pMatches[ *p - pStr ]; + assert( **p == '{' && *q2 == '}' ); + for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ ) + Fanins[nVars] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); + assert( *p == q2 ); + pLits2 = Fanins; + } + else + pLits2 = pLits; + // read MUX + *p = pOld; + q = pStr + pMatches[ *p - pStr ]; + assert( **p == '<' && *q == '>' ); + // verify internal variables + if ( nVars ) + for ( ; pOld < q; pOld++ ) + if ( *pOld >= 'a' && *pOld <= 'z' ) + assert( *pOld - 'a' < nVars ); + // derive MUX components + for ( (*p)++; *p < q; (*p)++ ) + *pTemp++ = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits2, vCover ); + assert( pTemp == Temp + 3 ); + assert( *p == q ); + if ( *(q+1) == '{' ) // and/or + { + char * q = pStr + pMatches[ ++(*p) - pStr ]; + assert( **p == '{' && *q == '}' ); + *p = q; + } + Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] ); + return Abc_LitNotCond( Res, fCompl ); + } + if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + { + word Func; + int Fanins[6], Res; + Vec_Int_t vLeaves; + char * q; + int i, nVars = Abc_TtReadHex( &Func, *p ); + *p += Abc_TtHexDigitNum( nVars ); + q = pStr + pMatches[ *p - pStr ]; + assert( **p == '{' && *q == '}' ); + for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) + Fanins[i] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); + assert( i == nVars ); + assert( *p == q ); +// Res = Dau_DsdToGiaCompose_rec( pGia, Func, Fanins, nVars ); + vLeaves.nCap = nVars; + vLeaves.nSize = nVars; + vLeaves.pArray = Fanins; + Res = Kit_TruthToGia( pGia, (unsigned *)&Func, nVars, vCover, &vLeaves, 1 ); + return Abc_LitNotCond( Res, fCompl ); + } + assert( 0 ); + return 0; +} +int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover ) +{ + int Res; + if ( *p == '0' && *(p+1) == 0 ) + Res = 0; + else if ( *p == '1' && *(p+1) == 0 ) + Res = 1; + else + Res = Dau_DsdToGia_rec( pGia, p, &p, Dau_DsdComputeMatches(p), pLits, vCover ); + assert( *++p == 0 ); + return Res; +} + +/**Function************************************************************* + + Synopsis [Convert TT to GIA via DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover ) +{ + Gia_Man_t * pGia = (Gia_Man_t *)p; + char pDsd[1000]; + int nSizeNonDec; +// static int Counter = 0; Counter++; + nSizeNonDec = Dau_DsdDecompose( &uTruth, Vec_IntSize(vLeaves), 1, 1, pDsd ); +// printf( "%s\n", pDsd ); + return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make index 5a3df1d5..f339810b 100644 --- a/src/opt/dau/module.make +++ b/src/opt/dau/module.make @@ -3,5 +3,6 @@ SRC += src/opt/dau/dauCanon.c \ src/opt/dau/dauDivs.c \ src/opt/dau/dauDsd.c \ src/opt/dau/dauEnum.c \ + src/opt/dau/dauGia.c \ src/opt/dau/dauMerge.c \ src/opt/dau/dauTree.c -- cgit v1.2.3