diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-11 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-11 08:01:00 -0700 |
commit | 066726076deedaf6d5b38ee4ed27eeb4a2b0061a (patch) | |
tree | 4d8b8eb2f44d4e6ef2f5176aab58e42ed677236e /src/aig | |
parent | a8d75dcc60da15644efbd20529609a1495df229a (diff) | |
download | abc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.tar.gz abc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.tar.bz2 abc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.zip |
Version abc70711
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/csw/csw.h | 65 | ||||
-rw-r--r-- | src/aig/csw/cswCore.c | 80 | ||||
-rw-r--r-- | src/aig/csw/cswCut.c | 383 | ||||
-rw-r--r-- | src/aig/csw/cswInt.h | 141 | ||||
-rw-r--r-- | src/aig/csw/cswMan.c | 108 | ||||
-rw-r--r-- | src/aig/csw/cswTable.c | 176 | ||||
-rw-r--r-- | src/aig/csw/csw_.c | 48 | ||||
-rw-r--r-- | src/aig/csw/module.make | 4 | ||||
-rw-r--r-- | src/aig/dar/dar.h | 1 | ||||
-rw-r--r-- | src/aig/dar/darDfs.c | 29 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 1 | ||||
-rw-r--r-- | src/aig/fra/fraAnd.c | 14 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 10 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 1 |
14 files changed, 1061 insertions, 0 deletions
diff --git a/src/aig/csw/csw.h b/src/aig/csw/csw.h new file mode 100644 index 00000000..4a326414 --- /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 Dar_Man_t * Csw_Sweep( Dar_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..ddf37035 --- /dev/null +++ b/src/aig/csw/cswCore.c @@ -0,0 +1,80 @@ +/**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 [] + +***********************************************************************/ +Dar_Man_t * Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ) +{ + Csw_Man_t * p; + Dar_Man_t * pRes; + Dar_Obj_t * pObj, * pObjNew, * pObjRes; + int i; + // start the manager + p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose ); + // set elementary cuts at the PIs + Dar_ManForEachPi( p->pManRes, pObj, i ) + Csw_ObjPrepareCuts( p, pObj, 1 ); + // process the nodes + Dar_ManForEachNode( pAig, pObj, i ) + { + // create the new node + pObjNew = Dar_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, Dar_Regular(pObjNew), pObj->nRefs > 1 ); + pObjRes = Dar_NotCond( pObjRes, Dar_IsComplement(pObjNew) ); + // set the resulting node + Csw_ObjSetEquiv( p, pObj, pObjRes ); + } + // add the POs + Dar_ManForEachPo( pAig, pObj, i ) + Dar_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) ); + // remove dangling nodes + Dar_ManCleanup( p->pManRes ); + // return the resulting manager + 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..f1cb1fde --- /dev/null +++ b/src/aig/csw/cswCut.c @@ -0,0 +1,383 @@ +/**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 ) +{ + Dar_Obj_t * pObj; + int i, Cost = 0; + Csw_CutForEachLeaf( p->pManRes, pCut, pObj, i ) + Cost += pObj->nRefs; + return Cost * 100 / pCut->nFanins; +} + +/**Function************************************************************* + + Synopsis [Returns the next free cut to use.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Csw_Cut_t * Csw_CutFindFree( Csw_Man_t * p, Dar_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 ); + return Csw_CutTruth(pCut); +} + +/**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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv ) +{ + Csw_Cut_t * pCutSet, * pCut; + int i; + // create the cutset of the node + pCutSet = (Csw_Cut_t *)Dar_MmFixedEntryFetch( p->pMemCuts ); + Csw_ObjSetCuts( p, pObj, pCutSet ); + Csw_ObjForEachCut( p, pObj, pCut, i ) + { + pCut->nFanins = 0; + pCut->iNode = pObj->Id; + } + // 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 = Csw_ObjCutSign( pObj->Id ); + memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords ); + } + return pCutSet; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv ) +{ + Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet; + Dar_Obj_t * pFanin0 = Dar_ObjFanin0(pObj); + Dar_Obj_t * pFanin1 = Dar_ObjFanin1(pObj); + Dar_Obj_t * pObjNew; + unsigned * pTruth; + int i, k, nVars, iVar; + + assert( !Dar_IsComplement(pObj) ); + if ( !Dar_ObjIsNode(pObj) ) + return pObj; + if ( Csw_ObjCuts(p, pObj) ) + return pObj; + // the node is not processed yet + assert( Csw_ObjCuts(p, pObj) == NULL ); + assert( Dar_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 ); + // assemble the new cut + if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) ) + { + assert( pCut->nFanins == 0 ); + continue; + } +/* + // check containment + if ( Csw_CutFilter( p, pCutSet, pCut ) ) + { + pCut->nFanins = 0; + continue; + } +*/ + // create its truth table + pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Dar_ObjFaninC0(pObj), Dar_ObjFaninC1(pObj) ); + // check for trivial truth table + nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax ); + if ( nVars == 0 ) + return Dar_NotCond( Dar_ManConst1(p->pManRes), !(pTruth[0] & 1) ); + if ( nVars == 1 ) + { + iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) ); + assert( iVar < pCut->nFanins ); + return Dar_NotCond( Dar_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) ); + } + // check if an equivalent node with the same cut exists + if ( pObjNew = Csw_TableCutLookup( p, pCut ) ) + return pObjNew; + // assign the cost + pCut->Cost = Csw_CutFindCost( p, pCut ); + assert( pCut->nFanins > 0 ); + assert( pCut->Cost > 0 ); + } + + // load the resulting cuts into the table + Csw_ObjForEachCut( p, pObj, pCut, i ) + if ( pCut->nFanins > 2 ) + { + assert( pCut->Cost > 0 ); + Csw_TableCutInsert( p, pCut ); + } + + // 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..74fa417b --- /dev/null +++ b/src/aig/csw/cswInt.h @@ -0,0 +1,141 @@ +/**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 <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.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 + unsigned uSign; // cut signature + int iNode; // the node, for which it is the cut + int nFanins; // the number of words in truth table + int pFanins[0]; // the fanins (followed by the truth table) +}; + +// the CNF computation manager +struct Csw_Man_t_ +{ + // AIG manager + Dar_Man_t * pManAig; // the input AIG manager + Dar_Man_t * pManRes; // the output AIG manager + Dar_Obj_t ** pEquiv; // the equivalent nodes in the resulting manager + Csw_Cut_t ** pCuts; // the cuts for each node in the output manager + // 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 + Dar_MmFixed_t * pMemCuts; // memory manager for cuts + unsigned * puTemp[4]; // used for the truth table computation +}; + +static inline unsigned Csw_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); } + +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->nFanins); } +static inline Csw_Cut_t * Csw_CutNext( Csw_Man_t * p, Csw_Cut_t * pCut ) { return (Csw_Cut_t *)(((char *)pCut) + p->nCutSize); } + +static inline Csw_Cut_t * Csw_ObjCuts( Csw_Man_t * p, Dar_Obj_t * pObj ) { return p->pCuts[pObj->Id]; } +static inline void Csw_ObjSetCuts( Csw_Man_t * p, Dar_Obj_t * pObj, Csw_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; } + +static inline Dar_Obj_t * Csw_ObjEquiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { return p->pEquiv[pObj->Id]; } +static inline void Csw_ObjSetEquiv( Csw_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; } + +static inline Dar_Obj_t * Csw_ObjChild0Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; } +static inline Dar_Obj_t * Csw_ObjChild1Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin1(pObj)), Dar_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(p, pCut) ) +// iterator over leaves of the cut +#define Csw_CutForEachLeaf( p, pCut, pLeaf, i ) \ + for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cnfCut.c ========================================================*/ +extern Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv ); +extern Dar_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv ); +/*=== cnfMan.c ========================================================*/ +extern Csw_Man_t * Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose ); +extern void Csw_ManStop( Csw_Man_t * p ); +/*=== cnfTable.c ========================================================*/ +extern void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut ); +extern Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut ); +extern unsigned int Cudd_PrimeCws( unsigned int p ); + +#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..180fecef --- /dev/null +++ b/src/aig/csw/cswMan.c @@ -0,0 +1,108 @@ +/**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( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose ) +{ + Csw_Man_t * p; + Dar_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 = Dar_ManStartFrom( pMan ); + assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManRes) ); + // allocate room for cuts and equivalent nodes + p->pEquiv = ALLOC( Dar_Obj_t *, Dar_ManObjIdMax(pMan) + 1 ); + p->pCuts = ALLOC( Csw_Cut_t *, Dar_ManObjIdMax(pMan) + 1 ); + memset( p->pCuts, 0, sizeof(Dar_Obj_t *) * (Dar_ManObjIdMax(pMan) + 1) ); + // allocate memory manager + p->nTruthWords = Dar_TruthWordNum(nLeafMax); + p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords; + p->pMemCuts = Dar_MmFixedStart( p->nCutSize * p->nCutsMax, 512 ); + // allocate hash table for cuts + p->nTableSize = Cudd_PrimeCws( Dar_ManNodeNum(pMan) * p->nCutsMax / 2 ); + p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize ); + // set the pointers to the available fraig nodes + Csw_ObjSetEquiv( p, Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManRes) ); + Dar_ManForEachPi( p->pManAig, pObj, i ) + Csw_ObjSetEquiv( p, pObj, Dar_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 ) +{ + free( p->puTemp[0] ); + Dar_MmFixedStop( p->pMemCuts, 0 ); + 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..82f09d01 --- /dev/null +++ b/src/aig/csw/cswTable.c @@ -0,0 +1,176 @@ +/**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 next prime >= p.] + + Description [Copied from CUDD, for stand-aloneness.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +unsigned int Cudd_PrimeCws( unsigned int p ) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + +/**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 [] + +***********************************************************************/ +Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut ) +{ + Dar_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 = Dar_ManObj( p->pManRes, pEnt->iNode ); + assert( pRes->fPhase == Dar_ManObj( p->pManRes, pCut->iNode )->fPhase ); + break; + } + } + else + { + if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) ) + { + pRes = Dar_Not( Dar_ManObj( p->pManRes, pEnt->iNode ) ); + assert( Dar_Regular(pRes)->fPhase != Dar_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 diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 9744da88..8e82cdf4 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -382,6 +382,7 @@ extern Vec_Int_t * Dar_LibReadOuts(); extern void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops ); /*=== darDfs.c ==========================================================*/ extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ); +extern Vec_Ptr_t * Dar_ManDfsNodes( Dar_Man_t * p, Dar_Obj_t ** ppNodes, int nNodes ); extern int Dar_ManCountLevels( Dar_Man_t * p ); extern void Dar_ManCreateRefs( Dar_Man_t * p ); extern int Dar_DagSize( Dar_Obj_t * pObj ); diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c index bdb23c9d..116f428c 100644 --- a/src/aig/dar/darDfs.c +++ b/src/aig/dar/darDfs.c @@ -90,6 +90,35 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ) /**Function************************************************************* + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManDfsNodes( Dar_Man_t * p, Dar_Obj_t ** ppNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj; + int i; + assert( Dar_ManLatchNum(p) == 0 ); + Dar_ManIncrementTravId( p ); + // mark constant and PIs + Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) ); + Dar_ManForEachPi( p, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) ); + for ( i = 0; i < nNodes; i++ ) + Dar_ManDfs_rec( p, ppNodes[i], vNodes ); + return vNodes; +} + +/**Function************************************************************* + Synopsis [Computes the max number of levels in the manager.] Description [] diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index ee52520a..29195d19 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -117,6 +117,7 @@ struct Fra_Man_t_ int nSatProof; int nSatFails; int nSatFailsReal; + int nSpeculs; // runtime int timeSim; int timeTrav; diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c index 86cbbc9e..a360ce9b 100644 --- a/src/aig/fra/fraAnd.c +++ b/src/aig/fra/fraAnd.c @@ -51,6 +51,8 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); // get the fraiged node pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); + if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) ) + return pObjFraig; Dar_Regular(pObjFraig)->pData = p; // get representative of this class pObjOldRepr = Fra_ObjRepr(pObjOld); @@ -79,14 +81,26 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) } if ( RetValue == -1 ) // failed { + Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) }; + Vec_Ptr_t * vNodes; + if ( !p->pPars->fSpeculate ) return pObjFraig; // substitute the node // pObjOld->fMarkB = 1; + p->nSpeculs++; + + vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 ); + printf( "%d ", Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); + return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); } +// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id ); // simulate the counter-example and return the Fraig node +// printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); Fra_Resimulate( p ); +// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 ); assert( Fra_ObjRepr(pObjOld) != pObjOldRepr ); return pObjFraig; } diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index ac6a4f4a..33421423 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -334,6 +334,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) Dar_Obj_t * pObj, ** ppThis; int i; assert( ppClass[0] != NULL && ppClass[1] != NULL ); + // check if the class is going to be refined for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) ) @@ -349,6 +350,15 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) Vec_PtrPush( p->vClassOld, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); +/* + printf( "Refining class (" ); + Vec_PtrForEachEntry( p->vClassOld, pObj, i ) + printf( "%d,", pObj->Id ); + printf( ") + (" ); + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + printf( "%d,", pObj->Id ); + printf( ")\n" ); +*/ // put the nodes back into the class memory Vec_PtrForEachEntry( p->vClassOld, pObj, i ) { diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 67921318..19ed6c03 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -205,6 +205,7 @@ void Fra_ManPrint( Fra_Man_t * p ) PRT( "Class refining ", p->timeRef ); PRT( "TOTAL RUNTIME ", p->timeTotal ); if ( p->time1 ) { PRT( "time1 ", p->time1 ); } + printf( "Speculations = %d.\n", p->nSpeculs ); } //////////////////////////////////////////////////////////////////////// |