summaryrefslogtreecommitdiffstats
path: root/src/opt/xyz/xyzMinEsop.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/xyz/xyzMinEsop.c')
-rw-r--r--src/opt/xyz/xyzMinEsop.c277
1 files changed, 277 insertions, 0 deletions
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
new file mode 100644
index 00000000..114e28a6
--- /dev/null
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -0,0 +1,277 @@
+/**CFile****************************************************************
+
+ FileName [xyzMinEsop.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: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_EsopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Min_EsopMinimize( Min_Man_t * p )
+{
+ int nCubesInit, nCubesOld, nIter;
+ if ( p->nCubes < 3 )
+ return;
+ nIter = 0;
+ nCubesInit = p->nCubes;
+ do {
+ nCubesOld = p->nCubes;
+ Min_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 []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Min_EsopRewrite( Min_Man_t * p )
+{
+ Min_Cube_t * pCube, ** ppPrev;
+ Min_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
+ Min_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
+ Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+ if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+ break;
+ if ( pThis == NULL && Index < p->nVars )
+ Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+ if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+ break;
+ if ( pThis == NULL && Index < p->nVars - 1 )
+ Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+ if ( Min_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 = Min_CubeGetVar( pCube, Var0 );
+ v01 = Min_CubeGetVar( pCube, Var1 );
+ v10 = Min_CubeGetVar( pThis, Var0 );
+ v11 = Min_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+ // derive the first pair of resulting cubes
+ Min_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits -= (v00 != 3);
+ pCube->nLits += ((v00 ^ v10) != 3);
+ Min_CubeXorVar( pThis, Var1, v01 );
+ pThis->nLits -= (v11 != 3);
+ pThis->nLits += ((v01 ^ v11) != 3);
+
+ // add the cubes
+ nCubesOld = p->nCubes;
+ while ( Min_EsopAddCube( p, pCube ) );
+ while ( Min_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
+ Min_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits -= ((v00 ^ v10) != 3);
+ pCube->nLits += (v00 != 3);
+ Min_CubeXorVar( pCube, Var1, v11 );
+ pCube->nLits -= (v01 != 3);
+ pCube->nLits += ((v01 ^ v11) != 3);
+
+ Min_CubeXorVar( pThis, Var0, v00 );
+ pThis->nLits -= (v10 != 3);
+ pThis->nLits += ((v00 ^ v10) != 3);
+ Min_CubeXorVar( pThis, Var1, v01 );
+ pThis->nLits -= ((v01 ^ v11) != 3);
+ pThis->nLits += (v11 != 3);
+
+ // add them anyhow
+ while ( Min_EsopAddCube( p, pCube ) );
+ while ( Min_EsopAddCube( p, pThis ) );
+ }
+// printf( "Pairs = %d ", nPairs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the cube to storage.]
+
+ Description [If the distance one cube is found, returns the transformed
+ cube. If there is no distance one, adds the given cube to storage.
+ Do not forget to clean the storage!]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+ Min_Cube_t * pThis, ** ppPrev;
+ // try to find the identical cube
+ Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+ {
+ if ( Min_CubesAreEqual( pCube, pThis ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubeRecycle( p, pCube );
+ Min_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 0;
+ }
+ }
+ // find a distance-1 cube if it exists
+ if ( pCube->nLits < pCube->nVars )
+ Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+ {
+ if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubesTransform( pCube, pThis, p->pTemp );
+ pCube->nLits++;
+ Min_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+ {
+ if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubesTransform( pCube, pThis, p->pTemp );
+ pCube->nLits--;
+ Min_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ if ( pCube->nLits > 0 )
+ Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+ {
+ if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubesTransform( pCube, pThis, p->pTemp );
+ Min_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;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+