summaryrefslogtreecommitdiffstats
path: root/src/temp
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp')
-rw-r--r--src/temp/aig-alan.tar.gzbin27265 -> 0 bytes
-rw-r--r--src/temp/esop/esop.h723
-rw-r--r--src/temp/esop/esopMan.c117
-rw-r--r--src/temp/esop/esopMin.c299
-rw-r--r--src/temp/esop/esopUtil.c277
-rw-r--r--src/temp/esop/module.make3
-rw-r--r--src/temp/ivy/ivy.h1
-rw-r--r--src/temp/ivy/ivyFraig.c131
-rw-r--r--src/temp/ivy/ivyMan.c5
-rw-r--r--src/temp/player/module.make4
-rw-r--r--src/temp/player/player.h113
-rw-r--r--src/temp/player/playerAbc.c228
-rw-r--r--src/temp/player/playerBuild.c283
-rw-r--r--src/temp/player/playerCore.c376
-rw-r--r--src/temp/player/playerMan.c125
-rw-r--r--src/temp/player/playerToAbc.c523
-rw-r--r--src/temp/player/playerUtil.c353
17 files changed, 106 insertions, 3455 deletions
diff --git a/src/temp/aig-alan.tar.gz b/src/temp/aig-alan.tar.gz
deleted file mode 100644
index b61827ad..00000000
--- a/src/temp/aig-alan.tar.gz
+++ /dev/null
Binary files differ
diff --git a/src/temp/esop/esop.h b/src/temp/esop/esop.h
deleted file mode 100644
index 5f95f371..00000000
--- a/src/temp/esop/esop.h
+++ /dev/null
@@ -1,723 +0,0 @@
-/**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"
-#include "mem.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Esop_Man_t_ Esop_Man_t;
-typedef struct Esop_Cube_t_ Esop_Cube_t;
-typedef struct Mem_Fixed_t_ Mem_Fixed_t;
-
-struct Esop_Man_t_
-{
- int nVars; // the number of vars
- int nWords; // the number of words
- Mem_Fixed_t * pMemMan1; // memory manager for cubes
- Mem_Fixed_t * pMemMan2; // memory manager for cubes
- Mem_Fixed_t * pMemMan4; // memory manager for cubes
- Mem_Fixed_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 Mem_Fixed_t * Mem_FixedStart( int nEntrySize );
-extern void Mem_FixedStop( Mem_Fixed_t * p, int fVerbose );
-extern char * Mem_FixedEntryFetch( Mem_Fixed_t * p );
-extern void Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry );
-extern void Mem_FixedRestart( Mem_Fixed_t * p );
-extern int Mem_FixedReadMemUsage( Mem_Fixed_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 *)Mem_FixedEntryFetch( p->pMemMan1 );
- else if ( p->nWords <= 2 )
- pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan2 );
- else if ( p->nWords <= 4 )
- pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan4 );
- else if ( p->nWords <= 8 )
- pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( 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 )
- Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube );
- else if ( pCube->nWords <= 2 )
- Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube );
- else if ( pCube->nWords <= 4 )
- Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube );
- else if ( pCube->nWords <= 8 )
- Mem_FixedEntryRecycle( 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 )
- Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube );
- else if ( pCover->nWords <= 2 )
- Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube );
- else if ( pCover->nWords <= 4 )
- Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube );
- else if ( pCover->nWords <= 8 )
- Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- Mem_FixedEntryRecycle( 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
deleted file mode 100644
index 5c411349..00000000
--- a/src/temp/esop/esopMan.c
+++ /dev/null
@@ -1,117 +0,0 @@
-/**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 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) );
- pMan->pMemMan2 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) );
- pMan->pMemMan4 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) );
- pMan->pMemMan8 = Mem_FixedStart( 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 )
-{
- Mem_FixedStop ( p->pMemMan1, 0 );
- Mem_FixedStop ( p->pMemMan2, 0 );
- Mem_FixedStop ( p->pMemMan4, 0 );
- Mem_FixedStop ( p->pMemMan8, 0 );
- free( p->ppStore );
- free( p );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/esop/esopMin.c b/src/temp/esop/esopMin.c
deleted file mode 100644
index 7a460f8e..00000000
--- a/src/temp/esop/esopMin.c
+++ /dev/null
@@ -1,299 +0,0 @@
-/**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
deleted file mode 100644
index 7230cc87..00000000
--- a/src/temp/esop/esopUtil.c
+++ /dev/null
@@ -1,277 +0,0 @@
-/**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\n", fEsop? "ESOP":"SOP", pName );
- 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
deleted file mode 100644
index 1003ccc1..00000000
--- a/src/temp/esop/module.make
+++ /dev/null
@@ -1,3 +0,0 @@
-SRC += src/temp/esop/esopMan.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
index eb5f50e4..a8c8b289 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -136,6 +136,7 @@ struct Ivy_FraigParams_t_
double dActConeBumpMax; // the largest bump in activity
int fProve; // prove the miter outputs
int fVerbose; // verbose output
+ int fDoSparse; // skip sparse functions
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
int nBTLimitGlobal; // conflict limit global
diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c
index 694d5a30..209ff8e7 100644
--- a/src/temp/ivy/ivyFraig.c
+++ b/src/temp/ivy/ivyFraig.c
@@ -216,6 +216,7 @@ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pParams->fPatScores = 0; // enables simulation pattern scoring
pParams->MaxScore = 25; // max score after which resimulation is used
+ pParams->fDoSparse = 1; // skips sparse functions
// pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pParams->dActConeBumpMax = 5.0; // the largest bump of activity
pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped
@@ -1227,6 +1228,69 @@ int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
return RetValue + 1;
}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the counter-example from the successful pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i, k, BestPat, * pModel;
+ // find the word of the pattern
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims->pData[i] )
+ break;
+ assert( i < p->nSimWords );
+ // find the bit of the pattern
+ for ( k = 0; k < 32; k++ )
+ if ( pSims->pData[i] & (1 << k) )
+ break;
+ assert( k < 32 );
+ // determine the best pattern
+ BestPat = i * 32 + k;
+ // fill in the counter-example data
+ pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
+ // set the model
+ assert( p->pManFraig->pData == NULL );
+ p->pManFraig->pData = pModel;
+ return;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the one of the output is already non-constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
+ {
+ // create the counter-example from this pattern
+ Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
+ return 1;
+ }
+ return 0;
+}
/**Function*************************************************************
@@ -1244,6 +1308,13 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass, * pClass2;
int clk, RetValue, Counter = 0;
+ // check if some outputs already became non-constant
+ // this is a special case when computation can be stopped!!!
+ if ( p->pParams->fProve )
+ Ivy_FraigCheckOutputSims( p );
+ if ( p->pManFraig->pData )
+ return 0;
+ // refine the classed
clk = clock();
Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
{
@@ -1447,27 +1518,6 @@ void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
/**Function*************************************************************
- Synopsis [Returns 1 if the one of the output is already non-constant 0.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
-{
- Ivy_Obj_t * pObj;
- int i;
- Ivy_ManForEachPo( p->pManAig, pObj, i )
- if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
- return 1;
- return 0;
-}
-
-/**Function*************************************************************
-
Synopsis [Performs simulation of the manager.]
Description []
@@ -1490,11 +1540,15 @@ void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
Ivy_FraigSavePattern1( p );
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
// refine classes by random simulation
do {
@@ -1502,13 +1556,11 @@ void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
Ivy_FraigSimulateOne( p );
nClasses = p->lClasses.nItems;
nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
// Ivy_FraigPrintSimClasses( p );
-
- // check if some outputs already became non-constant
-// if ( Ivy_FraigCheckOutputSims(p) )
-// printf( "Special case: One of the POs is already non-const zero.\n" );
}
@@ -1620,6 +1672,8 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
if ( p->pParams->fPatScores )
Ivy_FraigCleanPatScores( p );
nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
if ( nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
@@ -1635,6 +1689,8 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
Ivy_FraigSimulateOne( p );
Ivy_FraigCleanPatScores( p );
nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
if ( nChanges == 0 )
break;
@@ -1765,6 +1821,14 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
break;
}
+/*
+ // check the representative of this node
+ pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
+ if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
+ printf( "Representative is not constant 1.\n" );
+ else
+ printf( "Representative is constant 1.\n" );
+*/
// try to prove the output constant 0
RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
if ( RetValue == 1 ) // proved equivalent
@@ -1816,7 +1880,11 @@ p->nClassesBeg = p->lClasses.nItems;
Ivy_ManForEachNode( p->pManAig, pObj, i )
{
Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
- pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+ // default to simple strashing if simulation detected a counter-example for a PO
+ if ( p->pManFraig->pData )
+ pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ else
+ pObj->pEquiv = Ivy_FraigAnd( p, pObj );
assert( pObj->pEquiv != NULL );
// pTemp = Ivy_Regular(pObj->pEquiv);
// assert( Ivy_Regular(pObj->pEquiv)->Type );
@@ -1826,7 +1894,7 @@ p->nClassesEnd = p->lClasses.nItems;
// try to prove the outputs of the miter
p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
// Ivy_FraigMiterStatus( p->pManFraig );
- if ( p->pParams->fProve )
+ if ( p->pParams->fProve && p->pManFraig->pData == NULL )
Ivy_FraigMiterProve( p );
// add the POs
Ivy_ManForEachPo( p->pManAig, pObj, i )
@@ -1860,7 +1928,7 @@ p->nClassesEnd = p->lClasses.nItems;
***********************************************************************/
Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
-{
+{
Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
int RetValue;
// get the fraiged fanins
@@ -1869,8 +1937,13 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
// get the candidate fraig node
pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
// get representative of this class
- if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL ) // this is a unique node
+ if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
+ (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
{
+// if ( Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1 )
+// {
+// int x = 0;
+// }
assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
assert( pObjNew != Ivy_Regular(pFanin0New) );
assert( pObjNew != Ivy_Regular(pFanin1New) );
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 8099b834..ac58cb61 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch )
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{
Ivy_Obj_t * pNode;
- int LimitFactor = 100;
+ int LimitFactor = 5;
int NodeBeg = Ivy_ManNodeNum(p);
int nSteps;
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
@@ -430,7 +430,8 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
if ( nSteps > NodeBeg * LimitFactor )
{
- printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor );
+ printf( "Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor );
+ printf( "This circuit cannot be forward-retimed completely. Quitting.\n" );
break;
}
}
diff --git a/src/temp/player/module.make b/src/temp/player/module.make
deleted file mode 100644
index 5185f56e..00000000
--- a/src/temp/player/module.make
+++ /dev/null
@@ -1,4 +0,0 @@
-SRC += src/temp/player/playerToAbc.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
deleted file mode 100644
index a4ee5650..00000000
--- a/src/temp/player/player.h
+++ /dev/null
@@ -1,113 +0,0 @@
-/**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 : 31; // the depth in terms of LUTs/PLAs
- int nRefs; // 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_Man_t * p, Ivy_Obj_t * pObj ) { return (Pla_Man_t *)p->pData; }
-static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return ((Pla_Man_t *)p->pData)->pPlaStrs + pObj->Id; }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== playerToAbc.c ==============================================================*/
-extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
-/*=== playerCore.c =============================================================*/
-extern Pla_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
deleted file mode 100644
index dcbca462..00000000
--- a/src/temp/player/playerAbc.c
+++ /dev/null
@@ -1,228 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
-#if 0
-
-/**Function*************************************************************
-
- Synopsis [Gives the current ABC network to PLAyer for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
-{
- int fUseRewriting = 1;
- 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 );
- if ( fUseRewriting )
- {
- // simplify
- pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
- Ivy_ManStop( pManExt );
- 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_AigConst1(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_AigConst1(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_EdgeId(Fanin) );
- pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId );
- Abc_ObjAddFanin( pObjNew, pFaninNew );
- pCompls[k] = Ivy_EdgeIsComplement(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_EdgeId(Fanin) );
- // get the new ABC node corresponding to the old fanin
- pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId );
- if ( Ivy_EdgeIsComplement(Fanin) ) // complement
- {
-// pFaninNew = Abc_NtkCreateNodeInv(pNtkNew, pFaninNew);
- if ( Abc_ObjIsCi(pFaninNew) )
- pFaninNew = Abc_NtkCreateNodeInv(pNtkNew, pFaninNew);
- else
- {
- // clone the node
- pObjNew = Abc_NtkCloneObj( 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;
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/player/playerBuild.c b/src/temp/player/playerBuild.c
deleted file mode 100644
index e878f19c..00000000
--- a/src/temp/player/playerBuild.c
+++ /dev/null
@@ -1,283 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
-#if 0
-
-/**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_EdgeCreate(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( pNew, 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_EdgeCreate(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_EdgeCreate(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_EdgeCreate(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_EdgeCreate( 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(pNew, pObjOld)->vSupp;
- assert( Vec_IntSize(vSupp) <= 8 );
- pTruth = Ivy_ObjGetTruth( pObjNew );
- pComputed = Ivy_ManCutTruth( pNew, 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_EdgeCreate(0, 1) );
- }
- memcpy( pTruth, pComputed, sizeof(unsigned) * 8 );
-// Extra_PrintBinary( stdout, pTruth, 16 ); printf( "\n" );
- }
- Vec_IntFree( vTemp );
- Vec_IntFree( vNodes );
- return Counter;
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/player/playerCore.c b/src/temp/player/playerCore.c
deleted file mode 100644
index b87f39d4..00000000
--- a/src/temp/player/playerCore.c
+++ /dev/null
@@ -1,376 +0,0 @@
-/**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 []
-
-***********************************************************************/
-Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose )
-{
- Pla_Man_t * p;
- p = Pla_ManAlloc( pAig, nLutMax, nPlaMax );
- if ( !Pla_ManDecomposeInt( p ) )
- {
- printf( "Decomposition/mapping failed.\n" );
- Pla_ManFree( p );
- return NULL;
- }
- return p;
-}
-
-/**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( pAig, 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( p->pManAig, pObj );
- pStr0 = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin0( pObj ) );
- pStr1 = Ivy_ObjPlaStr( p->pManAig, 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;
- }
- assert( pStr->Depth );
-
- // 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( p->pManAig, pObj );
- pStr0 = Ivy_ObjPlaStr( p->pManAig, pFan0 );
- pStr1 = Ivy_ObjPlaStr( p->pManAig, 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
deleted file mode 100644
index 32eacc9b..00000000
--- a/src/temp/player/playerMan.c
+++ /dev/null
@@ -1,125 +0,0 @@
-/**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, Ivy_ManObjIdMax(pAig)+1 );
- memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) );
- // 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_ManObjIdMax(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/playerToAbc.c b/src/temp/player/playerToAbc.c
deleted file mode 100644
index 81032826..00000000
--- a/src/temp/player/playerToAbc.c
+++ /dev/null
@@ -1,523 +0,0 @@
-/**CFile****************************************************************
-
- FileName [playerToAbc.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: playerToAbc.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 * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode );
-static Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp );
-static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp );
-static Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp );
-static int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose );
-
-static inline void Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) { assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc ); }
-static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) { return Vec_PtrEntry( p->pCopy, IvyId ); }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Applies PLA/LUT mapping to the ABC network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose )
-{
- Pla_Man_t * p;
- Ivy_Man_t * pMan, * pManExt;
- Abc_Ntk_t * pNtkNew;
- 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 );
- if ( fRewriting )
- {
- // simplify
- pMan = Ivy_ManResyn0( pManExt = pMan, 1, 0 );
- Ivy_ManStop( pManExt );
- if ( fVerbose )
- Ivy_ManPrintStats( pMan );
- }
- if ( fSynthesis )
- {
- // simplify
- pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
- Ivy_ManStop( pManExt );
- if ( fVerbose )
- Ivy_ManPrintStats( pMan );
- }
- // perform decomposition
- if ( fFastMode )
- {
- // perform mapping into LUTs
- Ivy_FastMapPerform( pMan, nLutMax, 1, fVerbose );
- // convert from the extended AIG manager into an SOP network
- pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode );
-// pNtkNew = NULL;
- Ivy_FastMapStop( pMan );
- }
- else
- {
- assert( nLutMax >= 2 && nLutMax <= 8 );
- // perform decomposition/mapping into PLAs/LUTs
- p = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose );
- // convert from the extended AIG manager into an SOP network
- pNtkNew = Ivy_ManToAbc( pNtk, pMan, p, fFastMode );
- Pla_ManFree( p );
- }
- Ivy_ManStop( pMan );
- // chech the resulting network
- if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
- {
- printf( "Abc_NtkPlayer: The network check has failed.\n" );
- Abc_NtkDelete( pNtkNew );
- return NULL;
- }
-// Abc_NtkPlayerCost( pNtkNew, RankCost, fVerbose );
- return pNtkNew;
-}
-
-/**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();
- // create the PIs
- Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
- Abc_NtkForEachCi( pNtk, pObj, i )
- pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan);
- // perform the conversion of the internal nodes
- Abc_AigForEachAnd( pNtk, pObj, i )
- pObj->pCopy = (Abc_Obj_t *)Ivy_And( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) );
- // create the POs
- Abc_NtkForEachCo( pNtk, pObj, i )
- Ivy_ObjCreatePo( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) );
- Ivy_ManCleanup( pMan );
- return pMan;
-}
-
-/**Function*************************************************************
-
- Synopsis [Constructs the ABC network after mapping.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode )
-{
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObjAbc, * pObj;
- Ivy_Obj_t * pObjIvy;
- Vec_Int_t * vNodes, * vTemp;
- int i;
- // start mapping from Ivy into Abc
- pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 );
- // start the new ABC network
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
- // transfer the pointers to the basic nodes
- Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) );
- Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
- Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc );
- // recursively construct the network
- vNodes = Vec_IntAlloc( 100 );
- vTemp = Vec_IntAlloc( 100 );
- Ivy_ManForEachPo( pMan, pObjIvy, i )
- {
- // get the new ABC node corresponding to the old fanin of the PO in IVY
- if ( fFastMode )
- pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp );
- else
- pObjAbc = Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp );
- // consider the case of complemented fanin of the PO
- if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
- {
- if ( Abc_ObjIsCi(pObjAbc) )
- pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc );
- else
- {
- // clone the node
- pObj = Abc_NtkCloneObj( pObjAbc );
- // set complemented functions
- pObj->pData = Abc_SopRegister( pNtkNew->pManFunc, pObjAbc->pData );
- Abc_SopComplement(pObj->pData);
- // return the new node
- pObjAbc = pObj;
- }
- assert( Abc_SopGetVarNum(pObjAbc->pData) == Abc_ObjFaninNum(pObjAbc) );
- }
- Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc );
- }
- Vec_IntFree( vTemp );
- Vec_IntFree( vNodes );
- Vec_PtrFree( pMan->pCopy );
- pMan->pCopy = NULL;
- // remove dangling nodes
-// Abc_NtkForEachNode( pNtkNew, pObjAbc, i )
-// if ( Abc_ObjFanoutNum(pObjAbc) == 0 )
-// Abc_NtkDeleteObj(pObjAbc);
- Abc_NtkCleanup( pNtkNew, 0 );
- // fix CIs feeding directly into COs
- Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
- return pNtkNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Recursively construct the new node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp )
-{
- Vec_Int_t * vSupp;
- Esop_Cube_t * pCover, * pCube;
- Abc_Obj_t * pObjAbc, * pFaninAbc;
- Pla_Obj_t * pStr;
- int Entry, nCubes, i;
- unsigned * puTruth;
- // skip the node if it is a constant or already processed
- pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
- if ( pObjAbc )
- return pObjAbc;
- assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
- // get the support and the cover
- pStr = Ivy_ObjPlaStr( pMan, pObjIvy );
- 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 );
- }
- // create new node and its fanins
- Vec_IntForEachEntry( vSupp, Entry, i )
- Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ManObj(pMan, Entry), vNodes, vTemp );
- // consider the case of a LUT
- if ( pCover == PLA_EMPTY )
- {
- pObjAbc = Abc_NtkCreateNode( pNtkNew );
- Vec_IntForEachEntry( vSupp, Entry, i )
- Abc_ObjAddFanin( pObjAbc, Abc_ObjGetIvy2Abc(pMan, Entry) );
- // check if the truth table is constant 0
- puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp );
- // if the function is constant 0, create constant 0 node
- if ( Extra_TruthIsConst0(puTruth, 8) )
- {
- pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
- pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew );
- }
- else if ( Extra_TruthIsConst1(puTruth, 8) )
- {
- pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
- pObjAbc = Abc_NtkCreateNodeConst1( pNtkNew );
- }
- else
- {
- int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
- if ( vNodes->nSize == -1 )
- printf( "Ivy_ManToAbc_rec(): Internal error.\n" );
- pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
- if ( fCompl ) Abc_SopComplement(pObjAbc->pData);
-// printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) );
-// pObjAbc->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, Vec_IntSize(vSupp), puTruth );
- }
- }
- else
- {
- // for each cube, construct the node
- nCubes = Esop_CoverCountCubes( pCover );
- if ( nCubes == 0 )
- pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew );
- else if ( nCubes == 1 )
- pObjAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCover, vSupp );
- else
- {
- pObjAbc = Abc_NtkCreateNode( pNtkNew );
- Esop_CoverForEachCube( pCover, pCube )
- {
- pFaninAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCube, vSupp );
- Abc_ObjAddFanin( pObjAbc, pFaninAbc );
- }
- pObjAbc->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc) );
- }
- }
- Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc );
- return pObjAbc;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp )
-{
- int pCompls[PLAYER_FANIN_LIMIT];
- Abc_Obj_t * pObjAbc, * pFaninAbc;
- int i, k, Value;
- // if tautology cube, create constant 1 node
- if ( pCube->nLits == 0 )
- return Abc_NtkCreateNodeConst1(pNtkNew);
- // create AND node
- pObjAbc = Abc_NtkCreateNode( pNtkNew );
- for ( i = k = 0; i < (int)pCube->nVars; i++ )
- {
- Value = Esop_CubeGetVar( pCube, i );
- assert( Value != 0 );
- if ( Value == 3 )
- continue;
- pFaninAbc = Abc_ObjGetIvy2Abc( pMan, Vec_IntEntry(vSupp, i) );
- pFaninAbc = Abc_ObjNotCond( pFaninAbc, Value==1 );
- Abc_ObjAddFanin( pObjAbc, Abc_ObjRegular(pFaninAbc) );
- pCompls[k++] = Abc_ObjIsComplement(pFaninAbc);
- }
- pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc), pCompls );
- assert( Abc_ObjFaninNum(pObjAbc) == (int)pCube->nLits );
- return pObjAbc;
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Recursively construct the new node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp )
-{
- Vec_Int_t Supp, * vSupp = &Supp;
- Abc_Obj_t * pObjAbc, * pFaninAbc;
- int i, Entry;
- unsigned * puTruth;
- // skip the node if it is a constant or already processed
- pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
- if ( pObjAbc )
- return pObjAbc;
- assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
- // get the support of K-LUT
- Ivy_FastMapReadSupp( pMan, pObjIvy, vSupp );
- // create new ABC node and its fanins
- pObjAbc = Abc_NtkCreateNode( pNtkNew );
- Vec_IntForEachEntry( vSupp, Entry, i )
- {
- pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes, vTemp );
- Abc_ObjAddFanin( pObjAbc, pFaninAbc );
- }
- // check if the truth table is constant 0
- puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp );
- // if the function is constant 0, create constant 0 node
- if ( Extra_TruthIsConst0(puTruth, 8) )
- {
- pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
- pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew );
- }
- else if ( Extra_TruthIsConst1(puTruth, 8) )
- {
- pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
- pObjAbc = Abc_NtkCreateNodeConst1( pNtkNew );
- }
- else
- {
- int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
- if ( vNodes->nSize == -1 )
- printf( "Ivy_ManToAbcFast_rec(): Internal error.\n" );
- pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
- if ( fCompl ) Abc_SopComplement(pObjAbc->pData);
- }
- Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc );
- return pObjAbc;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Computes cost of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Abc_NodePlayerCost( int nFanins )
-{
- if ( nFanins <= 4 )
- return 1;
- if ( nFanins <= 6 )
- return 2;
- if ( nFanins <= 8 )
- return 4;
- if ( nFanins <= 16 )
- return 8;
- if ( nFanins <= 32 )
- return 16;
- if ( nFanins <= 64 )
- return 32;
- if ( nFanins <= 128 )
- return 64;
- assert( 0 );
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the number of ranks needed for one level.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Abc_NtkPlayerCostOneLevel( int nCost, int RankCost )
-{
- return (nCost / RankCost) + ((nCost % RankCost) > 0);
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes the cost function for the network (number of ranks).]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
-{
- Abc_Obj_t * pObj;
- int * pLevelCosts, * pLevelCostsR;
- int Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR;
- int nFanins, nLevels, LevelR, i;
- // compute the reverse levels
- Abc_NtkStartReverseLevels( pNtk );
- // compute the costs for each level
- nLevels = Abc_NtkGetLevelNum( pNtk );
- pLevelCosts = ALLOC( int, nLevels + 1 );
- pLevelCostsR = ALLOC( int, nLevels + 1 );
- memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) );
- memset( pLevelCostsR, 0, sizeof(int) * (nLevels + 1) );
- Abc_NtkForEachNode( pNtk, pObj, i )
- {
- nFanins = Abc_ObjFaninNum(pObj);
- if ( nFanins == 0 )
- continue;
- Cost = Abc_NodePlayerCost( nFanins );
- LevelR = Vec_IntEntry( pNtk->vLevelsR, pObj->Id );
- pLevelCosts[ pObj->Level ] += Cost;
- pLevelCostsR[ LevelR ] += Cost;
- }
- // compute the total cost
- CostTotal = CostTotalR = nRanksTotal = nRanksTotalR = 0;
- for ( i = 0; i <= nLevels; i++ )
- {
- CostTotal += pLevelCosts[i];
- CostTotalR += pLevelCostsR[i];
- nRanksTotal += Abc_NtkPlayerCostOneLevel( pLevelCosts[i], RankCost );
- nRanksTotalR += Abc_NtkPlayerCostOneLevel( pLevelCostsR[i], RankCost );
- }
- assert( CostTotal == CostTotalR );
- // print out statistics
- if ( fVerbose )
- {
- for ( i = 1; i <= nLevels; i++ )
- {
- printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i,
- pLevelCosts[i], ((double)pLevelCosts[i])/RankCost,
- pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost );
- }
- printf( "TOTAL : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n",
- CostTotal, nRanksTotal, nRanksTotalR, nLevels );
- }
- free( pLevelCosts );
- free( pLevelCostsR );
- return nRanksTotal;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/player/playerUtil.c b/src/temp/player/playerUtil.c
deleted file mode 100644
index 1c8aeec2..00000000
--- a/src/temp/player/playerUtil.c
+++ /dev/null
@@ -1,353 +0,0 @@
-/**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;
-}
-
-#if 0
-
-/**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_EdgeId(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_EdgeId(Fanin) );
- pObj->Level = pFanin->Level;
- Delay = IVY_MAX( Delay, (int)pObj->Level );
- }
- printf( "Area = %d. Delay = %d.\n", Area, Delay );
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 12:37:56 +0000