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

Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.

This commit is contained in:
Alan Mishchenko 2012-09-06 15:32:07 -07:00
parent 4393a5fade
commit 9c8be56ccd
17 changed files with 1212 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abclib.dsp
View File

@ -3759,6 +3759,14 @@ SOURCE=.\src\bool\lucky\lucky.h
# End Source File
# Begin Source File
SOURCE=.\src\bool\lucky\luckyFast16.c
# End Source File
# Begin Source File
SOURCE=.\src\bool\lucky\luckyFast6.c
# End Source File
# Begin Source File
SOURCE=.\src\bool\lucky\luckyInt.h
# End Source File
# Begin Source File
@ -3769,6 +3777,10 @@ SOURCE=.\src\bool\lucky\luckyRead.c
SOURCE=.\src\bool\lucky\luckySwap.c
# End Source File
# Begin Source File
SOURCE=.\src\bool\lucky\luckySwapIJ.c
# End Source File
# End Group
# End Group
# Begin Group "prove"

8
src/aig/aig/aigCanon.c
View File

@ -37,7 +37,7 @@ typedef struct Aig_VSig_t_ Aig_VSig_t;
struct Aig_VSig_t_
{
int nOnes;
short nCofOnes[RMAN_MAXVARS];
int nCofOnes[RMAN_MAXVARS];
};
typedef struct Aig_Tru_t_ Aig_Tru_t;
@ -307,7 +307,7 @@ void Aig_RManQuit()
***********************************************************************/
void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAux )
{
short pStore2[32];
int pStore2[32];
int i;
Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux );
for ( i = 0; i < nVars; i++ )
@ -326,7 +326,7 @@ void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAu
SeeAlso []
***********************************************************************/
void Aig_RManSortNums( short * pArray, int nVars )
void Aig_RManSortNums( int * pArray, int nVars )
{
int i, j, best_i, tmp;
for ( i = 0; i < nVars-1; i++ )
@ -409,7 +409,7 @@ void Aig_RManComputeVSigs( unsigned * pTruth, int nVars, Aig_VSig_t * pSigs, uns
***********************************************************************/
static inline int Aig_RManCompareSigs( Aig_VSig_t * p0, Aig_VSig_t * p1, int nVars )
{
// return memcmp( p0, p1, sizeof(int) + sizeof(short) * nVars );
// return memcmp( p0, p1, sizeof(int) + sizeof(int) * nVars );
return memcmp( p0, p1, sizeof(int) );
}

5
src/base/abci/abc.c
View File

@ -4907,10 +4907,11 @@ usage:
Abc_Print( -2, "\t testbench for computing semi-canonical forms of Boolean functions\n" );
Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
Abc_Print( -2, "\t 0: none (reading and writing the file)\n" );
Abc_Print( -2, "\t 1: exact canonical form (work only for 6 variables)\n" );
Abc_Print( -2, "\t 1: exact canonical form (works only for 6 variables)\n" );
Abc_Print( -2, "\t 2: semi-canonical form by counting 1s in cofactors\n" );
Abc_Print( -2, "\t 3: semi-canonical form by minimizing truth table value\n" );
Abc_Print( -2, "\t 4: hybrid semi-canonical form (work only for 6 variables)\n" );
Abc_Print( -2, "\t 4: hybrid semi-canonical form (works only for 6 variables)\n" );
Abc_Print( -2, "\t 5: Jake's hybrid semi-canonical form (works up to 16 variables)\n" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

74
src/base/abci/abcNpn.c
View File

@ -41,10 +41,10 @@ ABC_NAMESPACE_IMPL_START
typedef struct Abc_TtStore_t_ Abc_TtStore_t;
struct Abc_TtStore_t_
{
int nVars;
int nWords;
int nFuncs;
word ** pFuncs;
int nVars;
int nWords;
int nFuncs;
word ** pFuncs;
};
extern Abc_TtStore_t * Abc_TtStoreLoad( char * pFileName );
@ -82,6 +82,26 @@ int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
return (p->nFuncs = k);
}
/**Function*************************************************************
Synopsis [Prints out one NPN transform.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
{
int i;
printf( " %c = ( ", Abc_InfoHasBit(&uCanonPhase, nVars) ? 'Z':'z' );
for ( i = 0; i < nVars; i++ )
printf( "%c%s", pCanonPerm[i] + ('A'-'a') * Abc_InfoHasBit(&uCanonPhase, pCanonPerm[i]-'a'), i == nVars-1 ? "":"," );
printf( " ) " );
}
/**Function*************************************************************
Synopsis [Apply decomposition to the truth table.]
@ -95,24 +115,25 @@ int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
***********************************************************************/
void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
short pStore[16];
char pCanonPerm[16];
unsigned pAux[2048];
char pCanonPerm[32];
unsigned uCanonPhase=0;
clock_t clk = clock();
int i;//, nFuncs = 0;
int i;
char * pAlgoName = NULL;
if ( NpnType == 0 )
pAlgoName = "uniqifying ";
pAlgoName = "uniqifying ";
else if ( NpnType == 1 )
pAlgoName = "exact NPN ";
pAlgoName = "exact NPN ";
else if ( NpnType == 2 )
pAlgoName = "counting 1s ";
pAlgoName = "counting 1s ";
else if ( NpnType == 3 )
pAlgoName = "minimizing TT";
pAlgoName = "minimizing TT ";
else if ( NpnType == 4 )
pAlgoName = "hybrid NPN ";
pAlgoName = "hybrid NPN ";
else if ( NpnType == 5 )
pAlgoName = "Jake's hybrid NPN";
assert( p->nVars <= 16 );
if ( pAlgoName )
@ -157,9 +178,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm, pStore );
resetPCanonPermArray(pCanonPerm, p->nVars);
uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
else if ( NpnType == 3 )
@ -168,9 +190,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
resetPCanonPermArray(pCanonPerm, p->nVars);
uCanonPhase = Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
else if ( NpnType == 4 )
@ -181,7 +204,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm, pStore );
resetPCanonPermArray(pCanonPerm, p->nVars);
Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
*((word *)p->pFuncs[i]) = Extra_Truth6MinimumHeuristic( *((word *)p->pFuncs[i]) );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
@ -190,6 +214,18 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
else
printf( "This feature only works for 6-variable functions.\n" );
}
else if ( NpnType == 5 )
{
for ( i = 0; i < p->nFuncs; i++ )
{
if ( fVerbose )
printf( "%7d : ", i );
resetPCanonPermArray(pCanonPerm, p->nVars);
uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
else assert( 0 );
clk = clock() - clk;
@ -248,7 +284,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
if ( NpnType >= 0 && NpnType <= 4 )
if ( NpnType >= 0 && NpnType <= 5 )
Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
else
printf( "Unknown canonical form value (%d).\n", NpnType );

8
src/base/abci/abcRec.c
View File

@ -881,7 +881,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);
Vec_PtrGrow(s_pMan->vLabels, Abc_NtkObjNumMax(pAig));
@ -2252,7 +2252,7 @@ clk = clock();
// semi-canonicize the truth table
clk = clock();
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm, (short *)s_pMan->pMints );
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm );
If_CutTruthStretch(pInOut, nLeaves, s_pMan->nVars);
s_pMan->timeCanon += clock() - clk;
// pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@ -2819,7 +2819,7 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
//canonicize
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
s_pMan->timeIfCanonicize += clock() - timeCanonicize;
timeDelayComput = clock();
@ -2997,7 +2997,7 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
pCanonPerm[i] = i;
// canonicize the truth table
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nVars, pCanonPerm, (short *)s_pMan->pMints );
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nVars, pCanonPerm );
// get hold of the curresponding class
ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );

11
src/base/abci/abcRec2.c
View File

@ -1183,6 +1183,11 @@ for ( i = 0; i < p->nBins; i++ )
for ( entry = p->pBins[i]; entry != REC_EMPTY_ID; entry = Rec_Obj(p, entry)->pCopy )
{
int tmp = 0;
assert( 0 );
// added the next line to silence the warning that 'pEntry' is not initialized
pEntry = -1;
// pTruth = (unsigned*)Vec_PtrEntry(p->vTtNodes, entry);
pTruth = Rec_MemReadEntry( p, Rec_Obj(p, pEntry)->truthID );
/*if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
@ -1525,7 +1530,7 @@ clk = clock();
// semi-canonicize the truth table
clk = clock();
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm, (short *)s_pMan->pMints );
uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm );
If_CutTruthStretch(pInOut, nLeaves, s_pMan->nVars);
s_pMan->timeCanon += clock() - clk;
// pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@ -1875,7 +1880,7 @@ int If_CutDelayRecCost2(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
//canonicize
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
s_pMan->timeIfCanonicize += clock() - timeCanonicize;
timeDelayComput = clock();
@ -1986,7 +1991,7 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);

8
src/bool/kit/kit.h
View File

@ -623,11 +623,11 @@ extern int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar
extern int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
extern void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore );
extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore );
extern void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore );
extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux );
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
extern void Kit_TruthPrintProfile( unsigned * pTruth, int nVars );

18
src/bool/kit/kitTruth.c
View File

@ -1397,7 +1397,7 @@ int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigne
Synopsis [Counts the number of 1's in each cofactor.]
Description [The resulting numbers are stored in the array of shorts,
Description [The resulting numbers are stored in the array of ints,
whose length is 2*nVars. The number of 1's is counted in a different
space than the original function. For example, if the function depends
on k variables, the cofactors are assumed to depend on k-1 variables.]
@ -1407,11 +1407,11 @@ int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigne
SeeAlso []
***********************************************************************/
void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Counter;
memset( pStore, 0, sizeof(short) * 2 * nVars );
memset( pStore, 0, sizeof(int) * 2 * nVars );
if ( nVars <= 5 )
{
if ( nVars > 0 )
@ -1473,7 +1473,7 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
Synopsis [Counts the number of 1's in each negative cofactor.]
Description [The resulting numbers are stored in the array of shorts,
Description [The resulting numbers are stored in the array of ints,
whose length is nVars. The number of 1's is counted in a different
space than the original function. For example, if the function depends
on k variables, the cofactors are assumed to depend on k-1 variables.]
@ -1483,11 +1483,11 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
SeeAlso []
***********************************************************************/
void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore )
void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Counter;
memset( pStore, 0, sizeof(short) * nVars );
memset( pStore, 0, sizeof(int) * nVars );
if ( nVars <= 5 )
{
if ( nVars > 0 )
@ -1534,7 +1534,7 @@ void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore )
SeeAlso []
***********************************************************************/
void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux )
void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux )
{
int i;
for ( i = 0; i < nVars; i++ )
@ -1654,9 +1654,9 @@ unsigned Kit_TruthHash( unsigned * pIn, int nWords )
SeeAlso []
***********************************************************************/
unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
{
// short pStore2[32];
int pStore[32];
unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
int nWords = Kit_TruthWordNum( nVars );
int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;

4
src/bool/lucky/lucky.c
View File

@ -655,7 +655,7 @@ int main ()
word** a, ** b;
Abc_TtStore_t* p;
word * pAux, * pAux1;
short * pStore;
int * pStore;
// cycleCtr* cCtr;
charArray = (char**)malloc(sizeof(char*)*3);
@ -672,7 +672,7 @@ int main ()
pAux = (word*)malloc(sizeof(word)*(p->nWords));
pAux1 = (word*)malloc(sizeof(word)*(p->nWords));
pStore = (short*)malloc(sizeof(short)*(p->nVars));
pStore = (int*)malloc(sizeof(int)*(p->nVars));
printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
tempNF = p->nFuncs;

4
src/bool/lucky/lucky.h
View File

@ -6,7 +6,7 @@
PackageName [Semi-canonical form computation package.]
Synopsis [Internal declarations.]
Synopsis [External declarations.]
Author [Jake]
@ -21,6 +21,8 @@
ABC_NAMESPACE_HEADER_START
extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
extern int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
extern void resetPCanonPermArray(char* x, int nVars);
ABC_NAMESPACE_HEADER_END

625
src/bool/lucky/luckyFast16.c Normal file
View File

@ -0,0 +1,625 @@
/**CFile****************************************************************
FileName [luckyFast16.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Semi-canonical form computation package.]
Synopsis [Truth table minimization procedures for up to 16 vars.]
Author [Jake]
Date [Started - September 2012]
***********************************************************************/
#include "luckyInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
// there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
//updataInfo updates CanonPerm and CanonPhase based on what quoter in position iQ and jQ
inline void updataInfo(int iQ, int jQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
{
*pCanonPhase = adjustInfoAfterSwap(pCanonPerm, *pCanonPhase, iVar, ((abs(iQ-jQ)-1)<<2) + iQ );
}
// It rearranges InOut (swaps and flips through rearrangement of quoters)
// It updates Info at the end
inline void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
{
int i;
int blockSize = 1<<iVar;
for(i=start;i>=0;i--)
{
pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) |
(((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) |
(((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) |
(((pInOut[i] & SFmask[iVar][lQ])<<(lQ*blockSize))>>3*blockSize);
}
updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
}
//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 0Q and 3Q
inline int minTemp0_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
{
int i, j=1;
int blockSize = 1<<iVar;
int shiftSize = blockSize*4;
word temp;
for(i=nWords - 1; i>=0; i--)
{
temp = ((pInOut[i] & SFmask[iVar][0])) ^ ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize));
if( temp == 0)
continue;
else
{
*pDifStart = i*100;
while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
j++;
*pDifStart += 21 - j;
if( ((pInOut[i] & SFmask[iVar][0])) < ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)) )
return 0;
else
return 3;
}
}
*pDifStart=0;
return 0;
}
//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 1Q and 2Q
inline int minTemp1_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
{
int i, j=1;
int blockSize = 1<<iVar;
int shiftSize = blockSize*4;
word temp;
for(i=nWords - 1; i>=0; i--)
{
temp = ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) ^ ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize));
if( temp == 0)
continue;
else
{
*pDifStart = i*100;
while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
j++;
*pDifStart += 21 - j;
if( ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) < ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)) )
return 1;
else
return 2;
}
}
*pDifStart=0;
return 1;
}
//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in iQ and jQ
inline int minTemp2_fast(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
{
int i, j=1;
int blockSize = 1<<iVar;
int shiftSize = blockSize*4;
word temp;
for(i=nWords - 1; i>=0; i--)
{
temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
if( temp == 0)
continue;
else
{
*pDifStart = i*100;
while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
j++;
*pDifStart += 21 - j;
if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
return 0;
else
return 1;
}
}
*pDifStart=0;
return iQ;
}
// same as minTemp2_fast but this one has a start position
inline int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
{
int i, j=1;
int blockSize = 1<<iVar;
int shiftSize = blockSize*4;
word temp;
for(i=start; i>=finish; i--)
{
temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
if( temp == 0)
continue;
else
{
*pDifStart = i*100;
while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
j++;
*pDifStart += 21 - j;
if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
return 0;
else
return 1;
}
}
*pDifStart=0;
return iQ;
}
// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
{
int min1, min2, DifStart0, DifStart1, DifStartMin;
int M[2];
int blockSize = 1<<iVar;
int shiftSize = blockSize*4;
M[0] = minTemp0_fast(pInOut, iVar, nWords, &DifStart0); // 0, 3
M[1] = minTemp1_fast(pInOut, iVar, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
{
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart0/100), M[0], M[1], 3 - M[1], 3 - M[0], iVar, nWords, pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart1/100), M[1], M[0], 3 - M[0], 3 - M[1], iVar, nWords, pCanonPerm, pCanonPhase);
}
else
{
if(DifStartMin>=DifStart0)
arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
else
{
min2 = minTemp3_fast(pInOut, iVar, DifStart0/100, DifStartMin/100, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
if(DifStart1>DifStartMin)
arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, nWords, pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
}
}
}
////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
// It rearranges InOut (swaps and flips through rearrangement of quoters)
// It updates Info at the end
inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int start, int iQ, int jQ, int kQ, int lQ, char * pCanonPerm, unsigned* pCanonPhase)
{
int i,blockSize,shiftSize;
unsigned* tempPtr = temp+start;
if(iQ == 0 && jQ == 1)
return;
blockSize = sizeof(unsigned);
shiftSize = 4;
for(i=start-1;i>0;i-=shiftSize)
{
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-iQ, blockSize);
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-jQ, blockSize);
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-kQ, blockSize);
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-lQ, blockSize);
}
memcpy(pInOut, temp, start*sizeof(unsigned));
updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
}
//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 0Q and 3Q
inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
{
int i, temp;
for(i=(nWords)*2 - 1; i>=0; i-=4)
{
temp = CompareWords(pInOut[i],pInOut[i-3]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 3;
}
}
*pDifStart=0;
return 0;
}
//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 1Q and 2Q
inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
{
int i, temp;
for(i=(nWords)*2 - 2; i>=0; i-=4)
{
temp = CompareWords(pInOut[i],pInOut[i-1]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+2;
return 1;
}
else
{
*pDifStart = i+2;
return 2;
}
}
*pDifStart=0;
return 1;
}
//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in iQ and jQ
inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart)
{
int i, temp;
for(i=(nWords)*2 - 1; i>=0; i-=4)
{
temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 1;
}
}
*pDifStart=0;
return iQ;
}
// same as minTemp2_fast but this one has a start position
inline int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart)
{
int i, temp;
for(i=start-1; i>=finish; i-=4)
{
temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 1;
}
}
*pDifStart=0;
return iQ;
}
// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
{
int min1, min2, DifStart0, DifStart1, DifStartMin;
int M[2];
unsigned temp[2048];
M[0] = minTemp0_fast_iVar5(pInOut, nWords, &DifStart0); // 0, 3
M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
{
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], pCanonPerm, pCanonPhase);
}
else
{
if(DifStartMin>=DifStart0)
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
else
{
min2 = minTemp3_fast_iVar5(pInOut, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
if(DifStart1>DifStartMin)
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
}
}
}
////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
// It rearranges InOut (swaps and flips through rearrangement of quoters)
// It updates Info at the end
inline void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int start, int iQ, int jQ, int kQ, int lQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
{
int i,wordBlock,blockSize,shiftSize;
word* tempPtr = temp+start;
if(iQ == 0 && jQ == 1)
return;
wordBlock = (1<<(iVar-6));
blockSize = wordBlock*sizeof(word);
shiftSize = wordBlock*4;
for(i=start-wordBlock;i>0;i-=shiftSize)
{
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize);
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize);
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize);
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);
}
memcpy(pInOut, temp, start*sizeof(word));
updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
}
//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 0Q and 3Q
inline int minTemp0_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
{
int i, j, temp;
int wordBlock = 1<<(iVar-6);
int wordDif = 3*wordBlock;
int shiftBlock = wordBlock*4;
for(i=nWords - 1; i>=0; i-=shiftBlock)
for(j=0;j<wordBlock;j++)
{
temp = CompareWords(pInOut[i-j],pInOut[i-j-wordDif]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 3;
}
}
*pDifStart=0;
return 0;
}
//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in 1Q and 2Q
inline int minTemp1_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
{
int i, j, temp;
int wordBlock = 1<<(iVar-6);
int shiftBlock = wordBlock*4;
for(i=nWords - wordBlock - 1; i>=0; i-=shiftBlock)
for(j=0;j<wordBlock;j++)
{
temp = CompareWords(pInOut[i-j],pInOut[i-j-wordBlock]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+wordBlock+1;
return 1;
}
else
{
*pDifStart = i+wordBlock+1;
return 2;
}
}
*pDifStart=0;
return 1;
}
//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
// DifStart contains the information about the first different bit in iQ and jQ
inline int minTemp2_fast_moreThen5(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
{
int i, j, temp;
int wordBlock = 1<<(iVar-6);
int shiftBlock = wordBlock*4;
for(i=nWords - 1; i>=0; i-=shiftBlock)
for(j=0;j<wordBlock;j++)
{
temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 1;
}
}
*pDifStart=0;
return iQ;
}
// same as minTemp2_fast but this one has a start position
inline int minTemp3_fast_moreThen5(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
{
int i, j, temp;
int wordBlock = 1<<(iVar-6);
int shiftBlock = wordBlock*4;
for(i=start-1; i>=finish; i-=shiftBlock)
for(j=0;j<wordBlock;j++)
{
temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
if(temp == 0)
continue;
else if(temp == -1)
{
*pDifStart = i+1;
return 0;
}
else
{
*pDifStart = i+1;
return 1;
}
}
*pDifStart=0;
return iQ;
}
// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
{
int min1, min2, DifStart0, DifStart1, DifStartMin;
int M[2];
word temp[1024];
int blockSize = 1<<(iVar-6);
int shiftSize = blockSize*4;
M[0] = minTemp0_fast_moreThen5(pInOut, iVar, nWords, &DifStart0); // 0, 3
M[1] = minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast_moreThen5(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
{
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], iVar, pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], iVar, pCanonPerm, pCanonPhase);
}
else
{
if(DifStartMin>=DifStart0)
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
else
{
min2 = minTemp3_fast_moreThen5(pInOut, iVar, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
if(DifStart1>DifStartMin)
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, pCanonPerm, pCanonPhase);
else
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
}
}
}
/////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase)
{
word oneWord=1;
if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
{
Kit_TruthNot_64bit( pInOut, nVars );
(* pCanonPhase) ^=(1<<nVars);
}
}
// this function finds minimal for all TIED(and tied only) iVars
//it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store
inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
{
int i;
word pDuplicate[1024];
int bitInfoTemp = pStore[0];
memcpy(pDuplicate,pInOut,nWords*sizeof(word));
for(i=0;i<5;i++)
{
if(bitInfoTemp == pStore[i+1])
minimalSwapAndFlipIVar_superFast_lessThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
else
{
bitInfoTemp = pStore[i+1];
continue;
}
}
if(bitInfoTemp == pStore[i+1])
minimalSwapAndFlipIVar_superFast_iVar5((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
else
bitInfoTemp = pStore[i+1];
for(i=6;i<nVars-1;i++)
{
if(bitInfoTemp == pStore[i+1])
minimalSwapAndFlipIVar_superFast_moreThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
else
{
bitInfoTemp = pStore[i+1];
continue;
}
}
if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
return 0;
else
return 1;
}
inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
{
minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
continue;
}
inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
{
// word pDuplicateLocal[1024]={0};
// memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
assert( nVars <= 16 );
assert( nVars > 6 );
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
luckyCanonicizerS_F_first_16Vars(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
// memcpy(pDuplicate,pInOut,nWords*sizeof(word));
// assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
}
// top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
{
int pStore[16];
int uCanonPhase = 0;
int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
if ( nVars <= 6 )
pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
else if ( nVars <= 16 )
luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
else assert( 0 );
return uCanonPhase;
}
ABC_NAMESPACE_IMPL_END

233
src/bool/lucky/luckyFast6.c Normal file
View File

@ -0,0 +1,233 @@
/**CFile****************************************************************
FileName [luckyFast6.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Semi-canonical form computation package.]
Synopsis [Truth table minimization procedures for 6 vars.]
Author [Jake]
Date [Started - September 2012]
***********************************************************************/
#include "luckyInt.h"
ABC_NAMESPACE_IMPL_START
inline void resetPCanonPermArray_6Vars(char* x)
{
x[0]='a';
x[1]='b';
x[2]='c';
x[3]='d';
x[4]='e';
x[5]='f';
}
inline void resetPCanonPermArray(char* x, int nVars)
{
int i;
for(i=0;i<nVars;i++)
x[i] = 'a'+i;
}
// we need next two functions only for verification of lucky method in debugging mode
void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
{
int Temp;
swap_ij(pAfter, nVars, iVarInPosition, jVar);
Temp = pCanonPerm[iVarInPosition];
pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
pCanonPerm[jVar] = Temp;
if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
{
*pUCanonPhase ^= (1 << iVarInPosition);
*pUCanonPhase ^= (1 << jVar);
}
if(*pUCanonPhase>>iVarInPosition & (unsigned)1 == 1)
Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
}
int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
{
int i,j;
char tempChar;
for(j=0;j<nVars;j++)
{
tempChar = 'a'+ j;
for(i=j;i<nVars;i++)
{
if(tempChar != pCanonPerm[i])
continue;
swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
break;
}
}
if(uCanonPhase>>nVars & (unsigned)1 == 1)
Kit_TruthNot_64bit(pAfter, nVars );
if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
return 0;
else
return 1;
}
inline word Abc_allFlip(word x, unsigned* pCanonPhase)
{
if( (x>>63) )
{
(* pCanonPhase) ^=(1<<6);
return ~x;
}
else
return x;
}
inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
{
if(info<4)
return (uCanonPhase ^= (info << iVar));
else
{
char temp;
uCanonPhase ^= ((info-4) << iVar);
temp=pCanonPerm[iVar];
pCanonPerm[iVar]=pCanonPerm[iVar+1];
pCanonPerm[iVar+1]=temp;
if ( ((uCanonPhase & (1 << iVar)) > 0) != ((uCanonPhase & (1 << (iVar+1))) > 0) )
{
uCanonPhase ^= (1 << iVar);
uCanonPhase ^= (1 << (iVar+1));
}
return uCanonPhase;
}
}
inline word Extra_Truth6SwapAdjacent( word t, int iVar )
{
// variable swapping code
static word PMasks[5][3] = {
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
{ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
{ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
};
assert( iVar < 5 );
return (t & PMasks[iVar][0]) | ((t & PMasks[iVar][1]) << (1 << iVar)) | ((t & PMasks[iVar][2]) >> (1 << iVar));
}
inline word Extra_Truth6ChangePhase( word t, int iVar)
{
// elementary truth tables
static word Truth6[6] = {
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
assert( iVar < 6 );
return ((t & ~Truth6[iVar]) << (1 << iVar)) | ((t & Truth6[iVar]) >> (1 << iVar));
}
inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, unsigned* pCanonPhase )
{
word tCur, tMin = t; // ab
unsigned info =0;
assert( iVar >= 0 && iVar < 5 );
tCur = Extra_Truth6ChangePhase( t, iVar ); // !a b
if(tCur<tMin)
{
info = 1;
tMin = tCur;
}
tCur = Extra_Truth6ChangePhase( t, iVar+1 ); // a !b
if(tCur<tMin)
{
info = 2;
tMin = tCur;
}
tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !a !b
if(tCur<tMin)
{
info = 3;
tMin = tCur;
}
t = Extra_Truth6SwapAdjacent( t, iVar ); // b a
if(t<tMin)
{
info = 4;
tMin = t;
}
tCur = Extra_Truth6ChangePhase( t, iVar ); // !b a
if(tCur<tMin)
{
info = 6;
tMin = tCur;
}
tCur = Extra_Truth6ChangePhase( t, iVar+1 ); // b !a
if(tCur<tMin)
{
info = 5;
tMin = tCur;
}
tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !b !a
if(tCur<tMin)
{
(* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, 7);
return tCur;
}
else
{
(* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, info);
return tMin;
}
}
// this function finds minimal for all TIED(and tied only) iVars
//it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store
inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
{
int i, bitInfoTemp;
word tMin0, tMin;
tMin=Abc_allFlip(t, pCanonPhase);
do
{
bitInfoTemp = pStore[0];
tMin0 = tMin;
for ( i = 0; i < 5; i++ )
{
if(bitInfoTemp == pStore[i+1])
tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
else
bitInfoTemp = pStore[i+1];
}
}while ( tMin0 != tMin );
return tMin;
}
inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
{
// word temp, duplicat = InOut;
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
// InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
// temp = InOut;
// assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
// return(InOut);
return Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPerm, pCanonPhase );
}
ABC_NAMESPACE_IMPL_END

34
src/bool/lucky/luckyInt.h
View File

@ -24,6 +24,7 @@
#include <math.h>
#include <time.h>
// comment out this line to run Lucky Code outside of ABC
#define _RUNNING_ABC_
@ -80,6 +81,8 @@ typedef struct
int totalFlips;
}permInfo;
static inline void TimePrint( char* Message )
{
static int timeBegin;
@ -89,6 +92,25 @@ static inline void TimePrint( char* Message )
timeBegin = clock();
}
static word SFmask[5][4] = {
{0x8888888888888888,0x4444444444444444,0x2222222222222222,0x1111111111111111},
{0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
{0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
{0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
{0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
};
static inline int CompareWords(word x, word y)
{
if(x>y)
return 1;
else if(x<y)
return -1;
else
return 0;
}
extern inline int memCompare(word* x, word* y, int nVars);
extern inline int Kit_TruthWordNum_64bit( int nVars );
extern Abc_TtStore_t * setTtStore(char * pFileInput);
@ -101,8 +123,16 @@ extern inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars );
extern void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
extern permInfo* setPermInfoPtr(int var);
extern void freePermInfoPtr(permInfo* x);
extern inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm );
extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm );
extern inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
extern inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore );
extern inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase );
extern inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
extern inline void resetPCanonPermArray_6Vars(char* x);
extern void swap_ij( word* f,int totalVars, int varI, int varJ);
extern inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
extern inline void resetPCanonPermArray(char* x, int nVars);
ABC_NAMESPACE_HEADER_END

117
src/bool/lucky/luckySwap.c
View File

@ -16,6 +16,7 @@
#include "luckyInt.h"
ABC_NAMESPACE_IMPL_START
@ -205,7 +206,69 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
if ( pStore[i] <= nOnes-pStore[i])
if ( pStore[i] >= nOnes-pStore[i])
continue;
uCanonPhase |= (1 << i);
pStore[i] = nOnes-pStore[i];
Kit_TruthChangePhase_64bit( pInOut, nVars, i );
}
do {
fChange = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pStore[i] <= pStore[i+1] )
continue;
fChange = 1;
Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[i+1];
pCanonPerm[i+1] = Temp;
Temp = pStore[i];
pStore[i] = pStore[i+1];
pStore[i+1] = Temp;
// if the polarity of variables is different, swap them
if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
{
uCanonPhase ^= (1 << i);
uCanonPhase ^= (1 << (i+1));
}
Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
return uCanonPhase;
}
inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
{
int nWords = Kit_TruthWordNum_64bit( nVars );
int i, fChange, nOnes;
int Temp;
unsigned uCanonPhase=0;
assert( nVars <= 16 );
nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
// if ( (nOnes == nWords * 32) )
// return 999999;
if ( (nOnes > nWords * 32) )
{
uCanonPhase |= (1 << nVars);
Kit_TruthNot_64bit( pInOut, nVars );
nOnes = nWords*64 - nOnes;
}
// collect the minterm counts
Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
// if ( pStore[i] == nOnes-pStore[i])
// return 999999;
if ( pStore[i] >= nOnes-pStore[i])
continue;
uCanonPhase |= (1 << i);
pStore[i] = nOnes-pStore[i];
@ -241,10 +304,55 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
return uCanonPhase;
}
inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
// inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
// {
// unsigned uCanonPhase = 0;
// int pStore[16];
// int nWords = Kit_TruthWordNum_64bit( nVars );
// int i, Temp, fChange, nOnes;
// assert( nVars <= 16 );
//
// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
//
// if ( (nOnes > nWords * 32) )
// {
// Kit_TruthNot_64bit( pInOut, nVars );
// nOnes = nWords*64 - nOnes;
// }
//
// // collect the minterm counts
// Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
//
// // canonicize phase
// for ( i = 0; i < nVars; i++ )
// {
// if ( pStore[i] >= nOnes-pStore[i])
// continue;
// pStore[i] = nOnes-pStore[i];
// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
// }
//
// do {
// fChange = 0;
// for ( i = 0; i < nVars-1; i++ )
// {
// if ( pStore[i] <= pStore[i+1] )
// continue;
// fChange = 1;
//
// Temp = pStore[i];
// pStore[i] = pStore[i+1];
// pStore[i+1] = Temp;
//
// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
// }
// } while ( fChange );
// return uCanonPhase;
// }
inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore )
{
unsigned uCanonPhase = 0;
int pStore[16];
int nWords = Kit_TruthWordNum_64bit( nVars );
int i, Temp, fChange, nOnes;
assert( nVars <= 16 );
@ -284,7 +392,6 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars,
Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
return uCanonPhase;
}

102
src/bool/lucky/luckySwapIJ.c Normal file
View File

@ -0,0 +1,102 @@
/**CFile****************************************************************
FileName [luckySwapIJ.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Semi-canonical form computation package.]
Synopsis [just for support of swap_ij() function]
Author [Jake]
Date [Started - September 2012]
***********************************************************************/
#include "luckyInt.h"
ABC_NAMESPACE_IMPL_START
void swap_ij_case1( word* f,int totalVars, int i, int j)
{
int e,wordsNumber,n,shift;
word maskArray[45]=
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 ,0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 ,
0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 ,0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 ,
0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 ,0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 ,
0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 ,0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 ,
0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 ,0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 ,
0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 ,0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 ,
0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000
};
e = 3*((9*i - i*i -2)/2 + j); // Exact formula for index in maskArray
wordsNumber = Kit_TruthWordNum_64bit(totalVars);
shift = (1<<j)-(1<<i);
for(n = 0; n < wordsNumber; n++)
f[n] = (f[n]&maskArray[e])+((f[n]&(maskArray[e+1]))<< shift)+((f[n]&(maskArray[e+2]))>> shift);
}
// "width" - how many "Words" in a row have "1s" (or "0s")in position "i"
// wi - width of i
// wj - width of j
// wwi = 2*wi; wwj = 2*wj;
void swap_ij_case2( word* f,int totalVars, int i, int j)
{
word mask[] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
word temp;
int x,y,wj;
int WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
// int forShift = ((Word)1)<<i;
int forShift = (1<<i);
wj = 1 << (j - 6);
x = 0;
y = wj;
for(y=wj; y<WORDS_IN_TT;y+=2*wj)
for(x=y-wj; x < y; x++)
{
temp = f[x+wj];
f[x+wj] = ((f[x+wj])&(mask[i])) + (((f[x]) & (mask[i])) >> forShift);
f[x] = ((f[x])&(~mask[i])) + ((temp&(~mask[i])) << forShift);
}
}
void swap_ij_case3( word* f,int totalVars, int i, int j)
{
int x,y,wwi,wwj,shift;
int WORDS_IN_TT;
int SizeOfBlock;
word* temp;
wwi = 1 << (i - 5);
wwj = 1 << (j - 5);
shift = (wwj - wwi)/2;
WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
SizeOfBlock = sizeof(word)*wwi/2;
temp = malloc(SizeOfBlock);
for(y=wwj/2; y<WORDS_IN_TT; y+=wwj)
for(x=y-shift; x<y; x+=wwi)
{
memcpy(temp,&f[x],SizeOfBlock);
memcpy(&f[x],&f[x+shift],SizeOfBlock);
memcpy(&f[x+shift],temp,SizeOfBlock);
}
}
void swap_ij( word* f,int totalVars, int varI, int varJ)
{
if (varI == varJ)
return;
else if(varI>varJ)
swap_ij( f,totalVars,varJ,varI);
else if((varI <= 4) && (varJ <= 5))
swap_ij_case1(f,totalVars, varI, varJ);
else if((varI <= 5) && (varJ > 5))
swap_ij_case2(f,totalVars, varI, varJ);
else if((varI > 5) && (varJ > 5))
swap_ij_case3(f,totalVars,varI,varJ);
}
ABC_NAMESPACE_IMPL_END

3
src/bool/lucky/module.make
View File

@ -1,3 +1,6 @@
SRC += src/bool/lucky/lucky.c \
src/bool/lucky/luckyFast16.c \
src/bool/lucky/luckyFast6.c \
src/bool/lucky/luckyRead.c \
src/bool/lucky/luckySwapIJ.c \
src/bool/lucky/luckySwap.c

2
src/map/if/ifDec16.c
View File

@ -1585,7 +1585,7 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, in
short pStore[32];
unsigned uCanonPhase;
If_CluCopy( pF, pTruth, nVars );
uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore );
uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm );
G1.nVars = 1;
return G1;
}