From 2d6a6f66547345e1f67923363c4f63125a07e242 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 11 Apr 2016 21:42:00 -0700 Subject: Added Exorcism package, reading ESOP (read_pla -x file.esop) and deriving AIG (cubes -x; st). --- abclib.dsp | 32 ++ src/aig/gia/giaEsop.c | 55 ++- src/base/abc/abcUtil.c | 17 +- src/base/abci/abc.c | 100 +++- src/base/exor/exor.c | 832 +++++++++++++++++++++++++++++++++ src/base/exor/exor.h | 178 +++++++ src/base/exor/exorBits.c | 425 +++++++++++++++++ src/base/exor/exorCubes.c | 190 ++++++++ src/base/exor/exorLink.c | 746 +++++++++++++++++++++++++++++ src/base/exor/exorList.c | 1140 +++++++++++++++++++++++++++++++++++++++++++++ src/base/exor/exorUtil.c | 204 ++++++++ src/base/exor/module.make | 6 + src/base/io/io.c | 14 +- src/base/io/ioAbc.h | 2 +- src/base/io/ioReadPla.c | 11 +- src/base/io/ioUtil.c | 2 +- 16 files changed, 3921 insertions(+), 33 deletions(-) create mode 100644 src/base/exor/exor.c create mode 100644 src/base/exor/exor.h create mode 100644 src/base/exor/exorBits.c create mode 100644 src/base/exor/exorCubes.c create mode 100644 src/base/exor/exorLink.c create mode 100644 src/base/exor/exorList.c create mode 100644 src/base/exor/exorUtil.c create mode 100644 src/base/exor/module.make diff --git a/abclib.dsp b/abclib.dsp index 61bf44b2..f2332446 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -954,6 +954,38 @@ SOURCE=.\src\base\cba\cbaWriteBlif.c SOURCE=.\src\base\cba\cbaWriteVer.c # End Source File # End Group +# Begin Group "exor" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\base\exor\exor.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exor.h +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exorBits.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exorCubes.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exorLink.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exorList.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\exor\exorUtil.c +# End Source File +# End Group # End Group # Begin Group "bdd" diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c index 9d95ccf5..db69bf02 100644 --- a/src/aig/gia/giaEsop.c +++ b/src/aig/gia/giaEsop.c @@ -143,6 +143,33 @@ void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop ) printf( "\n" ); Vec_StrFree( vStr ); } +Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover ) +{ + Vec_Wec_t * vRes; + Vec_Int_t * vEsop, * vLevel; int i; + vRes = Vec_WecAlloc( Vec_VecSizeSize((Vec_Vec_t *)vCover) ); + Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i ) + { + if ( Vec_IntSize(vEsop) > 0 ) + { + int c, Cube; + Vec_IntForEachEntry( vEsop, Cube, c ) + { + vLevel = Vec_WecPushLevel( vRes ); + if ( Cube != p->Cube1 ) + { + int k, Lit; + Vec_Int_t * vCube = Eso_ManCube( p, Cube ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_IntPush( vLevel, Lit ); + } + Vec_IntPush( vLevel, -i-1 ); + } + } + } + assert( Vec_WecSize(vRes) == Vec_WecCap(vRes) ); + return vRes; +} Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover ) { Vec_Int_t * vEsop; @@ -459,14 +486,15 @@ Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose ) +Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes ) { abctime clk = Abc_Clock(); Vec_Ptr_t * vCover; - Gia_Man_t * pNew; - Gia_Obj_t * pObj; int i, nCubes = 0, nCubesUsed = 0; + Gia_Man_t * pNew = NULL; + Gia_Obj_t * pObj; + int i, nCubes = 0, nCubesUsed = 0; Vec_Int_t * vEsop1, * vEsop2, * vEsop; - Eso_Man_t * p = Eso_ManAlloc( pGia ); + Eso_Man_t * p = Eso_ManAlloc( pGia ); Gia_ManForEachAnd( pGia, pObj, i ) { vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) ); @@ -482,16 +510,23 @@ Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose ) { vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) ); vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 ); - printf( "Output %3d: ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) ); if ( fVerbose ) - Eso_ManCoverPrint( p, vEsop1 ); + printf( "Output %3d: ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) ); +// if ( fVerbose ) +// Eso_ManCoverPrint( p, vEsop1 ); Vec_PtrPush( vCover, Vec_IntDup(vEsop1) ); nCubesUsed += Vec_IntSize(vEsop1); } - printf( "Outs = %d. Cubes = %d. Used = %d. Hashed = %d. ", - Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - pNew = Eso_ManCoverConvert( p, vCover ); + if ( fVerbose ) + { + printf( "Outs = %d. Cubes = %d. Used = %d. Hashed = %d. ", + Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + if ( pvRes ) + *pvRes = Eso_ManCoverDerive( p, vCover ); + else + pNew = Eso_ManCoverConvert( p, vCover ); Vec_VecFree( (Vec_Vec_t *)vCover ); Eso_ManStop( p ); return pNew; diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index f7e0939f..59993614 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -2501,7 +2501,7 @@ float Abc_NtkComputeDelay( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) +void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, int fXor ) { Abc_Obj_t * pNodeOr, * pNodeNew, * pFanin; char * pCube, * pSop = (char *)pNodeOld->pData; @@ -2517,7 +2517,10 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) } // add the OR gate pNodeOr = Abc_NtkCreateNode( pNtkNew ); - pNodeOr->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop), NULL ); + if ( fXor ) + pNodeOr->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop) ); + else + pNodeOr->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop), NULL ); // check the logic function of the node Abc_SopForEachCube( pSop, nVars, pCube ) { @@ -2525,6 +2528,12 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) Abc_CubeForEachVar( pCube, Value, v ) if ( Value == '0' || Value == '1' ) nFanins++; + if ( nFanins == 0 ) // const1 cube in ESOP + { + pNodeNew = Abc_NtkCreateNodeConst1( pNtkNew ); + Abc_ObjAddFanin( pNodeOr, pNodeNew ); + continue; + } assert( nFanins > 0 ); // create node pNodeNew = Abc_NtkCreateNode( pNtkNew ); @@ -2548,7 +2557,7 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) assert( pNodeOld->pCopy == NULL ); pNodeOld->pCopy = pNodeOr; } -Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk, int fXor ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode; @@ -2560,7 +2569,7 @@ Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk ) // perform conversion in the topological order vNodes = Abc_NtkDfs( pNtk, 0 ); Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) - Abc_NodeSopToCubes( pNode, pNtkNew ); + Abc_NodeSopToCubes( pNode, pNtkNew, fXor ); Vec_PtrFree( vNodes ); // make sure everything is okay Abc_NtkFinalize( pNtk, pNtkNew ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index eadd2ddd..fb7ee06d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -465,6 +465,7 @@ static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1092,6 +1093,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); @@ -8826,17 +8828,20 @@ usage: ***********************************************************************/ int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk, int fXor ); Abc_Ntk_t * pNtk, * pNtkRes; - int c; + int c, fXor = 0; pNtk = Abc_FrameReadNtk(pAbc); // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF ) { switch ( c ) { + case 'x': + fXor ^= 1; + break; case 'h': goto usage; default: @@ -8857,7 +8862,7 @@ int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSopToCubes( pNtk ); + pNtkRes = Abc_NtkSopToCubes( pNtk, fXor ); if ( pNtkRes == NULL ) { Abc_Print( -1, "Converting to cubes has failed.\n" ); @@ -8868,9 +8873,10 @@ int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cubes [-h]\n" ); + Abc_Print( -2, "usage: cubes [-xh]\n" ); Abc_Print( -2, "\t converts the current network into a network derived by creating\n" ); Abc_Print( -2, "\t a separate node for each product and sum in the local SOPs\n" ); + Abc_Print( -2, "\t-v : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -39186,7 +39192,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose ); + extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes ); Gia_Man_t * pTemp; int c, fVerbose = 0; Extra_UtilGetoptReset(); @@ -39208,7 +39214,7 @@ int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); return 0; } - pTemp = Eso_ManCompute( pAbc->pGia, fVerbose ); + pTemp = Eso_ManCompute( pAbc->pGia, fVerbose, NULL ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; @@ -39220,6 +39226,86 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity ); + extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes ); + Vec_Wec_t * vEsop = NULL; + char * pFileNameOut = NULL; + int c, Quality = 2, Verbosity = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "QVvh" ) ) != EOF ) + { + switch ( c ) + { + case 'Q': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + Quality = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Quality < 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + Verbosity = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Verbosity < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Exorcism(): There is no AIG.\n" ); + return 0; + } + // get the output file name + if ( argc == globalUtilOptind + 1 ) + pFileNameOut = argv[globalUtilOptind]; + // generate starting cover and run minimization + Eso_ManCompute( pAbc->pGia, fVerbose, &vEsop ); + Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity ); + Vec_WecFree( vEsop ); + return 0; + +usage: + Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] \n" ); + Abc_Print( -2, " performs heuristic exclusive sum-of-project minimization\n" ); + Abc_Print( -2, " -Q N : minimization quality [default = 0]\n"); + Abc_Print( -2, " increasing this number improves quality and adds to runtime\n"); + Abc_Print( -2, " -Q N : verbosity level [default = 0]\n"); + Abc_Print( -2, " 0 = no output; 1 = outline; 2 = verbose\n"); + Abc_Print( -2, " : the output file name in ESOP-PLA format\n"); + Abc_Print( -2, "\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c new file mode 100644 index 00000000..4d567033 --- /dev/null +++ b/src/base/exor/exor.c @@ -0,0 +1,832 @@ +/**CFile**************************************************************** + + FileName [exor.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Main procedure.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exor.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Main Module /// +/// ESOP Minimization Task Coordinator /// +/// /// +/// 1) interprets command line /// +/// 2) calls the approapriate reading procedure /// +/// 3) calls the minimization module /// +/// /// +/// Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000 /// +/// Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 26, 2000 /// +/// Ver. 1.6. Started - Sep 11, 2000. Last update - Sep 15, 2000 /// +/// Ver. 1.7. Started - Sep 20, 2000. Last update - Sep 23, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +/////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// information about the cube cover +cinfo g_CoverInfo; + +extern int s_fDecreaseLiterals; + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION main() /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int ReduceEsopCover() +{ + /////////////////////////////////////////////////////////////// + // SIMPLIFICATION + //////////////////////////////////////////////////////////////////// + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + int GainTotal; + int z; + + do + { +//START: + if ( g_CoverInfo.Verbosity == 2 ) + printf( "\nITERATION #%d\n\n", ++nIterCount ); + else if ( g_CoverInfo.Verbosity == 1 ) + printf( "." ); + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) ) + { + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|0 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + +// if ( g_CoverInfo.Quality >= 2 && nIterWithoutImprovement == 2 ) +// s_fDecreaseLiterals = 1; + } + while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality ); + + + // improve the literal count + s_fDecreaseLiterals = 1; + for ( z = 0; z < 1; z++ ) + { + if ( g_CoverInfo.Verbosity == 2 ) + printf( "\nITERATION #%d\n\n", ++nIterCount ); + else if ( g_CoverInfo.Verbosity == 1 ) + printf( "." ); + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + +// if ( GainTotal ) +// { +// nIterWithoutImprovement = 0; +// goto START; +// } + } + + +/* //////////////////////////////////////////////////////////////////// + // Print statistics + printf( "\nShallow simplification time is "; + cout << (float)(clk2 - clk1)/(float)(CLOCKS_PER_SEC) << " sec\n" ); + printf( "Deep simplification time is "; + cout << (float)(clock() - clk2)/(float)(CLOCKS_PER_SEC) << " sec\n" ); + printf( "Cover after iterative simplification = " << s_nCubesInUse << endl; + printf( "Reduced by initial cube writing = " << g_CoverInfo.nCubesBefore-nCubesAfterWriting << endl; + printf( "Reduced by shallow simplification = " << nCubesAfterWriting-nCubesAfterShallow << endl; + printf( "Reduced by deep simplification = " << nCubesAfterWriting-s_nCubesInUse << endl; + +// printf( "\nThe total number of cubes created = " << g_CoverInfo.cIDs << endl; +// printf( "Total number of places in a queque = " << s_nPosAlloc << endl; +// printf( "Minimum free places in queque-2 = " << s_nPosMax[0] << endl; +// printf( "Minimum free places in queque-3 = " << s_nPosMax[1] << endl; +// printf( "Minimum free places in queque-4 = " << s_nPosMax[2] << endl; +*/ //////////////////////////////////////////////////////////////////// + + // write the number of cubes into cover information + assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc ); + +// printf( "\nThe output cover is\n" ); +// PrintCoverDebug( cout ); + + return 0; +} + +////////////////////////////////////////////////////////////////// +// quite a good script +////////////////////////////////////////////////////////////////// +/* + long clk1 = clock(); + int nIterWithoutImprovement = 0; + do + { + PrintQuequeStats(); + GainTotal = 0; + GainTotal += IterativelyApplyExorLink( DIST2, 0|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 0|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + if ( nIterWithoutImprovement > 2 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + } + + if ( nIterWithoutImprovement > 6 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 12 ); + + nCubesAfterShallow = s_nCubesInUse; + +*/ + +/* + // alu4 - 439 + long clk1 = clock(); + int nIterWithoutImprovement = 0; + do + { + PrintQuequeStats(); + GainTotal = 0; + GainTotal += IterativelyApplyExorLink( DIST2, 1|0|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + if ( nIterWithoutImprovement > 2 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + } + + if ( nIterWithoutImprovement > 6 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 12 ); +*/ + +/* +// alu4 - 412 cubes, 700 sec + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + do + { + printf( "\nITERATION #" << ++nIterCount << endl << endl; + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + if ( nIterWithoutImprovement > 3 ) + { + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + } + + if ( nIterWithoutImprovement > 7 ) + { + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 12 ); +*/ + +/* +// pretty good script +// alu4 = 424 in 250 sec + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + do + { + printf( "\nITERATION #" << ++nIterCount << " |"; + for ( int k = 0; k < nIterWithoutImprovement; k++ ) + printf( "*"; + for ( ; k < 11; k++ ) + printf( "_"; + printf( "|" << endl << endl; + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + if ( nIterWithoutImprovement > 2 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + } + + if ( nIterWithoutImprovement > 4 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 7 ); +*/ + +/* +alu4 = 435 70 secs + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + + do + { + printf( "\nITERATION #" << ++nIterCount << endl << endl; + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 4 ); +*/ + +/* + // the best previous + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + int GainTotal; + do + { + if ( g_CoverInfo.Verbosity == 2 ) + printf( "\nITERATION #" << ++nIterCount << endl << endl; + else if ( g_CoverInfo.Verbosity == 1 ) + cout << '.'; + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + + if ( nIterWithoutImprovement > 1 ) + { + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 ); + GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 ); + GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } +// while ( nIterWithoutImprovement < 20 ); +// while ( nIterWithoutImprovement < 7 ); + while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality ); + +*/ + +/* +// the last tried + + long clk1 = clock(); + int nIterWithoutImprovement = 0; + int nIterCount = 0; + int GainTotal; + do + { + if ( g_CoverInfo.Verbosity == 2 ) + printf( "\nITERATION #" << ++nIterCount << endl << endl; + else if ( g_CoverInfo.Verbosity == 1 ) + cout << '.'; + + GainTotal = 0; + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + + if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) ) + { + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|0 ); + + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|0 ); + GainTotal += IterativelyApplyExorLink2( 1|2|0 ); + GainTotal += IterativelyApplyExorLink3( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|4 ); + GainTotal += IterativelyApplyExorLink2( 1|2|4 ); + GainTotal += IterativelyApplyExorLink4( 1|2|0 ); + } + + if ( GainTotal ) + nIterWithoutImprovement = 0; + else + nIterWithoutImprovement++; + } + while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality ); +*/ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void AddCubesToStartingCover( Vec_Wec_t * vEsop ) +{ + Vec_Int_t * vCube; + Cube * pNew; + int * s_Level2Var; + int * s_LevelValues; + int c, i, k, Lit, Out; + + s_Level2Var = ABC_ALLOC( int, g_CoverInfo.nVarsIn ); + s_LevelValues = ABC_ALLOC( int, g_CoverInfo.nVarsIn ); + + for ( i = 0; i < g_CoverInfo.nVarsIn; i++ ) + s_Level2Var[i] = i; + + g_CoverInfo.nLiteralsBefore = 0; + Vec_WecForEachLevel( vEsop, vCube, c ) + { + // get the output of this cube + Out = -Vec_IntPop(vCube) - 1; + + // fill in the cube with blanks + for ( i = 0; i < g_CoverInfo.nVarsIn; i++ ) + s_LevelValues[i] = VAR_ABS; + Vec_IntForEachEntry( vCube, Lit, k ) + { + if ( Abc_LitIsCompl(Lit) ) + s_LevelValues[Abc_Lit2Var(Lit)] = VAR_NEG; + else + s_LevelValues[Abc_Lit2Var(Lit)] = VAR_POS; + } + + // get the new cube + pNew = GetFreeCube(); + // consider the need to clear the cube + if ( pNew->pCubeDataIn[0] ) // this is a recycled cube + { + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + pNew->pCubeDataIn[i] = 0; + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + pNew->pCubeDataOut[i] = 0; + } + + InsertVarsWithoutClearing( pNew, s_Level2Var, g_CoverInfo.nVarsIn, s_LevelValues, Out ); + // set literal counts + pNew->a = Vec_IntSize(vCube); + pNew->z = 1; + // set the ID + pNew->ID = g_CoverInfo.cIDs++; + // skip through zero-ID + if ( g_CoverInfo.cIDs == 256 ) + g_CoverInfo.cIDs = 1; + + // add this cube to storage + CheckForCloseCubes( pNew, 1 ); + + g_CoverInfo.nLiteralsBefore += Vec_IntSize(vCube); + } + ABC_FREE( s_Level2Var ); + ABC_FREE( s_LevelValues ); + + assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc ); +} + +/**Function************************************************************* + + Synopsis [Performs heuristic minimization of ESOPs.] + + Description [Returns 1 on success, 0 on failure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut ) +{ + long clk1; + int RemainderBits; + int TotalWords; + int MemTemp, MemTotal; + + /////////////////////////////////////////////////////////////////////// + // STEPS of HEURISTIC ESOP MINIMIZATION + /////////////////////////////////////////////////////////////////////// + /////////////////////////////////////////////////////////////////////// + // STEP 1: determine the size of the starting cover + /////////////////////////////////////////////////////////////////////// + assert( nIns > 0 ); + // inputs + RemainderBits = (nIns*2)%(sizeof(unsigned)*8); + TotalWords = (nIns*2)/(sizeof(unsigned)*8) + (RemainderBits > 0); + g_CoverInfo.nVarsIn = nIns; + g_CoverInfo.nWordsIn = TotalWords; + // outputs + RemainderBits = (nOuts)%(sizeof(unsigned)*8); + TotalWords = (nOuts)/(sizeof(unsigned)*8) + (RemainderBits > 0); + g_CoverInfo.nVarsOut = nOuts; + g_CoverInfo.nWordsOut = TotalWords; + g_CoverInfo.cIDs = 1; + + // cubes + clk1 = clock(); +// g_CoverInfo.nCubesBefore = CountTermsInPseudoKroneckerCover( g_Func.dd, nOuts ); + g_CoverInfo.nCubesBefore = Vec_WecSize(vEsop); + g_CoverInfo.TimeStart = clock() - clk1; + + if ( g_CoverInfo.Verbosity ) + { + printf( "Starting cover generation time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) ); + printf( "The number of cubes in the starting cover is %d\n", g_CoverInfo.nCubesBefore ); + } + + if ( g_CoverInfo.nCubesBefore > 20000 ) + { + printf( "\nThe size of the starting cover is more than 20000 cubes. Quitting...\n" ); + return 0; + } + + /////////////////////////////////////////////////////////////////////// + // STEP 2: prepare internal data structures + /////////////////////////////////////////////////////////////////////// + g_CoverInfo.nCubesAlloc = g_CoverInfo.nCubesBefore + ADDITIONAL_CUBES; + + // allocate cube cover + MemTotal = 0; + MemTemp = AllocateCover( g_CoverInfo.nCubesAlloc, g_CoverInfo.nWordsIn, g_CoverInfo.nWordsOut ); + if ( MemTemp == 0 ) + { + printf( "Unexpected memory allocation problem. Quitting...\n" ); + return 0; + } + else + MemTotal += MemTemp; + + // allocate cube sets + MemTemp = AllocateCubeSets( g_CoverInfo.nVarsIn, g_CoverInfo.nVarsOut ); + if ( MemTemp == 0 ) + { + printf( "Unexpected memory allocation problem. Quitting...\n" ); + return 0; + } + else + MemTotal += MemTemp; + + // allocate adjacency queques + MemTemp = AllocateQueques( g_CoverInfo.nCubesAlloc*g_CoverInfo.nCubesAlloc/CUBE_PAIR_FACTOR ); + if ( MemTemp == 0 ) + { + printf( "Unexpected memory allocation problem. Quitting...\n" ); + return 0; + } + else + MemTotal += MemTemp; + + if ( g_CoverInfo.Verbosity ) + printf( "Dynamically allocated memory is %dK\n", MemTotal/1000 ); + + /////////////////////////////////////////////////////////////////////// + // STEP 3: write the cube cover into the allocated storage + /////////////////////////////////////////////////////////////////////// + /////////////////////////////////////////////////////////////////////// + clk1 = clock(); + if ( g_CoverInfo.Verbosity ) + printf( "Generating the starting cover...\n" ); + AddCubesToStartingCover( vEsop ); + /////////////////////////////////////////////////////////////////////// + + /////////////////////////////////////////////////////////////////////// + // STEP 4: iteratively improve the cover + /////////////////////////////////////////////////////////////////////// + if ( g_CoverInfo.Verbosity ) + printf( "Performing minimization...\n" ); + clk1 = clock(); + ReduceEsopCover(); + g_CoverInfo.TimeMin = clock() - clk1; +// g_Func.TimeMin = (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC); + if ( g_CoverInfo.Verbosity ) + { + printf( "\nMinimization time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) ); + printf( "\nThe number of cubes after minimization is %d\n", g_CoverInfo.nCubesInUse ); + } + + /////////////////////////////////////////////////////////////////////// + // STEP 5: save the cover into file + /////////////////////////////////////////////////////////////////////// + // if option is MULTI_OUTPUT, the output is written into the output file; + // if option is SINGLE_NODE, the output is added to the input file + // and written into the output file; in this case, the minimized nodes is + // also stored in the temporary file "temp.blif" for verification + + // create the file name and write the output + { + char Buffer[1000]; + sprintf( Buffer, "%s", pFileNameOut ? pFileNameOut : "temp.esop" ); + WriteResultIntoFile( Buffer ); + //if ( g_CoverInfo.Verbosity ) + printf( "Minimum cover has been written into file <%s>\n", Buffer ); + } + + /////////////////////////////////////////////////////////////////////// + // STEP 6: delocate memory + /////////////////////////////////////////////////////////////////////// + DelocateCubeSets(); + DelocateCover(); + DelocateQueques(); + + // return success + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity ) +{ + memset( &g_CoverInfo, 0, sizeof(cinfo) ); + + g_CoverInfo.Quality = Quality; + g_CoverInfo.Verbosity = Verbosity; + + printf( "EXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" ); + printf( "by Alan Mishchenko, Portland State University, July-September 2000\n" ); + + if ( g_CoverInfo.Verbosity ) + printf( "Incoming ESOP has %d inputs, %d outputs, and %d cubes.\n", nIns, nOuts, Vec_WecSize(vEsop) ); + + PrepareBitSetModule(); + if ( Exorcism( vEsop, nIns, nOuts, pFileNameOut ) == 0 ) + { + printf( "Something went wrong when minimizing the cover\n" ); + return 0; + } + return 1; +} + + + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/exor/exor.h b/src/base/exor/exor.h new file mode 100644 index 00000000..fc1f546b --- /dev/null +++ b/src/base/exor/exor.h @@ -0,0 +1,178 @@ +/**CFile**************************************************************** + + FileName [exor.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exor.h,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Interface of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Main Module /// +/// /// +/// Ver. 1.0. Started - July 15, 2000. Last update - July 20, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 10, 2000 /// +/// Ver. 1.7. Started - Sep 20, 2000. Last update - Sep 23, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#ifndef __EXORMAIN_H__ +#define __EXORMAIN_H__ + +#include +#include +#include +#include +#include "misc/vec/vec.h" +#include "misc/vec/vecWec.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// the number of bits per integer (can be 16, 32, 64 - tested for 32) +#define BPI 32 +#define BPIMASK 31 +#define LOGBPI 5 + +// the maximum number of input variables +#define MAXVARS 1000 + +// the number of cubes that are allocated additionally +#define ADDITIONAL_CUBES 33 + +// the factor showing how many cube pairs will be allocated +#define CUBE_PAIR_FACTOR 20 +// the following number of cube pairs are allocated: +// nCubesAlloc/CUBE_PAIR_FACTOR + +#if BPI == 64 +#define DIFFERENT 0x5555555555555555 +#define BIT_COUNT(w) (BitCount[(w)&0xffff] + BitCount[((w)>>16)&0xffff] + BitCount[((w)>>32)&0xffff] + BitCount[(w)>>48]) +#elif BPI == 32 +#define DIFFERENT 0x55555555 +#define BIT_COUNT(w) (BitCount[(w)&0xffff] + BitCount[(w)>>16]) +#else +#define DIFFERENT 0x5555 +#define BIT_COUNT(w) (BitCount[(w)]) +#endif + + +#define VarWord(element) ((element)>>LOGBPI) +#define VarBit(element) ((element)&BPIMASK) + +#define TICKS_TO_SECONDS(time) ((float)(time)/(float)(CLOCKS_PER_SEC)) + +//////////////////////////////////////////////////////////////////////// +/// CUBE COVER and CUBE typedefs /// +//////////////////////////////////////////////////////////////////////// + +typedef enum { MULTI_OUTPUT = 1, SINGLE_NODE, MULTI_NODE } type; + +// infomation about the cover +typedef struct cinfo_tag +{ + int nVarsIn; // number of input binary variables in the cubes + int nVarsOut; // number of output binary variables in the cubes + int nWordsIn; // number of input words used to represent the cover + int nWordsOut; // number of output words used to represent the cover + int nCubesAlloc; // the number of allocated cubes + int nCubesBefore; // number of cubes before simplification + int nCubesInUse; // number of cubes after simplification + int nCubesFree; // number of free cubes + int nLiteralsBefore;// number of literals before + int nLiteralsAfter; // number of literals before + int cIDs; // the counter of cube IDs + + int Verbosity; // verbosity level + int Quality; // quality + + int TimeRead; // reading time + int TimeStart; // starting cover computation time + int TimeMin; // pure minimization time +} cinfo; + +// representation of one cube (24 bytes + bit info) +typedef unsigned int drow; +typedef unsigned char byte; +typedef struct cube +{ + byte fMark; // the flag which is TRUE if the cubes is enabled + byte ID; // (almost) unique ID of the cube + short a; // the number of literals + short z; // the number of 1's in the output part + drow* pCubeDataIn; // a pointer to the bit string representing literals + drow* pCubeDataOut; // a pointer to the bit string representing literals + struct cube* Prev; // pointers to the previous/next cubes in the list/ring + struct cube* Next; +} Cube; + + +// preparation +extern void PrepareBitSetModule(); +extern int WriteResultIntoFile( char * pFileName ); + +// iterative ExorLink +extern int IterativelyApplyExorLink2( char fDistEnable ); +extern int IterativelyApplyExorLink3( char fDistEnable ); +extern int IterativelyApplyExorLink4( char fDistEnable ); + +// cube storage allocation/delocation +extern int AllocateCubeSets( int nVarsIn, int nVarsOut ); +extern void DelocateCubeSets(); + +// adjacency queque allocation/delocation procedures +extern int AllocateQueques( int nPlaces ); +extern void DelocateQueques(); + +extern int AllocateCover( int nCubes, int nWordsIn, int nWordsOut ); +extern void DelocateCover(); + +extern void AddToFreeCubes( Cube* pC ); +extern Cube* GetFreeCube(); +// getting and returning free cubes to the heap + +extern void InsertVarsWithoutClearing( Cube * pC, int * pVars, int nVarsIn, int * pVarValues, int Output ); +extern int CheckForCloseCubes( Cube* p, int fAddCube ); + +extern int FindDiffVars( int *pDiffVars, Cube* pC1, Cube* pC2 ); +// determines the variables that are different in cubes pC1 and pC2 +// returns the number of variables + +//////////////////////////////////////////////////////////////////////// +/// VARVALUE and CUBEDIST enum typedefs /// +//////////////////////////////////////////////////////////////////////// + +// literal values +typedef enum { VAR_NEG = 1, VAR_POS, VAR_ABS } varvalue; + +// the flag in some function calls can take one of the follwing values +typedef enum { DIST2, DIST3, DIST4 } cubedist; + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/base/exor/exorBits.c b/src/base/exor/exorBits.c new file mode 100644 index 00000000..41560e65 --- /dev/null +++ b/src/base/exor/exorBits.c @@ -0,0 +1,425 @@ +/**CFile**************************************************************** + + FileName [exorBits.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Bit-level procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exorBits.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// EXOR-Oriented Bit String Manipulation /// +/// /// +/// Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 10, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// information about the cube cover +// the number of cubes is constantly updated when the cube cover is processed +// in this module, only the number of variables (nVarsIn) and integers (nWordsIn) +// is used, which do not change +extern cinfo g_CoverInfo; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTIONS OF THIS MODULE /// +//////////////////////////////////////////////////////////////////////// + +int GetDistance( Cube * pC1, Cube * pC2 ); +// return the distance between two cubes +int GetDistancePlus( Cube * pC1, Cube * pC2 ); + +int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 ); +// determine different variables in cubes from pCubes[] and writes them into pDiffVars +// returns the number of different variables + +void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues ); + +//inline int VarWord( int element ); +//inline int VarBit( int element ); +varvalue GetVar( Cube * pC, int Var ); + +void ExorVar( Cube * pC, int Var, varvalue Val ); + +//////////////////////////////////////////////////////////////////////// +/// STATIC VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// the bit count for the first 256 integer numbers +static unsigned char BitCount8[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + +static int SparseNumbers[163] = { + 0,1,4,5,16,17,20,21,64,65,68,69,80,81,84,85,256,257,260, + 261,272,273,276,277,320,321,324,325,336,337,340,1024,1025, + 1028,1029,1040,1041,1044,1045,1088,1089,1092,1093,1104,1105, + 1108,1280,1281,1284,1285,1296,1297,1300,1344,1345,1348,1360, + 4096,4097,4100,4101,4112,4113,4116,4117,4160,4161,4164,4165, + 4176,4177,4180,4352,4353,4356,4357,4368,4369,4372,4416,4417, + 4420,4432,5120,5121,5124,5125,5136,5137,5140,5184,5185,5188, + 5200,5376,5377,5380,5392,5440,16384,16385,16388,16389,16400, + 16401,16404,16405,16448,16449,16452,16453,16464,16465,16468, + 16640,16641,16644,16645,16656,16657,16660,16704,16705,16708, + 16720,17408,17409,17412,17413,17424,17425,17428,17472,17473, + 17476,17488,17664,17665,17668,17680,17728,20480,20481,20484, + 20485,20496,20497,20500,20544,20545,20548,20560,20736,20737, + 20740,20752,20800,21504,21505,21508,21520,21568,21760 +}; + +static unsigned char GroupLiterals[163][4] = { + {0}, {0}, {1}, {0,1}, {2}, {0,2}, {1,2}, {0,1,2}, {3}, {0,3}, + {1,3}, {0,1,3}, {2,3}, {0,2,3}, {1,2,3}, {0,1,2,3}, {4}, {0,4}, + {1,4}, {0,1,4}, {2,4}, {0,2,4}, {1,2,4}, {0,1,2,4}, {3,4}, + {0,3,4}, {1,3,4}, {0,1,3,4}, {2,3,4}, {0,2,3,4}, {1,2,3,4}, {5}, + {0,5}, {1,5}, {0,1,5}, {2,5}, {0,2,5}, {1,2,5}, {0,1,2,5}, {3,5}, + {0,3,5}, {1,3,5}, {0,1,3,5}, {2,3,5}, {0,2,3,5}, {1,2,3,5}, + {4,5}, {0,4,5}, {1,4,5}, {0,1,4,5}, {2,4,5}, {0,2,4,5}, + {1,2,4,5}, {3,4,5}, {0,3,4,5}, {1,3,4,5}, {2,3,4,5}, {6}, {0,6}, + {1,6}, {0,1,6}, {2,6}, {0,2,6}, {1,2,6}, {0,1,2,6}, {3,6}, + {0,3,6}, {1,3,6}, {0,1,3,6}, {2,3,6}, {0,2,3,6}, {1,2,3,6}, + {4,6}, {0,4,6}, {1,4,6}, {0,1,4,6}, {2,4,6}, {0,2,4,6}, + {1,2,4,6}, {3,4,6}, {0,3,4,6}, {1,3,4,6}, {2,3,4,6}, {5,6}, + {0,5,6}, {1,5,6}, {0,1,5,6}, {2,5,6}, {0,2,5,6}, {1,2,5,6}, + {3,5,6}, {0,3,5,6}, {1,3,5,6}, {2,3,5,6}, {4,5,6}, {0,4,5,6}, + {1,4,5,6}, {2,4,5,6}, {3,4,5,6}, {7}, {0,7}, {1,7}, {0,1,7}, + {2,7}, {0,2,7}, {1,2,7}, {0,1,2,7}, {3,7}, {0,3,7}, {1,3,7}, + {0,1,3,7}, {2,3,7}, {0,2,3,7}, {1,2,3,7}, {4,7}, {0,4,7}, + {1,4,7}, {0,1,4,7}, {2,4,7}, {0,2,4,7}, {1,2,4,7}, {3,4,7}, + {0,3,4,7}, {1,3,4,7}, {2,3,4,7}, {5,7}, {0,5,7}, {1,5,7}, + {0,1,5,7}, {2,5,7}, {0,2,5,7}, {1,2,5,7}, {3,5,7}, {0,3,5,7}, + {1,3,5,7}, {2,3,5,7}, {4,5,7}, {0,4,5,7}, {1,4,5,7}, {2,4,5,7}, + {3,4,5,7}, {6,7}, {0,6,7}, {1,6,7}, {0,1,6,7}, {2,6,7}, + {0,2,6,7}, {1,2,6,7}, {3,6,7}, {0,3,6,7}, {1,3,6,7}, {2,3,6,7}, + {4,6,7}, {0,4,6,7}, {1,4,6,7}, {2,4,6,7}, {3,4,6,7}, {5,6,7}, + {0,5,6,7}, {1,5,6,7}, {2,5,6,7}, {3,5,6,7}, {4,5,6,7} +}; + +// the bit count to 16-bit numbers +#define FULL16BITS 0x10000 +#define MARKNUMBER 200 + +static unsigned char BitGroupNumbers[FULL16BITS]; +unsigned char BitCount[FULL16BITS]; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void PrepareBitSetModule() +// this function should be called before anything is done with the cube cover +{ + // prepare bit count + int i, k; + int nLimit; + + nLimit = FULL16BITS; + for ( i = 0; i < nLimit; i++ ) + { + BitCount[i] = BitCount8[ i & 0xff ] + BitCount8[ i>>8 ]; + BitGroupNumbers[i] = MARKNUMBER; + } + // prepare bit groups + for ( k = 0; k < 163; k++ ) + BitGroupNumbers[ SparseNumbers[k] ] = k; +/* + // verify bit groups + int n = 4368; + char Buff[100]; + cout << "The number is " << n << endl; + cout << "The binary is " << itoa(n,Buff,2) << endl; + cout << "BitGroupNumbers[n] is " << (int)BitGroupNumbers[n] << endl; + cout << "The group literals are "; + for ( int g = 0; g < 4; g++ ) + cout << " " << (int)GroupLiterals[BitGroupNumbers[n]][g]; +*/ +} + +//////////////////////////////////////////////////////////////////////// +/// INLINE FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +/* +int VarWord( int element ) +{ + return ( element >> LOGBPI ); +} + +int VarBit( int element ) +{ + return ( element & BPIMASK ); +} +*/ + +varvalue GetVar( Cube * pC, int Var ) +// returns VAR_NEG if var is neg, VAR_POS if var is pos, VAR_ABS if var is absent +{ + int Bit = (Var<<1); + int Value = ((pC->pCubeDataIn[VarWord(Bit)] >> VarBit(Bit)) & 3); + assert( Value == VAR_NEG || Value == VAR_POS || Value == VAR_ABS ); + return (varvalue)Value; +} + +void ExorVar( Cube * pC, int Var, varvalue Val ) +// EXORs the value Val with the value of variable Var in the given cube +// ((cube[VAR_WORD((v)<<1)]) ^ ( (pol)<pCubeDataIn[VarWord(Bit)] ^= ( Val << VarBit(Bit) ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static int DiffVarCounter, cVars; +static drow Temp1, Temp2, Temp; +static drow LastNonZeroWord; +static int LastNonZeroWordNum; + +int GetDistance( Cube * pC1, Cube * pC2 ) +// finds and returns the distance between two cubes pC1 and pC2 +{ + int i; + DiffVarCounter = 0; + + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + { + Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i]; + Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT; + + // count how many bits are one in this var difference + DiffVarCounter += BIT_COUNT(Temp2); + if ( DiffVarCounter > 4 ) + return 5; + } + // check whether the output parts are different + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] ) + { + DiffVarCounter++; + break; + } + return DiffVarCounter; +} + +// place to put the number of the different variable and its value in the second cube +extern int s_DiffVarNum; +extern int s_DiffVarValueP_old; +extern int s_DiffVarValueP_new; +extern int s_DiffVarValueQ; + +int GetDistancePlus( Cube * pC1, Cube * pC2 ) +// finds and returns the distance between two cubes pC1 and pC2 +// if the distance is 1, returns the number of diff variable in VarNum +{ + int i; + + DiffVarCounter = 0; + LastNonZeroWordNum = -1; + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + { + Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i]; + Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT; + + // save the value of var difference, in case + // the distance is one and we need to return the var number + if ( Temp2 ) + { + LastNonZeroWordNum = i; + LastNonZeroWord = Temp2; + } + + // count how many bits are one in this var difference + DiffVarCounter += BIT_COUNT(Temp2); + if ( DiffVarCounter > 4 ) + return 5; + } + // check whether the output parts are different + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] ) + { + DiffVarCounter++; + break; + } + + if ( DiffVarCounter == 1 ) + { + if ( LastNonZeroWordNum == -1 ) // the output is the only different variable + s_DiffVarNum = -1; + else + { + Temp = (LastNonZeroWord>>2); + for ( i = 0; Temp; Temp>>=2, i++ ); + s_DiffVarNum = LastNonZeroWordNum*BPI/2 + i; + + // save the old var value + s_DiffVarValueP_old = GetVar( pC1, s_DiffVarNum ); + s_DiffVarValueQ = GetVar( pC2, s_DiffVarNum ); + + // EXOR this value with the corresponding value in p cube + ExorVar( pC1, s_DiffVarNum, (varvalue)s_DiffVarValueQ ); + + s_DiffVarValueP_new = GetVar( pC1, s_DiffVarNum ); + } + } + + return DiffVarCounter; +} + +int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 ) +// determine different variables in two cubes and +// writes them into pDiffVars[] +// -1 is written into pDiffVars[0] if the cubes have different outputs +// returns the number of different variables (including the output) +{ + int i, v; + DiffVarCounter = 0; + // check whether the output parts of the cubes are different + + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + if ( pC1->pCubeDataOut[i] != pC2->pCubeDataOut[i] ) + { // they are different + pDiffVars[0] = -1; + DiffVarCounter = 1; + break; + } + + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + { + + Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i]; + Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT; + + // check the first part of this word + Temp = Temp2 & 0xffff; + cVars = BitCount[ Temp ]; + if ( cVars ) + { + if ( cVars < 5 ) + for ( v = 0; v < cVars; v++ ) + { + assert( BitGroupNumbers[Temp] != MARKNUMBER ); + pDiffVars[ DiffVarCounter++ ] = i*16 + GroupLiterals[ BitGroupNumbers[Temp] ][v]; + } + else + return 5; + } + if ( DiffVarCounter > 4 ) + return 5; + + // check the second part of this word + Temp = Temp2 >> 16; + cVars = BitCount[ Temp ]; + if ( cVars ) + { + if ( cVars < 5 ) + for ( v = 0; v < cVars; v++ ) + { + assert( BitGroupNumbers[Temp] != MARKNUMBER ); + pDiffVars[ DiffVarCounter++ ] = i*16 + 8 + GroupLiterals[ BitGroupNumbers[Temp] ][v]; + } + else + return 5; + } + if ( DiffVarCounter > 4 ) + return 5; + } + return DiffVarCounter; +} + +void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues ) +// corrects the given number of variables (nVarsIn) in pC->pCubeDataIn[] +// variable numbers are given in pVarNumbers[], their values are in pVarValues[] +// arrays pVarNumbers[] and pVarValues[] are provided by the user +{ + int GlobalBit; + int LocalWord; + int LocalBit; + int i; + assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn ); + for ( i = 0; i < nVarsIn; i++ ) + { + assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn ); + assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS ); + GlobalBit = (pVars[i]<<1); + LocalWord = VarWord(GlobalBit); + LocalBit = VarBit(GlobalBit); + + // correct this variables + pC->pCubeDataIn[LocalWord] = ((pC->pCubeDataIn[LocalWord]&(~(3<pCubeDataIn[] +// variable numbers are given in pVarNumbers[], their values are in pVarValues[] +// arrays pVarNumbers[] and pVarValues[] are provided by the user +{ + int GlobalBit; + int LocalWord; + int LocalBit; + int i; + assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn ); + for ( i = 0; i < nVarsIn; i++ ) + { + assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn ); + assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS ); + GlobalBit = (pVars[i]<<1); + LocalWord = VarWord(GlobalBit); + LocalBit = VarBit(GlobalBit); + + // correct this variables + pC->pCubeDataIn[LocalWord] |= ( pVarValues[i] << LocalBit ); + } + // insert the output bit + pC->pCubeDataOut[VarWord(Output)] |= ( 1 << VarBit(Output) ); +} + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/exor/exorCubes.c b/src/base/exor/exorCubes.c new file mode 100644 index 00000000..c8b40a82 --- /dev/null +++ b/src/base/exor/exorCubes.c @@ -0,0 +1,190 @@ +/**CFile**************************************************************** + + FileName [exorCubes.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Cube manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exorCubes.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Cube Allocation and Free Cube Management /// +/// /// +/// Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000 /// +/// Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000 /// +/// Ver. 1.2. Started - July 30, 2000. Last update - July 30, 2000 /// +/// Ver. 1.5. Started - Aug 19, 2000. Last update - Aug 19, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// information about the cube cover before and after simplification +extern cinfo g_CoverInfo; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTIONS OF THIS MODULE /// +//////////////////////////////////////////////////////////////////////// + +// cube cover memory allocation/delocation procedures +// (called from the ExorMain module) +int AllocateCover( int nCubes, int nWordsIn, int nWordsOut ); +void DelocateCover(); + +// manipulation of the free cube list +// (called from Pseudo-Kronecker, ExorList, and ExorLink modules) +void AddToFreeCubes( Cube * pC ); +Cube * GetFreeCube(); + +//////////////////////////////////////////////////////////////////////// +/// EXPORTED VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STATIC VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// the pointer to the allocated memory +Cube ** s_pCoverMemory; + +// the list of free cubes +Cube * s_CubesFree; + +/////////////////////////////////////////////////////////////////// +/// CUBE COVER MEMORY MANAGEMENT // +/////////////////////////////////////////////////////////////////// + +int AllocateCover( int nCubes, int nWordsIn, int nWordsOut ) +// uses the cover parameters nCubes and nWords +// to allocate-and-clean the cover in one large piece +{ + int OneCubeSize; + int OneInputSetSize; + Cube ** pp; + int TotalSize; + int i, k; + + // determine the size of one cube WITH storage for bits + OneCubeSize = sizeof(Cube) + (nWordsIn+nWordsOut)*sizeof(unsigned); + // determine what is the amount of storage for the input part of the cube + OneInputSetSize = nWordsIn*sizeof(unsigned); + + // allocate memory for the array of pointers + pp = (Cube **)ABC_ALLOC( Cube *, nCubes ); + if ( pp == NULL ) + return 0; + + // determine the size of the total cube cover + TotalSize = nCubes*OneCubeSize; + // allocate and clear memory for the cover in one large piece + pp[0] = (Cube *)ABC_ALLOC( char, TotalSize ); + if ( pp[0] == NULL ) + return 0; + memset( pp[0], 0, TotalSize ); + + // assign pointers to cubes and bit strings inside this piece + pp[0]->pCubeDataIn = (unsigned*)(pp[0] + 1); + pp[0]->pCubeDataOut = (unsigned*)((char*)pp[0]->pCubeDataIn + OneInputSetSize); + for ( i = 1; i < nCubes; i++ ) + { + pp[i] = (Cube *)((char*)pp[i-1] + OneCubeSize); + pp[i]->pCubeDataIn = (unsigned*)(pp[i] + 1); + pp[i]->pCubeDataOut = (unsigned*)((char*)pp[i]->pCubeDataIn + OneInputSetSize); + } + + // connect the cubes into the list using Next pointers + for ( k = 0; k < nCubes-1; k++ ) + pp[k]->Next = pp[k+1]; + // the last pointer is already set to NULL + + // assign the head of the free list + s_CubesFree = pp[0]; + // set the counters of the used and free cubes + g_CoverInfo.nCubesInUse = 0; + g_CoverInfo.nCubesFree = nCubes; + + // save the pointer to the allocated memory + s_pCoverMemory = pp; + + assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc ); + + return nCubes*sizeof(Cube *) + TotalSize; +} + +void DelocateCover() +{ + ABC_FREE( s_pCoverMemory[0] ); + ABC_FREE( s_pCoverMemory ); +} + +/////////////////////////////////////////////////////////////////// +/// FREE CUBE LIST MANIPULATION FUNCTIONS /// +/////////////////////////////////////////////////////////////////// + +void AddToFreeCubes( Cube * p ) +{ + assert( p ); + assert( p->Prev == NULL ); // the cube should not be in use + assert( p->Next == NULL ); + assert( p->ID ); + + p->Next = s_CubesFree; + s_CubesFree = p; + + // set the ID of the cube to 0, + // so that cube pair garbage collection could recognize it as different + p->ID = 0; + + g_CoverInfo.nCubesFree++; +} + +Cube * GetFreeCube() +{ + Cube * p; + assert( s_CubesFree ); + p = s_CubesFree; + s_CubesFree = s_CubesFree->Next; + p->Next = NULL; + g_CoverInfo.nCubesFree--; + return p; +} + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/exor/exorLink.c b/src/base/exor/exorLink.c new file mode 100644 index 00000000..032ed318 --- /dev/null +++ b/src/base/exor/exorLink.c @@ -0,0 +1,746 @@ +/**CFile**************************************************************** + + FileName [exorLink.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Cube iterators.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exorLink.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Generation of ExorLinked Cubes /// +/// /// +/// Ver. 1.0. Started - July 26, 2000. Last update - July 29, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 12, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define LARGE_NUM 1000000 + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTIONS OF THIS MODULE /// +//////////////////////////////////////////////////////////////////////// + +int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist ); +// this function starts the Exor-Link iterator, which iterates +// through the cube groups starting from the group with min literals +// returns 1 on success, returns 0 if the cubes have wrong distance + +int ExorLinkCubeIteratorNext( Cube** pGroup ); +// give the next group in the decreasing order of sum of literals +// returns 1 on success, returns 0 if there are no more groups + +int ExorLinkCubeIteratorPick( Cube** pGroup, int g ); +// gives the group #g in the order in which the groups were given +// during iteration +// returns 1 on success, returns 0 if something g is too large + +void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup ); +// removes the cubes from the store back into the list of free cubes +// if fTakeLastGroup is 0, removes all cubes +// if fTakeLastGroup is 1, does not store the last group + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// information about the cube cover before +extern cinfo g_CoverInfo; +// new IDs are assigned only when it is known that the cubes are useful +// this is done in ExorLinkCubeIteratorCleanUp(); + +// the head of the list of free cubes +extern Cube* g_CubesFree; + +extern byte BitCount[]; + +//////////////////////////////////////////////////////////////////////// +/// EXORLINK INFO /// +//////////////////////////////////////////////////////////////////////// + +const int s_ELMax = 4; + +// ExorLink-2: there are 4 cubes, 2 literals each, combined into 2 groups +// ExorLink-3: there are 12 cubes, 3 literals each, combined into 6 groups +// ExorLink-4: there are 32 cubes, 4 literals each, combined into 24 groups +// ExorLink-5: there are 80 cubes, 5 literals each, combined into 120 groups +// Exorlink-n: there are n*2^(n-1) cubes, n literals each, combined into n! groups +const int s_ELnCubes[4] = { 4, 12, 32, 80 }; +const int s_ELnGroups[4] = { 2, 6, 24, 120 }; + +// value sets of cubes X{a0}Y{b0}Z{c0}U{d0} and X{a1}Y{b1}Z{c1}U{d1} +// used to represent the ExorLink cube generation rules +enum { vs0, vs1, vsX }; +// vs0 = 0, // the value set of the first cube +// vs1 = 1, // the value set of the second cube +// vsX = 2 // EXOR of the value sets of the first and second cubes + +// representation of ExorLinked cubes +static int s_ELCubeRules[3][32][4] = { +{ // ExorLink-2 Cube Generating Rules + // | 0 | 1 | - sections + // |-------| + {vsX,vs0}, // cube 0 | | | + {vsX,vs1}, // cube 1 | | 0 | + {vs0,vsX}, // cube 2 | | | + {vs1,vsX} // cube 3 | 0 | | +}, +{ // ExorLink-3 Cube Generating Rules + // | 0 | 1 | 2 | - sections + // |-----------| + {vsX,vs0,vs0}, // cube 0 | | | | + {vsX,vs0,vs1}, // cube 1 | | | 0 | + {vsX,vs1,vs0}, // cube 2 | | 0 | | + {vsX,vs1,vs1}, // cube 3 | | 1 | 1 | + + {vs0,vsX,vs0}, // cube 4 | | | | + {vs0,vsX,vs1}, // cube 5 | | | 2 | + {vs1,vsX,vs0}, // cube 6 | 0 | | | + {vs1,vsX,vs1}, // cube 7 | 1 | | 3 | + + {vs0,vs0,vsX}, // cube 8 | | | | + {vs0,vs1,vsX}, // cube 9 | | 2 | | + {vs1,vs0,vsX}, // cube 10 | 2 | | | + {vs1,vs1,vsX} // cube 11 | 3 | 3 | | +}, +{ // ExorLink-4 Rules Generating Rules + // | 0 | 1 | 2 | 4 | - sections + // |---------------| + {vsX,vs0,vs0,vs0}, // cube 0 | | | | | + {vsX,vs0,vs0,vs1}, // cube 1 | | | | 0 | + {vsX,vs0,vs1,vs0}, // cube 2 | | | 0 | | + {vsX,vs0,vs1,vs1}, // cube 3 | | | 1 | 1 | + {vsX,vs1,vs0,vs0}, // cube 4 | | 0 | | | + {vsX,vs1,vs0,vs1}, // cube 5 | | 1 | | 2 | + {vsX,vs1,vs1,vs0}, // cube 6 | | 2 | 2 | | + {vsX,vs1,vs1,vs1}, // cube 7 | | 3 | 3 | 3 | + + {vs0,vsX,vs0,vs0}, // cube 8 | | | | | + {vs0,vsX,vs0,vs1}, // cube 9 | | | | 4 | + {vs0,vsX,vs1,vs0}, // cube 10 | | | 4 | | + {vs0,vsX,vs1,vs1}, // cube 11 | | | 5 | 5 | + {vs1,vsX,vs0,vs0}, // cube 12 | 0 | | | | + {vs1,vsX,vs0,vs1}, // cube 13 | 1 | | | 6 | + {vs1,vsX,vs1,vs0}, // cube 14 | 2 | | 6 | | + {vs1,vsX,vs1,vs1}, // cube 15 | 3 | | 7 | 7 | + + {vs0,vs0,vsX,vs0}, // cube 16 | | | | | + {vs0,vs0,vsX,vs1}, // cube 17 | | | | 8 | + {vs0,vs1,vsX,vs0}, // cube 18 | | 4 | | | + {vs0,vs1,vsX,vs1}, // cube 19 | | 5 | | 9 | + {vs1,vs0,vsX,vs0}, // cube 20 | 4 | | | | + {vs1,vs0,vsX,vs1}, // cube 21 | 5 | | | 10| + {vs1,vs1,vsX,vs0}, // cube 22 | 6 | 6 | | | + {vs1,vs1,vsX,vs1}, // cube 23 | 7 | 7 | | 11| + + {vs0,vs0,vs0,vsX}, // cube 24 | | | | | + {vs0,vs0,vs1,vsX}, // cube 25 | | | 8 | | + {vs0,vs1,vs0,vsX}, // cube 26 | | 8 | | | + {vs0,vs1,vs1,vsX}, // cube 27 | | 9 | 9 | | + {vs1,vs0,vs0,vsX}, // cube 28 | 8 | | | | + {vs1,vs0,vs1,vsX}, // cube 29 | 9 | | 10| | + {vs1,vs1,vs0,vsX}, // cube 30 | 10| 10| | | + {vs1,vs1,vs1,vsX} // cube 31 | 11| 11| 11| | +} +}; + +// these cubes are combined into groups +static int s_ELGroupRules[3][24][4] = { +{ // ExorLink-2 Group Forming Rules + {0,3}, // group 0 - section 0 + {2,1} // group 1 - section 1 +}, +{ // ExorLink-3 Group Forming Rules + {0,6,11}, // group 0 - section 0 + {0,7,10}, // group 1 + {4,2,11}, // group 2 - section 1 + {4,3,9}, // group 3 + {8,1,7}, // group 4 - section 2 + {8,3,5} // group 5 +}, +{ // ExorLink-4 Group Forming Rules +// section 0: (0-12)(1-13)(2-14)(3-15)(4-20)(5-21)(6-22)(7-23)(8-28)(9-29)(10-30)(11-31) + {0,12,22,31}, // group 0 // {0,6,11}, // group 0 - section 0 + {0,12,23,30}, // group 1 // {0,7,10}, // group 1 + {0,20,14,31}, // group 2 // {4,2,11}, // group 2 + {0,20,15,29}, // group 3 // {4,3,9}, // group 3 + {0,28,13,23}, // group 4 // {8,1,7}, // group 4 + {0,28,15,21}, // group 5 // {8,3,5} // group 5 +// section 1: (0-4)(1-5)(2-6)(3-7)(4-18)(5-19)(6-22)(7-23)(8-26)(9-27)(10-30)(11-31) + {8,4,22,31}, // group 6 + {8,4,23,30}, // group 7 + {8,18,6,31}, // group 8 + {8,18,7,27}, // group 9 + {8,26,5,23}, // group 10 + {8,26,7,19}, // group 11 +// section 2: (0-2)(1-3)(2-6)(3-7)(4-10)(5-11)(6-14)(7-15)(8-25)(9-27)(10-29)(11-31) + {16,2,14,31}, // group 12 + {16,2,15,29}, // group 13 + {16,10,6,31}, // group 14 + {16,10,7,27}, // group 15 + {16,25,3,15}, // group 16 + {16,25,7,11}, // group 17 +// section 3: (0-1)(1-3)(2-5)(3-7)(4-9)(5-11)(6-13)(7-15)(8-17)(9-19)(10-21)(11-23) + {24,1,13,23}, // group 18 + {24,1,15,21}, // group 19 + {24,9, 5,23}, // group 20 + {24,9, 7,19}, // group 21 + {24,17,3,15}, // group 22 + {24,17,7,11} // group 23 +} +}; + +// it is assumed that if literals in the first cube, second cube +// and their EXOR are 0 or 1 (as opposed to -), they are written +// into a mask, which is used to count the number of literals in +// the cube groups cubes +// +// below is the set of masks selecting literals belonging +// to the given cube of the group + +static drow s_CubeLitMasks[3][32] = { +{ // ExorLink-2 Literal Counting Masks +// v3 v2 v1 v0 +// -xBA -xBA -xBA -xBA +// ------------------- + 0x14, // cube 0 <0000 0000 0001 0100> {vsX,vs0} + 0x24, // cube 1 <0000 0000 0010 0100> {vsX,vs1} + 0x41, // cube 2 <0000 0000 0100 0001> {vs0,vsX} + 0x42, // cube 3 <0000 0000 0100 0010> {vs1,vsX} +}, +{ // ExorLink-3 Literal Counting Masks + 0x114, // cube 0 <0000 0001 0001 0100> {vsX,vs0,vs0} + 0x214, // cube 1 <0000 0010 0001 0100> {vsX,vs0,vs1} + 0x124, // cube 2 <0000 0001 0010 0100> {vsX,vs1,vs0} + 0x224, // cube 3 <0000 0010 0010 0100> {vsX,vs1,vs1} + 0x141, // cube 4 <0000 0001 0100 0001> {vs0,vsX,vs0} + 0x241, // cube 5 <0000 0010 0100 0001> {vs0,vsX,vs1} + 0x142, // cube 6 <0000 0001 0100 0010> {vs1,vsX,vs0} + 0x242, // cube 7 <0000 0010 0100 0010> {vs1,vsX,vs1} + 0x411, // cube 8 <0000 0100 0001 0001> {vs0,vs0,vsX} + 0x421, // cube 9 <0000 0100 0010 0001> {vs0,vs1,vsX} + 0x412, // cube 10 <0000 0100 0001 0010> {vs1,vs0,vsX} + 0x422, // cube 11 <0000 0100 0010 0010> {vs1,vs1,vsX} +}, +{ // ExorLink-4 Literal Counting Masks + 0x1114, // cube 0 <0001 0001 0001 0100> {vsX,vs0,vs0,vs0} + 0x2114, // cube 1 <0010 0001 0001 0100> {vsX,vs0,vs0,vs1} + 0x1214, // cube 2 <0001 0010 0001 0100> {vsX,vs0,vs1,vs0} + 0x2214, // cube 3 <0010 0010 0001 0100> {vsX,vs0,vs1,vs1} + 0x1124, // cube 4 <0001 0001 0010 0100> {vsX,vs1,vs0,vs0} + 0x2124, // cube 5 <0010 0001 0010 0100> {vsX,vs1,vs0,vs1} + 0x1224, // cube 6 <0001 0010 0010 0100> {vsX,vs1,vs1,vs0} + 0x2224, // cube 7 <0010 0010 0010 0100> {vsX,vs1,vs1,vs1} + 0x1141, // cube 8 <0001 0001 0100 0001> {vs0,vsX,vs0,vs0} + 0x2141, // cube 9 <0010 0001 0100 0001> {vs0,vsX,vs0,vs1} + 0x1241, // cube 10 <0001 0010 0100 0001> {vs0,vsX,vs1,vs0} + 0x2241, // cube 11 <0010 0010 0100 0001> {vs0,vsX,vs1,vs1} + 0x1142, // cube 12 <0001 0001 0100 0010> {vs1,vsX,vs0,vs0} + 0x2142, // cube 13 <0010 0001 0100 0010> {vs1,vsX,vs0,vs1} + 0x1242, // cube 14 <0001 0010 0100 0010> {vs1,vsX,vs1,vs0} + 0x2242, // cube 15 <0010 0010 0100 0010> {vs1,vsX,vs1,vs1} + 0x1411, // cube 16 <0001 0100 0001 0001> {vs0,vs0,vsX,vs0} + 0x2411, // cube 17 <0010 0100 0001 0001> {vs0,vs0,vsX,vs1} + 0x1421, // cube 18 <0001 0100 0010 0001> {vs0,vs1,vsX,vs0} + 0x2421, // cube 19 <0010 0100 0010 0001> {vs0,vs1,vsX,vs1} + 0x1412, // cube 20 <0001 0100 0001 0010> {vs1,vs0,vsX,vs0} + 0x2412, // cube 21 <0010 0100 0001 0010> {vs1,vs0,vsX,vs1} + 0x1422, // cube 22 <0001 0100 0010 0010> {vs1,vs1,vsX,vs0} + 0x2422, // cube 23 <0010 0100 0010 0010> {vs1,vs1,vsX,vs1} + 0x4111, // cube 24 <0100 0001 0001 0001> {vs0,vs0,vs0,vsX} + 0x4211, // cube 25 <0100 0010 0001 0001> {vs0,vs0,vs1,vsX} + 0x4121, // cube 26 <0100 0001 0010 0001> {vs0,vs1,vs0,vsX} + 0x4221, // cube 27 <0100 0010 0010 0001> {vs0,vs1,vs1,vsX} + 0x4112, // cube 28 <0100 0001 0001 0010> {vs1,vs0,vs0,vsX} + 0x4212, // cube 29 <0100 0010 0001 0010> {vs1,vs0,vs1,vsX} + 0x4122, // cube 30 <0100 0001 0010 0010> {vs1,vs1,vs0,vsX} + 0x4222, // cube 31 <0100 0010 0010 0010> {vs1,vs1,vs1,vsX} +} +}; + +static drow s_BitMasks[32] = +{ + 0x00000001,0x00000002,0x00000004,0x00000008, + 0x00000010,0x00000020,0x00000040,0x00000080, + 0x00000100,0x00000200,0x00000400,0x00000800, + 0x00001000,0x00002000,0x00004000,0x00008000, + 0x00010000,0x00020000,0x00040000,0x00080000, + 0x00100000,0x00200000,0x00400000,0x00800000, + 0x01000000,0x02000000,0x04000000,0x08000000, + 0x10000000,0x20000000,0x40000000,0x80000000 +}; + +//////////////////////////////////////////////////////////////////////// +/// STATIC VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// this flag is TRUE as long as the storage is allocated +static int fWorking; + +// set these flags to have minimum literal groups generated first +static int fMinLitGroupsFirst[4] = { 0 /*dist2*/, 0 /*dist3*/, 0 /*dist4*/}; + +static int nDist; +static int nCubes; +static int nCubesInGroup; +static int nGroups; +static Cube *pCA, *pCB; + +// storage for variable numbers that are different in the cubes +static int DiffVars[5]; +static int* pDiffVars; +static int nDifferentVars; + +// storage for the bits and words of different input variables +static int nDiffVarsIn; +static int DiffVarWords[5]; +static int DiffVarBits[5]; + +// literal mask used to count the number of literals in the cubes +static drow MaskLiterals; +// the base for counting literals +static int StartingLiterals; +// the number of literals in each cube +static int CubeLiterals[32]; +static int BitShift; +static int DiffVarValues[4][3]; +static int Value; + +// the sorted array of groups in the increasing order of costs +static int GroupCosts[32]; +static int GroupCostBest; +static int GroupCostBestNum; + +static int CubeNum; +static int NewZ; +static drow Temp; + +// the cubes currently created +static Cube* ELCubes[32]; + +// the bit string with 1's corresponding to cubes in ELCubes[] +// that constitute the last group +static drow LastGroup; + +static int GroupOrder[24]; +static drow VisitedGroups; +static int nVisitedGroups; + +//int RemainderBits = (nVars*2)%(sizeof(drow)*8); +//int TotalWords = (nVars*2)/(sizeof(drow)*8) + (RemainderBits > 0); +static drow DammyBitData[(MAXVARS*2)/(sizeof(drow)*8)+(MAXVARS*2)%(sizeof(drow)*8)]; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINTIONS /// +//////////////////////////////////////////////////////////////////////// + +// IDEA! if we already used a cube to count distances and it did not improve +// there is no need to try it again with other group +// (this idea works only for ExorLink-2 and -3) + +int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist ) +// this function starts the Exor-Link iterator, which iterates +// through the cube groups starting from the group with min literals +// returns 1 on success, returns 0 if the cubes have wrong distance +{ + int i, c; + + // check that everything is okey + assert( pC1 != NULL ); + assert( pC2 != NULL ); + assert( !fWorking ); + + nDist = Dist; + nCubes = Dist + 2; + nCubesInGroup = s_ELnCubes[nDist]; + nGroups = s_ELnGroups[Dist]; + pCA = pC1; + pCB = pC2; + // find what variables are different in these two cubes + // FindDiffVars returns DiffVars[0] < 0, if the output is different + nDifferentVars = FindDiffVars( DiffVars, pCA, pCB ); + if ( nCubes != nDifferentVars ) + { +// cout << "ExorLinkCubeIterator(): Distance mismatch"; +// cout << " nCubes = " << nCubes << " nDiffVars = " << nDifferentVars << endl; + fWorking = 0; + return 0; + } + + // copy the input variable cube data into DammyBitData[] + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + DammyBitData[i] = pCA->pCubeDataIn[i]; + + // find the number of different input variables + nDiffVarsIn = ( DiffVars[0] >= 0 )? nCubes: nCubes-1; + // assign the pointer to the place where the number of diff input vars is stored + pDiffVars = ( DiffVars[0] >= 0 )? DiffVars: DiffVars+1; + // find the bit offsets and remove different variables + for ( i = 0; i < nDiffVarsIn; i++ ) + { + DiffVarWords[i] = ((2*pDiffVars[i]) >> LOGBPI) ; + DiffVarBits[i] = ((2*pDiffVars[i]) & BPIMASK); + // clear this position + DammyBitData[ DiffVarWords[i] ] &= ~( 3 << DiffVarBits[i] ); + } + + // extract the values from the cubes and create the mask of literals + MaskLiterals = 0; + // initialize the base for literal counts + StartingLiterals = pCA->a; + for ( i = 0, BitShift = 0; i < nDiffVarsIn; i++, BitShift++ ) + { + DiffVarValues[i][0] = ( pCA->pCubeDataIn[DiffVarWords[i]] >> DiffVarBits[i] ) & 3; + if ( DiffVarValues[i][0] != VAR_ABS ) + { + MaskLiterals |= ( 1 << BitShift ); + // update the base for literal counts + StartingLiterals--; + } + BitShift++; + + DiffVarValues[i][1] = ( pCB->pCubeDataIn[DiffVarWords[i]] >> DiffVarBits[i] ) & 3; + if ( DiffVarValues[i][1] != VAR_ABS ) + MaskLiterals |= ( 1 << BitShift ); + BitShift++; + + DiffVarValues[i][2] = DiffVarValues[i][0] ^ DiffVarValues[i][1]; + if ( DiffVarValues[i][2] != VAR_ABS ) + MaskLiterals |= ( 1 << BitShift ); + BitShift++; + } + + // count the number of additional literals in each cube of the group + for ( i = 0; i < nCubesInGroup; i++ ) + CubeLiterals[i] = BitCount[ MaskLiterals & s_CubeLitMasks[Dist][i] ]; + + // compute the costs of all groups + for ( i = 0; i < nGroups; i++ ) + // go over all cubes in the group + for ( GroupCosts[i] = 0, c = 0; c < nCubes; c++ ) + GroupCosts[i] += CubeLiterals[ s_ELGroupRules[Dist][i][c] ]; + + // find the best cost group + if ( fMinLitGroupsFirst[Dist] ) + { // find the minimum cost group + GroupCostBest = LARGE_NUM; + for ( i = 0; i < nGroups; i++ ) + if ( GroupCostBest > GroupCosts[i] ) + { + GroupCostBest = GroupCosts[i]; + GroupCostBestNum = i; + } + } + else + { // find the maximum cost group + GroupCostBest = -1; + for ( i = 0; i < nGroups; i++ ) + if ( GroupCostBest < GroupCosts[i] ) + { + GroupCostBest = GroupCosts[i]; + GroupCostBestNum = i; + } + } + + // create the cubes with min number of literals needed for the group + LastGroup = 0; + for ( c = 0; c < nCubes; c++ ) + { + CubeNum = s_ELGroupRules[Dist][GroupCostBestNum][c]; + LastGroup |= s_BitMasks[CubeNum]; + + // bring a cube from the free cube list + ELCubes[CubeNum] = GetFreeCube(); + + // copy the input bit data into the cube + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + ELCubes[CubeNum]->pCubeDataIn[i] = DammyBitData[i]; + + // copy the output bit data into the cube + NewZ = 0; + if ( DiffVars[0] >= 0 ) // the output is not involved in ExorLink + { + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + ELCubes[CubeNum]->pCubeDataOut[i] = pCA->pCubeDataOut[i]; + NewZ = pCA->z; + } + else // the output is involved + { // determine where the output information comes from + Value = s_ELCubeRules[Dist][CubeNum][nDiffVarsIn]; + if ( Value == vs0 ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCA->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + else if ( Value == vs1 ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCB->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + else if ( Value == vsX ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCA->pCubeDataOut[i] ^ pCB->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + } + // set the number of literals + ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; + ELCubes[CubeNum]->z = NewZ; + + // set the variables that should be there + for ( i = 0; i < nDiffVarsIn; i++ ) + { + Value = DiffVarValues[i][ s_ELCubeRules[Dist][CubeNum][i] ]; + ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] ); + } + + // assign the ID + ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++; + // skip through zero-ID + if ( g_CoverInfo.cIDs == 256 ) + g_CoverInfo.cIDs = 1; + + // prepare the return array + pGroup[c] = ELCubes[CubeNum]; + } + + // mark this group as visited + VisitedGroups |= s_BitMasks[ GroupCostBestNum ]; + // set the first visited group number + GroupOrder[0] = GroupCostBestNum; + // increment the counter of visited groups + nVisitedGroups = 1; + fWorking = 1; + return 1; +} + +int ExorLinkCubeIteratorNext( Cube** pGroup ) +// give the next group in the decreasing order of sum of literals +// returns 1 on success, returns 0 if there are no more groups +{ + int i, c; + + // check that everything is okey + assert( fWorking ); + + if ( nVisitedGroups == nGroups ) + // we have iterated through all groups + return 0; + + // find the min/max cost group + if ( fMinLitGroupsFirst[nDist] ) +// if ( nCubes == 4 ) + { // find the minimum cost + // go through all groups + GroupCostBest = LARGE_NUM; + for ( i = 0; i < nGroups; i++ ) + if ( !(VisitedGroups & s_BitMasks[i]) && GroupCostBest > GroupCosts[i] ) + { + GroupCostBest = GroupCosts[i]; + GroupCostBestNum = i; + } + assert( GroupCostBest != LARGE_NUM ); + } + else + { // find the maximum cost + // go through all groups + GroupCostBest = -1; + for ( i = 0; i < nGroups; i++ ) + if ( !(VisitedGroups & s_BitMasks[i]) && GroupCostBest < GroupCosts[i] ) + { + GroupCostBest = GroupCosts[i]; + GroupCostBestNum = i; + } + assert( GroupCostBest != -1 ); + } + + // create the cubes needed for the group, if they are not created already + LastGroup = 0; + for ( c = 0; c < nCubes; c++ ) + { + CubeNum = s_ELGroupRules[nDist][GroupCostBestNum][c]; + LastGroup |= s_BitMasks[CubeNum]; + + if ( ELCubes[CubeNum] == NULL ) // this cube does not exist + { + // bring a cube from the free cube list + ELCubes[CubeNum] = GetFreeCube(); + + // copy the input bit data into the cube + for ( i = 0; i < g_CoverInfo.nWordsIn; i++ ) + ELCubes[CubeNum]->pCubeDataIn[i] = DammyBitData[i]; + + // copy the output bit data into the cube + NewZ = 0; + if ( DiffVars[0] >= 0 ) // the output is not involved in ExorLink + { + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + ELCubes[CubeNum]->pCubeDataOut[i] = pCA->pCubeDataOut[i]; + NewZ = pCA->z; + } + else // the output is involved + { // determine where the output information comes from + Value = s_ELCubeRules[nDist][CubeNum][nDiffVarsIn]; + if ( Value == vs0 ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCA->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + else if ( Value == vs1 ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCB->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + else if ( Value == vsX ) + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + Temp = pCA->pCubeDataOut[i] ^ pCB->pCubeDataOut[i]; + ELCubes[CubeNum]->pCubeDataOut[i] = Temp; + NewZ += BIT_COUNT(Temp); + } + } + // set the number of literals and output ones + ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; + ELCubes[CubeNum]->z = NewZ; + + assert( NewZ != 255 ); + + // set the variables that should be there + for ( i = 0; i < nDiffVarsIn; i++ ) + { + Value = DiffVarValues[i][ s_ELCubeRules[nDist][CubeNum][i] ]; + ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] ); + } + + // assign the ID + ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++; + // skip through zero-ID + if ( g_CoverInfo.cIDs == 256 ) + g_CoverInfo.cIDs = 1; + + } + // prepare the return array + pGroup[c] = ELCubes[CubeNum]; + } + + // mark this group as visited + VisitedGroups |= s_BitMasks[ GroupCostBestNum ]; + // set the next visited group number and + // increment the counter of visited groups + GroupOrder[ nVisitedGroups++ ] = GroupCostBestNum; + return 1; +} + +int ExorLinkCubeIteratorPick( Cube** pGroup, int g ) +// gives the group #g in the order in which the groups were given +// during iteration +// returns 1 on success, returns 0 if something is wrong (g is too large) +{ + int GroupNum, c; + + assert( fWorking ); + assert( g >= 0 && g < nGroups ); + assert( VisitedGroups & s_BitMasks[g] ); + + GroupNum = GroupOrder[g]; + // form the group + LastGroup = 0; + for ( c = 0; c < nCubes; c++ ) + { + CubeNum = s_ELGroupRules[nDist][GroupNum][c]; + + // remember this group as the last one + LastGroup |= s_BitMasks[CubeNum]; + + assert( ELCubes[CubeNum] != NULL ); // this cube should exist + // prepare the return array + pGroup[c] = ELCubes[CubeNum]; + } + return 1; +} + +void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup ) +// removes the cubes from the store back into the list of free cubes +// if fTakeLastGroup is 0, removes all cubes +// if fTakeLastGroup is 1, does not store the last group +{ + int c; + assert( fWorking ); + + // put cubes back + // set the cube pointers to zero + if ( fTakeLastGroup == 0 ) + for ( c = 0; c < nCubesInGroup; c++ ) + { + ELCubes[c]->fMark = 0; + AddToFreeCubes( ELCubes[c] ); + ELCubes[c] = NULL; + } + else + for ( c = 0; c < nCubesInGroup; c++ ) + if ( ELCubes[c] ) + { + ELCubes[c]->fMark = 0; + if ( (LastGroup & s_BitMasks[c]) == 0 ) // does not belong to the last group + AddToFreeCubes( ELCubes[c] ); + ELCubes[c] = NULL; + } + + // set the cube groups to zero + VisitedGroups = 0; + // shut down the iterator + fWorking = 0; +} + + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/exor/exorList.c b/src/base/exor/exorList.c new file mode 100644 index 00000000..6388fbe3 --- /dev/null +++ b/src/base/exor/exorList.c @@ -0,0 +1,1140 @@ +/**CFile**************************************************************** + + FileName [exorList.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Cube lists.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exorList.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Iterative Cube Set Minimization /// +/// Iterative ExorLink Procedure /// +/// Support of Cube Pair Queques /// +/// /// +/// Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000 /// +/// Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000 /// +/// Ver. 1.2. Started - July 30, 2000. Last update - July 31, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 26, 2000 /// +/// Ver. 1.5. Started - Aug 30, 2000. Last update - Aug 30, 2000 /// +/// Ver. 1.6. Started - Sep 11, 2000. Last update - Sep 15, 2000 /// +/// Ver. 1.7. Started - Sep 20, 2000. Last update - Sep 23, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// information about options and the cover +extern cinfo g_CoverInfo; + +// the look-up table for the number of 1's in unsigned short +extern unsigned char BitCount[]; + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int GetDistance( Cube* pC1, Cube* pC2 ); +// distance computation for two cubes +extern int GetDistancePlus( Cube* pC1, Cube* pC2 ); + +extern void ExorVar( Cube* pC, int Var, varvalue Val ); + +extern void AddToFreeCubes( Cube* pC ); +// returns a simplified cube back into the free list + +//extern void PrintCube( ostream& DebugStream, Cube* pC ); +// debug output for cubes + +extern Cube* GetFreeCube(); + +//////////////////////////////////////////////////////////////////////// +/// ExorLink Functions +extern int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist ); +// this function starts the Exor-Link IteratorCubePair, which iterates +// through the cube groups starting from the group with min literals +// returns 1 on success, returns 0 if the cubes have wrong distance + +extern int ExorLinkCubeIteratorNext( Cube** pGroup ); +// give the next group in the decreasing order of sum of literals +// returns 1 on success, returns 0 if there are no more groups + +extern int ExorLinkCubeIteratorPick( Cube** pGroup, int g ); +// gives the group #g in the order in which the groups were given +// during iteration +// returns 1 on success, returns 0 if something g is too large + +extern void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup ); +// removes the cubes from the store back into the list of free cubes +// if fTakeLastGroup is 0, removes all cubes +// if fTakeLastGroup is 1, does not store the last group + +//////////////////////////////////////////////////////////////////////// +/// FUNCTIONS OF THIS MODULE /// +//////////////////////////////////////////////////////////////////////// + +// iterative ExorLink +int IterativelyApplyExorLink2( char fDistEnable ); +int IterativelyApplyExorLink3( char fDistEnable ); +int IterativelyApplyExorLink4( char fDistEnable ); + +// function which performs distance computation and simplifes on the fly +// it is also called from the Pseudo-Kronecker module when cubes are added +int CheckForCloseCubes( Cube* p, int fAddCube ); +int CheckAndInsert( Cube* p ); + +// this function changes the cube back after it was DIST-1 transformed +void UndoRecentChanges(); + +//////////////////////////////////////////////////////////////////////// +// iterating through adjucency pair queques (with authomatic garbage collection) + +// start an iterator through cubes of dist CubeDist, +// the resulting pointers are written into ppC1 and ppC2 +int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 ); +// gives the next VALID cube pair (the previous one is automatically dequequed) +int IteratorCubePairNext(); + +//////////////////////////////////////////////////////////////////////// +// the cube storage + +// cube storage allocation/delocation +int AllocateCubeSets( int nVarsIn, int nVarsOut ); +void DelocateCubeSets(); + +// insert/extract a cube into/from the storage +void CubeInsert( Cube* p ); +Cube* CubeExtract( Cube* p ); + +//////////////////////////////////////////////////////////////////////// +// Cube Set Iterator +Cube* IterCubeSetStart(); +// starts an iterator that traverses all the cubes in the ring +Cube* IterCubeSetNext(); +// returns the next cube in the ring +// to use it again after it has returned NULL, call IterCubeSetStart() first + +//////////////////////////////////////////////////////////////////////// +// cube adjacency queques + +// adjacency queque allocation/delocation procedures +int AllocateQueques( int nPlaces ); +void DelocateQueques(); + +// conditional adding cube pairs to queques +// reset temporarily stored new range of cube pairs +static void NewRangeReset(); +// add temporarily stored new range of cube pairs to the queque +static void NewRangeAdd(); +// insert one cube pair into the new range +static void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 ); + +static void MarkSet(); +static void MarkRewind(); + +void PrintQuequeStats(); +int GetQuequeStats( cubedist Dist ); + +// iterating through the queque (with authomatic garbage collection) +// start an iterator through cubes of dist CubeDist, +// the resulting pointers are written into ppC1 and ppC2 +int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 ); +// gives the next VALID cube pair (the previous one is automatically dequequed) +int IteratorCubePairNext(); + +//////////////////////////////////////////////////////////////////////// +/// EXPORTED VARIABLES /// +////////////////////////////////////////////////////////////////////////` + +// the number of allocated places +int s_nPosAlloc; +// the maximum number of occupied places +int s_nPosMax[3]; + +//////////////////////////////////////////////////////////////////////// +/// Minimization Strategy /// +//////////////////////////////////////////////////////////////////////// + +// 1) check that ExorLink for this cube pair can be performed +// (it may happen that the group is outdated due to recent reshaping) +// 2) find out what is the improvement achieved by each cube group +// 3) depending on the distance, do the following: +// a) if ( Dist == 2 ) +// try both cube groups, +// if one of them leads to improvement, take the cube group right away +// if none of them leads to improment +// - take the last one (because it reshapes) +// - take the last one only in case it does not increase literals +// b) if ( Dist == 3 ) +// try groups one by one +// if one of them leads to improvement, take the group right away +// if none of them leads to improvement +// - take the group which reshapes +// - take the reshaping group only in case it does not increase literals +// if none of them leads to reshaping, do not take any of them +// c) if ( Dist == 4 ) +// try groups one by one +// if one of the leads to reshaping, take it right away +// if none of them leads to reshaping, do not take any of them + +//////////////////////////////////////////////////////////////////////// +/// STATIC VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +// Cube set is a list of cubes +static Cube* s_List; + +/////////////////////////////////////////////////////////////////////////// +// undo information +/////////////////////////////////////////////////////////////////////////// +static struct +{ + int fInput; // 1 if the input was changed + Cube* p; // the pointer to the modified cube + int PrevQa; + int PrevPa; + int PrevPz; + int Var; // the number of variable that was changed + int Value; // the value what was there + int PrevID; // the previous ID of the removed cube +} s_ChangeStore; +/////////////////////////////////////////////////////////////////////////// + +// enable pair accumulation +// from the begginning (while the starting cover is generated) +// only the distance 2 accumulation is enabled +static int s_fDistEnable2 = 1; +static int s_fDistEnable3; +static int s_fDistEnable4; + +// temporary storage for cubes generated by the ExorLink iterator +static Cube* s_CubeGroup[5]; +// the marks telling whether the given cube is inserted +static int s_fInserted[5]; + +// enable selection only those Dist2 and Dist3 that do not increase literals +int s_fDecreaseLiterals = 0; + +// the counters for display +static int s_cEnquequed; +static int s_cAttempts; +static int s_cReshapes; + +// the number of cubes before ExorLink starts +static int s_nCubesBefore; +// the distance code specific for each ExorLink +static cubedist s_Dist; + +// other variables +static int s_Gain; +static int s_GainTotal; +static int s_GroupCounter; +static int s_GroupBest; +static Cube *s_pC1, *s_pC2; + +//////////////////////////////////////////////////////////////////////// +/// Iterative ExorLink Operation /// +//////////////////////////////////////////////////////////////////////// + +int CheckAndInsert( Cube* p ) +{ +// return CheckForCloseCubes( p, 1 ); + CubeInsert( p ); + return 0; +} + +int IterativelyApplyExorLink2( char fDistEnable ) +// MEMO: instead of inserting the cubes that have already been checked +// by running CheckForCloseCubes again, try inserting them without checking +// and observe the difference (it will save 50% of checking time) +{ + int z; + + // this var is specific to ExorLink-2 + s_Dist = (cubedist)0; + + // enable pair accumulation + s_fDistEnable2 = fDistEnable & 1; + s_fDistEnable3 = fDistEnable & 2; + s_fDistEnable4 = fDistEnable & 4; + + // initialize counters + s_cEnquequed = GetQuequeStats( s_Dist ); + s_cAttempts = 0; + s_cReshapes = 0; + + // remember the number of cubes before minimization + s_nCubesBefore = g_CoverInfo.nCubesInUse; + + for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() ) + { + s_cAttempts++; + // start ExorLink of the given Distance + if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) ) + { + // extract old cubes from storage (to prevent EXORing with their derivitives) + CubeExtract( s_pC1 ); + CubeExtract( s_pC2 ); + + // mark the current position in the cube pair queques + MarkSet(); + + // check the first group (generated by ExorLinkCubeIteratorStart()) + if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) + { // the first cube leads to improvement - it is already inserted + CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube + goto SUCCESS; + } + if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) + { // the second cube leads to improvement - it is already inserted + CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube +// CheckAndInsert( s_CubeGroup[0] ); + goto SUCCESS; + } + // the first group does not lead to improvement + + // rewind to the previously marked position in the cube pair queques + MarkRewind(); + + // generate the second group + ExorLinkCubeIteratorNext( s_CubeGroup ); + + // check the second group + if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) + { // the first cube leads to improvement - it is already inserted + CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube + goto SUCCESS; + } + if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) + { // the second cube leads to improvement - it is already inserted + CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube +// CheckAndInsert( s_CubeGroup[0] ); + goto SUCCESS; + } + // the second group does not lead to improvement + + // decide whether to accept the second group, depending on literals + if ( s_fDecreaseLiterals ) + { + if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a ) + // the group increases literals + { // do not take the last group + + // rewind to the previously marked position in the cube pair queques + MarkRewind(); + + // return the old cubes back to storage + CubeInsert( s_pC1 ); + CubeInsert( s_pC2 ); + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 0 ); + continue; + } + } + + // take the last group + // there is no need to test these cubes again, + // because they have been tested and did not yield any improvement + CubeInsert( s_CubeGroup[0] ); + CubeInsert( s_CubeGroup[1] ); +// CheckForCloseCubes( s_CubeGroup[0], 1 ); +// CheckForCloseCubes( s_CubeGroup[1], 1 ); + +SUCCESS: + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 1 ); // take the last group + // free old cubes + AddToFreeCubes( s_pC1 ); + AddToFreeCubes( s_pC2 ); + // increate the counter + s_cReshapes++; + } + } + // print the report + if ( g_CoverInfo.Verbosity == 2 ) + { + printf( "ExLink-%d", 2 ); + printf( ": Que= %5d", s_cEnquequed ); + printf( " Att= %4d", s_cAttempts ); + printf( " Resh= %4d", s_cReshapes ); + printf( " NoResh= %4d", s_cAttempts - s_cReshapes ); + printf( " Cubes= %3d", g_CoverInfo.nCubesInUse ); + printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse ); + printf( "\n" ); + } + + // return the number of cubes gained in the process + return s_nCubesBefore - g_CoverInfo.nCubesInUse; +} + +int IterativelyApplyExorLink3( char fDistEnable ) +{ + int z, c, d; + // this var is specific to ExorLink-3 + s_Dist = (cubedist)1; + + // enable pair accumulation + s_fDistEnable2 = fDistEnable & 1; + s_fDistEnable3 = fDistEnable & 2; + s_fDistEnable4 = fDistEnable & 4; + + // initialize counters + s_cEnquequed = GetQuequeStats( s_Dist ); + s_cAttempts = 0; + s_cReshapes = 0; + + // remember the number of cubes before minimization + s_nCubesBefore = g_CoverInfo.nCubesInUse; + + for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() ) + { + s_cAttempts++; + // start ExorLink of the given Distance + if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) ) + { + // extract old cubes from storage (to prevent EXORing with their derivitives) + CubeExtract( s_pC1 ); + CubeExtract( s_pC2 ); + + // mark the current position in the cube pair queques + MarkSet(); + + // check cube groups one by one + s_GroupCounter = 0; + do + { // check the cubes of this group one by one + for ( c = 0; c < 3; c++ ) + if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked + { + s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default + if ( s_Gain ) + { // this cube leads to improvement or reshaping - it is already inserted + + // decide whether to accept this group based on literal count + if ( s_fDecreaseLiterals && s_Gain == 1 ) + if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a + s_CubeGroup[2]->a > + s_pC1->a + s_pC2->a + s_ChangeStore.PrevQa ) // the group increases literals + { // do not take this group + // remember the group + s_GroupBest = s_GroupCounter; + // undo changes to be able to continue checking other groups + UndoRecentChanges(); + break; + } + + // take this group + for ( d = 0; d < 3; d++ ) // insert other cubes + if ( d != c ) + { + CheckForCloseCubes( s_CubeGroup[d], 1 ); +// if ( s_CubeGroup[d]->fMark ) +// CheckAndInsert( s_CubeGroup[d] ); +// CheckOnlyOneCube( s_CubeGroup[d] ); +// CheckForCloseCubes( s_CubeGroup[d], 1 ); +// else +// CheckForCloseCubes( s_CubeGroup[d], 1 ); + } + + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 1 ); // take the last group + // free old cubes + AddToFreeCubes( s_pC1 ); + AddToFreeCubes( s_pC2 ); + // update the counter + s_cReshapes++; + goto END_OF_LOOP; + } + else // mark the cube as checked + s_CubeGroup[c]->fMark = 1; + } + // the group is not taken - find the new group + s_GroupCounter++; + + // rewind to the previously marked position in the cube pair queques + MarkRewind(); + } + while ( ExorLinkCubeIteratorNext( s_CubeGroup ) ); + // none of the groups leads to improvement + + // return the old cubes back to storage + CubeInsert( s_pC1 ); + CubeInsert( s_pC2 ); + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 0 ); + } +END_OF_LOOP: {} + } + + // print the report + if ( g_CoverInfo.Verbosity == 2 ) + { + printf( "ExLink-%d", 3 ); + printf( ": Que= %5d", s_cEnquequed ); + printf( " Att= %4d", s_cAttempts ); + printf( " Resh= %4d", s_cReshapes ); + printf( " NoResh= %4d", s_cAttempts - s_cReshapes ); + printf( " Cubes= %3d", g_CoverInfo.nCubesInUse ); + printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse ); + printf( "\n" ); + } + + // return the number of cubes gained in the process + return s_nCubesBefore - g_CoverInfo.nCubesInUse; +} + +int IterativelyApplyExorLink4( char fDistEnable ) +{ + int z, c; + // this var is specific to ExorLink-4 + s_Dist = (cubedist)2; + + // enable pair accumulation + s_fDistEnable2 = fDistEnable & 1; + s_fDistEnable3 = fDistEnable & 2; + s_fDistEnable4 = fDistEnable & 4; + + // initialize counters + s_cEnquequed = GetQuequeStats( s_Dist ); + s_cAttempts = 0; + s_cReshapes = 0; + + // remember the number of cubes before minimization + s_nCubesBefore = g_CoverInfo.nCubesInUse; + + for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() ) + { + s_cAttempts++; + // start ExorLink of the given Distance + if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) ) + { + // extract old cubes from storage (to prevent EXORing with their derivitives) + CubeExtract( s_pC1 ); + CubeExtract( s_pC2 ); + + // mark the current position in the cube pair queques + MarkSet(); + + // check cube groups one by one + do + { // check the cubes of this group one by one + s_GainTotal = 0; + for ( c = 0; c < 4; c++ ) + if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked + { + s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default + // if the cube leads to gain, it is already inserted + s_fInserted[c] = (int)(s_Gain>0); + // increment the total gain + s_GainTotal += s_Gain; + } + else + s_fInserted[c] = 0; // the cube has already been checked - it is not inserted + + if ( s_GainTotal == 0 ) // the group does not lead to any gain + { // mark the cubes + for ( c = 0; c < 4; c++ ) + s_CubeGroup[c]->fMark = 1; + } + else if ( s_GainTotal == 1 ) // the group does not lead to substantial gain, too + { + // undo changes to be able to continue checking groups + UndoRecentChanges(); + // mark those cubes that were not inserted + for ( c = 0; c < 4; c++ ) + s_CubeGroup[c]->fMark = !s_fInserted[c]; + } + else // if ( s_GainTotal > 1 ) // the group reshapes or improves + { // accept the group + for ( c = 0; c < 4; c++ ) // insert other cubes + if ( !s_fInserted[c] ) + CheckForCloseCubes( s_CubeGroup[c], 1 ); +// CheckAndInsert( s_CubeGroup[c] ); + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 1 ); // take the last group + // free old cubes + AddToFreeCubes( s_pC1 ); + AddToFreeCubes( s_pC2 ); + // update the counter + s_cReshapes++; + goto END_OF_LOOP; + } + + // rewind to the previously marked position in the cube pair queques + MarkRewind(); + } + while ( ExorLinkCubeIteratorNext( s_CubeGroup ) ); + // none of the groups leads to improvement + + // return the old cubes back to storage + CubeInsert( s_pC1 ); + CubeInsert( s_pC2 ); + // clean the results of generating ExorLinked cubes + ExorLinkCubeIteratorCleanUp( 0 ); + } +END_OF_LOOP: {} + } + + // print the report + if ( g_CoverInfo.Verbosity == 2 ) + { + printf( "ExLink-%d", 4 ); + printf( ": Que= %5d", s_cEnquequed ); + printf( " Att= %4d", s_cAttempts ); + printf( " Resh= %4d", s_cReshapes ); + printf( " NoResh= %4d", s_cAttempts - s_cReshapes ); + printf( " Cubes= %3d", g_CoverInfo.nCubesInUse ); + printf( " (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse ); + printf( "\n" ); + } + + // return the number of cubes gained in the process + return s_nCubesBefore - g_CoverInfo.nCubesInUse; +} + +// local static variables +Cube* s_q; +int s_Distance; +int s_DiffVarNum; +int s_DiffVarValueP_old; +int s_DiffVarValueP_new; +int s_DiffVarValueQ; + +int CheckForCloseCubes( Cube* p, int fAddCube ) +// checks the cube storage for a cube that is dist-0 and dist-1 removed +// from the given one (p) if such a cube is found, extracts it from the data +// structure, EXORs it with the given cube, adds the resultant cube +// to the data structure and performed the same check for the resultant cube; +// returns the number of cubes gained in the process of reduction; +// if an adjacent cube is not found, inserts the cube only if (fAddCube==1)!!! +{ + // start the new range + NewRangeReset(); + + for ( s_q = s_List; s_q; s_q = s_q->Next ) + { + s_Distance = GetDistancePlus( p, s_q ); + if ( s_Distance > 4 ) + { + } + else if ( s_Distance == 4 ) + { + if ( s_fDistEnable4 ) + NewRangeInsertCubePair( DIST4, p, s_q ); + } + else if ( s_Distance == 3 ) + { + if ( s_fDistEnable3 ) + NewRangeInsertCubePair( DIST3, p, s_q ); + } + else if ( s_Distance == 2 ) + { + if ( s_fDistEnable2 ) + NewRangeInsertCubePair( DIST2, p, s_q ); + } + else if ( s_Distance == 1 ) + { // extract the cube from the data structure + + ////////////////////////////////////////////////////////// + // store the changes + s_ChangeStore.fInput = (s_DiffVarNum != -1); + s_ChangeStore.p = p; + s_ChangeStore.PrevQa = s_q->a; + s_ChangeStore.PrevPa = p->a; + s_ChangeStore.PrevPz = p->z; + s_ChangeStore.Var = s_DiffVarNum; + s_ChangeStore.Value = s_DiffVarValueQ; + s_ChangeStore.PrevID = s_q->ID; + ////////////////////////////////////////////////////////// + + CubeExtract( s_q ); + // perform the EXOR of the two cubes and write the result into p + + // it is important that the resultant cube is written into p!!! + + if ( s_DiffVarNum == -1 ) + { + int i; + // exor the output part + p->z = 0; + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + { + p->pCubeDataOut[i] ^= s_q->pCubeDataOut[i]; + p->z += BIT_COUNT(p->pCubeDataOut[i]); + } + } + else + { + // the cube has already been updated by GetDistancePlus() + + // modify the parameters of the number of literals in the new cube +// p->a += s_UpdateLiterals[ s_DiffVarValueP ][ s_DiffVarValueQ ]; + if ( s_DiffVarValueP_old == VAR_NEG || s_DiffVarValueP_old == VAR_POS ) + p->a--; + if ( s_DiffVarValueP_new == VAR_NEG || s_DiffVarValueP_new == VAR_POS ) + p->a++; + } + + // move q to the free cube list + AddToFreeCubes( s_q ); + + // make sure that nobody with use the pairs created so far +// NewRangeReset(); + // call the function again for the new cube + return 1 + CheckForCloseCubes( p, 1 ); + } + else // if ( Distance == 0 ) + { // extract the second cube from the data structure and add them both to the free list + AddToFreeCubes( p ); + AddToFreeCubes( CubeExtract( s_q ) ); + + // make sure that nobody with use the pairs created so far + NewRangeReset(); + return 2; + } + } + + // add the cube to the data structure if needed + if ( fAddCube ) + CubeInsert( p ); + + // add temporarily stored new range of cube pairs to the queque + NewRangeAdd(); + + return 0; +} + +void UndoRecentChanges() +{ + Cube * p, * q; + // get back cube q that was deleted + q = GetFreeCube(); + // restore the ID + q->ID = s_ChangeStore.PrevID; + // insert the cube into storage again + CubeInsert( q ); + + // extract cube p + p = CubeExtract( s_ChangeStore.p ); + + // modify it back + if ( s_ChangeStore.fInput ) // the input has changed + { + ExorVar( p, s_ChangeStore.Var, (varvalue)s_ChangeStore.Value ); + p->a = s_ChangeStore.PrevPa; + // p->z did not change + } + else // if ( s_ChangeStore.fInput ) // the output has changed + { + int i; + for ( i = 0; i < g_CoverInfo.nWordsOut; i++ ) + p->pCubeDataOut[i] ^= q->pCubeDataOut[i]; + p->z = s_ChangeStore.PrevPz; + // p->a did not change + } +} + +/////////////////////////////////////////////////////////////////// +/// CUBE SET MANIPULATION PROCEDURES /// +/////////////////////////////////////////////////////////////////// + +// Cube set is a list of cubes +//static Cube* s_List; + +/////////////////////////////////////////////////////////////////// +/// Memory Allocation/Delocation /// +/////////////////////////////////////////////////////////////////// + +int AllocateCubeSets( int nVarsIn, int nVarsOut ) +{ + s_List = NULL; + + // clean other data + s_fDistEnable2 = 1; + s_fDistEnable3 = 0; + s_fDistEnable4 = 0; + memset( s_CubeGroup, 0, sizeof(void *) * 5 ); + memset( s_fInserted, 0, sizeof(int) * 5 ); + s_fDecreaseLiterals = 0; + s_cEnquequed = 0; + s_cAttempts = 0; + s_cReshapes = 0; + s_nCubesBefore = 0; + s_Gain = 0; + s_GainTotal = 0; + s_GroupCounter = 0; + s_GroupBest = 0; + s_pC1 = s_pC2 = NULL; + + return 4; +} + +void DelocateCubeSets() +{ +} + +/////////////////////////////////////////////////////////////////// +/// Insertion Operators /// +/////////////////////////////////////////////////////////////////// + +void CubeInsert( Cube* p ) +// inserts the cube into storage (puts it at the beginning of the list) +{ + assert( p->Prev == NULL && p->Next == NULL ); + assert( p->ID ); + + if ( s_List == NULL ) + s_List = p; + else + { + p->Next = s_List; + + s_List->Prev = p; + s_List = p; + } + + g_CoverInfo.nCubesInUse++; +} + +Cube* CubeExtract( Cube* p ) +// extracts the cube from storage +{ +// assert( p->Prev && p->Next ); // can be done only with rings + assert( p->ID ); + +// if ( s_List == p ) +// s_List = p->Next; +// if ( p->Prev ) +// p->Prev->Next = p->Next; + + if ( s_List == p ) + s_List = p->Next; + else + p->Prev->Next = p->Next; + + if ( p->Next ) + p->Next->Prev = p->Prev; + + p->Prev = NULL; + p->Next = NULL; + + g_CoverInfo.nCubesInUse--; + return p; +} + +/////////////////////////////////////////////////////////////////// +/// CUBE ITERATOR /// +/////////////////////////////////////////////////////////////////// + +// the iterator starts from the Head and stops when it sees NULL +Cube* s_pCubeLast; + +/////////////////////////////////////////////////////////////////// +/// Cube Set Iterator /// +/////////////////////////////////////////////////////////////////// + +Cube* IterCubeSetStart() +// starts an iterator that traverses all the cubes in the ring +{ + assert( s_pCubeLast == NULL ); + + // check whether the List has cubes + if ( s_List == NULL ) + return NULL; + + return ( s_pCubeLast = s_List ); +} + +Cube* IterCubeSetNext() +// returns the next cube in the cube set +// to use it again after it has returned NULL, first call IterCubeSetStart() +{ + assert( s_pCubeLast ); + return ( s_pCubeLast = s_pCubeLast->Next ); +} + +/////////////////////////////////////////////////////////////////// +//// ADJACENCY QUEQUES ////// +/////////////////////////////////////////////////////////////////// + +typedef struct +{ + Cube** pC1; // the pointer to the first cube + Cube** pC2; // the pointer to the second cube + byte* ID1; // the ID of the first cube + byte* ID2; // the ID of the second cube + int PosOut; // extract position + int PosIn; // insert position + int PosCur; // temporary insert position + int PosMark; // the marked position + int fEmpty; // this flag is 1 if there is nothing in the queque +} que; + +static que s_Que[3]; // Dist-2, Dist-3, Dist-4 queques + +// the number of allocated places +//int s_nPosAlloc; +// the maximum number of occupied places +//int s_nPosMax[3]; + +////////////////////////////////////////////////////////////////////// +// Conditional Adding Cube Pairs To Queques // +////////////////////////////////////////////////////////////////////// + +int GetPosDiff( int PosBeg, int PosEnd ) +{ + return (PosEnd - PosBeg + s_nPosAlloc) % s_nPosAlloc; +} + +void MarkSet() +// sets marks in the cube pair queques +{ + s_Que[0].PosMark = s_Que[0].PosIn; + s_Que[1].PosMark = s_Que[1].PosIn; + s_Que[2].PosMark = s_Que[2].PosIn; +} + +void MarkRewind() +// rewinds the queques to the previously set marks +{ + s_Que[0].PosIn = s_Que[0].PosMark; + s_Que[1].PosIn = s_Que[1].PosMark; + s_Que[2].PosIn = s_Que[2].PosMark; +} + +void NewRangeReset() +// resets temporarily stored new range of cube pairs +{ + s_Que[0].PosCur = s_Que[0].PosIn; + s_Que[1].PosCur = s_Que[1].PosIn; + s_Que[2].PosCur = s_Que[2].PosIn; +} + +void NewRangeAdd() +// adds temporarily stored new range of cube pairs to the queque +{ + s_Que[0].PosIn = s_Que[0].PosCur; + s_Que[1].PosIn = s_Que[1].PosCur; + s_Que[2].PosIn = s_Que[2].PosCur; +} + +void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 ) +// insert one cube pair into the new range +{ + que* p = &s_Que[Dist]; + int Pos = p->PosCur; + + if ( p->fEmpty || Pos != p->PosOut ) + { + p->pC1[Pos] = p1; + p->pC2[Pos] = p2; + p->ID1[Pos] = p1->ID; + p->ID2[Pos] = p2->ID; + + p->PosCur = (p->PosCur+1)%s_nPosAlloc; + } + else + assert(0); +// cout << endl << "DIST-" << (int)(Dist+2) << ": Have run out of queque space!" << endl; +} + +void PrintQuequeStats() +{ +/* + cout << endl << "Queque statistics: "; + cout << " Alloc = " << s_nPosAlloc; + cout << " DIST2 = " << GetPosDiff( s_Que[0].PosOut, s_Que[0].PosIn ); + cout << " DIST3 = " << GetPosDiff( s_Que[1].PosOut, s_Que[1].PosIn ); + cout << " DIST4 = " << GetPosDiff( s_Que[2].PosOut, s_Que[2].PosIn ); + cout << endl; + cout << endl; +*/ +} + +int GetQuequeStats( cubedist Dist ) +{ + return GetPosDiff( s_Que[Dist].PosOut, s_Que[Dist].PosIn ); +} + +////////////////////////////////////////////////////////////////////// +// Queque Iterators // +////////////////////////////////////////////////////////////////////// + +// iterating through the queque (with authomatic garbage collection) +// only one iterator can be active at a time +static struct +{ + int fStarted; // status of the iterator (1 if working) + cubedist Dist; // the currently iterated queque + Cube** ppC1; // the position where the first cube pointer goes + Cube** ppC2; // the position where the second cube pointer goes + int PosStop; // the stop position (to prevent the iterator from + // choking when new pairs are added during iteration) + int CutValue; // the number of literals below which the cubes are not used +} s_Iter; + +static que* pQ; +static Cube *p1, *p2; + +int IteratorCubePairStart( cubedist CubeDist, Cube** ppC1, Cube** ppC2 ) +// start an iterator through cubes of dist CubeDist, +// the resulting pointers are written into ppC1 and ppC2 +// returns 1 if the first cube pair is found +{ + int fEntryFound; + + assert( s_Iter.fStarted == 0 ); + assert( CubeDist >= 0 && CubeDist <= 2 ); + + s_Iter.fStarted = 1; + s_Iter.Dist = CubeDist; + s_Iter.ppC1 = ppC1; + s_Iter.ppC2 = ppC2; + + s_Iter.PosStop = s_Que[ CubeDist ].PosIn; + + // determine the cut value +// s_Iter.CutValue = s_nLiteralsInUse/s_nCubesInUse/2; + s_Iter.CutValue = -1; + + fEntryFound = 0; + // go through the entries while there is something in the queque + for ( pQ = &s_Que[ CubeDist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc ) + { + p1 = pQ->pC1[ pQ->PosOut ]; + p2 = pQ->pC2[ pQ->PosOut ]; + + // check whether the entry is valid + if ( p1->ID == pQ->ID1[ pQ->PosOut ] && + p2->ID == pQ->ID2[ pQ->PosOut ] ) //&& + //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue ) + { + fEntryFound = 1; + break; + } + } + + if ( fEntryFound ) + { // write the result into the pick-up place + *ppC1 = pQ->pC1[ pQ->PosOut ]; + *ppC2 = pQ->pC2[ pQ->PosOut ]; + + pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc; + } + else + s_Iter.fStarted = 0; + return fEntryFound; +} + +int IteratorCubePairNext() +// gives the next VALID cube pair (the previous one is automatically dequequed) +{ + int fEntryFound = 0; + assert( s_Iter.fStarted ); + + // go through the entries while there is something in the queque + for ( pQ = &s_Que[ s_Iter.Dist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc ) + { + p1 = pQ->pC1[ pQ->PosOut ]; + p2 = pQ->pC2[ pQ->PosOut ]; + + // check whether the entry is valid + if ( p1->ID == pQ->ID1[ pQ->PosOut ] && + p2->ID == pQ->ID2[ pQ->PosOut ] ) //&& + //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue ) + { + fEntryFound = 1; + break; + } + } + + if ( fEntryFound ) + { // write the result into the pick-up place + *(s_Iter.ppC1) = pQ->pC1[ pQ->PosOut ]; + *(s_Iter.ppC2) = pQ->pC2[ pQ->PosOut ]; + + pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc; + } + else // iteration has finished + s_Iter.fStarted = 0; + + return fEntryFound; +} + +////////////////////////////////////////////////////////////////////// +// Allocation/Delocation // +////////////////////////////////////////////////////////////////////// + +int AllocateQueques( int nPlaces ) +// nPlaces should be approximately nCubes*nCubes/10 +// allocates memory for cube pair queques +{ + int i; + s_nPosAlloc = nPlaces; + + for ( i = 0; i < 3; i++ ) + { + // clean data + memset( &s_Que[i], 0, sizeof(que) ); + + s_Que[i].pC1 = (Cube**) ABC_ALLOC( Cube*, nPlaces ); + s_Que[i].pC2 = (Cube**) ABC_ALLOC( Cube*, nPlaces ); + s_Que[i].ID1 = (byte*) ABC_ALLOC( byte, nPlaces ); + s_Que[i].ID2 = (byte*) ABC_ALLOC( byte, nPlaces ); + + if ( s_Que[i].pC1==NULL || s_Que[i].pC2==NULL || s_Que[i].ID1==NULL || s_Que[i].ID2==NULL ) + return 0; + + s_nPosMax[i] = 0; + s_Que[i].fEmpty = 1; + } + + return nPlaces * (sizeof(Cube*) + sizeof(Cube*) + 2*sizeof(byte) ); +} + +void DelocateQueques() +{ + int i; + for ( i = 0; i < 3; i++ ) + { + ABC_FREE( s_Que[i].pC1 ); + ABC_FREE( s_Que[i].pC2 ); + ABC_FREE( s_Que[i].ID1 ); + ABC_FREE( s_Que[i].ID2 ); + } +} + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c new file mode 100644 index 00000000..fb0f40f3 --- /dev/null +++ b/src/base/exor/exorUtil.c @@ -0,0 +1,204 @@ +/**CFile**************************************************************** + + FileName [exorUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Exclusive sum-of-product minimization.] + + Synopsis [Utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: exorUtil.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// /// +/// Implementation of EXORCISM - 4 /// +/// An Exclusive Sum-of-Product Minimizer /// +/// Alan Mishchenko /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// /// +/// Utility Functions /// +/// /// +/// 1) allocating memory for and creating the ESOP cover /// +/// 2) writing the resultant cover into an ESOP PLA file /// +/// /// +/// Ver. 1.0. Started - July 15, 2000. Last update - July 20, 2000 /// +/// Ver. 1.4. Started - Aug 10, 2000. Last update - Aug 10, 2000 /// +/// Ver. 1.5. Started - Aug 19, 2000. Last update - Aug 19, 2000 /// +/// Ver. 1.7. Started - Sep 20, 2000. Last update - Sep 23, 2000 /// +/// /// +//////////////////////////////////////////////////////////////////////// +/// This software was tested with the BDD package "CUDD", v.2.3.0 /// +/// by Fabio Somenzi /// +/// http://vlsi.colorado.edu/~fabio/ /// +//////////////////////////////////////////////////////////////////////// + +#include "exor.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL VARIABLES //// +//////////////////////////////////////////////////////////////////////// + +// information about the options, the function, and the cover +extern cinfo g_CoverInfo; + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +// Cube Cover Iterator +// starts an iterator that traverses all the cubes in the ring +extern Cube* IterCubeSetStart(); +// returns the next cube in the ring +extern Cube* IterCubeSetNext(); + +// retrieves the variable from the cube +extern varvalue GetVar( Cube* pC, int Var ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/////////////////////////////////////////////////////////////////// +//////////// Cover Service Procedures ///////////////// +/////////////////////////////////////////////////////////////////// + +int CountLiterals() +// nCubesAlloc is the number of allocated cubes +{ + Cube* p; + int Value, v; + int LitCounter = 0; + int LitCounterControl = 0; + + for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() ) + { + LitCounterControl += p->a; + + assert( p->fMark == 0 ); + + // write the input variables + for ( v = 0; v < g_CoverInfo.nVarsIn; v++ ) + { + Value = GetVar( p, v ); + if ( Value == VAR_NEG ) + LitCounter++; + else if ( Value == VAR_POS ) + LitCounter++; + else if ( Value != VAR_ABS ) + { + assert(0); + } + } + } + + if ( LitCounterControl != LitCounter ) + printf( "Warning! The recorded number of literals (%d) differs from the actual number (%d)\n", LitCounterControl, LitCounter ); + return LitCounter; +} + + +void WriteTableIntoFile( FILE * pFile ) +// nCubesAlloc is the number of allocated cubes +{ + int v, w; + Cube * p; + int cOutputs; + int nOutput; + int WordSize; + + for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() ) + { + assert( p->fMark == 0 ); + + // write the input variables + for ( v = 0; v < g_CoverInfo.nVarsIn; v++ ) + { + int Value = GetVar( p, v ); + if ( Value == VAR_NEG ) + fprintf( pFile, "0" ); + else if ( Value == VAR_POS ) + fprintf( pFile, "1" ); + else if ( Value == VAR_ABS ) + fprintf( pFile, "-" ); + else + assert(0); + } + fprintf( pFile, " " ); + + // write the output variables + cOutputs = 0; + nOutput = g_CoverInfo.nVarsOut; + WordSize = 8*sizeof( unsigned ); + for ( w = 0; w < g_CoverInfo.nWordsOut; w++ ) + for ( v = 0; v < WordSize; v++ ) + { + if ( p->pCubeDataOut[w] & (1< +{ + FILE * pFile; + time_t ltime; + char * TimeStr; + + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( pFile, "\n\nCannot open the output file\n" ); + return 1; + } + + // get current time + time( <ime ); + TimeStr = asctime( localtime( <ime ) ); + // get the number of literals + g_CoverInfo.nLiteralsAfter = CountLiterals(); + fprintf( pFile, "# EXORCISM-4 output for command line arguments: " ); + fprintf( pFile, "\"-Q %d -V %d\"\n", g_CoverInfo.Quality, g_CoverInfo.Verbosity ); + fprintf( pFile, "# Minimization performed %s", TimeStr ); + fprintf( pFile, "# Initial statistics: " ); + fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore ); + fprintf( pFile, "# Final statistics: " ); + fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter ); + fprintf( pFile, "# File reading and reordering time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeRead) ); + fprintf( pFile, "# Starting cover generation time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) ); + fprintf( pFile, "# Pure ESOP minimization time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) ); + fprintf( pFile, ".i %d\n", g_CoverInfo.nVarsIn ); + fprintf( pFile, ".o %d\n", g_CoverInfo.nVarsOut ); + fprintf( pFile, ".p %d\n", g_CoverInfo.nCubesInUse ); + fprintf( pFile, ".type esop\n" ); + WriteTableIntoFile( pFile ); + fprintf( pFile, ".e\n" ); + fclose( pFile ); + return 0; +} + +/////////////////////////////////////////////////////////////////// +//////////// End of File ///////////////// +/////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/exor/module.make b/src/base/exor/module.make new file mode 100644 index 00000000..842f9328 --- /dev/null +++ b/src/base/exor/module.make @@ -0,0 +1,6 @@ +SRC += src/base/exor/exor.c \ + src/base/exor/exorBits.c \ + src/base/exor/exorCubes.c \ + src/base/exor/exorLink.c \ + src/base/exor/exorList.c \ + src/base/exor/exorUtil.c diff --git a/src/base/io/io.c b/src/base/io/io.c index 83ffaf53..1abe6abf 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -903,10 +903,10 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; char * pFileName; - int c, fZeros = 0, fBoth = 0, fCheck = 1; + int c, fZeros = 0, fBoth = 0, fSkipPrepro = 0, fCheck = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "zbch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "zbxch" ) ) != EOF ) { switch ( c ) { @@ -916,6 +916,9 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fBoth ^= 1; break; + case 'x': + fSkipPrepro ^= 1; + break; case 'c': fCheck ^= 1; break; @@ -930,10 +933,10 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the input file name pFileName = argv[globalUtilOptind]; // read the file using the corresponding file reader - if ( fZeros || fBoth ) + if ( fZeros || fBoth || fSkipPrepro ) { Abc_Ntk_t * pTemp; - pNtk = Io_ReadPla( pFileName, fZeros, fBoth, fCheck ); + pNtk = Io_ReadPla( pFileName, fZeros, fBoth, fSkipPrepro, fCheck ); if ( pNtk == NULL ) { printf( "Reading PLA file has failed.\n" ); @@ -952,10 +955,11 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pAbc->Err, "usage: read_pla [-zbch] \n" ); + fprintf( pAbc->Err, "usage: read_pla [-zbxch] \n" ); fprintf( pAbc->Err, "\t reads the network in PLA\n" ); fprintf( pAbc->Err, "\t-z : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" ); fprintf( pAbc->Err, "\t-b : toggle reading both on-set and off-set as on-set [default = %s]\n", fBoth? "off-set":"on-set" ); + fprintf( pAbc->Err, "\t-x : toggle reading Exclusive SOP rather than SOP [default = %s]\n", fSkipPrepro? "yes":"no" ); fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h index aa532ec5..a1239558 100644 --- a/src/base/io/ioAbc.h +++ b/src/base/io/ioAbc.h @@ -93,7 +93,7 @@ extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ); /*=== abcReadEqn.c ============================================================*/ extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ); /*=== abcReadPla.c ============================================================*/ -extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck ); +extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fSkipPrepro, int fCheck ); /*=== abcReadVerilog.c ========================================================*/ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcWriteAiger.c =========================================================*/ diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index ceadbebc..2c261dc3 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth ); +static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, int fSkipPrepro ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -326,7 +326,7 @@ void Io_ReadPlaCubePreprocess( Vec_Str_t * vSop, int iCover, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck ) +Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fSkipPrepro, int fCheck ) { Extra_FileReader_t * p; Abc_Ntk_t * pNtk; @@ -338,7 +338,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck ) return NULL; // read the network - pNtk = Io_ReadPlaNetwork( p, fZeros, fBoth ); + pNtk = Io_ReadPlaNetwork( p, fZeros, fBoth, fSkipPrepro ); Extra_FileReaderFree( p ); if ( pNtk == NULL ) return NULL; @@ -363,7 +363,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth ) +Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, int fSkipPrepro ) { ProgressBar * pProgress; Vec_Ptr_t * vTokens; @@ -567,7 +567,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth ) continue; } Vec_StrPush( ppSops[i], 0 ); - Io_ReadPlaCubePreprocess( ppSops[i], i, 0 ); + if ( !fSkipPrepro ) + Io_ReadPlaCubePreprocess( ppSops[i], i, 0 ); pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, ppSops[i]->pArray ); Vec_StrFree( ppSops[i] ); } diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 2432079f..7e8ece6e 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -144,7 +144,7 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck else if ( FileType == IO_FILE_EQN ) pNtk = Io_ReadEqn( pFileName, fCheck ); else if ( FileType == IO_FILE_PLA ) - pNtk = Io_ReadPla( pFileName, 0, 0, fCheck ); + pNtk = Io_ReadPla( pFileName, 0, 0, 0, fCheck ); else if ( FileType == IO_FILE_VERILOG ) pNtk = Io_ReadVerilog( pFileName, fCheck ); else -- cgit v1.2.3