Skip to content

A
abc
Commit 06672607 by Alan Mishchenko
Options

Version abc70711

parent a8d75dcc
Showing with 842 additions and 10 deletions
Makefile
...@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \ ...@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/base/io src/base/main src/base/ver \ src/base/io src/base/main src/base/ver \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ 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/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/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
src/bdd/parse src/bdd/reo src/bdd/cas \ src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio \ src/map/fpga src/map/mapper src/map/mio \
......
abc.dsp
...@@ -945,6 +945,34 @@ SOURCE=.\src\aig\cnf\cnfUtil.c ...@@ -945,6 +945,34 @@ SOURCE=.\src\aig\cnf\cnfUtil.c
SOURCE=.\src\aig\cnf\cnfWrite.c SOURCE=.\src\aig\cnf\cnfWrite.c
# End Source File # End Source File
# End Group # 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 # End Group
# Begin Group "bdd" # Begin Group "bdd"
......
abc.rc
...@@ -163,6 +163,9 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_ ...@@ -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 t "r i10_if4.blif; lp"
#alias t1 "r pj1_if4.blif; lp" #alias t1 "r pj1_if4.blif; lp"
#alias t2 "r pj1_if6.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"
src/aig/csw/csw.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/cswCore.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/cswInt.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/cswMan.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/cswTable.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/csw_.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/csw/module.make 0 → 100644
SRC += src/aig/csw/cswCore.c \
src/aig/csw/cswCut.c \
src/aig/csw/cswMan.c \
src/aig/csw/cswTable.c
src/aig/dar/dar.h
...@@ -382,6 +382,7 @@ extern Vec_Int_t * Dar_LibReadOuts(); ...@@ -382,6 +382,7 @@ extern Vec_Int_t * Dar_LibReadOuts();
extern void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops ); extern void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== darDfs.c ==========================================================*/ /*=== darDfs.c ==========================================================*/
extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ); 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 int Dar_ManCountLevels( Dar_Man_t * p );
extern void Dar_ManCreateRefs( Dar_Man_t * p ); extern void Dar_ManCreateRefs( Dar_Man_t * p );
extern int Dar_DagSize( Dar_Obj_t * pObj ); extern int Dar_DagSize( Dar_Obj_t * pObj );
......
src/aig/dar/darDfs.c
...@@ -90,6 +90,35 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ) ...@@ -90,6 +90,35 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p )
/**Function************************************************************* /**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.] Synopsis [Computes the max number of levels in the manager.]
Description [] Description []
......
src/aig/fra/fra.h
...@@ -117,6 +117,7 @@ struct Fra_Man_t_ ...@@ -117,6 +117,7 @@ struct Fra_Man_t_
int nSatProof; int nSatProof;
int nSatFails; int nSatFails;
int nSatFailsReal; int nSatFailsReal;
int nSpeculs;
// runtime // runtime
int timeSim; int timeSim;
int timeTrav; int timeTrav;
......
src/aig/fra/fraAnd.c
...@@ -51,6 +51,8 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) ...@@ -51,6 +51,8 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
// get the fraiged node // get the fraiged node
pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
return pObjFraig;
Dar_Regular(pObjFraig)->pData = p; Dar_Regular(pObjFraig)->pData = p;
// get representative of this class // get representative of this class
pObjOldRepr = Fra_ObjRepr(pObjOld); pObjOldRepr = Fra_ObjRepr(pObjOld);
...@@ -79,14 +81,26 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) ...@@ -79,14 +81,26 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
} }
if ( RetValue == -1 ) // failed if ( RetValue == -1 ) // failed
{ {
Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
Vec_Ptr_t * vNodes;
if ( !p->pPars->fSpeculate ) if ( !p->pPars->fSpeculate )
return pObjFraig; return pObjFraig;
// substitute the node // substitute the node
// pObjOld->fMarkB = 1; // 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 ); 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 // 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 ); Fra_Resimulate( p );
// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
assert( Fra_ObjRepr(pObjOld) != pObjOldRepr ); assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
return pObjFraig; return pObjFraig;
} }
......
src/aig/fra/fraClass.c
...@@ -334,6 +334,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) ...@@ -334,6 +334,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
Dar_Obj_t * pObj, ** ppThis; Dar_Obj_t * pObj, ** ppThis;
int i; int i;
assert( ppClass[0] != NULL && ppClass[1] != NULL ); assert( ppClass[0] != NULL && ppClass[1] != NULL );
// check if the class is going to be refined // check if the class is going to be refined
for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )
if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) ) if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
...@@ -349,6 +350,15 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) ...@@ -349,6 +350,15 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
Vec_PtrPush( p->vClassOld, pObj ); Vec_PtrPush( p->vClassOld, pObj );
else else
Vec_PtrPush( p->vClassNew, pObj ); 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 // put the nodes back into the class memory
Vec_PtrForEachEntry( p->vClassOld, pObj, i ) Vec_PtrForEachEntry( p->vClassOld, pObj, i )
{ {
......
src/aig/fra/fraMan.c
...@@ -205,6 +205,7 @@ void Fra_ManPrint( Fra_Man_t * p ) ...@@ -205,6 +205,7 @@ void Fra_ManPrint( Fra_Man_t * p )
PRT( "Class refining ", p->timeRef ); PRT( "Class refining ", p->timeRef );
PRT( "TOTAL RUNTIME ", p->timeTotal ); PRT( "TOTAL RUNTIME ", p->timeTotal );
if ( p->time1 ) { PRT( "time1 ", p->time1 ); } if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
printf( "Speculations = %d.\n", p->nSpeculs );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
...@@ -113,6 +113,7 @@ static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -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_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIFraig ( 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_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_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( 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 ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -269,6 +270,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -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", "isat", Abc_CommandISat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 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", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 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 ) ...@@ -6919,22 +6921,23 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes; Abc_Ntk_t * pNtk, * pNtkRes;
int c, fProve, fVerbose, fDoSparse; int c, fProve, fVerbose, fDoSparse, fSpeculate;
int nConfLimit; 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); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// set defaults // set defaults
nConfLimit = 100; nConfLimit = 100;
fDoSparse = 0; fSpeculate = 0;
fDoSparse = 1;
fProve = 0; fProve = 0;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -6955,6 +6958,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6955,6 +6958,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p': case 'p':
fProve ^= 1; fProve ^= 1;
break; break;
case 'r':
fSpeculate ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -6970,7 +6976,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6970,7 +6976,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
fprintf( pErr, "Command has failed.\n" ); fprintf( pErr, "Command has failed.\n" );
...@@ -6981,11 +6987,101 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6981,11 +6987,101 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: 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 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-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-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-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-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
......
src/base/abci/abcDar.c
...@@ -455,7 +455,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) ...@@ -455,7 +455,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
SeeAlso [] 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; Fra_Par_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
...@@ -468,6 +468,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in ...@@ -468,6 +468,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
pParams->fVerbose = fVerbose; pParams->fVerbose = fVerbose;
pParams->fProve = fProve; pParams->fProve = fProve;
pParams->fDoSparse = fDoSparse; pParams->fDoSparse = fDoSparse;
pParams->fSpeculate = fSpeculate;
pMan = Fra_Perform( pTemp = pMan, pParams ); pMan = Fra_Perform( pTemp = pMan, pParams );
pNtkAig = Abc_NtkFromDar( pNtk, pMan ); pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Dar_ManStop( pTemp ); Dar_ManStop( pTemp );
...@@ -475,6 +476,32 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in ...@@ -475,6 +476,32 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
return pNtkAig; 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment