summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2019-09-26 14:05:16 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2019-09-26 14:05:16 -0700
commitb292595062b947bc0c1de79fe25facb34c0e20c1 (patch)
tree46442f4d5924d4ba962492ee2fcfedb16d1a6e2e
parentdf2bce1e40bcc14710cc8e019b0ab5a01176c54f (diff)
downloadabc-b292595062b947bc0c1de79fe25facb34c0e20c1.tar.gz
abc-b292595062b947bc0c1de79fe25facb34c0e20c1.tar.bz2
abc-b292595062b947bc0c1de79fe25facb34c0e20c1.zip
Adding switch to &if to consider special type of 6-input cuts.
-rw-r--r--src/base/abci/abc.c7
-rw-r--r--src/map/if/if.h4
-rw-r--r--src/map/if/ifMan.c5
-rw-r--r--src/map/if/ifMap.c2
-rw-r--r--src/map/if/ifTruth.c73
-rw-r--r--src/misc/vec/vecMem.h7
-rw-r--r--src/proof/acec/acecMult.c56
7 files changed, 151 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4eafa0b9..69d6db89 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36701,7 +36701,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fExpRed ^= 1;
break;
case 'l':
- pPars->fLatchPaths ^= 1;
+ pPars->fLut6Filter ^= 1;
break;
case 'e':
pPars->fEdge ^= 1;
@@ -36961,7 +36961,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutSize = pPars->nGateSize;
}
- if ( pPars->fUseDsd || pPars->fUseTtPerm )
+ if ( pPars->fUseDsd || pPars->fUseTtPerm || pPars->fLut6Filter )
{
pPars->fTruth = 1;
pPars->fCutMin = 1;
@@ -37077,7 +37077,8 @@ usage:
Abc_Print( -2, "\t-q : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
Abc_Print( -2, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
- Abc_Print( -2, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+// Abc_Print( -2, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggle restricting the type of 6-input lookup tables [default = %s]\n", pPars->fLut6Filter? "yes": "no" );
Abc_Print( -2, "\t-e : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
Abc_Print( -2, "\t-p : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
Abc_Print( -2, "\t-m : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index eb81d64e..aa9608c9 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -117,6 +117,7 @@ struct If_Par_t_
int fFancy; // a fancy feature
int fExpRed; // expand/reduce of the best cuts
int fLatchPaths; // reset timing on latch paths
+ int fLut6Filter; // uses filtering of 6-LUT functions
int fEdge; // uses edge-based cut selection heuristics
int fPower; // uses power-aware cut selection heuristics
int fCutMin; // performs cut minimization by removing functionally reducdant variables
@@ -260,6 +261,7 @@ struct If_Man_t_
Hash_IntMan_t * vPairHash; // hashing pairs of truth tables
Vec_Int_t * vPairRes; // resulting truth table
Vec_Str_t * vPairPerms; // resulting permutation
+ Vec_Mem_t * vTtMem6;
char pCanonPerm[IF_MAX_LUTSIZE];
unsigned uCanonPhase;
int nCacheHits;
@@ -652,6 +654,8 @@ extern void If_ManComputeRequired( If_Man_t * p );
extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
extern int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern Vec_Mem_t * If_DeriveHashTable6( int nVars, word Truth );
+extern int If_CutCheckTruth6( If_Man_t * p, If_Cut_t * pCut );
/*=== ifTune.c ===========================================================*/
extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
extern int Ifn_NtkTtBits( char * pStr );
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 27d7245e..4027b780 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -284,6 +284,11 @@ void If_ManStop( If_Man_t * p )
for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
Vec_IntFreeP( &p->vTtOccurs[i] );
Mem_FixedStop( p->pMemObj, 0 );
+ if ( p->vTtMem6 )
+ {
+ Vec_MemHashFree( p->vTtMem6 );
+ Vec_MemFreeP( &p->vTtMem6 );
+ }
ABC_FREE( p->pMemCi );
ABC_FREE( p->pMemAnd );
ABC_FREE( p->puTemp[0] );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index b5ae6b11..afeba005 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -292,6 +292,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
p->timeCache[4] += Abc_Clock() - clk;
if ( !p->pPars->fSkipCutFilter && fChange && If_CutFilter( pCutSet, pCut, fSave0 ) )
continue;
+ if ( p->pPars->fLut6Filter && pCut->nLeaves == 6 && !If_CutCheckTruth6(p, pCut) )
+ continue;
if ( p->pPars->fUseDsd )
{
extern void If_ManCacheRecord( If_Man_t * p, int iDsd0, int iDsd1, int nShared, int iDsd );
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 7c8892d3..83c40952 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -330,6 +330,79 @@ p->timeCache[2] += Abc_Clock() - clk;
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Check the function of 6-input LUT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Mem_t * If_DeriveHashTable6( int nVars, word uTruth )
+{
+ int fVerbose = 0;
+ int nMints = (1 << nVars);
+ int nPerms = Extra_Factorial( nVars );
+ int * pComp = Extra_GreyCodeSchedule( nVars );
+ int * pPerm = Extra_PermSchedule( nVars );
+ word Canon = ABC_CONST(0xFFFFFFFFFFFFFFFF);
+ word tCur, tTemp1, tTemp2;
+ Vec_Mem_t * vTtMem6 = Vec_MemAllocForTTSimple( nVars );
+ int i, p, c;
+ for ( i = 0; i < 2; i++ )
+ {
+ tCur = i ? ~uTruth : uTruth;
+ tTemp1 = tCur;
+ for ( p = 0; p < nPerms; p++ )
+ {
+ tTemp2 = tCur;
+ for ( c = 0; c < nMints; c++ )
+ {
+ if ( Canon > tCur )
+ Canon = tCur;
+ Vec_MemHashInsert( vTtMem6, &tCur );
+ tCur = Abc_Tt6Flip( tCur, pComp[c] );
+ }
+ assert( tTemp2 == tCur );
+ tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[p] );
+ }
+ assert( tTemp1 == tCur );
+ }
+ ABC_FREE( pComp );
+ ABC_FREE( pPerm );
+ if ( fVerbose )
+ {
+/*
+ word * pEntry;
+ Vec_MemForEachEntry( vTtMem6, pEntry, i )
+ {
+ Extra_PrintHex( stdout, (unsigned*)pEntry, nVars );
+ printf( ", " );
+ if ( i % 4 == 3 )
+ printf( "\n" );
+ }
+*/
+ Extra_PrintHex( stdout, (unsigned*)&uTruth, nVars ); printf( "\n" );
+ Extra_PrintHex( stdout, (unsigned*)&Canon, nVars ); printf( "\n" );
+ printf( "Members = %d.\n", Vec_MemEntryNum(vTtMem6) );
+ }
+ return vTtMem6;
+}
+
+int If_CutCheckTruth6( If_Man_t * p, If_Cut_t * pCut )
+{
+ if ( pCut->nLeaves != 6 )
+ return 0;
+ if ( p->vTtMem6 == NULL )
+ p->vTtMem6 = If_DeriveHashTable6( 6, ABC_CONST(0xfedcba9876543210) );
+ if ( *Vec_MemHashLookup( p->vTtMem6, If_CutTruthWR(p, pCut) ) == -1 )
+ return 0;
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index ef2d2af7..e8ddd44a 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -397,6 +397,13 @@ static int Vec_MemHashInsert( Vec_Mem_t * p, word * pEntry )
SeeAlso []
***********************************************************************/
+static inline Vec_Mem_t * Vec_MemAllocForTTSimple( int nVars )
+{
+ int nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));
+ Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 12 );
+ Vec_MemHashAlloc( vTtMem, 10000 );
+ return vTtMem;
+}
static inline Vec_Mem_t * Vec_MemAllocForTT( int nVars, int fCompl )
{
int Value, nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 66ee2fb7..d6cf10a9 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -158,6 +158,62 @@ unsigned s_Classes4c[768] = {
SeeAlso []
***********************************************************************/
+word Extra_TruthCanonNPN3( word uTruth, int nVars, Vec_Wrd_t * vRes )
+{
+ int nMints = (1 << nVars);
+ int nPerms = Extra_Factorial( nVars );
+ int * pComp = Extra_GreyCodeSchedule( nVars );
+ int * pPerm = Extra_PermSchedule( nVars );
+ word tCur, tTemp1, tTemp2;
+ word uTruthMin = ABC_CONST(0xFFFFFFFFFFFFFFFF);
+ int i, p, c;
+ Vec_WrdClear( vRes );
+ for ( i = 0; i < 2; i++ )
+ {
+ tCur = i ? ~uTruth : uTruth;
+ tTemp1 = tCur;
+ for ( p = 0; p < nPerms; p++ )
+ {
+ tTemp2 = tCur;
+ for ( c = 0; c < nMints; c++ )
+ {
+ if ( uTruthMin > tCur )
+ uTruthMin = tCur;
+ Vec_WrdPushUnique( vRes, tCur );
+ tCur = Abc_Tt6Flip( tCur, pComp[c] );
+ }
+ assert( tTemp2 == tCur );
+ tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[p] );
+ }
+ assert( tTemp1 == tCur );
+ }
+ ABC_FREE( pComp );
+ ABC_FREE( pPerm );
+ return uTruthMin;
+}
+void Acec_MultFuncTest6()
+{
+ Vec_Wrd_t * vRes = Vec_WrdAlloc( 10000 );
+ int i; word Entry;
+
+ word Truth = ABC_CONST(0xfedcba9876543210);
+ word Canon = Extra_TruthCanonNPN3( Truth, 6, vRes );
+
+ Extra_PrintHex( stdout, (unsigned*)&Truth, 6 ); printf( "\n" );
+ Extra_PrintHex( stdout, (unsigned*)&Canon, 6 ); printf( "\n" );
+
+ printf( "Members = %d.\n", Vec_WrdSize(vRes) );
+ Vec_WrdForEachEntry( vRes, Entry, i )
+ {
+ Extra_PrintHex( stdout, (unsigned*)&Entry, 6 );
+ printf( ", " );
+ if ( i % 8 == 7 )
+ printf( "\n" );
+ }
+
+ Vec_WrdFree( vRes );
+}
+
unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
{
static int nVarsOld, nPerms;