luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc70202

This commit is contained in:
Alan Mishchenko 2007-02-02 08:01:00 -08:00
parent 12578e622f
commit 8da52b6f20
28 changed files with 1241 additions and 328 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abc.dsp
View File

@ -1697,6 +1697,18 @@ SOURCE=.\src\opt\res\resUpdate.c
SOURCE=.\src\opt\res\resWin.c
# End Source File
# End Group
# Begin Group "bdc"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\bdc\bdc.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\bdc\bdcInt.h
# End Source File
# End Group
# End Group
# Begin Group "map"

4
abc.rc
View File

@ -102,6 +102,10 @@ alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l;
alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
# experimental implementation of don't-cares
alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
# temporaries
#alias t "rvl th/lib.v; rvv th/t2.v"
#alias t "so c/pure_sat/test.c"

2
src/aig/ivy/ivy.h
View File

@ -152,6 +152,7 @@ struct Ivy_FraigParams_t_
typedef struct Ivy_Cut_t_ Ivy_Cut_t;
struct Ivy_Cut_t_
{
int nLatches;
short nSize;
short nSizeMax;
int pArray[IVY_CUT_INPUT];
@ -541,6 +542,7 @@ extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj
extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj );
extern void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
extern int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth );
#ifdef __cplusplus
}

34
src/aig/ivy/ivySeq.c
View File

@ -41,6 +41,11 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); }
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
//int nMoves;
//int nMovesS;
//int nClauses;
//int timeInv;
/**Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
@ -58,6 +63,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
Ivy_Obj_t * pNode;
int i, nNodes, nGain;
int clk, clkStart = clock();
// set the DC latch values
Ivy_ManForEachLatch( p, pNode, i )
pNode->Init = IVY_INIT_DC;
@ -81,7 +87,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
// if ( Ivy_ObjIsBuf(pNode) )
// continue;
// stop if all nodes have been tried once
if ( i > nNodes )
if ( i > nNodes )
break;
// for each cut, try to resynthesize it
nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
@ -114,6 +120,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
return 1;
}
/**Function*************************************************************
Synopsis [Performs rewriting for one node.]
@ -140,11 +147,11 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
Ivy_Cut_t * pCut;
Ivy_Obj_t * pFanin;//, * pFanout;
Vec_Ptr_t * vFanout;
unsigned uPhase, uTruthBest, uTruth;
unsigned uPhase, uTruthBest, uTruth;//, nNewClauses;
char * pPerm;
int nNodesSaved, nNodesSaveCur;
int i, c, GainCur, GainBest = -1;
int clk, clk2;
int clk, clk2;//, clk3;
p->nNodesConsidered++;
// get the node's cuts
@ -201,18 +208,6 @@ clk2 = clock();
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
p->timeMffc += clock() - clk2;
/*
if ( pNode->Id == 8648 )
{
int i;
printf( "Trying cut : {" );
for ( i = 0; i < pCut->nSize; i++ )
printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
// printf( " }\n" );
printf( " } " );
Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
}
*/
// evaluate the cut
clk2 = clock();
@ -252,6 +247,15 @@ p->timeRes += clock() - clk;
}
*/
//clk3 = clock();
//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
//timeInv += clock() - clk;
// nClauses += nNewClauses;
// nMoves++;
// if ( nNewClauses > 0 )
// nMovesS++;
// copy the leaves
Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );

80
src/aig/ivy/ivyUtil.c
View File

@ -731,6 +731,86 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
{
int i;
printf( "Trying cut : {" );
for ( i = 0; i < pCut->nSize; i++ )
printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
printf( " } " );
Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
return 0;
}
/**Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
{
Vec_Ptr_t * vArray;
Ivy_Obj_t * pObj, * pFanout;
int nLatches = 0;
int nPresent = 0;
int i, k;
int fVerbose = 0;
if ( fVerbose )
printf( "Trying cut : {" );
for ( i = 0; i < pCut->nSize; i++ )
{
if ( fVerbose )
printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
nLatches += Ivy_LeafLat(pCut->pArray[i]);
}
if ( fVerbose )
printf( " } " );
if ( fVerbose )
printf( "Latches = %d. ", nLatches );
// check if there are latches on the fanout edges
vArray = Vec_PtrAlloc( 100 );
for ( i = 0; i < pCut->nSize; i++ )
{
pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
{
if ( Ivy_ObjIsLatch(pFanout) )
{
nPresent++;
break;
}
}
}
Vec_PtrSize( vArray );
if ( fVerbose )
{
printf( "Present = %d. ", nPresent );
if ( nLatches > nPresent )
printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
printf( "\n" );
}
return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/base/abc/abc.h
View File

@ -814,6 +814,7 @@ extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
extern int Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );

22
src/base/abc/abcUtil.c
View File

@ -105,7 +105,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
if ( pNtk->nTravIds == (1<<30)-1 )
if ( pNtk->nTravIds >= (1<<30)-1 )
{
pNtk->nTravIds = 0;
Abc_NtkForEachObj( pNtk, pObj, i )
@ -445,6 +445,26 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk )
return nFaninsMax;
}
/**Function*************************************************************
Synopsis [Reads the total number of all fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i, nFanins = 0;
Abc_NtkForEachNode( pNtk, pNode, i )
nFanins += Abc_ObjFaninNum(pNode);
return nFanins;
}
/**Function*************************************************************
Synopsis [Cleans the copy field of all objects.]

7
src/base/abci/abc.c
View File

@ -2569,6 +2569,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Res_Par_t Pars, * pPars = &Pars;
int c;
// printf( "Implementation of this command is not finished.\n" );
// return 1;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@ -2641,8 +2644,8 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" );
fprintf( pErr, "\t-W <NM> : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-S <num> : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-W <NM> : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");

26
src/base/abci/abcIvy.c
View File

@ -187,18 +187,44 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
int clk;
// int i;
/*
extern int nMoves;
extern int nMovesS;
extern int nClauses;
extern int timeInv;
nMoves = 0;
nMovesS = 0;
nClauses = 0;
timeInv = 0;
*/
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = clock();
clk = clock();
Ivy_ManHaigStart( pMan, fVerbose );
// Ivy_ManRewriteSeq( pMan, 0, 0 );
// for ( i = 0; i < nIters; i++ )
// Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
Ivy_ManRewriteSeq( pMan, 0, 0 );
Ivy_ManRewriteSeq( pMan, 0, 0 );
Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
//PRT( " ", clock() - clk );
//printf( "\n" );
/*
printf( "Moves = %d. ", nMoves );
printf( "MovesS = %d. ", nMovesS );
printf( "Clauses = %d. ", nClauses );
PRT( "Time", timeInv );
*/
// Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
// Ivy_ManHaigPostprocess( pMan, fVerbose );

3
src/base/abci/abcPrint.c
View File

@ -77,7 +77,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
}
else
{
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
fprintf( pFile, " net = %5d", Abc_NtkGetTotalFanins(pNtk) );
}
if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
{

6
src/base/abci/abcSat.c
View File

@ -65,6 +65,10 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
if ( pSat == NULL )
return 1;
//printf( "%d \n", pSat->clauses.size );
//sat_solver_delete( pSat );
//return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
@ -619,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
nMuxes = 0;
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
//sat_solver_store_alloc( pSat );
RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
sat_solver_store_mark_roots( pSat );

73
src/opt/bdc/bdc.h Normal file
View File

@ -0,0 +1,73 @@
/**CFile****************************************************************
FileName [bdc.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BDC_H__
#define __BDC_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Bdc_Man_t_ Bdc_Man_t;
typedef struct Bdc_Par_t_ Bdc_Par_t;
struct Bdc_Par_t_
{
// general parameters
int nVarsMax; // the maximum support
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bdcCore.c ==========================================================*/
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
extern void Bdc_ManAlloc( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

157
src/opt/bdc/bdcCore.c Normal file
View File

@ -0,0 +1,157 @@
/**CFile****************************************************************
FileName [bdcCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [The gateway to bi-decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocate resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
{
Bdc_Man_t * p;
int i;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
p->pPars = pPars;
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
p->nNodesAlloc = 256;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
p->vSpots = Vec_IntAlloc( 256 );
// set up constant 1 and elementary variables
for ( i = 0; i < pPars->nVarsMax; i++ )
{
}
p->nNodes = pPars->nVarsMax + 1;
// remember the current place in memory
p->nMemStart = Vec_IntSize( p->vMemory );
return p;
}
/**Function*************************************************************
Synopsis [Deallocate resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_ManAlloc( Bdc_Man_t * p )
{
}
/**Function*************************************************************
Synopsis [Sets up the divisors.]
Description [The first n+1 entries are const1 and elem variables.]
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
{
Bdc_Fun_t ** pSpot, * pFunc;
unsigned * puTruth;
int i;
// clean hash table
Vec_PtrForEachEntry( p->vSpots, pSpot, i )
*pSpot = NULL;
// reset nodes
p->nNodes = p->pPars->nVarsMax + 1;
// reset memory
Vec_IntShrink( p->vMemory, p->nMemStart );
// add new nodes to the hash table
Vec_PtrForEachEntry( vDivs, puTruth, i )
{
pFunc = Bdc_ManNewNode( p );
pFunc->Type = BDC_TYPE_PI;
pFunc->puFunc = puTruth;
pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars );
}
}
/**Function*************************************************************
Synopsis [Performs decomposition of one function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
// set current manager parameters
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( nVars );
p->nNodeLimit = nNodeLimit;
Bdc_ManPrepare( p, vDivs );
// copy the function
pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords );
pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords );
Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
// call decomposition
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
if ( p->pRoot == NULL )
return -1;
return p->nNodes - (p->pPars->nVarsMax + 1);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

76
src/opt/bdc/bdcDec.c Normal file
View File

@ -0,0 +1,76 @@
/**CFile****************************************************************
FileName [bdc_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs one step of bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
Bdc_Fun_t * pFunc;
Bdc_Isf_t IsfA, * pIsfA = &IsfA;
Bdc_Isf_t IsfB, * pIsfB = &IsfB;
int Type;
Bdc_SuppMinimize( p, pIsf );
if ( pFunc = Bdc_TableLookup( p, pIsf ) )
return pFunc;
pFunc = Bdc_ManNewNode( p );
pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfA, pIsfB );
pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfA );
if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfA, pIsfB, pFunc->pFan0->puFunc ) )
{
p->nNodes--;
return pFunc->pFan0;
}
pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfA );
pFunc->puFunc = Vec_IntFetch( p->vMemory, p->nWords );
pFunc->puFunc =
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

127
src/opt/bdc/bdcInt.h Normal file
View File

@ -0,0 +1,127 @@
/**CFile****************************************************************
FileName [bdcInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BDC_INT_H__
#define __BDC_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "dec.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// network types
typedef enum {
BDC_TYPE_NONE = 0, // 0: unknown
BDC_TYPE_CONST1, // 1: constant 1
BDC_TYPE_PI, // 2: primary input
BDC_TYPE_AND, // 4: AND-gate
BDC_TYPE_XOR, // 5: XOR-gate
BDC_TYPE_MUX, // 6: MUX-gate
BDC_TYPE_OTHER // 7: unused
} Bdc_Type_t;
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
struct Bdc_Fun_t_
{
int Type; // Const1, PI, AND, XOR, MUX
Bdc_Fun_t * pFan0; // next function with same support
Bdc_Fun_t * pFan1; // next function with same support
Bdc_Fun_t * pFan2; // next function with same support
unsigned uSupp; // bit mask of current support
unsigned * puFunc; // the function of the node
Bdc_Fun_t * pNext; // next function with same support
void * pCopy; // the copy field
};
typedef struct Bdc_Isf_t_ Bdc_Isf_t;
struct Bdc_Isf_t_
{
unsigned uSupp; // bit mask of current support
unsigned uUnique; // bit mask of unique support
unsigned * puOn; // on-set
unsigned * puOff; // off-set
int Cost; // cost of this component
};
typedef struct Bdc_Man_t_ Bdc_Man_t;
struct Bdc_Man_t_
{
// external parameters
Bdc_Par_t * pPars; // parameter set
int nVars; // the number of variables
int nWords; // the number of words
int nNodeLimit; // the limit on the number of new nodes
// internal nodes
Bdc_Fun_t * pNodes; // storage for decomposition nodes
int nNodes; // the number of nodes used
int nNodesAlloc; // the number of nodes allocated
Bdc_Fun_t * pRoot; // the root node
// resub candidates
Bdc_Fun_t ** pTable; // hash table of candidates
int nTableSize; // hash table size (1 << nVarsMax)
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
int nMemStart; // the starting memory size
};
// working with complemented attributes of objects
static inline bool Bdc_IsComplement( Bdc_Fun_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bdcSupp.c ==========================================================*/
extern int Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

50
src/opt/bdc/bdc_.c Normal file
View File

@ -0,0 +1,50 @@
/**CFile****************************************************************
FileName [bdc_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

8
src/opt/bdc/module.make Normal file
View File

@ -0,0 +1,8 @@
SRC += src/opt/res/resCore.c \
src/opt/res/resDivs.c \
src/opt/res/resFilter.c \
src/opt/res/resSat.c \
src/opt/res/resSim.c \
src/opt/res/resStrash.c \
src/opt/res/resUpdate.c \
src/opt/res/resWin.c

73
src/opt/res/resCore.c
View File

@ -39,15 +39,19 @@ struct Res_Man_t_
Sto_Man_t * pCnf; // the CNF of the SAT problem
Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vResubs; // resubstitution candidates
Vec_Vec_t * vResubs; // resubstitution candidates of the AIG
Vec_Vec_t * vResubsW; // resubstitution candidates of the window
Vec_Vec_t * vLevels; // levelized structure for updating
// statistics
int nWins; // the number of windows tried
int nWinNodes; // the total number of window nodes
int nDivNodes; // the total number of divisors
int nWinsTriv; // the total number of trivial windows
int nWinsUsed; // the total number of useful windows (with at least one candidate)
int nCandSets; // the total number of candidates
int nProvedSets; // the total number of proved groups
int nSimEmpty; // the empty simulation info
int nTotalNets; // the total number of nets
// runtime
int timeWin; // windowing
int timeDiv; // divisors
@ -90,6 +94,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
p->pMan = Int_ManAlloc( 512 );
p->vMem = Vec_IntAlloc( 0 );
p->vResubs = Vec_VecStart( pPars->nCands );
p->vResubsW = Vec_VecStart( pPars->nCands );
p->vLevels = Vec_VecStart( 32 );
return p;
}
@ -113,9 +118,11 @@ void Res_ManFree( Res_Man_t * p )
printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
printf( "\n" );
printf( "SimEmpt = %d. ", p->nSimEmpty );
printf( "WinsTriv = %d. ", p->nWinsTriv );
printf( "SimsEmpt = %d. ", p->nSimEmpty );
printf( "WindUsed = %d. ", p->nWinsUsed );
printf( "Cands = %d. ", p->nCandSets );
printf( "Proved = %d. ", p->nProvedSets );
printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
printf( "\n" );
PRT( "Windowing ", p->timeWin );
@ -135,6 +142,7 @@ void Res_ManFree( Res_Man_t * p )
Int_ManFree( p->pMan );
Vec_IntFree( p->vMem );
Vec_VecFree( p->vResubs );
Vec_VecFree( p->vResubsW );
Vec_VecFree( p->vLevels );
free( p );
}
@ -164,6 +172,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
// start the manager
p = Res_ManAlloc( pPars );
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
// set the number of levels
Abc_NtkLevel( pNtk );
@ -182,15 +191,32 @@ clk = clock();
p->timeWin += clock() - clk;
if ( !RetValue )
continue;
p->nWinsTriv += Res_WinIsTrivial( p->pWin );
p->nWins++;
p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels );
if ( p->pPars->fVeryVerbose )
{
printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
printf( "Win = %3d/%3d/%4d/%3d ",
Vec_PtrSize(p->pWin->vLeaves),
Vec_PtrSize(p->pWin->vBranches),
Vec_PtrSize(p->pWin->vNodes),
Vec_PtrSize(p->pWin->vRoots) );
}
// collect the divisors
clk = clock();
Res_WinDivisors( p->pWin, pObj->Level - 1 );
p->timeDiv += clock() - clk;
p->nDivNodes += Vec_PtrSize( p->pWin->vDivs );
p->nWins++;
p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
if ( p->pPars->fVeryVerbose )
{
printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
printf( "D+ = %3d ", p->pWin->nDivsPlus );
}
// create the AIG for the window
clk = clock();
@ -200,13 +226,6 @@ p->timeAig += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
printf( "Win = %3d/%3d/%4d/%3d ",
Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus,
p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels),
Vec_PtrSize(p->pWin->vRoots) );
printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
printf( "D+ = %3d ", p->pWin->nDivsPlus );
printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
printf( "\n" );
}
@ -223,12 +242,14 @@ p->timeSim += clock() - clk;
// find resub candidates for the node
clk = clock();
RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs );
RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
p->timeCand += clock() - clk;
p->nCandSets += RetValue;
if ( RetValue == 0 )
continue;
p->nWinsUsed++;
// iterate through candidate resubstitutions
Vec_VecForEachLevel( p->vResubs, vFanins, k )
{
@ -247,26 +268,19 @@ p->timeSat += clock() - clk;
}
p->nProvedSets++;
// printf( " Unsat\n" );
continue;
// continue;
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
// interplate the problem if it was UNSAT
// interpolate the problem if it was UNSAT
clk = clock();
RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth );
nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += clock() - clk;
assert( RetValue == Vec_PtrSize(vFanins) - 2 );
if ( puTruth )
{
Extra_PrintBinary( stdout, puTruth, 1 << RetValue );
printf( "\n" );
}
continue;
assert( nFanins == Vec_PtrSize(vFanins) - 2 );
assert( puTruth );
// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
// transform interpolant into the AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
@ -276,10 +290,11 @@ p->timeInt += clock() - clk;
// update the network
clk = clock();
Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
p->timeUpd += clock() - clk;
break;
}
}
// quit resubstitution manager

172
src/opt/res/resDivs.c
View File

@ -25,6 +25,9 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Res_WinMarkTfi( Res_Win_t * p );
static int Res_WinVisitMffc( Res_Win_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -43,84 +46,155 @@
void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
{
Abc_Obj_t * pObj, * pFanout, * pFanin;
int i, k, f, m;
int k, f, m;
// set the maximum level of the divisors
p->nLevDivMax = nLevDivMax;
// mark the leaves and the internal nodes
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->fMarkA = 1;
Vec_VecForEachEntry( p->vLevels, pObj, i, k )
pObj->fMarkA = 1;
// prepare the new trav ID
// mark the TFI with the current trav ID
Abc_NtkIncrementTravId( p->pNode->pNtk );
// mark the TFO of the node (does not increment trav ID)
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
// mark the MFFC of the node (does not increment trav ID)
Res_WinMarkTfi( p );
// mark with the current trav ID those nodes that should not be divisors:
// (1) the node and its TFO
// (2) the MFFC of the node
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
Res_WinVisitMffc( p );
Abc_ObjForEachFanin( p->pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
// what about the fanouts of the leaves!!!
// at this point the nodes are marked with two trav IDs:
// nodes to be collected as divisors are marked with previous trav ID
// nodes to be avoided as divisors are marked with current trav ID
// go through all the legal levels and check if their fanouts can be divisors
p->nDivsPlus = 0;
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
// start collecting the divisors
Vec_PtrClear( p->vDivs );
Vec_PtrForEachEntry( p->vLeaves, pObj, k )
{
// skip nodes in the TFO or in the MFFC of node
if ( Abc_NodeIsTravIdCurrent(pObj) )
assert( (int)pObj->Level >= p->nLevLeafMin );
if ( !Abc_NodeIsTravIdPrevious(pObj) )
continue;
if ( (int)pObj->Level > p->nLevDivMax )
continue;
Vec_PtrPush( p->vDivs, pObj );
}
// add the internal nodes to the data structure
Vec_PtrForEachEntry( p->vNodes, pObj, k )
{
if ( !Abc_NodeIsTravIdPrevious(pObj) )
continue;
if ( (int)pObj->Level > p->nLevDivMax )
continue;
Vec_PtrPush( p->vDivs, pObj );
}
// explore the fanouts of already collected divisors
p->nDivsPlus = 0;
Vec_PtrForEachEntry( p->vDivs, pObj, k )
{
// consider fanouts of this node
Abc_ObjForEachFanout( pObj, pFanout, f )
{
// stop if there are too many fanouts
if ( f > 20 )
break;
// skip nodes that are already added
if ( pFanout->fMarkA )
continue;
// skip COs
if ( !Abc_ObjIsNode(pFanout) )
if ( Abc_NodeIsTravIdPrevious(pFanout) )
continue;
// skip nodes in the TFO or in the MFFC of node
if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue;
// skip nodes with large level
if ( (int)pFanout->Level > p->nLevDivMax )
// skip COs
if ( !Abc_ObjIsNode(pFanout) )
continue;
// skip nodes whose fanins are not in the cone
// skip nodes with large level
if ( (int)pFanout->Level >= p->nLevDivMax )
continue;
// skip nodes whose fanins are not divisors
Abc_ObjForEachFanin( pFanout, pFanin, m )
if ( !pFanin->fMarkA )
if ( !Abc_NodeIsTravIdPrevious(pFanin) )
break;
if ( m < Abc_ObjFaninNum(pFanout) )
continue;
// add the node
Res_WinAddNode( p, pFanout );
// add the node to the divisors
Vec_PtrPush( p->vDivs, pFanout );
Vec_PtrPush( p->vNodes, pFanout );
Abc_NodeSetTravIdPrevious( pFanout );
p->nDivsPlus++;
}
}
}
// unmark the leaves and the internal nodes
/**Function*************************************************************
Synopsis [Marks the TFI cone of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin;
int i;
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
Abc_NodeSetTravIdCurrent( pObj );
assert( Abc_ObjIsNode(pObj) );
// visit the fanins of the node
Abc_ObjForEachFanin( pObj, pFanin, i )
Res_WinMarkTfi_rec( p, pFanin );
}
/**Function*************************************************************
Synopsis [Marks the TFI cone of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinMarkTfi( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i;
// mark the leaves
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->fMarkA = 0;
Vec_VecForEachEntry( p->vLevels, pObj, i, k )
pObj->fMarkA = 0;
Abc_NodeSetTravIdCurrent( pObj );
// start from the node
Res_WinMarkTfi_rec( p, p->pNode );
}
// collect the divisors below the line
Vec_PtrClear( p->vDivs );
// collect the node fanins first and mark the fanins
Abc_ObjForEachFanin( p->pNode, pFanin, m )
{
Vec_PtrPush( p->vDivs, pFanin );
Abc_NodeSetTravIdCurrent( pFanin );
}
// collect the remaining leaves
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
if ( !Abc_NodeIsTravIdCurrent(pObj) )
Vec_PtrPush( p->vDivs, pObj );
// collect remaining unvisited divisors
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax )
if ( !Abc_NodeIsTravIdCurrent(pObj) )
Vec_PtrPush( p->vDivs, pObj );
/**Function*************************************************************
// verify the resulting window
// Res_WinVerify( p );
Synopsis [Marks the TFO of the collected nodes up to the given level.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
{
Abc_Obj_t * pFanout;
int i;
if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
return;
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
Abc_NodeSetTravIdCurrent( pObj );
Abc_ObjForEachFanout( pObj, pFanout, i )
Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit );
}
/**Function*************************************************************

10
src/opt/res/resFilter.c
View File

@ -42,7 +42,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
SeeAlso []
***********************************************************************/
int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs )
int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo;
@ -52,18 +52,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
printf( "Failed 1!" );
printf( "Failed 1!\n" );
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
printf( "Failed 2!" );
printf( "Failed 2!\n" );
// try removing fanins
// printf( "Fanins: " );
Counter = 0;
Vec_VecClear( vResubs );
Vec_VecClear( vResubsW );
Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
{
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
@ -78,7 +79,10 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
Abc_ObjForEachFanin( pWin->pNode, pFanin2, k )
{
if ( k != i )
{
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
Vec_VecPush( vResubsW, Counter, pFanin2 );
}
}
Counter++;
}

70
src/opt/res/resInt.h
View File

@ -42,49 +42,48 @@ extern "C" {
typedef struct Res_Win_t_ Res_Win_t;
struct Res_Win_t_
{
// the general data
int nWinTfiMax; // the fanin levels
int nWinTfoMax; // the fanout levels
int nLevLeaves; // the level where leaves begin
int nLevDivMax; // the maximum divisor level
int nDivsPlus; // the number of additional divisors
int nLeavesPlus;// the number of additional leaves
Abc_Obj_t * pNode; // the node in the center
// windowing parameters
Abc_Obj_t * pNode; // the node in the center
int nWinTfiMax; // the fanin levels
int nWinTfoMax; // the fanout levels
int nLevDivMax; // the maximum divisor level
// internal windowing parameters
int nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root)
int nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves
// derived windowing parameters
int nLevLeafMin; // the minimum level of a leaf
int nLevTravMin; // the minimum level to search from TFO
int nDivsPlus; // the number of additional divisors
// the window data
Vec_Vec_t * vLevels; // nodes by level
Vec_Ptr_t * vLeaves; // leaves of the window
Vec_Ptr_t * vRoots; // roots of the window
Vec_Ptr_t * vDivs; // the candidate divisors of the node
Vec_Ptr_t * vRoots; // outputs of the window
Vec_Ptr_t * vLeaves; // inputs of the window
Vec_Ptr_t * vBranches; // side nodes of the window
Vec_Ptr_t * vNodes; // internal nodes of the window
Vec_Ptr_t * vDivs; // candidate divisors of the node
// temporary data
Vec_Vec_t * vMatrix; // TFI nodes below the given node
};
typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
Abc_Ntk_t * pAig; // AIG for simulation
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
Vec_Ptr_t * vPats; // input simulation patterns
Vec_Ptr_t * vPats0; // input simulation patterns
Vec_Ptr_t * vPats1; // input simulation patterns
Vec_Ptr_t * vOuts; // output simulation info
int nPats0; // the number of 0-patterns accumulated
int nPats1; // the number of 1-patterns accumulated
Vec_Ptr_t * vPats; // input simulation patterns
Vec_Ptr_t * vPats0; // input simulation patterns
Vec_Ptr_t * vPats1; // input simulation patterns
Vec_Ptr_t * vOuts; // output simulation info
int nPats0; // the number of 0-patterns accumulated
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
Vec_Vec_t * vCands; // resubstitution candidates
};
// adds one node to the window
static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
{
assert( !pObj->fMarkA );
pObj->fMarkA = 1;
Vec_VecPush( p->vLevels, pObj->Level, pObj );
}
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -95,11 +94,12 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern int Res_WinVisitMffc( Res_Win_t * p );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
/*=== resFilter.c ==========================================================*/
extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs );
extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
@ -111,7 +111,7 @@ extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, H
/*=== resWnd.c ==========================================================*/
extern Res_Win_t * Res_WinAlloc();
extern void Res_WinFree( Res_Win_t * p );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode );
extern int Res_WinIsTrivial( Res_Win_t * p );
extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );

62
src/opt/res/resSat.c
View File

@ -37,7 +37,7 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int
/**Function*************************************************************
Synopsis [Loads AIG into the SAT solver.]
Synopsis [Loads AIG into the SAT solver for checking resubstitution.]
Description []
@ -124,6 +124,66 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
return pCnf;
}
/**Function*************************************************************
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
Description [The array of fanins contains exactly two entries: the
care set and the functions.]
SideEffects []
SeeAlso []
***********************************************************************/
void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
{
sat_solver * pSat;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj;
int i, nNodes;
// make sure fanins contain POs of the AIG
pObj = Vec_PtrEntry( vFanins, 0 );
assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
assert( Vec_PtrSize(vFanins) == 2 );
// collect reachable nodes
vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
// assign unique numbers to each node
nNodes = 0;
Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i )
pObj->pCopy = (void *)nNodes++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pCopy = (void *)nNodes++;
Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
pObj->pCopy = (void *)nNodes++;
// start the solver
pSat = sat_solver_new();
// add clause for the constant node
Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
Vec_PtrForEachEntry( vNodes, pObj, i )
Res_SatAddAnd( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
// add clauses for POs
Vec_PtrForEachEntry( vFanins, pObj, i )
Res_SatAddEqual( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
pObj = Vec_PtrEntry(vFanins, 0);
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
pObj = Vec_PtrEntry(vFanins, 1);
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
return pSat;
}
/**Function*************************************************************
Synopsis [Asserts equality of the variable to a constant.]

6
src/opt/res/resSim.c
View File

@ -484,13 +484,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
Res_SimProcessPats( p );
if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
break;
}
// printf( "%d ", Limit );
// report the last set of patterns
Res_SimReportOne( p );
printf( "\n" );
// Res_SimReportOne( p );
// printf( "\n" );
// quit if there is not enough
// if ( p->nPats0 < 4 || p->nPats1 < 4 )
if ( p->nPats0 < 4 || p->nPats1 < 4 )
{
// Res_SimReportOne( p );

22
src/opt/res/resStrash.c
View File

@ -48,22 +48,25 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
Vec_Ptr_t * vPairs;
Abc_Ntk_t * pAig;
Abc_Obj_t * pObj, * pMiter;
int i, k;
int i;
assert( Abc_NtkHasAig(p->pNode->pNtk) );
// Abc_NtkCleanCopy( p->pNode->pNtk );
// create the network
pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pAig->pName = Extra_UtilStrsav( "window" );
// create the inputs
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->pCopy = Abc_NtkCreatePi( pAig );
Vec_PtrForEachEntry( p->vBranches, pObj, i )
pObj->pCopy = Abc_NtkCreatePi( pAig );
// go through the nodes in the topological order
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
Vec_PtrForEachEntry( p->vNodes, pObj, i )
{
pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
if ( pObj == p->pNode )
pObj->pCopy = Abc_ObjNot( pObj->pCopy );
}
// collect the PO outputs
// collect the POs
vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
Vec_PtrForEachEntry( p->vRoots, pObj, i )
{
@ -72,15 +75,17 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
}
// mark the TFO of the node
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL );
// redo strashing in the TFO
Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax );
// update strashing of the node
p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax )
Abc_NodeSetTravIdPrevious( p->pNode );
// redo strashing in the TFO
Vec_PtrForEachEntry( p->vNodes, pObj, i )
{
if ( Abc_NodeIsTravIdCurrent(pObj) )
pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
}
// collect the PO outputs
// collect the POs
Vec_PtrForEachEntry( p->vRoots, pObj, i )
Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
// add the miter
@ -89,6 +94,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
Vec_PtrFree( vPairs );
// add the node
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
// add the fanins
Abc_ObjForEachFanin( p->pNode, pObj, i )
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
// add the divisors
Vec_PtrForEachEntry( p->vDivs, pObj, i )
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );

8
src/opt/res/resUpdate.c
View File

@ -45,11 +45,11 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
int i, k, m;
int Lev, k, m;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, i )
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
pObjNew->Level = pObj->Level;
@ -62,12 +62,12 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( vLevels, pTemp, i, k, pObjNew->Level )
Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
{
pTemp->fMarkA = 0;
pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
// if the level did not change, to need to check the fanout levels
if ( (int)pTemp->Level == i )
if ( (int)pTemp->Level == Lev )
continue;
// schedule fanout for level update
Abc_ObjForEachFanout( pTemp, pFanout, m )

412
src/opt/res/resWin.c
View File

@ -43,12 +43,19 @@
Res_Win_t * Res_WinAlloc()
{
Res_Win_t * p;
// start the manager
p = ALLOC( Res_Win_t, 1 );
memset( p, 0, sizeof(Res_Win_t) );
p->vLevels = Vec_VecStart( 128 );
p->vLeaves = Vec_PtrAlloc( 512 );
p->vRoots = Vec_PtrAlloc( 512 );
p->vDivs = Vec_PtrAlloc( 512 );
// set internal parameters
p->nFanoutLimit = 10;
p->nLevTfiMinus = 3;
// allocate storage
p->vRoots = Vec_PtrAlloc( 256 );
p->vLeaves = Vec_PtrAlloc( 256 );
p->vBranches = Vec_PtrAlloc( 256 );
p->vNodes = Vec_PtrAlloc( 256 );
p->vDivs = Vec_PtrAlloc( 256 );
p->vMatrix = Vec_VecStart( 128 );
return p;
}
@ -65,48 +72,87 @@ Res_Win_t * Res_WinAlloc()
***********************************************************************/
void Res_WinFree( Res_Win_t * p )
{
Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vRoots );
Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vBranches );
Vec_PtrFree( p->vNodes );
Vec_PtrFree( p->vDivs );
Vec_VecFree( p->vMatrix );
free( p );
}
/**Function*************************************************************
Synopsis [Collects nodes in the limited TFI of the node.]
Synopsis [Collect the limited TFI cone of the node.]
Description [Marks the collected nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinCollectNodeTfi( Res_Win_t * p )
void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
{
Vec_Ptr_t * vFront;
Abc_Obj_t * pObj, * pFanin;
Abc_Obj_t * pObj, * pTemp;
int i, k, m;
// expand storage for levels
if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
// start the frontier
Vec_VecClear( p->vLevels );
Res_WinAddNode( p, p->pNode );
// add one level at a time
Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 )
assert( p->nWinTfiMax > 0 );
assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax );
// start matrix with the node
Vec_VecClear( p->vMatrix );
Vec_VecPush( p->vMatrix, 0, p->pNode );
Abc_NtkIncrementTravId( p->pNode->pNtk );
Abc_NodeSetTravIdCurrent( p->pNode );
// collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
Vec_PtrClear( p->vLeaves );
Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax )
{
Vec_PtrForEachEntry( vFront, pObj, k )
Abc_ObjForEachFanin( pObj, pFanin, m )
if ( !pFanin->fMarkA )
Res_WinAddNode( p, pFanin );
{
Abc_ObjForEachFanin( pObj, pTemp, m )
{
if ( Abc_NodeIsTravIdCurrent( pTemp ) )
continue;
Abc_NodeSetTravIdCurrent( pTemp );
if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax )
Vec_PtrPush( p->vLeaves, pTemp );
else
Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp );
}
}
}
assert( Vec_PtrSize(p->vLeaves) > 0 );
// collect the nodes in the reverse order
Vec_PtrClear( p->vNodes );
Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 )
{
Vec_PtrForEachEntry( vFront, pObj, k )
Vec_PtrPush( p->vNodes, pObj );
Vec_PtrClear( vFront );
}
// get the lowest leaf level
p->nLevLeafMin = ABC_INFINITY;
Vec_PtrForEachEntry( p->vLeaves, pObj, k )
p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level );
// set minimum traversal level
p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
assert( p->nLevTravMin >= 0 );
}
/**Function*************************************************************
Synopsis [Collect all the nodes that fanin into the window nodes.]
Synopsis [Returns 1 if the node should be a root.]
Description []
@ -115,48 +161,25 @@ void Res_WinCollectNodeTfi( Res_Win_t * p )
SeeAlso []
***********************************************************************/
void Res_WinCollectLeaves( Res_Win_t * p )
{
Vec_Ptr_t * vLevel;
Abc_Obj_t * pObj;
int i, k;
// add the leaves
Vec_PtrClear( p->vLeaves );
// collect the nodes below the given level
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
Vec_PtrPush( p->vLeaves, pObj );
// remove leaves from the set
Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
Vec_PtrClear( vLevel );
}
/**Function*************************************************************
Synopsis [Marks the TFO of the collected nodes up to the given level.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
{
Abc_Obj_t * pFanout;
int i;
if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
return;
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
Abc_NodeSetTravIdCurrent( pObj );
Abc_ObjForEachFanout( pObj, pFanout, i )
Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
// the node is the root if one of the following is true:
// (1) the node has more than fanouts than the limit
if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
return 1;
// (2) the node has CO fanouts
// (3) the node has fanouts above the cutoff level
Abc_ObjForEachFanout( pNode, pFanout, i )
if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Marks the TFO of the collected nodes up to the given level.]
Synopsis [Recursively collects the root candidates.]
Description []
@ -165,15 +188,112 @@ void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNo
SeeAlso []
***********************************************************************/
void Res_WinSweepLeafTfo( Res_Win_t * p )
void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
{
Abc_Obj_t * pFanout;
int i;
assert( Abc_ObjIsNode(pNode) );
if ( Abc_NodeIsTravIdCurrent(pNode) )
return;
Abc_NodeSetTravIdCurrent( pNode );
// check if the node should be the root
if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
Vec_PtrPush( vRoots, pNode );
else // if not, explore its fanouts
Abc_ObjForEachFanout( pNode, pFanout, i )
Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
}
/**Function*************************************************************
Synopsis [Recursively collects the root candidates.]
Description [Returns 1 if the only root is this node.]
SideEffects []
SeeAlso []
***********************************************************************/
int Res_WinComputeRoots( Res_Win_t * p )
{
Vec_PtrClear( p->vRoots );
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots );
assert( Vec_PtrSize(p->vRoots) > 0 );
if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Marks the paths from the roots to the leaves.]
Description [Returns 1 if the the node can reach a leaf.]
SideEffects []
SeeAlso []
***********************************************************************/
int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin )
{
Abc_Obj_t * pFanin;
int i, RetValue;
// skip visited nodes
if ( Abc_NodeIsTravIdCurrent(pNode) )
return 1;
if ( Abc_NodeIsTravIdPrevious(pNode) )
return 0;
// assume that the node does not have access to the leaves
Abc_NodeSetTravIdPrevious( pNode );
// skip nodes below the given level
if ( pNode == pPivot || (int)pNode->Level <= nLevelMin )
return 0;
assert( Abc_ObjIsNode(pNode) );
// check if the fanins have access to the leaves
RetValue = 0;
Abc_ObjForEachFanin( pNode, pFanin, i )
RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin );
// relabel the node if it has access to the leaves
if ( RetValue )
Abc_NodeSetTravIdCurrent( pNode );
return RetValue;
}
/**Function*************************************************************
Synopsis [Marks the paths from the roots to the leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinMarkPaths( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i;
// mark the leaves
Abc_NtkIncrementTravId( p->pNode->pNtk );
Abc_NtkIncrementTravId( p->pNode->pNtk );
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
Res_WinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
Abc_NodeSetTravIdCurrent( pObj );
// traverse from the roots and mark the nodes that can reach leaves
// the nodes that do not reach leaves have previous trav ID
// the nodes that reach leaves have current trav ID
Vec_PtrForEachEntry( p->vRoots, pObj, i )
Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin );
}
/**Function*************************************************************
Synopsis [Recursively collects the roots.]
@ -185,29 +305,27 @@ void Res_WinSweepLeafTfo( Res_Win_t * p )
SeeAlso []
***********************************************************************/
void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
{
Abc_Obj_t * pFanout;
int i;
assert( Abc_ObjIsNode(pObj) );
assert( Abc_NodeIsTravIdCurrent(pObj) );
// check if the node has all fanouts marked
Abc_ObjForEachFanout( pObj, pFanout, i )
if ( !Abc_NodeIsTravIdCurrent(pFanout) )
break;
// if some of the fanouts are unmarked, add the node to the root
// if some of the fanouts are unmarked, add the node to the roots
if ( i < Abc_ObjFanoutNum(pObj) )
{
Vec_PtrPushUnique( vRoots, pObj );
return;
}
// otherwise, call recursively
Abc_ObjForEachFanout( pObj, pFanout, i )
Res_WinCollectRoots_rec( pFanout, vRoots );
else // otherwise, call recursively
Abc_ObjForEachFanout( pObj, pFanout, i )
Res_WinFinalizeRoots_rec( pFanout, vRoots );
}
/**Function*************************************************************
Synopsis [Collects the roots of the window.]
Synopsis [Finalizes the roots of the window.]
Description [Roots of the window are the nodes that have at least
one fanout that it not in the TFO of the leaves.]
@ -217,13 +335,21 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
SeeAlso []
***********************************************************************/
void Res_WinCollectRoots( Res_Win_t * p )
int Res_WinFinalizeRoots( Res_Win_t * p )
{
assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
// mark the node with the old traversal ID
Abc_NodeSetTravIdCurrent( p->pNode );
// recollect the roots
Vec_PtrClear( p->vRoots );
Res_WinCollectRoots_rec( p->pNode, p->vRoots );
Res_WinFinalizeRoots_rec( p->pNode, p->vRoots );
assert( Vec_PtrSize(p->vRoots) > 0 );
if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Recursively adds missing nodes and leaves.]
@ -235,23 +361,27 @@ void Res_WinCollectRoots( Res_Win_t * p )
SeeAlso []
***********************************************************************/
void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
{
Abc_Obj_t * pFanin;
int i;
if ( pObj->fMarkA )
// skip the already collected leaves, nodes, and branches
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
// if this is not an internal node - make it a new branch
if ( !Abc_NodeIsTravIdPrevious(pObj) )
{
p->nLeavesPlus++;
Vec_PtrPush( p->vLeaves, pObj );
pObj->fMarkA = 1;
Abc_NodeSetTravIdCurrent( pObj );
Vec_PtrPush( p->vBranches, pObj );
return;
}
Res_WinAddNode( p, pObj );
assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect!
Abc_NodeSetTravIdCurrent( pObj );
// visit the fanins of the node
Abc_ObjForEachFanin( pObj, pFanin, i )
Res_WinAddMissing_rec( p, pFanin );
Res_WinAddMissing_rec( p, pFanin, nLevTravMin );
// collect the node
Vec_PtrPush( p->vNodes, pObj );
}
/**Function*************************************************************
@ -269,66 +399,36 @@ void Res_WinAddMissing( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i;
Vec_PtrForEachEntry( p->vRoots, pObj, i )
Res_WinAddMissing_rec( p, pObj );
}
/**Function*************************************************************
Synopsis [Unmarks the leaves and nodes of the window.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinUnmark( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i, k;
Vec_VecForEachEntry( p->vLevels, pObj, i, k )
pObj->fMarkA = 0;
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->fMarkA = 0;
}
/**Function*************************************************************
Synopsis [Verifies the window.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_WinVerify( Res_Win_t * p )
{
Abc_Obj_t * pObj, * pFanin;
int i, k, f;
// make sure the nodes are not marked
Abc_NtkForEachObj( p->pNode->pNtk, pObj, i )
assert( !pObj->fMarkA );
// mark the leaves
Abc_NtkIncrementTravId( p->pNode->pNtk );
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->fMarkA = 1;
// make sure all nodes in the topological order have their fanins in the set
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
{
assert( (int)pObj->Level == i );
assert( !pObj->fMarkA );
Abc_ObjForEachFanin( pObj, pFanin, f )
assert( pFanin->fMarkA );
pObj->fMarkA = 1;
}
// make sure the roots are marked
Abc_NodeSetTravIdCurrent( pObj );
// mark the already collected nodes
Vec_PtrForEachEntry( p->vNodes, pObj, i )
Abc_NodeSetTravIdCurrent( pObj );
// explore from the roots
Vec_PtrClear( p->vBranches );
Vec_PtrForEachEntry( p->vRoots, pObj, i )
assert( pObj->fMarkA );
// unmark
Res_WinUnmark( p );
Res_WinAddMissing_rec( p, pObj, p->nLevTravMin );
}
/**Function*************************************************************
Synopsis [Returns 1 if the window is trivial (without TFO).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Res_WinIsTrivial( Res_Win_t * p )
{
return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
}
/**Function*************************************************************
@ -345,31 +445,29 @@ void Res_WinVerify( Res_Win_t * p )
int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
{
assert( Abc_ObjIsNode(pNode) );
assert( nWinTfiMax > 0 && nWinTfoMax > 0 );
assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );
// initialize the window
p->pNode = pNode;
p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
p->nLeavesPlus = 0;
p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
// collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
Res_WinCollectNodeTfi( p );
// find the leaves of the window
Res_WinCollectLeaves( p );
// mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
Res_WinSweepLeafTfo( p );
// find the roots of the window
Res_WinCollectRoots( p );
// add the nodes in the TFI of the roots that are not yet in the window
Res_WinAddMissing( p );
// unmark window nodes
Res_WinUnmark( p );
// clear the divisor information
p->nLevDivMax = 0;
p->nDivsPlus = 0;
Vec_PtrClear( p->vDivs );
// verify the resulting window
// Res_WinVerify( p );
Vec_PtrClear( p->vRoots );
Vec_PtrPush( p->vRoots, pNode );
// compute the leaves
Res_WinCollectLeavesAndNodes( p );
// compute the candidate roots
if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
{
// mark the paths from the roots to the leaves
Res_WinMarkPaths( p );
// refine the roots and add branches and missing nodes
if ( Res_WinFinalizeRoots( p ) )
Res_WinAddMissing( p );
}
return 1;
}

42
src/sat/bsat/satInter.c
View File

@ -771,7 +771,8 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
{
// construct the proof
Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
if ( p->fVerbose )
printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
return 0;
}
@ -827,7 +828,7 @@ int Int_ManProcessRoots( Int_Man_t * p )
if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
{
// detected root level conflict
printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
assert( 0 );
return 0;
}
@ -838,8 +839,9 @@ int Int_ManProcessRoots( Int_Man_t * p )
if ( pClause )
{
// detected root level conflict
printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
// assert( 0 );
Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
if ( p->fVerbose )
printf( "Found root level conflict!\n" );
return 0;
}
@ -925,17 +927,12 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
p->pCnf = pCnf;
p->fVerbose = fVerbose;
*ppResult = NULL;
// adjust the manager
Int_ManResize( p );
// propagate root level assignments
if ( !Int_ManProcessRoots( p ) )
{
*ppResult = NULL;
return p->nVarsAB;
}
// prepare the interpolant computation
Int_ManPrepareInter( p );
@ -951,15 +948,19 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
Sto_ManForEachClauseRoot( p->pCnf, pClause )
Int_ManProofWriteOne( p, pClause );
// consider each learned clause
Sto_ManForEachClause( p->pCnf, pClause )
// propagate root level assignments
if ( Int_ManProcessRoots( p ) )
{
if ( pClause->fRoot )
continue;
if ( !Int_ManProofRecordOne( p, pClause ) )
// if there is no conflict, consider learned clauses
Sto_ManForEachClause( p->pCnf, pClause )
{
RetValue = 0;
break;
if ( pClause->fRoot )
continue;
if ( !Int_ManProofRecordOne( p, pClause ) )
{
RetValue = 0;
break;
}
}
}
@ -970,12 +971,15 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
p->pFile = NULL;
}
if ( fVerbose )
{
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += clock() - clkTotal;
}
*ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
return p->nVarsAB;
}

4
src/sat/bsat/satSolver.c
View File

@ -1264,7 +1264,7 @@ void sat_solver_store_alloc( sat_solver * s )
void sat_solver_store_write( sat_solver * s, char * pFileName )
{
extern void Sto_ManDumpClauses( void * p, char * pFileName );
Sto_ManDumpClauses( s->pStore, pFileName );
if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
}
void sat_solver_store_free( sat_solver * s )
@ -1273,7 +1273,7 @@ void sat_solver_store_free( sat_solver * s )
if ( s->pStore ) Sto_ManFree( s->pStore );
s->pStore = NULL;
}
void sat_solver_store_mark_roots( sat_solver * s )
{
extern void Sto_ManMarkRoots( void * p );