Skip to content

A
abc
Commit 4cf99cae by Alan Mishchenko
Options

Version abc61206

parent 38254947
Showing with 3309 additions and 1324 deletions
abc.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
......@@ -630,10 +630,6 @@ SOURCE=.\src\aig\ivy\ivyFastMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ivy\ivyFpga.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ivy\ivyFraig.c
# End Source File
# Begin Source File
......@@ -642,10 +638,6 @@ SOURCE=.\src\aig\ivy\ivyHaig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ivy\ivyIsop.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ivy\ivyMan.c
# End Source File
# Begin Source File
......@@ -1597,6 +1589,42 @@ SOURCE=.\src\opt\ret\retInt.h
SOURCE=.\src\opt\ret\retLvalue.c
# End Source File
# End Group
# Begin Group "kit"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\kit\kit.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitBdd.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitFactor.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitGraph.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitHop.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitIsop.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitSop.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\kit\kitTruth.c
# End Source File
# End Group
# End Group
# Begin Group "map"
......
src/aig/ivy/ivy.h
......@@ -466,8 +466,6 @@ extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
extern void Ivy_ManHaigSimulate( Ivy_Man_t * p );
/*=== ivyIsop.c ==========================================================*/
extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
/*=== ivyMan.c ==========================================================*/
extern Ivy_Man_t * Ivy_ManStart();
extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p );
......
src/aig/ivy/ivyFactor.c deleted 100644 → 0
/**CFile****************************************************************
FileName [ivyFactor.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Factoring the cover up to 16 inputs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivyFactor.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
#include "dec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// ISOP computation fails if intermediate memory usage exceed this limit
#define IVY_FACTOR_MEM_LIMIT 16*4096
// intermediate ISOP representation
typedef struct Ivy_Sop_t_ Ivy_Sop_t;
struct Ivy_Sop_t_
{
unsigned * uCubes;
int nCubes;
};
static inline int Ivy_CubeHasLit( unsigned uCube, int i ) { return (uCube & (unsigned)(1<<i)) > 0;}
static inline unsigned Ivy_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1<<i); }
static inline unsigned Ivy_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1<<i); }
static inline unsigned Ivy_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1<<i); }
static inline int Ivy_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall; }
static inline unsigned Ivy_CubeSharp( unsigned uCube, unsigned uPart ) { return uCube & ~uPart; }
static inline unsigned Ivy_CubeMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline int Ivy_CubeIsMarked( unsigned uCube ) { return Ivy_CubeHasLit( uCube, 31 ); }
static inline void Ivy_CubeMark( unsigned uCube ) { Ivy_CubeSetLit( uCube, 31 ); }
static inline void Ivy_CubeUnmark( unsigned uCube ) { Ivy_CubeRemLit( uCube, 31 ); }
static inline int Ivy_SopCubeNum( Ivy_Sop_t * cSop ) { return cSop->nCubes; }
static inline unsigned Ivy_SopCube( Ivy_Sop_t * cSop, int i ) { return cSop->uCubes[i]; }
static inline void Ivy_SopAddCube( Ivy_Sop_t * cSop, unsigned uCube ) { cSop->uCubes[cSop->nCubes++] = uCube; }
static inline void Ivy_SopSetCube( Ivy_Sop_t * cSop, unsigned uCube, int i ) { cSop->uCubes[i] = uCube; }
static inline void Ivy_SopShrink( Ivy_Sop_t * cSop, int nCubesNew ) { cSop->nCubes = nCubesNew; }
// iterators
#define Ivy_SopForEachCube( cSop, uCube, i ) \
for ( i = 0; (i < Ivy_SopCubeNum(cSop)) && ((uCube) = Ivy_SopCube(cSop, i)); i++ )
#define Ivy_CubeForEachLiteral( uCube, Lit, nLits, i ) \
for ( i = 0; (i < (nLits)) && ((Lit) = Ivy_CubeHasLit(uCube, i)); i++ )
/**Function*************************************************************
Synopsis [Divides cover by one cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopDivideByCube( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem )
{
unsigned uCube, uDiv;
int i;
// get the only cube
assert( Ivy_SopCubeNum(cDiv) == 1 );
uDiv = Ivy_SopCube(cDiv, 0);
// allocate covers
vQuo->nCubes = 0;
vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) );
vRem->nCubes = 0;
vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) );
// sort the cubes
Ivy_SopForEachCube( cSop, uCube, i )
{
if ( Ivy_CubeContains( uCube, uDiv ) )
Ivy_SopAddCube( vQuo, Ivy_CubeSharp(uCube, uDiv) );
else
Ivy_SopAddCube( vRem, uCube );
}
}
/**Function*************************************************************
Synopsis [Divides cover by one cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopDivideInternal( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem )
{
unsigned uCube, uCube2, uDiv, uDiv2, uQuo;
int i, i2, k, k2;
assert( Ivy_SopCubeNum(cSop) >= Ivy_SopCubeNum(cDiv) );
if ( Ivy_SopCubeNum(cDiv) == 1 )
{
Ivy_SopDivideByCube( cSop, cDiv, vQuo, vRem );
return;
}
// allocate quotient
vQuo->nCubes = 0;
vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) / Ivy_SopCubeNum(cDiv) );
// for each cube of the cover
// it either belongs to the quotient or to the remainder
Ivy_SopForEachCube( cSop, uCube, i )
{
// skip taken cubes
if ( Ivy_CubeIsMarked(uCube) )
continue;
// mark the cube
Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube), i );
// find a matching cube in the divisor
Ivy_SopForEachCube( cDiv, uDiv, k )
if ( Ivy_CubeContains( uCube, uDiv ) )
break;
// the case when the cube is not found
// (later we will add marked cubes to the remainder)
if ( k == Ivy_SopCubeNum(cDiv) )
continue;
// if the quotient cube exist, it will be
uQuo = Ivy_CubeSharp( uCube, uDiv );
// try to find other cubes of the divisor
Ivy_SopForEachCube( cDiv, uDiv2, k2 )
{
if ( k2 == k )
continue;
// find a matching cube
Ivy_SopForEachCube( cSop, uCube2, i2 )
{
// skip taken cubes
if ( Ivy_CubeIsMarked(uCube2) )
continue;
// check if the cube can be used
if ( Ivy_CubeContains( uCube2, uDiv2 ) && uQuo == Ivy_CubeSharp( uCube2, uDiv2 ) )
break;
}
// the case when the cube is not found
if ( i2 == Ivy_SopCubeNum(cSop) )
break;
// the case when the cube is found - mark it and keep going
Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube2), i2 );
}
// if we did not find some cube, continue
// (later we will add marked cubes to the remainder)
if ( k2 != Ivy_SopCubeNum(cDiv) )
continue;
// we found all cubes - add the quotient cube
Ivy_SopAddCube( vQuo, uQuo );
}
// allocate remainder
vRem->nCubes = 0;
vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) - Ivy_SopCubeNum(vQuo) * Ivy_SopCubeNum(cDiv) );
// finally add the remaining cubes to the remainder
// and clean the marked cubes in the cover
Ivy_SopForEachCube( cSop, uCube, i )
{
if ( !Ivy_CubeIsMarked(uCube) )
continue;
Ivy_SopSetCube( cSop, Ivy_CubeUnmark(uCube), i );
Ivy_SopAddCube( vRem, Ivy_CubeUnmark(uCube) );
}
}
/**Function*************************************************************
Synopsis [Derives the quotient of division by literal.]
Description [Reduces the cover to be the equal to the result of
division of the given cover by the literal.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopDivideByLiteralQuo( Ivy_Sop_t * cSop, int iLit )
{
unsigned uCube;
int i, k = 0;
Ivy_SopForEachCube( cSop, uCube, i )
{
if ( Ivy_CubeHasLit(uCube, iLit) )
Ivy_SopSetCube( cSop, Ivy_CubeRemLit(uCube, iLit), k++ );
}
Ivy_SopShrink( cSop, k );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopCommonCubeCover( Ivy_Sop_t * cSop, Ivy_Sop_t * vCommon, Vec_Int_t * vStore )
{
unsigned uTemp, uCube;
int i;
uCube = ~(unsigned)0;
Ivy_SopForEachCube( cSop, uTemp, i )
uCube &= uTemp;
vCommon->nCubes = 0;
vCommon->uCubes = Vec_IntFetch( vStore, 1 );
Ivy_SopPush( vCommon, uCube );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopCreateInverse( Ivy_Sop_t * cSop, Vec_Int_t * vInput, int nVars, Vec_Int_t * vStore )
{
unsigned uCube, uMask;
int i;
// start the cover
cSop->nCubes = 0;
cSop->uCubes = Vec_IntFetch( vStore, Vec_IntSize(vInput) );
// add the cubes
uMask = Ivy_CubeMask( nVars );
Vec_IntForEachEntry( vInput, uCube, i )
Vec_IntPush( cSop, Ivy_CubeSharp(uMask, uCube) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopDup( Ivy_Sop_t * cSop, Ivy_Sop_t * vCopy, Vec_Int_t * vStore )
{
unsigned uCube;
int i;
// start the cover
vCopy->nCubes = 0;
vCopy->uCubes = Vec_IntFetch( vStore, Vec_IntSize(cSop) );
// add the cubes
Ivy_SopForEachCube( cSop, uTemp, i )
Ivy_SopPush( vCopy, uTemp );
}
/**Function*************************************************************
Synopsis [Find the least often occurring literal.]
Description [Find the least often occurring literal among those
that occur more than once.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_SopWorstLiteral( Ivy_Sop_t * cSop, int nLits )
{
unsigned uCube;
int nWord, nBit;
int i, k, iMin, nLitsMin, nLitsCur;
int fUseFirst = 1;
// go through each literal
iMin = -1;
nLitsMin = 1000000;
for ( i = 0; i < nLits; i++ )
{
// go through all the cubes
nLitsCur = 0;
Ivy_SopForEachCube( cSop, uCube, k )
if ( Ivy_CubeHasLit(uCube, i) )
nLitsCur++;
// skip the literal that does not occur or occurs once
if ( nLitsCur < 2 )
continue;
// check if this is the best literal
if ( fUseFirst )
{
if ( nLitsMin > nLitsCur )
{
nLitsMin = nLitsCur;
iMin = i;
}
}
else
{
if ( nLitsMin >= nLitsCur )
{
nLitsMin = nLitsCur;
iMin = i;
}
}
}
if ( nLitsMin < 1000000 )
return iMin;
return -1;
}
/**Function*************************************************************
Synopsis [Computes a level-zero kernel.]
Description [Modifies the cover to contain one level-zero kernel.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopMakeCubeFree( Ivy_Sop_t * cSop )
{
unsigned uMask;
int i;
assert( Ivy_SopCubeNum(cSop) > 0 );
// find the common cube
uMask = ~(unsigned)0;
Ivy_SopForEachCube( cSop, uCube, i )
uMask &= uCube;
if ( uMask == 0 )
return;
// remove the common cube
Ivy_SopForEachCube( cSop, uCube, i )
Ivy_SopSetCube( cSop, Ivy_CubeSharp(uCube, uMask), i );
}
/**Function*************************************************************
Synopsis [Computes a level-zero kernel.]
Description [Modifies the cover to contain one level-zero kernel.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_SopDivisorZeroKernel_rec( Ivy_Sop_t * cSop, int nLits )
{
int iLit;
// find any literal that occurs at least two times
iLit = Ivy_SopWorstLiteral( cSop, nLits );
if ( iLit == -1 )
return;
// derive the cube-free quotient
Ivy_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
Ivy_SopMakeCubeFree( cSop ); // the same cover
// call recursively
Ivy_SopDivisorZeroKernel_rec( cSop ); // the same cover
}
/**Function*************************************************************
Synopsis [Returns the quick divisor of the cover.]
Description [Returns NULL, if there is not divisor other than
trivial.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_SopDivisor( Ivy_Sop_t * cSop, int nLits, Ivy_Sop_t * cDiv, Vec_Int_t * vStore )
{
if ( Ivy_SopCubeNum(cSop) <= 1 )
return 0;
if ( Ivy_SopWorstLiteral( cSop, nLits ) == -1 )
return 0;
// duplicate the cover
Ivy_SopDup( cSop, cDiv, vStore );
// perform the kerneling
Ivy_SopDivisorZeroKernel_rec( cDiv, int nLits );
assert( Ivy_SopCubeNum(cDiv) > 0 );
return 1;
}
extern Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars );
extern Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, Vec_Int_t * vSimple );
extern Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars );
extern Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, unsigned uCube, Vec_Int_t * vEdgeLits );
extern Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
extern int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Factors the cover.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Graph_t * Dec_Factor32( Vec_Int_t * cSop, int nVars, Vec_Int_t * vStore )
{
Ivy_Sop_t cSop, cRes;
Ivy_Sop_t * pcSop = &cSop, * pcRes = &cRes;
Dec_Graph_t * pFForm;
Dec_Edge_t eRoot;
assert( nVars < 16 );
// check for trivial functions
if ( Vec_IntSize(cSop) == 0 )
return Dec_GraphCreateConst0();
if ( Vec_IntSize(cSop) == 1 && Vec_IntEntry(cSop, 0) == Ivy_CubeMask(nVars) )
return Dec_GraphCreateConst1();
// prepare memory manager
Vec_IntClear( vStore );
Vec_IntGrow( vStore, IVY_FACTOR_MEM_LIMIT );
// perform CST
Ivy_SopCreateInverse( cSop, pcSop, nVars, vStore ); // CST
// start the factored form
pFForm = Dec_GraphCreate( nVars );
// factor the cover
eRoot = Dec_Factor32_rec( pFForm, cSop, 2 * nVars );
// finalize the factored form
Dec_GraphSetRoot( pFForm, eRoot );
// verify the factored form
if ( !Dec_Factor32Verify( pSop, pFForm, nVars ) )
printf( "Verification has failed.\n" );
return pFForm;
}
/**Function*************************************************************
Synopsis [Internal recursive factoring procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits )
{
Vec_Int_t * cDiv, * vQuo, * vRem, * vCom;
Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
Dec_Edge_t eNodeAnd, eNode;
// make sure the cover contains some cubes
assert( Vec_IntSize(cSop) );
// get the divisor
cDiv = Ivy_SopDivisor( cSop, nLits );
if ( cDiv == NULL )
return Dec_Factor32Trivial( pFForm, cSop, nLits );
// divide the cover by the divisor
Ivy_SopDivideInternal( cSop, nLits, cDiv, &vQuo, &vRem );
assert( Vec_IntSize(vQuo) );
Vec_IntFree( cDiv );
Vec_IntFree( vRem );
// check the trivial case
if ( Vec_IntSize(vQuo) == 1 )
{
eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vQuo );
Vec_IntFree( vQuo );
return eNode;
}
// make the quotient cube free
Ivy_SopMakeCubeFree( vQuo );
// divide the cover by the quotient
Ivy_SopDivideInternal( cSop, nLits, vQuo, &cDiv, &vRem );
// check the trivial case
if ( Ivy_SopIsCubeFree( cDiv ) )
{
eNodeDiv = Dec_Factor32_rec( pFForm, cDiv );
eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
Vec_IntFree( cDiv );
Vec_IntFree( vQuo );
eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
if ( Vec_IntSize(vRem) == 0 )
{
Vec_IntFree( vRem );
return eNodeAnd;
}
else
{
eNodeRem = Dec_Factor32_rec( pFForm, vRem );
Vec_IntFree( vRem );
return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
}
}
// get the common cube
vCom = Ivy_SopCommonCubeCover( cDiv );
Vec_IntFree( cDiv );
Vec_IntFree( vQuo );
Vec_IntFree( vRem );
// solve the simple problem
eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vCom );
Vec_IntFree( vCom );
return eNode;
}
/**Function*************************************************************
Synopsis [Internal recursive factoring procedure for the leaf case.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits, Vec_Int_t * vSimple )
{
Dec_Man_t * pManDec = Abc_FrameReadManDec();
Vec_Int_t * vEdgeLits = pManDec->vLits;
Vec_Int_t * cDiv, * vQuo, * vRem;
Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
Dec_Edge_t eNodeAnd;
// get the most often occurring literal
cDiv = Ivy_SopBestLiteralCover( cSop, nLits, vSimple );
// divide the cover by the literal
Ivy_SopDivideByLiteral( cSop, nLits, cDiv, &vQuo, &vRem );
// get the node pointer for the literal
eNodeDiv = Dec_Factor32TrivialCube( pFForm, cDiv, Ivy_SopReadCubeHead(cDiv), vEdgeLits );
Vec_IntFree( cDiv );
// factor the quotient and remainder
eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
Vec_IntFree( vQuo );
eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
if ( Vec_IntSize(vRem) == 0 )
{
Vec_IntFree( vRem );
return eNodeAnd;
}
else
{
eNodeRem = Dec_Factor32_rec( pFForm, vRem );
Vec_IntFree( vRem );
return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
}
}
/**Function*************************************************************
Synopsis [Factoring the cover, which has no algebraic divisors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits )
{
Dec_Man_t * pManDec = Abc_FrameReadManDec();
Vec_Int_t * vEdgeCubes = pManDec->vCubes;
Vec_Int_t * vEdgeLits = pManDec->vLits;
Mvc_Manager_t * pMem = pManDec->pMvcMem;
Dec_Edge_t eNode;
unsigned uCube;
int i;
// create the factored form for each cube
Vec_IntClear( vEdgeCubes );
Ivy_SopForEachCube( cSop, uCube )
{
eNode = Dec_Factor32TrivialCube( pFForm, cSop, nLits, uCube, vEdgeLits );
Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
}
// balance the factored forms
return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
}
/**Function*************************************************************
Synopsis [Factoring the cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vEdgeLits )
{
Dec_Edge_t eNode;
int iBit, Value;
// create the factored form for each literal
Vec_IntClear( vEdgeLits );
Mvc_CubeForEachLit( cSop, uCube, iBit, Value )
if ( Value )
{
eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
}
// balance the factored forms
return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
}
/**Function*************************************************************
Synopsis [Create the well-balanced tree of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
{
Dec_Edge_t eNode1, eNode2;
int nNodes1, nNodes2;
if ( nNodes == 1 )
return peNodes[0];
// split the nodes into two parts
nNodes1 = nNodes/2;
nNodes2 = nNodes - nNodes1;
// nNodes2 = nNodes/2;
// nNodes1 = nNodes - nNodes2;
// recursively construct the tree for the parts
eNode1 = Dec_Factor32TrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr );
eNode2 = Dec_Factor32TrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
if ( fNodeOr )
return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
else
return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
}
// verification using temporary BDD package
#include "cuddInt.h"
/**Function*************************************************************
Synopsis [Verifies that the factoring is correct.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Ivy_SopCoverToBdd( DdManager * dd, Vec_Int_t * cSop, int nVars )
{
DdNode * bSum, * bCube, * bTemp, * bVar;
unsigned uCube;
int Value, v;
assert( nVars < 16 );
// start the cover
bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum );
// check the logic function of the node
Vec_IntForEachEntry( cSop, uCube, i )
{
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
for ( v = 0; v < nVars; v++ )
{
Value = ((uCube >> 2*v) & 3);
if ( Value == 1 )
bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
else if ( Value == 2 )
bVar = Cudd_bddIthVar( dd, v );
else
continue;
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );
Cudd_Ref( bSum );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
// complement the result if necessary
Cudd_Deref( bSum );
return bSum;
}
/**Function*************************************************************
Synopsis [Verifies that the factoring is correct.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm, int nVars )
{
static DdManager * dd = NULL;
DdNode * bFunc1, * bFunc2;
int RetValue;
// get the manager
if ( dd == NULL )
dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// get the functions
bFunc1 = Ivy_SopCoverToBdd( dd, cSop, nVars ); Cudd_Ref( bFunc1 );
bFunc2 = Dec_GraphDeriveBdd( dd, pFForm ); Cudd_Ref( bFunc2 );
//Extra_bddPrint( dd, bFunc1 ); printf("\n");
//Extra_bddPrint( dd, bFunc2 ); printf("\n");
RetValue = (bFunc1 == bFunc2);
if ( bFunc1 != bFunc2 )
{
int s;
Extra_bddPrint( dd, bFunc1 ); printf("\n");
Extra_bddPrint( dd, bFunc2 ); printf("\n");
s = 0;
}
Cudd_RecursiveDeref( dd, bFunc1 );
Cudd_RecursiveDeref( dd, bFunc2 );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ivy/ivyFpga.c deleted 100644 → 0
/**CFile****************************************************************
FileName [ivyFpga.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Prepares the AIG package to work as an FPGA mapper.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivyFpga.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
#include "attr.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Ivy_FpgaMan_t_ Ivy_FpgaMan_t;
typedef struct Ivy_FpgaObj_t_ Ivy_FpgaObj_t;
typedef struct Ivy_FpgaCut_t_ Ivy_FpgaCut_t;
// manager
struct Ivy_FpgaMan_t_
{
Ivy_Man_t * pManIvy; // the AIG manager
Attr_Man_t * pManAttr; // the attribute manager
int nLutSize; // the LUT size
int nCutsMax; // the max number of cuts
int nEntrySize; // the size of the entry
int nEntryBase; // the size of the entry minus cut leaf arrays
int fVerbose; // the verbosity flag
// temporary cut storage
Ivy_FpgaCut_t * pCutStore; // the temporary cuts
};
// priority cut
struct Ivy_FpgaCut_t_
{
float Delay; // the delay of the cut
float AreaFlow; // the area flow of the cut
float Area; // the area of the cut
int nLeaves; // the number of leaves
int * pLeaves; // the array of fanins
};
// node extension
struct Ivy_FpgaObj_t_
{
unsigned Type : 4; // type
unsigned nCuts : 28; // the number of cuts
int Id; // integer ID
int nRefs; // the number of references
Ivy_FpgaObj_t * pFanin0; // the first fanin
Ivy_FpgaObj_t * pFanin1; // the second fanin
float Required; // required time of the onde
Ivy_FpgaCut_t * pCut; // the best cut
Ivy_FpgaCut_t Cuts[0]; // the cuts of the node
};
static Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose );
static void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga );
static void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId );
static void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManFpga( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose )
{
Ivy_FpgaMan_t * pFpga;
pFpga = Ivy_ManFpgaPrepare( p, nLutSize, nCutsMax, fVerbose );
Ivy_ManFpgaDelay( pFpga );
Ivy_ManFpgaUndo( pFpga );
}
/**Function*************************************************************
Synopsis [Prepares manager for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose )
{
Ivy_FpgaMan_t * pFpga;
Ivy_Obj_t * pObj;
int i;
pFpga = ALLOC( Ivy_FpgaMan_t, 1 );
memset( pFpga, 0, sizeof(Ivy_FpgaMan_t) );
// compute the size of the node
pFpga->pManIvy = p;
pFpga->nLutSize = nLutSize;
pFpga->nCutsMax = nCutsMax;
pFpga->fVerbose = fVerbose;
pFpga->nEntrySize = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t) + sizeof(int) * nLutSize);
pFpga->nEntryBase = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t));
pFpga->pManAttr = Attr_ManStartPtrMem( Ivy_ManObjIdMax(p) + 1, pFpga->nEntrySize );
if ( fVerbose )
printf( "Entry size = %d. Total memory = %5.2f Mb.\n", pFpga->nEntrySize,
1.0 * pFpga->nEntrySize * (Ivy_ManObjIdMax(p) + 1) / (1<<20) );
// connect memory for cuts
Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjFpgaCreate( pFpga, pObj->Id );
// create temporary cuts
pFpga->pCutStore = (Ivy_FpgaCut_t *)ALLOC( char, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) );
memset( pFpga->pCutStore, 0, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) );
{
int i, * pArrays;
pArrays = (int *)((char *)pFpga->pCutStore + sizeof(Ivy_FpgaCut_t) * (nCutsMax + 1) * (nCutsMax + 1));
for ( i = 0; i < (nCutsMax + 1) * (nCutsMax + 1); i++ )
pFpga->pCutStore[i].pLeaves = pArrays + i * pFpga->nLutSize;
}
return pFpga;
}
/**Function*************************************************************
Synopsis [Quits the manager for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga )
{
Attr_ManStop( pFpga->pManAttr );
free( pFpga );
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId )
{
Ivy_FpgaObj_t * pObjFpga;
int i, * pArrays;
pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId );
pArrays = (int *)((char *)pObjFpga + pFpga->nEntryBase);
for ( i = 0; i <= pFpga->nCutsMax; i++ )
pObjFpga->Cuts[i].pLeaves = pArrays + i * pFpga->nLutSize;
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ObjFpgaMerge( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1, Ivy_FpgaCut_t * pC, int nLimit )
{
int i, k, c;
assert( pC0->nLeaves >= pC1->nLeaves );
// the case of the largest cut sizes
if ( pC0->nLeaves == nLimit && pC1->nLeaves == nLimit )
{
for ( i = 0; i < pC0->nLeaves; i++ )
if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
return 0;
for ( i = 0; i < pC0->nLeaves; i++ )
pC->pLeaves[i] = pC0->pLeaves[i];
pC->nLeaves = pC0->nLeaves;
pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
return 1;
}
// the case when one of the cuts is the largest
if ( pC0->nLeaves == nLimit )
{
for ( i = 0; i < pC1->nLeaves; i++ )
{
for ( k = pC0->nLeaves - 1; k >= 0; k-- )
if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
break;
if ( k == -1 ) // did not find
return 0;
}
for ( i = 0; i < pC0->nLeaves; i++ )
pC->pLeaves[i] = pC0->pLeaves[i];
pC->nLeaves = pC0->nLeaves;
pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
return 1;
}
// compare two cuts with different numbers
i = k = 0;
for ( c = 0; c < nLimit; c++ )
{
if ( k == pC1->nLeaves )
{
if ( i == pC0->nLeaves )
{
pC->nLeaves = c;
pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
return 1;
}
pC->pLeaves[c] = pC0->pLeaves[i++];
continue;
}
if ( i == pC0->nLeaves )
{
if ( k == pC1->nLeaves )
{
pC->nLeaves = c;
pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
return 1;
}
pC->pLeaves[c] = pC1->pLeaves[k++];
continue;
}
if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
{
pC->pLeaves[c] = pC0->pLeaves[i++];
continue;
}
if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
{
pC->pLeaves[c] = pC1->pLeaves[k++];
continue;
}
pC->pLeaves[c] = pC0->pLeaves[i++];
k++;
}
if ( i < pC0->nLeaves || k < pC1->nLeaves )
return 0;
pC->nLeaves = c;
pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
return 1;
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FpgaCutCompare( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1 )
{
if ( pC0->Delay < pC1->Delay )
return -1;
if ( pC0->Delay > pC1->Delay )
return 1;
if ( pC0->nLeaves < pC1->nLeaves )
return -1;
if ( pC0->nLeaves > pC1->nLeaves )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ObjFpgaDelay( Ivy_FpgaMan_t * pFpga, int ObjId, int Fan0Id, int Fan1Id )
{
Ivy_FpgaObj_t * pObjFpga, * pObjFpga0, * pObjFpga1;
int nCuts, i, k;
pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId );
pObjFpga0 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan0Id );
pObjFpga1 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan1Id );
// create cross-product of the cuts
nCuts = 0;
for ( i = 0; pObjFpga0->Cuts[i].nLeaves > 0 && i < pFpga->nCutsMax; i++ )
for ( k = 0; pObjFpga1->Cuts[k].nLeaves > 0 && k < pFpga->nCutsMax; k++ )
if ( Ivy_ObjFpgaMerge( pObjFpga0->Cuts + i, pObjFpga1->Cuts + k, pFpga->pCutStore + nCuts, pFpga->nLutSize ) )
nCuts++;
// sort the cuts
qsort( pFpga->pCutStore, nCuts, sizeof(Ivy_FpgaCut_t), (int (*)(const void *, const void *))Ivy_FpgaCutCompare );
// take the first
pObjFpga->Cuts[0].nLeaves = 1;
pObjFpga->Cuts[0].pLeaves[0] = ObjId;
pObjFpga->Cuts[0].Delay = pFpga->pCutStore[0].Delay;
pObjFpga->Cuts[1] = pFpga->pCutStore[0];
}
/**Function*************************************************************
Synopsis [Maps the nodes for delay.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga )
{
Ivy_FpgaObj_t * pObjFpga;
Ivy_Obj_t * pObj;
int i, DelayBest;
int clk = clock();
// set arrival times and trivial cuts at const 1 and PIs
pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, 0 );
pObjFpga->Cuts[0].nLeaves = 1;
Ivy_ManForEachPi( pFpga->pManIvy, pObj, i )
{
pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, pObj->Id );
pObjFpga->Cuts[0].nLeaves = 1;
pObjFpga->Cuts[0].pLeaves[0] = pObj->Id;
}
// map the internal nodes
Ivy_ManForEachNode( pFpga->pManIvy, pObj, i )
{
Ivy_ObjFpgaDelay( pFpga, pObj->Id, Ivy_ObjFaninId0(pObj), Ivy_ObjFaninId1(pObj) );
}
// get the best arrival time of the POs
DelayBest = 0;
Ivy_ManForEachPo( pFpga->pManIvy, pObj, i )
{
pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, Ivy_ObjFanin0(pObj)->Id );
if ( DelayBest < (int)pObjFpga->Cuts[1].Delay )
DelayBest = (int)pObjFpga->Cuts[1].Delay;
}
printf( "Best delay = %d. ", DelayBest );
PRT( "Time", clock() - clk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ivy/module.make
......@@ -9,7 +9,6 @@ SRC += src/aig/ivy/ivyBalance.c \
src/aig/ivy/ivyFastMap.c \
src/aig/ivy/ivyFraig.c \
src/aig/ivy/ivyHaig.c \
src/aig/ivy/ivyIsop.c \
src/aig/ivy/ivyMan.c \
src/aig/ivy/ivyMem.c \
src/aig/ivy/ivyMulti.c \
......
src/base/abc/abcSop.c
......@@ -427,9 +427,9 @@ char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCov
{
Literal = 3 & (Entry >> (k << 1));
if ( Literal == 1 )
pCube[k] = '1';
else if ( Literal == 2 )
pCube[k] = '0';
else if ( Literal == 2 )
pCube[k] = '1';
else if ( Literal != 0 )
assert( 0 );
}
......
src/base/abci/abc.c
......@@ -2034,25 +2034,28 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int nFaninMax, c;
int nFaninMax, nCubeMax, c;
int fUseBdds;
int fUseSops;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose );
extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFaninMax = 8;
nFaninMax = 5;
nCubeMax = 5;
fUseBdds = 0;
fUseSops = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fbvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCbsvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
case 'K':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
......@@ -2063,9 +2066,23 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFaninMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCubeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCubeMax < 0 )
goto usage;
break;
case 'b':
fUseBdds ^= 1;
break;
case 's':
fUseSops ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -2076,6 +2093,12 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if ( fUseBdds && fUseSops )
{
fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" );
goto usage;
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
......@@ -2088,7 +2111,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, fUseBdds, fVerbose );
pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, nCubeMax, fUseBdds, fUseSops, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Renoding has failed.\n" );
......@@ -2099,10 +2122,13 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: renode [-F num] [-bv]\n" );
fprintf( pErr, "\t transforms an AIG into a logic network by creating larger nodes\n" );
fprintf( pErr, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
fprintf( pErr, "\t-b : toggles cost function (BDD nodes or FF literals) [default = %s]\n", fUseBdds? "BDD nodes": "FF literals" );
fprintf( pErr, "usage: renode [-K num] [-C num] [-bsv]\n" );
fprintf( pErr, "\t transforms the AIG into a logic network with larger nodes\n" );
fprintf( pErr, "\t while minimizing the number of FF literals of the node SOPs\n" );
fprintf( pErr, "\t-K num : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
fprintf( pErr, "\t-C num : the maximum number of cubes used at a node [default = %d]\n", nCubeMax );
fprintf( pErr, "\t-b : toggles minimizing the number of BDD nodes [default = %s]\n", fUseBdds? "yes": "no" );
fprintf( pErr, "\t-s : toggles minimizing the number of SOP cubes [default = %s]\n", fUseSops? "yes": "no" );
fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/abcIf.c
......@@ -20,6 +20,7 @@
#include "abc.h"
#include "if.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -164,6 +165,8 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
// create the new network
if ( pIfMan->pPars->fUseBdds )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
else if ( pIfMan->pPars->fUseSops )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
else
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
// prepare the mapping manager
......@@ -223,7 +226,6 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
// derive the function of this node
if ( pIfMan->pPars->fTruth )
{
if ( pIfMan->pPars->fUseBdds )
......@@ -235,20 +237,29 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
// reorder the fanins to minimize the BDD size
Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
}
else
else if ( pIfMan->pPars->fUseSops )
{
typedef int Kit_Graph_t;
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
extern Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
// transform truth table into the decomposition tree
Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit );
Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
// transform truth table into the SOP
int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), pCutBest->nLimit, vCover, 0 );
assert( RetValue == 0 );
// derive the AIG for that tree
pNodeNew->pData = Dec_GraphToNetworkAig( pNtkNew->pManFunc, pGraph );
pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCutBest->nLimit, vCover );
Vec_IntFree( vCover );
}
else
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
Vec_Int_t * vMemory = Vec_IntAlloc( 1 << 16 );
// transform truth table into the decomposition tree
Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit, vMemory );
// derive the AIG for the decomposition tree
pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
Kit_GraphFree( pGraph );
Vec_IntFree( vMemory );
}
}
else
pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
If_ObjSetCopy( pIfObj, pNodeNew );
return pNodeNew;
......
src/base/abci/abcRenode.c
......@@ -21,6 +21,7 @@
#include "abc.h"
#include "reo.h"
#include "if.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -28,13 +29,11 @@
static int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
static int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars );
static reo_man * s_pReo = NULL;
static DdManager * s_pDd = NULL;
typedef int Kit_Graph_t;
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
static reo_man * s_pReo = NULL;
static DdManager * s_pDd = NULL;
static Vec_Int_t * s_vMemory = NULL;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -51,7 +50,7 @@ extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose )
Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose )
{
extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
If_Par_t Pars, * pPars = &Pars;
......@@ -77,7 +76,14 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
pPars->pTimesArr = NULL;
pPars->pTimesArr = NULL;
pPars->pFuncCost = fUseBdds? Abc_NtkRenodeEvalBdd : Abc_NtkRenodeEvalSop;
pPars->fUseBdds = fUseBdds;
pPars->fUseSops = fUseSops;
if ( fUseBdds )
pPars->pFuncCost = Abc_NtkRenodeEvalBdd;
else if ( fUseSops )
pPars->pFuncCost = Abc_NtkRenodeEvalSop;
else
pPars->pFuncCost = Abc_NtkRenodeEvalAig;
// start the manager
if ( fUseBdds )
......@@ -85,9 +91,13 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
assert( s_pReo == NULL );
s_pDd = Cudd_Init( nFaninMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
s_pReo = Extra_ReorderInit( nFaninMax, 100 );
pPars->fUseBdds = 1;
pPars->pReoMan = s_pReo;
}
else
{
assert( s_vMemory == NULL );
s_vMemory = Vec_IntAlloc( 1 << 16 );
}
// perform mapping/renoding
pNtkNew = Abc_NtkIf( pNtk, pPars );
......@@ -98,14 +108,20 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
Extra_StopManager( s_pDd );
Extra_ReorderQuit( s_pReo );
s_pReo = NULL;
s_pDd = NULL;
s_pDd = NULL;
}
else
{
Vec_IntFree( s_vMemory );
s_vMemory = NULL;
}
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Derives the BDD after reordering.]
Synopsis [Computes the cost based on the BDD size after reordering.]
Description []
......@@ -120,7 +136,8 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
int nNodes, nSupport;
bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars ); Cudd_Ref( bFunc );
bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL ); Cudd_Ref( bFuncNew );
nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
// nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
nSupport = 1;
nNodes = Cudd_DagSize( bFuncNew );
Cudd_RecursiveDeref( s_pDd, bFuncNew );
Cudd_RecursiveDeref( s_pDd, bFunc );
......@@ -129,7 +146,7 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
/**Function*************************************************************
Synopsis [Derives the BDD after reordering.]
Synopsis [Computes the cost based on ISOP.]
Description []
......@@ -140,11 +157,32 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
***********************************************************************/
int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
{
int nCubes, RetValue;
RetValue = Kit_TruthIsop( pTruth, nVars, s_vMemory, 0 );
assert( RetValue == 0 );
nCubes = Vec_IntSize( s_vMemory );
return (1 << 16) | nCubes;
}
/**Function*************************************************************
Synopsis [Computes the cost based on the factored form.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars )
{
Kit_Graph_t * pGraph;
int nNodes, nDepth;
pGraph = Kit_TruthToGraph( pTruth, nVars );
pGraph = Kit_TruthToGraph( pTruth, nVars, s_vMemory );
nNodes = Kit_GraphNodeNum( pGraph );
nDepth = Kit_GraphLevelNum( pGraph );
// nDepth = Kit_GraphLevelNum( pGraph );
nDepth = 1;
Kit_GraphFree( pGraph );
return (nDepth << 16) | nNodes;
}
......
src/map/if/if.h
......@@ -85,6 +85,7 @@ struct If_Par_t_
// internal parameters
int fTruth; // truth table computation enabled
int fUseBdds; // sets local BDDs at the nodes
int fUseSops; // sets local SOPs at the nodes
int nLatches; // the number of latches in seq mapping
If_Lib_t * pLutLib; // the LUT library
float * pTimesArr; // arrival times
......
src/map/if/ifMan.c
......@@ -205,7 +205,7 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
{
If_Cut_t * pCut;
If_Obj_t * pObj;
int i, * pArrays;
int i, * pArrays, nTruthWords;
// get memory for the object
pObj = (If_Obj_t *)Mem_FixedEntryFetch( p->pMem );
memset( pObj, 0, p->nEntryBase );
......@@ -230,6 +230,13 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
pObj->nCuts = 1;
// set the required times
pObj->Required = IF_FLOAT_LARGE;
// set up elementary truth table of the unit cut
if ( p->pPars->fTruth )
{
nTruthWords = Extra_TruthWordNum( pCut->nLimit );
for ( i = 0; i < nTruthWords; i++ )
If_CutTruth(pCut)[i] = 0xAAAAAAAA;
}
return pObj;
}
......
src/map/if/ifTruth.c
......@@ -69,6 +69,8 @@ static inline unsigned Cut_TruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
***********************************************************************/
void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
extern void Kit_FactorTest( unsigned * pTruth, int nVars );
// permute the first table
if ( fCompl0 )
Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
......@@ -86,6 +88,9 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
else
Extra_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
// perform
// Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit );
}
////////////////////////////////////////////////////////////////////////
......
src/misc/extra/extra.h
......@@ -511,7 +511,6 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
extern void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
extern void Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern DdNode * Extra_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
extern int Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
extern int Extra_TruthSupportSize( unsigned * pTruth, int nVars );
extern int Extra_TruthSupport( unsigned * pTruth, int nVars );
......
src/misc/extra/extraUtilTruth.c
......@@ -250,64 +250,6 @@ void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description [Note the caching makes no sense for this procedure.]
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal )
{
DdNode * bF0, * bF1, * bF;
if ( nVars == 0 )
{
if ( pTruth[iBit>>5] & (1 << iBit&31) )
return b1;
return b0;
}
if ( nVars == 5 )
{
if ( pTruth[iBit>>5] == 0xFFFFFFFF )
return b1;
if ( pTruth[iBit>>5] == 0 )
return b0;
}
// other special cases can be added
bF0 = Extra_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal ); Cudd_Ref( bF0 );
bF1 = Extra_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal ); Cudd_Ref( bF1 );
bF = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 ); Cudd_Ref( bF );
Cudd_RecursiveDeref( dd, bF0 );
Cudd_RecursiveDeref( dd, bF1 );
Cudd_Deref( bF );
return bF;
}
/**Function*************************************************************
Synopsis [Compute BDD corresponding to the truth table.]
Description [If truth table has N vars, the BDD depends on N topmost
variables of the BDD manager. The most significant variable of the table
is encoded by the topmost variable of the manager. BDD construction is
very efficient in this case because BDD is constructed one node at a time,
by simply adding BDD nodes on top of existent BDD nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars )
{
return Extra_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars );
}
/**Function*************************************************************
Synopsis [Returns 1 if TT depends on the given variable.]
Description []
......
src/misc/vec/vecInt.h
......@@ -598,6 +598,9 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
***********************************************************************/
static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
{
if ( nWords == 0 )
return NULL;
assert( nWords > 0 );
p->nSize += nWords;
if ( p->nSize > p->nCap )
{
......
src/opt/kit/kit.h 0 → 100644
/**CFile****************************************************************
FileName [kit.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kit.h,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __KIT_H__
#define __KIT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Kit_Sop_t_ Kit_Sop_t;
struct Kit_Sop_t_
{
int nCubes; // the number of cubes
unsigned * pCubes; // the storage for cubes
};
typedef struct Kit_Edge_t_ Kit_Edge_t;
struct Kit_Edge_t_
{
unsigned fCompl : 1; // the complemented bit
unsigned Node : 30; // the decomposition node pointed by the edge
};
typedef struct Kit_Node_t_ Kit_Node_t;
struct Kit_Node_t_
{
Kit_Edge_t eEdge0; // the left child of the node
Kit_Edge_t eEdge1; // the right child of the node
// other info
void * pFunc; // the function of the node (BDD or AIG)
unsigned Level : 14; // the level of this node in the global AIG
// printing info
unsigned fNodeOr : 1; // marks the original OR node
unsigned fCompl0 : 1; // marks the original complemented edge
unsigned fCompl1 : 1; // marks the original complemented edge
// latch info
unsigned nLat0 : 5; // the number of latches on the first edge
unsigned nLat1 : 5; // the number of latches on the second edge
unsigned nLat2 : 5; // the number of latches on the output edge
};
typedef struct Kit_Graph_t_ Kit_Graph_t;
struct Kit_Graph_t_
{
int fConst; // marks the constant 1 graph
int nLeaves; // the number of leaves
int nSize; // the number of nodes (including the leaves)
int nCap; // the number of allocated nodes
Kit_Node_t * pNodes; // the array of leaves and internal nodes
Kit_Edge_t eRoot; // the pointer to the topmost node
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
#ifndef REALLOC
#define REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#endif
static inline int Kit_CubeHasLit( unsigned uCube, int i ) { return(uCube & (unsigned)(1<<i)) > 0; }
static inline unsigned Kit_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1<<i); }
static inline unsigned Kit_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1<<i); }
static inline unsigned Kit_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1<<i); }
static inline int Kit_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall; }
static inline unsigned Kit_CubeSharp( unsigned uCube, unsigned uMask ) { return uCube & ~uMask; }
static inline unsigned Kit_CubeMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline int Kit_CubeIsMarked( unsigned uCube ) { return Kit_CubeHasLit( uCube, 31 ); }
static inline unsigned Kit_CubeMark( unsigned uCube ) { return Kit_CubeSetLit( uCube, 31 ); }
static inline unsigned Kit_CubeUnmark( unsigned uCube ) { return Kit_CubeRemLit( uCube, 31 ); }
static inline int Kit_SopCubeNum( Kit_Sop_t * cSop ) { return cSop->nCubes; }
static inline unsigned Kit_SopCube( Kit_Sop_t * cSop, int i ) { return cSop->pCubes[i]; }
static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew ) { cSop->nCubes = nCubesNew; }
static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; }
static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; }
static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; }
static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; }
static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); }
static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; }
static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; }
static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; }
static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; }
static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }
static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; }
static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; }
static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; }
static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; }
static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i ) { return pGraph->pNodes + i; }
static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; }
static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; }
static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); }
static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) );}
static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline void Kit_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); }
static inline void Kit_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); }
static inline int Kit_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; }
static inline int Kit_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
return (uWord & 0x0000FFFF) + (uWord>>16);
}
static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
{
int w, Counter = 0;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
Counter += Kit_WordCountOnes(pIn[w]);
return Counter;
}
static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn0[w] != pIn1[w] )
return 0;
return 1;
}
static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn[w] )
return 0;
return 1;
}
static inline int Kit_TruthIsConst1( unsigned * pIn, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn[w] != ~(unsigned)0 )
return 0;
return 1;
}
static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn1[w] & ~pIn2[w] )
return 0;
return 1;
}
static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn[w];
}
static inline void Kit_TruthClear( unsigned * pOut, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = 0;
}
static inline void Kit_TruthFill( unsigned * pOut, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(unsigned)0;
}
static inline void Kit_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~pIn[w];
}
static inline void Kit_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & pIn1[w];
}
static inline void Kit_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] | pIn1[w];
}
static inline void Kit_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & ~pIn1[w];
}
static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(pIn0[w] & pIn1[w]);
}
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
#define Kit_SopForEachCube( cSop, uCube, i ) \
for ( i = 0; (i < Kit_SopCubeNum(cSop)) && ((uCube) = Kit_SopCube(cSop, i)); i++ )
#define Kit_CubeForEachLiteral( uCube, Lit, nLits, i ) \
for ( i = 0; (i < (nLits)) && ((Lit) = Kit_CubeHasLit(uCube, i)); i++ )
#define Kit_GraphForEachLeaf( pGraph, pLeaf, i ) \
for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Kit_GraphNode(pGraph, i)), 1); i++ )
#define Kit_GraphForEachNode( pGraph, pAnd, i ) \
for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Kit_GraphNode(pGraph, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== kitBdd.c ==========================================================*/
extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
/*=== kitFactor.c ==========================================================*/
extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
/*=== kitGraph.c ==========================================================*/
extern Kit_Graph_t * Kit_GraphCreate( int nLeaves );
extern Kit_Graph_t * Kit_GraphCreateConst0();
extern Kit_Graph_t * Kit_GraphCreateConst1();
extern Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl );
extern void Kit_GraphFree( Kit_Graph_t * pGraph );
extern Kit_Node_t * Kit_GraphAppendNode( Kit_Graph_t * pGraph );
extern Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
extern Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
extern Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1, int Type );
extern Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type );
extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
/*=== kitHop.c ==========================================================*/
/*=== kitIsop.c ==========================================================*/
extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
/*=== kitSop.c ==========================================================*/
extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
extern void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
extern void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit );
extern void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
extern void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
extern void Kit_SopMakeCubeFree( Kit_Sop_t * cSop );
extern int Kit_SopIsCubeFree( Kit_Sop_t * cSop );
extern void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
extern int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits );
extern int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
extern void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory );
/*=== kitTruth.c ==========================================================*/
extern void Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
extern void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars );
extern int Kit_TruthSupport( unsigned * pTruth, int nVars );
extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kitBdd.c 0 → 100644
/**CFile****************************************************************
FileName [kitBdd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures involving BDDs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitBdd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derives the BDD for the given SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars )
{
DdNode * bSum, * bCube, * bTemp, * bVar;
unsigned uCube;
int Value, i, v;
assert( nVars < 16 );
// start the cover
bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum );
// check the logic function of the node
Kit_SopForEachCube( cSop, uCube, i )
{
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
for ( v = 0; v < nVars; v++ )
{
Value = ((uCube >> 2*v) & 3);
if ( Value == 1 )
bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
else if ( Value == 2 )
bVar = Cudd_bddIthVar( dd, v );
else
continue;
bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );
Cudd_Ref( bSum );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
}
// complement the result if necessary
Cudd_Deref( bSum );
return bSum;
}
/**Function*************************************************************
Synopsis [Converts graph to BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph )
{
DdNode * bFunc, * bFunc0, * bFunc1;
Kit_Node_t * pNode;
int i;
// sanity checks
assert( Kit_GraphLeaveNum(pGraph) >= 0 );
assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
// check for constant function
if ( Kit_GraphIsConst(pGraph) )
return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );
// assign the elementary variables
Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->pFunc = Cudd_bddIthVar( dd, i );
// compute the function for each internal node
Kit_GraphForEachNode( pGraph, pNode, i )
{
bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( pNode->pFunc );
}
// deref the intermediate results
bFunc = pNode->pFunc; Cudd_Ref( bFunc );
Kit_GraphForEachNode( pGraph, pNode, i )
Cudd_RecursiveDeref( dd, pNode->pFunc );
Cudd_Deref( bFunc );
// complement the result if necessary
return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal )
{
DdNode * bF0, * bF1, * bF;
if ( nVars == 0 )
{
if ( pTruth[iBit>>5] & (1 << iBit&31) )
return b1;
return b0;
}
if ( nVars == 5 )
{
if ( pTruth[iBit>>5] == 0xFFFFFFFF )
return b1;
if ( pTruth[iBit>>5] == 0 )
return b0;
}
// other special cases can be added
bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal ); Cudd_Ref( bF0 );
bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal ); Cudd_Ref( bF1 );
bF = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 ); Cudd_Ref( bF );
Cudd_RecursiveDeref( dd, bF0 );
Cudd_RecursiveDeref( dd, bF1 );
Cudd_Deref( bF );
return bF;
}
/**Function*************************************************************
Synopsis [Compute BDD corresponding to the truth table.]
Description [If truth table has N vars, the BDD depends on N topmost
variables of the BDD manager. The most significant variable of the table
is encoded by the topmost variable of the manager. BDD construction is
efficient in this case because BDD is constructed one node at a time,
by simply adding BDD nodes on top of existent BDD nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars )
{
return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars );
}
/**Function*************************************************************
Synopsis [Verifies that the factoring is correct.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopFactorVerify( Vec_Int_t * vCover, Kit_Graph_t * pFForm, int nVars )
{
static DdManager * dd = NULL;
Kit_Sop_t Sop, * cSop = &Sop;
DdNode * bFunc1, * bFunc2;
Vec_Int_t * vMemory;
int RetValue;
// get the manager
if ( dd == NULL )
dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// derive SOP
vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
Kit_SopCreate( cSop, vCover, nVars, vMemory );
// get the functions
bFunc1 = Kit_SopToBdd( dd, cSop, nVars ); Cudd_Ref( bFunc1 );
bFunc2 = Kit_GraphToBdd( dd, pFForm ); Cudd_Ref( bFunc2 );
//Extra_bddPrint( dd, bFunc1 ); printf("\n");
//Extra_bddPrint( dd, bFunc2 ); printf("\n");
RetValue = (bFunc1 == bFunc2);
if ( bFunc1 != bFunc2 )
{
int s;
Extra_bddPrint( dd, bFunc1 ); printf("\n");
Extra_bddPrint( dd, bFunc2 ); printf("\n");
s = 0;
}
Cudd_RecursiveDeref( dd, bFunc1 );
Cudd_RecursiveDeref( dd, bFunc2 );
Vec_IntFree( vMemory );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kitFactor.c 0 → 100644
/**CFile****************************************************************
FileName [kitFactor.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Algebraic factoring.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitFactor.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// factoring fails if intermediate memory usage exceed this limit
#define KIT_FACTOR_MEM_LIMIT (1<<16)
static Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
static Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory );
static Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits );
static Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits );
extern int Kit_SopFactorVerify( Vec_Int_t * cSop, Kit_Graph_t * pFForm, int nVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Factors the cover.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory )
{
Kit_Sop_t Sop, Res;
Kit_Sop_t * cSop = &Sop, * cRes = &Res;
Kit_Graph_t * pFForm;
Kit_Edge_t eRoot;
int nCubes = Vec_IntSize(vCover);
// works for up to 15 variables because divisin procedure
// used the last bit for marking the cubes going to the remainder
assert( nVars < 16 );
// check for trivial functions
if ( Vec_IntSize(vCover) == 0 )
return Kit_GraphCreateConst0();
if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == (int)Kit_CubeMask(nVars) )
return Kit_GraphCreateConst1();
// prepare memory manager
// Vec_IntClear( vMemory );
Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
// perform CST
Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
// start the factored form
pFForm = Kit_GraphCreate( nVars );
// factor the cover
eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
// finalize the factored form
Kit_GraphSetRoot( pFForm, eRoot );
if ( fCompl )
Kit_GraphComplement( pFForm );
// verify the factored form
// Vec_IntShrink( vCover, nCubes );
// if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
// printf( "Verification has failed.\n" );
return pFForm;
}
/**Function*************************************************************
Synopsis [Recursive factoring procedure.]
Description [For the pseudo-code, see Hachtel/Somenzi,
Logic synthesis and verification algorithms, Kluwer, 1996, p. 432.]
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
{
Kit_Sop_t Div, Quo, Rem, Com;
Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem, * cCom = &Com;
Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
// make sure the cover contains some cubes
assert( Kit_SopCubeNum(cSop) > 0 );
// get the divisor
if ( !Kit_SopDivisor(cDiv, cSop, nLits, vMemory) )
return Kit_SopFactorTrivial( pFForm, cSop, nLits );
// divide the cover by the divisor
Kit_SopDivideInternal( cSop, cDiv, cQuo, cRem, vMemory );
// check the trivial case
assert( Kit_SopCubeNum(cQuo) > 0 );
if ( Kit_SopCubeNum(cQuo) == 1 )
return Kit_SopFactorLF_rec( pFForm, cSop, cQuo, nLits, vMemory );
// make the quotient cube free
Kit_SopMakeCubeFree( cQuo );
// divide the cover by the quotient
Kit_SopDivideInternal( cSop, cQuo, cDiv, cRem, vMemory );
// check the trivial case
if ( Kit_SopIsCubeFree( cDiv ) )
{
eNodeDiv = Kit_SopFactor_rec( pFForm, cDiv, nLits, vMemory );
eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
if ( Kit_SopCubeNum(cRem) == 0 )
return eNodeAnd;
eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
}
// get the common cube
Kit_SopCommonCubeCover( cCom, cDiv, vMemory );
// solve the simple problem
return Kit_SopFactorLF_rec( pFForm, cSop, cCom, nLits, vMemory );
}
/**Function*************************************************************
Synopsis [Internal recursive factoring procedure for the leaf case.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory )
{
Kit_Sop_t Div, Quo, Rem;
Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem;
Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
assert( Kit_SopCubeNum(cSimple) == 1 );
// get the most often occurring literal
Kit_SopBestLiteralCover( cDiv, cSop, Kit_SopCube(cSimple, 0), nLits, vMemory );
// divide the cover by the literal
Kit_SopDivideByCube( cSop, cDiv, cQuo, cRem, vMemory );
// get the node pointer for the literal
eNodeDiv = Kit_SopFactorTrivialCube( pFForm, Kit_SopCube(cDiv, 0), nLits );
// factor the quotient and remainder
eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
if ( Kit_SopCubeNum(cRem) == 0 )
return eNodeAnd;
eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
}
/**Function*************************************************************
Synopsis [Factoring cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, int nStart, int nFinish )
{
Kit_Edge_t eNode1, eNode2;
int i, iLit, nLits, nLits1, nLits2;
// count the number of literals in this interval
nLits = 0;
for ( i = nStart; i < nFinish; i++ )
if ( Kit_CubeHasLit(uCube, i) )
{
iLit = i;
nLits++;
}
// quit if there is only one literal
if ( nLits == 1 )
return Kit_EdgeCreate( iLit/2, iLit%2 ); // CST
// split the literals into two parts
nLits1 = nLits/2;
nLits2 = nLits - nLits1;
// nLits2 = nLits/2;
// nLits1 = nLits - nLits2;
// find the splitting point
nLits = 0;
for ( i = nStart; i < nFinish; i++ )
if ( Kit_CubeHasLit(uCube, i) )
{
if ( nLits == nLits1 )
break;
nLits++;
}
// recursively construct the tree for the parts
eNode1 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, nStart, i );
eNode2 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, i, nFinish );
return Kit_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
}
/**Function*************************************************************
Synopsis [Factoring cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits )
{
return Kit_SopFactorTrivialCube_rec( pFForm, uCube, 0, nLits );
}
/**Function*************************************************************
Synopsis [Factoring SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactorTrivial_rec( Kit_Graph_t * pFForm, unsigned * pCubes, int nCubes, int nLits )
{
Kit_Edge_t eNode1, eNode2;
int nCubes1, nCubes2;
if ( nCubes == 1 )
return Kit_SopFactorTrivialCube_rec( pFForm, pCubes[0], 0, nLits );
// split the cubes into two parts
nCubes1 = nCubes/2;
nCubes2 = nCubes - nCubes1;
// nCubes2 = nCubes/2;
// nCubes1 = nCubes - nCubes2;
// recursively construct the tree for the parts
eNode1 = Kit_SopFactorTrivial_rec( pFForm, pCubes, nCubes1, nLits );
eNode2 = Kit_SopFactorTrivial_rec( pFForm, pCubes + nCubes1, nCubes2, nLits );
return Kit_GraphAddNodeOr( pFForm, eNode1, eNode2 );
}
/**Function*************************************************************
Synopsis [Factoring the cover, which has no algebraic divisors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits )
{
return Kit_SopFactorTrivial_rec( pFForm, cSop->pCubes, cSop->nCubes, nLits );
}
/**Function*************************************************************
Synopsis [Testing procedure for the factoring code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_FactorTest( unsigned * pTruth, int nVars )
{
Vec_Int_t * vCover, * vMemory;
Kit_Graph_t * pGraph;
// unsigned uTruthRes;
int RetValue;
// derive SOP
vCover = Vec_IntAlloc( 0 );
RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 );
assert( RetValue == 0 );
// derive factored form
vMemory = Vec_IntAlloc( 0 );
pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
/*
// derive truth table
assert( nVars <= 5 );
uTruthRes = Kit_GraphToTruth( pGraph );
if ( uTruthRes != pTruth[0] )
printf( "Verification failed!" );
*/
printf( "Vars = %2d. Cubes = %3d. FFNodes = %3d. FF_memory = %3d.\n",
nVars, Vec_IntSize(vCover), Kit_GraphNodeNum(pGraph), Vec_IntSize(vMemory) );
Vec_IntFree( vMemory );
Vec_IntFree( vCover );
Kit_GraphFree( pGraph );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kitGraph.c 0 → 100644
/**CFile****************************************************************
FileName [kitGraph.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Decomposition graph representation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitGraph.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_GraphCreate( int nLeaves )
{
Kit_Graph_t * pGraph;
pGraph = ALLOC( Kit_Graph_t, 1 );
memset( pGraph, 0, sizeof(Kit_Graph_t) );
pGraph->nLeaves = nLeaves;
pGraph->nSize = nLeaves;
pGraph->nCap = 2 * nLeaves + 50;
pGraph->pNodes = ALLOC( Kit_Node_t, pGraph->nCap );
memset( pGraph->pNodes, 0, sizeof(Kit_Node_t) * pGraph->nSize );
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 0 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_GraphCreateConst0()
{
Kit_Graph_t * pGraph;
pGraph = ALLOC( Kit_Graph_t, 1 );
memset( pGraph, 0, sizeof(Kit_Graph_t) );
pGraph->fConst = 1;
pGraph->eRoot.fCompl = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 1 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_GraphCreateConst1()
{
Kit_Graph_t * pGraph;
pGraph = ALLOC( Kit_Graph_t, 1 );
memset( pGraph, 0, sizeof(Kit_Graph_t) );
pGraph->fConst = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates the literal graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )
{
Kit_Graph_t * pGraph;
assert( 0 <= iLeaf && iLeaf < nLeaves );
pGraph = Kit_GraphCreate( nLeaves );
pGraph->eRoot.Node = iLeaf;
pGraph->eRoot.fCompl = fCompl;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_GraphFree( Kit_Graph_t * pGraph )
{
FREE( pGraph->pNodes );
free( pGraph );
}
/**Function*************************************************************
Synopsis [Appends a new node to the graph.]
Description [This procedure is meant for internal use.]
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Node_t * Kit_GraphAppendNode( Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
if ( pGraph->nSize == pGraph->nCap )
{
pGraph->pNodes = REALLOC( Kit_Node_t, pGraph->pNodes, 2 * pGraph->nCap );
pGraph->nCap = 2 * pGraph->nCap;
}
pNode = pGraph->pNodes + pGraph->nSize++;
memset( pNode, 0, sizeof(Kit_Node_t) );
return pNode;
}
/**Function*************************************************************
Synopsis [Creates an AND node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 )
{
Kit_Node_t * pNode;
// get the new node
pNode = Kit_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
}
/**Function*************************************************************
Synopsis [Creates an OR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 )
{
Kit_Node_t * pNode;
// get the new node
pNode = Kit_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
// make adjustments for the OR gate
pNode->fNodeOr = 1;
pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1, int Type )
{
Kit_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eEdge0.fCompl ^= 1;
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
eEdge0.fCompl ^= 1;
// derive the second AND
eEdge1.fCompl ^= 1;
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// derive the first AND
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the second AND
eEdge0.fCompl ^= 1;
eEdge1.fCompl ^= 1;
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type )
{
Kit_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// complement the arguments
eEdgeT.fCompl ^= 1;
eEdgeE.fCompl ^= 1;
// derive the first AND
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
/**Function*************************************************************
Synopsis [Derives the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph )
{
unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned uTruth, uTruth0, uTruth1;
Kit_Node_t * pNode;
int i;
// sanity checks
assert( Kit_GraphLeaveNum(pGraph) >= 0 );
assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
assert( Kit_GraphLeaveNum(pGraph) <= 5 );
// check for constant function
if ( Kit_GraphIsConst(pGraph) )
return Kit_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
return Kit_GraphIsComplement(pGraph)? ~uTruths[Kit_GraphVarInt(pGraph)] : uTruths[Kit_GraphVarInt(pGraph)];
// assign the elementary variables
Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->pFunc = (void *)uTruths[i];
// compute the function for each internal node
Kit_GraphForEachNode( pGraph, pNode, i )
{
uTruth0 = (unsigned)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
uTruth1 = (unsigned)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
uTruth = uTruth0 & uTruth1;
pNode->pFunc = (void *)uTruth;
}
// complement the result if necessary
return Kit_GraphIsComplement(pGraph)? ~uTruth : uTruth;
}
/**Function*************************************************************
Synopsis [Derives the factored form from the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
{
Kit_Graph_t * pGraph;
int RetValue;
// derive SOP
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 );
assert( RetValue == 0 );
// derive factored form
pGraph = Kit_SopFactor( vMemory, 0, nVars, vMemory );
return pGraph;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kitHop.c 0 → 100644
/**CFile****************************************************************
FileName [kitHop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures involving AIGs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitHop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
#include "hop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Kit_GraphToHopInternal( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
Hop_Obj_t * pAnd0, * pAnd1;
int i;
// check for constant function
if ( Kit_GraphIsConst(pGraph) )
return Hop_NotCond( Hop_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
return Hop_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Kit_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Hop_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
pAnd1 = Hop_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Hop_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
return Hop_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
int i;
// collect the fanins
Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->pFunc = Hop_IthVar( pMan, i );
// perform strashing
return Kit_GraphToHopInternal( pMan, pGraph );
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory )
{
Kit_Graph_t * pGraph;
Hop_Obj_t * pFunc;
// perform factoring
pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
// convert graph to the AIG
pFunc = Kit_GraphToHop( pMan, pGraph );
Kit_GraphFree( pGraph );
return pFunc;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ivy/ivyIsop.c → src/opt/kit/kitIsop.c
/**CFile****************************************************************
FileName [ivyIsop.c]
FileName [kitIsop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
PackageName [Computation kit.]
Synopsis [Computing irredundant SOP using truth table.]
Synopsis [ISOP computation based on Morreale's algorithm.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
Revision [$Id: kitIsop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// ISOP computation fails if intermediate memory usage exceed this limit
#define IVY_ISOP_MEM_LIMIT 16*4096
// intermediate ISOP representation
typedef struct Ivy_Sop_t_ Ivy_Sop_t;
struct Ivy_Sop_t_
{
unsigned * pCubes;
int nCubes;
};
#define KIT_ISOP_MEM_LIMIT (1<<16)
// static procedures to compute ISOP
static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
static unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
static unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -47,9 +39,9 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, I
Synopsis [Computes ISOP from TT.]
Description [Returns the cover in vCover. Uses the rest of array in vCover
Description [Returns the cover in vMemory. Uses the rest of array in vMemory
as an intermediate memory storage. Returns the cover with -1 cubes, if the
the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of
the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of
intermediate data).]
SideEffects []
......@@ -57,10 +49,10 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, I
SeeAlso []
***********************************************************************/
int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth )
{
Ivy_Sop_t cRes, * pcRes = &cRes;
Ivy_Sop_t cRes2, * pcRes2 = &cRes2;
Kit_Sop_t cRes, * pcRes = &cRes;
Kit_Sop_t cRes2, * pcRes2 = &cRes2;
unsigned * pResult;
int RetValue = 0;
assert( nVars >= 0 && nVars < 16 );
......@@ -68,13 +60,13 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBo
// for ( i = nVars; i < 5; i++ )
// assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
// prepare memory manager
Vec_IntClear( vCover );
Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT );
Vec_IntClear( vMemory );
Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
// compute ISOP for the direct polarity
pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover );
pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
if ( pcRes->nCubes == -1 )
{
vCover->nSize = -1;
vMemory->nSize = -1;
return 0;
}
assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
......@@ -82,7 +74,7 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBo
{
// compute ISOP for the complemented polarity
Extra_TruthNot( puTruth, puTruth, nVars );
pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover );
pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
if ( pcRes2->nCubes >= 0 )
{
assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
......@@ -94,10 +86,10 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBo
}
Extra_TruthNot( puTruth, puTruth, nVars );
}
// printf( "%d ", vCover->nSize );
// printf( "%d ", vMemory->nSize );
// move the cover representation to the beginning of the memory buffer
memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
Vec_IntShrink( vCover, pcRes->nCubes );
memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
Vec_IntShrink( vMemory, pcRes->nCubes );
return RetValue;
}
......@@ -112,10 +104,10 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBo
SeeAlso []
***********************************************************************/
unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
{
Ivy_Sop_t cRes0, cRes1, cRes2;
Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
Kit_Sop_t cRes0, cRes1, cRes2;
Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
unsigned * puRes0, * puRes1, * puRes2;
unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
int i, k, Var, nWords, nWordsAll;
......@@ -159,7 +151,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
// consider a simple case when one-word computation can be used
if ( Var < 5 )
{
unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
for ( i = 0; i < nWordsAll; i++ )
pTemp[i] = uRes;
return pTemp;
......@@ -172,14 +164,14 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
pTemp0 = pTemp; pTemp1 = pTemp + nWords;
// solve for cofactors
Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
if ( pcRes0->nCubes == -1 )
{
pcRes->nCubes = -1;
return NULL;
}
Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
if ( pcRes1->nCubes == -1 )
{
pcRes->nCubes = -1;
......@@ -189,7 +181,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
if ( pcRes2->nCubes == -1 )
{
pcRes->nCubes = -1;
......@@ -205,9 +197,9 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
}
k = 0;
for ( i = 0; i < pcRes0->nCubes; i++ )
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
for ( i = 0; i < pcRes1->nCubes; i++ )
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
for ( i = 0; i < pcRes2->nCubes; i++ )
pcRes->pCubes[k++] = pcRes2->pCubes[i];
assert( k == pcRes->nCubes );
......@@ -236,11 +228,11 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
SeeAlso []
***********************************************************************/
unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
{
unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
Ivy_Sop_t cRes0, cRes1, cRes2;
Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
Kit_Sop_t cRes0, cRes1, cRes2;
Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
int i, k, Var;
assert( nVars <= 5 );
......@@ -278,19 +270,19 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
// solve for cofactors
uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
if ( pcRes0->nCubes == -1 )
{
pcRes->nCubes = -1;
return 0;
}
uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
if ( pcRes1->nCubes == -1 )
{
pcRes->nCubes = -1;
return 0;
}
uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
if ( pcRes2->nCubes == -1 )
{
pcRes->nCubes = -1;
......@@ -306,9 +298,9 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
}
k = 0;
for ( i = 0; i < pcRes0->nCubes; i++ )
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
for ( i = 0; i < pcRes1->nCubes; i++ )
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
for ( i = 0; i < pcRes2->nCubes; i++ )
pcRes->pCubes[k++] = pcRes2->pCubes[i];
assert( k == pcRes->nCubes );
......
src/opt/kit/kitSop.c 0 → 100644
/**CFile****************************************************************
FileName [kitSop.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures involving SOPs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates SOP from the cube array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory )
{
unsigned uCube;
int i;
// start the cover
cResult->nCubes = 0;
cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
// add the cubes
Vec_IntForEachEntry( vInput, uCube, i )
Kit_SopPushCube( cResult, uCube );
}
/**Function*************************************************************
Synopsis [Creates SOP from the cube array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nLits, Vec_Int_t * vMemory )
{
unsigned uCube, uMask = 0;
int i, nCubes = Vec_IntSize(vInput);
// start the cover
cResult->nCubes = 0;
cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
// add the cubes
// Vec_IntForEachEntry( vInput, uCube, i )
for ( i = 0; i < nCubes; i++ )
{
uCube = Vec_IntEntry( vInput, i );
uMask = ((uCube | (uCube >> 1)) & 0x55555555);
uMask |= (uMask << 1);
Kit_SopPushCube( cResult, uCube ^ uMask );
}
}
/**Function*************************************************************
Synopsis [Duplicates SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
{
unsigned uCube;
int i;
// start the cover
cResult->nCubes = 0;
cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
// add the cubes
Kit_SopForEachCube( cSop, uCube, i )
Kit_SopPushCube( cResult, uCube );
}
/**Function*************************************************************
Synopsis [Derives the quotient of division by literal.]
Description [Reduces the cover to be equal to the result of
division of the given cover by the literal.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit )
{
unsigned uCube;
int i, k = 0;
Kit_SopForEachCube( cSop, uCube, i )
{
if ( Kit_CubeHasLit(uCube, iLit) )
Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
}
Kit_SopShrink( cSop, k );
}
/**Function*************************************************************
Synopsis [Divides cover by one cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
{
unsigned uCube, uDiv;
int i;
// get the only cube
assert( Kit_SopCubeNum(cDiv) == 1 );
uDiv = Kit_SopCube(cDiv, 0);
// allocate covers
vQuo->nCubes = 0;
vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
vRem->nCubes = 0;
vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
// sort the cubes
Kit_SopForEachCube( cSop, uCube, i )
{
if ( Kit_CubeContains( uCube, uDiv ) )
Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
else
Kit_SopPushCube( vRem, uCube );
}
}
/**Function*************************************************************
Synopsis [Divides cover by one cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
{
unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
int i, i2, k, k2, nCubesRem;
assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
// consider special case
if ( Kit_SopCubeNum(cDiv) == 1 )
{
Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
return;
}
// allocate quotient
vQuo->nCubes = 0;
vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
// for each cube of the cover
// it either belongs to the quotient or to the remainder
Kit_SopForEachCube( cSop, uCube, i )
{
// skip taken cubes
if ( Kit_CubeIsMarked(uCube) )
continue;
// find a matching cube in the divisor
Kit_SopForEachCube( cDiv, uDiv, k )
if ( Kit_CubeContains( uCube, uDiv ) )
break;
// the cube is not found
if ( k == Kit_SopCubeNum(cDiv) )
continue;
// the quotient cube exists
uQuo = Kit_CubeSharp( uCube, uDiv );
// find corresponding cubes for other cubes of the divisor
Kit_SopForEachCube( cDiv, uDiv2, k2 )
{
if ( k2 == k )
continue;
// find a matching cube
Kit_SopForEachCube( cSop, uCube2, i2 )
{
// skip taken cubes
if ( Kit_CubeIsMarked(uCube2) )
continue;
// check if the cube can be used
if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
break;
}
// the case when the cube is not found
if ( i2 == Kit_SopCubeNum(cSop) )
break;
}
// we did not find some cubes - continue looking at other cubes
if ( k2 != Kit_SopCubeNum(cDiv) )
continue;
// we found all cubes - add the quotient cube
Kit_SopPushCube( vQuo, uQuo );
// mark the first cube
Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
// mark other cubes that have this quotient
Kit_SopForEachCube( cDiv, uDiv2, k2 )
{
if ( k2 == k )
continue;
// find a matching cube
Kit_SopForEachCube( cSop, uCube2, i2 )
{
// skip taken cubes
if ( Kit_CubeIsMarked(uCube2) )
continue;
// check if the cube can be used
if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
break;
}
assert( i2 < Kit_SopCubeNum(cSop) );
// the cube is found, mark it
// (later we will add all unmarked cubes to the remainder)
Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
}
}
// determine the number of cubes in the remainder
nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
// allocate remainder
vRem->nCubes = 0;
vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
// finally add the remaining unmarked cubes to the remainder
// and clean the marked cubes in the cover
Kit_SopForEachCube( cSop, uCube, i )
{
if ( !Kit_CubeIsMarked(uCube) )
{
Kit_SopPushCube( vRem, uCube );
continue;
}
Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
}
assert( nCubesRem == Kit_SopCubeNum(vRem) );
}
/**Function*************************************************************
Synopsis [Returns the common cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop )
{
unsigned uMask, uCube;
int i;
uMask = ~(unsigned)0;
Kit_SopForEachCube( cSop, uCube, i )
uMask &= uCube;
return uMask;
}
/**Function*************************************************************
Synopsis [Makes the cover cube-free.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopMakeCubeFree( Kit_Sop_t * cSop )
{
unsigned uMask, uCube;
int i;
uMask = Kit_SopCommonCube( cSop );
if ( uMask == 0 )
return;
// remove the common cube
Kit_SopForEachCube( cSop, uCube, i )
Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
}
/**Function*************************************************************
Synopsis [Checks if the cover is cube-free.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopIsCubeFree( Kit_Sop_t * cSop )
{
return Kit_SopCommonCube( cSop ) == 0;
}
/**Function*************************************************************
Synopsis [Creates SOP composes of the common cube of the given SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
{
assert( Kit_SopCubeNum(cSop) > 0 );
cResult->nCubes = 0;
cResult->pCubes = Vec_IntFetch( vMemory, 1 );
Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
}
/**Function*************************************************************
Synopsis [Find any literal that occurs more than once.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits )
{
unsigned uCube;
int i, k, nLitsCur;
// go through each literal
for ( i = 0; i < nLits; i++ )
{
// go through all the cubes
nLitsCur = 0;
Kit_SopForEachCube( cSop, uCube, k )
if ( Kit_CubeHasLit(uCube, i) )
nLitsCur++;
if ( nLitsCur > 1 )
return i;
}
return -1;
}
/**Function*************************************************************
Synopsis [Find the least often occurring literal.]
Description [Find the least often occurring literal among those
that occur more than once.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopWorstLiteral( Kit_Sop_t * cSop, int nLits )
{
unsigned uCube;
int i, k, iMin, nLitsMin, nLitsCur;
int fUseFirst = 1;
// go through each literal
iMin = -1;
nLitsMin = 1000000;
for ( i = 0; i < nLits; i++ )
{
// go through all the cubes
nLitsCur = 0;
Kit_SopForEachCube( cSop, uCube, k )
if ( Kit_CubeHasLit(uCube, i) )
nLitsCur++;
// skip the literal that does not occur or occurs once
if ( nLitsCur < 2 )
continue;
// check if this is the best literal
if ( fUseFirst )
{
if ( nLitsMin > nLitsCur )
{
nLitsMin = nLitsCur;
iMin = i;
}
}
else
{
if ( nLitsMin >= nLitsCur )
{
nLitsMin = nLitsCur;
iMin = i;
}
}
}
if ( nLitsMin < 1000000 )
return iMin;
return -1;
}
/**Function*************************************************************
Synopsis [Find the least often occurring literal.]
Description [Find the least often occurring literal among those
that occur more than once.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopBestLiteral( Kit_Sop_t * cSop, int nLits, unsigned uMask )
{
unsigned uCube;
int i, k, iMax, nLitsMax, nLitsCur;
int fUseFirst = 1;
// go through each literal
iMax = -1;
nLitsMax = -1;
for ( i = 0; i < nLits; i++ )
{
if ( !Kit_CubeHasLit(uMask, i) )
continue;
// go through all the cubes
nLitsCur = 0;
Kit_SopForEachCube( cSop, uCube, k )
if ( Kit_CubeHasLit(uCube, i) )
nLitsCur++;
// skip the literal that does not occur or occurs once
if ( nLitsCur < 2 )
continue;
// check if this is the best literal
if ( fUseFirst )
{
if ( nLitsMax < nLitsCur )
{
nLitsMax = nLitsCur;
iMax = i;
}
}
else
{
if ( nLitsMax <= nLitsCur )
{
nLitsMax = nLitsCur;
iMax = i;
}
}
}
if ( nLitsMax >= 0 )
return iMax;
return -1;
}
/**Function*************************************************************
Synopsis [Computes a level-zero kernel.]
Description [Modifies the cover to contain one level-zero kernel.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopDivisorZeroKernel_rec( Kit_Sop_t * cSop, int nLits )
{
int iLit;
// find any literal that occurs at least two times
iLit = Kit_SopWorstLiteral( cSop, nLits );
if ( iLit == -1 )
return;
// derive the cube-free quotient
Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
Kit_SopMakeCubeFree( cSop ); // the same cover
// call recursively
Kit_SopDivisorZeroKernel_rec( cSop, nLits ); // the same cover
}
/**Function*************************************************************
Synopsis [Computes the quick divisor of the cover.]
Description [Returns 0, if there is no divisor other than trivial.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
{
if ( Kit_SopCubeNum(cSop) <= 1 )
return 0;
if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
return 0;
// duplicate the cover
Kit_SopDup( cResult, cSop, vMemory );
// perform the kerneling
Kit_SopDivisorZeroKernel_rec( cResult, nLits );
assert( Kit_SopCubeNum(cResult) > 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Create the one-literal cover with the best literal from cSop.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory )
{
int iLitBest;
// get the best literal
iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
// start the cover
cResult->nCubes = 0;
cResult->pCubes = Vec_IntFetch( vMemory, 1 );
// set the cube
Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kitTruth.c 0 → 100644
/**CFile****************************************************************
FileName [kitTruth.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures involving truth tables.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitTruth.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static unsigned s_VarMasks[5][2] = {
{ 0x33333333, 0xAAAAAAAA },
{ 0x55555555, 0xCCCCCCCC },
{ 0x0F0F0F0F, 0xF0F0F0F0 },
{ 0x00FF00FF, 0xFF00FF00 },
{ 0x0000FFFF, 0xFFFF0000 }
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Swaps two adjacent variables in the truth table.]
Description [Swaps var number Start and var number Start+1 (0-based numbers).
The input truth table is pIn. The output truth table is pOut.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
{
static unsigned PMasks[4][3] = {
{ 0x99999999, 0x22222222, 0x44444444 },
{ 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
{ 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
{ 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
};
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step, Shift;
assert( iVar < nVars - 1 );
if ( iVar < 4 )
{
Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
}
else if ( iVar > 4 )
{
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 4*Step )
{
for ( i = 0; i < Step; i++ )
pOut[i] = pIn[i];
for ( i = 0; i < Step; i++ )
pOut[Step+i] = pIn[2*Step+i];
for ( i = 0; i < Step; i++ )
pOut[2*Step+i] = pIn[Step+i];
for ( i = 0; i < Step; i++ )
pOut[3*Step+i] = pIn[3*Step+i];
pIn += 4*Step;
pOut += 4*Step;
}
}
else // if ( iVar == 4 )
{
for ( i = 0; i < nWords; i += 2 )
{
pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
}
}
}
/**Function*************************************************************
Synopsis [Swaps two adjacent variables in the truth table.]
Description [Swaps var number Start and var number Start+1 (0-based numbers).
The input truth table is pIn. The output truth table is pOut.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int Start )
{
int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
int i, k, Step;
assert( Start < nVars - 1 );
switch ( Start )
{
case 0:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
return;
case 4:
for ( i = 0; i < nWords; i += 2 )
{
pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
}
return;
default:
Step = (1 << (Start - 5));
for ( k = 0; k < nWords; k += 4*Step )
{
for ( i = 0; i < Step; i++ )
pOut[i] = pIn[i];
for ( i = 0; i < Step; i++ )
pOut[Step+i] = pIn[2*Step+i];
for ( i = 0; i < Step; i++ )
pOut[2*Step+i] = pIn[Step+i];
for ( i = 0; i < Step; i++ )
pOut[3*Step+i] = pIn[3*Step+i];
pIn += 4*Step;
pOut += 4*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Expands the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
(Phase) contains shows where the variables should go.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
{
unsigned * pTemp;
int i, k, Var = nVars - 1, Counter = 0;
for ( i = nVarsAll - 1; i >= 0; i-- )
if ( Phase & (1 << i) )
{
for ( k = Var; k < i; k++ )
{
Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
pTemp = pIn; pIn = pOut; pOut = pTemp;
Counter++;
}
Var--;
}
assert( Var == -1 );
// swap if it was moved an even number of times
if ( !(Counter & 1) )
Kit_TruthCopy( pOut, pIn, nVarsAll );
}
/**Function*************************************************************
Synopsis [Shrinks the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
(Phase) contains shows what variables should remain.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
{
unsigned * pTemp;
int i, k, Var = 0, Counter = 0;
for ( i = 0; i < nVarsAll; i++ )
if ( Phase & (1 << i) )
{
for ( k = i-1; k >= Var; k-- )
{
Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
pTemp = pIn; pIn = pOut; pOut = pTemp;
Counter++;
}
Var++;
}
assert( Var == nVars );
// swap if it was moved an even number of times
if ( !(Counter & 1) )
Kit_TruthCopy( pOut, pIn, nVarsAll );
}
/**Function*************************************************************
Synopsis [Returns 1 if TT depends on the given variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
return 1;
return 0;
case 1:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
return 1;
return 0;
case 2:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
return 1;
return 0;
case 3:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
return 1;
return 0;
case 4:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
return 1;
return 0;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
if ( pTruth[i] != pTruth[Step+i] )
return 1;
pTruth += 2*Step;
}
return 0;
}
}
/**Function*************************************************************
Synopsis [Returns the number of support vars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
{
int i, Counter = 0;
for ( i = 0; i < nVars; i++ )
Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
return Counter;
}
/**Function*************************************************************
Synopsis [Returns support of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthSupport( unsigned * pTruth, int nVars )
{
int i, Support = 0;
for ( i = 0; i < nVars; i++ )
if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
Support |= (1 << i);
return Support;
}
/**Function*************************************************************
Synopsis [Computes positive cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
pTruth[i] = pTruth[Step+i];
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Computes negative cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
pTruth[Step+i] = pTruth[i];
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Existentially quantifies the variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pTruth[i] |= pTruth[Step+i];
pTruth[Step+i] = pTruth[i];
}
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Existentially quantifies the variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pTruth[i] &= pTruth[Step+i];
pTruth[Step+i] = pTruth[i];
}
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Computes negative cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pOut[i] = pCof0[i];
pOut[Step+i] = pCof1[Step+i];
}
pOut += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Checks symmetry of two variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
{
static unsigned uTemp0[16], uTemp1[16];
assert( nVars <= 9 );
// compute Cof01
Kit_TruthCopy( uTemp0, pTruth, nVars );
Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
Kit_TruthCofactor1( uTemp0, nVars, iVar1 );
// compute Cof10
Kit_TruthCopy( uTemp1, pTruth, nVars );
Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
Kit_TruthCofactor0( uTemp1, nVars, iVar1 );
// compare
return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
}
/**Function*************************************************************
Synopsis [Checks antisymmetry of two variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
{
static unsigned uTemp0[16], uTemp1[16];
assert( nVars <= 9 );
// compute Cof00
Kit_TruthCopy( uTemp0, pTruth, nVars );
Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
Kit_TruthCofactor0( uTemp0, nVars, iVar1 );
// compute Cof11
Kit_TruthCopy( uTemp1, pTruth, nVars );
Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
Kit_TruthCofactor1( uTemp1, nVars, iVar1 );
// compare
return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
}
/**Function*************************************************************
Synopsis [Changes phase of the function w.r.t. one variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
unsigned Temp;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
Temp = pTruth[i];
pTruth[i] = pTruth[Step+i];
pTruth[Step+i] = Temp;
}
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Computes minimum overlap in supports of cofactors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
{
static unsigned uCofactor[16];
int i, ValueCur, ValueMin, VarMin;
unsigned uSupp0, uSupp1;
int nVars0, nVars1;
assert( nVars <= 9 );
ValueMin = 32;
VarMin = -1;
for ( i = 0; i < nVars; i++ )
{
// get negative cofactor
Kit_TruthCopy( uCofactor, pTruth, nVars );
Kit_TruthCofactor0( uCofactor, nVars, i );
uSupp0 = Kit_TruthSupport( uCofactor, nVars );
nVars0 = Kit_WordCountOnes( uSupp0 );
//Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
// get positive cofactor
Kit_TruthCopy( uCofactor, pTruth, nVars );
Kit_TruthCofactor1( uCofactor, nVars, i );
uSupp1 = Kit_TruthSupport( uCofactor, nVars );
nVars1 = Kit_WordCountOnes( uSupp1 );
//Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
// get the number of common vars
ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
{
ValueMin = ValueCur;
VarMin = i;
}
if ( ValueMin == 0 )
break;
}
if ( pVarMin )
*pVarMin = VarMin;
return ValueMin;
}
/**Function*************************************************************
Synopsis [Counts the number of 1's in each cofactor.]
Description [The resulting numbers are stored in the array of shorts,
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.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Counter;
memset( pStore, 0, sizeof(short) * 2 * nVars );
if ( nVars <= 5 )
{
if ( nVars > 0 )
{
pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
}
if ( nVars > 1 )
{
pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
}
if ( nVars > 2 )
{
pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
}
if ( nVars > 3 )
{
pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
}
if ( nVars > 4 )
{
pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
}
return;
}
// nVars >= 6
// count 1's for all other variables
for ( k = 0; k < nWords; k++ )
{
Counter = Kit_WordCountOnes( pTruth[k] );
for ( i = 5; i < nVars; i++ )
if ( k & (1 << (i-5)) )
pStore[2*i+1] += Counter;
else
pStore[2*i+0] += Counter;
}
// count 1's for the first five variables
for ( k = 0; k < nWords/2; k++ )
{
pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
pTruth += 2;
}
}
/**Function*************************************************************
Synopsis [Canonicize the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Kit_TruthHash( unsigned * pIn, int nWords )
{
// The 1,024 smallest prime numbers used to compute the hash value
// http://www.math.utah.edu/~alfeld/math/primelist.html
static int HashPrimes[1024] = { 2, 3, 5,
7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97,
101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191,
193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283,
293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401,
409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509,
521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631,
641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751,
757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877,
881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091,
1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193,
1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291,
1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423,
1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493,
1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699,
1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811,
1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931,
1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029,
2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137,
2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267,
2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357,
2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459,
2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593,
2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693,
2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791,
2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903,
2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023,
3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167,
3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271,
3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373,
3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511,
3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607,
3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709,
3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833,
3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931,
3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057,
4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177,
4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283,
4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423,
4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547,
4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657,
4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789,
4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931,
4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011,
5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147,
5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279,
5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413,
5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507,
5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647,
5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743,
5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857,
5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007,
6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121,
6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247,
6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343,
6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473,
6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607,
6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733,
6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857,
6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971,
6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103,
7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229,
7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369,
7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517,
7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603,
7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723,
7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873,
7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009,
8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123,
8147, 8161 };
int i;
unsigned uHashKey;
assert( nWords <= 1024 );
uHashKey = 0;
for ( i = 0; i < nWords; i++ )
uHashKey ^= HashPrimes[i] * pIn[i];
return uHashKey;
}
/**Function*************************************************************
Synopsis [Canonicize the truth table.]
Description [Returns the phase. ]
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
{
unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
int nWords = Kit_TruthWordNum( nVars );
int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
unsigned uCanonPhase;
// canonicize output
uCanonPhase = 0;
nOnes = Kit_TruthCountOnes(pIn, nVars);
if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
{
uCanonPhase |= (1 << nVars);
Kit_TruthNot( pIn, pIn, nVars );
}
// collect the minterm counts
Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
if ( pStore[2*i+0] <= pStore[2*i+1] )
continue;
uCanonPhase |= (1 << i);
Temp = pStore[2*i+0];
pStore[2*i+0] = pStore[2*i+1];
pStore[2*i+1] = Temp;
Kit_TruthChangePhase( pIn, nVars, i );
}
// Kit_PrintHexadecimal( stdout, pIn, nVars );
// printf( "\n" );
// permute
Counter = 0;
do {
fChange = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pStore[2*i] <= pStore[2*(i+1)] )
continue;
Counter++;
fChange = 1;
Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[i+1];
pCanonPerm[i+1] = Temp;
Temp = pStore[2*i];
pStore[2*i] = pStore[2*(i+1)];
pStore[2*(i+1)] = Temp;
Temp = pStore[2*i+1];
pStore[2*i+1] = pStore[2*(i+1)+1];
pStore[2*(i+1)+1] = Temp;
Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
pTemp = pIn; pIn = pOut; pOut = pTemp;
}
} while ( fChange );
/*
Kit_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
for ( i = 0; i < nVars; i++ )
printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
printf( " C = %d\n", Counter );
Kit_PrintHexadecimal( stdout, pIn, nVars );
printf( "\n" );
*/
/*
// process symmetric variable groups
uSymms = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
continue;
if ( pStore[2*i] != pStore[2*i+1] )
continue;
if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
continue;
if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
Kit_TruthChangePhase( pIn, nVars, i+1 );
}
*/
/*
// process symmetric variable groups
uSymms = 0;
for ( i = 0; i < nVars-1; i++ )
{
if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
continue;
// i and i+1 can be symmetric
// find the end of this group
for ( k = i+1; k < nVars; k++ )
if ( pStore[2*i] != pStore[2*k] )
break;
Limit = k;
assert( i < Limit-1 );
// go through the variables in this group
for ( j = i + 1; j < Limit; j++ )
{
// check symmetry
if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
{
uSymms |= (1 << j);
continue;
}
// they are phase-unknown
if ( pStore[2*i] == pStore[2*i+1] )
{
if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
{
Kit_TruthChangePhase( pIn, nVars, j );
uCanonPhase ^= (1 << j);
uSymms |= (1 << j);
continue;
}
}
// they are not symmetric - move j as far as it goes in the group
for ( k = j; k < Limit-1; k++ )
{
Counter++;
Temp = pCanonPerm[k];
pCanonPerm[k] = pCanonPerm[k+1];
pCanonPerm[k+1] = Temp;
assert( pStore[2*k] == pStore[2*(k+1)] );
Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
pTemp = pIn; pIn = pOut; pOut = pTemp;
}
Limit--;
j--;
}
i = Limit - 1;
}
*/
// swap if it was moved an even number of times
if ( Counter & 1 )
Kit_TruthCopy( pOut, pIn, nVars );
return uCanonPhase;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/kit_.c 0 → 100644
/**CFile****************************************************************
FileName [kit_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kit_.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/kit/module.make 0 → 100644
SRC += src/opt/kit/kitBdd.c \
src/opt/kit/kitFactor.c \
src/opt/kit/kitGraph.c \
src/opt/kit/kitHop.c \
src/opt/kit/kitIsop.c \
src/opt/kit/kitSop.c \
src/opt/kit/kitTruth.c
src/sat/bsat/satSolver.c
......@@ -801,14 +801,14 @@ void sat_solver_reducedb(sat_solver* s)
vecp_resize(&s->learnts,j);
}
static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts)
static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts)
{
int* levels = s->levels;
double var_decay = 0.95;
double clause_decay = 0.999;
double random_var_freq = 0.02;
int conflictC = 0;
sint64 conflictC = 0;
veci learnt_clause;
int i;
......@@ -1118,8 +1118,8 @@ bool sat_solver_simplify(sat_solver* s)
int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
{
double nof_conflicts = 100;
double nof_learnts = sat_solver_nclauses(s) / 3;
sint64 nof_conflicts = 100;
sint64 nof_learnts = sat_solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
......@@ -1178,9 +1178,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
s->progress_estimate*100);
fflush(stdout);
}
status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
status = sat_solver_search(s, nof_conflicts, nof_learnts);
nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
// quit the loop if reached an external limit
if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment