diff options
Diffstat (limited to 'src/temp')
31 files changed, 7997 insertions, 0 deletions
diff --git a/src/temp/esop/esop.h b/src/temp/esop/esop.h new file mode 100644 index 00000000..d6cdff71 --- /dev/null +++ b/src/temp/esop/esop.h @@ -0,0 +1,722 @@ +/**CFile**************************************************************** + + FileName [esop.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: esop.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __ESOP_H__ +#define __ESOP_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#include "stdio.h" +#include "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Esop_Man_t_ Esop_Man_t; +typedef struct Esop_Cube_t_ Esop_Cube_t; +typedef struct Esop_MmFixed_t_ Esop_MmFixed_t; + +struct Esop_Man_t_ +{ + int nVars; // the number of vars + int nWords; // the number of words + Esop_MmFixed_t * pMemMan1; // memory manager for cubes + Esop_MmFixed_t * pMemMan2; // memory manager for cubes + Esop_MmFixed_t * pMemMan4; // memory manager for cubes + Esop_MmFixed_t * pMemMan8; // memory manager for cubes + // temporary cubes + Esop_Cube_t * pOne0; // tautology cube + Esop_Cube_t * pOne1; // tautology cube + Esop_Cube_t * pTriv0; // trivial cube + Esop_Cube_t * pTriv1; // trivial cube + Esop_Cube_t * pTemp; // cube for computing the distance + Esop_Cube_t * pBubble; // cube used as a separator + // temporary storage for the new cover + int nCubes; // the number of cubes + Esop_Cube_t ** ppStore; // storage for cubes by number of literals +}; + +struct Esop_Cube_t_ +{ + Esop_Cube_t * pNext; // the pointer to the next cube in the cover + unsigned nVars : 10; // the number of variables + unsigned nWords : 12; // the number of machine words + unsigned nLits : 10; // the number of literals in the cube + unsigned uData[1]; // the bit-data for the cube +}; + +#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) +#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#define REALLOC(type, obj, num) \ + ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ + ((type *) malloc(sizeof(type) * (num)))) + +// iterators through the entries in the linked lists of cubes +#define Esop_CoverForEachCube( pCover, pCube ) \ + for ( pCube = pCover; \ + pCube; \ + pCube = pCube->pNext ) +#define Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ + for ( pCube = pCover, \ + pCube2 = pCube? pCube->pNext: NULL; \ + pCube; \ + pCube = pCube2, \ + pCube2 = pCube? pCube->pNext: NULL ) +#define Esop_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ + for ( pCube = pCover, \ + ppPrev = &(pCover); \ + pCube; \ + ppPrev = &pCube->pNext, \ + pCube = pCube->pNext ) + + +// macros to get hold of bits and values in the cubes +static inline int Esop_CubeHasBit( Esop_Cube_t * p, int i ) { return (p->uData[i >> 5] & (1<<(i & 31))) > 0; } +static inline void Esop_CubeSetBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] |= (1<<(i & 31)); } +static inline void Esop_CubeXorBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] ^= (1<<(i & 31)); } +static inline int Esop_CubeGetVar( Esop_Cube_t * p, int Var ) { return 3 & (p->uData[(Var<<1)>>5] >> ((Var<<1) & 31)); } +static inline void Esop_CubeXorVar( Esop_Cube_t * p, int Var, int Value ) { p->uData[(Var<<1)>>5] ^= (Value<<((Var<<1) & 31)); } +static inline int Esop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } + +/*=== esopMem.c ===========================================================*/ +extern Esop_MmFixed_t * Esop_MmFixedStart( int nEntrySize ); +extern void Esop_MmFixedStop( Esop_MmFixed_t * p, int fVerbose ); +extern char * Esop_MmFixedEntryFetch( Esop_MmFixed_t * p ); +extern void Esop_MmFixedEntryRecycle( Esop_MmFixed_t * p, char * pEntry ); +extern void Esop_MmFixedRestart( Esop_MmFixed_t * p ); +extern int Esop_MmFixedReadMemUsage( Esop_MmFixed_t * p ); +/*=== esopMin.c ===========================================================*/ +extern void Esop_EsopMinimize( Esop_Man_t * p ); +extern void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube ); +/*=== esopMan.c ===========================================================*/ +extern Esop_Man_t * Esop_ManAlloc( int nVars ); +extern void Esop_ManClean( Esop_Man_t * p, int nSupp ); +extern void Esop_ManFree( Esop_Man_t * p ); +/*=== esopUtil.c ===========================================================*/ +extern void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube ); +extern void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover ); +extern void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p ); +extern void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop ); +extern void Esop_CoverCheck( Esop_Man_t * p ); +extern int Esop_CubeCheck( Esop_Cube_t * pCube ); +extern Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize ); +extern void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover ); +extern int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CubeAlloc( Esop_Man_t * p ) +{ + Esop_Cube_t * pCube; + if ( p->nWords <= 1 ) + pCube = (Esop_Cube_t *)Esop_MmFixedEntryFetch( p->pMemMan1 ); + else if ( p->nWords <= 2 ) + pCube = (Esop_Cube_t *)Esop_MmFixedEntryFetch( p->pMemMan2 ); + else if ( p->nWords <= 4 ) + pCube = (Esop_Cube_t *)Esop_MmFixedEntryFetch( p->pMemMan4 ); + else if ( p->nWords <= 8 ) + pCube = (Esop_Cube_t *)Esop_MmFixedEntryFetch( p->pMemMan8 ); + pCube->pNext = NULL; + pCube->nVars = p->nVars; + pCube->nWords = p->nWords; + pCube->nLits = 0; + memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube representing elementary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CubeAllocVar( Esop_Man_t * p, int iVar, int fCompl ) +{ + Esop_Cube_t * pCube; + pCube = Esop_CubeAlloc( p ); + Esop_CubeXorBit( pCube, iVar*2+fCompl ); + pCube->nLits = 1; + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CubeDup( Esop_Man_t * p, Esop_Cube_t * pCopy ) +{ + Esop_Cube_t * pCube; + pCube = Esop_CubeAlloc( p ); + memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); + pCube->nLits = pCopy->nLits; + return pCube; +} + +/**Function************************************************************* + + Synopsis [Recycles the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CubeRecycle( Esop_Man_t * p, Esop_Cube_t * pCube ) +{ + if ( pCube->nWords <= 1 ) + Esop_MmFixedEntryRecycle( p->pMemMan1, (char *)pCube ); + else if ( pCube->nWords <= 2 ) + Esop_MmFixedEntryRecycle( p->pMemMan2, (char *)pCube ); + else if ( pCube->nWords <= 4 ) + Esop_MmFixedEntryRecycle( p->pMemMan4, (char *)pCube ); + else if ( pCube->nWords <= 8 ) + Esop_MmFixedEntryRecycle( p->pMemMan8, (char *)pCube ); +} + +/**Function************************************************************* + + Synopsis [Recycles the cube cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CoverRecycle( Esop_Man_t * p, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube, * pCube2; + if ( pCover == NULL ) + return; + if ( pCover->nWords <= 1 ) + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Esop_MmFixedEntryRecycle( p->pMemMan1, (char *)pCube ); + else if ( pCover->nWords <= 2 ) + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Esop_MmFixedEntryRecycle( p->pMemMan2, (char *)pCube ); + else if ( pCover->nWords <= 4 ) + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Esop_MmFixedEntryRecycle( p->pMemMan4, (char *)pCube ); + else if ( pCover->nWords <= 8 ) + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Esop_MmFixedEntryRecycle( p->pMemMan8, (char *)pCube ); +} + +/**Function************************************************************* + + Synopsis [Recycles the cube cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CoverDup( Esop_Man_t * p, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube, * pCubeNew; + Esop_Cube_t * pCoverNew = NULL, ** ppTail = &pCoverNew; + Esop_CoverForEachCube( pCover, pCube ) + { + pCubeNew = Esop_CubeDup( p, pCube ); + *ppTail = pCubeNew; + ppTail = &pCubeNew->pNext; + } + *ppTail = NULL; + return pCoverNew; +} + + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubeCountLits( Esop_Cube_t * pCube ) +{ + unsigned uData; + int Count = 0, i, w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Count++; + } + return Count; +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CubeGetLits( Esop_Cube_t * pCube, Vec_Int_t * vLits ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vLits ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vLits, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CoverCountCubes( Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube; + int Count = 0; + Esop_CoverForEachCube( pCover, pCube ) + Count++; + return Count; +} + + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubesDisjoint( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) +{ + unsigned uData; + int i; + assert( pCube0->nVars == pCube1->nVars ); + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] & pCube1->uData[i]; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( uData != 0x55555555 ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Collects the disjoint variables of the two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CoverGetDisjVars( Esop_Cube_t * pThis, Esop_Cube_t * pCube, Vec_Int_t * vVars ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vVars ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; + uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); + if ( uData == 0 ) + continue; + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vVars, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubesDistOne( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, Esop_Cube_t * pTemp ) +{ + unsigned uData; + int i, fFound = 0; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + { + if ( pTemp ) pTemp->uData[i] = 0; + continue; + } + if ( fFound ) + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (uData & (uData-1)) > 0 ) // more than one 1 + return 0; + if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); + fFound = 1; + } + if ( fFound == 0 ) + { + printf( "\n" ); + Esop_CubeWrite( stdout, pCube0 ); + Esop_CubeWrite( stdout, pCube1 ); + printf( "Error: Esop_CubesDistOne() looks at two equal cubes!\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubesDistTwo( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, int * pVar0, int * pVar1 ) +{ + unsigned uData;//, uData2; + int i, k, Var0 = -1, Var1 = -1; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + continue; + if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) + return 0; + for ( k = 0; k < 32; k += 2 ) + if ( uData & (1 << k) ) + { + if ( Var0 == -1 ) + Var0 = 16 * i + k/2; + else if ( Var1 == -1 ) + Var1 = 16 * i + k/2; + else + return 0; + } + /* + if ( Var0 >= 0 ) + { + uData &= 0xFFFF; + uData2 = (uData >> 16); + if ( uData && uData2 ) + return 0; + if ( uData ) + { + } + uData }= uData2; + uData &= 0x + } + */ + } + if ( Var0 >= 0 && Var1 >= 0 ) + { + *pVar0 = Var0; + *pVar1 = Var1; + return 1; + } + if ( Var0 == -1 || Var1 == -1 ) + { + printf( "\n" ); + Esop_CubeWrite( stdout, pCube0 ); + Esop_CubeWrite( stdout, pCube1 ); + printf( "Error: Esop_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CubesProduct( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) +{ + Esop_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Esop_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; + pCube->nLits = Esop_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Esop_Cube_t * Esop_CubesXor( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) +{ + Esop_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Esop_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; + pCube->nLits = Esop_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubesAreEqual( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( pCube0->uData[i] != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CubeIsContained( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CubesTransform( Esop_Cube_t * pCube, Esop_Cube_t * pDist, Esop_Cube_t * pMask ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; + pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); + } +} + +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of distance-1 merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CubesTransformOr( Esop_Cube_t * pCube, Esop_Cube_t * pDist ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + pCube->uData[w] |= pDist->uData[w]; +} + + + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Esop_CoverExpandRemoveEqual( Esop_Man_t * p, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube, * pCube2, * pThis; + if ( pCover == NULL ) + { + Esop_ManClean( p, p->nVars ); + return; + } + Esop_ManClean( p, pCover->nVars ); + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + // go through the linked list + Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + if ( Esop_CubesAreEqual( pCube, pThis ) ) + { + Esop_CubeRecycle( p, pCube ); + break; + } + if ( pThis != NULL ) + continue; + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Esop_CoverContainsCube( Esop_Man_t * p, Esop_Cube_t * pCube ) +{ + Esop_Cube_t * pThis; + int i; +/* + // this cube cannot be equal to any cube + Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + { + if ( Esop_CubesAreEqual( pCube, pThis ) ) + { + Esop_CubeWrite( stdout, pCube ); + assert( 0 ); + } + } +*/ + // try to find a containing cube + for ( i = 0; i <= (int)pCube->nLits; i++ ) + Esop_CoverForEachCube( p->ppStore[i], pThis ) + { + // skip the bubble + if ( pThis != p->pBubble && Esop_CubeIsContained( pThis, pCube ) ) + return 1; + } + return 0; +} + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/esop/esopMan.c b/src/temp/esop/esopMan.c new file mode 100644 index 00000000..e81411f8 --- /dev/null +++ b/src/temp/esop/esopMan.c @@ -0,0 +1,117 @@ +/**CFile**************************************************************** + + FileName [esopMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [SOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: esopMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "esop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Esop_Man_t * Esop_ManAlloc( int nVars ) +{ + Esop_Man_t * pMan; + // start the manager + pMan = ALLOC( Esop_Man_t, 1 ); + memset( pMan, 0, sizeof(Esop_Man_t) ); + pMan->nVars = nVars; + pMan->nWords = Esop_BitWordNum( nVars * 2 ); + pMan->pMemMan1 = Esop_MmFixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) ); + pMan->pMemMan2 = Esop_MmFixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) ); + pMan->pMemMan4 = Esop_MmFixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) ); + pMan->pMemMan8 = Esop_MmFixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (8 - 1) ); + // allocate storage for the temporary cover + pMan->ppStore = ALLOC( Esop_Cube_t *, pMan->nVars + 1 ); + // create tautology cubes + Esop_ManClean( pMan, nVars ); + pMan->pOne0 = Esop_CubeAlloc( pMan ); + pMan->pOne1 = Esop_CubeAlloc( pMan ); + pMan->pTemp = Esop_CubeAlloc( pMan ); + pMan->pBubble = Esop_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0; + // create trivial cubes + Esop_ManClean( pMan, 1 ); + pMan->pTriv0 = Esop_CubeAllocVar( pMan, 0, 0 ); + pMan->pTriv1 = Esop_CubeAllocVar( pMan, 0, 0 ); + Esop_ManClean( pMan, nVars ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Cleans the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_ManClean( Esop_Man_t * p, int nSupp ) +{ + // set the size of the cube manager + p->nVars = nSupp; + p->nWords = Esop_BitWordNum(2*nSupp); + // clean the storage + memset( p->ppStore, 0, sizeof(Esop_Cube_t *) * (nSupp + 1) ); + p->nCubes = 0; +} + +/**Function************************************************************* + + Synopsis [Stops the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_ManFree( Esop_Man_t * p ) +{ + Esop_MmFixedStop ( p->pMemMan1, 0 ); + Esop_MmFixedStop ( p->pMemMan2, 0 ); + Esop_MmFixedStop ( p->pMemMan4, 0 ); + Esop_MmFixedStop ( p->pMemMan8, 0 ); + free( p->ppStore ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/esop/esopMem.c b/src/temp/esop/esopMem.c new file mode 100644 index 00000000..9d8e7405 --- /dev/null +++ b/src/temp/esop/esopMem.c @@ -0,0 +1,274 @@ +/**CFile**************************************************************** + + FileName [esopMem.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Memory managers.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: esopMem.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "esop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Esop_MmFixed_t_ +{ + // information about individual entries + int nEntrySize; // the size of one entry + int nEntriesAlloc; // the total number of entries allocated + int nEntriesUsed; // the number of entries in use + int nEntriesMax; // the max number of entries in use + char * pEntriesFree; // the linked list of free entries + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +struct Esop_MmFlex_t_ +{ + // information about individual entries + int nEntriesUsed; // the number of entries allocated + char * pCurrent; // the current pointer to free memory + char * pEnd; // the first entry outside the free memory + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +struct Esop_MmStep_t_ +{ + int nMems; // the number of fixed memory managers employed + Esop_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc + int nMapSize; // the size of the memory array + Esop_MmFixed_t ** pMap; // maps the number of bytes into its memory manager +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates memory pieces of fixed size.] + + Description [The size of the chunk is computed as the minimum of + 1024 entries and 64K. Can only work with entry size at least 4 byte long.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Esop_MmFixed_t * Esop_MmFixedStart( int nEntrySize ) +{ + Esop_MmFixed_t * p; + + p = ALLOC( Esop_MmFixed_t, 1 ); + memset( p, 0, sizeof(Esop_MmFixed_t) ); + + p->nEntrySize = nEntrySize; + p->nEntriesAlloc = 0; + p->nEntriesUsed = 0; + p->pEntriesFree = NULL; + + if ( nEntrySize * (1 << 10) < (1<<16) ) + p->nChunkSize = (1 << 10); + else + p->nChunkSize = (1<<16) / nEntrySize; + if ( p->nChunkSize < 8 ) + p->nChunkSize = 8; + + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); + + p->nMemoryUsed = 0; + p->nMemoryAlloc = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_MmFixedStop( Esop_MmFixed_t * p, int fVerbose ) +{ + int i; + if ( p == NULL ) + return; + if ( fVerbose ) + { + printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", + p->nEntrySize, p->nChunkSize, p->nChunks ); + printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", + p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); + } + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Esop_MmFixedEntryFetch( Esop_MmFixed_t * p ) +{ + char * pTemp; + int i; + + // check if there are still free entries + if ( p->nEntriesUsed == p->nEntriesAlloc ) + { // need to allocate more entries + assert( p->pEntriesFree == NULL ); + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; + // transform these entries into a linked list + pTemp = p->pEntriesFree; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // add the chunk to the chunk storage + p->pChunks[ p->nChunks++ ] = p->pEntriesFree; + // add to the number of entries allocated + p->nEntriesAlloc += p->nChunkSize; + } + // incrememt the counter of used entries + p->nEntriesUsed++; + if ( p->nEntriesMax < p->nEntriesUsed ) + p->nEntriesMax = p->nEntriesUsed; + // return the first entry in the free entry list + pTemp = p->pEntriesFree; + p->pEntriesFree = *((char **)pTemp); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_MmFixedEntryRecycle( Esop_MmFixed_t * p, char * pEntry ) +{ + // decrement the counter of used entries + p->nEntriesUsed--; + // add the entry to the linked list of free entries + *((char **)pEntry) = p->pEntriesFree; + p->pEntriesFree = pEntry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [Relocates all the memory except the first chunk.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_MmFixedRestart( Esop_MmFixed_t * p ) +{ + int i; + char * pTemp; + + // deallocate all chunks except the first one + for ( i = 1; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + p->nChunks = 1; + // transform these entries into a linked list + pTemp = p->pChunks[0]; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // set the free entry list + p->pEntriesFree = p->pChunks[0]; + // set the correct statistics + p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; + p->nMemoryUsed = 0; + p->nEntriesAlloc = p->nChunkSize; + p->nEntriesUsed = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Esop_MmFixedReadMemUsage( Esop_MmFixed_t * p ) +{ + return p->nMemoryAlloc; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/temp/esop/esopMin.c b/src/temp/esop/esopMin.c new file mode 100644 index 00000000..7a460f8e --- /dev/null +++ b/src/temp/esop/esopMin.c @@ -0,0 +1,299 @@ +/**CFile**************************************************************** + + FileName [esopMin.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [ESOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: esopMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "esop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Esop_EsopRewrite( Esop_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [ESOP minimization procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_EsopMinimize( Esop_Man_t * p ) +{ + int nCubesInit, nCubesOld, nIter; + if ( p->nCubes < 3 ) + return; + nIter = 0; + nCubesInit = p->nCubes; + do { + nCubesOld = p->nCubes; + Esop_EsopRewrite( p ); + nIter++; + } + while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); + +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of rewriting using distance 2 cubes.] + + Description [The weakness of this procedure is that it tries each cube + with only one distance-2 cube. If this pair does not lead to improvement + the cube is inserted into the cover anyhow, and we try another pair. + A possible improvement would be to try this cube with all distance-2 + cubes, until an improvement is found, or until all such cubes are tried.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_EsopRewrite( Esop_Man_t * p ) +{ + Esop_Cube_t * pCube, ** ppPrev; + Esop_Cube_t * pThis, ** ppPrevT; + int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld; + int nPairs = 0; + + // insert the bubble before the first cube + p->pBubble->pNext = p->ppStore[0]; + p->ppStore[0] = p->pBubble; + p->pBubble->nLits = 0; + + // go through the cubes + while ( 1 ) + { + // get the index of the bubble + Index = p->pBubble->nLits; + + // find the bubble + Esop_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) + if ( pCube == p->pBubble ) + break; + assert( pCube == p->pBubble ); + + // remove the bubble, get the next cube after the bubble + *ppPrev = p->pBubble->pNext; + pCube = p->pBubble->pNext; + if ( pCube == NULL ) + for ( Index++; Index <= p->nVars; Index++ ) + if ( p->ppStore[Index] ) + { + ppPrev = &(p->ppStore[Index]); + pCube = p->ppStore[Index]; + break; + } + // stop if there is no more cubes + if ( pCube == NULL ) + break; + + // find the first dist2 cube + Esop_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) + if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars ) + Esop_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) + if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars - 1 ) + Esop_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT ) + if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + // continue if there is no dist2 cube + if ( pThis == NULL ) + { + // insert the bubble after the cube + p->pBubble->pNext = pCube->pNext; + pCube->pNext = p->pBubble; + p->pBubble->nLits = pCube->nLits; + continue; + } + nPairs++; + + // remove the cubes, insert the bubble instead of pCube + *ppPrevT = pThis->pNext; + *ppPrev = p->pBubble; + p->pBubble->pNext = pCube->pNext; + p->pBubble->nLits = pCube->nLits; + p->nCubes -= 2; + + // Exorlink-2: + // A{v00} B{v01} + A{v10} B{v11} = + // A{v00+v10} B{v01} + A{v10} B{v01+v11} = + // A{v00} B{v01+v11} + A{v00+v10} B{v11} + + // save the dist2 parameters + v00 = Esop_CubeGetVar( pCube, Var0 ); + v01 = Esop_CubeGetVar( pCube, Var1 ); + v10 = Esop_CubeGetVar( pThis, Var0 ); + v11 = Esop_CubeGetVar( pThis, Var1 ); +//printf( "\n" ); +//Esop_CubeWrite( stdout, pCube ); +//Esop_CubeWrite( stdout, pThis ); + + // derive the first pair of resulting cubes + Esop_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= (v00 != 3); + pCube->nLits += ((v00 ^ v10) != 3); + Esop_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= (v11 != 3); + pThis->nLits += ((v01 ^ v11) != 3); + + // add the cubes + nCubesOld = p->nCubes; + Esop_EsopAddCube( p, pCube ); + Esop_EsopAddCube( p, pThis ); + // check if the cubes were absorbed + if ( p->nCubes < nCubesOld + 2 ) + continue; + + // pull out both cubes + assert( pThis == p->ppStore[pThis->nLits] ); + p->ppStore[pThis->nLits] = pThis->pNext; + assert( pCube == p->ppStore[pCube->nLits] ); + p->ppStore[pCube->nLits] = pCube->pNext; + p->nCubes -= 2; + + // derive the second pair of resulting cubes + Esop_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= ((v00 ^ v10) != 3); + pCube->nLits += (v00 != 3); + Esop_CubeXorVar( pCube, Var1, v11 ); + pCube->nLits -= (v01 != 3); + pCube->nLits += ((v01 ^ v11) != 3); + + Esop_CubeXorVar( pThis, Var0, v00 ); + pThis->nLits -= (v10 != 3); + pThis->nLits += ((v00 ^ v10) != 3); + Esop_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= ((v01 ^ v11) != 3); + pThis->nLits += (v11 != 3); + + // add them anyhow + Esop_EsopAddCube( p, pCube ); + Esop_EsopAddCube( p, pThis ); + } +// printf( "Pairs = %d ", nPairs ); +} + +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [Returns 0 if the cube is added or removed. Returns 1 + if the cube is glued with some other cube and has to be added again. + Do not forget to clean the storage!] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Esop_EsopAddCubeInt( Esop_Man_t * p, Esop_Cube_t * pCube ) +{ + Esop_Cube_t * pThis, ** ppPrev; + // try to find the identical cube + Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Esop_CubesAreEqual( pCube, pThis ) ) + { + *ppPrev = pThis->pNext; + Esop_CubeRecycle( p, pCube ); + Esop_CubeRecycle( p, pThis ); + p->nCubes--; + return 0; + } + } + // find a distance-1 cube if it exists + if ( pCube->nLits < pCube->nVars ) + Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev ) + { + if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Esop_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits++; + Esop_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Esop_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits--; + Esop_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + if ( pCube->nLits > 0 ) + Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev ) + { + if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Esop_CubesTransform( pCube, pThis, p->pTemp ); + Esop_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + // add the cube + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + return 0; +} + +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube ) +{ + assert( pCube != p->pBubble ); + assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) ); + while ( Esop_EsopAddCubeInt( p, pCube ) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/esop/esopUtil.c b/src/temp/esop/esopUtil.c new file mode 100644 index 00000000..dec6eae2 --- /dev/null +++ b/src/temp/esop/esopUtil.c @@ -0,0 +1,277 @@ +/**CFile**************************************************************** + + FileName [esopUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: esopUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "esop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube ) +{ + int i; + assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) ); + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Esop_CubeHasBit(pCube, i*2) ) + { + if ( Esop_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "-" ); + else + fprintf( pFile, "0" ); + } + else + { + if ( Esop_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "1" ); + else + fprintf( pFile, "?" ); + } + fprintf( pFile, " 1\n" ); +// fprintf( pFile, " %d\n", pCube->nLits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube; + Esop_CoverForEachCube( pCover, pCube ) + Esop_CubeWrite( pFile, pCube ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p ) +{ + Esop_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + { + Esop_CoverForEachCube( p->ppStore[i], pCube ) + { + printf( "%2d : ", i ); + if ( pCube == p->pBubble ) + { + printf( "Bubble\n" ); + continue; + } + Esop_CubeWrite( pFile, pCube ); + } + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop ) +{ + char Buffer[1000]; + Esop_Cube_t * pCube; + FILE * pFile; + int i; + sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" ); + for ( i = strlen(Buffer) - 1; i >= 0; i-- ) + if ( Buffer[i] == '<' || Buffer[i] == '>' ) + Buffer[i] = '_'; + pFile = fopen( Buffer, "w" ); + fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() ); + fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); + fprintf( pFile, ".o %d\n", 1 ); + fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) ); + if ( fEsop ) fprintf( pFile, ".type esop\n" ); + Esop_CoverForEachCube( pCover, pCube ) + Esop_CubeWrite( pFile, pCube ); + fprintf( pFile, ".e\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CoverCheck( Esop_Man_t * p ) +{ + Esop_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + Esop_CoverForEachCube( p->ppStore[i], pCube ) + assert( i == (int)pCube->nLits ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Esop_CubeCheck( Esop_Cube_t * pCube ) +{ + int i; + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Esop_CubeGetVar( pCube, i ) == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Converts the cover from the sorted structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize ) +{ + Esop_Cube_t * pCov = NULL, ** ppTail = &pCov; + Esop_Cube_t * pCube, * pCube2; + int i; + for ( i = 0; i <= nSuppSize; i++ ) + { + Esop_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 ) + { + assert( i == (int)pCube->nLits ); + *ppTail = pCube; + ppTail = &pCube->pNext; + assert( pCube->uData[0] ); // not a bubble + } + } + *ppTail = NULL; + return pCov; +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube, * pCube2; + Esop_ManClean( p, p->nVars ); + Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover ) +{ + Esop_Cube_t * pCube; + int i, Counter; + if ( pCover == NULL ) + return 0; + // clean the cube + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] = ~((unsigned)0); + // add the bit data + Esop_CoverForEachCube( pCover, pCube ) + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] &= pCube->uData[i]; + // count the vars + Counter = 0; + for ( i = 0; i < (int)pCover->nVars; i++ ) + Counter += ( Esop_CubeGetVar(p->pTemp, i) != 3 ); + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/esop/module.make b/src/temp/esop/module.make new file mode 100644 index 00000000..cab5e737 --- /dev/null +++ b/src/temp/esop/module.make @@ -0,0 +1,4 @@ +SRC += src/temp/esop/esopMan.c \ + src/temp/esop/esopMem.c \ + src/temp/esop/esopMin.c \ + src/temp/esop/esopUtil.c diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h new file mode 100644 index 00000000..55ada384 --- /dev/null +++ b/src/temp/ivy/ivy.h @@ -0,0 +1,450 @@ +/**CFile**************************************************************** + + FileName [ivy.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __IVY_H__ +#define __IVY_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Man_t_ Ivy_Man_t; +typedef struct Ivy_Obj_t_ Ivy_Obj_t; + +// object types +typedef enum { + IVY_NONE, // 0: unused node + IVY_PI, // 1: primary input (and constant 1 node) + IVY_PO, // 2: primary output + IVY_ASSERT, // 3: assertion + IVY_LATCH, // 4: sequential element + IVY_AND, // 5: internal AND node + IVY_EXOR, // 6: internal EXOR node + IVY_BUF, // 7: internal buffer (temporary) + IVY_ANDM, // 8: multi-input AND (logic network only) + IVY_EXORM, // 9: multi-input EXOR (logic network only) + IVY_LUT // 10: multi-input LUT (logic network only) +} Ivy_Type_t; + +// latch initial values +typedef enum { + IVY_INIT_NONE, // 0: not a latch + IVY_INIT_0, // 1: zero + IVY_INIT_1, // 2: one + IVY_INIT_DC // 3: don't-care +} Ivy_Init_t; + +// the AIG node +struct Ivy_Obj_t_ // 6 words +{ + int Id; // integer ID + int TravId; // traversal ID + int Fanin0; // fanin ID + int Fanin1; // fanin ID + int nRefs; // reference counter + unsigned Type : 4; // object type + unsigned fPhase : 1; // value under 000...0 pattern + unsigned fMarkA : 1; // multipurpose mask + unsigned fMarkB : 1; // multipurpose mask + unsigned fExFan : 1; // set to 1 if last fanout added is EXOR + unsigned fComp0 : 1; // complemented attribute + unsigned fComp1 : 1; // complemented attribute + unsigned Init : 2; // latch initial value + unsigned LevelR : 8; // reverse logic level + unsigned Level : 12; // logic level +}; + +// the AIG manager +struct Ivy_Man_t_ +{ + // AIG nodes + int nObjs[12]; // the number of objects by type + int nCreated; // the number of created objects + int nDeleted; // the number of deleted objects + int ObjIdNext; // the next free obj ID to assign + int nObjsAlloc; // the allocated number of nodes + Ivy_Obj_t * pObjs; // the array of all nodes + Vec_Int_t * vPis; // the array of PIs + Vec_Int_t * vPos; // the array of POs + // stuctural hash table + int * pTable; // structural hash table + int nTableSize; // structural hash table size + // various data members + int fExtended; // set to 1 in extended mode + int nTravIds; // the traversal ID + int nLevelMax; // the maximum level + void * pData; // the temporary data + // truth table of the 8-LUTs + unsigned * pMemory; // memory for truth tables + Vec_Int_t * vTruths; // offset for truth table of each node + // storage for the undo operation + Vec_Int_t * vFree; // storage for all deleted entries + Ivy_Obj_t * pUndos; // description of recently deleted nodes + int nUndos; // the number of recently deleted nodes + int nUndosAlloc; // the number of allocated cells + int fRecording; // shows that recording goes on +}; + + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define IVY_SANDBOX_SIZE 1 + +#define IVY_MIN(a,b) (((a) < (b))? (a) : (b)) +#define IVY_MAX(a,b) (((a) > (b))? (a) : (b)) + +static inline int Ivy_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Ivy_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } + +static inline int Ivy_FanCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } +static inline int Ivy_FanId( int Fan ) { return Fan >> 1; } +static inline int Ivy_FanCompl( int Fan ) { return Fan & 1; } + +static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; } +static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; } +static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; } + +static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); } +static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); } +static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); } +static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned)p) & 01); } + +static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pObjs); } +static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pObjs; } +static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return p->pObjs - IVY_SANDBOX_SIZE; } +static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPis,i); } +static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPos,i); } +static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return p->pObjs + i; } + +static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; } +static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; } +static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; } +static inline int Ivy_ManLatchNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LATCH]; } +static inline int Ivy_ManAndNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]; } +static inline int Ivy_ManExorNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXOR]; } +static inline int Ivy_ManBufNum( Ivy_Man_t * p ) { return p->nObjs[IVY_BUF]; } +static inline int Ivy_ManAndMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ANDM]; } +static inline int Ivy_ManExorMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXORM]; } +static inline int Ivy_ManLutNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LUT]; } +static inline int Ivy_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; } +static inline int Ivy_ManObjIdNext( Ivy_Man_t * p ) { return p->ObjIdNext; } +static inline int Ivy_ManObjAllocNum( Ivy_Man_t * p ) { return p->nObjsAlloc; } +static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->fExtended? p->nObjs[IVY_ANDM]+p->nObjs[IVY_EXORM]+p->nObjs[IVY_LUT] : p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]; } +static inline int Ivy_ManHashObjNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH]; } +static inline int Ivy_ManGetCost( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; } + +static inline Ivy_Type_t Ivy_ObjType( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type; } +static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Init; } +static inline int Ivy_ObjIsConst1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id == 0; } +static inline int Ivy_ObjIsGhost( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id < 0; } +static inline int Ivy_ObjIsNone( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_NONE; } +static inline int Ivy_ObjIsPi( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI; } +static inline int Ivy_ObjIsPo( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO; } +static inline int Ivy_ObjIsCi( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; } +static inline int Ivy_ObjIsCo( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; } +static inline int Ivy_ObjIsAssert( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ASSERT; } +static inline int Ivy_ObjIsLatch( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LATCH; } +static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND; } +static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR; } +static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF; } +static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; } +static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } +static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } +static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } + +static inline int Ivy_ObjIsAndMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM; } +static inline int Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM; } +static inline int Ivy_ObjIsLut( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LUT; } +static inline int Ivy_ObjIsNodeExt( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type >= IVY_ANDM; } + +static inline int Ivy_ObjIsMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA; } +static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1; } +static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0; } + +static inline Ivy_Man_t * Ivy_ObjMan( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return *((Ivy_Man_t **)(pObj - pObj->Id - IVY_SANDBOX_SIZE - 1)); } +static inline Ivy_Obj_t * Ivy_ObjConst0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Not(pObj - pObj->Id); } +static inline Ivy_Obj_t * Ivy_ObjConst1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id; } +static inline Ivy_Obj_t * Ivy_ObjGhost( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id - IVY_SANDBOX_SIZE; } +static inline Ivy_Obj_t * Ivy_ObjObj( Ivy_Obj_t * pObj, int n ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + n; } +static inline Ivy_Obj_t * Ivy_ObjNext( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + pObj->TravId; } + +static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId; } +static inline void Ivy_ObjSetTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds; } +static inline void Ivy_ObjSetTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds - 1; } +static inline int Ivy_ObjIsTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds); } +static inline int Ivy_ObjIsTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds - 1); } + +static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id; } +static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase; } +static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fExFan; } +static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs; } +static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++; } +static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--; } +static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin0; } +static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin1; } +static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp0; } +static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp1; } +static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin0); } +static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin1); } +static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin0(pObj), Ivy_ObjFaninC0(pObj) ); } +static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) ); } +static inline int Ivy_ObjLevelR( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR; } +static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Level; } +static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } +static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) { + int IdSaved = pObj->Id; + if ( IdSaved == 54 ) + { + int x = 0; + } + memset( pObj, 0, sizeof(Ivy_Obj_t) ); + pObj->Id = IdSaved; +} +static inline void Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData ) { int IdSaved = pBase->Id; memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); pBase->Id = IdSaved; } +static inline int Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) +{ + if ( Ivy_ObjFaninId0(pObj) == Ivy_ObjId(pFanin) ) return 0; + if ( Ivy_ObjFaninId1(pObj) == Ivy_ObjId(pFanin) ) return 1; + assert(0); return -1; +} +static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + if ( Ivy_ObjFaninId0(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC0(pObj); + if ( Ivy_ObjFaninId1(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC1(pObj); + assert(0); return -1; +} + +// create the ghost of the new node +static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) +{ + Ivy_Obj_t * pGhost; + int Temp; + pGhost = Ivy_ObjGhost(Ivy_Regular(p0)); + pGhost->Type = Type; + pGhost->Init = Init; + pGhost->fComp0 = Ivy_IsComplement(p0); + pGhost->fComp1 = Ivy_IsComplement(p1); + pGhost->Fanin0 = Ivy_ObjId(Ivy_Regular(p0)); + pGhost->Fanin1 = Ivy_ObjId(Ivy_Regular(p1)); + if ( pGhost->Fanin0 < pGhost->Fanin1 ) + { + Temp = pGhost->Fanin0, pGhost->Fanin0 = pGhost->Fanin1, pGhost->Fanin1 = Temp; + Temp = pGhost->fComp0, pGhost->fComp0 = pGhost->fComp1, pGhost->fComp1 = Temp; + } + assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); + return pGhost; +} + +// create the ghost of the new node +static inline Ivy_Obj_t * Ivy_ObjCreateGhost2( Ivy_Man_t * p, Ivy_Obj_t * pObjDead ) +{ + Ivy_Obj_t * pGhost; + pGhost = Ivy_ManGhost(p); + pGhost->Type = pObjDead->Type; + pGhost->Init = pObjDead->Init; + pGhost->fComp0 = pObjDead->fComp0; + pGhost->fComp1 = pObjDead->fComp1; + pGhost->Fanin0 = pObjDead->Fanin0; + pGhost->Fanin1 = pObjDead->Fanin1; + assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); + return pGhost; +} + +// get the complemented initial state +static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl ) +{ + assert( Init != IVY_INIT_NONE ); + if ( fCompl == 0 ) + return Init; + if ( Init == IVY_INIT_0 ) + return IVY_INIT_1; + if ( Init == IVY_INIT_1 ) + return IVY_INIT_0; + return IVY_INIT_DC; +} + +// get the initial state after forward retiming over AND gate +static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB ) +{ + assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); + if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 ) + return IVY_INIT_0; + if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) + return IVY_INIT_DC; + return IVY_INIT_1; +} + +// get the initial state after forward retiming over EXOR gate +static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB ) +{ + assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); + if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) + return IVY_INIT_DC; + if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 ) + return IVY_INIT_1; + if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 ) + return IVY_INIT_1; + return IVY_INIT_0; +} + +// extended fanins +static inline Vec_Int_t * Ivy_ObjGetFanins( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return (Vec_Int_t *)*(((int*)pObj)+2); } +static inline void Ivy_ObjSetFanins( Ivy_Obj_t * pObj, Vec_Int_t * vFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); assert(Ivy_ObjGetFanins(pObj)==NULL); *(Vec_Int_t **)(((int*)pObj)+2) = vFanins; } +static inline void Ivy_ObjStartFanins( Ivy_Obj_t * pObj, int nFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); Ivy_ObjSetFanins( pObj, Vec_IntAlloc(nFanins) ); } +static inline void Ivy_ObjAddFanin( Ivy_Obj_t * pObj, int Fanin ) { assert(Ivy_ObjMan(pObj)->fExtended); Vec_IntPush( Ivy_ObjGetFanins(pObj), Fanin ); } +static inline int Ivy_ObjReadFanin( Ivy_Obj_t * pObj, int i ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntEntry( Ivy_ObjGetFanins(pObj), i ); } +static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntSize( Ivy_ObjGetFanins(pObj) ); } + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +// iterator over all objects, including those currently not used +#define Ivy_ManForEachObj( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) +// iterator over the primary inputs +#define Ivy_ManForEachPi( p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ ) +// iterator over the primary outputs +#define Ivy_ManForEachPo( p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(p->vPos) && ((pObj) = Ivy_ManPo(p, i)); i++ ) +// iterator over the combinational inputs +#define Ivy_ManForEachCi( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsCi(pObj) ) {} else +// iterator over the combinational outputs +#define Ivy_ManForEachCo( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsCo(pObj) ) {} else +// iterator over logic nodes (AND and EXOR gates) +#define Ivy_ManForEachNode( p, pObj, i ) \ + for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsNode(pObj) ) {} else +// iterator over logic latches +#define Ivy_ManForEachLatch( p, pObj, i ) \ + for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsLatch(pObj) ) {} else +// iterator over the nodes whose IDs are stored in the array +#define Ivy_ManForEachNodeVec( p, vIds, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== ivyCanon.c ========================================================*/ +extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ); +/*=== ivyCheck.c ========================================================*/ +extern int Ivy_ManCheck( Ivy_Man_t * p ); +/*=== ivyCut.c ==========================================================*/ +extern void Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); +/*=== ivyBalance.c ======================================================*/ +extern int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); +/*=== ivyDfs.c ==========================================================*/ +extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ); +extern Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ); +/*=== ivyDsd.c ==========================================================*/ +extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ); +extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ); +extern unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ); +extern void Ivy_TruthDsdComputePrint( unsigned uTruth ); +extern Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ); +/*=== ivyMan.c ==========================================================*/ +extern Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ); +extern void Ivy_ManStop( Ivy_Man_t * p ); +extern void Ivy_ManGrow( Ivy_Man_t * p ); +extern int Ivy_ManCleanup( Ivy_Man_t * p ); +extern void Ivy_ManPrintStats( Ivy_Man_t * p ); +/*=== ivyMulti.c ==========================================================*/ +extern Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +/*=== ivyObj.c ==========================================================*/ +extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ); +extern Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ); +extern void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ); +extern void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ); +extern void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ); +/*=== ivyOper.c =========================================================*/ +extern Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); +extern Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); +extern Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ); +/*=== ivyRewrite.c =========================================================*/ +extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); +/*=== ivyTable.c ========================================================*/ +extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ); +extern void Ivy_TableInsert( Ivy_Obj_t * pObj ); +extern void Ivy_TableDelete( Ivy_Obj_t * pObj ); +extern void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ); +extern int Ivy_TableCountEntries( Ivy_Man_t * p ); +extern void Ivy_TableResize( Ivy_Man_t * p ); +/*=== ivyUndo.c =========================================================*/ +extern void Ivy_ManUndoStart( Ivy_Man_t * p ); +extern void Ivy_ManUndoStop( Ivy_Man_t * p ); +extern void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ); +/*=== ivyUtil.c =========================================================*/ +extern void Ivy_ManIncrementTravId( Ivy_Man_t * p ); +extern void Ivy_ManCleanTravId( Ivy_Man_t * p ); +extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj ); +extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE ); +extern unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); +extern Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ); +extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c new file mode 100644 index 00000000..bbe69dd9 --- /dev/null +++ b/src/temp/ivy/ivyBalance.c @@ -0,0 +1,421 @@ +/**CFile**************************************************************** + + FileName [ivyBalance.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Algebraic AIG balancing.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ); + +// this procedure returns 1 if the node cannot be expanded +static inline int Ivy_NodeStopFanin( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + return Ivy_ObjFanin0(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) > 1 || Ivy_ObjFaninC0(pNode); + else + return Ivy_ObjFanin1(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) > 1 || Ivy_ObjFaninC1(pNode); +} + +// this procedure returns 1 if the node cannot be recursively dereferenced +static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + return Ivy_ObjFanin0(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) == 0 && !Ivy_ObjFaninC0(pNode); + else + return Ivy_ObjFanin1(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) == 0 && !Ivy_ObjFaninC1(pNode); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs algebraic balancing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) +{ + Vec_Int_t * vNodes; + Vec_Ptr_t * vFront, * vSpots; + Ivy_Obj_t * pNode; + int i; + vSpots = Vec_PtrAlloc( 50 ); + vFront = Vec_PtrAlloc( 50 ); + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + { + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + // skip node if it became a buffer + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // skip nodes with one fanout if type of the node is the same as type of the fanout + // such nodes will be processed when the fanouts are processed + if ( Ivy_ObjRefs(pNode) == 1 && Ivy_ObjIsExor(pNode) == Ivy_ObjExorFanout(pNode) ) + continue; + assert( Ivy_ObjRefs(pNode) > 0 ); + // do not balance the node if both if its fanins have more than one fanout + if ( Ivy_NodeStopFanin(pNode, 0) && Ivy_NodeStopFanin(pNode, 1) ) + continue; + // try balancing this node + Ivy_NodeBalance( pNode, fUpdateLevel, vFront, vSpots ); + } + Vec_IntFree( vNodes ); + Vec_PtrFree( vSpots ); + Vec_PtrFree( vFront ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Dereferences MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFan; + // deref the first fanin + pFan = Ivy_ObjFanin0(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_NodeBalanceDerefFanin(pNode, 0) ) + Ivy_NodeBalanceDeref_rec( pFan ); + // deref the second fanin + pFan = Ivy_ObjFanin1(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_NodeBalanceDerefFanin(pNode, 1) ) + Ivy_NodeBalanceDeref_rec( pFan ); +} + +/**Function************************************************************* + + Synopsis [Removes nodes inside supergate and determines frontier.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront ) +{ + Ivy_Obj_t * pFanin; + // skip visited nodes + if ( Vec_PtrFind(vSpots, pNode) >= 0 ) + return; + // collect node + Vec_PtrPush( vSpots, pNode ); + // first fanin + pFanin = Ivy_ObjFanin0(pNode); + if ( Ivy_ObjRefs(pFanin) == 0 ) + Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); + else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild0(pNode)) >= 0 ) + Vec_PtrRemove( vFront, Ivy_ObjChild0(pNode) ); + else + Vec_PtrPushUnique( vFront, Ivy_ObjChild0(pNode) ); + // second fanin + pFanin = Ivy_ObjFanin1(pNode); + if ( Ivy_ObjRefs(pFanin) == 0 ) + Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); + else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild1(pNode)) >= 0 ) + Vec_PtrRemove( vFront, Ivy_ObjChild1(pNode) ); + else + Vec_PtrPushUnique( vFront, Ivy_ObjChild1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two nodes by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) +{ + int Level1 = Ivy_ObjLevel( *pp1 ); + int Level2 = Ivy_ObjLevel( *pp2 ); + if ( Level1 > Level2 ) + return -1; + if ( Level1 < Level2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Removes nodes inside supergate and determines frontier.] + + Description [Return 1 if the output needs to be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) +{ + Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); + Ivy_Obj_t * pObj, * pNext; + int i, k, Counter = 0; + // dereference the cone + Ivy_NodeBalanceDeref_rec( pNode ); + // collect the frontier and the internal nodes + Vec_PtrClear( vFront ); + Vec_PtrClear( vSpots ); + Ivy_NodeBalanceCollect_rec( pNode, vSpots, vFront ); + // remove all the nodes + Vec_PtrForEachEntry( vSpots, pObj, i ) + { + // skip the first entry (the node itself) + if ( i == 0 ) continue; + // collect the free entries + Vec_IntPush( pMan->vFree, pObj->Id ); + Ivy_ObjDelete( pObj, 1 ); + } + // sort nodes by level in decreasing order + qsort( (void *)Vec_PtrArray(vFront), Vec_PtrSize(vFront), sizeof(Ivy_Obj_t *), + (int (*)(const void *, const void *))Ivy_BalanceCompareByLevel ); + // check if there are nodes and their complements + Counter = 0; + Vec_PtrForEachEntry( vFront, pObj, i ) + { + if ( i == Vec_PtrSize(vFront) - 1 ) + break; + pNext = Vec_PtrEntry( vFront, i+1 ); + if ( Ivy_Regular(pObj) == Ivy_Regular(pNext) ) + { + assert( pObj == Ivy_Not(pNext) ); + Vec_PtrWriteEntry( vFront, i, NULL ); + Vec_PtrWriteEntry( vFront, i+1, NULL ); + i++; + Counter++; + } + } + // if there are no complemented pairs, go ahead and balance + if ( Counter == 0 ) + return 0; + // if there are complemented pairs and this is AND, create const 0 + if ( Counter > 0 && Ivy_ObjIsAnd(pNode) ) + { + Vec_PtrClear( vFront ); + Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); + return 0; + } + assert( Counter > 0 && Ivy_ObjIsExor(pNode) ); + // remove the pairs + k = 0; + Vec_PtrForEachEntry( vFront, pObj, i ) + if ( pObj ) + Vec_PtrWriteEntry( vFront, k++, pObj ); + Vec_PtrShrink( vFront, k ); + // add constant zero node if nothing is left + if ( Vec_PtrSize(vFront) == 0 ) + Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); + // return 1 if the number of pairs is odd (need to complement the output) + return Counter & 1; +} + +/**Function************************************************************* + + Synopsis [Finds the left bound on the next candidate to be paired.] + + Description [The nodes in the array are in the decreasing order of levels. + The last node in the array has the smallest level. By default it would be paired + with the next node on the left. However, it may be possible to pair it with some + other node on the left, in such a way that the new node is shared. This procedure + finds the index of the left-most node, which can be paired with the last node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) +{ + Ivy_Obj_t * pNodeRight, * pNodeLeft; + int Current; + // if two or less nodes, pair with the first + if ( Vec_PtrSize(vSuper) < 3 ) + return 0; + // set the pointer to the one before the last + Current = Vec_PtrSize(vSuper) - 2; + pNodeRight = Vec_PtrEntry( vSuper, Current ); + // go through the nodes to the left of this one + for ( Current--; Current >= 0; Current-- ) + { + // get the next node on the left + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + // if the level of this node is different, quit the loop + if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->Level ) + break; + } + Current++; + // get the node, for which the equality holds + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + assert( Ivy_Regular(pNodeLeft)->Level == Ivy_Regular(pNodeRight)->Level ); + return Current; +} + +/**Function************************************************************* + + Synopsis [Moves closer to the end the node that is best for sharing.] + + Description [If there is no node with sharing, randomly chooses one of + the legal nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +{ + Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost; + int RightBound, i; + // get the right bound + RightBound = Vec_PtrSize(vSuper) - 2; + assert( LeftBound <= RightBound ); + if ( LeftBound == RightBound ) + return; + // get the two last nodes + pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 ); + pNode2 = Vec_PtrEntry( vSuper, RightBound ); + // find the first node that can be shared + for ( i = RightBound; i >= LeftBound; i-- ) + { + pNode3 = Vec_PtrEntry( vSuper, i ); + pGhost = Ivy_ObjCreateGhost( pNode1, pNode3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); + if ( Ivy_TableLookup( pGhost ) ) + { + if ( pNode3 == pNode2 ) + return; + Vec_PtrWriteEntry( vSuper, i, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + return; + } + } +/* + // we did not find the node to share, randomize choice + { + int Choice = rand() % (RightBound - LeftBound + 1); + pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); + if ( pNode3 == pNode2 ) + return; + Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + } +*/ +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode1, * pNode2; + int i; + if ( Vec_PtrPushUnique(vFront, pNode) ) + return; + // find the p of the node + for ( i = vFront->nSize-1; i > 0; i-- ) + { + pNode1 = vFront->pArray[i ]; + pNode2 = vFront->pArray[i-1]; + if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + break; + vFront->pArray[i ] = pNode2; + vFront->pArray[i-1] = pNode1; + } +} + +/**Function************************************************************* + + Synopsis [Balances one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) +{ + Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); + Ivy_Obj_t * pFan0, * pFan1, * pNodeNew; + int fCompl, LeftBound; + // remove internal nodes and derive the frontier + fCompl = Ivy_NodeBalancePrepare( pNode, vFront, vSpots ); + assert( Vec_PtrSize(vFront) > 0 ); + // balance the nodes + while ( Vec_PtrSize(vFront) > 1 ) + { + // find the left bound on the node to be paired + LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vFront ); + // find the node that can be shared (if no such node, randomize choice) + Ivy_NodeBalancePermute( pMan, vFront, LeftBound, Ivy_ObjIsExor(pNode) ); + // pull out the last two nodes + pFan0 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan0)) ); + pFan1 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan1)) ); + // create the new node + pNodeNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pFan0, pFan1, Ivy_ObjType(pNode), IVY_INIT_NONE) ); + // add the new node to the frontier + Ivy_NodeBalancePushUniqueOrderByLevel( vFront, pNodeNew ); + } + assert( Vec_PtrSize(vFront) == 1 ); + // perform the replacement + Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCanon.c b/src/temp/ivy/ivyCanon.c new file mode 100644 index 00000000..c6f43d15 --- /dev/null +++ b/src/temp/ivy/ivyCanon.c @@ -0,0 +1,147 @@ +/**CFile**************************************************************** + + FileName [ivyCanon.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Finding canonical form of objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCanon.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) +{ + Ivy_Obj_t * pResult, * pLat0, * pLat1; + Ivy_Init_t Init, Init0, Init1; + int fCompl0, fCompl1; + Ivy_Type_t Type; + assert( Ivy_ObjIsNode(pGhost) ); + assert( Ivy_ObjIsAnd(pGhost) || (!Ivy_ObjFaninC0(pGhost) && !Ivy_ObjFaninC1(pGhost)) ); + assert( Ivy_ObjFaninId0(pGhost) != 0 && Ivy_ObjFaninId1(pGhost) != 0 ); + // consider the case when the pair is canonical + if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) ) + { + if ( pResult = Ivy_TableLookup( pGhost ) ) + return pResult; + return Ivy_ObjCreate( pGhost ); + } + /// remember the latches + pLat0 = Ivy_ObjFanin0(pGhost); + pLat1 = Ivy_ObjFanin1(pGhost); + // remember type and compls + Type = Ivy_ObjType(pGhost); + fCompl0 = Ivy_ObjFaninC0(pGhost); + fCompl1 = Ivy_ObjFaninC1(pGhost); + // modify the fanins to be latch fanins + pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0); + pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1); + // call recursively + pResult = Ivy_CanonPair_rec( pGhost ); + // build latch on top of this + Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 ); + Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 ); + Init = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1); + return Ivy_CanonLatch( pResult, Init ); +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +{ + Ivy_Obj_t * pGhost, * pResult; + pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( pGhost ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +{ + Ivy_Obj_t * pGhost, * pResult; + int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1); + pObj0 = Ivy_Regular(pObj0); + pObj1 = Ivy_Regular(pObj1); + pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( pGhost ); + return Ivy_NotCond( pResult, fCompl ); +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) +{ + Ivy_Obj_t * pGhost, * pResult; + int fCompl = Ivy_IsComplement(pObj); + pObj = Ivy_Regular(pObj); + pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) ); + pResult = Ivy_TableLookup( pGhost ); + if ( pResult == NULL ) + pResult = Ivy_ObjCreate( pGhost ); + return Ivy_NotCond( pResult, fCompl ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c new file mode 100644 index 00000000..c39eac12 --- /dev/null +++ b/src/temp/ivy/ivyCheck.c @@ -0,0 +1,121 @@ +/**CFile**************************************************************** + + FileName [ivyCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG checking procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks the consistency of the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManCheck( Ivy_Man_t * pMan ) +{ + Ivy_Obj_t * pObj, * pObj2; + int i; + Ivy_ManForEachObj( pMan, pObj, i ) + { + // skip deleted nodes + if ( Ivy_ObjIsNone(pObj) ) + continue; + // consider the constant node and PIs + if ( i == 0 || Ivy_ObjIsPi(pObj) ) + { + if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + if ( Ivy_ObjIsPo(pObj) ) + { + if ( Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + if ( Ivy_ObjIsBuf(pObj) ) + { + continue; + } + if ( Ivy_ObjIsLatch(pObj) ) + { + if ( Ivy_ObjFaninId1(pObj) != 0 ) + { + printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id ); + return 0; + } + if ( Ivy_ObjInit(pObj) == 0 ) + { + printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id ); + return 0; + } + pObj2 = Ivy_TableLookup( pObj ); + if ( pObj2 != pObj ) + printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); + continue; + } + // consider the AND node + if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id ); + return 0; + } + if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); + return 0; + } +// if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) +// printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id ); + pObj2 = Ivy_TableLookup( pObj ); + if ( pObj2 != pObj ) + printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); + } + // count the number of nodes in the table + if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) ) + { + printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + return 0; + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c new file mode 100644 index 00000000..a8fd148b --- /dev/null +++ b/src/temp/ivy/ivyCut.c @@ -0,0 +1,205 @@ +/**CFile**************************************************************** + + FileName [ivyCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Computes reconvergence driven sequential cut.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCut.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Evaluate the cost of removing the node from the set of leaves.] + + Description [Returns the number of new leaves that will be brought in. + Returns large number if the node cannot be removed from the set of leaves.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_NodeGetLeafCostOne( Ivy_Man_t * p, int Leaf, Vec_Int_t * vInside ) +{ + Ivy_Obj_t * pNode; + int nLatches, FaninLeaf, Cost; + // make sure leaf is not a contant node + assert( Leaf > 0 ); + // get the node + pNode = Ivy_ManObj( p, Ivy_LeafId(Leaf) ); + // cannot expand over the PI node + if ( Ivy_ObjIsPi(pNode) || Ivy_ObjIsConst1(pNode) ) + return 999; + // get the number of latches + nLatches = Ivy_LeafLat(Leaf) + Ivy_ObjIsLatch(pNode); + if ( nLatches > 15 ) + return 999; + // get the first fanin + FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches ); + Cost = FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1); + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return Cost; + assert( Ivy_ObjIsNode(pNode) ); + // get the second fanin + FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches ); + Cost += FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1); + return Cost; +} + +/**Function************************************************************* + + Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.] + + Description [This procedure looks at the current leaves and tries to change + one leaf at a time in such a way that the cut grows as little as possible. + In evaluating the fanins, this procedure looks only at their immediate + predecessors (this is why it is called a one-level construction procedure).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqFindCut_int( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSizeLimit ) +{ + Ivy_Obj_t * pNode; + int CostBest, CostCur, Leaf, LeafBest, Next, nLatches, i; + int LeavesBest[10]; + int Counter; + + // add random selection of the best fanin!!! + + // find the best fanin + CostBest = 99; + LeafBest = -1; + Counter = -1; +//printf( "Evaluating fanins of the cut:\n" ); + Vec_IntForEachEntry( vFront, Leaf, i ) + { + CostCur = Ivy_NodeGetLeafCostOne( p, Leaf, vInside ); +//printf( " Fanin %s has cost %d.\n", Ivy_ObjName(pNode), CostCur ); + if ( CostBest > CostCur ) + { + CostBest = CostCur; + LeafBest = Leaf; + LeavesBest[0] = Leaf; + Counter = 1; + } + else if ( CostBest == CostCur ) + LeavesBest[Counter++] = Leaf; + + if ( CostBest <= 1 ) // can be if ( CostBest <= 1 ) + break; + } + if ( CostBest == 99 ) + return 0; +// return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit ); + + assert( CostBest < 3 ); + if ( Vec_IntSize(vFront) - 1 + CostBest > nSizeLimit ) + return 0; +// return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit ); + + assert( Counter > 0 ); +printf( "%d", Counter ); + + LeafBest = LeavesBest[rand() % Counter]; + + // remove the node from the array + assert( LeafBest >= 0 ); + Vec_IntRemove( vFront, LeafBest ); +//printf( "Removing fanin %s.\n", Ivy_ObjName(pNode) ); + + // get the node and its latches + pNode = Ivy_ManObj( p, Ivy_LeafId(LeafBest) ); + nLatches = Ivy_LeafLat(LeafBest) + Ivy_ObjIsLatch(pNode); + assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ); + + // add the left child to the fanins + Next = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches ); + if ( Next && Vec_IntFind(vInside, Next) == -1 ) + { +//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) ); + Vec_IntPush( vFront, Next ); + Vec_IntPush( vInside, Next ); + } + + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return 1; + assert( Ivy_ObjIsNode(pNode) ); + + // add the right child to the fanins + Next = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches ); + if ( Next && Vec_IntFind(vInside, Next) == -1 ) + { +//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) ); + Vec_IntPush( vFront, Next ); + Vec_IntPush( vInside, Next ); + } + assert( Vec_IntSize(vFront) <= nSizeLimit ); + // keep doing this + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes one sequential cut of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ) +{ + assert( !Ivy_IsComplement(pRoot) ); + assert( Ivy_ObjIsNode(pRoot) ); + assert( Ivy_ObjFaninId0(pRoot) ); + assert( Ivy_ObjFaninId1(pRoot) ); + + // start the cut + Vec_IntClear( vFront ); + Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); + Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); + + // start the visited nodes + Vec_IntClear( vInside ); + Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) ); + Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); + Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); + + // compute the cut + while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) ); + assert( Vec_IntSize(vFront) <= nSize ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c new file mode 100644 index 00000000..2db80b00 --- /dev/null +++ b/src/temp/ivy/ivyDfs.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [ivyDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [DFS collection procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) ) + return; + if ( Ivy_ObjIsMarkA(pObj) ) + return; + Ivy_ObjSetMarkA(pObj); + assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) ); + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + if ( !Ivy_ObjIsBuf(pObj) ) + Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj; + int i; + // collect the nodes + vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); + if ( Ivy_ManLatchNum(p) > 0 ) + Ivy_ManForEachCo( p, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + else + Ivy_ManForEachPo( p, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + // unmark the collected nodes + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + Ivy_ObjClearMarkA(pObj); + // make sure network does not have dangling nodes + assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + Vec_Int_t * vFanins; + int i, Fanin; + if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) ) + return; + // mark the node as visited + Ivy_ObjSetMarkA(pObj); + // traverse the fanins + vFanins = Ivy_ObjGetFanins( pObj ); + Vec_IntForEachEntry( vFanins, Fanin, i ) + Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes ); + // add the node + Vec_IntPush( vNodes, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj, * pFanin; + int i; + assert( p->fExtended ); + assert( Ivy_ManLatchNum(p) == 0 ); + // make sure network does not have buffers + vNodes = Vec_IntAlloc( 10 ); + Ivy_ManForEachPo( p, pObj, i ) + { + pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) ); + Ivy_ManDfsExt_rec( pFanin, vNodes ); + } + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + Ivy_ObjClearMarkA(pObj); + // make sure network does not have dangling nodes + // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes +// assert( p->nNodes == Vec_PtrSize(vNodes) ); + return vNodes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyDsd.c b/src/temp/ivy/ivyDsd.c new file mode 100644 index 00000000..5dfdd30f --- /dev/null +++ b/src/temp/ivy/ivyDsd.c @@ -0,0 +1,819 @@ +/**CFile**************************************************************** + + FileName [ivyDsd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Disjoint-support decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// decomposition types +typedef enum { + IVY_DEC_PI, // 0: var + IVY_DEC_CONST1, // 1: CONST1 + IVY_DEC_BUF, // 2: BUF + IVY_DEC_AND, // 3: AND + IVY_DEC_EXOR, // 4: EXOR + IVY_DEC_MUX, // 5: MUX + IVY_DEC_MAJ, // 6: MAJ + IVY_DEC_PRIME // 7: undecomposable +} Ivy_DecType_t; + +typedef struct Ivy_Dec_t_ Ivy_Dec_t; +struct Ivy_Dec_t_ +{ + unsigned Type : 4; // the node type (PI, CONST1, AND, EXOR, MUX, PRIME) + unsigned fCompl : 1; // shows if node is complemented (root node only) + unsigned nFans : 3; // the number of fanins + unsigned Fan0 : 4; // fanin 0 + unsigned Fan1 : 4; // fanin 1 + unsigned Fan2 : 4; // fanin 2 + unsigned Fan3 : 4; // fanin 3 + unsigned Fan4 : 4; // fanin 4 + unsigned Fan5 : 4; // fanin 5 +}; + +static inline int Ivy_DecToInt( Ivy_Dec_t Node ) { return *((int *)&Node); } +static inline Ivy_Dec_t Ivy_IntToDec( int Node ) { return *((Ivy_Dec_t *)&Node); } +static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *((int *)pNode) = 0; } + + +static unsigned s_Masks[6][2] = { + { 0x55555555, 0xAAAAAAAA }, + { 0x33333333, 0xCCCCCCCC }, + { 0x0F0F0F0F, 0xF0F0F0F0 }, + { 0x00FF00FF, 0xFF00FF00 }, + { 0x0000FFFF, 0xFFFF0000 }, + { 0x00000000, 0xFFFFFFFF } +}; + +static inline int Ivy_TruthWordCountOnes( 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 Ivy_TruthCofactorIsConst( unsigned uTruth, int Var, int Cof, int Const ) +{ + if ( Const == 0 ) + return (uTruth & s_Masks[Var][Cof]) == 0; + else + return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof]; +} + +static inline int Ivy_TruthCofactorIsOne( unsigned uTruth, int Var ) +{ + return (uTruth & s_Masks[Var][0]) == 0; +} + +static inline unsigned Ivy_TruthCofactor( unsigned uTruth, int Var ) +{ + unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0]; + int Shift = (1 << (Var >> 1)); + if ( Var & 1 ) + return uCofactor | (uCofactor << Shift); + return uCofactor | (uCofactor >> Shift); +} + +static inline unsigned Ivy_TruthCofactor2( unsigned uTruth, int Var0, int Var1 ) +{ + return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 ); +} + +// returns 1 if the truth table depends on this var (var is regular interger var) +static inline int Ivy_TruthDepends( unsigned uTruth, int Var ) +{ + return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1); +} + +static inline void Ivy_DecSetVar( Ivy_Dec_t * pNode, int iNum, unsigned Var ) +{ + assert( iNum >= 0 && iNum <= 5 ); + switch( iNum ) + { + case 0: pNode->Fan0 = Var; break; + case 1: pNode->Fan1 = Var; break; + case 2: pNode->Fan2 = Var; break; + case 3: pNode->Fan3 = Var; break; + case 4: pNode->Fan4 = Var; break; + case 5: pNode->Fan5 = Var; break; + } +} + +static inline unsigned Ivy_DecGetVar( Ivy_Dec_t * pNode, int iNum ) +{ + assert( iNum >= 0 && iNum <= 5 ); + switch( iNum ) + { + case 0: return pNode->Fan0; + case 1: return pNode->Fan1; + case 2: return pNode->Fan2; + case 3: return pNode->Fan3; + case 4: return pNode->Fan4; + case 5: return pNode->Fan5; + } + return ~0; +} + +static int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree ); +static int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree ); + +//int nTruthDsd; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes DSD of truth table of 5 variables or less.] + + Description [Returns 1 if the function is a constant or is fully + DSD decomposable using AND/EXOR/MUX gates.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int i, RetValue; + // set the PI variables + Vec_IntClear( vTree ); + for ( i = 0; i < 5; i++ ) + Vec_IntPush( vTree, 0 ); + // check if it is a constant + if ( uTruth == 0 || ~uTruth == 0 ) + { + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_CONST1; + Node.fCompl = (uTruth == 0); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return 1; + } + // perform the decomposition + RetValue = Ivy_TruthDecompose_rec( uTruth, vTree ); + if ( RetValue == -1 ) + return 0; + // get the topmost node + if ( (RetValue >> 1) < 5 ) + { // add buffer + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_BUF; + Node.fCompl = (RetValue & 1); + Node.Fan0 = ((RetValue >> 1) << 1); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + } + else if ( RetValue & 1 ) + { // check if the topmost node has to be complemented + Node = Ivy_IntToDec( Vec_IntPop(vTree) ); + assert( Node.fCompl == 0 ); + Node.fCompl = (RetValue & 1); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + } + if ( uTruth != Ivy_TruthDsdCompute(vTree) ) + printf( "Verification failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes DSD of truth table.] + + Description [Returns the number of topmost decomposition node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars; + int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, i; + unsigned uTruthCof, uCof0, uCof1; + + // get constant confactors + Count0 = Count1 = Count2 = nSupp = 0; + for ( i = 0; i < 5; i++ ) + { + if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) ) + Vars0[Count0++] = (i << 1) | 0; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) ) + Vars0[Count0++] = (i << 1) | 1; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) ) + Vars1[Count1++] = (i << 1) | 0; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) ) + Vars1[Count1++] = (i << 1) | 1; + else + { + uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 ); + uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 ); + if ( uCof0 == ~uCof1 ) + Vars2[Count2++] = (i << 1) | 0; + else if ( uCof0 != uCof1 ) + Supp[nSupp++] = i; + } + } + assert( Count0 == 0 || Count1 == 0 ); + assert( Count0 == 0 || Count2 == 0 ); + assert( Count1 == 0 || Count2 == 0 ); + + // consider the case of a single variable + if ( Count0 == 1 && nSupp == 0 ) + return Vars0[0]; + + // consider more complex decompositions + if ( Count0 == 0 && Count1 == 0 && Count2 == 0 ) + return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree ); + + // extract the nodes + Ivy_DecClear( &Node ); + if ( Count0 > 0 ) + nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND, fCompl = 0; + else if ( Count1 > 0 ) + nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND, fCompl = 1, uTruth = ~uTruth; + else if ( Count2 > 0 ) + nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0; + else + assert( 0 ); + Node.nFans = nVars+(nSupp>0); + + // compute cofactor + uTruthCof = uTruth; + for ( i = 0; i < nVars; i++ ) + { + uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] ); + Ivy_DecSetVar( &Node, i, pVars[i] ); + } + + if ( Node.Type == IVY_DEC_EXOR ) + fCompl ^= ((Node.nFans & 1) == 0); + + if ( nSupp > 0 ) + { + assert( uTruthCof != 0 && ~uTruthCof != 0 ); + // call recursively + RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree ); + // quit if non-decomposable + if ( RetValue == -1 ) + return -1; + // remove the complement from the child if the node is EXOR + if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) ) + { + fCompl ^= 1; + RetValue ^= 1; + } + // set the new decomposition + Ivy_DecSetVar( &Node, nVars, RetValue ); + } + else if ( Node.Type == IVY_DEC_EXOR ) + fCompl ^= (uTruthCof == 0); + + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | fCompl; +} + +/**Function************************************************************* + + Synopsis [Returns a non-negative number if the truth table is a MUX.] + + Description [If the truth table is a MUX, returns the variable as follows: + first, control variable; second, positive cofactor; third, negative cofactor.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int i, k, RetValue0, RetValue1; + unsigned uCof0, uCof1, Num; + char Count[3]; + assert( nSupp >= 3 ); + // start the node + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_MUX; + Node.nFans = 3; + // try each of the variables + for ( i = 0; i < nSupp; i++ ) + { + // get the cofactors with respect to these variables + uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 ); + uCof1 = Ivy_TruthCofactor( uTruth, pSupp[i] << 1 ); + // go through all other variables and make sure + // each of them belongs to the support of one cofactor + for ( k = 0; k < nSupp; k++ ) + { + if ( k == i ) + continue; + if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) ) + break; + } + if ( k < nSupp ) + continue; + // MUX decomposition exists + RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree ); + if ( RetValue0 == -1 ) + break; + RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree ); + if ( RetValue1 == -1 ) + break; + // both of them exist; create the node + Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 ); + Ivy_DecSetVar( &Node, 1, RetValue1 ); + Ivy_DecSetVar( &Node, 2, RetValue0 ); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | 0; + } + // check majority gate + if ( nSupp > 3 ) + return -1; + if ( Ivy_TruthWordCountOnes(uTruth) != 16 ) + return -1; + // this is a majority gate; determine polarity + Node.Type = IVY_DEC_MAJ; + Count[0] = Count[1] = Count[2] = 0; + for ( i = 0; i < 8; i++ ) + { + Num = 0; + for ( k = 0; k < 3; k++ ) + if ( i & (1 << k) ) + Num |= (1 << pSupp[k]); + assert( Num < 32 ); + if ( (uTruth & (1 << Num)) == 0 ) + continue; + for ( k = 0; k < 3; k++ ) + if ( i & (1 << k) ) + Count[k]++; + } + assert( Count[0] == 1 || Count[0] == 3 ); + assert( Count[1] == 1 || Count[1] == 3 ); + assert( Count[2] == 1 || Count[2] == 3 ); + Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) ); + Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) ); + Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) ); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | 0; +} + + +/**Function************************************************************* + + Synopsis [Computes truth table of decomposition tree for verification.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_TruthDsdCompute_rec( int iNode, Vec_Int_t * vTree ) +{ + unsigned uTruthChild, uTruthTotal; + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + return s_Masks[5][ !Node.fCompl ]; + if ( Node.Type == IVY_DEC_PI ) + return s_Masks[iNode][ !Node.fCompl ]; + if ( Node.Type == IVY_DEC_BUF ) + { + uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree ); + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + if ( Node.Type == IVY_DEC_AND ) + { + uTruthTotal = s_Masks[5][1]; + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree ); + uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild; + } + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + if ( Node.Type == IVY_DEC_EXOR ) + { + uTruthTotal = 0; + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree ); + assert( (Var & 1) == 0 ); + } + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + assert( Node.fCompl == 0 ); + if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + unsigned uTruthChildC, uTruthChild1, uTruthChild0; + int VarC, Var1, Var0; + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree ); + uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree ); + uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree ); + assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 ); + uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC; + uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1; + uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0; + if ( Node.Type == IVY_DEC_MUX ) + return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0); + else + return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0); + } + assert( 0 ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Computes truth table of decomposition tree for verification.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ) +{ + return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree ); +} + +/**Function************************************************************* + + Synopsis [Prints the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdPrint_rec( FILE * pFile, int iNode, Vec_Int_t * vTree ) +{ + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") ); + else if ( Node.Type == IVY_DEC_PI ) + fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") ); + else if ( Node.Type == IVY_DEC_BUF ) + { + Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree ); + fprintf( pFile, "%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_AND ) + { + fprintf( pFile, "AND(" ); + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree ); + fprintf( pFile, "%s", (Var & 1)? "\'" : "" ); + if ( i != (int)Node.nFans-1 ) + fprintf( pFile, "," ); + } + fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_EXOR ) + { + fprintf( pFile, "EXOR(" ); + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree ); + if ( i != (int)Node.nFans-1 ) + fprintf( pFile, "," ); + assert( (Var & 1) == 0 ); + } + fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + int VarC, Var1, Var0; + assert( Node.fCompl == 0 ); + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" ); + Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree ); + fprintf( pFile, "%s", (VarC & 1)? "\'" : "" ); + fprintf( pFile, "," ); + Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree ); + fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" ); + fprintf( pFile, "," ); + Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree ); + fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" ); + fprintf( pFile, ")" ); + } + else assert( 0 ); +} + + +/**Function************************************************************* + + Synopsis [Prints the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ) +{ + fprintf( pFile, "F = " ); + Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Implement DSD in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNode, Vec_Int_t * vTree ) +{ + Ivy_Obj_t * pResult, * pChild, * pNodes[16]; + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl ); + if ( Node.Type == IVY_DEC_PI ) + { + pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + if ( Node.Type == IVY_DEC_BUF ) + { + pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR ) + { + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 ); + pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree ); + pChild = Ivy_NotCond( pChild, (Var & 1) ); + pNodes[i] = pChild; + } + +// Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); + + pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + assert( Node.fCompl == 0 ); + if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + int VarC, Var1, Var0; + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree ); + pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree ); + pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree ); + assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 ); + pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) ); + pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) ); + pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) ); + if ( Node.Type == IVY_DEC_MUX ) + return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] ); + else + return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] ); + } + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Implement DSD in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ) +{ + int Entry, i; + // implement latches on the frontier (TEMPORARY!!!) + Vec_IntForEachEntry( vFront, Entry, i ) + Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) ); + // recursively construct the tree + return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree ); +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdComputePrint( unsigned uTruth ) +{ + static Vec_Int_t * vTree = NULL; + if ( vTree == NULL ) + vTree = Vec_IntAlloc( 12 ); + if ( Ivy_TruthDsd( uTruth, vTree ) ) + Ivy_TruthDsdPrint( stdout, vTree ); + else + printf( "Undecomposable\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTestOne( unsigned uTruth ) +{ + static int Counter = 0; + static Vec_Int_t * vTree = NULL; + // decompose + if ( vTree == NULL ) + vTree = Vec_IntAlloc( 12 ); + + if ( !Ivy_TruthDsd( uTruth, vTree ) ) + { +// printf( "Undecomposable\n" ); + } + else + { +// nTruthDsd++; + printf( "%5d : ", Counter++ ); + Extra_PrintBinary( stdout, &uTruth, 32 ); + printf( " " ); + Ivy_TruthDsdPrint( stdout, vTree ); + if ( uTruth != Ivy_TruthDsdCompute(vTree) ) + printf( "Verification failed.\n" ); + } +// Vec_IntFree( vTree ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + + pFile = fopen( "npn4.txt", "r" ); + for ( i = 0; i < 222; i++ ) +// pFile = fopen( "npn5.txt", "r" ); +// for ( i = 0; i < 616126; i++ ) + { + fscanf( pFile, "%s", Buffer ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); +// Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); + uTruth |= (uTruth << 16); +// uTruth = ~uTruth; + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest3() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + + pFile = fopen( "npn3.txt", "r" ); + for ( i = 0; i < 14; i++ ) + { + fscanf( pFile, "%s", Buffer ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 ); + uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest5() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + +// pFile = fopen( "npn4.txt", "r" ); +// for ( i = 0; i < 222; i++ ) + pFile = fopen( "npn5.txt", "r" ); + for ( i = 0; i < 616126; i++ ) + { + fscanf( pFile, "%s", Buffer ); +// Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); +// uTruth |= (uTruth << 16); +// uTruth = ~uTruth; + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c new file mode 100644 index 00000000..04c31f3d --- /dev/null +++ b/src/temp/ivy/ivyMan.c @@ -0,0 +1,207 @@ +/**CFile**************************************************************** + + FileName [ivyMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pObj; + int i, nTotalSize; + // start the manager + p = ALLOC( Ivy_Man_t, 1 ); + memset( p, 0, sizeof(Ivy_Man_t) ); + p->nTravIds = 1; + // AIG nodes + p->nObjsAlloc = 1 + nPis + nPos + nNodesMax; +// p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even + nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1; + p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize ); + memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize ); + // temporary storage for deleted entries + p->vFree = Vec_IntAlloc( 100 ); + // set the node IDs + for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ ) + pObj->Id = i - IVY_SANDBOX_SIZE - 1; + // remember the manager in the first entry + *((Ivy_Man_t **)p->pObjs) = p; + p->pObjs += IVY_SANDBOX_SIZE + 1; + // create the constant node + p->nCreated = 1; + p->ObjIdNext = 1; + Ivy_ManConst1(p)->fPhase = 1; + // create PIs + pObj = Ivy_ManGhost(p); + pObj->Type = IVY_PI; + p->vPis = Vec_IntAlloc( 100 ); + for ( i = 0; i < nPis; i++ ) + Ivy_ObjCreate( pObj ); + // create POs + pObj->Type = IVY_PO; + p->vPos = Vec_IntAlloc( 100 ); + for ( i = 0; i < nPos; i++ ) + Ivy_ObjCreate( pObj ); + // start the table + p->nTableSize = p->nObjsAlloc*5/2+13; + p->pTable = ALLOC( int, p->nTableSize ); + memset( p->pTable, 0, sizeof(int) * p->nTableSize ); + // allocate undo storage + p->nUndosAlloc = 100; + p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc ); + memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStop( Ivy_Man_t * p ) +{ + if ( p->fExtended ) + { + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachObj( p, pObj, i ) + if ( Ivy_ObjGetFanins(pObj) ) + Vec_IntFree( Ivy_ObjGetFanins(pObj) ); + } + if ( p->vFree ) Vec_IntFree( p->vFree ); + if ( p->vTruths ) Vec_IntFree( p->vTruths ); + if ( p->vPis ) Vec_IntFree( p->vPis ); + if ( p->vPos ) Vec_IntFree( p->vPos ); + FREE( p->pMemory ); + free( p->pObjs - IVY_SANDBOX_SIZE - 1 ); + free( p->pTable ); + free( p->pUndos ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManGrow( Ivy_Man_t * p ) +{ + int i; + assert( p->ObjIdNext == p->nObjsAlloc ); + if ( p->ObjIdNext != p->nObjsAlloc ) + return; +// printf( "Ivy_ObjCreate(): Reallocing the node array.\n" ); + p->nObjsAlloc = 2 * p->nObjsAlloc; + p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1; + memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 ); + for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ ) + Ivy_ManObj( p, i )->Id = i; +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManCleanup( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pNode; + int i, nNodesOld; + nNodesOld = Ivy_ManNodeNum(p); + Ivy_ManForEachNode( p, pNode, i ) + if ( Ivy_ObjRefs(pNode) == 0 ) + Ivy_ObjDelete_rec( pNode, 1 ); + return nNodesOld - Ivy_ManNodeNum(p); +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManPrintStats( Ivy_Man_t * p ) +{ + printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) ); + if ( p->fExtended ) + { + printf( "Am = %d. ", Ivy_ManAndMultiNum(p) ); + printf( "Xm = %d. ", Ivy_ManExorMultiNum(p) ); + printf( "Lut = %d. ", Ivy_ManLutNum(p) ); + } + else + { + printf( "A = %d. ", Ivy_ManAndNum(p) ); + printf( "X = %d. ", Ivy_ManExorNum(p) ); + printf( "B = %d. ", Ivy_ManBufNum(p) ); + } + printf( "MaxID = %d. ", p->ObjIdNext-1 ); + printf( "All = %d. ", p->nObjsAlloc ); + printf( "Cre = %d. ", p->nCreated ); + printf( "Del = %d. ", p->nDeleted ); + printf( "\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c new file mode 100644 index 00000000..059d1500 --- /dev/null +++ b/src/temp/ivy/ivyMulti.c @@ -0,0 +1,427 @@ +/**CFile**************************************************************** + + FileName [ivyMulti.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Constructing multi-input AND/EXOR gates.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyMulti.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Eval_t_ Ivy_Eval_t; +struct Ivy_Eval_t_ +{ + unsigned Mask : 5; // the mask of covered nodes + unsigned Weight : 3; // the number of covered nodes + unsigned Cost : 4; // the number of overlapping nodes + unsigned Level : 12; // the level of this node + unsigned Fan0 : 4; // the first fanin + unsigned Fan1 : 4; // the second fanin +}; + +static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ); +static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ); +static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Constructs the well-balanced tree of gates.] + + Description [Disregards levels and possible logic sharing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type ); + pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Ivy_Oper( pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Constructs a balanced tree while taking sharing into account.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type ) +{ + static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5}; + static Ivy_Eval_t pEvals[15+15*14/2]; + static Ivy_Obj_t * pArgs[16]; + Ivy_Eval_t * pEva, * pEvaBest; + int nArgsNew, nEvals, i, k; + Ivy_Obj_t * pTemp; + + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgsInit[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type ); + +//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" ); + + // set the initial ones + for ( i = 0; i < nArgs; i++ ) + { + pArgs[i] = pArgsInit[i]; + pEva = pEvals + i; + pEva->Mask = (1 << i); + pEva->Weight = 1; + pEva->Cost = 0; + pEva->Level = Ivy_Regular(pArgs[i])->Level; + pEva->Fan0 = 0; + pEva->Fan1 = 0; + } + + // find the available nodes + pEvaBest = pEvals; + nArgsNew = nArgs; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) ) + { + pEva = pEvals + nArgsNew; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; +// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) ); + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + pArgs[nArgsNew++] = pTemp; + if ( nArgsNew == 15 ) + goto Outside; + } +Outside: + +// printf( "Best = %d.\n", pEvaBest - pEvals ); + + // the case of no common nodes + if ( nArgsNew == nArgs ) + { + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case of one common node + if ( nArgsNew == nArgs + 1 ) + { + assert( pEvaBest - pEvals == nArgs ); + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pArgs[nArgs]; + assert( k == nArgs - 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case when there is a node that covers everything + if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) ) + return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // evaluate node pairs + nEvals = nArgsNew; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + { + pEva = pEvals + nEvals; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + nEvals++; + } + assert( pEvaBest - pEvals >= nArgsNew ); + +// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 ); + + // get the best implementation + pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // collect those not covered by EvaBest + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( (pEvaBest->Mask & (1 << i)) == 0 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pTemp; + assert( k == nArgs - (int)pEvaBest->Weight + 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNode0, * pNode1; + if ( iNum < nArgs ) + return pArgs[iNum]; + pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type ); + pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type ); + return Ivy_Oper( pNode0, pNode1, Type ); +} + +/**Function************************************************************* + + Synopsis [Selection-sorts the nodes in the decreasing over of level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ) +{ + Ivy_Obj_t * pTemp; + int i, j, iBest; + + for ( i = 0; i < nArgs-1; i++ ) + { + iBest = i; + for ( j = i+1; j < nArgs; j++ ) + if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level ) + iBest = j; + pTemp = pArgs[i]; + pArgs[i] = pArgs[iBest]; + pArgs[iBest] = pTemp; + } +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode1, * pNode2; + int i; + // try to find the node in the array + for ( i = 0; i < nArgs; i++ ) + if ( pArray[i] == pNode ) + return nArgs; + // put the node last + pArray[nArgs++] = pNode; + // find the place to put the new node + for ( i = nArgs-1; i > 0; i-- ) + { + pNode1 = pArray[i ]; + pNode2 = pArray[i-1]; + if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + break; + pArray[i ] = pNode2; + pArray[i-1] = pNode1; + } + return nArgs; +} + +/**Function************************************************************* + + Synopsis [Balances the array recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNodeNew; + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgs[0], pArgs[1], Type ); + // get the last two nodes + pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type ); + // add the new node + nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pTemp; + int i, k; + int nArgsOld = nArgs; + for ( i = 0; i < nArgs; i++ ) + printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level ); + for ( i = 1; i < nArgs; i++ ) + for ( k = 0; k < i; k++ ) + { + pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)); + if ( pTemp != NULL ) + { + printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i ); + pArgs[nArgs++] = pTemp; + } + } + printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld ); + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pArgsRef[5], * pTemp; + int i, k, m, nArgsNew, Counter = 0; + + +//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" ); + + + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + + // find the nodes with more than one fanout + nArgsNew = 0; + for ( i = 0; i < nArgs; i++ ) + if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 ) + pArgsRef[nArgsNew++] = pArgs[i]; + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + Counter++; +// printf( "%d", Counter ); + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + { + nArgsNew = 0; + for ( m = 0; m < nArgs; m++ ) + if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] ) + pArgs[nArgsNew++] = pArgs[m]; + pArgs[nArgsNew++] = pTemp; + assert( nArgsNew == nArgs - 1 ); + return Ivy_Multi1( pArgs, nArgsNew, Type ); + } + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c new file mode 100644 index 00000000..5d063525 --- /dev/null +++ b/src/temp/ivy/ivyObj.c @@ -0,0 +1,325 @@ +/**CFile**************************************************************** + + FileName [ivyObj.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Adding/removing objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) +{ + Ivy_Man_t * p = Ivy_ObjMan(pGhost); + Ivy_Obj_t * pObj; + assert( !Ivy_IsComplement(pGhost) ); + assert( Ivy_ObjIsGhost(pGhost) ); + + assert( Ivy_TableLookup(pGhost) == NULL ); + + // realloc the node array + if ( p->ObjIdNext == p->nObjsAlloc ) + { + Ivy_ManGrow( p ); + pGhost = Ivy_ManGhost( p ); + } + // get memory for the new object + if ( Vec_IntSize(p->vFree) > 0 ) + pObj = p->pObjs + Vec_IntPop(p->vFree); + else + pObj = p->pObjs + p->ObjIdNext++; + assert( pObj->Id == pObj - p->pObjs ); + assert( Ivy_ObjIsNone(pObj) ); + // add basic info (fanins, compls, type, init) + Ivy_ObjOverwrite( pObj, pGhost ); + // increment references of the fanins + Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); + Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); + // add the node to the structural hash table + Ivy_TableInsert( pObj ); + // compute level + if ( Ivy_ObjIsNode(pObj) ) + pObj->Level = Ivy_ObjLevelNew(pObj); + else if ( Ivy_ObjIsLatch(pObj) ) + pObj->Level = 0; + else if ( Ivy_ObjIsOneFanin(pObj) ) + pObj->Level = Ivy_ObjFanin0(pObj)->Level; + else if ( !Ivy_ObjIsPi(pObj) ) + assert( 0 ); + // mark the fanins in a special way if the node is EXOR + if ( Ivy_ObjIsExor(pObj) ) + { + Ivy_ObjFanin0(pObj)->fExFan = 1; + Ivy_ObjFanin1(pObj)->fExFan = 1; + } + // add PIs/POs to the arrays + if ( Ivy_ObjIsPi(pObj) ) + Vec_IntPush( p->vPis, pObj->Id ); + else if ( Ivy_ObjIsPo(pObj) ) + Vec_IntPush( p->vPos, pObj->Id ); + // update node counters of the manager + p->nObjs[Ivy_ObjType(pObj)]++; + p->nCreated++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj; + assert( Type == IVY_ANDM || Type == IVY_EXORM || Type == IVY_LUT ); + // realloc the node array + if ( p->ObjIdNext == p->nObjsAlloc ) + Ivy_ManGrow( p ); + // create the new node + pObj = p->pObjs + p->ObjIdNext; + assert( pObj->Id == p->ObjIdNext ); + p->ObjIdNext++; + pObj->Type = Type; + // update node counters of the manager + p->nObjs[Type]++; + p->nCreated++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Connect the object to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsOneFanin(pObj) ); + assert( Ivy_ObjFaninId0(pObj) == 0 ); + // add the first fanin + pObj->fComp0 = Ivy_IsComplement(pFanin); + pObj->Fanin0 = Ivy_Regular(pFanin)->Id; + // increment references of the fanins + Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); + // add the node to the structural hash table + Ivy_TableInsert( pObj ); +} + +/**Function************************************************************* + + Synopsis [Deletes the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ) +{ + Ivy_Man_t * p; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjRefs(pObj) == 0 ); + // remove connections + Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); + Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); + // remove the node from the structural hash table + Ivy_TableDelete( pObj ); + // update node counters of the manager + p = Ivy_ObjMan(pObj); + p->nObjs[pObj->Type]--; + p->nDeleted++; + // remove PIs/POs from the arrays + if ( Ivy_ObjIsPi(pObj) ) + Vec_IntRemove( p->vPis, pObj->Id ); + else if ( Ivy_ObjIsPo(pObj) ) + Vec_IntRemove( p->vPos, pObj->Id ); + // recorde the deleted node + if ( p->fRecording ) + Ivy_ManUndoRecord( p, pObj ); + // clean the node's memory + Ivy_ObjClean( pObj ); + // remember the entry + if ( fFreeTop ) + Vec_IntPush( p->vFree, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Deletes the MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ) +{ + Ivy_Obj_t * pFanin0, * pFanin1; + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsNone(pObj) ); + if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) ) + return; + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + Ivy_ObjDelete( pObj, fFreeTop ); + if ( !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 ) + Ivy_ObjDelete_rec( pFanin0, 1 ); + if ( !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 ) + Ivy_ObjDelete_rec( pFanin1, 1 ); +} + +/**Function************************************************************* + + Synopsis [Replaces one object by another.] + + Description [Both objects are currently in the manager. The new object + (pObjNew) should be used instead of the old object (pObjOld). If the + new object is complemented or used, the buffer is added.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ) +{ + int nRefsOld; + // the object to be replaced cannot be complemented + assert( !Ivy_IsComplement(pObjOld) ); + // the object to be replaced cannot be a terminal + assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsTerm(pObjOld) ); + // the object to be used cannot be a PO or assert + assert( !Ivy_ObjIsPo(Ivy_Regular(pObjNew)) ); + // the object cannot be the same + assert( pObjOld != Ivy_Regular(pObjNew) ); + // if the new object is complemented or already used, add the buffer + if ( Ivy_IsComplement(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) + pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pObjNew, Ivy_ObjConst1(pObjOld), IVY_BUF, IVY_INIT_NONE) ); + assert( !Ivy_IsComplement(pObjNew) ); + // remember the reference counter + nRefsOld = pObjOld->nRefs; + pObjOld->nRefs = 0; + // delete the old object + if ( fDeleteOld ) + Ivy_ObjDelete_rec( pObjOld, fFreeTop ); + // transfer the old object + assert( Ivy_ObjRefs(pObjNew) == 0 ); + Ivy_ObjOverwrite( pObjOld, pObjNew ); + pObjOld->nRefs = nRefsOld; + // update the hash table + Ivy_TableUpdate( pObjNew, pObjOld->Id ); + // create the object that was taken over by pObjOld + Ivy_ObjClean( pObjNew ); + // remember the entry + Vec_IntPush( Ivy_ObjMan(pObjOld)->vFree, pObjNew->Id ); +} + +/**Function************************************************************* + + Synopsis [Returns the first real fanins (not a buffer/inverter).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + { + if ( Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ) + return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin0(pNode), 0), Ivy_ObjFaninC0(pNode) ); + else + return Ivy_ObjChild0(pNode); + } + else + { + if ( Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) + return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin1(pNode), 0), Ivy_ObjFaninC1(pNode) ); + else + return Ivy_ObjChild1(pNode); + } +} + +/**Function************************************************************* + + Synopsis [Fixes buffer fanins.] + + Description [This situation happens because NodeReplace is a lazy + procedure, which does not propagate the change to the fanouts but + instead records the change in the form of a buf/inv node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult; + assert( Ivy_ObjIsNode(pNode) ); + if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) + return; + // get the real fanins + pFanReal0 = Ivy_NodeRealFanin_rec( pNode, 0 ); + pFanReal1 = Ivy_NodeRealFanin_rec( pNode, 1 ); + // get the new node + pResult = Ivy_Oper( pFanReal0, pFanReal1, Ivy_ObjType(pNode) ); + // perform the replacement + Ivy_ObjReplace( pNode, pResult, 1, 0 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c new file mode 100644 index 00000000..a10ba343 --- /dev/null +++ b/src/temp/ivy/ivyOper.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [ivyOper.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG operations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// procedure to detect an EXOR gate +static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t ** ppFan0, Ivy_Obj_t ** ppFan1 ) +{ + if ( !Ivy_IsComplement(p0) || !Ivy_IsComplement(p1) ) + return 0; + p0 = Ivy_Regular(p0); + p1 = Ivy_Regular(p1); + if ( !Ivy_ObjIsAnd(p0) || !Ivy_ObjIsAnd(p1) ) + return 0; + if ( Ivy_ObjFanin0(p0) != Ivy_ObjFanin0(p1) || Ivy_ObjFanin1(p0) != Ivy_ObjFanin1(p1) ) + return 0; + if ( Ivy_ObjFaninC0(p0) == Ivy_ObjFaninC0(p1) || Ivy_ObjFaninC1(p0) == Ivy_ObjFaninC1(p1) ) + return 0; + *ppFan0 = Ivy_ObjChild0(p0); + *ppFan1 = Ivy_ObjChild1(p0); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Perform one operation.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) +{ + if ( Type == IVY_AND ) + return Ivy_And( p0, p1 ); + if ( Type == IVY_EXOR ) + return Ivy_Exor( p0, p1 ); + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + Ivy_Obj_t * pFan0, * pFan1; + // check trivial cases + if ( p0 == p1 ) + return p0; + if ( p0 == Ivy_Not(p1) ) + return Ivy_Not(pConst1); + if ( Ivy_Regular(p0) == pConst1 ) + return p0 == pConst1 ? p1 : Ivy_Not(pConst1); + if ( Ivy_Regular(p1) == pConst1 ) + return p1 == pConst1 ? p0 : Ivy_Not(pConst1); + // check if it can be an EXOR gate + if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) + return Ivy_CanonExor( pFan0, pFan1 ); + return Ivy_CanonAnd( p0, p1 ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + // check trivial cases + if ( p0 == p1 ) + return Ivy_Not(pConst1); + if ( p0 == Ivy_Not(p1) ) + return pConst1; + if ( Ivy_Regular(p0) == pConst1 ) + return Ivy_NotCond( p1, p0 == pConst1 ); + if ( Ivy_Regular(p1) == pConst1 ) + return Ivy_NotCond( p0, p1 == pConst1 ); + // check the table + return Ivy_CanonExor( p0, p1 ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) +{ + return Ivy_CanonLatch( pObj, Init ); +} + +/**Function************************************************************* + + Synopsis [Implements Boolean OR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp; + int Count0, Count1; + // consider trivial cases + if ( p0 == Ivy_Not(p1) ) + return Ivy_Exor( pC, p0 ); + // other cases can be added + // implement the first MUX (F = C * x1 + C' * x0) + pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, p1, IVY_AND, IVY_INIT_NONE) ); + pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) ); + if ( pTempA1 && pTempA2 ) + { + pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) ); + if ( pTemp ) return Ivy_Not(pTemp); + } + Count0 = (pTempA1 != NULL) + (pTempA2 != NULL); + // implement the second MUX (F' = C * x1' + C' * x0') + pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) ); + pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) ); + if ( pTempB1 && pTempB2 ) + { + pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) ); + if ( pTemp ) return pTemp; + } + Count1 = (pTempB1 != NULL) + (pTempB2 != NULL); + // compare and decide which one to implement + if ( Count0 >= Count1 ) + { + pTempA1 = pTempA1? pTempA1 : Ivy_And(pC, p1); + pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0); + return Ivy_Or( pTempA1, pTempA2 ); + } + pTempB1 = pTempB1? pTempB1 : Ivy_And(pC, Ivy_Not(p1)); + pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0)); + return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) ); + +// return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ) +{ + return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ) +{ + int i; + assert( vPairs->nSize > 0 ); + assert( vPairs->nSize % 2 == 0 ); + // go through the cubes of the node's SOP + for ( i = 0; i < vPairs->nSize; i += 2 ) + vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) ); + vPairs->nSize = vPairs->nSize/2; + return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c new file mode 100644 index 00000000..031db9bc --- /dev/null +++ b/src/temp/ivy/ivyRewrite.c @@ -0,0 +1,365 @@ +/**CFile**************************************************************** + + FileName [ivyRewrite.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ); +static void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ); +static int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs Boolean rewriting of sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) +{ + Vec_Int_t * vNodes, * vFront, * vInside, * vTree; + Ivy_Obj_t * pNode, * pNodeNew, * pTemp; + int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs; + int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock(); + unsigned uTruth; + + nInputs = 4; + vTree = Vec_IntAlloc( 8 ); + vFront = Vec_IntAlloc( 8 ); + vInside = Vec_IntAlloc( 50 ); + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + { + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + if ( Ivy_ObjIsBuf(pNode) ) + continue; + + // find one sequential cut rooted at this node +clk = clock(); + Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs ); +clkCut += clock() - clk; + // compute the truth table of the cut +clk = clock(); + uTruth = Ivy_ManSeqFindTruth( pNode, vFront ); +clkTru += clock() - clk; + // decompose the truth table +clk = clock(); + RetValue = Ivy_TruthDsd( uTruth, vTree ); +clkDsd += clock() - clk; + if ( !RetValue ) + continue; // DSD does not exist +// Ivy_TruthDsdPrint( stdout, vTree ); + +clk = clock(); + // remember the cost of the current network + nCostOld = Ivy_ManGetCost(p); + // increment references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { + pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + Ivy_ObjRefsInc( pTemp ); + } + // dereference and record undo + nRefsSaved = pNode->nRefs; pNode->nRefs = 0; + Ivy_ManUndoStart( p ); + Ivy_ObjDelete_rec( pNode, 0 ); + Ivy_ManUndoStop( p ); + pNode->nRefs = nRefsSaved; + + // get the intermediate cost + nCostInt = Ivy_ManGetCost(p); + +// printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt ); + + // construct the new logic cone + pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree ); + // remember the cost + nCostNew = Ivy_ManGetCost(p); + +// printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew ); +// nCostNew = nCostNew; + +/* + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + Ivy_ObjRefsDec( pTemp ); + } +clkUpd += clock() - clk; + continue; +*/ + + // detect the case when they are exactly the same +// if ( pNodeNew == pNode ) +// continue; + + // compare the costs + if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost ) + { // accept the change +// printf( "NODES GAINED = %d\n", nCostOld - nCostNew ); + + Ivy_ObjReplace( pNode, pNodeNew, 0, 1 ); + pNode->nRefs = nRefsSaved; + } + else + { // reject change +// printf( "Rejected\n" ); + + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + // reconstruct the old node + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + } + // decrement references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + if ( Ivy_ObjIsNone(pTemp) ) + continue; + Ivy_ObjRefsDec( pTemp ); + if ( Ivy_ObjRefs(pTemp) == 0 ) + Ivy_ObjDelete_rec( pTemp, 1 ); + } + +clkUpd += clock() - clk; + } + +PRT( "Cut ", clkCut ); +PRT( "Truth ", clkTru ); +PRT( "DSD ", clkDsd ); +PRT( "Update ", clkUpd ); +PRT( "TOTAL ", clock() - clkStart ); + + Vec_IntFree( vTree ); + Vec_IntFree( vFront ); + Vec_IntFree( vInside ); + Vec_IntFree( vNodes ); + + if ( !Ivy_ManCheck(p) ) + { + printf( "Ivy_ManSeqRewrite(): The check has failed.\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront ) +{ + static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth0, uTruth1; + Ivy_Obj_t * pNode; + int nLatches, Number; + // consider the case of a constant + if ( Node == 0 ) + return ~((unsigned)0); + // try to find this node in the frontier + Number = Vec_IntFind( vFront, Node ); + if ( Number >= 0 ) + return uMasks[Number]; + // get the node + pNode = Ivy_ManObj( p, Ivy_LeafId(Node) ); + assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) ); + // get the number of latches + nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode); + // expand the first fanin + uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC0(pNode) ) + uTruth0 = ~uTruth0; + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return uTruth0; + assert( Ivy_ObjIsNode(pNode) ); + // expand the second fanin + uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC1(pNode) ) + uTruth1 = ~uTruth1; + // return the truth table + return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ) +{ + assert( Ivy_ObjIsNode(pNode) ); + return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront ); +} + + +/**Function************************************************************* + + Synopsis [Recursively dereferences the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // deref the first fanin + pFan = Ivy_ObjFanin0(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // deref the second fanin + pFan = Ivy_ObjFanin1(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // save the node + Vec_IntPush( vCone, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Recursively references the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // ref the first fanin + pFan = Ivy_ObjFanin0(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); + // ref the second fanin + pFan = Ivy_ObjFanin1(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); +} + +/**Function************************************************************* + + Synopsis [Collect MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Vec_IntClear( vCone ); + Ivy_ManSeqDeref_rec( pNode, vCone ); + Ivy_ManSeqRef_rec( pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the cost of the logic cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pObj; + int i, Cost = 0; + Ivy_ManForEachNodeVec( p, vCone, pObj, i ) + { + if ( Ivy_ObjIsAnd(pObj) ) + Cost += 1; + else if ( Ivy_ObjIsExor(pObj) ) + Cost += 2; + } + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c new file mode 100644 index 00000000..d8fbdd9b --- /dev/null +++ b/src/temp/ivy/ivySeq.c @@ -0,0 +1,101 @@ +/**CFile**************************************************************** + + FileName [ivySeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts a combinational AIG manager into a sequential one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj, * pObjNew, * pFan0, * pFan1; + int i, fChanges; + assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) ); + // change POs into buffers + assert( Ivy_ManPoNum(p) == Vec_IntSize(p->vPos) ); + for ( i = Ivy_ManPoNum(p) - nLatches; i < Vec_IntSize(p->vPos); i++ ) + { + pObj = Ivy_ManPo(p, i); + pObj->Type = IVY_BUF; + } + // change PIs into latches and connect them to the corresponding POs + assert( Ivy_ManPiNum(p) == Vec_IntSize(p->vPis) ); + for ( i = Ivy_ManPiNum(p) - nLatches; i < Vec_IntSize(p->vPis); i++ ) + { + pObj = Ivy_ManPi(p, i); + pObj->Type = IVY_LATCH; + Ivy_ObjConnect( pObj, Ivy_ManPo(p, Ivy_ManPoNum(p) - Ivy_ManPiNum(p)) ); + } + // shrink the array + Vec_IntShrink( p->vPis, Ivy_ManPiNum(p) - nLatches ); + Vec_IntShrink( p->vPos, Ivy_ManPoNum(p) - nLatches ); + // update the counters of different objects + p->nObjs[IVY_PI] -= nLatches; + p->nObjs[IVY_PO] -= nLatches; + p->nObjs[IVY_BUF] += nLatches; + p->nObjs[IVY_LATCH] += nLatches; + // perform structural hashing while there are changes + fChanges = 1; + while ( fChanges ) + { + fChanges = 0; + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + { + if ( Ivy_ObjIsBuf(pObj) ) + continue; + pFan0 = Ivy_NodeRealFanin_rec( pObj, 0 ); + pFan1 = Ivy_NodeRealFanin_rec( pObj, 1 ); + if ( Ivy_ObjIsAnd(pObj) ) + pObjNew = Ivy_And(pFan0, pFan1); + else if ( Ivy_ObjIsExor(pObj) ) + pObjNew = Ivy_Exor(pFan0, pFan1); + else assert( 0 ); + if ( pObjNew == pObj ) + continue; + Ivy_ObjReplace( pObj, pObjNew, 1, 1 ); + fChanges = 1; + } + Vec_IntFree( vNodes ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c new file mode 100644 index 00000000..815caa29 --- /dev/null +++ b/src/temp/ivy/ivyTable.c @@ -0,0 +1,237 @@ +/**CFile**************************************************************** + + FileName [ivyTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Structural hashing table.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// hashing the node +static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize ) +{ + unsigned Key = Ivy_ObjIsExor(pObj) * 1699; + Key ^= Ivy_ObjFaninId0(pObj) * 7937; + Key ^= Ivy_ObjFaninId1(pObj) * 2971; + Key ^= Ivy_ObjFaninC0(pObj) * 911; + Key ^= Ivy_ObjFaninC1(pObj) * 353; + Key ^= Ivy_ObjInit(pObj) * 911; + return Key % TableSize; +} + +// returns the place where this node is stored (or should be stored) +static int * Ivy_TableFind( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + int i; + assert( Ivy_ObjIsHash(pObj) ); + p = Ivy_ObjMan(pObj); + for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) + if ( p->pTable[i] == pObj->Id ) + break; + return p->pTable + i; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks if node with the given attributes is in the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pEntry; + int i; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return NULL; + assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 ); + assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) ); + p = Ivy_ObjMan(pObj); + for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) + { + pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); + if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && + Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && + Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && + Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && + Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && + Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) ) + return Ivy_ObjObj( pObj, p->pTable[i] ); + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Adds the node to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableInsert( Ivy_Obj_t * pObj ) +{ + int * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == 0 ); + *pPlace = pObj->Id; +} + +/**Function************************************************************* + + Synopsis [Deletes the node from the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableDelete( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pEntry; + int i, * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == pObj->Id ); // node should be in the table + *pPlace = 0; + // rehash the adjacent entries + p = Ivy_ObjMan(pObj); + i = pPlace - p->pTable; + for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize ) + { + pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); + p->pTable[i] = 0; + Ivy_TableInsert( pEntry ); + } +} + +/**Function************************************************************* + + Synopsis [Updates the table to point to the new node.] + + Description [If the old node (pObj) is in the table, updates the table + to point to an object with different ID (ObjIdNew). The table should + not contain an object with ObjIdNew (this is currently not checked).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ) +{ + int * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == pObj->Id ); // node should be in the table + *pPlace = ObjIdNew; +} + +/**Function************************************************************* + + Synopsis [Count the number of nodes in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TableCountEntries( Ivy_Man_t * p ) +{ + int i, Counter = 0; + for ( i = 0; i < p->nTableSize; i++ ) + Counter += (p->pTable[i] != 0); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [Typically this procedure should not be called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableResize( Ivy_Man_t * p ) +{ + int * pTableOld, * pPlace; + int nTableSizeOld, Counter, e, clk; + assert( 0 ); +clk = clock(); + // save the old table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; + // get the new table + p->nTableSize = p->nObjsAlloc*5/2+13; + p->pTable = ALLOC( int, p->nTableSize ); + memset( p->pTable, 0, sizeof(int) * p->nTableSize ); + // rehash the entries from the old table + Counter = 0; + for ( e = 0; e < nTableSizeOld; e++ ) + { + if ( pTableOld[e] == 0 ) + continue; + Counter++; + // get the place where this entry goes in the table table + pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) ); + assert( *pPlace == 0 ); // should not be in the table + *pPlace = pTableOld[e]; + } + assert( Counter == Ivy_ManHashObjNum(p) ); +// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pTable ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyUndo.c b/src/temp/ivy/ivyUndo.c new file mode 100644 index 00000000..6612bf42 --- /dev/null +++ b/src/temp/ivy/ivyUndo.c @@ -0,0 +1,165 @@ +/**CFile**************************************************************** + + FileName [ivyUndo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Recording the results of recent deletion of logic cone.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoStart( Ivy_Man_t * p ) +{ + p->fRecording = 1; + p->nUndos = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoStop( Ivy_Man_t * p ) +{ + p->fRecording = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + Ivy_Obj_t * pObjUndo; + if ( p->nUndos >= p->nUndosAlloc ) + { + printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" ); + return; + } + pObjUndo = p->pUndos + p->nUndos++; + // required data for Ivy_ObjCreateGhost() + pObjUndo->Type = pObj->Type; + pObjUndo->Init = pObj->Init; + pObjUndo->Fanin0 = pObj->Fanin0; + pObjUndo->Fanin1 = pObj->Fanin1; + pObjUndo->fComp0 = pObj->fComp0; + pObjUndo->fComp1 = pObj->fComp1; + // additional data + pObjUndo->Id = pObj->Id; + pObjUndo->nRefs = pObj->nRefs; + pObjUndo->Level = pObj->Level; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Vec_IntPutLast( Vec_Int_t * vFree, int Last ) +{ + int Place, i; + // find the entry + Place = Vec_IntFind( vFree, Last ); + if ( Place == -1 ) + return 0; + // shift entries by one + assert( vFree->pArray[Place] == Last ); + for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ ) + vFree->pArray[i] = vFree->pArray[i+1]; + // put the entry in the end + vFree->pArray[i] = Last; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ) +{ + Ivy_Obj_t * pObjUndo, * pObjNew; + int i; + assert( p->nUndos > 0 ); + assert( p->fRecording == 0 ); + for ( i = p->nUndos - 1; i >= 0; i-- ) + { + // get the undo object + pObjUndo = p->pUndos + i; + // if this is the last object + if ( i == 0 ) + Vec_IntPush( p->vFree, pRoot->Id ); + else + Vec_IntPutLast( p->vFree, pObjUndo->Id ); + // create the new object + pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) ); + pObjNew->nRefs = pObjUndo->nRefs; + pObjNew->Level = pObjUndo->Level; + // make sure the object is created in the same place as before + assert( pObjNew->Id == pObjUndo->Id ); + } + p->nUndos = 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c new file mode 100644 index 00000000..590affd7 --- /dev/null +++ b/src/temp/ivy/ivyUtil.c @@ -0,0 +1,369 @@ +/**CFile**************************************************************** + + FileName [ivyUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Various procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Increments the current traversal ID of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManIncrementTravId( Ivy_Man_t * p ) +{ + if ( p->nTravIds >= (1<<30)-1 - 1000 ) + Ivy_ManCleanTravId( p ); + p->nTravIds++; +} + +/**Function************************************************************* + + Synopsis [Sets the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCleanTravId( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + p->nTravIds = 1; + Ivy_ManForEachObj( p, pObj, i ) + pObj->TravId = 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Ivy_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Ivy_ObjIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) + return 0; + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE ) +{ + Ivy_Obj_t * pNode0, * pNode1; + assert( !Ivy_IsComplement(pNode) ); + assert( Ivy_ObjIsMuxType(pNode) ); + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // find the control variable +// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) +{ + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) ); + Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes ); + Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes ); + Vec_IntPush( vNodes, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + int i, Leaf; + // collect and mark the leaves + Vec_IntClear( vNodes ); + Vec_IntForEachEntry( vLeaves, Leaf, i ) + { + Vec_IntPush( vNodes, Leaf ); + Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1; + } + // collect and mark the nodes + Ivy_ManCollectCut_rec( pRoot, vNodes ); + // clean the nodes + Vec_IntForEachEntry( vNodes, Leaf, i ) + Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0; +} + +/**Function************************************************************* + + Synopsis [Returns the pointer to the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth ) +{ + return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + int i; + pTruth = Ivy_ObjGetTruthStore( pNode->TravId, vTruth ); + pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth ); + pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth ); + if ( Ivy_ObjIsExor(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) +{ + static unsigned uTruths[8][8] = { // elementary truth tables + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + int i, Leaf; + // collect the cut + Ivy_ManCollectCut( pRoot, vLeaves, vNodes ); + // set the node numbers + Vec_IntForEachEntry( vNodes, Leaf, i ) + Ivy_ObjObj(pRoot, Leaf)->TravId = i; + // alloc enough memory + Vec_IntClear( vTruth ); + Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); + // set the elementary truth tables + Vec_IntForEachEntry( vLeaves, Leaf, i ) + memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); + // compute truths for other nodes + Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) + Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 ); + return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth ); +} + +/**Function************************************************************* + + Synopsis [Collect the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ) +{ + Vec_Int_t * vLatches; + Ivy_Obj_t * pObj; + int i; + vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); + Ivy_ManForEachLatch( p, pObj, i ) + Vec_IntPush( vLatches, pObj->Id ); + return vLatches; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivy_.c b/src/temp/ivy/ivy_.c new file mode 100644 index 00000000..65689689 --- /dev/null +++ b/src/temp/ivy/ivy_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [ivy_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make new file mode 100644 index 00000000..d59a3fa3 --- /dev/null +++ b/src/temp/ivy/module.make @@ -0,0 +1,14 @@ +SRC += src/temp/ivy/ivyBalance.c \ + src/temp/ivy/ivyCanon.c \ + src/temp/ivy/ivyCheck.c \ + src/temp/ivy/ivyCut.c \ + src/temp/ivy/ivyDfs.c \ + src/temp/ivy/ivyDsd.c \ + src/temp/ivy/ivyMan.c \ + src/temp/ivy/ivyObj.c \ + src/temp/ivy/ivyOper.c \ + src/temp/ivy/ivyRewrite.c \ + src/temp/ivy/ivySeq.c \ + src/temp/ivy/ivyTable.c \ + src/temp/ivy/ivyUndo.c \ + src/temp/ivy/ivyUtil.c diff --git a/src/temp/player/module.make b/src/temp/player/module.make new file mode 100644 index 00000000..81a5d77e --- /dev/null +++ b/src/temp/player/module.make @@ -0,0 +1,5 @@ +SRC += src/temp/player/playerAbc.c \ + src/temp/player/playerBuild.c \ + src/temp/player/playerCore.c \ + src/temp/player/playerMan.c \ + src/temp/player/playerUtil.c diff --git a/src/temp/player/player.h b/src/temp/player/player.h new file mode 100644 index 00000000..9ecad35b --- /dev/null +++ b/src/temp/player/player.h @@ -0,0 +1,123 @@ +/**CFile**************************************************************** + + FileName [player.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLA decomposition package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: player.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __XYZ_H__ +#define __XYZ_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#include "ivy.h" +#include "esop.h" +#include "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Pla_Man_t_ Pla_Man_t; +typedef struct Pla_Obj_t_ Pla_Obj_t; + +// storage for node information +struct Pla_Obj_t_ +{ + unsigned fFixed : 1; // fixed node + unsigned Depth : 7; // the depth in terms of LUTs/PLAs + unsigned nRefs : 24; // the number of references + Vec_Int_t vSupp[2]; // supports in two frames + Esop_Cube_t * pCover[2]; // esops in two frames +}; + +// storage for additional information +struct Pla_Man_t_ +{ + // general characteristics + int nLutMax; // the number of vars + int nPlaMax; // the number of vars + int nCubesMax; // the limit on the number of cubes in the intermediate covers + Ivy_Man_t * pManAig; // the AIG manager + Pla_Obj_t * pPlaStrs; // memory for structures + Esop_Man_t * pManMin; // the cube manager + // arrays to map local variables + Vec_Int_t * vComTo0; // mapping of common variables into first fanin + Vec_Int_t * vComTo1; // mapping of common variables into second fanin + Vec_Int_t * vPairs0; // the first var in each pair of common vars + Vec_Int_t * vPairs1; // the second var in each pair of common vars + Vec_Int_t * vTriv0; // trival support of the first node + Vec_Int_t * vTriv1; // trival support of the second node + // statistics + int nNodes; // the number of nodes processed + int nNodesLut; // the number of nodes processed + int nNodesPla; // the number of nodes processed + int nNodesBoth; // the number of nodes processed + int nNodesDeref; // the number of nodes processed +}; + +#define PLAYER_FANIN_LIMIT 128 + +#define PLA_MIN(a,b) (((a) < (b))? (a) : (b)) +#define PLA_MAX(a,b) (((a) > (b))? (a) : (b)) + +#define PLA_EMPTY ((Esop_Cube_t *)1) + +static inline Pla_Man_t * Ivy_ObjPlaMan( Ivy_Obj_t * pObj ) { return (Pla_Man_t *)Ivy_ObjMan(pObj)->pData; } +static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Obj_t * pObj ) { return Ivy_ObjPlaMan(pObj)->pPlaStrs + pObj->Id; } + +static inline unsigned * Ivy_ObjGetTruth( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p = Ivy_ObjMan(pObj); + int Offset = Vec_IntEntry( p->vTruths, pObj->Id ); + return Offset < 0 ? NULL : p->pMemory + Offset; + +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== playerAbc.c ==============================================================*/ +extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nFaninMax, int fVerbose ); +/*=== playerBuild.c ============================================================*/ +extern Ivy_Man_t * Pla_ManToAig( Ivy_Man_t * p ); +/*=== playerCore.c =============================================================*/ +extern Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose ); +/*=== playerMan.c ==============================================================*/ +extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax ); +extern void Pla_ManFree( Pla_Man_t * p ); +extern void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr ); +/*=== playerUtil.c =============================================================*/ +extern int Pla_ManMergeTwoSupports( Pla_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1, Vec_Int_t * vSupp ); +extern Esop_Cube_t * Pla_ManAndTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ); +extern Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ); +extern void Pla_ManComputeStats( Ivy_Man_t * pAig, Vec_Int_t * vNodes ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + + diff --git a/src/temp/player/playerAbc.c b/src/temp/player/playerAbc.c new file mode 100644 index 00000000..9cc342d9 --- /dev/null +++ b/src/temp/player/playerAbc.c @@ -0,0 +1,215 @@ +/**CFile**************************************************************** + + FileName [playerAbc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLAyer decomposition package.] + + Synopsis [Bridge between ABC and PLAyer.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 20, 2006.] + + Revision [$Id: playerAbc.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p ); +static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to PLAyer for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose ) +{ + Ivy_Man_t * pMan, * pManExt; + Abc_Ntk_t * pNtkAig; + if ( !Abc_NtkIsStrash(pNtk) ) + return NULL; + // convert to the new AIG manager + pMan = Ivy_ManFromAbc( pNtk ); + // check the correctness of conversion + if ( !Ivy_ManCheck( pMan ) ) + { + printf( "Abc_NtkPlayer: Internal AIG check has failed.\n" ); + Ivy_ManStop( pMan ); + return NULL; + } + if ( fVerbose ) + Ivy_ManPrintStats( pMan ); + // perform decomposition/mapping into PLAs/LUTs + pManExt = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose ); + Ivy_ManStop( pMan ); + pMan = pManExt; + if ( fVerbose ) + Ivy_ManPrintStats( pMan ); + // convert from the extended AIG manager into an SOP network + pNtkAig = Ivy_ManToAbc( pNtk, pMan ); + Ivy_ManStop( pMan ); + // chech the resulting network + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkPlayer: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Converts from strashed AIG in ABC into strash AIG in IVY.] + + Description [Assumes DFS ordering of nodes in the AIG of ABC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk ) +{ + Ivy_Man_t * pMan; + Abc_Obj_t * pObj; + int i; + // create the manager + pMan = Ivy_ManStart( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), Abc_NtkNodeNum(pNtk) + 10 ); + // create the PIs + Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Ivy_ManPi(pMan, i); + // perform the conversion of the internal nodes + Abc_AigForEachAnd( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Ivy_And( (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) ); + // create the POs + Abc_NtkForEachCo( pNtk, pObj, i ) + Ivy_ObjConnect( Ivy_ManPo(pMan, i), (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) ); + Ivy_ManCleanup( pMan ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Converts AIG manager after PLA/LUT mapping into a logic ABC network.] + + Description [The AIG manager contains nodes with extended functionality. + Node types are in pObj->Type. Node fanins are in pObj->vFanins. Functions + of LUT nodes are in pMan->vTruths.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) +{ + Abc_Ntk_t * pNtkNew; + Vec_Int_t * vIvyNodes, * vIvyFanins, * vTruths = pMan->vTruths; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew; + Ivy_Obj_t * pIvyNode, * pIvyFanin; + int pCompls[PLAYER_FANIN_LIMIT]; + int i, k, Fanin, nFanins; + // start the new ABC network + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // transfer the pointers to the basic nodes + Ivy_ManCleanTravId(pMan); + Ivy_ManConst1(pMan)->TravId = Abc_NtkConst1(pNtkNew)->Id; + Abc_NtkForEachCi( pNtkNew, pObjNew, i ) + Ivy_ManPi(pMan, i)->TravId = pObjNew->Id; + // construct the logic network isomorphic to logic network in the AIG manager + vIvyNodes = Ivy_ManDfsExt( pMan ); + Ivy_ManForEachNodeVec( pMan, vIvyNodes, pIvyNode, i ) + { + // get fanins of the old node + vIvyFanins = Ivy_ObjGetFanins( pIvyNode ); + nFanins = Vec_IntSize(vIvyFanins); + // create the new node + pObjNew = Abc_NtkCreateNode( pNtkNew ); + Vec_IntForEachEntry( vIvyFanins, Fanin, k ) + { + pIvyFanin = Ivy_ObjObj( pIvyNode, Ivy_FanId(Fanin) ); + pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId ); + Abc_ObjAddFanin( pObjNew, pFaninNew ); + pCompls[k] = Ivy_FanCompl(Fanin); + assert( Ivy_ObjIsAndMulti(pIvyNode) || nFanins == 1 || pCompls[k] == 0 ); // EXOR/LUT cannot have complemented fanins + } + assert( k <= PLAYER_FANIN_LIMIT ); + // create logic function of the node + if ( Ivy_ObjIsAndMulti(pIvyNode) ) + pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFanins, pCompls ); + else if ( Ivy_ObjIsExorMulti(pIvyNode) ) + pObjNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nFanins ); + else if ( Ivy_ObjIsLut(pIvyNode) ) + pObjNew->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, nFanins, Ivy_ObjGetTruth(pIvyNode) ); + else assert( 0 ); + assert( Abc_SopGetVarNum(pObjNew->pData) == nFanins ); + pIvyNode->TravId = pObjNew->Id; + } +//Pla_ManComputeStats( pMan, vIvyNodes ); + Vec_IntFree( vIvyNodes ); + // connect the PO nodes + Abc_NtkForEachCo( pNtkOld, pObj, i ) + { + // get the old fanin of the PO node + vIvyFanins = Ivy_ObjGetFanins( Ivy_ManPo(pMan, i) ); + Fanin = Vec_IntEntry( vIvyFanins, 0 ); + pIvyFanin = Ivy_ManObj( pMan, Ivy_FanId(Fanin) ); + // get the new ABC node corresponding to the old fanin + pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId ); + if ( Ivy_FanCompl(Fanin) ) // complement + { +// pFaninNew = Abc_NodeCreateInv(pNtkNew, pFaninNew); + if ( Abc_ObjIsCi(pFaninNew) ) + pFaninNew = Abc_NodeCreateInv(pNtkNew, pFaninNew); + else + { + // clone the node + pObjNew = Abc_NodeClone( pFaninNew ); + // set complemented functions + pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pFaninNew->pData ); + Abc_SopComplement(pObjNew->pData); + // return the new node + pFaninNew = pObjNew; + } + assert( Abc_SopGetVarNum(pFaninNew->pData) == Abc_ObjFaninNum(pFaninNew) ); + } + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + } + // remove dangling nodes + Abc_NtkForEachNode(pNtkNew, pObj, i) + if ( Abc_ObjFanoutNum(pObj) == 0 ) + Abc_NtkDeleteObj(pObj); + // fix CIs feeding directly into COs + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + return pNtkNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/player/playerBuild.c b/src/temp/player/playerBuild.c new file mode 100644 index 00000000..a7b06f03 --- /dev/null +++ b/src/temp/player/playerBuild.c @@ -0,0 +1,279 @@ +/**CFile**************************************************************** + + FileName [playerBuild.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLA decomposition package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: playerBuild.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld ); +static Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Esop_Cube_t * pCube, Vec_Int_t * vSupp ); +static Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 ); +static int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Constructs the AIG manager (IVY) for the network after mapping.] + + Description [Uses extended node types (multi-input AND, multi-input EXOR, LUT).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Pla_ManToAig( Ivy_Man_t * pOld ) +{ + Ivy_Man_t * pNew; + Ivy_Obj_t * pObjOld, * pObjNew; + int i; + // start the new manager + pNew = Ivy_ManStart( Ivy_ManPiNum(pOld), Ivy_ManPoNum(pOld), 2*Ivy_ManNodeNum(pOld) + 10 ); + pNew->fExtended = 1; + // transfer the const/PI numbers + Ivy_ManCleanTravId(pOld); + Ivy_ManConst1(pOld)->TravId = Ivy_ManConst1(pNew)->Id; + Ivy_ManForEachPi( pOld, pObjOld, i ) + pObjOld->TravId = Ivy_ManPi(pNew, i)->Id; + // recursively construct the network + Ivy_ManForEachPo( pOld, pObjOld, i ) + { + pObjNew = Pla_ManToAig_rec( pNew, Ivy_ObjFanin0(pObjOld) ); + Ivy_ObjStartFanins( Ivy_ManPo(pNew, i), 1 ); + Ivy_ObjAddFanin( Ivy_ManPo(pNew, i), Ivy_FanCreate(pObjNew->Id, Ivy_ObjFaninC0(pObjOld)) ); + } + // compute the LUT functions + Pla_ManToAigLutFuncs( pNew, pOld ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Recursively construct the new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld ) +{ + Pla_Man_t * p = Ivy_ObjMan(pObjOld)->pData; + Vec_Int_t * vSupp; + Esop_Cube_t * pCover, * pCube; + Ivy_Obj_t * pFaninOld, * pFaninNew, * pObjNew; + Pla_Obj_t * pStr; + int Entry, nCubes, ObjNewId, i; + // skip the node if it is a constant or already processed + if ( Ivy_ObjIsConst1(pObjOld) || pObjOld->TravId ) + return Ivy_ManObj( pNew, pObjOld->TravId ); + assert( Ivy_ObjIsAnd(pObjOld) || Ivy_ObjIsExor(pObjOld) ); + // get the support and the cover + pStr = Ivy_ObjPlaStr( pObjOld ); + if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax ) + { + vSupp = &pStr->vSupp[0]; + pCover = PLA_EMPTY; + } + else + { + vSupp = &pStr->vSupp[1]; + pCover = pStr->pCover[1]; + assert( pCover != PLA_EMPTY ); + } + // process the fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + Pla_ManToAig_rec( pNew, Ivy_ObjObj(pObjOld, Entry) ); + // consider the case of a LUT + if ( pCover == PLA_EMPTY ) + { + pObjNew = Ivy_ObjCreateExt( pNew, IVY_LUT ); + Ivy_ObjStartFanins( pObjNew, p->nLutMax ); + // remember new object ID in case it changes + ObjNewId = pObjNew->Id; + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFaninOld = Ivy_ObjObj( pObjOld, Entry ); + Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_FanCreate(pFaninOld->TravId, 0) ); + } + // get the new object + pObjNew = Ivy_ManObj(pNew, ObjNewId); + } + else + { + // for each cube, construct the node + nCubes = Esop_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pObjNew = Ivy_ManToAigConst( pNew, 0 ); + else if ( nCubes == 1 ) + pObjNew = Ivy_ManToAigCube( pNew, pObjOld, pCover, vSupp ); + else + { + pObjNew = Ivy_ObjCreateExt( pNew, IVY_EXORM ); + Ivy_ObjStartFanins( pObjNew, p->nLutMax ); + // remember new object ID in case it changes + ObjNewId = pObjNew->Id; + Esop_CoverForEachCube( pCover, pCube ) + { + pFaninNew = Ivy_ManToAigCube( pNew, pObjOld, pCube, vSupp ); + Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_FanCreate(pFaninNew->Id, 0) ); + } + // get the new object + pObjNew = Ivy_ManObj(pNew, ObjNewId); + } + } + pObjOld->TravId = pObjNew->Id; + pObjNew->TravId = pObjOld->Id; + return pObjNew; +} + + +/**Function************************************************************* + + Synopsis [Returns constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 ) +{ + Ivy_Obj_t * pObjNew; + pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM ); + Ivy_ObjStartFanins( pObjNew, 1 ); + Ivy_ObjAddFanin( pObjNew, Ivy_FanCreate(0, !fConst1) ); + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Esop_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + Ivy_Obj_t * pObjNew, * pFaninOld; + int i, Value; + // if tautology cube, create constant 1 node + if ( pCube->nLits == 0 ) + return Ivy_ManToAigConst( pNew, 1 ); + // create AND node + pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM ); + Ivy_ObjStartFanins( pObjNew, pCube->nLits ); + // add fanins + for ( i = 0; i < (int)pCube->nVars; i++ ) + { + Value = Esop_CubeGetVar( pCube, i ); + assert( Value != 0 ); + if ( Value == 3 ) + continue; + pFaninOld = Ivy_ObjObj( pObjOld, Vec_IntEntry(vSupp, i) ); + Ivy_ObjAddFanin( pObjNew, Ivy_FanCreate( pFaninOld->TravId, Value==1 ) ); + } + assert( Ivy_ObjFaninNum(pObjNew) == (int)pCube->nLits ); + return pObjNew; +} + + +/**Function************************************************************* + + Synopsis [Recursively construct the new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ) +{ + Vec_Int_t * vSupp, * vFanins, * vNodes, * vTemp; + Ivy_Obj_t * pObjOld, * pObjNew; + unsigned * pComputed, * pTruth; + int i, k, Counter = 0; + // create mapping from the LUT nodes into truth table indices + assert( pNew->vTruths == NULL ); + vNodes = Vec_IntAlloc( 100 ); + vTemp = Vec_IntAlloc( 100 ); + pNew->vTruths = Vec_IntStart( Ivy_ManObjIdNext(pNew) ); + Ivy_ManForEachObj( pNew, pObjNew, i ) + { + if ( Ivy_ObjIsLut(pObjNew) ) + Vec_IntWriteEntry( pNew->vTruths, i, 8 * Counter++ ); + else + Vec_IntWriteEntry( pNew->vTruths, i, -1 ); + } + // allocate memory + pNew->pMemory = ALLOC( unsigned, 8 * Counter ); + memset( pNew->pMemory, 0, sizeof(unsigned) * 8 * Counter ); + // derive truth tables + Ivy_ManForEachObj( pNew, pObjNew, i ) + { + if ( !Ivy_ObjIsLut(pObjNew) ) + continue; + pObjOld = Ivy_ManObj( pOld, pObjNew->TravId ); + vSupp = Ivy_ObjPlaStr(pObjOld)->vSupp; + assert( Vec_IntSize(vSupp) <= 8 ); + pTruth = Ivy_ObjGetTruth( pObjNew ); + pComputed = Ivy_ManCutTruth( pObjOld, vSupp, vNodes, vTemp ); + // check if the truth table is constant 0 + for ( k = 0; k < 8; k++ ) + if ( pComputed[k] ) + break; + if ( k == 8 ) + { + // create inverter + for ( k = 0; k < 8; k++ ) + pComputed[k] = 0x55555555; + // point it to the constant 1 node + vFanins = Ivy_ObjGetFanins( pObjNew ); + Vec_IntClear( vFanins ); + Vec_IntPush( vFanins, Ivy_FanCreate(0, 1) ); + } + memcpy( pTruth, pComputed, sizeof(unsigned) * 8 ); +// Extra_PrintBinary( stdout, pTruth, 16 ); printf( "\n" ); + } + Vec_IntFree( vTemp ); + Vec_IntFree( vNodes ); + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/player/playerCore.c b/src/temp/player/playerCore.c new file mode 100644 index 00000000..3cd3d8a8 --- /dev/null +++ b/src/temp/player/playerCore.c @@ -0,0 +1,381 @@ +/**CFile**************************************************************** + + FileName [playerCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLA decomposition package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: playerCore.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Pla_ManDecomposeInt( Pla_Man_t * p ); +static int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj ); +static void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level, + Vec_Int_t ** pvSuppA, Vec_Int_t ** pvSuppB, Esop_Cube_t ** pvCovA, Esop_Cube_t ** pvCovB ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs decomposition/mapping into PLAs and K-LUTs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose ) +{ + Pla_Man_t * p; + Ivy_Man_t * pAigNew; + p = Pla_ManAlloc( pAig, nLutMax, nPlaMax ); + if ( !Pla_ManDecomposeInt( p ) ) + { + printf( "Decomposition/mapping failed.\n" ); + Pla_ManFree( p ); + return NULL; + } + pAigNew = Pla_ManToAig( pAig ); +// if ( fVerbose ) +// printf( "PLA stats: Both = %6d. Pla = %6d. Lut = %6d. Total = %6d. Deref = %6d.\n", +// p->nNodesBoth, p->nNodesPla, p->nNodesLut, p->nNodes, p->nNodesDeref ); + Pla_ManFree( p ); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [Performs decomposition/mapping into PLAs and K-LUTs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManDecomposeInt( Pla_Man_t * p ) +{ + Ivy_Man_t * pAig = p->pManAig; + Ivy_Obj_t * pObj; + Pla_Obj_t * pStr; + int i; + + // prepare the PI structures + Ivy_ManForEachPi( pAig, pObj, i ) + { + pStr = Ivy_ObjPlaStr( pObj ); + pStr->fFixed = 1; + pStr->Depth = 0; + pStr->nRefs = (unsigned)pObj->nRefs; + pStr->pCover[0] = PLA_EMPTY; + pStr->pCover[1] = PLA_EMPTY; + } + + // assuming DFS ordering of nodes in the manager + Ivy_ManForEachNode( pAig, pObj, i ) + if ( !Pla_ManDecomposeNode(p, pObj) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records decomposition statistics for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Pla_ManCountDecNodes( Pla_Man_t * p, Pla_Obj_t * pStr ) +{ + if ( Vec_IntSize(pStr->vSupp) <= p->nLutMax && pStr->pCover[1] != PLA_EMPTY ) + p->nNodesBoth++; + else if ( Vec_IntSize(pStr->vSupp) <= p->nLutMax ) + p->nNodesLut++; + else if ( pStr->pCover[1] != PLA_EMPTY ) + p->nNodesPla++; +} + +/**Function************************************************************* + + Synopsis [Performs decomposition/mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj ) +{ + Pla_Obj_t * pStr, * pStr0, * pStr1; + Vec_Int_t * vSuppA, * vSuppB, * vSupp0, * vSupp1; + Esop_Cube_t * pCovA, * pCovB; + int nSuppSize1, nSuppSize2; + + assert( pObj->nRefs > 0 ); + p->nNodes++; + + // get the structures + pStr = Ivy_ObjPlaStr( pObj ); + pStr0 = Ivy_ObjPlaStr( Ivy_ObjFanin0( pObj ) ); + pStr1 = Ivy_ObjPlaStr( Ivy_ObjFanin1( pObj ) ); + vSupp0 = &pStr->vSupp[0]; + vSupp1 = &pStr->vSupp[1]; + pStr->pCover[0] = PLA_EMPTY; + pStr->pCover[1] = PLA_EMPTY; + + // process level 1 + Pla_NodeGetSuppsAndCovers( p, pObj, 1, &vSuppA, &vSuppB, &pCovA, &pCovB ); + nSuppSize1 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp0 ); + if ( nSuppSize1 > p->nPlaMax || pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) + pStr->pCover[0] = PLA_EMPTY; + else if ( Ivy_ObjIsAnd(pObj) ) + pStr->pCover[0] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize1, 1 ); + else + pStr->pCover[0] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize1, 1 ); + + // process level 2 + if ( PLA_MAX(pStr0->Depth, pStr1->Depth) > 1 ) + { + Pla_NodeGetSuppsAndCovers( p, pObj, 2, &vSuppA, &vSuppB, &pCovA, &pCovB ); + nSuppSize2 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp1 ); + if ( nSuppSize2 > p->nPlaMax || pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) + pStr->pCover[1] = PLA_EMPTY; + else if ( Ivy_ObjIsAnd(pObj) ) + pStr->pCover[1] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize2, 1 ); + else + pStr->pCover[1] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize2, 1 ); + } + + // determine the level of this node + pStr->nRefs = (unsigned)pObj->nRefs; + pStr->Depth = PLA_MAX( pStr0->Depth, pStr1->Depth ); + pStr->Depth = pStr->Depth? pStr->Depth : 1; + if ( nSuppSize1 > p->nLutMax && pStr->pCover[1] == PLA_EMPTY ) + { + pStr->Depth++; + // free second level + if ( pStr->pCover[1] != PLA_EMPTY ) + Esop_CoverRecycle( p->pManMin, pStr->pCover[1] ); + vSupp1->nCap = 0; + vSupp1->nSize = 0; + FREE( vSupp1->pArray ); + pStr->pCover[1] = PLA_EMPTY; + // move first to second + pStr->vSupp[1] = pStr->vSupp[0]; + pStr->pCover[1] = pStr->pCover[0]; + vSupp0->nCap = 0; + vSupp0->nSize = 0; + vSupp0->pArray = NULL; + pStr->pCover[0] = PLA_EMPTY; + // get zero level + Pla_NodeGetSuppsAndCovers( p, pObj, 0, &vSuppA, &vSuppB, &pCovA, &pCovB ); + nSuppSize2 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp0 ); + assert( nSuppSize2 == 2 ); + if ( pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) + pStr->pCover[0] = PLA_EMPTY; + else if ( Ivy_ObjIsAnd(pObj) ) + pStr->pCover[0] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize2, 0 ); + else + pStr->pCover[0] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize2, 0 ); + // count stats + if ( pStr0->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr0 ); + if ( pStr1->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr1 ); + // mark the nodes + pStr0->fFixed = 1; + pStr1->fFixed = 1; + } + else if ( pStr0->Depth < pStr1->Depth ) + { + if ( pStr0->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr0 ); + pStr0->fFixed = 1; + } + else // if ( pStr0->Depth > pStr1->Depth ) + { + if ( pStr1->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr1 ); + pStr1->fFixed = 1; + } + + // free some of the covers to save memory + assert( pStr0->nRefs > 0 ); + assert( pStr1->nRefs > 0 ); + pStr0->nRefs--; + pStr1->nRefs--; + + if ( pStr0->nRefs == 0 && !pStr0->fFixed ) + Pla_ManFreeStr( p, pStr0 ), p->nNodesDeref++; + if ( pStr1->nRefs == 0 && !pStr1->fFixed ) + Pla_ManFreeStr( p, pStr1 ), p->nNodesDeref++; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns pointers to the support arrays on the given level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level, + Vec_Int_t ** pvSuppA, Vec_Int_t ** pvSuppB, Esop_Cube_t ** pvCovA, Esop_Cube_t ** pvCovB ) +{ + Ivy_Obj_t * pFan0, * pFan1; + Pla_Obj_t * pStr, * pStr0, * pStr1; + Esop_Cube_t * pCovA, * pCovB; + int fCompl0, fCompl1; + assert( Level >= 0 && Level <= 2 ); + // get the complemented attributes + fCompl0 = Ivy_ObjFaninC0( pObj ); + fCompl1 = Ivy_ObjFaninC1( pObj ); + // get the fanins + pFan0 = Ivy_ObjFanin0( pObj ); + pFan1 = Ivy_ObjFanin1( pObj ); + // get the structures + pStr = Ivy_ObjPlaStr( pObj ); + pStr0 = Ivy_ObjPlaStr( pFan0 ); + pStr1 = Ivy_ObjPlaStr( pFan1 ); + // make sure the fanins are processed + assert( Ivy_ObjIsPi(pFan0) || pStr0->Depth > 0 ); + assert( Ivy_ObjIsPi(pFan1) || pStr1->Depth > 0 ); + // prepare the return values depending on the level + Vec_IntWriteEntry( p->vTriv0, 0, pFan0->Id ); + Vec_IntWriteEntry( p->vTriv1, 0, pFan1->Id ); + *pvSuppA = p->vTriv0; + *pvSuppB = p->vTriv1; + pCovA = p->pManMin->pTriv0; + pCovB = p->pManMin->pTriv1; + if ( Level == 1 ) + { + if ( pStr0->Depth == pStr1->Depth ) + { + if ( pStr0->Depth > 0 ) + { + *pvSuppA = &pStr0->vSupp[0]; + *pvSuppB = &pStr1->vSupp[0]; + pCovA = pStr0->pCover[0]; + pCovB = pStr1->pCover[0]; + } + } + else if ( pStr0->Depth < pStr1->Depth ) + { + *pvSuppB = &pStr1->vSupp[0]; + pCovB = pStr1->pCover[0]; + } + else // if ( pStr0->Depth > pStr1->Depth ) + { + *pvSuppA = &pStr0->vSupp[0]; + pCovA = pStr0->pCover[0]; + } + } + else if ( Level == 2 ) + { + if ( pStr0->Depth == pStr1->Depth ) + { + *pvSuppA = &pStr0->vSupp[1]; + *pvSuppB = &pStr1->vSupp[1]; + pCovA = pStr0->pCover[1]; + pCovB = pStr1->pCover[1]; + } + else if ( pStr0->Depth + 1 == pStr1->Depth ) + { + *pvSuppA = &pStr0->vSupp[0]; + *pvSuppB = &pStr1->vSupp[1]; + pCovA = pStr0->pCover[0]; + pCovB = pStr1->pCover[1]; + } + else if ( pStr0->Depth == pStr1->Depth + 1 ) + { + *pvSuppA = &pStr0->vSupp[1]; + *pvSuppB = &pStr1->vSupp[0]; + pCovA = pStr0->pCover[1]; + pCovB = pStr1->pCover[0]; + } + else if ( pStr0->Depth < pStr1->Depth ) + { + *pvSuppB = &pStr1->vSupp[1]; + pCovB = pStr1->pCover[1]; + } + else // if ( pStr0->Depth > pStr1->Depth ) + { + *pvSuppA = &pStr0->vSupp[1]; + pCovA = pStr0->pCover[1]; + } + } + // complement the first if needed + if ( pCovA == PLA_EMPTY || !fCompl0 ) + *pvCovA = pCovA; + else if ( pCovA && pCovA->nLits == 0 ) // topmost one is the tautology cube + *pvCovA = pCovA->pNext; + else + *pvCovA = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCovA; + // complement the second if needed + if ( pCovB == PLA_EMPTY || !fCompl1 ) + *pvCovB = pCovB; + else if ( pCovB && pCovB->nLits == 0 ) // topmost one is the tautology cube + *pvCovB = pCovB->pNext; + else + *pvCovB = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCovB; +} + + +/* + if ( pObj->Id == 1371 ) + { + int k; + printf( "Zero : " ); + for ( k = 0; k < vSuppA->nSize; k++ ) + printf( "%d ", vSuppA->pArray[k] ); + printf( "\n" ); + printf( "One : " ); + for ( k = 0; k < vSuppB->nSize; k++ ) + printf( "%d ", vSuppB->pArray[k] ); + printf( "\n" ); + printf( "Node : " ); + for ( k = 0; k < vSupp0->nSize; k++ ) + printf( "%d ", vSupp0->pArray[k] ); + printf( "\n" ); + printf( "\n" ); + printf( "\n" ); + Esop_CoverWrite( stdout, pCovA ); + printf( "\n" ); + Esop_CoverWrite( stdout, pCovB ); + printf( "\n" ); + } +*/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c new file mode 100644 index 00000000..7f2c0919 --- /dev/null +++ b/src/temp/player/playerMan.c @@ -0,0 +1,125 @@ +/**CFile**************************************************************** + + FileName [playerMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLA decomposition package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: playerMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the PLA/LUT mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax ) +{ + Pla_Man_t * pMan; + assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128) ); + // start the manager + pMan = ALLOC( Pla_Man_t, 1 ); + memset( pMan, 0, sizeof(Pla_Man_t) ); + pMan->nLutMax = nLutMax; + pMan->nPlaMax = nPlaMax; + pMan->nCubesMax = 2 * nPlaMax; // higher limit, later reduced + pMan->pManAig = pAig; + // set up the temporaries + pMan->vComTo0 = Vec_IntAlloc( 2 * nPlaMax ); + pMan->vComTo1 = Vec_IntAlloc( 2 * nPlaMax ); + pMan->vPairs0 = Vec_IntAlloc( nPlaMax ); + pMan->vPairs1 = Vec_IntAlloc( nPlaMax ); + pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); + pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); + // allocate memory for object structures + pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) ); + memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) ); + // create the cube manager + pMan->pManMin = Esop_ManAlloc( nPlaMax ); + // save the resulting manager + assert( pAig->pData == NULL ); + pAig->pData = pMan; + return pMan; +} + +/**Function************************************************************* + + Synopsis [Frees the PLA/LUT mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_ManFree( Pla_Man_t * p ) +{ + Pla_Obj_t * pStr; + int i; + Esop_ManFree( p->pManMin ); + Vec_IntFree( p->vTriv0 ); + Vec_IntFree( p->vTriv1 ); + Vec_IntFree( p->vComTo0 ); + Vec_IntFree( p->vComTo1 ); + Vec_IntFree( p->vPairs0 ); + Vec_IntFree( p->vPairs1 ); + for ( i = 0, pStr = p->pPlaStrs; i < Ivy_ManObjIdNext(p->pManAig); i++, pStr++ ) + FREE( pStr->vSupp[0].pArray ), FREE( pStr->vSupp[1].pArray ); + free( p->pPlaStrs ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Cleans the PLA/LUT structure of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr ) +{ + if ( pStr->pCover[0] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[0] ); + if ( pStr->pCover[1] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[1] ); + if ( pStr->vSupp[0].pArray ) free( pStr->vSupp[0].pArray ); + if ( pStr->vSupp[1].pArray ) free( pStr->vSupp[1].pArray ); + memset( pStr, 0, sizeof(Pla_Obj_t) ); + pStr->pCover[0] = PLA_EMPTY; + pStr->pCover[1] = PLA_EMPTY; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/player/playerUtil.c b/src/temp/player/playerUtil.c new file mode 100644 index 00000000..1b361839 --- /dev/null +++ b/src/temp/player/playerUtil.c @@ -0,0 +1,349 @@ +/**CFile**************************************************************** + + FileName [playerUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLA decomposition package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: playerUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Merges two supports.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManMergeTwoSupports( Pla_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1, Vec_Int_t * vSupp ) +{ + int k0, k1; + + assert( vSupp0->nSize && vSupp1->nSize ); + + Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntClear( p->vPairs0 ); + Vec_IntClear( p->vPairs1 ); + + vSupp->nSize = 0; + vSupp->nCap = vSupp0->nSize + vSupp1->nSize; + vSupp->pArray = ALLOC( int, vSupp->nCap ); + + for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; ) + { + if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( p->vPairs0, k0 ); + Vec_IntPush( p->vPairs1, k1 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; k1++; + } + else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; + } + else + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + k1++; + } + } + for ( ; k0 < vSupp0->nSize; k0++ ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + } + for ( ; k1 < vSupp1->nSize; k1++ ) + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + } +/* + printf( "Zero : " ); + for ( k = 0; k < vSupp0->nSize; k++ ) + printf( "%d ", vSupp0->pArray[k] ); + printf( "\n" ); + + printf( "One : " ); + for ( k = 0; k < vSupp1->nSize; k++ ) + printf( "%d ", vSupp1->pArray[k] ); + printf( "\n" ); + + printf( "Sum : " ); + for ( k = 0; k < vSupp->nSize; k++ ) + printf( "%d ", vSupp->pArray[k] ); + printf( "\n" ); + printf( "\n" ); +*/ + return Vec_IntSize(vSupp); +} + + +/**Function************************************************************* + + Synopsis [Computes the produce of two covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Esop_Cube_t * Pla_ManAndTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ) +{ + Esop_Cube_t * pCube, * pCube0, * pCube1; + Esop_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 != PLA_EMPTY && pCover1 != PLA_EMPTY ); + + // clean storage + assert( nSupp <= p->nPlaMax ); + Esop_ManClean( p->pManMin, nSupp ); + // go through the cube pairs + Esop_CoverForEachCube( pCover0, pCube0 ) + Esop_CoverForEachCube( pCover1, pCube1 ) + { + // go through the support variables of the cubes + for ( i = 0; i < p->vPairs0->nSize; i++ ) + { + Val0 = Esop_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); + Val1 = Esop_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); + if ( (Val0 & Val1) == 0 ) + break; + } + // check disjointness + if ( i < p->vPairs0->nSize ) + continue; + + if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Esop_CoverCollect( p->pManMin, nSupp ); +//Esop_CoverWriteFile( pCover, "large", 1 ); + Esop_CoverRecycle( p->pManMin, pCover ); + return PLA_EMPTY; + } + + // create the product cube + pCube = Esop_CubeAlloc( p->pManMin ); + + // add the literals + pCube->nLits = 0; + for ( i = 0; i < nSupp; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + Val0 = 3; + else + Val0 = Esop_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + + if ( p->vComTo1->pArray[i] == -1 ) + Val1 = 3; + else + Val1 = Esop_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + + if ( (Val0 & Val1) == 3 ) + continue; + + Esop_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); + pCube->nLits++; + } + // add the cube to storage + Esop_EsopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + Esop_EsopMinimize( p->pManMin ); + pCover = Esop_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( fStopAtLimit && Esop_CoverCountCubes(pCover) > p->nPlaMax ) + { + Esop_CoverRecycle( p->pManMin, pCover ); + return PLA_EMPTY; + } +// if ( pCover && pCover->nWords > 4 ) +// printf( "%d", pCover->nWords ); +// else +// printf( "." ); + return pCover; +} + +/**Function************************************************************* + + Synopsis [Computes the EXOR of two covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ) +{ + Esop_Cube_t * pCube, * pCube0, * pCube1; + Esop_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 != PLA_EMPTY && pCover1 != PLA_EMPTY ); + + // clean storage + assert( nSupp <= p->nPlaMax ); + Esop_ManClean( p->pManMin, nSupp ); + Esop_CoverForEachCube( pCover0, pCube0 ) + { + // create the cube + pCube = Esop_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo0->nSize; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + continue; + Val0 = Esop_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + if ( Val0 == 3 ) + continue; + Esop_CubeXorVar( pCube, i, Val0 ^ 3 ); + pCube->nLits++; + } + if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Esop_CoverCollect( p->pManMin, nSupp ); + Esop_CoverRecycle( p->pManMin, pCover ); + return PLA_EMPTY; + } + // add the cube to storage + Esop_EsopAddCube( p->pManMin, pCube ); + } + Esop_CoverForEachCube( pCover1, pCube1 ) + { + // create the cube + pCube = Esop_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo1->nSize; i++ ) + { + if ( p->vComTo1->pArray[i] == -1 ) + continue; + Val1 = Esop_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + if ( Val1 == 3 ) + continue; + Esop_CubeXorVar( pCube, i, Val1 ^ 3 ); + pCube->nLits++; + } + if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Esop_CoverCollect( p->pManMin, nSupp ); + Esop_CoverRecycle( p->pManMin, pCover ); + return PLA_EMPTY; + } + // add the cube to storage + Esop_EsopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + Esop_EsopMinimize( p->pManMin ); + pCover = Esop_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( fStopAtLimit && Esop_CoverCountCubes(pCover) > p->nPlaMax ) + { + Esop_CoverRecycle( p->pManMin, pCover ); + return PLA_EMPTY; + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [Computes area/delay of the mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_ManComputeStats( Ivy_Man_t * p, Vec_Int_t * vNodes ) +{ + Ivy_Obj_t * pObj, * pFanin; + Vec_Int_t * vFanins; + int Area, Delay, Fanin, nFanins, i, k; + + Delay = Area = 0; + // compute levels and area + Ivy_ManForEachPi( p, pObj, i ) + pObj->Level = 0; + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + { + // compute level of the node + pObj->Level = 0; + vFanins = Ivy_ObjGetFanins( pObj ); + Vec_IntForEachEntry( vFanins, Fanin, k ) + { + pFanin = Ivy_ManObj(p, Ivy_FanId(Fanin)); + pObj->Level = IVY_MAX( pObj->Level, pFanin->Level ); + } + pObj->Level += 1; + // compute area of the node + nFanins = Ivy_ObjFaninNum( pObj ); + if ( nFanins <= 4 ) + Area += 1; + else if ( nFanins <= 6 ) + Area += 2; + else if ( nFanins <= 8 ) + Area += 4; + else if ( nFanins <= 16 ) + Area += 8; + else if ( nFanins <= 32 ) + Area += 16; + else if ( nFanins <= 64 ) + Area += 32; + else if ( nFanins <= 128 ) + Area += 64; + else + assert( 0 ); + } + Ivy_ManForEachPo( p, pObj, i ) + { + Fanin = Ivy_ObjReadFanin(pObj, 0); + pFanin = Ivy_ManObj( p, Ivy_FanId(Fanin) ); + pObj->Level = pFanin->Level; + Delay = IVY_MAX( Delay, (int)pObj->Level ); + } + printf( "Area = %d. Delay = %d.\n", Area, Delay ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |