From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/aig/csw/csw.h | 65 ++++++ src/aig/csw/cswCore.c | 94 ++++++++ src/aig/csw/cswCut.c | 602 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/csw/cswInt.h | 157 +++++++++++++ src/aig/csw/cswMan.c | 125 ++++++++++ src/aig/csw/cswTable.c | 161 +++++++++++++ src/aig/csw/csw_.c | 48 ++++ src/aig/csw/module.make | 4 + 8 files changed, 1256 insertions(+) create mode 100644 src/aig/csw/csw.h create mode 100644 src/aig/csw/cswCore.c create mode 100644 src/aig/csw/cswCut.c create mode 100644 src/aig/csw/cswInt.h create mode 100644 src/aig/csw/cswMan.c create mode 100644 src/aig/csw/cswTable.c create mode 100644 src/aig/csw/csw_.c create mode 100644 src/aig/csw/module.make (limited to 'src/aig/csw') diff --git a/src/aig/csw/csw.h b/src/aig/csw/csw.h new file mode 100644 index 00000000..1443f4d9 --- /dev/null +++ b/src/aig/csw/csw.h @@ -0,0 +1,65 @@ +/**CFile**************************************************************** + + FileName [csw.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: csw.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CSW_H__ +#define __CSW_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cnfCore.c ========================================================*/ +extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/csw/cswCore.c b/src/aig/csw/cswCore.c new file mode 100644 index 00000000..20893058 --- /dev/null +++ b/src/aig/csw/cswCore.c @@ -0,0 +1,94 @@ +/**CFile**************************************************************** + + FileName [cswCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: cswCore.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ) +{ + Csw_Man_t * p; + Aig_Man_t * pRes; + Aig_Obj_t * pObj, * pObjNew, * pObjRes; + int i, clk; +clk = clock(); + // start the manager + p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose ); + // set elementary cuts at the PIs + Aig_ManForEachPi( p->pManRes, pObj, i ) + { + Csw_ObjPrepareCuts( p, pObj, 1 ); + Csw_ObjAddRefs( p, pObj, Aig_ManPi(p->pManAig,i)->nRefs ); + } + // process the nodes + Aig_ManForEachNode( pAig, pObj, i ) + { + // create the new node + pObjNew = Aig_And( p->pManRes, Csw_ObjChild0Equiv(p, pObj), Csw_ObjChild1Equiv(p, pObj) ); + // check if this node can be represented using another node +// pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 ); +// pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) ); + // try recursively if resubsitution is used + do { + pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 ); + pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) ); + pObjNew = pObjRes; + } while ( Csw_ObjCuts(p, Aig_Regular(pObjNew)) == NULL && !Aig_ObjIsConst1(Aig_Regular(pObjNew)) ); + // save the resulting node + Csw_ObjSetEquiv( p, pObj, pObjRes ); + // add to the reference counter + Csw_ObjAddRefs( p, Aig_Regular(pObjRes), pObj->nRefs ); + } + // add the POs + Aig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) ); + // remove dangling nodes + Aig_ManCleanup( p->pManRes ); + // return the resulting manager +p->timeTotal = clock() - clk; +p->timeOther = p->timeTotal - p->timeCuts - p->timeHash; + pRes = p->pManRes; + Csw_ManStop( p ); + return pRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/csw/cswCut.c b/src/aig/csw/cswCut.c new file mode 100644 index 00000000..b3b7152b --- /dev/null +++ b/src/aig/csw/cswCut.c @@ -0,0 +1,602 @@ +/**CFile**************************************************************** + + FileName [cswCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: cswCut.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Compute the cost of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Csw_CutFindCost( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + Aig_Obj_t * pLeaf; + int i, Cost = 0; + assert( pCut->nFanins > 0 ); + Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i ) + { +// Cost += pLeaf->nRefs; + Cost += Csw_ObjRefs( p, pLeaf ); +// printf( "%d ", pLeaf->nRefs ); + } +//printf( "\n" ); + return Cost * 100 / pCut->nFanins; +} + +/**Function************************************************************* + + Synopsis [Compute the cost of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline float Csw_CutFindCost2( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + Aig_Obj_t * pLeaf; + float Cost = 0.0; + int i; + assert( pCut->nFanins > 0 ); + Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i ) + Cost += (float)1.0/pLeaf->nRefs; + return 1/Cost; +} + +/**Function************************************************************* + + Synopsis [Returns the next free cut to use.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Csw_Cut_t * Csw_CutFindFree( Csw_Man_t * p, Aig_Obj_t * pObj ) +{ + Csw_Cut_t * pCut, * pCutMax; + int i; + pCutMax = NULL; + Csw_ObjForEachCut( p, pObj, pCut, i ) + { + if ( pCut->nFanins == 0 ) + return pCut; + if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost ) + pCutMax = pCut; + } + assert( pCutMax != NULL ); + pCutMax->nFanins = 0; + return pCutMax; +} + +/**Function************************************************************* + + Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Cut_TruthPhase( Csw_Cut_t * pCut, Csw_Cut_t * pCut1 ) +{ + unsigned uPhase = 0; + int i, k; + for ( i = k = 0; i < pCut->nFanins; i++ ) + { + if ( k == pCut1->nFanins ) + break; + if ( pCut->pFanins[i] < pCut1->pFanins[k] ) + continue; + assert( pCut->pFanins[i] == pCut1->pFanins[k] ); + uPhase |= (1 << i); + k++; + } + return uPhase; +} + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Csw_CutComputeTruth( Csw_Man_t * p, Csw_Cut_t * pCut, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, int fCompl0, int fCompl1 ) +{ + // permute the first table + if ( fCompl0 ) + Kit_TruthNot( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax ); + else + Kit_TruthCopy( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax ); + Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut0), 0 ); + // permute the second table + if ( fCompl1 ) + Kit_TruthNot( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax ); + else + Kit_TruthCopy( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax ); + Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut1), 0 ); + // produce the resulting table + Kit_TruthAnd( Csw_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax ); +// assert( pCut->nFanins >= Kit_TruthSupportSize( Csw_CutTruth(pCut), p->nLeafMax ) ); + return Csw_CutTruth(pCut); +} + +/**Function************************************************************* + + Synopsis [Performs support minimization for the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Csw_CutSupportMinimize( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + unsigned * pTruth; + int uSupp, nFansNew, i, k; + // get truth table + pTruth = Csw_CutTruth( pCut ); + // get support + uSupp = Kit_TruthSupport( pTruth, p->nLeafMax ); + // get the new support size + nFansNew = Kit_WordCountOnes( uSupp ); + // check if there are redundant variables + if ( nFansNew == pCut->nFanins ) + return nFansNew; + assert( nFansNew < pCut->nFanins ); + // minimize support + Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 ); + for ( i = k = 0; i < pCut->nFanins; i++ ) + if ( uSupp & (1 << i) ) + pCut->pFanins[k++] = pCut->pFanins[i]; + assert( k == nFansNew ); + pCut->nFanins = nFansNew; +// assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) ); +//Extra_PrintBinary( stdout, pTruth, (1<nLeafMax) ); printf( "\n" ); + return nFansNew; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pDom is contained in pCut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Csw_CutCheckDominance( Csw_Cut_t * pDom, Csw_Cut_t * pCut ) +{ + int i, k; + for ( i = 0; i < (int)pDom->nFanins; i++ ) + { + for ( k = 0; k < (int)pCut->nFanins; k++ ) + if ( pDom->pFanins[i] == pCut->pFanins[k] ) + break; + if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut + return 0; + } + // every node in pDom is contained in pCut + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cut is contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Csw_CutFilter( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCut ) +{ + Csw_Cut_t * pTemp; + int i; + // go through the cuts of the node + Csw_ObjForEachCut( p, pObj, pTemp, i ) + { + if ( pTemp->nFanins < 2 ) + continue; + if ( pTemp == pCut ) + continue; + if ( pTemp->nFanins > pCut->nFanins ) + { + // skip the non-contained cuts + if ( (pTemp->uSign & pCut->uSign) != pCut->uSign ) + continue; + // check containment seriously + if ( Csw_CutCheckDominance( pCut, pTemp ) ) + { + // remove contained cut + pTemp->nFanins = 0; + } + } + else + { + // skip the non-contained cuts + if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign ) + continue; + // check containment seriously + if ( Csw_CutCheckDominance( pTemp, pCut ) ) + { + // remove the given + pCut->nFanins = 0; + return 1; + } + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Csw_CutMergeOrdered( Csw_Man_t * p, Csw_Cut_t * pC0, Csw_Cut_t * pC1, Csw_Cut_t * pC ) +{ + int i, k, c; + assert( pC0->nFanins >= pC1->nFanins ); + // the case of the largest cut sizes + if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax ) + { + for ( i = 0; i < pC0->nFanins; i++ ) + if ( pC0->pFanins[i] != pC1->pFanins[i] ) + return 0; + for ( i = 0; i < pC0->nFanins; i++ ) + pC->pFanins[i] = pC0->pFanins[i]; + pC->nFanins = pC0->nFanins; + return 1; + } + // the case when one of the cuts is the largest + if ( pC0->nFanins == p->nLeafMax ) + { + for ( i = 0; i < pC1->nFanins; i++ ) + { + for ( k = pC0->nFanins - 1; k >= 0; k-- ) + if ( pC0->pFanins[k] == pC1->pFanins[i] ) + break; + if ( k == -1 ) // did not find + return 0; + } + for ( i = 0; i < pC0->nFanins; i++ ) + pC->pFanins[i] = pC0->pFanins[i]; + pC->nFanins = pC0->nFanins; + return 1; + } + + // compare two cuts with different numbers + i = k = 0; + for ( c = 0; c < p->nLeafMax; c++ ) + { + if ( k == pC1->nFanins ) + { + if ( i == pC0->nFanins ) + { + pC->nFanins = c; + return 1; + } + pC->pFanins[c] = pC0->pFanins[i++]; + continue; + } + if ( i == pC0->nFanins ) + { + if ( k == pC1->nFanins ) + { + pC->nFanins = c; + return 1; + } + pC->pFanins[c] = pC1->pFanins[k++]; + continue; + } + if ( pC0->pFanins[i] < pC1->pFanins[k] ) + { + pC->pFanins[c] = pC0->pFanins[i++]; + continue; + } + if ( pC0->pFanins[i] > pC1->pFanins[k] ) + { + pC->pFanins[c] = pC1->pFanins[k++]; + continue; + } + pC->pFanins[c] = pC0->pFanins[i++]; + k++; + } + if ( i < pC0->nFanins || k < pC1->nFanins ) + return 0; + pC->nFanins = c; + return 1; +} + +/**Function************************************************************* + + Synopsis [Prepares the object for FPGA mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Csw_CutMerge( Csw_Man_t * p, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, Csw_Cut_t * pCut ) +{ + assert( p->nLeafMax > 0 ); + // merge the nodes + if ( pCut0->nFanins < pCut1->nFanins ) + { + if ( !Csw_CutMergeOrdered( p, pCut1, pCut0, pCut ) ) + return 0; + } + else + { + if ( !Csw_CutMergeOrdered( p, pCut0, pCut1, pCut ) ) + return 0; + } + pCut->uSign = pCut0->uSign | pCut1->uSign; + return 1; +} + +/**Function************************************************************* + + Synopsis [Consider cut with more than 2 fanins having 2 true variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Csw_ObjTwoVarCut( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + Aig_Obj_t * pRes, * pIn0, * pIn1; + int nVars, uTruth, fCompl = 0; + assert( pCut->nFanins > 2 ); + // minimize support of this cut + nVars = Csw_CutSupportMinimize( p, pCut ); + assert( nVars == 2 ); + // get the fanins + pIn0 = Aig_ManObj( p->pManRes, pCut->pFanins[0] ); + pIn1 = Aig_ManObj( p->pManRes, pCut->pFanins[1] ); + // derive the truth table + uTruth = 0xF & *Csw_CutTruth(pCut); + if ( uTruth == 14 || uTruth == 13 || uTruth == 11 || uTruth == 7 ) + { + uTruth = 0xF & ~uTruth; + fCompl = 1; + } + // compute the result + pRes = NULL; + if ( uTruth == 1 ) // 0001 // 1110 14 + pRes = Aig_And( p->pManRes, Aig_Not(pIn0), Aig_Not(pIn1) ); + if ( uTruth == 2 ) // 0010 // 1101 13 + pRes = Aig_And( p->pManRes, pIn0 , Aig_Not(pIn1) ); + if ( uTruth == 4 ) // 0100 // 1011 11 + pRes = Aig_And( p->pManRes, Aig_Not(pIn0), pIn1 ); + if ( uTruth == 8 ) // 1000 // 0111 7 + pRes = Aig_And( p->pManRes, pIn0 , pIn1 ); + if ( pRes ) + pRes = Aig_NotCond( pRes, fCompl ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv ) +{ + Csw_Cut_t * pCutSet, * pCut; + int i; + // create the cutset of the node + pCutSet = (Csw_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts ); + Csw_ObjSetCuts( p, pObj, pCutSet ); + Csw_ObjForEachCut( p, pObj, pCut, i ) + { + pCut->nFanins = 0; + pCut->iNode = pObj->Id; + pCut->nCutSize = p->nCutSize; + pCut->nLeafMax = p->nLeafMax; + } + // add unit cut if needed + if ( fTriv ) + { + pCut = pCutSet; + pCut->Cost = 0; + pCut->iNode = pObj->Id; + pCut->nFanins = 1; + pCut->pFanins[0] = pObj->Id; + pCut->uSign = Aig_ObjCutSign( pObj->Id ); + memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords ); + } + return pCutSet; +} + +/**Function************************************************************* + + Synopsis [Derives cuts for one node and sweeps this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv ) +{ + int fUseResub = 1; + Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet; + Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj); + Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj); + Aig_Obj_t * pObjNew; + unsigned * pTruth; + int i, k, nVars, nFanins, iVar, clk; + + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) ) + return pObj; + if ( Csw_ObjCuts(p, pObj) ) + return pObj; + // the node is not processed yet + assert( Csw_ObjCuts(p, pObj) == NULL ); + assert( Aig_ObjIsNode(pObj) ); + + // set up the first cut + pCutSet = Csw_ObjPrepareCuts( p, pObj, fTriv ); + + // compute pair-wise cut combinations while checking table + Csw_ObjForEachCut( p, pFanin0, pCut0, i ) + if ( pCut0->nFanins > 0 ) + Csw_ObjForEachCut( p, pFanin1, pCut1, k ) + if ( pCut1->nFanins > 0 ) + { + // make sure K-feasible cut exists + if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax ) + continue; + // get the next cut of this node + pCut = Csw_CutFindFree( p, pObj ); +clk = clock(); + // assemble the new cut + if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) ) + { + assert( pCut->nFanins == 0 ); + continue; + } + // check containment + if ( Csw_CutFilter( p, pObj, pCut ) ) + { + assert( pCut->nFanins == 0 ); + continue; + } + // create its truth table + pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); + // support minimize the truth table + nFanins = pCut->nFanins; +// nVars = Csw_CutSupportMinimize( p, pCut ); // leads to quality degradation + nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax ); +p->timeCuts += clock() - clk; + + // check for trivial truth tables + if ( nVars == 0 ) + { + p->nNodesTriv0++; + return Aig_NotCond( Aig_ManConst1(p->pManRes), !(pTruth[0] & 1) ); + } + if ( nVars == 1 ) + { + p->nNodesTriv1++; + iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) ); + assert( iVar < pCut->nFanins ); + return Aig_NotCond( Aig_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) ); + } + if ( nVars == 2 && nFanins > 2 && fUseResub ) + { + if ( pObjNew = Csw_ObjTwoVarCut( p, pCut ) ) + { + p->nNodesTriv2++; + return pObjNew; + } + } + + // check if an equivalent node with the same cut exists +clk = clock(); + pObjNew = pCut->nFanins > 2 ? Csw_TableCutLookup( p, pCut ) : NULL; +p->timeHash += clock() - clk; + if ( pObjNew ) + { + p->nNodesCuts++; + return pObjNew; + } + + // assign the cost + pCut->Cost = Csw_CutFindCost( p, pCut ); + assert( pCut->nFanins > 0 ); + assert( pCut->Cost > 0 ); + } + p->nNodesTried++; + + // load the resulting cuts into the table +clk = clock(); + Csw_ObjForEachCut( p, pObj, pCut, i ) + { + if ( pCut->nFanins > 2 ) + { + assert( pCut->Cost > 0 ); + Csw_TableCutInsert( p, pCut ); + } + } +p->timeHash += clock() - clk; + + // return the node if could not replace it + return pObj; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/csw/cswInt.h b/src/aig/csw/cswInt.h new file mode 100644 index 00000000..37efe9b4 --- /dev/null +++ b/src/aig/csw/cswInt.h @@ -0,0 +1,157 @@ +/**CFile**************************************************************** + + FileName [cswInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: cswInt.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CSW_INT_H__ +#define __CSW_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include +#include +#include +#include + +#include "aig.h" +#include "dar.h" +#include "kit.h" +#include "csw.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Csw_Man_t_ Csw_Man_t; +typedef struct Csw_Cut_t_ Csw_Cut_t; + +// the cut used to represent node in the AIG +struct Csw_Cut_t_ +{ + Csw_Cut_t * pNext; // the next cut in the table + int Cost; // the cost of the cut +// float Cost; // the cost of the cut + unsigned uSign; // cut signature + int iNode; // the node, for which it is the cut + short nCutSize; // the number of bytes in the cut + char nLeafMax; // the maximum number of fanins + char nFanins; // the current number of fanins + int pFanins[0]; // the fanins (followed by the truth table) +}; + +// the CNF computation manager +struct Csw_Man_t_ +{ + // AIG manager + Aig_Man_t * pManAig; // the input AIG manager + Aig_Man_t * pManRes; // the output AIG manager + Aig_Obj_t ** pEquiv; // the equivalent nodes in the resulting manager + Csw_Cut_t ** pCuts; // the cuts for each node in the output manager + int * pnRefs; // the number of references of each new node + // hash table for cuts + Csw_Cut_t ** pTable; // the table composed of cuts + int nTableSize; // the size of hash table + // parameters + int nCutsMax; // the max number of cuts at the node + int nLeafMax; // the max number of leaves of a cut + int fVerbose; // enables verbose output + // internal variables + int nCutSize; // the number of bytes needed to store one cut + int nTruthWords; // the number of truth table words + Aig_MmFixed_t * pMemCuts; // memory manager for cuts + unsigned * puTemp[4]; // used for the truth table computation + // statistics + int nNodesTriv0; // the number of trivial nodes + int nNodesTriv1; // the number of trivial nodes + int nNodesTriv2; // the number of trivial nodes + int nNodesCuts; // the number of rewritten nodes + int nNodesTried; // the number of nodes tried + int timeCuts; // time to compute the cut and its truth table + int timeHash; // time for hashing cuts + int timeOther; // other time + int timeTotal; // total time +}; + +static inline int Csw_CutLeaveNum( Csw_Cut_t * pCut ) { return pCut->nFanins; } +static inline int * Csw_CutLeaves( Csw_Cut_t * pCut ) { return pCut->pFanins; } +static inline unsigned * Csw_CutTruth( Csw_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); } +static inline Csw_Cut_t * Csw_CutNext( Csw_Cut_t * pCut ) { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize); } + +static inline int Csw_ObjRefs( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pnRefs[pObj->Id]; } +static inline void Csw_ObjAddRefs( Csw_Man_t * p, Aig_Obj_t * pObj, int nRefs ) { p->pnRefs[pObj->Id] += nRefs; } + +static inline Csw_Cut_t * Csw_ObjCuts( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; } +static inline void Csw_ObjSetCuts( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; } + +static inline Aig_Obj_t * Csw_ObjEquiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquiv[pObj->Id]; } +static inline void Csw_ObjSetEquiv( Csw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; } + +static inline Aig_Obj_t * Csw_ObjChild0Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Csw_ObjChild1Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +// iterator over cuts of the node +#define Csw_ObjForEachCut( p, pObj, pCut, i ) \ + for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) ) +// iterator over leaves of the cut +#define Csw_CutForEachLeaf( p, pCut, pLeaf, i ) \ + for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cnfCut.c ========================================================*/ +extern Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv ); +extern Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv ); +/*=== cnfMan.c ========================================================*/ +extern Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose ); +extern void Csw_ManStop( Csw_Man_t * p ); +/*=== cnfTable.c ========================================================*/ +extern int Csw_TableCountCuts( Csw_Man_t * p ); +extern void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut ); +extern Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/csw/cswMan.c b/src/aig/csw/cswMan.c new file mode 100644 index 00000000..c3061dee --- /dev/null +++ b/src/aig/csw/cswMan.c @@ -0,0 +1,125 @@ +/**CFile**************************************************************** + + FileName [cswMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: cswMan.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the cut sweeping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose ) +{ + Csw_Man_t * p; + Aig_Obj_t * pObj; + int i; + assert( nCutsMax >= 2 ); + assert( nLeafMax <= 16 ); + // allocate the fraiging manager + p = ALLOC( Csw_Man_t, 1 ); + memset( p, 0, sizeof(Csw_Man_t) ); + p->nCutsMax = nCutsMax; + p->nLeafMax = nLeafMax; + p->fVerbose = fVerbose; + p->pManAig = pMan; + // create the new manager + p->pManRes = Aig_ManStartFrom( pMan ); + assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) ); + // allocate room for cuts and equivalent nodes + p->pnRefs = ALLOC( int, Aig_ManObjNumMax(pMan) ); + p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMan) ); + p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjNumMax(pMan) ); + memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) ); + memset( p->pnRefs, 0, sizeof(int) * Aig_ManObjNumMax(pMan) ); + // allocate memory manager + p->nTruthWords = Aig_TruthWordNum(nLeafMax); + p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords; + p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 ); + // allocate hash table for cuts + p->nTableSize = Aig_PrimeCudd( Aig_ManNodeNum(pMan) * p->nCutsMax / 2 ); + p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize ); + // set the pointers to the available fraig nodes + Csw_ObjSetEquiv( p, Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManRes) ); + Aig_ManForEachPi( p->pManAig, pObj, i ) + Csw_ObjSetEquiv( p, pObj, Aig_ManPi(p->pManRes, i) ); + // room for temporary truth tables + p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords ); + p->puTemp[1] = p->puTemp[0] + p->nTruthWords; + p->puTemp[2] = p->puTemp[1] + p->nTruthWords; + p->puTemp[3] = p->puTemp[2] + p->nTruthWords; + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Csw_ManStop( Csw_Man_t * p ) +{ + if ( p->fVerbose ) + { + int nNodesBeg = Aig_ManNodeNum(p->pManAig); + int nNodesEnd = Aig_ManNodeNum(p->pManRes); + printf( "Beg = %7d. End = %7d. (%6.2f %%) Try = %7d. Cuts = %8d.\n", + nNodesBeg, nNodesEnd, 100.0*(nNodesBeg-nNodesEnd)/nNodesBeg, + p->nNodesTried, Csw_TableCountCuts( p ) ); + printf( "Triv0 = %6d. Triv1 = %6d. Triv2 = %6d. Cut-replace = %6d.\n", + p->nNodesTriv0, p->nNodesTriv1, p->nNodesTriv2, p->nNodesCuts ); + PRTP( "Cuts ", p->timeCuts, p->timeTotal ); + PRTP( "Hashing ", p->timeHash, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + } + free( p->puTemp[0] ); + Aig_MmFixedStop( p->pMemCuts, 0 ); + free( p->pnRefs ); + free( p->pEquiv ); + free( p->pCuts ); + free( p->pTable ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/csw/cswTable.c b/src/aig/csw/cswTable.c new file mode 100644 index 00000000..87e36ae1 --- /dev/null +++ b/src/aig/csw/cswTable.c @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [cswTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: cswTable.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes hash value of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Csw_CutHash( Csw_Cut_t * pCut ) +{ + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned uHash; + int i; + assert( pCut->nFanins <= 16 ); + uHash = 0; + for ( i = 0; i < pCut->nFanins; i++ ) + uHash ^= pCut->pFanins[i] * s_FPrimes[i]; + return uHash; +} + +/**Function************************************************************* + + Synopsis [Returns the total number of cuts in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Csw_TableCountCuts( Csw_Man_t * p ) +{ + Csw_Cut_t * pEnt; + int i, Counter = 0; + for ( i = 0; i < p->nTableSize; i++ ) + for ( pEnt = p->pTable[i]; pEnt; pEnt = pEnt->pNext ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Adds the cut to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + int iEntry = Csw_CutHash(pCut) % p->nTableSize; + pCut->pNext = p->pTable[iEntry]; + p->pTable[iEntry] = pCut; +} + +/**Function************************************************************* + + Synopsis [Returns an equivalent node if it exists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + Aig_Obj_t * pRes = NULL; + Csw_Cut_t * pEnt; + unsigned * pTruthNew, * pTruthOld; + int iEntry = Csw_CutHash(pCut) % p->nTableSize; + for ( pEnt = p->pTable[iEntry]; pEnt; pEnt = pEnt->pNext ) + { + if ( pEnt->nFanins != pCut->nFanins ) + continue; + if ( pEnt->uSign != pCut->uSign ) + continue; + if ( memcmp( pEnt->pFanins, pCut->pFanins, sizeof(int) * pCut->nFanins ) ) + continue; + pTruthOld = Csw_CutTruth(pEnt); + pTruthNew = Csw_CutTruth(pCut); + if ( (pTruthOld[0] & 1) == (pTruthNew[0] & 1) ) + { + if ( Kit_TruthIsEqual( pTruthOld, pTruthNew, pCut->nFanins ) ) + { + pRes = Aig_ManObj( p->pManRes, pEnt->iNode ); + assert( pRes->fPhase == Aig_ManObj( p->pManRes, pCut->iNode )->fPhase ); + break; + } + } + else + { + if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) ) + { + pRes = Aig_Not( Aig_ManObj( p->pManRes, pEnt->iNode ) ); + assert( Aig_Regular(pRes)->fPhase != Aig_ManObj( p->pManRes, pCut->iNode )->fPhase ); + break; + } + } + } + return pRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/csw/csw_.c b/src/aig/csw/csw_.c new file mode 100644 index 00000000..1c59f152 --- /dev/null +++ b/src/aig/csw/csw_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [csw_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cut sweeping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 11, 2007.] + + Revision [$Id: csw_.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/csw/module.make b/src/aig/csw/module.make new file mode 100644 index 00000000..8fdb7bef --- /dev/null +++ b/src/aig/csw/module.make @@ -0,0 +1,4 @@ +SRC += src/aig/csw/cswCore.c \ + src/aig/csw/cswCut.c \ + src/aig/csw/cswMan.c \ + src/aig/csw/cswTable.c -- cgit v1.2.3