mirror of https://github.com/YosysHQ/abc.git
Changes to the matching procedure and new abstraction code.
This commit is contained in:
Alan Mishchenko
parent
976f5f5a12
commit
519b03e8e8
|
|
@ -2039,7 +2039,7 @@ SOURCE=.\src\map\if\ifDec10.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
SOURCE=.\src\map\if\ifDec10f.c
|
SOURCE=.\src\map\if\ifDec16.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
|
|
@ -3507,6 +3507,10 @@ SOURCE=.\src\aig\saig\saigAbsStart.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\saig\saigAbsVfa.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
SOURCE=.\src\aig\saig\saigBmc.c
|
SOURCE=.\src\aig\saig\saigBmc.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
|
||||||
|
|
@ -2,6 +2,7 @@ SRC += src/aig/saig/saigAbs.c \
|
||||||
src/aig/saig/saigAbsCba.c \
|
src/aig/saig/saigAbsCba.c \
|
||||||
src/aig/saig/saigAbsPba.c \
|
src/aig/saig/saigAbsPba.c \
|
||||||
src/aig/saig/saigAbsStart.c \
|
src/aig/saig/saigAbsStart.c \
|
||||||
|
src/aig/saig/saigAbsVfa.c \
|
||||||
src/aig/saig/saigBmc.c \
|
src/aig/saig/saigBmc.c \
|
||||||
src/aig/saig/saigBmc2.c \
|
src/aig/saig/saigBmc2.c \
|
||||||
src/aig/saig/saigBmc3.c \
|
src/aig/saig/saigBmc3.c \
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,328 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [saigAbsVfa.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Sequential AIG package.]
|
||||||
|
|
||||||
|
Synopsis [Intergrated abstraction procedure.]
|
||||||
|
|
||||||
|
Author [Alan Mishchenko]
|
||||||
|
|
||||||
|
Affiliation [UC Berkeley]
|
||||||
|
|
||||||
|
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||||
|
|
||||||
|
Revision [$Id: saigAbsVfa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "saig.h"
|
||||||
|
#include "cnf.h"
|
||||||
|
#include "satSolver.h"
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
typedef struct Abs_VfaMan_t_ Abs_VfaMan_t;
|
||||||
|
struct Abs_VfaMan_t_
|
||||||
|
{
|
||||||
|
Aig_Man_t * pAig;
|
||||||
|
int nConfLimit;
|
||||||
|
int fVerbose;
|
||||||
|
// unrolling info
|
||||||
|
int iFrame;
|
||||||
|
int nFrames;
|
||||||
|
Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
|
||||||
|
Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
|
||||||
|
Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
|
||||||
|
Vec_Int_t * vFra2Var; // maps frame number into the first variable
|
||||||
|
// SAT solver
|
||||||
|
sat_solver * pSat;
|
||||||
|
Cnf_Dat_t * pCnf;
|
||||||
|
Vec_Int_t * vAssumps;
|
||||||
|
Vec_Int_t * vCore;
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Adds CNF clauses for the MUX.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Abs_VfaManSatMux( sat_solver * pSat, int VarF, int VarI, int VarT, int VarE )
|
||||||
|
{
|
||||||
|
int RetValue, pLits[3];
|
||||||
|
|
||||||
|
// f = ITE(i, t, e)
|
||||||
|
|
||||||
|
// i' + t' + f
|
||||||
|
// i' + t + f'
|
||||||
|
// i + e' + f
|
||||||
|
// i + e + f'
|
||||||
|
|
||||||
|
// create four clauses
|
||||||
|
pLits[0] = toLitCond(VarI, 1);
|
||||||
|
pLits[1] = toLitCond(VarT, 1);
|
||||||
|
pLits[2] = toLitCond(VarF, 0);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
|
||||||
|
pLits[0] = toLitCond(VarI, 1);
|
||||||
|
pLits[1] = toLitCond(VarT, 0);
|
||||||
|
pLits[2] = toLitCond(VarF, 1);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
|
||||||
|
pLits[0] = toLitCond(VarI, 0);
|
||||||
|
pLits[1] = toLitCond(VarE, 1);
|
||||||
|
pLits[2] = toLitCond(VarF, 0);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
|
||||||
|
pLits[0] = toLitCond(VarI, 0);
|
||||||
|
pLits[1] = toLitCond(VarE, 0);
|
||||||
|
pLits[2] = toLitCond(VarF, 1);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
|
||||||
|
// two additional clauses
|
||||||
|
// t' & e' -> f'
|
||||||
|
// t & e -> f
|
||||||
|
|
||||||
|
// t + e + f'
|
||||||
|
// t' + e' + f
|
||||||
|
assert( VarT != VarE );
|
||||||
|
|
||||||
|
pLits[0] = toLitCond(VarT, 0);
|
||||||
|
pLits[1] = toLitCond(VarE, 0);
|
||||||
|
pLits[2] = toLitCond(VarF, 1);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
|
||||||
|
pLits[0] = toLitCond(VarT, 1);
|
||||||
|
pLits[1] = toLitCond(VarE, 1);
|
||||||
|
pLits[2] = toLitCond(VarF, 0);
|
||||||
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
|
||||||
|
assert( RetValue );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Abs_VfaManAddVar( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f, int * pfNew )
|
||||||
|
{
|
||||||
|
int i, SatId, VecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
|
||||||
|
*pfNew = 0;
|
||||||
|
if ( VecId == -1 )
|
||||||
|
return -1;
|
||||||
|
if ( VecId == 0 )
|
||||||
|
{
|
||||||
|
VecId = Vec_IntSize( p->vVec2Var ) / p->nFrames;
|
||||||
|
for ( i = 0; i < p->nFrames; i++ )
|
||||||
|
Vec_IntPush( p->vVec2Var, 0 );
|
||||||
|
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), VecId );
|
||||||
|
}
|
||||||
|
SatId = Vec_IntEntry( p->vVec2Var, p->nFrames * VecId + f );
|
||||||
|
if ( SatId )
|
||||||
|
return SatId;
|
||||||
|
SatId = Vec_IntSize( p->vVar2Inf ) / 2;
|
||||||
|
// save SatId
|
||||||
|
Vec_IntWriteEntry( p->vVec2Var, p->nFrames * VecId + f, SatId );
|
||||||
|
Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
|
||||||
|
Vec_IntPush( p->vVar2Inf, f );
|
||||||
|
if ( Saig_ObjIsLo( p->pAig, pObj ) ) // reserve IDs for aux vars
|
||||||
|
{
|
||||||
|
Vec_IntPush( p->vVar2Inf, -1 );
|
||||||
|
Vec_IntPush( p->vVar2Inf, f );
|
||||||
|
Vec_IntPush( p->vVar2Inf, -2 );
|
||||||
|
Vec_IntPush( p->vVar2Inf, f );
|
||||||
|
}
|
||||||
|
*pfNew = 1;
|
||||||
|
return SatId;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f )
|
||||||
|
{
|
||||||
|
int SatVar, fNew;
|
||||||
|
if ( Aig_ObjIsConst1(pObj) )
|
||||||
|
return -1;
|
||||||
|
SatVar = Abs_VfaManAddVar( p, pObj, f, &fNew );
|
||||||
|
if ( (SatVar > 0 && !fNew) || Saig_ObjIsPi(p->pAig, pObj) || (Aig_ObjIsPi(pObj) && f==0) )
|
||||||
|
return SatVar;
|
||||||
|
if ( Aig_ObjIsPo(pObj) )
|
||||||
|
return Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f );
|
||||||
|
if ( Aig_ObjIsPi(pObj) )
|
||||||
|
return Abs_VfaManCreateFrame_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1 );
|
||||||
|
assert( Aig_ObjIsAnd(pObj) );
|
||||||
|
Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f );
|
||||||
|
Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin1(pObj), f );
|
||||||
|
return SatVar;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Abs_VfaManCreateFrame( Abs_VfaMan_t * p, int f )
|
||||||
|
{
|
||||||
|
Aig_Obj_t * pObj;
|
||||||
|
int i, clk = clock();
|
||||||
|
|
||||||
|
Saig_ManForEachPo( p->pAig, pObj, i )
|
||||||
|
Abs_VfaManCreateFrame_rec( p, pObj, f );
|
||||||
|
|
||||||
|
Vec_IntPush( p->vFra2Var, Vec_IntSize( p->vVar2Inf ) / 2 );
|
||||||
|
|
||||||
|
printf( "Frame = %3d : ", f );
|
||||||
|
printf( "Vecs = %8d ", Vec_IntSize( p->vVec2Var ) / p->nFrames );
|
||||||
|
printf( "Vars = %8d ", Vec_IntSize( p->vVar2Inf ) / 2 );
|
||||||
|
Abc_PrintTime( 1, "Time", clock() - clk );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Abs_VfaMan_t * Abs_VfaManStart( Aig_Man_t * pAig )
|
||||||
|
{
|
||||||
|
Abs_VfaMan_t * p;
|
||||||
|
int i;
|
||||||
|
|
||||||
|
p = ABC_CALLOC( Abs_VfaMan_t, 1 );
|
||||||
|
p->pAig = pAig;
|
||||||
|
p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
|
||||||
|
p->vVec2Var = Vec_IntAlloc( 1 << 20 );
|
||||||
|
p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
|
||||||
|
p->vFra2Var = Vec_IntStart( 1 );
|
||||||
|
|
||||||
|
// skip the first variable
|
||||||
|
Vec_IntPush( p->vVar2Inf, -3 );
|
||||||
|
Vec_IntPush( p->vVar2Inf, -3 );
|
||||||
|
for ( i = 0; i < p->nFrames; i++ )
|
||||||
|
Vec_IntPush( p->vVec2Var, -1 );
|
||||||
|
|
||||||
|
// transfer values from CNF
|
||||||
|
p->pCnf = Cnf_DeriveOther( pAig );
|
||||||
|
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
|
||||||
|
if ( p->pCnf->pObj2Clause[i] == -1 )
|
||||||
|
Vec_IntWriteEntry( p->vObj2Vec, i, -1 );
|
||||||
|
|
||||||
|
p->vAssumps = Vec_IntAlloc( 100 );
|
||||||
|
p->vCore = Vec_IntAlloc( 100 );
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Abs_VfaManStop( Abs_VfaMan_t * p )
|
||||||
|
{
|
||||||
|
Vec_IntFreeP( &p->vObj2Vec );
|
||||||
|
Vec_IntFreeP( &p->vVec2Var );
|
||||||
|
Vec_IntFreeP( &p->vVar2Inf );
|
||||||
|
Vec_IntFreeP( &p->vFra2Var );
|
||||||
|
Vec_IntFreeP( &p->vAssumps );
|
||||||
|
Vec_IntFreeP( &p->vCore );
|
||||||
|
if ( p->pCnf )
|
||||||
|
Cnf_DataFree( p->pCnf );
|
||||||
|
if ( p->pSat )
|
||||||
|
sat_solver_delete( p->pSat );
|
||||||
|
ABC_FREE( p );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Perform variable frame abstraction.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose )
|
||||||
|
{
|
||||||
|
Abs_VfaMan_t * p;
|
||||||
|
int i;
|
||||||
|
|
||||||
|
p = Abs_VfaManStart( pAig );
|
||||||
|
p->nFrames = nFrames;
|
||||||
|
p->nConfLimit = nConfLimit;
|
||||||
|
p->fVerbose = fVerbose;
|
||||||
|
|
||||||
|
|
||||||
|
// create unrolling for the given number of frames
|
||||||
|
for ( i = 0; i < p->nFrames; i++ )
|
||||||
|
Abs_VfaManCreateFrame( p, i );
|
||||||
|
|
||||||
|
|
||||||
|
Abs_VfaManStop( p );
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_END
|
||||||
|
|
||||||
|
|
@ -903,8 +903,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
||||||
}
|
}
|
||||||
*/
|
*/
|
||||||
{
|
{
|
||||||
extern void If_CluTest();
|
// extern void If_CluTest();
|
||||||
If_CluTest();
|
// If_CluTest();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -8861,8 +8861,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
*/
|
*/
|
||||||
|
|
||||||
{
|
{
|
||||||
void Bdc_SpfdDecomposeTest();
|
extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
|
||||||
Bdc_SpfdDecomposeTest();
|
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||||
|
if ( pNtk )
|
||||||
|
{
|
||||||
|
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
|
||||||
|
Abs_VfaManTest( pAig, 32, 1000000, 1 );
|
||||||
|
Aig_ManStop( pAig );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
{
|
||||||
|
// void Bdc_SpfdDecomposeTest();
|
||||||
|
// Bdc_SpfdDecomposeTest();
|
||||||
}
|
}
|
||||||
return 0;
|
return 0;
|
||||||
usage:
|
usage:
|
||||||
|
|
|
||||||
|
|
@ -27,17 +27,16 @@ ABC_NAMESPACE_IMPL_START
|
||||||
/// DECLARATIONS ///
|
/// DECLARATIONS ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
#define CLU_MAX 16
|
#define CLU_VAR_MAX 16
|
||||||
|
#define CLU_WRD_MAX (1 << ((CLU_VAR_MAX)-6))
|
||||||
|
|
||||||
// decomposition
|
// decomposition
|
||||||
typedef struct If_Bst_t_ If_Bst_t;
|
typedef struct If_Grp_t_ If_Grp_t;
|
||||||
struct If_Bst_t_
|
struct If_Grp_t_
|
||||||
{
|
{
|
||||||
int nMyu;
|
char nVars;
|
||||||
int nVars;
|
char nMyu;
|
||||||
int Vars[CLU_MAX];
|
char pVars[6];
|
||||||
float Dels[CLU_MAX];
|
|
||||||
word Truth[1 << (CLU_MAX-6)];
|
|
||||||
};
|
};
|
||||||
|
|
||||||
// the bit count for the first 256 integer numbers
|
// the bit count for the first 256 integer numbers
|
||||||
|
|
@ -68,7 +67,7 @@ static word Truth6[6] = {
|
||||||
0xFFFF0000FFFF0000,
|
0xFFFF0000FFFF0000,
|
||||||
0xFFFFFFFF00000000
|
0xFFFFFFFF00000000
|
||||||
};
|
};
|
||||||
static word TruthAll[CLU_MAX][1 << (CLU_MAX-6)];
|
static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX];
|
||||||
|
|
||||||
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
|
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
|
||||||
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
|
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
|
||||||
|
|
@ -84,12 +83,12 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
|
||||||
void If_CluInitTruthTables()
|
void If_CluInitTruthTables()
|
||||||
{
|
{
|
||||||
int i, k;
|
int i, k;
|
||||||
assert( CLU_MAX <= 16 );
|
assert( CLU_VAR_MAX <= 16 );
|
||||||
for ( i = 0; i < 6; i++ )
|
for ( i = 0; i < 6; i++ )
|
||||||
for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
|
for ( k = 0; k < CLU_WRD_MAX; k++ )
|
||||||
TruthAll[i][k] = Truth6[i];
|
TruthAll[i][k] = Truth6[i];
|
||||||
for ( i = 6; i < CLU_MAX; i++ )
|
for ( i = 6; i < CLU_VAR_MAX; i++ )
|
||||||
for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
|
for ( k = 0; k < CLU_WRD_MAX; k++ )
|
||||||
TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0;
|
TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -104,6 +103,14 @@ static inline void If_CluCopy( word * pOut, word * pIn, int nVars )
|
||||||
for ( w = 0; w < nWords; w++ )
|
for ( w = 0; w < nWords; w++ )
|
||||||
pOut[w] = pIn[w];
|
pOut[w] = pIn[w];
|
||||||
}
|
}
|
||||||
|
static inline int If_CluEqual( word * pOut, word * pIn, int nVars )
|
||||||
|
{
|
||||||
|
int w, nWords = If_CluWordNum( nVars );
|
||||||
|
for ( w = 0; w < nWords; w++ )
|
||||||
|
if ( pOut[w] != pIn[w] )
|
||||||
|
return 0;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
|
static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
|
||||||
{
|
{
|
||||||
int i, k, nWords = If_CluWordNum( nVars );
|
int i, k, nWords = If_CluWordNum( nVars );
|
||||||
|
|
@ -144,7 +151,7 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV
|
||||||
// moves one var (v) to the given position (p)
|
// moves one var (v) to the given position (p)
|
||||||
void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
|
void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p )
|
||||||
{
|
{
|
||||||
word pG[1 << (CLU_MAX-6)], * pIn = pF, * pOut = pG, * pTemp;
|
word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp;
|
||||||
int iPlace0, iPlace1, Count = 0;
|
int iPlace0, iPlace1, Count = 0;
|
||||||
assert( v >= 0 && v < nVars );
|
assert( v >= 0 && v < nVars );
|
||||||
if ( Var2Pla[v] <= p )
|
if ( Var2Pla[v] <= p )
|
||||||
|
|
@ -185,27 +192,59 @@ void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, i
|
||||||
}
|
}
|
||||||
|
|
||||||
// moves vars to be the most signiticant ones (Group[0] is MSB)
|
// moves vars to be the most signiticant ones (Group[0] is MSB)
|
||||||
void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, word Group )
|
void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
|
||||||
{
|
{
|
||||||
char * pVars = (char *)&Group;
|
|
||||||
int v;
|
int v;
|
||||||
for ( v = 0; v < pVars[7]; v++ )
|
for ( v = 0; v < g->nVars; v++ )
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, pVars[pVars[7] - 1 - v], nVars - 1 - v );
|
If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v );
|
||||||
}
|
}
|
||||||
|
|
||||||
// return the number of cofactors w.r.t. the topmost vars (nBSsize)
|
// return the number of cofactors w.r.t. the topmost vars (nBSsize)
|
||||||
int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift )
|
int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word * pCofs[2] )
|
||||||
|
{
|
||||||
|
word iCofs[64], iCof;
|
||||||
|
int i, c, w, nMints = (1 << nBSsize), nCofs;
|
||||||
|
|
||||||
|
assert( nBSsize < nVars );
|
||||||
|
assert( nBSsize >= 3 && nBSsize <= 6 );
|
||||||
|
|
||||||
|
if ( nVars - nBSsize >= 6 )
|
||||||
|
{
|
||||||
|
word * pCofA, * pCofB;
|
||||||
|
int nWords = (1 << (nVars - nBSsize - 6));
|
||||||
|
assert( nWords * nMints == If_CluWordNum(nVars) );
|
||||||
|
for ( nCofs = i = 0; i < nMints; i++ )
|
||||||
|
{
|
||||||
|
for ( c = 0; c < nCofs; c++ )
|
||||||
|
{
|
||||||
|
pCofA = pF + i * nWords;
|
||||||
|
pCofB = pF + iCofs[c] * nWords;
|
||||||
|
for ( w = 0; w < nWords; w++ )
|
||||||
|
if ( pCofA[w] != pCofB[w] )
|
||||||
|
break;
|
||||||
|
if ( w == nWords )
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if ( c == nCofs )
|
||||||
|
iCofs[nCofs++] = i;
|
||||||
|
if ( nCofs == 5 )
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if ( nCofs == 2 && pCofs )
|
||||||
|
{
|
||||||
|
for ( c = 0; c < nCofs; c++ )
|
||||||
|
{
|
||||||
|
word * pCofA = pF + iCofs[c] * nWords;
|
||||||
|
for ( w = 0; w < nWords; w++ )
|
||||||
|
pCofs[c][w] = pCofA[w];
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
{
|
{
|
||||||
int nShift = (1 << (nVars - nBSsize));
|
int nShift = (1 << (nVars - nBSsize));
|
||||||
word Mask = (((word)1) << nShift) - 1;
|
word Mask = ((((word)1) << nShift) - 1);
|
||||||
word iCofs[64], iCof;
|
for ( nCofs = i = 0; i < nMints; i++ )
|
||||||
int i, c, nMints = (1 << nBSsize), nCofs = 1;
|
|
||||||
assert( nBSsize >= 3 && nBSsize <= 6 );
|
|
||||||
assert( nVars - nBSsize > 0 && nVars - nBSsize <= 6 );
|
|
||||||
if ( nVars - nBSsize == 6 )
|
|
||||||
Mask = ~0;
|
|
||||||
iCofs[0] = (pF[iShift / 64] >> (iShift & 63)) & Mask;
|
|
||||||
for ( i = 1; i < nMints; i++ )
|
|
||||||
{
|
{
|
||||||
iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask;
|
iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask;
|
||||||
for ( c = 0; c < nCofs; c++ )
|
for ( c = 0; c < nCofs; c++ )
|
||||||
|
|
@ -216,6 +255,7 @@ int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift )
|
||||||
if ( nCofs == 5 )
|
if ( nCofs == 5 )
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
}
|
||||||
assert( nCofs >= 2 && nCofs <= 5 );
|
assert( nCofs >= 2 && nCofs <= 5 );
|
||||||
return nCofs;
|
return nCofs;
|
||||||
}
|
}
|
||||||
|
|
@ -252,82 +292,123 @@ void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// derives non-disjoint decomposition (assumes the shared var in pG->pVars[pG->nVars-1]
|
||||||
|
word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * pG )
|
||||||
|
{
|
||||||
|
/*
|
||||||
|
word Truth, Truth0, Truth1;
|
||||||
|
word Cof[2][CLU_WRD_MAX], Cof0[2][CLU_WRD_MAX], Cof1[2][CLU_WRD_MAX];
|
||||||
|
int i, nFSvars, nFSHalfBits, nBSHalfBits;
|
||||||
|
assert( pG->nVars >= 3 && pG->nVar <= 6 );
|
||||||
|
assert( pG->nMyu == 3 || pG->nMyu == 4 );
|
||||||
|
|
||||||
|
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, pG );
|
||||||
|
|
||||||
|
If_CluCofactors( pF, nVars, nVars - 1, Cof[0], Cof[1] );
|
||||||
|
|
||||||
|
assert( 2 >= If_Dec6CofCount2(c0) );
|
||||||
|
assert( 2 >= If_Dec6CofCount2(c1) );
|
||||||
|
|
||||||
|
assert( 2 >= If_CluCountCofs( Cof[0], nVars - 1, pG->nVars - 1, 0 ) );
|
||||||
|
assert( 2 >= If_CluCountCofs( Cof[1], nVars - 1, pG->nVars - 1, 0 ) );
|
||||||
|
|
||||||
|
Truth0 = If_CluExtract2Cofs( Cof[0], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] );
|
||||||
|
Truth1 = If_CluExtract2Cofs( Cof[1], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] );
|
||||||
|
|
||||||
|
nFSHalfBits = (1 << (nVars - pG->nVars - 1));
|
||||||
|
nBSHalfBits = (1 << (pG->nVars - 1))
|
||||||
|
|
||||||
|
Truth = ((Truth0 && ((1 << nBSHalfBits) - 1)) << nBSHalfBits) | (Truth0 && ((1 << nBSHalfBits) - 1))
|
||||||
|
|
||||||
|
|
||||||
|
for ( i = 0; i < 4; i++ )
|
||||||
|
z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
|
||||||
|
z |= ((word)((Cof0[1] << 4) | Cof0[0]) << 32);
|
||||||
|
z |= ((word)((Cof1[1] << 4) | Cof1[0]) << 40);
|
||||||
|
for ( i = 0; i < 2; i++ )
|
||||||
|
z |= (((word)Pla2Var[i]) << (48 + 4*i));
|
||||||
|
z |= (((word)7) << (48 + 4*i++));
|
||||||
|
z |= (((word)Pla2Var[5]) << (48 + 4*i++));
|
||||||
|
assert( i == 4 );
|
||||||
|
return z;
|
||||||
|
*/
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
// check non-disjoint decomposition
|
// check non-disjoint decomposition
|
||||||
int If_CluCheckNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, int nBSsize, char * pGroup )
|
int If_CluCheckNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g )
|
||||||
{
|
{
|
||||||
int v, i, nCofsBest2;
|
int v, i, nCofsBest2;
|
||||||
if ( (pGroup[6] == 3 || pGroup[6] == 4) )
|
if ( (g->nMyu == 3 || g->nMyu == 4) )
|
||||||
{
|
{
|
||||||
word pCof0[1 << (CLU_MAX-6)];
|
word pCof0[CLU_WRD_MAX];
|
||||||
word pCof1[1 << (CLU_MAX-6)];
|
word pCof1[CLU_WRD_MAX];
|
||||||
// try cofactoring w.r.t. each variable
|
// try cofactoring w.r.t. each variable
|
||||||
for ( v = 0; v < pGroup[7]; v++ )
|
for ( v = 0; v < g->nVars; v++ )
|
||||||
{
|
{
|
||||||
If_CluCofactors( pF, nVars, pGroup[v], pCof0, pCof1 );
|
If_CluCofactors( pF, nVars, V2P[g->pVars[v]], pCof0, pCof1 );
|
||||||
nCofsBest2 = If_CluCountCofs( pCof0, nVars, nBSsize, 0 );
|
nCofsBest2 = If_CluCountCofs( pCof0, nVars, g->nVars, 0, NULL );
|
||||||
if ( nCofsBest2 > 2 )
|
if ( nCofsBest2 > 2 )
|
||||||
continue;
|
continue;
|
||||||
nCofsBest2 = If_CluCountCofs( pCof1, nVars, nBSsize, 0 );
|
nCofsBest2 = If_CluCountCofs( pCof1, nVars, g->nVars, 0, NULL );
|
||||||
if ( nCofsBest2 > 2 )
|
if ( nCofsBest2 > 2 )
|
||||||
continue;
|
continue;
|
||||||
// find a good variable - move to the end
|
// found good shared variable - move to the end
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, pGroup[v], nVars-1 );
|
If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[v], nVars-1 );
|
||||||
for ( i = 0; i < nBSsize; i++ )
|
for ( i = 0; i < g->nVars; i++ )
|
||||||
pGroup[i] = P2V[nVars-nBSsize+i];
|
g->pVars[i] = P2V[nVars-g->nVars+i];
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
void If_CluPrintGroup( word Group )
|
void If_CluPrintGroup( If_Grp_t * g )
|
||||||
{
|
{
|
||||||
char * pGroup = (char *)&Group;
|
|
||||||
int i;
|
int i;
|
||||||
for ( i = 0; i < pGroup[7]; i++ )
|
for ( i = 0; i < g->nVars; i++ )
|
||||||
printf( "%d ", pGroup[i] );
|
printf( "%d ", g->pVars[i] );
|
||||||
printf( "\n" );
|
printf( "\n" );
|
||||||
printf( "Cofs = %d", pGroup[6] );
|
printf( "Cofs = %d", g->nMyu );
|
||||||
printf( "\n" );
|
printf( "\n" );
|
||||||
printf( "Vars = %d", pGroup[7] );
|
printf( "Vars = %d", g->nVars );
|
||||||
printf( "\n" );
|
printf( "\n" );
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// finds a good var group (cof count < 6; vars are MSBs)
|
// finds a good var group (cof count < 6; vars are MSBs)
|
||||||
word If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint )
|
If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint )
|
||||||
{
|
{
|
||||||
int nRounds = 3;
|
If_Grp_t G = {0}, * g = &G;
|
||||||
word GroupBest = 0;
|
|
||||||
char * pGroupBest = (char *)&GroupBest;
|
|
||||||
int i, r, v, nCofs, VarBest, nCofsBest2;
|
int i, r, v, nCofs, VarBest, nCofsBest2;
|
||||||
assert( nVars >= nBSsize + iVarStart && nVars <= CLU_MAX );
|
assert( nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX );
|
||||||
assert( nBSsize >= 3 && nBSsize <= 6 );
|
assert( nBSsize >= 3 && nBSsize <= 6 );
|
||||||
// start with the default group
|
// start with the default group
|
||||||
pGroupBest[7] = nBSsize;
|
g->nVars = nBSsize;
|
||||||
pGroupBest[6] = If_CluCountCofs( pF, nVars, nBSsize, 0 );
|
g->nMyu = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
|
||||||
for ( i = 0; i < nBSsize; i++ )
|
for ( i = 0; i < nBSsize; i++ )
|
||||||
pGroupBest[i] = P2V[nVars-nBSsize+i];
|
g->pVars[i] = P2V[nVars-nBSsize+i];
|
||||||
// check if good enough
|
// check if good enough
|
||||||
if ( pGroupBest[6] == 2 )
|
if ( g->nMyu == 2 )
|
||||||
return GroupBest;
|
return G;
|
||||||
if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, nBSsize, pGroupBest ) )
|
if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, g ) )
|
||||||
return GroupBest;
|
return G;
|
||||||
|
|
||||||
printf( "Iter %d ", -1 );
|
printf( "Iter %d ", -1 );
|
||||||
If_CluPrintGroup( GroupBest );
|
If_CluPrintGroup( g );
|
||||||
|
|
||||||
// try to find better group
|
// try to find better group
|
||||||
for ( r = 0; r < nRounds; r++ )
|
for ( r = 0; r < nBSsize; r++ )
|
||||||
{
|
{
|
||||||
// find the best var to add
|
// find the best var to add
|
||||||
VarBest = P2V[nVars-1-nBSsize];
|
VarBest = P2V[nVars-1-nBSsize];
|
||||||
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0 );
|
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
|
||||||
for ( v = nVars-2-nBSsize; v >= iVarStart; v-- )
|
for ( v = nVars-2-nBSsize; v >= iVarStart; v-- )
|
||||||
{
|
{
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
|
If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
|
||||||
nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0 );
|
nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
|
||||||
if ( nCofsBest2 > nCofs )
|
if ( nCofsBest2 >= nCofs )
|
||||||
{
|
{
|
||||||
nCofsBest2 = nCofs;
|
nCofsBest2 = nCofs;
|
||||||
VarBest = P2V[nVars-1-nBSsize];
|
VarBest = P2V[nVars-1-nBSsize];
|
||||||
|
|
@ -335,80 +416,97 @@ word If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V,
|
||||||
}
|
}
|
||||||
// go back
|
// go back
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
|
If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
|
||||||
|
// update best bound set
|
||||||
|
nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL );
|
||||||
|
assert( nCofs == nCofsBest2 );
|
||||||
|
|
||||||
// find the best var to remove
|
// find the best var to remove
|
||||||
VarBest = P2V[nVars-1-nBSsize];
|
VarBest = P2V[nVars-1-nBSsize];
|
||||||
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0 );
|
nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
|
||||||
for ( v = nVars-nBSsize; v < nVars; v++ )
|
for ( v = nVars-nBSsize; v < nVars; v++ )
|
||||||
{
|
{
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, v, nVars-1-nBSsize );
|
If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize );
|
||||||
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0 );
|
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
|
||||||
if ( nCofsBest2 > nCofs )
|
if ( nCofsBest2 >= nCofs )
|
||||||
{
|
{
|
||||||
nCofsBest2 = nCofs;
|
nCofsBest2 = nCofs;
|
||||||
VarBest = P2V[nVars-1-nBSsize];
|
VarBest = P2V[nVars-1-nBSsize];
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// go back
|
// go back
|
||||||
If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
|
If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize );
|
||||||
|
|
||||||
// update best bound set
|
// update best bound set
|
||||||
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0 );
|
nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL );
|
||||||
assert( nCofs == nCofsBest2 );
|
assert( nCofs == nCofsBest2 );
|
||||||
if ( pGroupBest[6] > nCofs )
|
if ( g->nMyu >= nCofs )
|
||||||
{
|
{
|
||||||
pGroupBest[7] = nBSsize;
|
g->nVars = nBSsize;
|
||||||
pGroupBest[6] = nCofs;
|
g->nMyu = nCofs;
|
||||||
for ( i = 0; i < nBSsize; i++ )
|
for ( i = 0; i < nBSsize; i++ )
|
||||||
pGroupBest[i] = P2V[nVars-nBSsize+i];
|
g->pVars[i] = P2V[nVars-nBSsize+i];
|
||||||
}
|
}
|
||||||
|
|
||||||
printf( "Iter %d ", r );
|
printf( "Iter %d ", r );
|
||||||
If_CluPrintGroup( GroupBest );
|
If_CluPrintGroup( g );
|
||||||
|
|
||||||
// check if good enough
|
// check if good enough
|
||||||
if ( pGroupBest[6] == 2 )
|
if ( g->nMyu == 2 )
|
||||||
return GroupBest;
|
return G;
|
||||||
if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, nBSsize, pGroupBest ) )
|
if ( If_CluCheckNonDisjoint( pF, nVars, V2P, P2V, g ) )
|
||||||
return GroupBest;
|
return G;
|
||||||
}
|
}
|
||||||
assert( r == nRounds );
|
assert( r == nBSsize );
|
||||||
return 0;
|
g->nVars = 0;
|
||||||
|
return G;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// double check that the given group has a decomposition
|
// double check that the given group has a decomposition
|
||||||
void If_CluCheckGroup( word * pTruth, int nVars, word Group )
|
void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g )
|
||||||
{
|
{
|
||||||
word pF[1 << (CLU_MAX-6)];
|
word pF[CLU_WRD_MAX];
|
||||||
int v, nCofs, V2P[CLU_MAX], P2V[CLU_MAX];
|
int v, nCofs, V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX];
|
||||||
char * pVars = (char *)&Group;
|
assert( g->nVars >= 3 && g->nVars <= 6 ); // vars
|
||||||
assert( pVars[7] >= 3 && pVars[7] <= 6 ); // vars
|
assert( g->nMyu >= 2 && g->nMyu <= 4 ); // cofs
|
||||||
assert( pVars[6] >= 2 && pVars[6] <= 4 ); // cofs
|
|
||||||
// create permutation
|
// create permutation
|
||||||
for ( v = 0; v < nVars; v++ )
|
for ( v = 0; v < nVars; v++ )
|
||||||
V2P[v] = P2V[v] = v;
|
V2P[v] = P2V[v] = v;
|
||||||
// create truth table
|
// create truth table
|
||||||
If_CluCopy( pF, pTruth, nVars );
|
If_CluCopy( pF, pTruth, nVars );
|
||||||
// move group up
|
// move group up
|
||||||
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, Group );
|
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, g );
|
||||||
// check the number of cofactors
|
// check the number of cofactors
|
||||||
nCofs = If_CluCountCofs( pF, nVars, pVars[7], 0 );
|
nCofs = If_CluCountCofs( pF, nVars, g->nVars, 0, NULL );
|
||||||
if ( nCofs != pVars[6] )
|
if ( nCofs != g->nMyu )
|
||||||
printf( "Group check 0 has failed.\n" );
|
printf( "Group check 0 has failed.\n" );
|
||||||
// check compatible
|
// check compatible
|
||||||
if ( nCofs > 2 )
|
if ( nCofs > 2 )
|
||||||
{
|
{
|
||||||
nCofs = If_CluCountCofs( pF, nVars-1, pVars[7]-1, 0 );
|
nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, 0, NULL );
|
||||||
if ( nCofs > 2 )
|
if ( nCofs > 2 )
|
||||||
printf( "Group check 1 has failed.\n" );
|
printf( "Group check 1 has failed.\n" );
|
||||||
nCofs = If_CluCountCofs( pF, nVars-1, pVars[7]-1, (1 << (nVars-1)) );
|
nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, (1 << (nVars-1)), NULL );
|
||||||
if ( nCofs > 2 )
|
if ( nCofs > 2 )
|
||||||
printf( "Group check 2 has failed.\n" );
|
printf( "Group check 2 has failed.\n" );
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// double check that the permutation derived is correct
|
||||||
|
void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V )
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
for ( i = 0; i < nVars; i++ )
|
||||||
|
If_CluMoveVar( pF, nVars, V2P, P2V, i, i );
|
||||||
|
|
||||||
|
if ( If_CluEqual( pTruth, pF, nVars ) )
|
||||||
|
printf( "Permutation successful\n" );
|
||||||
|
else
|
||||||
|
printf( "Permutation FAILED.\n" );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
static inline int If_CluSuppIsMinBase( int Supp )
|
static inline int If_CluSuppIsMinBase( int Supp )
|
||||||
|
|
@ -449,57 +547,56 @@ static inline int If_CluSupport( word * t, int nVars )
|
||||||
return Supp;
|
return Supp;
|
||||||
}
|
}
|
||||||
|
|
||||||
// returns the number of nodes and conf bits in vConf
|
// returns the best group found
|
||||||
word If_CluCheck( word * pTruth, int nVars, int nLutLeaf, int nLutRoot )
|
If_Grp_t If_CluCheck( word * pTruth, int nVars, int nLutLeaf, int nLutRoot )
|
||||||
{
|
{
|
||||||
int V2P[CLU_MAX], P2V[CLU_MAX];
|
int V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX];
|
||||||
word Group1, pF[1 << (CLU_MAX-6)];
|
word pF[CLU_WRD_MAX];
|
||||||
|
If_Grp_t G1 = {0};
|
||||||
int i, nSupp;
|
int i, nSupp;
|
||||||
assert( nVars <= CLU_MAX );
|
assert( nVars <= CLU_VAR_MAX );
|
||||||
assert( nVars <= nLutLeaf + nLutRoot - 1 );
|
assert( nVars <= nLutLeaf + nLutRoot - 1 );
|
||||||
|
|
||||||
// check minnimum base
|
// check minnimum base
|
||||||
If_CluCopy( pF, pTruth, nVars );
|
If_CluCopy( pF, pTruth, nVars );
|
||||||
nSupp = If_CluSupport( pF, nVars );
|
nSupp = If_CluSupport( pF, nVars );
|
||||||
if ( !nSupp || !If_CluSuppIsMinBase(nSupp) )
|
if ( !nSupp || !If_CluSuppIsMinBase(nSupp) )
|
||||||
return 0;
|
return G1;
|
||||||
|
|
||||||
// perform testing
|
// perform testing
|
||||||
for ( i = 0; i < nVars; i++ )
|
for ( i = 0; i < nVars; i++ )
|
||||||
V2P[i] = P2V[i] = i;
|
V2P[i] = P2V[i] = i;
|
||||||
Group1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
|
G1 = If_CluFindGroup( pF, nVars, 0, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 );
|
||||||
if ( Group1 == 0 )
|
|
||||||
return 0;
|
// check permutation
|
||||||
|
If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
|
||||||
|
|
||||||
|
if ( G1.nVars == 0 )
|
||||||
|
return G1;
|
||||||
|
|
||||||
// perform checking
|
// perform checking
|
||||||
If_CluCheckGroup( pTruth, nVars, Group1 );
|
If_CluCheckGroup( pTruth, nVars, &G1 );
|
||||||
|
return G1;
|
||||||
// compute conf bits
|
|
||||||
return Group1;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// computes delay of the decomposition
|
// computes delay of the decomposition
|
||||||
float If_CluDelayMax( word Group, float * pDelays )
|
float If_CluDelayMax( If_Grp_t * g, float * pDelays )
|
||||||
{
|
{
|
||||||
char * pVars = (char *)&Group;
|
|
||||||
float Delay = 0.0;
|
float Delay = 0.0;
|
||||||
int i;
|
int i;
|
||||||
for ( i = 0; i < pVars[7]; i++ )
|
for ( i = 0; i < g->nVars; i++ )
|
||||||
Delay = Abc_MaxFloat( Delay, pDelays[pVars[i]] );
|
Delay = Abc_MaxFloat( Delay, pDelays[g->pVars[i]] );
|
||||||
return Delay;
|
return Delay;
|
||||||
}
|
}
|
||||||
|
|
||||||
// returns delay of the decomposition; sets area of the cut as its cost
|
// returns delay of the decomposition; sets area of the cut as its cost
|
||||||
float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay )
|
float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay )
|
||||||
{
|
{
|
||||||
float Delays[CLU_MAX+2];
|
float Delays[CLU_VAR_MAX+2];
|
||||||
int fUsed[CLU_MAX+2] = {0};
|
int fUsed[CLU_VAR_MAX+2] = {0};
|
||||||
If_Obj_t * pLeaf;
|
If_Obj_t * pLeaf;
|
||||||
word Group1 = 0, Group2 = 0, Group3 = 0;
|
If_Grp_t G1 = {0}, G2 = {0}, G3 = {0};
|
||||||
char * pGroup1 = (char *)&Group1;
|
|
||||||
char * pGroup2 = (char *)&Group2;
|
|
||||||
char * pGroup3 = (char *)&Group3;
|
|
||||||
int nLeaves = If_CutLeaveNum(pCut);
|
int nLeaves = If_CutLeaveNum(pCut);
|
||||||
int i, nLutLeaf, nLutRoot;
|
int i, nLutLeaf, nLutRoot;
|
||||||
// mark the cut as user cut
|
// mark the cut as user cut
|
||||||
|
|
@ -539,48 +636,49 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
|
||||||
for ( i = 0; i < nLeaves; i++ )
|
for ( i = 0; i < nLeaves; i++ )
|
||||||
{
|
{
|
||||||
pCut->pPerm[i] = 1;
|
pCut->pPerm[i] = 1;
|
||||||
pGroup1[i] = i;
|
G1.pVars[i] = i;
|
||||||
}
|
}
|
||||||
pGroup1[7] = nLeaves;
|
G1.nVars = nLeaves;
|
||||||
pCut->Cost = 1;
|
pCut->Cost = 1;
|
||||||
return 1.0 + If_CluDelayMax( Group1, Delays );
|
return 1.0 + If_CluDelayMax( &G1, Delays );
|
||||||
}
|
}
|
||||||
|
|
||||||
// derive the first group
|
// derive the first group
|
||||||
Group1 = If_CluCheck( (word *)If_CutTruth(pCut), nLeaves, nLutLeaf, nLutRoot );
|
G1 = If_CluCheck( (word *)If_CutTruth(pCut), nLeaves, nLutLeaf, nLutRoot );
|
||||||
if ( Group1 == 0 )
|
if ( G1.nVars == 0 )
|
||||||
return ABC_INFINITY;
|
return ABC_INFINITY;
|
||||||
// compute the delay
|
// compute the delay
|
||||||
Delays[nLeaves] = If_CluDelayMax( Group1, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
|
Delays[nLeaves] = If_CluDelayMax( &G1, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
|
||||||
if ( Group2 )
|
if ( G2.nVars )
|
||||||
Delays[nLeaves+1] = If_CluDelayMax( Group2, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
|
Delays[nLeaves+1] = If_CluDelayMax( &G2, Delays ) + (WireDelay == 0.0)?1.0:WireDelay;
|
||||||
|
|
||||||
// mark used groups
|
// mark used groups
|
||||||
for ( i = 0; i < pGroup1[7]; i++ )
|
for ( i = 0; i < G1.nVars; i++ )
|
||||||
fUsed[pGroup1[i]] = 1;
|
fUsed[G1.pVars[i]] = 1;
|
||||||
for ( i = 0; i < pGroup2[7]; i++ )
|
for ( i = 0; i < G2.nVars; i++ )
|
||||||
fUsed[pGroup2[i]] = 1;
|
fUsed[G2.pVars[i]] = 1;
|
||||||
// mark unused groups
|
// mark unused groups
|
||||||
assert( pGroup1[6] >= 2 && pGroup1[6] <= 4 );
|
assert( G1.nMyu >= 2 && G1.nMyu <= 4 );
|
||||||
if ( pGroup1[6] > 2 )
|
if ( G1.nMyu > 2 )
|
||||||
fUsed[pGroup1[0]] = 0;
|
fUsed[G1.pVars[G1.nVars-1]] = 0;
|
||||||
assert( pGroup2[6] >= 2 && pGroup2[6] <= 4 );
|
assert( G2.nMyu >= 2 && G2.nMyu <= 4 );
|
||||||
if ( pGroup2[6] > 2 )
|
if ( G2.nMyu > 2 )
|
||||||
fUsed[pGroup2[0]] = 0;
|
fUsed[G2.pVars[G2.nVars-1]] = 0;
|
||||||
|
|
||||||
// create remaining group
|
// create remaining group
|
||||||
assert( pGroup3[7] == 0 );
|
assert( G3.nVars == 0 );
|
||||||
for ( i = 0; i < nLeaves; i++ )
|
for ( i = 0; i < nLeaves; i++ )
|
||||||
if ( !fUsed[i] )
|
if ( !fUsed[i] )
|
||||||
pGroup3[pGroup3[7]++] = i;
|
G3.pVars[G3.nVars++] = i;
|
||||||
pGroup3[pGroup3[7]++] = nLeaves;
|
G3.pVars[G3.nVars++] = nLeaves;
|
||||||
if ( Group2 )
|
if ( G2.nVars )
|
||||||
pGroup3[pGroup3[7]++] = nLeaves+1;
|
G3.pVars[G3.nVars++] = nLeaves+1;
|
||||||
assert( pGroup1[7] + pGroup2[7] + pGroup3[7] == nLeaves + (pGroup1[7] > 0) + (pGroup2[7] > 0) + (pGroup1[6] > 2) + (pGroup2[6] > 2) );
|
assert( G1.nVars + G2.nVars + G3.nVars == nLeaves +
|
||||||
|
(G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) );
|
||||||
// what if both non-disjoint vars are the same???
|
// what if both non-disjoint vars are the same???
|
||||||
|
|
||||||
pCut->Cost = 2 + (pGroup2[7] > 0);
|
pCut->Cost = 2 + (G2.nVars > 0);
|
||||||
return 1.0 + If_CluDelayMax( Group3, Delays );
|
return 1.0 + If_CluDelayMax( &G3, Delays );
|
||||||
}
|
}
|
||||||
|
|
||||||
// testing procedure
|
// testing procedure
|
||||||
|
|
@ -591,13 +689,11 @@ void If_CluTest()
|
||||||
int nLeaves = 6;
|
int nLeaves = 6;
|
||||||
int nLutLeaf = 4;
|
int nLutLeaf = 4;
|
||||||
int nLutRoot = 4;
|
int nLutRoot = 4;
|
||||||
word Group1;
|
If_Grp_t G;
|
||||||
char * pVars = (char *)&Group1;
|
|
||||||
// return;
|
|
||||||
|
|
||||||
Group1 = If_CluCheck( &t, nLeaves, nLutLeaf, nLutRoot );
|
G = If_CluCheck( &t, nLeaves, nLutLeaf, nLutRoot );
|
||||||
|
|
||||||
If_CluPrintGroup( Group1 );
|
If_CluPrintGroup( &G );
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -3,6 +3,7 @@ SRC += src/map/if/ifCore.c \
|
||||||
src/map/if/ifDec07.c \
|
src/map/if/ifDec07.c \
|
||||||
src/map/if/ifDec08.c \
|
src/map/if/ifDec08.c \
|
||||||
src/map/if/ifDec10.c \
|
src/map/if/ifDec10.c \
|
||||||
|
src/map/if/ifDec16.c \
|
||||||
src/map/if/ifLib.c \
|
src/map/if/ifLib.c \
|
||||||
src/map/if/ifMan.c \
|
src/map/if/ifMan.c \
|
||||||
src/map/if/ifMap.c \
|
src/map/if/ifMap.c \
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue