summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-07-11 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-07-11 08:01:00 -0700
commit066726076deedaf6d5b38ee4ed27eeb4a2b0061a (patch)
tree4d8b8eb2f44d4e6ef2f5176aab58e42ed677236e
parenta8d75dcc60da15644efbd20529609a1495df229a (diff)
downloadabc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.tar.gz
abc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.tar.bz2
abc-066726076deedaf6d5b38ee4ed27eeb4a2b0061a.zip
Version abc70711
-rw-r--r--Makefile2
-rw-r--r--abc.dsp28
-rw-r--r--abc.rc5
-rw-r--r--src/aig/csw/csw.h65
-rw-r--r--src/aig/csw/cswCore.c80
-rw-r--r--src/aig/csw/cswCut.c383
-rw-r--r--src/aig/csw/cswInt.h141
-rw-r--r--src/aig/csw/cswMan.c108
-rw-r--r--src/aig/csw/cswTable.c176
-rw-r--r--src/aig/csw/csw_.c48
-rw-r--r--src/aig/csw/module.make4
-rw-r--r--src/aig/dar/dar.h1
-rw-r--r--src/aig/dar/darDfs.c29
-rw-r--r--src/aig/fra/fra.h1
-rw-r--r--src/aig/fra/fraAnd.c14
-rw-r--r--src/aig/fra/fraClass.c10
-rw-r--r--src/aig/fra/fraMan.c1
-rw-r--r--src/base/abci/abc.c110
-rw-r--r--src/base/abci/abcDar.c29
19 files changed, 1225 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index 28131069..3375bc42 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/base/io src/base/main src/base/ver \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
- src/aig/ec \
+ src/aig/csw src/aig/ec \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio \
diff --git a/abc.dsp b/abc.dsp
index c2fa926c..067aaaa5 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -945,6 +945,34 @@ SOURCE=.\src\aig\cnf\cnfUtil.c
SOURCE=.\src\aig\cnf\cnfWrite.c
# End Source File
# End Group
+# Begin Group "csw"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\csw\csw.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswTable.c
+# End Source File
+# End Group
# End Group
# Begin Group "bdd"
diff --git a/abc.rc b/abc.rc
index f1cf78d6..4b253b07 100644
--- a/abc.rc
+++ b/abc.rc
@@ -163,6 +163,9 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
#alias t "r i10_if4.blif; lp"
#alias t1 "r pj1_if4.blif; lp"
#alias t2 "r pj1_if6.blif; lp"
-alias t "r pj/pj1.blif; st; dfraig -v"
+#alias t "r pj/pj1.blif; st; dfraig -v"
+#alias t "r c/16/csat_2.bench; st; dfraig -C 100 -v -r"
+#alias t "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
+alias t "r i10.blif; st; ps; csweep; ps; cec"
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 );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 06f4299d..9c2c0153 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -113,6 +113,7 @@ static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -269,6 +270,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "csweep", Abc_CommandCSweep, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
@@ -6919,22 +6921,23 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fProve, fVerbose, fDoSparse;
+ int c, fProve, fVerbose, fDoSparse, fSpeculate;
int nConfLimit;
- extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nConfLimit = 100;
- fDoSparse = 0;
+ nConfLimit = 100;
+ fSpeculate = 0;
+ fDoSparse = 1;
fProve = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF )
{
switch ( c )
{
@@ -6955,6 +6958,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fProve ^= 1;
break;
+ case 'r':
+ fSpeculate ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -6970,7 +6976,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
+ pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -6981,11 +6987,101 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dfraig [-C num] [-spvh]\n" );
+ fprintf( pErr, "usage: dfraig [-C num] [-sprvh]\n" );
fprintf( pErr, "\t performs fraiging using a new method\n" );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
+ fprintf( pErr, "\t-r : toggle speculative reduction [default = %s]\n", fSpeculate? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c, nCutsMax, nLeafMax, fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nCutsMax = 8;
+ nLeafMax = 8;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CKvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nCutsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nCutsMax < 0 )
+ goto usage;
+ break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLeafMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLeafMax < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: csweep [-C num] [-K num] [-vh]\n" );
+ fprintf( pErr, "\t performs cut sweeping using a new method\n" );
+ fprintf( pErr, "\t-C num : limit on the number of cuts [default = %d]\n", nCutsMax );
+ fprintf( pErr, "\t-K num : limit on the cut size [default = %d]\n", nLeafMax );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ba3ac89d..ed6fa77e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -455,7 +455,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose )
{
Fra_Par_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
@@ -468,6 +468,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
pParams->fVerbose = fVerbose;
pParams->fProve = fProve;
pParams->fDoSparse = fDoSparse;
+ pParams->fSpeculate = fSpeculate;
pMan = Fra_Perform( pTemp = pMan, pParams );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Dar_ManStop( pTemp );
@@ -475,6 +476,32 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
return pNtkAig;
}
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
+{
+ extern Dar_Man_t * Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+ Abc_Ntk_t * pNtkAig;
+ Dar_Man_t * pMan, * pTemp;
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+ pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Dar_ManStop( pTemp );
+ Dar_ManStop( pMan );
+ return pNtkAig;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////