summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-06-25 17:19:44 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-06-25 17:19:44 -0700
commited319531be61bb82204a4450db69de73eb9641e1 (patch)
tree668ef05fffebe79d91ef5689c670e323cd6be9f7
parent0255934884387ca7c9343d22507c4920a8f70556 (diff)
downloadabc-ed319531be61bb82204a4450db69de73eb9641e1.tar.gz
abc-ed319531be61bb82204a4450db69de73eb9641e1.tar.bz2
abc-ed319531be61bb82204a4450db69de73eb9641e1.zip
Improving integration of the 'if' mapper with GIA.
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaDup.c2
-rw-r--r--src/aig/gia/giaIf.c411
-rw-r--r--src/base/abci/abc.c24
-rw-r--r--src/base/abci/abcRec3.c2
-rw-r--r--src/map/if/if.h1
6 files changed, 211 insertions, 231 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f0769e79..952168d2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -310,7 +310,7 @@ static inline int Gia_ManMuxNum( Gia_Man_t * p ) { return p->nMuxe
static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); }
static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; }
static inline void Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1; }
-static inline int Gia_ManWithChoices( Gia_Man_t * p ) { return p->pReprs != NULL; }
+static inline int Gia_ManWithChoices( Gia_Man_t * p ) { return p->pSibls != NULL; }
static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; }
static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 965d6ce3..17440e65 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1875,7 +1875,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
Gia_ManForEachCi( p0, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachCi( p1, pObj, i )
- if ( i < Gia_ManPiNum(p1) - nInsDup )
+ if ( i < Gia_ManCiNum(p1) - nInsDup )
pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
else
pObj->Value = Gia_ManAppendCi( pNew );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 10f65af1..e3a78ac9 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -408,82 +408,6 @@ int Gia_ManNodeIfSopToGia( Gia_Man_t * pNew, If_Man_t * p, If_Cut_t * pCut, Vec_
/**Function*************************************************************
- Synopsis [Recursively derives the local AIG for the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, int fHash )
-{
- If_Cut_t * pCut;
- If_Obj_t * pTemp;
- int iFunc, iFunc0, iFunc1;
- // get the best cut
- pCut = If_ObjCutBest(pIfObj);
- // if the cut is visited, return the result
- if ( If_CutDataInt(pCut) )
- return If_CutDataInt(pCut);
- // mark the node as visited
- Vec_PtrPush( vVisited, pCut );
- // insert the worst case
- If_CutSetDataInt( pCut, ~0 );
- // skip in case of primary input
- if ( If_ObjIsCi(pIfObj) )
- return If_CutDataInt(pCut);
- // compute the functions of the children
- for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
- {
- iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited, fHash );
- if ( iFunc0 == ~0 )
- continue;
- iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
- if ( iFunc1 == ~0 )
- continue;
- // both branches are solved
- if ( fHash )
- iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
- else
- iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
- if ( pTemp->fPhase != pIfObj->fPhase )
- iFunc = Abc_LitNot(iFunc);
- If_CutSetDataInt( pCut, iFunc );
- break;
- }
- return If_CutDataInt(pCut);
-}
-int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
-{
- If_Cut_t * pCut;
- If_Obj_t * pLeaf;
- int i, iRes;
- // get the best cut
- pCut = If_ObjCutBest(pIfObj);
- assert( pCut->nLeaves > 1 );
- // set the leaf variables
- If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
- If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
- // recursively compute the function while collecting visited cuts
- Vec_PtrClear( pIfMan->vTemp );
- iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp, fHash );
- if ( iRes == ~0 )
- {
- Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
- return ~0;
- }
- // clean the cuts
- If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
- If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
- Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
- If_CutSetDataInt( pCut, 0 );
- return iRes;
-}
-
-/**Function*************************************************************
-
Synopsis [Converts IF into GIA manager.]
Description []
@@ -493,7 +417,7 @@ int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj,
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
+Gia_Man_t * Gia_ManFromIfAig( If_Man_t * pIfMan )
{
int fHash = 0;
Gia_Man_t * pNew;
@@ -501,10 +425,9 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
If_Cut_t * pCutBest;
Vec_Int_t * vLeaves;
Vec_Int_t * vCover;
- unsigned * pTruth;
- int Counter, iOffset, nItems = 0;
- int i, k, w, GiaId;
+ int i, k;
assert( pIfMan->pPars->pLutStruct == NULL );
+ assert( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fUserRecLib );
// create new manager
pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
Gia_ManHashAlloc( pNew );
@@ -524,137 +447,23 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
Vec_IntPush( vLeaves, pIfLeaf->iCopy );
// get the functionality
- if ( pIfMan->pPars->pLutStruct )
- pIfObj->iCopy = Kit_TruthToGia( pNew, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, vLeaves, fHash );
- else if ( pIfMan->pPars->fDelayOpt )
+ if ( pIfMan->pPars->fDelayOpt )
pIfObj->iCopy = Gia_ManNodeIfSopToGia( pNew, pIfMan, pCutBest, vLeaves, fHash );
else if ( pIfMan->pPars->fUserRecLib )
pIfObj->iCopy = Abc_RecToGia3( pNew, pIfMan, pCutBest, vLeaves, fHash );
- else
- pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, fHash );
- // complement the node if the TT was used and the cut was complemented
- if ( pIfMan->pPars->pLutStruct )
- pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
- // count entries in the mapping array
- nItems += 2 + If_CutLeaveNum( pCutBest );
+ else assert( 0 );
}
else if ( If_ObjIsCi(pIfObj) )
pIfObj->iCopy = Gia_ManAppendCi(pNew);
else if ( If_ObjIsCo(pIfObj) )
pIfObj->iCopy = Gia_ManAppendCo( pNew, Abc_LitNotCond(If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj)) );
else if ( If_ObjIsConst1(pIfObj) )
- {
pIfObj->iCopy = 1;
- nItems += 2;
- }
else assert( 0 );
}
Vec_IntFree( vCover );
Vec_IntFree( vLeaves );
Gia_ManHashStop( pNew );
-
- // GIA after mapping with choices may end up with dangling nodes
- // which participate as leaves of some cuts used in the mapping
- // such nodes are marked here and skipped when mapping is derived
- Counter = Gia_ManMarkDangling(pNew);
-// if ( pIfMan->pPars->fVerbose && Counter )
- if ( Counter )
- printf( "GIA after mapping has %d dangling nodes.\n", Counter );
-
- // create mapping
- iOffset = Gia_ManObjNum(pNew);
- pNew->pMapping = ABC_CALLOC( int, iOffset + nItems );
- assert( pNew->vTruths == NULL );
- if ( pIfMan->pPars->pLutStruct )
- pNew->vTruths = Vec_IntAlloc( 1000 );
- If_ManForEachObj( pIfMan, pIfObj, i )
- {
- if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
- continue;
- if ( If_ObjIsAnd(pIfObj) )
- {
- GiaId = Abc_Lit2Var( pIfObj->iCopy );
- if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) ) // skip trivial node
- continue;
- assert( Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) );
- if ( !Gia_ManObj(pNew, GiaId)->fMark0 ) // skip dangling node
- continue;
- // get the best cut
- pCutBest = If_ObjCutBest( pIfObj );
- // copy the truth tables
- pTruth = NULL;
- if ( pNew->vTruths )
- {
- // copy truth table
- for ( w = 0; w < pIfMan->nTruthWords; w++ )
- Vec_IntPush( pNew->vTruths, If_CutTruth(pCutBest)[w] );
- pTruth = (unsigned *)(Vec_IntArray(pNew->vTruths) + Vec_IntSize(pNew->vTruths) - pIfMan->nTruthWords);
- // complement
- if ( pCutBest->fCompl ^ Abc_LitIsCompl(pIfObj->iCopy) )
- for ( w = 0; w < pIfMan->nTruthWords; w++ )
- pTruth[w] = ~pTruth[w];
- }
- // create node
- pNew->pMapping[GiaId] = iOffset;
- pNew->pMapping[iOffset++] = If_CutLeaveNum(pCutBest);
- If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
- {
- int FaninId = Abc_Lit2Var(pIfLeaf->iCopy);
- if ( pTruth && Abc_LitIsCompl(pIfLeaf->iCopy) )
- Kit_TruthChangePhase( pTruth, If_CutLeaveNum(pCutBest), k );
- if ( !Gia_ManObj(pNew, FaninId)->fMark0 ) // skip dangling node
- {
- // update truth table
- if ( pTruth )
- {
- extern void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar );
- if ( If_CutLeaveNum(pCutBest) >= 6 )
- If_CluSwapVars( (word*)pTruth, If_CutLeaveNum(pCutBest), NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
- else
- {
- word Truth = ((word)pTruth[0] << 32) | (word)pTruth[0];
- If_CluSwapVars( &Truth, 6, NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
- pTruth[0] = (Truth & 0xFFFFFFFF);
- }
- }
- pNew->pMapping[iOffset-k-1]--;
- continue;
- }
- assert( FaninId < GiaId );
- pNew->pMapping[iOffset++] = FaninId;
- }
- pNew->pMapping[iOffset++] = GiaId;
- }
- else if ( If_ObjIsConst1(pIfObj) )
- {
- // create node
- pNew->pMapping[0] = iOffset;
- pNew->pMapping[iOffset++] = 0;
- pNew->pMapping[iOffset++] = 0;
-/*
- if ( pNew->vTruths )
- {
- printf( "%d ", nLeaves );
- for ( w = 0; w < pIfMan->nTruthWords; w++ )
- Vec_IntPush( pNew->vTruths, 0 );
- }
-*/
- }
- }
- pNew->nOffset = iOffset;
- Gia_ManCleanMark0( pNew );
-// assert( iOffset == Gia_ManObjNum(pNew) + nItems );
-// if ( pIfMan->pManTim )
-// pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
- // verify that COs have mapping
- {
- Gia_Obj_t * pObj;
- Gia_ManForEachCo( pNew, pObj, i )
- {
- if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
- assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
- }
- }
return pNew;
}
@@ -670,15 +479,15 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
SeeAlso []
***********************************************************************/
-int Gia_ManFromIfStrCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2 )
+int Gia_ManFromIfLogicCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2 )
{
int i, iLit, iObjLit1;
iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)pRes, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
// write mapping
Vec_IntSetEntry( vMapping, Abc_Lit2Var(iObjLit1), Vec_IntSize(vMapping2) );
Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
- Vec_IntForEachEntry( vLeaves, iLit, i )
- assert( Abc_Lit2Var(iLit) < Abc_Lit2Var(iObjLit1) );
+// Vec_IntForEachEntry( vLeaves, iLit, i )
+// assert( Abc_Lit2Var(iLit) < Abc_Lit2Var(iObjLit1) );
Vec_IntForEachEntry( vLeaves, iLit, i )
Vec_IntPush( vMapping2, Abc_Lit2Var(iLit) );
Vec_IntPush( vMapping2, Abc_Lit2Var(iObjLit1) );
@@ -697,11 +506,37 @@ int Gia_ManFromIfStrCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeave
SeeAlso []
***********************************************************************/
-int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp,
+int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp,
word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
{
int nLeaves = Vec_IntSize(vLeaves);
int i, Length, nLutLeaf, nLutLeaf2, nLutRoot, iObjLit1, iObjLit2, iObjLit3;
+ // check simple case
+ static word s_Truths6[6] = {
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0xCCCCCCCCCCCCCCCC),
+ ABC_CONST(0xF0F0F0F0F0F0F0F0),
+ ABC_CONST(0xFF00FF00FF00FF00),
+ ABC_CONST(0xFFFF0000FFFF0000),
+ ABC_CONST(0xFFFFFFFF00000000)
+ };
+/*
+ if ( *pRes == 0 || ~*pRes == 0 )
+ return Abc_LitNotCond( 0, ~*pRes == 0 );
+ for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
+ if ( *pRes == s_Truths6[i] || ~*pRes == s_Truths6[i] )
+ return Abc_LitNotCond( Vec_IntEntry(vLeaves, i), ~*pRes == s_Truths6[i] );
+*/
+/*
+ if ( *pRes == 0 || ~*pRes == 0 )
+ printf( "Const\n" );
+ for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
+ if ( *pRes == s_Truths6[i] || ~*pRes == s_Truths6[i] )
+ printf( "Literal\n" );
+*/
+ // check if there is no LUT structures
+ if ( pStr == NULL )
+ return Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
// quit if parameters are wrong
Length = strlen(pStr);
@@ -730,7 +565,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) )
{
// create mapping
- iObjLit1 = Gia_ManFromIfStrCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
+ iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
// write packing
Vec_IntPush( vPacking, 1 );
Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit1) );
@@ -811,7 +646,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
Vec_IntClear( vLeavesTemp );
for ( i = 0; i < pLut1[0]; i++ )
Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut1[2+i]) );
- iObjLit1 = Gia_ManFromIfStrCreateLut( pNew, &Func1, vLeavesTemp, vCover, vMapping, vMapping2 );
+ iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, &Func1, vLeavesTemp, vCover, vMapping, vMapping2 );
if ( Length == 3 && pLut2[0] > 0 )
{
@@ -834,7 +669,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
Vec_IntPush( vLeavesTemp, iObjLit1 );
else
Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut2[2+i]) );
- iObjLit2 = Gia_ManFromIfStrCreateLut( pNew, &Func2, vLeavesTemp, vCover, vMapping, vMapping2 );
+ iObjLit2 = Gia_ManFromIfLogicCreateLut( pNew, &Func2, vLeavesTemp, vCover, vMapping, vMapping2 );
// write packing
Vec_IntPush( vPacking, 3 );
@@ -872,7 +707,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
Vec_IntPush( vLeavesTemp, iObjLit2 );
else
Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut0[2+i]) );
- iObjLit3 = Gia_ManFromIfStrCreateLut( pNew, &Func0, vLeavesTemp, vCover, vMapping, vMapping2 );
+ iObjLit3 = Gia_ManFromIfLogicCreateLut( pNew, &Func0, vLeavesTemp, vCover, vMapping, vMapping2 );
// write packing
Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit3) );
@@ -881,6 +716,81 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
return iObjLit3;
}
+/**Function*************************************************************
+
+ Synopsis [Recursively derives the local AIG for the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, int fHash )
+{
+ If_Cut_t * pCut;
+ If_Obj_t * pTemp;
+ int iFunc, iFunc0, iFunc1;
+ // get the best cut
+ pCut = If_ObjCutBest(pIfObj);
+ // if the cut is visited, return the result
+ if ( If_CutDataInt(pCut) )
+ return If_CutDataInt(pCut);
+ // mark the node as visited
+ Vec_PtrPush( vVisited, pCut );
+ // insert the worst case
+ If_CutSetDataInt( pCut, ~0 );
+ // skip in case of primary input
+ if ( If_ObjIsCi(pIfObj) )
+ return If_CutDataInt(pCut);
+ // compute the functions of the children
+ for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+ {
+ iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited, fHash );
+ if ( iFunc0 == ~0 )
+ continue;
+ iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
+ if ( iFunc1 == ~0 )
+ continue;
+ // both branches are solved
+ if ( fHash )
+ iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
+ else
+ iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
+ if ( pTemp->fPhase != pIfObj->fPhase )
+ iFunc = Abc_LitNot(iFunc);
+ If_CutSetDataInt( pCut, iFunc );
+ break;
+ }
+ return If_CutDataInt(pCut);
+}
+int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
+{
+ If_Cut_t * pCut;
+ If_Obj_t * pLeaf;
+ int i, iRes;
+ // get the best cut
+ pCut = If_ObjCutBest(pIfObj);
+ assert( pCut->nLeaves > 1 );
+ // set the leaf variables
+ If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+ If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
+ // recursively compute the function while collecting visited cuts
+ Vec_PtrClear( pIfMan->vTemp );
+ iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp, fHash );
+ if ( iRes == ~0 )
+ {
+ Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
+ return ~0;
+ }
+ // clean the cuts
+ If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+ If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
+ Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
+ If_CutSetDataInt( pCut, 0 );
+ return iRes;
+}
/**Function*************************************************************
@@ -893,21 +803,54 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManFromIfStr( If_Man_t * pIfMan )
+static inline word Gia_ManTt6Stretch( word t, int nVars )
+{
+ assert( nVars >= 0 );
+ if ( nVars == 0 )
+ nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
+ if ( nVars == 1 )
+ nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
+ if ( nVars == 2 )
+ nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
+ if ( nVars == 3 )
+ nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
+ if ( nVars == 4 )
+ nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
+ if ( nVars == 5 )
+ nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
+ assert( nVars == 6 );
+ return t;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts IF into GIA manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
{
Gia_Man_t * pNew;
If_Cut_t * pCutBest;
If_Obj_t * pIfObj, * pIfLeaf;
- Vec_Int_t * vMapping, * vMapping2, * vPacking;
+ Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
Vec_Int_t * vLeaves, * vLeaves2, * vCover;
+ word Truth = 0, * pTruthTable;
int i, k, Entry;
- assert( pIfMan->pPars->pLutStruct != NULL );
- assert( pIfMan->pPars->nLutSize >= 6 ); // if 5, need to change (word *)If_CutTruth(pCutBest) below
+ assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
// start mapping and packing
vMapping = Vec_IntStart( If_ManObjNum(pIfMan) );
vMapping2 = Vec_IntStart( 1 );
- vPacking = Vec_IntAlloc( 1000 );
- Vec_IntPush( vPacking, 0 );
+ if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->pLutStruct )
+ {
+ vPacking = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vPacking, 0 );
+ }
// create new manager
pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
// iterate through nodes used in the mapping
@@ -926,9 +869,33 @@ Gia_Man_t * Gia_ManFromIfStr( If_Man_t * pIfMan )
Vec_IntClear( vLeaves );
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
Vec_IntPush( vLeaves, pIfLeaf->iCopy );
- // perform decomposition of the cut
- pIfObj->iCopy = Gia_ManFromIfStrNode( pNew, i, vLeaves, vLeaves2, (word *)If_CutTruth(pCutBest), pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking );
- pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+ // perform one of the two types of mapping: with and without structures
+ if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth )
+ {
+ // adjust the truth table
+ int nSize = pIfMan->pPars->nLutSize;
+ pTruthTable = (word *)If_CutTruth(pCutBest);
+ if ( nSize < 6 )
+ {
+ Truth = Gia_ManTt6Stretch( *pTruthTable, nSize );
+ pTruthTable = &Truth;
+ }
+ // perform decomposition of the cut
+ pIfObj->iCopy = Gia_ManFromIfLogicNode( pNew, i, vLeaves, vLeaves2, pTruthTable, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking );
+ pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+ }
+ else
+ {
+ pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, 0 );
+ // write mapping
+ Vec_IntSetEntry( vMapping, Abc_Lit2Var(pIfObj->iCopy), Vec_IntSize(vMapping2) );
+ Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
+ Vec_IntForEachEntry( vLeaves, Entry, k )
+ assert( Abc_Lit2Var(Entry) < Abc_Lit2Var(pIfObj->iCopy) );
+ Vec_IntForEachEntry( vLeaves, Entry, k )
+ Vec_IntPush( vMapping2, Abc_Lit2Var(Entry) );
+ Vec_IntPush( vMapping2, Abc_Lit2Var(pIfObj->iCopy) );
+ }
}
else if ( If_ObjIsCi(pIfObj) )
pIfObj->iCopy = Gia_ManAppendCi(pNew);
@@ -1057,7 +1024,8 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, k, iFan;
- assert( pGia->pMapping != NULL );
+ if ( pGia->pMapping == NULL )
+ return;
Gia_ManMappingVerify( pGia );
Vec_IntFreeP( &p->vMapping );
p->vMapping = Vec_IntAlloc( 2 * Gia_ManObjNum(p) );
@@ -1144,6 +1112,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
Gia_Man_t * pNew;
If_Man_t * pIfMan;
If_Par_t * pPars = (If_Par_t *)pp;
+ // disable cut minimization
+ if ( !(pPars->fDelayOpt || pPars->fUserRecLib) && !pPars->fDeriveLuts )//&& Gia_ManWithChoices(p) )
+ pPars->fCutMin = 0; // not compatible with deriving result
// reconstruct GIA according to the hierarchy manager
assert( pPars->pTimesArr == NULL );
assert( pPars->pTimesReq == NULL );
@@ -1178,19 +1149,16 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
return NULL;
}
// transform the result of mapping into the new network
- if ( pIfMan->pPars->pLutStruct )
- pNew = Gia_ManFromIfStr( pIfMan );
+ if ( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fUserRecLib )
+ pNew = Gia_ManFromIfAig( pIfMan );
else
- pNew = Gia_ManFromIf( pIfMan );
+ pNew = Gia_ManFromIfLogic( pIfMan );
If_ManStop( pIfMan );
// transfer name
assert( pNew->pName == NULL );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
- // unmap in case of SOP balancing
-// if ( pIfMan->pPars->fDelayOpt )
-// Vec_IntFreeP( &pNew->vMapping );
// return the original (unmodified by the mapper) timing manager
pNew->pManTime = p->pManTime; p->pManTime = NULL;
pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
@@ -1203,12 +1171,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
pNew->pManTime = p->pManTime; p->pManTime = NULL;
pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
pNew->nAnd2Delay = p->nAnd2Delay; p->nAnd2Delay = 0;
-// pNew->vPacking = p->vPacking; p->vPacking = NULL;
Gia_ManStop( p );
-
// printf( "PERFORMING VERIFICATION:\n" );
// Gia_ManVerifyWithBoxes( pNew, NULL );
-
return pNew;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aeb146e2..57cb9739 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28362,9 +28362,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
char * FileName, * pTemp;
char ** pArgvNew;
int c, nArgcNew, fMiter = 0;
+ int fDumpMiter = 0;
Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CTmvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdvh" ) ) != EOF )
{
switch ( c )
{
@@ -28393,6 +28394,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMiter ^= 1;
break;
+ case 'd':
+ fDumpMiter ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -28448,6 +28452,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
if ( pMiter )
{
+ if ( fDumpMiter )
+ {
+ Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+ }
pAbc->Status = Cec_ManVerify( pMiter, pPars );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Gia_ManStop( pMiter );
@@ -28456,11 +28465,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &cec [-CT num] [-mvh]\n" );
+ Abc_Print( -2, "usage: &cec [-CT num] [-mdvh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
+ Abc_Print( -2, "\t-d : toggle dumping dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -28824,7 +28834,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikczvh" ) ) != EOF )
{
switch ( c )
{
@@ -28986,6 +28996,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fEnableRealPos ^= 1;
break;
+ case 'z':
+ pPars->fDeriveLuts ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -29092,7 +29105,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// enable truth table computation if cut minimization is selected
- if ( pPars->fCutMin )
+ if ( pPars->fCutMin || pPars->fDeriveLuts )
{
pPars->fTruth = 1;
pPars->fExpRed = 0;
@@ -29165,7 +29178,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
- Abc_Print( -2, "usage: &if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbgyojikcvh]\n" );
+ Abc_Print( -2, "usage: &if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbgyojikczvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -29194,6 +29207,7 @@ usage:
Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
Abc_Print( -2, "\t-k : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" );
Abc_Print( -2, "\t-c : toggles enabling additional feature [default = %s]\n", pPars->fEnableRealPos? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
return 1;
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 68bb8cdc..cf90a79d 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -1149,7 +1149,7 @@ int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int
assert( Gia_ObjIsAnd(pGiaTemp) );
iGiaObj = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
// complement the result if needed
- return Abc_LitNotCond( iGiaObj, Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );
+ return Abc_LitNotCond( iGiaObj, Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) ^ pCut->fCompl );
}
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 902754dd..ca5937fd 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -119,6 +119,7 @@ struct If_Par_t_
int fEnableCheck10;// enable additional checking
int fEnableRealPos;// enable additional feature
int fUseDsd; // compute DSD of the cut functions
+ int fDeriveLuts; // enables deriving LUT structures
int fVerbose; // the verbosity flag
char * pLutStruct; // LUT structure
float WireDelay; // wire delay