Version abc70703

This commit is contained in:
Alan Mishchenko 2007-07-03 08:01:00 -07:00
parent d6804597a3
commit a8db621dc9
42 changed files with 8076 additions and 781 deletions

88
abc.dsp
View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
@ -822,10 +822,6 @@ SOURCE=.\src\aig\dar\darCheck.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darCore.c
# End Source File
# Begin Source File
@ -838,10 +834,6 @@ SOURCE=.\src\aig\dar\darData.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darData2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darDfs.c
# End Source File
# Begin Source File
@ -881,6 +873,82 @@ SOURCE=.\src\aig\dar\darTruth.c
SOURCE=.\src\aig\dar\darUtil.c
# End Source File
# End Group
# Begin Group "fra"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\fra\fra.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraAnd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraClass.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraSat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraSim.c
# End Source File
# End Group
# Begin Group "cnf"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\cnf\cnf.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfCut.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfData.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfPost.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfWrite.c
# End Source File
# End Group
# End Group
# Begin Group "bdd"

7
abc.rc
View File

@ -80,6 +80,7 @@ alias u undo
alias w write
alias wa write_aiger
alias wb write_bench
alias wc write_cnf
alias wh write_hie
alias wl write_blif
alias wp write_pla
@ -141,7 +142,7 @@ alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
alias chnew "st; haig_start; resyn2; haig_use"
alias chnewrs "st; haig_start; resyn2rs; haig_use"
alias t "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
alias t0 "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
alias t1 "read_dsd a*(b+(c*d)); clp -r; print_dsd"
alias t2 "read_dsd 56BA(a,b,c,d); clp -r; print_dsd"
alias t3 "read_dsd 56BA(a,b*c,e,d); clp -r; print_dsd"
@ -167,3 +168,7 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
alias bug "r pj1_if3.blif; lp"
alias table "r lutexp.baf; test"
alias t "r c.blif; st; wc c.cnf"

148
src/aig/cnf/cnf.h Normal file
View File

@ -0,0 +1,148 @@
/**CFile****************************************************************
FileName [cnf.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CNF_H__
#define __CNF_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "dar.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Cnf_Man_t_ Cnf_Man_t;
typedef struct Cnf_Dat_t_ Cnf_Dat_t;
typedef struct Cnf_Cut_t_ Cnf_Cut_t;
// the CNF asserting outputs of AIG to be 1
struct Cnf_Dat_t_
{
Dar_Man_t * pMan; // the AIG manager, for which CNF is computed
int nVars; // the number of variables
int nLiterals; // the number of CNF literals
int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
};
// the cut used to represent node in the AIG
struct Cnf_Cut_t_
{
char nFanins; // the number of leaves
char Cost; // the cost of this cut
short nWords; // the number of words in truth table
Vec_Int_t * vIsop[2]; // neg/pos ISOPs
int pFanins[0]; // the fanins (followed by the truth table)
};
// the CNF computation manager
struct Cnf_Man_t_
{
Dar_Man_t * pManAig; // the underlying AIG manager
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
Dar_MmFlex_t * pMemCuts; // memory manager for cuts
int nMergeLimit; // the limit on the size of merged cut
unsigned * pTruths[4]; // temporary truth tables
Vec_Int_t * vMemory; // memory for intermediate ISOP representation
};
static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut->nFanins; }
static inline int * Cnf_CutLeaves( Cnf_Cut_t * pCut ) { return pCut->pFanins; }
static inline unsigned * Cnf_CutTruth( Cnf_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
static inline Cnf_Cut_t * Cnf_ObjBestCut( Dar_Obj_t * pObj ) { return pObj->pData; }
static inline void Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over leaves of the cut
#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCore.c ========================================================*/
extern Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig );
/*=== cnfCut.c ========================================================*/
extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj );
extern void Cnf_CutPrint( Cnf_Cut_t * pCut );
extern void Cnf_CutFree( Cnf_Cut_t * pCut );
extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
extern Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
/*=== cnfData.c ========================================================*/
extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== cnfMan.c ========================================================*/
extern Cnf_Man_t * Cnf_ManStart();
extern void Cnf_ManStop( Cnf_Man_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
/*=== cnfMap.c ========================================================*/
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
/*=== cnfPost.c ========================================================*/
extern void Cnf_ManTransferCuts( Cnf_Man_t * p );
extern void Cnf_ManFreeCuts( Cnf_Man_t * p );
extern void Cnf_ManPostprocess( Cnf_Man_t * p );
/*=== cnfUtil.c ========================================================*/
extern Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect );
/*=== cnfWrite.c ========================================================*/
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

101
src/aig/cnf/cnfCore.c Normal file
View File

@ -0,0 +1,101 @@
/**CFile****************************************************************
FileName [cnfCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig )
{
Cnf_Dat_t * pCnf = NULL;
Vec_Ptr_t * vMapped;
int nIters = 2;
int clk;
// connect the managers
pAig->pManCnf = p;
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
Dar_ManComputeCuts( pAig );
PRT( "Cuts", clock() - clk );
/*
// iteratively improve area flow
for ( i = 0; i < nIters; i++ )
{
clk = clock();
Cnf_ManScanMapping( p, 0 );
Cnf_ManMapForCnf( p );
PRT( "iter ", clock() - clk );
}
*/
// write the file
vMapped = Dar_ManScanMapping( p, 1 );
Vec_PtrFree( vMapped );
clk = clock();
Cnf_ManTransferCuts( p );
Cnf_ManPostprocess( p );
Cnf_ManScanMapping( p, 0 );
/*
Cnf_ManPostprocess( p );
Cnf_ManScanMapping( p, 0 );
Cnf_ManPostprocess( p );
Cnf_ManScanMapping( p, 0 );
*/
PRT( "Ext ", clock() - clk );
/*
vMapped = Cnf_ManScanMapping( p, 1 );
pCnf = Cnf_ManWriteCnf( p, vMapped );
Vec_PtrFree( vMapped );
// clean up
Cnf_ManFreeCuts( p );
Dar_ManCutsFree( pAig );
return pCnf;
*/
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

371
src/aig/cnf/cnfCut.c Normal file
View File

@ -0,0 +1,371 @@
/**CFile****************************************************************
FileName [cnfCut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates cut of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves )
{
Cnf_Cut_t * pCut;
int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Dar_TruthWordNum(nLeaves);
pCut = (Cnf_Cut_t *)Dar_MmFlexEntryFetch( p->pMemCuts, nSize );
pCut->nFanins = nLeaves;
pCut->nWords = Dar_TruthWordNum(nLeaves);
pCut->vIsop[0] = pCut->vIsop[1] = NULL;
return pCut;
}
/**Function*************************************************************
Synopsis [Deallocates cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutFree( Cnf_Cut_t * pCut )
{
if ( pCut->vIsop[0] )
Vec_IntFree( pCut->vIsop[0] );
if ( pCut->vIsop[1] )
Vec_IntFree( pCut->vIsop[1] );
}
/**Function*************************************************************
Synopsis [Creates cut for the given node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj )
{
Dar_Cut_t * pCutBest;
Cnf_Cut_t * pCut;
unsigned * pTruth;
assert( Dar_ObjIsNode(pObj) );
pCutBest = Dar_ObjBestCut( pObj );
assert( pCutBest != NULL );
assert( pCutBest->nLeaves <= 4 );
pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
pTruth = Cnf_CutTruth(pCut);
*pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
pCut->Cost = p->pSopSizes[0xFFFF & *pTruth] + p->pSopSizes[0xFFFF & ~*pTruth];
return pCut;
}
/**Function*************************************************************
Synopsis [Deallocates cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutPrint( Cnf_Cut_t * pCut )
{
int i;
printf( "{" );
for ( i = 0; i < pCut->nFanins; i++ )
printf( "%d ", pCut->pFanins[i] );
printf( " } " );
}
/**Function*************************************************************
Synopsis [Allocates cut of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
Dar_Obj_t * pObj;
int i;
Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
{
assert( pObj->nRefs > 0 );
pObj->nRefs--;
}
}
/**Function*************************************************************
Synopsis [Allocates cut of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut )
{
Dar_Obj_t * pObj;
int i;
Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
{
pObj->nRefs++;
}
}
/**Function*************************************************************
Synopsis [Allocates cut of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes )
{
Cnf_CutDeref( p, pCut );
Cnf_CutDeref( p, pCutFan );
Cnf_CutRef( p, pCutRes );
}
/**Function*************************************************************
Synopsis [Merges two arrays of integers.]
Description [Returns the number of items.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cnf_CutMergeLeaves( Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int * pFanins )
{
int i, k, nFanins = 0;
for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; )
{
if ( pCut->pFanins[i] == pCutFan->pFanins[k] )
pFanins[nFanins++] = pCut->pFanins[i], i++, k++;
else if ( pCut->pFanins[i] < pCutFan->pFanins[k] )
pFanins[nFanins++] = pCut->pFanins[i], i++;
else
pFanins[nFanins++] = pCutFan->pFanins[k], k++;
}
for ( ; i < pCut->nFanins; i++ )
pFanins[nFanins++] = pCut->pFanins[i];
for ( ; k < pCutFan->nFanins; k++ )
pFanins[nFanins++] = pCutFan->pFanins[k];
return nFanins;
}
/**Function*************************************************************
Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Cnf_TruthPhase( Cnf_Cut_t * pCut, Cnf_Cut_t * pCut1 )
{
unsigned uPhase = 0;
int i, k;
for ( i = k = 0; i < pCut->nFanins; i++ )
{
if ( k == pCut1->nFanins )
break;
if ( pCut->pFanins[i] < pCut1->pFanins[k] )
continue;
assert( pCut->pFanins[i] == pCut1->pFanins[k] );
uPhase |= (1 << i);
k++;
}
return uPhase;
}
/**Function*************************************************************
Synopsis [Removes the fanin variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutRemoveIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
{
int i;
assert( pCut->pFanins[iVar] == iFan );
pCut->nFanins--;
for ( i = iVar; i < pCut->nFanins; i++ )
pCut->pFanins[i] = pCut->pFanins[i+1];
}
/**Function*************************************************************
Synopsis [Inserts the fanin variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutInsertIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
{
int i;
for ( i = pCut->nFanins; i > iVar; i-- )
pCut->pFanins[i] = pCut->pFanins[i-1];
pCut->pFanins[iVar] = iFan;
pCut->nFanins++;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description [Returns NULL of the cuts cannot be merged.]
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan )
{
Cnf_Cut_t * pCutRes;
static int pFanins[32];
unsigned * pTruth, * pTruthFan, * pTruthRes;
unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
unsigned uPhase, uPhaseFan;
int i, iVar, nFanins, RetValue;
// make sure the second cut is the fanin of the first
for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
if ( pCut->pFanins[iVar] == iFan )
break;
assert( iVar < pCut->nFanins );
// remove this variable
Cnf_CutRemoveIthVar( pCut, iVar, iFan );
// merge leaves of the cuts
nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
if ( nFanins+1 > p->nMergeLimit )
{
Cnf_CutInsertIthVar( pCut, iVar, iFan );
return NULL;
}
// create new cut
pCutRes = Cnf_CutAlloc( p, nFanins );
memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
// derive its truth table
// get the truth tables in the composition space
pTruth = Cnf_CutTruth(pCut);
pTruthFan = Cnf_CutTruth(pCutFan);
pTruthRes = Cnf_CutTruth(pCutRes);
for ( i = 0; i < 2*pCutRes->nWords; i++ )
pTop[i] = pTruth[i % pCut->nWords];
for ( i = 0; i < pCutRes->nWords; i++ )
pFan[i] = pTruthFan[i % pCutFan->nWords];
// move the variable to the end
uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
// compute the phases
uPhase = Cnf_TruthPhase( pCutRes, pCut ) | (1 << pCutRes->nFanins);
uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
// permute truth-tables to the common support
Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1, pCutRes->nFanins+1, uPhase, 1 );
Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins, uPhaseFan, 1 );
// perform Boolean operation
Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
// return the cut to its original condition
Cnf_CutInsertIthVar( pCut, iVar, iFan );
// consider the simple case
if ( pCutRes->nFanins < 5 )
{
pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
return pCutRes;
}
// derive ISOP for positive phase
RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
// derive ISOP for negative phase
Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
// compute the cut cost
if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
pCutRes->Cost = 127;
else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
pCutRes->Cost = 127;
else
pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
return pCutRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [dar_.c]
FileName [cnfData.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
@ -14,11 +14,11 @@
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: dar_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
Revision [$Id: cnfData.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dar.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -4531,7 +4531,7 @@ NULL
SeeAlso []
***********************************************************************/
void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops )
void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops )
{
unsigned uMasks[4][2] = {
{ 0x5555, 0xAAAA },
@ -4566,6 +4566,7 @@ void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops )
// set pointers and compute SOP sizes
pSopSizes = ALLOC( char, 65536 );
pSops = ALLOC( char *, 65536 );
pSopSizes[0] = 0;
pSops[0] = NULL;
pPrev = pMemory;
for ( k = 0, i = 1; i < 65536; k++ )

173
src/aig/cnf/cnfMan.c Normal file
View File

@ -0,0 +1,173 @@
/**CFile****************************************************************
FileName [cnfMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Man_t * Cnf_ManStart()
{
Cnf_Man_t * p;
int i;
// allocate the manager
p = ALLOC( Cnf_Man_t, 1 );
memset( p, 0, sizeof(Cnf_Man_t) );
// derive internal data structures
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// allocate memory manager for cuts
p->pMemCuts = Dar_MmFlexStart();
p->nMergeLimit = 10;
// allocate temporary truth tables
p->pTruths[0] = ALLOC( unsigned, 4 * Dar_TruthWordNum(p->nMergeLimit) );
for ( i = 1; i < 4; i++ )
p->pTruths[i] = p->pTruths[i-1] + Dar_TruthWordNum(p->nMergeLimit);
p->vMemory = Vec_IntAlloc( 1 << 18 );
return p;
}
/**Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_ManStop( Cnf_Man_t * p )
{
Vec_IntFree( p->vMemory );
free( p->pTruths[0] );
Dar_MmFlexStop( p->pMemCuts, 0 );
free( p->pSopSizes );
free( p->pSops[1] );
free( p->pSops );
free( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_DataFree( Cnf_Dat_t * p )
{
if ( p == NULL )
return;
free( p->pClauses[0] );
free( p->pClauses );
free( p->pVarNums );
free( p );
}
/**Function*************************************************************
Synopsis [Writes CNF into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
{
FILE * pFile;
int * pLit, * pStop, i;
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
return;
}
fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
fprintf( pFile, "p %d %d\n", p->nVars, p->nClauses );
for ( i = 0; i < p->nClauses; i++ )
{
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
fprintf( pFile, "%d ", Cnf_Lit2Var(*pLit) );
fprintf( pFile, "0\n" );
}
fprintf( pFile, "\n" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Writes CNF into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
{
sat_solver * pSat;
int i;
pSat = sat_solver_new();
sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < p->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
return pSat;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

271
src/aig/cnf/cnfMap.c Normal file
View File

@ -0,0 +1,271 @@
/**CFile****************************************************************
FileName [cnfMap.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
}
}
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i, Area = pCut->Cost;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs >= 0 );
if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
}
return Area;
}
/**Function*************************************************************
Synopsis [Computes exact area of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
{
int Area;
Area = Dar_CutRef( p, pCut );
Dar_CutDeref( p, pCut );
return Area;
}
/**Function*************************************************************
Synopsis [Returns 1 if the second cut is better.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cnf_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
{
if ( pC0->Area < pC1->Area - 0.0001 )
return -1;
if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better
return 1;
// if ( pC0->NoRefs < pC1->NoRefs )
// return -1;
// if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better
// return 1;
// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves )
// return -1;
// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves )
// return 1; // larger average fanin ref-counter is better
// return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns the cut with the smallest area flow.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut, * pCutBest;
int i;
pCutBest = NULL;
Dar_ObjForEachCut( pObj, pCut, i )
if ( pCutBest == NULL || Cnf_CutCompare(pCutBest, pCut) == 1 )
pCutBest = pCut;
return pCutBest;
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
pCut->NoRefs++;
}
else
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
if ( pCut->FanRefs + pLeaf->nRefs > 15 )
pCut->FanRefs = 15;
else
pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
pCut->NoRefs++;
}
else
{
if ( pCut->FanRefs + pLeaf->nRefs > 15 )
pCut->FanRefs = 15;
else
pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Performs one round of "area recovery" using exact local area.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_ManMapForCnf( Cnf_Man_t * p )
{
Dar_Obj_t * pObj;
Dar_Cut_t * pCut, * pCutBest;
int i, k;
// visit the nodes in the topological order and update their best cuts
Dar_ManForEachNode( p->pManAig, pObj, i )
{
// find the old best cut
pCutBest = Dar_ObjBestCut(pObj);
Dar_ObjClearBestCut(pCutBest);
// if the node is used, dereference its cut
if ( pObj->nRefs )
Dar_CutDeref( p->pManAig, pCutBest );
// evaluate the cuts of this node
Dar_ObjForEachCut( pObj, pCut, k )
// Cnf_CutAssignAreaFlow( p, pCut );
pCut->Area = (float)Cnf_CutArea( p->pManAig, pCut );
// find the new best cut
pCutBest = Cnf_ObjFindBestCut(pObj);
Dar_ObjSetBestCut( pCutBest );
// if the node is used, reference its cut
if ( pObj->nRefs )
Dar_CutRef( p->pManAig, pCutBest );
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

225
src/aig/cnf/cnfPost.c Normal file
View File

@ -0,0 +1,225 @@
/**CFile****************************************************************
FileName [cnfPost.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfPost.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_ManPostprocess_old( Cnf_Man_t * p )
{
extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
int nNew, Gain, nGain = 0, nVars = 0;
Dar_Obj_t * pObj, * pFan;
Dar_Cut_t * pCutBest, * pCut;
int i, k;//, a, b, Counter;
Dar_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
if ( pObj->nRefs == 0 )
continue;
pCutBest = Dar_ObjBestCut(pObj);
Dar_CutForEachLeaf( p->pManAig, pCutBest, pFan, k )
{
if ( !Dar_ObjIsNode(pFan) )
continue;
assert( pFan->nRefs != 0 );
if ( pFan->nRefs != 1 )
continue;
pCut = Dar_ObjBestCut(pFan);
/*
// find how many common variable they have
Counter = 0;
for ( a = 0; a < (int)pCut->nLeaves; a++ )
{
for ( b = 0; b < (int)pCutBest->nLeaves; b++ )
if ( pCut->pLeaves[a] == pCutBest->pLeaves[b] )
break;
if ( b == (int)pCutBest->nLeaves )
continue;
Counter++;
}
printf( "%d ", Counter );
*/
// find the new truth table after collapsing these two cuts
nNew = Dar_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
Gain = pCutBest->Cost+pCut->Cost-nNew;
if ( Gain > 0 )
{
nGain += Gain;
nVars++;
}
}
}
printf( "Total gain = %d. Vars = %d.\n", nGain, nVars );
}
/**Function*************************************************************
Synopsis [Transfers cuts of the mapped nodes into internal representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_ManTransferCuts( Cnf_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
Dar_MmFlexRestart( p->pMemCuts );
Dar_ManForEachObj( p->pManAig, pObj, i )
{
if ( Dar_ObjIsNode(pObj) && pObj->nRefs > 0 )
pObj->pData = Cnf_CutCreate( p, pObj );
else
pObj->pData = NULL;
}
}
/**Function*************************************************************
Synopsis [Transfers cuts of the mapped nodes into internal representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_ManFreeCuts( Cnf_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
Dar_ManForEachObj( p->pManAig, pObj, i )
if ( pObj->pData )
{
Cnf_CutFree( pObj->pData );
pObj->pData = NULL;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_ManPostprocess( Cnf_Man_t * p )
{
Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
Dar_Obj_t * pObj, * pFan;
int Order[16], Costs[16];
int i, k, fChanges;
Dar_ManForEachNode( p->pManAig, pObj, i )
{
if ( pObj->nRefs == 0 )
continue;
pCut = Cnf_ObjBestCut(pObj);
// sort fanins according to their size
Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
{
Order[k] = k;
Costs[k] = Dar_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
}
// sort the cuts by Weight
do {
int Temp;
fChanges = 0;
for ( k = 0; k < pCut->nFanins - 1; k++ )
{
if ( Costs[Order[k]] <= Costs[Order[k+1]] )
continue;
Temp = Order[k];
Order[k] = Order[k+1];
Order[k+1] = Temp;
fChanges = 1;
}
} while ( fChanges );
// Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Dar_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
{
if ( !Dar_ObjIsNode(pFan) )
continue;
assert( pFan->nRefs != 0 );
if ( pFan->nRefs != 1 )
continue;
pCutFan = Cnf_ObjBestCut(pFan);
// try composing these two cuts
// Cnf_CutPrint( pCut );
pCutRes = Cnf_CutCompose( p, pCut, pCutFan, pFan->Id );
// Cnf_CutPrint( pCut );
// printf( "\n" );
// check if the cost if reduced
if ( pCutRes == NULL || pCutRes->Cost == 127 || pCutRes->Cost > pCut->Cost + pCutFan->Cost )
{
if ( pCutRes )
Cnf_CutFree( pCutRes );
continue;
}
// update the cut
Cnf_ObjSetBestCut( pObj, pCutRes );
Cnf_ObjSetBestCut( pFan, NULL );
Cnf_CutUpdateRefs( p, pCut, pCutFan, pCutRes );
assert( pFan->nRefs == 0 );
Cnf_CutFree( pCut );
Cnf_CutFree( pCutFan );
break;
}
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

157
src/aig/cnf/cnfUtil.c Normal file
View File

@ -0,0 +1,157 @@
/**CFile****************************************************************
FileName [cnfUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
Dar_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
return 0;
assert( Dar_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
Vec_PtrPush( vMapped, pObj );
// visit the transitive fanin of the selected cut
pCutBest = Dar_ObjBestCut(pObj);
aArea = pCutBest->Cost;
Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
return aArea;
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
Dar_Obj_t * pObj;
int i;
// clean all references
Dar_ManForEachObj( p->pManAig, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Dar_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
Dar_Obj_t * pLeaf;
Cnf_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
return 0;
assert( Dar_ObjIsAnd(pObj) );
assert( pObj->pData != NULL );
// visit the transitive fanin of the selected cut
pCutBest = pObj->pData;
assert( pCutBest->Cost < 127 );
aArea = pCutBest->Cost;
Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped );
// collect the node first to derive pre-order
if ( vMapped )
Vec_PtrPush( vMapped, pObj );
return aArea;
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
Dar_Obj_t * pObj;
int i;
// clean all references
Dar_ManForEachObj( p->pManAig, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Dar_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Cnf_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

337
src/aig/cnf/cnfWrite.c Normal file
View File

@ -0,0 +1,337 @@
/**CFile****************************************************************
FileName [cnfWrite.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the cover into the array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
{
int Lits[4], Cube, iCube, i, b;
Vec_IntClear( vCover );
for ( i = 0; i < nCubes; i++ )
{
Cube = pSop[i];
for ( b = 0; b < 4; b++ )
{
if ( Cube % 3 == 0 )
Lits[b] = 1;
else if ( Cube % 3 == 1 )
Lits[b] = 2;
else
Lits[b] = 0;
Cube = Cube / 3;
}
iCube = 0;
for ( b = 0; b < 4; b++ )
iCube = (iCube << 2) | Lits[b];
Vec_IntPush( vCover, iCube );
}
}
/**Function*************************************************************
Synopsis [Returns the number of literals in the SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_SopCountLiterals( char * pSop, int nCubes )
{
int nLits = 0, Cube, i, b;
for ( i = 0; i < nCubes; i++ )
{
Cube = pSop[i];
for ( b = 0; b < 4; b++ )
{
if ( Cube % 3 != 2 )
nLits++;
Cube = Cube / 3;
}
}
return nLits;
}
/**Function*************************************************************
Synopsis [Returns the number of literals in the SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
{
int nLits = 0, Cube, i, b;
Vec_IntForEachEntry( vIsop, Cube, i )
{
for ( b = 0; b < nVars; b++ )
{
if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
nLits++;
Cube >>= 2;
}
}
return nLits;
}
/**Function*************************************************************
Synopsis [Writes the cube and returns the number of literals in it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
{
int nLits = 4, b;
for ( b = 0; b < 4; b++ )
{
if ( Cube % 3 == 0 )
*pLiterals++ = 2 * pVars[b] + !fCompl;
else if ( Cube % 3 == 1 )
*pLiterals++ = 2 * pVars[b] + fCompl;
else
nLits--;
Cube = Cube / 3;
}
return nLits;
}
/**Function*************************************************************
Synopsis [Writes the cube and returns the number of literals in it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals )
{
int nLits = nVars, b;
for ( b = 0; b < nVars; b++ )
{
if ( (Cube & 3) == 1 )
*pLiterals++ = 2 * pVars[b] + !fCompl;
else if ( (Cube & 3) == 2 )
*pLiterals++ = 2 * pVars[b] + fCompl;
else
nLits--;
Cube >>= 2;
}
return nLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
Dar_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Cnf_Cut_t * pCut;
int OutVar, pVars[32], * pLits, ** pClas;
unsigned uTruth;
int i, k, nLiterals, nClauses, nCubes, Cube, Number;
// count the number of literals and clauses
nLiterals = 1 + Dar_ManPoNum( p->pManAig );
nClauses = 1 + Dar_ManPoNum( p->pManAig );
Vec_PtrForEachEntry( vMapped, pObj, i )
{
assert( Dar_ObjIsNode(pObj) );
pCut = Cnf_ObjBestCut( pObj );
// positive polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
assert( p->pSopSizes[uTruth] >= 0 );
nClauses += p->pSopSizes[uTruth];
}
else
{
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
nClauses += Vec_IntSize(pCut->vIsop[1]);
}
// negative polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
assert( p->pSopSizes[uTruth] >= 0 );
nClauses += p->pSopSizes[uTruth];
}
else
{
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
nClauses += Vec_IntSize(pCut->vIsop[0]);
}
//printf( "%d ", nClauses-(1 + Dar_ManPoNum( p->pManAig )) );
}
//printf( "\n" );
// allocate CNF
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// set variable numbers
Number = 0;
pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p->pManAig)) );
Vec_PtrForEachEntry( vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
Dar_ManForEachPi( p->pManAig, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Dar_ManConst1(p->pManAig)->Id] = Number++;
pCnf->nVars = Number;
// assign the clauses
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Vec_PtrForEachEntry( vMapped, pObj, i )
{
pCut = Cnf_ObjBestCut( pObj );
// save variables of this cut
OutVar = pCnf->pVarNums[ pObj->Id ];
for ( k = 0; k < (int)pCut->nFanins; k++ )
{
pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
assert( pVars[k] <= Dar_ManObjIdMax(p->pManAig) );
}
// positive polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
nCubes = p->pSopSizes[uTruth];
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
}
}
else
{
Vec_IntForEachEntry( pCut->vIsop[1], Cube, k )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits );
}
}
// negative polarity of the cut
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
nCubes = p->pSopSizes[uTruth];
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
}
}
else
{
Vec_IntForEachEntry( pCut->vIsop[0], Cube, k )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits );
}
}
//printf( "%d ", pClas-pCnf->pClauses );
}
// write the constant literal
OutVar = pCnf->pVarNums[ Dar_ManConst1(p->pManAig)->Id ];
assert( OutVar <= Dar_ManObjIdMax(p->pManAig) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
// write the output literals
Dar_ManForEachPo( p->pManAig, pObj, i )
{
OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Dar_ObjFaninC0(pObj);
}
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
return pCnf;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

48
src/aig/cnf/cnf_.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [cnf_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnf_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

8
src/aig/cnf/module.make Normal file
View File

@ -0,0 +1,8 @@
SRC += src/aig/cnf/cnfCore.c \
src/aig/cnf/cnfCut.c \
src/aig/cnf/cnfData.c \
src/aig/cnf/cnfMan.c \
src/aig/cnf/cnfMap.c \
src/aig/cnf/cnfPost.c \
src/aig/cnf/cnfUtil.c \
src/aig/cnf/cnfWrite.c

View File

@ -84,10 +84,11 @@ struct Dar_Cut_t_ // 8 words
{
unsigned uSign;
unsigned uTruth : 16; // the truth table of the cut function
unsigned Cost : 6; // the cost of the cut in terms of CNF clauses
unsigned Cost : 5; // the cost of the cut in terms of CNF clauses
unsigned FanRefs : 4; // the average number of fanin references
unsigned NoRefs : 3; // the average number of fanin references
unsigned nLeaves : 3; // the number of leaves
unsigned fBest : 1; // marks the best cut
int pLeaves[4]; // the array of leaves
// unsigned char pIndices[4];
float Area; // the area flow or exact area of the cut
@ -139,6 +140,7 @@ struct Dar_Man_t_
int nNodesInit; // the original number of nodes
Vec_Ptr_t * vLeavesBest; // the best set of leaves
int OutBest; // the best output (in the library)
int OutNumBest; // the best number of the output
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
int ClassBest; // the equivalence class of the best replacement
@ -146,6 +148,7 @@ struct Dar_Man_t_
int ClassTimes[222];// the runtimes for each class
int ClassGains[222];// the gains for each class
int ClassSubgs[222];// the graphs for each class
int nCutMemUsed; // memory used for cuts
// various data members
Dar_MmFixed_t * pMemObjs; // memory manager for objects
Dar_MmFlex_t * pMemCuts; // memory manager for cuts
@ -155,9 +158,7 @@ struct Dar_Man_t_
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
// CNF mapping
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
void * pManCnf; // CNF conversion manager
// rewriting statistics
int nCutsBad;
int nCutsGood;
@ -274,8 +275,16 @@ static inline int Dar_ObjFanoutC( Dar_Obj_t * pObj, Dar_Obj_t * pFanout
if ( Dar_ObjFanin1(pFanout) == pObj ) return Dar_ObjFaninC1(pObj);
assert(0); return -1;
}
static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj ) { return (Dar_Cut_t *)pObj->pNext; }
static inline void Dar_ObjSetBestCut( Dar_Obj_t * pObj, Dar_Cut_t * pCut ) { pObj->pNext = (Dar_Obj_t *)pCut; }
static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut; int i;
for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ )
if ( pCut->fBest )
return pCut;
return NULL;
}
static inline void Dar_ObjSetBestCut( Dar_Cut_t * pCut ) { assert( !pCut->fBest ); pCut->fBest = 1; }
static inline void Dar_ObjClearBestCut( Dar_Cut_t * pCut ) { assert( pCut->fBest ); pCut->fBest = 0; }
// create the ghost of the new node
static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type )
@ -333,6 +342,9 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
// iterator over all objects, including those currently not used
#define Dar_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterator over all nodes
#define Dar_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Dar_ObjIsNode(pObj) ) {} else
// iterator over all cuts of the node
#define Dar_ObjForEachCut( pObj, pCut, i ) \
for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ ) if ( i==0 ) {} else
@ -383,6 +395,7 @@ extern void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t
extern Dar_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ==========================================================*/
extern Dar_Man_t * Dar_ManStart();
extern Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p );
extern Dar_Man_t * Dar_ManDup( Dar_Man_t * p );
extern void Dar_ManStop( Dar_Man_t * p );
extern int Dar_ManCleanup( Dar_Man_t * p );

View File

@ -1,679 +0,0 @@
/**CFile****************************************************************
FileName [darCnf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darCnf.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Dereferences the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dar_CurDeref2( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
pLeaf->nRefs--;
}
}
/**Function*************************************************************
Synopsis [References the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dar_CurRef2( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
pLeaf->nRefs++;
}
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
}
}
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i, Area = pCut->Cost;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs >= 0 );
if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
}
return Area;
}
/**Function*************************************************************
Synopsis [Computes exact area of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
{
int Area = Dar_CutRef( p, pCut );
Dar_CutDeref( p, pCut );
return Area;
}
/**Function*************************************************************
Synopsis [Returns 1 if the second cut is better.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dar_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
{
if ( pC0->Area < pC1->Area - 0.0001 )
return -1;
if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better
return 1;
/*
if ( pC0->NoRefs < pC1->NoRefs )
return -1;
if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better
return 1;
*/
// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves )
// return -1;
// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves )
return 1; // larger average fanin ref-counter is better
// return 0;
}
/**Function*************************************************************
Synopsis [Returns the cut with the smallest area flow.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cut_t * Dar_ObjFindBestCut( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut, * pCutBest;
int i;
pCutBest = NULL;
Dar_ObjForEachCut( pObj, pCut, i )
if ( pCutBest == NULL || Dar_CutCompare(pCutBest, pCut) == 1 )
pCutBest = pCut;
return pCutBest;
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
// pCut->NoRefs++;
}
else
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
// if ( pCut->FanRefs + pLeaf->nRefs > 15 )
// pCut->FanRefs = 15;
// else
// pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
pCut->NoRefs++;
}
else
{
if ( pCut->FanRefs + pLeaf->nRefs > 15 )
pCut->FanRefs = 15;
else
pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManScanMapping_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
Dar_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
return 0;
assert( Dar_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
{
// printf( "%d ", Dar_ObjBestCut(pObj)->Cost );
Vec_PtrPush( vMapped, pObj );
}
// visit the transitive fanin of the selected cut
pCutBest = Dar_ObjBestCut(pObj);
aArea = pCutBest->Cost;
Dar_CutForEachLeaf( p, pCutBest, pLeaf, i )
aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
return aArea;
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order in array
p->vMapping.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Dar_ManScanMapping( Dar_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
Dar_Obj_t * pObj;
int i;
// clean all references
Dar_ManForEachObj( p, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Dar_ManForEachPo( p, pObj, i )
p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
printf( "Variables = %d. Clauses = %6d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManMapForCnf( Dar_Man_t * p )
{
Dar_Obj_t * pObj;
Dar_Cut_t * pCut;
int i, k;
// visit the nodes in the topological order and update their best cuts
Dar_ManForEachObj( p, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
// if ( pObj->nRefs )
// continue;
// if the node is used, dereference its cut
if ( pObj->nRefs )
Dar_CutDeref( p, Dar_ObjBestCut(pObj) );
// evaluate the cuts of this node
Dar_ObjForEachCut( pObj, pCut, k )
// Dar_CutAssignArea( p, pCut );
// Dar_CutAssignAreaFlow( p, pCut );
pCut->Area = (float)Dar_CutArea( p, pCut );
// find a new good cut
Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
// if the node is used, reference its cut
if ( pObj->nRefs )
Dar_CutRef( p, Dar_ObjBestCut(pObj) );
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns the number of literals in the SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_SopCountLiterals( char * pSop, int nCubes )
{
int nLits = 0, Cube, i, b;
for ( i = 0; i < nCubes; i++ )
{
Cube = pSop[i];
for ( b = 3; b >= 0; b-- )
{
if ( Cube % 3 != 2 )
nLits++;
Cube = Cube / 3;
}
}
return nLits;
}
/**Function*************************************************************
Synopsis [Writes the cube and returns the number of literals in it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
{
int nLits = 4, b;
for ( b = 3; b >= 0; b-- )
{
if ( Cube % 3 == 0 )
*pLiterals++ = 2 * pVars[b] + 1 ^ fCompl;
else if ( Cube % 3 == 1 )
*pLiterals++ = 2 * pVars[b] + fCompl;
else
nLits--;
Cube = Cube / 3;
}
return nLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cnf_t * Dar_ManWriteCnf( Dar_Man_t * p, Vec_Ptr_t * vMapped )
{
Dar_Cnf_t * pCnf;
Dar_Obj_t * pObj;
Dar_Cut_t * pCut;
int OutVar, pVars[4], * pLits, ** pClas;
unsigned uTruth;
int i, k, nLiterals, nClauses, nCubes, Number;
// count the number of literals and clauses
nLiterals = 1 + Dar_ManPoNum( p );
nClauses = 1 + Dar_ManPoNum( p );
Vec_PtrForEachEntry( vMapped, pObj, i )
{
assert( Dar_ObjIsNode(pObj) );
pCut = Dar_ObjBestCut( pObj );
// positive polarity of the cut
uTruth = pCut->uTruth;
nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
nClauses += p->pSopSizes[uTruth];
// negative polarity of the cut
uTruth = 0xFFFF & ~pCut->uTruth;
nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
nClauses += p->pSopSizes[uTruth];
}
// allocate CNF
pCnf = ALLOC( Dar_Cnf_t, 1 );
memset( pCnf, 0, sizeof(Dar_Cnf_t) );
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p) );
// set variable numbers
Number = 0;
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p)) );
Vec_PtrForEachEntry( vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
Dar_ManForEachPi( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Dar_ManConst1(p)->Id] = Number++;
// assign the clauses
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Vec_PtrForEachEntry( vMapped, pObj, i )
{
pCut = Dar_ObjBestCut( pObj );
// write variables of this cut
OutVar = pCnf->pVarNums[ pObj->Id ];
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
pVars[k] = pCnf->pVarNums[ pCut->pLeaves[k] ];
assert( pVars[k] <= Dar_ManObjIdMax(p) );
}
// positive polarity of the cut
uTruth = pCut->uTruth;
nCubes = p->pSopSizes[uTruth];
// write the cubes
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar] + 1;
pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
}
// negative polarity of the cut
uTruth = 0xFFFF & ~pCut->uTruth;
nCubes = p->pSopSizes[uTruth];
// write the cubes
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar];
pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
}
}
// write the output literals
Dar_ManForEachPo( p, pObj, i )
{
OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar] + Dar_ObjFaninC0(pObj);
}
// write the constant literal
OutVar = pCnf->pVarNums[ Dar_ManConst1(p)->Id ];
assert( OutVar <= Dar_ManObjIdMax(p) );
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar];
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CnfFree( Dar_Cnf_t * pCnf )
{
if ( pCnf == NULL )
return;
free( pCnf->pClauses[0] );
free( pCnf->pClauses );
free( pCnf->pVarNums );
free( pCnf );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManExploreMapping( Dar_Man_t * p )
{
extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
int nNew, Gain, nGain = 0, nVars = 0;
Dar_Obj_t * pObj, * pLeaf;
Dar_Cut_t * pCutBest, * pCut;
int i, k, a, b, Counter;
Dar_ManForEachObj( p, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
if ( pObj->nRefs == 0 )
continue;
pCutBest = Dar_ObjBestCut(pObj);
Dar_CutForEachLeaf( p, pCutBest, pLeaf, k )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
assert( pLeaf->nRefs != 0 );
if ( pLeaf->nRefs != 1 )
continue;
pCut = Dar_ObjBestCut(pLeaf);
/*
// find how many common variable they have
Counter = 0;
for ( a = 0; a < (int)pCut->nLeaves; a++ )
{
for ( b = 0; b < (int)pCutBest->nLeaves; b++ )
if ( pCut->pLeaves[a] == pCutBest->pLeaves[b] )
break;
if ( b == (int)pCutBest->nLeaves )
continue;
Counter++;
}
printf( "%d ", Counter );
*/
// find the new truth table after collapsing these two cuts
nNew = Dar_ManLargeCutEval( p, pObj, pCutBest, pCut, pLeaf->Id );
// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
Gain = pCutBest->Cost+pCut->Cost-nNew;
if ( Gain > 0 )
{
nGain += Gain;
nVars++;
}
}
}
printf( "Total gain = %d. Vars = %d.\n", nGain, nVars );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p )
{
Dar_Cnf_t * pCnf = NULL;
Vec_Ptr_t * vMapped;
int i, nIters = 2;
int clk;
// derive SOPs for all 4-variable functions
clk = clock();
Dar_LibReadMsops( &p->pSopSizes, &p->pSops );
PRT( "setup", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts
// (used pObj->pNext for storing the best cut of the node!)
clk = clock();
Dar_ManComputeCuts( p );
PRT( "cuts ", clock() - clk );
// iteratively improve area flow
for ( i = 0; i < nIters; i++ )
{
clk = clock();
Dar_ManScanMapping( p, 0 );
Dar_ManMapForCnf( p );
PRT( "iter ", clock() - clk );
}
// write the file
vMapped = Dar_ManScanMapping( p, 1 );
clk = clock();
Dar_ManExploreMapping( p );
PRT( "exten", clock() - clk );
// pCnf = Dar_ManWriteCnf( p, vMapped );
Vec_PtrFree( vMapped );
// clean up
Dar_ManCutsFree( p );
return pCnf;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -106,11 +106,15 @@ p->timeCuts += clock() - clk;
// count gains of this class
p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
// if ( p->ClassBest == 29 )
// printf( "%d ", p->OutNumBest );
}
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
p->nCutMemUsed = Dar_MmFlexReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
// put the nodes into the DFS order and reassign their IDs
// Dar_NtkReassignIds( p );
@ -161,7 +165,6 @@ int Dar_ManComputeCuts( Dar_Man_t * p )
Dar_ManNodeNum(p), nCutsTotal, nCutsMax, (float)nCutsTotal/Dar_ManNodeNum(p),
p->nCutsFiltered, p->nCutsFiltered+nCutsTotal+Dar_ManNodeNum(p)+Dar_ManPiNum(p) );
PRT( "Time", clock() - clkStart );
// free the cuts
// Dar_ManCutsFree( p );
return 1;

View File

@ -65,7 +65,7 @@ static inline int Dar_CutCheckDominance( Dar_Cut_t * pDom, Dar_Cut_t * pCut )
SeeAlso []
***********************************************************************/
int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
static inline int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Cut_t * pTemp;
int i, k;
@ -213,7 +213,7 @@ static inline int Dar_CutMergeOrdered( Dar_Cut_t * pC, Dar_Cut_t * pC0, Dar_Cut_
SeeAlso []
***********************************************************************/
int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
static inline int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
{
// merge the nodes
if ( pCut0->nLeaves <= pCut1->nLeaves )
@ -347,7 +347,7 @@ static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned
SeeAlso []
***********************************************************************/
unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
static inline unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
unsigned uTruth0 = fCompl0 ? ~pCut0->uTruth : pCut0->uTruth;
unsigned uTruth1 = fCompl1 ? ~pCut1->uTruth : pCut1->uTruth;
@ -367,7 +367,7 @@ unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, i
SeeAlso []
***********************************************************************/
int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
{
unsigned uMasks[4][2] = {
{ 0x5555, 0xAAAA },
@ -420,7 +420,7 @@ void Dar_ObjSetupTrivial( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut;
pCut = pObj->pData;
pCut->Cost = 0;
memset( pCut, 0, sizeof(Dar_Cut_t) );
pCut->nLeaves = 1;
pCut->pLeaves[0] = pObj->Id;
// pCut->pIndices[0] = 0;
@ -464,10 +464,7 @@ void Dar_ManSetupPis( Dar_Man_t * p )
***********************************************************************/
void Dar_ManCutsFree( Dar_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
Dar_ManForEachObj( p, pObj, i )
pObj->pData = NULL;
// Dar_ManCleanData( p );
Dar_MmFlexStop( p->pMemCuts, 0 );
p->pMemCuts = NULL;
}
@ -519,11 +516,11 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
continue;
}
// CNF mapping: assign the cut cost if needed
if ( p->pSopSizes )
// CNF mapping: assign the cut cost
if ( p->pManCnf )
{
pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
Dar_CutAssignAreaFlow( p, pCut );
extern void Cnf_CutAssignAreaFlow( void * pManCnf, Dar_Cut_t * pCut );
Cnf_CutAssignAreaFlow( p->pManCnf, pCut );
}
// increment the number of cuts
@ -538,9 +535,12 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
for ( i = 0; i < p->nCutsUsed; i++ )
*++pCut = *(p->pBaseCuts[i]);
// CNF mapping: assign the best cut if needed
if ( p->pSopSizes )
Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
// CNF mapping: assign the best cut
if ( p->pManCnf )
{
extern Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj );
Dar_ObjSetBestCut( Cnf_ObjFindBestCut(pObj) );
}
return pObj->pData;
}

View File

@ -273,6 +273,7 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts )
for ( k = 0; k < p->nSubgr[i]; k++ )
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
nNodesTotal += p->nNodes[i];
//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
}
assert( nNodesTotal == p->pNodesTotal );
// prepare the number of the PI nodes
@ -604,6 +605,8 @@ void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
int i, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
if ( pCut->nLeaves != 4 )
return;
// if ( s_DarLib->nSubgr[ s_DarLib->pMap[pCut->uTruth] ] > 100 )
// return;
clk = clock();
/*
for ( k = 0; k < 4; k++ )
@ -643,10 +646,11 @@ void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
Vec_PtrClear( p->vLeavesBest );
for ( k = 0; k < 4; k++ )
Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
p->OutBest = s_DarLib->pSubgr[Class][i];
p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
p->GainBest = nNodesGained;
p->ClassBest = Class;
p->OutBest = s_DarLib->pSubgr[Class][i];
p->OutNumBest = i;
p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
p->GainBest = nNodesGained;
p->ClassBest = Class;
}
clk = clock() - clk;
p->ClassTimes[Class] += clk;

View File

@ -77,6 +77,68 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p )
{
Dar_Man_t * pNew;
Dar_Obj_t * pObj;
int i;
// create the new manager
pNew = Dar_ManStart();
// create the PIs
Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
Dar_ManForEachPi( p, pObj, i )
pObj->pData = Dar_ObjCreatePi(pNew);
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
{
Dar_Man_t * pNew;
Dar_Obj_t * pObj;
int i;
// create the new manager
pNew = Dar_ManStart();
// create the PIs
Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
Dar_ManForEachPi( p, pObj, i )
pObj->pData = Dar_ObjCreatePi(pNew);
// duplicate internal nodes
Dar_ManForEachObj( p, pObj, i )
if ( Dar_ObjIsBuf(pObj) )
pObj->pData = Dar_ObjChild0Copy(pObj);
else if ( Dar_ObjIsNode(pObj) )
pObj->pData = Dar_And( pNew, Dar_ObjChild0Copy(pObj), Dar_ObjChild1Copy(pObj) );
// add the POs
Dar_ManForEachPo( p, pObj, i )
Dar_ObjCreatePo( pNew, Dar_ObjChild0Copy(pObj) );
// check the resulting network
if ( !Dar_ManCheck(pNew) )
printf( "Dar_ManDup(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Stops the AIG manager.]
@ -107,13 +169,6 @@ void Dar_ManStop( Dar_Man_t * p )
if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
free( p->pTable );
// free CNF mapping data
if ( p->pSopSizes )
{
free( p->pSopSizes );
free( p->pSops[1] );
free( p->pSops );
}
free( p );
}
@ -185,7 +240,8 @@ void Dar_ManPrintStats( Dar_Man_t * p )
void Dar_ManPrintRuntime( Dar_Man_t * p )
{
int i, Gain;
printf( "Good cuts = %d. Bad cuts = %d.\n", p->nCutsGood, p->nCutsBad );
printf( "Good cuts = %d. Bad cuts = %d. Cut mem = %d Mb\n",
p->nCutsGood, p->nCutsBad, p->nCutMemUsed );
PRT( "Cuts ", p->timeCuts );
PRT( "Eval ", p->timeEval );
PRT( "Other ", p->timeOther );

196
src/aig/fra/fra.h Normal file
View File

@ -0,0 +1,196 @@
/**CFile****************************************************************
FileName [fra.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [[New FRAIG package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __FRA_H__
#define __FRA_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "dar.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Man_t_ Fra_Man_t;
// FRAIG parameters
struct Fra_Par_t_
{
int nSimWords; // the number of words in the simulation info
double dSimSatur; // the ratio of refined classes when saturation is reached
int fPatScores; // enables simulation pattern scoring
int MaxScore; // max score after which resimulation is used
double dActConeRatio; // the ratio of cone to be bumped
double dActConeBumpMax; // the largest bump in activity
int fSpeculate; // use speculative reduction
int fProve; // prove the miter outputs
int fVerbose; // verbose output
int fDoSparse; // skip sparse functions
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
};
// FRAIG manager
struct Fra_Man_t_
{
// high-level data
Fra_Par_t * pPars; // parameters governing fraiging
// AIG managers
Dar_Man_t * pManAig; // the starting AIG manager
Dar_Man_t * pManFraig; // the final AIG manager
// simulation info
unsigned * pSimWords; // memory for simulation information
int nSimWords; // the number of simulation words
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
int * pPatScores; // the scores of each pattern
// equivalence classes
Vec_Ptr_t * vClasses; // equivalence classes
Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
Dar_Obj_t ** pMemClasses; // memory allocated for equivalence classes
Dar_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
int nPairs; // the number of pairs of nodes
// equivalence checking
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
Vec_Ptr_t * vPiVars; // the PIs of the cone used
sint64 nBTLimitGlobal; // resource limit
sint64 nInsLimitGlobal; // resource limit
// various data members
Dar_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
Dar_Obj_t ** pMemRepr; // memory allocated for points to the node representatives
Vec_Ptr_t ** pMemFanins; // the arrays of fanins
int * pMemSatNums; // the array of SAT numbers
int nSizeAlloc; // allocated size of the arrays
// statistics
int nSimRounds;
int nNodesMiter;
int nClassesZero;
int nClassesBeg;
int nClassesEnd;
int nPairsBeg;
int nPairsEnd;
int nSatCalls;
int nSatCallsSat;
int nSatCallsUnsat;
int nSatProof;
int nSatFails;
int nSatFailsReal;
// runtime
int timeSim;
int timeTrav;
int timeSat;
int timeSatUnsat;
int timeSatSat;
int timeSatFail;
int timeRef;
int timeTotal;
int time1;
int time2;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline unsigned * Fra_ObjSim( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
static inline Dar_Obj_t * Fra_ObjFraig( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; }
static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; }
static inline Vec_Ptr_t * Fra_ObjFaninVec( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
static inline int Fra_ObjSatNum( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; }
static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; }
static inline void Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
static inline void Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
static inline void Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== fraAnd.c ========================================================*/
extern void Fra_Sweep( Fra_Man_t * p );
/*=== fraClass.c ========================================================*/
extern void Fra_CreateClasses( Fra_Man_t * p );
extern int Fra_RefineClasses( Fra_Man_t * p );
extern int Fra_RefineClasses1( Fra_Man_t * p );
/*=== fraCnf.c ========================================================*/
extern void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
extern void Fra_ManStop( Fra_Man_t * p );
extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
extern int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
/*=== fraSim.c ========================================================*/
extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
extern int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
extern void Fra_SavePattern( Fra_Man_t * p );
extern void Fra_Simulate( Fra_Man_t * p );
extern void Fra_Resimulate( Fra_Man_t * p );
extern int Fra_CheckOutputSims( Fra_Man_t * p );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

138
src/aig/fra/fraAnd.c Normal file
View File

@ -0,0 +1,138 @@
/**CFile****************************************************************
FileName [fraAnd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fraig FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraAnd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
{
Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
int RetValue;
assert( !Dar_IsComplement(pObjOld) );
assert( Dar_ObjIsNode(pObjOld) );
// get the fraiged fanins
pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
// get the fraiged node
pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
// get representative of this class
pObjOldRepr = Fra_ObjRepr(pObjOld);
if ( pObjOldRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
{
assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
assert( pObjFraig != Dar_Regular(pFanin0Fraig) );
assert( pObjFraig != Dar_Regular(pFanin1Fraig) );
return pObjFraig;
}
// get the fraiged representative
pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
// if the fraiged nodes are the same, return
if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
return pObjFraig;
assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
// if they are proved different, the c-ex will be in p->pPatWords
RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
pObjOld->fMarkA = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
if ( RetValue == -1 ) // failed
{
if ( !p->pPars->fSpeculate )
return pObjFraig;
// substitute the node
pObjOld->fMarkB = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
// simulate the counter-example and return the Fraig node
Fra_Resimulate( p );
return pObjFraig;
}
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_Sweep( Fra_Man_t * p )
{
Dar_Obj_t * pObj, * pObjNew;
int i, k = 0;
p->nClassesZero = Vec_PtrSize(p->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->vClasses);
// duplicate internal nodes
// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
Dar_ManForEachNode( p->pManAig, pObj, i )
{
// Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
assert( Fra_ObjFraig(pObj) != NULL );
Fra_ObjSetFraig( pObj, pObjNew );
}
// Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = Vec_PtrSize(p->vClasses);
// try to prove the outputs of the miter
p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
// Fra_MiterProve( p );
// add the POs
Dar_ManForEachPo( p->pManAig, pObj, i )
Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
// remove dangling nodes
Dar_ManCleanup( p->pManFraig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

394
src/aig/fra/fraClass.c Normal file
View File

@ -0,0 +1,394 @@
/**CFile****************************************************************
FileName [fraClass.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
/*
The candidate equivalence classes are stored as a vector of pointers
to the array of pointers to the nodes in each class.
The first node of the class is its representative node.
The representative has the smallest topological order among the class nodes.
The classes are ordered according to the topological order of their representatives.
The array of pointers to the class nodes is terminated with a NULL pointer.
To enable dynamic addition of new classes (during class refinement),
each array has at least as many NULLs in the end, as there are nodes in the class.
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_CountPairsClasses( Fra_Man_t * p )
{
Dar_Obj_t ** pClass;
int i, nNodes, nPairs = 0;
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
for ( nNodes = 0; pClass[nNodes]; nNodes++ )
{
if ( nNodes > DAR_INFINITY )
{
printf( "Error in equivalence classes.\n" );
break;
}
}
nPairs += (nNodes - 1) * (nNodes - 2) / 2;
}
return nPairs;
}
/**Function*************************************************************
Synopsis [Computes hash value using simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
{
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 * pSims;
unsigned uHash;
int i;
assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
uHash ^= pSims[i] * s_FPrimes[i];
return uHash;
}
/**Function********************************************************************
Synopsis [Returns the next prime &gt;= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Cudd_PrimeFra( 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 [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_CreateClasses( Fra_Man_t * p )
{
Dar_Obj_t ** pTable;
Dar_Obj_t * pObj;
int i, k, k2, nTableSize, nEntries, iEntry;
// allocate the table
nTableSize = Cudd_PrimeFra( Dar_ManNodeNum(p->pManAig) );
pTable = ALLOC( Dar_Obj_t *, nTableSize );
memset( pTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
// collect nodes into the table
Vec_PtrClear( p->vClasses1 );
Dar_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Dar_ObjIsPi(pObj) && !Dar_ObjIsNode(pObj) )
continue;
// hash the node by its simulation info
iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
// check if the node belongs to the class of constant 1
if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
{
Vec_PtrPush( p->vClasses1, pObj );
continue;
}
// add the node to the table
pObj->pData = pTable[iEntry];
pTable[iEntry] = pObj;
}
// count the total number of nodes in the non-trivial classes
nEntries = 0;
for ( i = 0; i < nTableSize; i++ )
if ( pTable[i] && pTable[i]->pData )
{
k = 0;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
k++;
nEntries += 2*k;
}
// allocate room for classes
p->pMemClasses = ALLOC( Dar_Obj_t *, nEntries + 2*Vec_PtrSize(p->vClasses1) );
p->pMemClassesFree = p->pMemClasses + nEntries;
// copy the entries into storage
Vec_PtrClear( p->vClasses );
nEntries = 0;
for ( i = 0; i < nTableSize; i++ )
if ( pTable[i] && pTable[i]->pData )
{
k = 0;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
k++;
// write entries in the topological order
k2 = k;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
{
k2--;
p->pMemClasses[nEntries+k2] = pObj;
p->pMemClasses[nEntries+k+k2] = NULL;
}
assert( k2 == 0 );
Vec_PtrPush( p->vClasses, p->pMemClasses + nEntries );
nEntries += 2*k;
}
free( pTable );
// now it is time to refine the classes
Fra_RefineClasses( p );
// set the pointer to the manager
Dar_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p->pManAig;
}
/**Function*************************************************************
Synopsis [Refines one class using simulation info.]
Description [Returns the new class if refinement happened.]
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** pClass )
{
Dar_Obj_t * pObj;
int i;
assert( pClass[1] != NULL );
// check if the class is going to be refined
for ( pObj = pClass[1]; pObj; pObj++ )
if ( !Fra_NodeCompareSims(p, pClass[0], pObj) )
break;
if ( pObj == NULL )
return NULL;
// split the class
Vec_PtrClear( p->vClassOld );
Vec_PtrClear( p->vClassNew );
Vec_PtrPush( p->vClassOld, pClass[0] );
for ( pObj = pClass[1]; pObj; pObj++ )
if ( Fra_NodeCompareSims(p, pClass[0], pObj) )
Vec_PtrPush( p->vClassOld, pObj );
else
Vec_PtrPush( p->vClassNew, pObj );
// put the nodes back into the class memory
Vec_PtrForEachEntry( p->vClassOld, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
}
pClass += 2*Vec_PtrSize(p->vClassOld);
// put the new nodes into the class memory
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
}
return pClass;
}
/**Function*************************************************************
Synopsis [Iteratively refines the classes after simulation.]
Description [Returns the number of refinements performed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
{
Dar_Obj_t ** pClass, ** pClass2;
int nRefis;
pClass = Vec_PtrEntryLast( vClasses );
for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
{
// if the original class is trivial, remove it
if ( pClass[1] == NULL )
Vec_PtrPop( vClasses );
// if the new class is trivial, stop
if ( pClass2[1] == NULL )
break;
// othewise, add the class and continue
Vec_PtrPush( vClasses, pClass2 );
pClass = pClass2;
}
return nRefis;
}
/**Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description [Assumes that simulation info is assigned. Returns the
number of classes refined.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_RefineClasses( Fra_Man_t * p )
{
Vec_Ptr_t * vTemp;
Dar_Obj_t ** pClass;
int clk, i, nRefis = 0;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
if ( p->pPars->fProve )
Fra_CheckOutputSims( p );
if ( p->pManFraig->pData )
return 0;
// refine the classes
clk = clock();
Vec_PtrClear( p->vClassesTemp );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
// add the class to the new array
Vec_PtrPush( p->vClassesTemp, pClass );
// refine the class interatively
nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
}
// exchange the class representation
vTemp = p->vClassesTemp;
p->vClassesTemp = p->vClasses;
p->vClasses = vTemp;
p->timeRef += clock() - clk;
return nRefis;
}
/**Function*************************************************************
Synopsis [Refines constant 1 equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_RefineClasses1( Fra_Man_t * p )
{
Dar_Obj_t * pObj, ** pClass;
int i, k;
// collect all the nodes to be refined
Vec_PtrClear( p->vClassNew );
k = 0;
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
{
if ( Fra_NodeHasZeroSim( p, pObj ) )
Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
else
Vec_PtrPush( p->vClassNew, pObj );
}
Vec_PtrShrink( p->vClasses1, k );
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
if ( Vec_PtrSize(p->vClassNew) == 1 )
return 1;
// create a new class composed of these nodes
pClass = p->pMemClassesFree;
p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
}
Vec_PtrPush( p->vClasses, pClass );
// iteratively refine this class
return 1 + Fra_RefineClassLastIter( p, p->vClasses );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

285
src/aig/fra/fraCnf.c Normal file
View File

@ -0,0 +1,285 @@
/**CFile****************************************************************
FileName [fraCnf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
{
Dar_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
assert( !Dar_IsComplement( pNode ) );
assert( Dar_ObjIsMuxType( pNode ) );
// get nodes (I = if, T = then, E = else)
pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the variable numbers
VarF = Fra_ObjSatNum(pNode);
VarI = Fra_ObjSatNum(pNodeI);
VarT = Fra_ObjSatNum(Dar_Regular(pNodeT));
VarE = Fra_ObjSatNum(Dar_Regular(pNodeE));
// get the complementation flags
fCompT = Dar_IsComplement(pNodeT);
fCompE = Dar_IsComplement(pNodeE);
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
if ( VarT == VarE )
{
// assert( fCompT == !fCompE );
return;
}
pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
Dar_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
assert( !Dar_IsComplement(pNode) );
assert( Dar_ObjIsNode( pNode ) );
// create storage for literals
nLits = Vec_PtrSize(vSuper) + 1;
pLits = ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
Vec_PtrForEachEntry( vSuper, pFanin, i )
{
pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin));
pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
Vec_PtrForEachEntry( vSuper, pFanin, i )
pLits[i] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin));
pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
assert( RetValue );
free( pLits );
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) ||
(fUseMuxes && Dar_ObjIsMuxType(pObj)) )
{
Vec_PtrPushUnique( vSuper, pObj );
return;
}
// go through the branches
Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
{
Vec_Ptr_t * vSuper;
assert( !Dar_IsComplement(pObj) );
assert( !Dar_ObjIsPi(pObj) );
vSuper = Vec_PtrAlloc( 4 );
Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
return vSuper;
}
/**Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
assert( !Dar_IsComplement(pObj) );
if ( Fra_ObjSatNum(pObj) )
return;
assert( Fra_ObjSatNum(pObj) == 0 );
assert( Fra_ObjFaninVec(pObj) == NULL );
if ( Dar_ObjIsConst1(pObj) )
return;
//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
Fra_ObjSetSatNum( pObj, p->nSatVars++ );
if ( Dar_ObjIsNode(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
/**Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
{
Vec_Ptr_t * vFrontier, * vFanins;
Dar_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
assert( pOld || pNew );
// quit if CNF is ready
if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
return;
// start the frontier
vFrontier = Vec_PtrAlloc( 100 );
if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
// explore nodes in the frontier
Vec_PtrForEachEntry( vFrontier, pNode, i )
{
// create the supergate
assert( Fra_ObjSatNum(pNode) );
assert( Fra_ObjFaninVec(pNode) == NULL );
if ( fUseMuxes && Dar_ObjIsMuxType(pNode) )
{
vFanins = Vec_PtrAlloc( 4 );
Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) );
Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) );
Vec_PtrForEachEntry( vFanins, pFanin, k )
Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
Fra_AddClausesMux( p, pNode );
}
else
{
vFanins = Fra_CollectSuper( pNode, fUseMuxes );
Vec_PtrForEachEntry( vFanins, pFanin, k )
Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
Fra_AddClausesSuper( p, pNode, vFanins );
}
assert( Vec_PtrSize(vFanins) > 1 );
Fra_ObjSetFaninVec( pNode, vFanins );
}
Vec_PtrFree( vFrontier );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

64
src/aig/fra/fraCore.c Normal file
View File

@ -0,0 +1,64 @@
/**CFile****************************************************************
FileName [fraCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Dar_Man_t * pManAigNew;
int clk;
if ( Dar_ManNodeNum(pManAig) == 0 )
return Dar_ManDup(pManAig);
clk = clock();
assert( Dar_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
Fra_Simulate( p );
Fra_Sweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
Fra_ManStop( p );
return pManAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

188
src/aig/fra/fraMan.c Normal file
View File

@ -0,0 +1,188 @@
/**CFile****************************************************************
FileName [fraMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Starts the FRAIG manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ParamsDefault( Fra_Par_t * pPars )
{
memset( pPars, 0, sizeof(Fra_Par_t) );
pPars->nSimWords = 32; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pPars->dActConeBumpMax = 5.0; // the largest bump of activity
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 100; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
}
/**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Dar_Obj_t * pObj;
int i;
// allocate the fraiging manager
p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars;
p->pManAig = pManAig;
p->pManFraig = Dar_ManStartFrom( pManAig );
assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) );
// allocate simulation info
p->nSimWords = pPars->nSimWords;
p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
// clean simulation info of the constant node
memset( p->pSimWords, 0, p->nSimWords * sizeof(unsigned) );
// allocate storage for sim pattern
p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
p->vClasses = Vec_PtrAlloc( 100 );
// allocate other members
p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
p->pMemFraig = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
p->pMemRepr = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc );
memset( p->pMemSatNums, 0xff, p->nSizeAlloc * sizeof(int) );
// set the pointers to the available fraig nodes
Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
Dar_ManForEachPi( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
// set the pointers to the manager
Dar_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p->pManFraig;
// set random number generator
srand( 0xABCABC );
return p;
}
/**Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManStop( Fra_Man_t * p )
{
int i;
for ( i = 0; i < p->nSizeAlloc; i++ )
if ( p->pMemFanins[i] )
Vec_PtrFree( p->pMemFanins[i] );
if ( p->pPars->fVerbose )
Fra_ManPrint( p );
if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
if ( p->vClasses ) Vec_PtrFree( p->vClasses );
if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
FREE( p->pMemSatNums );
FREE( p->pMemFanins );
FREE( p->pMemRepr );
FREE( p->pMemFraig );
FREE( p->pMemClasses );
FREE( p->pPatScores );
FREE( p->pPatWords );
FREE( p->pSimWords );
free( p );
}
/**Function*************************************************************
Synopsis [Prints stats for the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManPrint( Fra_Man_t * p )
{
double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG traversal ", p->timeTrav );
PRT( "SAT solving ", p->timeSat );
PRT( " Unsat ", p->timeSatUnsat );
PRT( " Sat ", p->timeSatSat );
PRT( " Fail ", p->timeSatFail );
PRT( "Class refining ", p->timeRef );
PRT( "TOTAL RUNTIME ", p->timeTotal );
if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

328
src/aig/fra/fraSat.c Normal file
View File

@ -0,0 +1,328 @@
/**CFile****************************************************************
FileName [fraSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
{
int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
// make sure the nodes are not complemented
assert( !Dar_IsComplement(pNew) );
assert( !Dar_IsComplement(pOld) );
assert( pNew != pOld );
// if at least one of the nodes is a failed node, perform adjustments:
// if the backtrack limit is small, simply skip this node
// if the backtrack limit is > 10, take the quare root of the limit
nBTLimit = p->pPars->nBTLimitNode;
/*
if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
{
p->nSatFails++;
// fail immediately
// return -1;
if ( nBTLimit <= 10 )
return -1;
nBTLimit = (int)pow(nBTLimit, 0.7);
}
*/
p->nSatCalls++;
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
}
// if the nodes do not have SAT variables, allocate them
Fra_NodeAddToSolver( p, pOld, pNew );
// prepare variable activity
Fra_SetActivityFactors( p, pOld, pNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
Fra_SavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
// if ( pOld != p->pManFraig->pConst1 )
// pOld->fFailTfo = 1;
// pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
// if the old node was constant 0, we already know the answer
if ( pOld == p->pManFraig->pConst1 )
{
p->nSatProof++;
return 1;
}
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
clk = clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
Fra_SavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
// pOld->fFailTfo = 1;
// pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
/*
// check BDD proof
{
int RetVal;
PRT( "Sat", clock() - clk2 );
clk2 = clock();
RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
// printf( "%d ", RetVal );
assert( RetVal );
PRT( "Bdd", clock() - clk2 );
printf( "\n" );
}
*/
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Runs equivalence test for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew )
{
int pLits[2], RetValue1, RetValue, clk;
// make sure the nodes are not complemented
assert( !Dar_IsComplement(pNew) );
assert( pNew != p->pManFraig->pConst1 );
p->nSatCalls++;
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
}
// if the nodes do not have SAT variables, allocate them
Fra_NodeAddToSolver( p, NULL, pNew );
// prepare variable activity
Fra_SetActivityFactors( p, NULL, pNew );
// solve under assumptions
clk = clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
(sint64)p->pPars->nBTLimitMiter, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
if ( p->pPatWords )
Fra_SavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
// pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax )
{
Vec_Ptr_t * vFanins;
Dar_Obj_t * pFanin;
int i, Counter = 0;
assert( !Dar_IsComplement(pObj) );
assert( Fra_ObjSatNum(pObj) );
// skip visited variables
if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) )
return 0;
Dar_ObjSetTravIdCurrent(p->pManFraig, pObj);
// add the PI to the list
if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) )
return 0;
// set the factor of this variable
// (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
// explore the fanins
vFanins = Fra_ObjFaninVec( pObj );
Vec_PtrForEachEntry( vFanins, pFanin, i )
Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax );
return 1 + Counter;
}
/**Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
{
int clk, LevelMin, LevelMax;
assert( pOld || pNew );
clk = clock();
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
Dar_ManIncrementTravId( p->pManFraig );
// determine the min and max level to visit
assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
// traverse
if ( pOld && !Dar_ObjIsConst1(pOld) )
Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
if ( pNew && !Dar_ObjIsConst1(pNew) )
Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Fra_PrintActivity( p );
p->timeTrav += clock() - clk;
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

599
src/aig/fra/fraSim.c Normal file
View File

@ -0,0 +1,599 @@
/**CFile****************************************************************
FileName [fraSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
{
unsigned * pSims;
int i;
assert( Dar_ObjIsPi(pObj) );
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = Fra_ObjRandomSim();
}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
{
unsigned * pSims;
int i;
assert( Dar_ObjIsPi(pObj) );
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
}
/**Function*************************************************************
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_AssignRandom( Fra_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
Dar_ManForEachPi( p->pManAig, pObj, i )
Fra_NodeAssignRandom( p, pObj );
}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
{
Dar_Obj_t * pObj;
int i, Limit;
Dar_ManForEachPi( p->pManAig, pObj, i )
Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = ~pSims[i];
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
{
unsigned * pSims0, * pSims1;
int i;
pSims0 = Fra_ObjSim(pObj0);
pSims1 = Fra_ObjSim(pObj1);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims0[i] != pSims1[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_NodeSimulate( Fra_Man_t * p, Dar_Obj_t * pObj )
{
unsigned * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
assert( !Dar_IsComplement(pObj) );
assert( Dar_ObjIsNode(pObj) );
// get hold of the simulation information
pSims = Fra_ObjSim(pObj);
pSims0 = Fra_ObjSim(Dar_ObjFanin0(pObj));
pSims1 = Fra_ObjSim(Dar_ObjFanin1(pObj));
// get complemented attributes of the children using their random info
fCompl = pObj->fPhase;
fCompl0 = Dar_ObjFaninPhase(Dar_ObjChild0(pObj));
fCompl1 = Dar_ObjFaninPhase(Dar_ObjChild1(pObj));
// simulate
if ( fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (pSims0[i] | pSims1[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = ~(pSims0[i] | pSims1[i]);
}
else if ( fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (pSims0[i] | ~pSims1[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (~pSims0[i] & pSims1[i]);
}
else if ( !fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (~pSims0[i] | pSims1[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (pSims0[i] & ~pSims1[i]);
}
else // if ( !fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = ~(pSims0[i] & pSims1[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = (pSims0[i] & pSims1[i]);
}
}
/**Function*************************************************************
Synopsis [Generated const 0 pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SavePattern0( Fra_Man_t * p )
{
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
}
/**Function*************************************************************
Synopsis [[Generated const 1 pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SavePattern1( Fra_Man_t * p )
{
memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SavePattern( Fra_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Dar_ManForEachPi( p->pManFraig, pObj, i )
// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
Dar_InfoSetBit( p->pPatWords, i );
// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
Synopsis [Cleans pattern scores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_CleanPatScores( Fra_Man_t * p )
{
int i, nLimit = p->nSimWords * 32;
for ( i = 0; i < nLimit; i++ )
p->pPatScores[i] = 0;
}
/**Function*************************************************************
Synopsis [Adds to pattern scores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNew )
{
unsigned * pSims0, * pSims1;
unsigned uDiff;
int i, w;
// get hold of the simulation information
pSims0 = Fra_ObjSim(pClass);
pSims1 = Fra_ObjSim(pClassNew);
// iterate through the differences and record the score
for ( w = 0; w < p->nSimWords; w++ )
{
uDiff = pSims0[w] ^ pSims1[w];
if ( uDiff == 0 )
continue;
for ( i = 0; i < 32; i++ )
if ( uDiff & ( 1 << i ) )
p->pPatScores[w*32+i]++;
}
}
/**Function*************************************************************
Synopsis [Selects the best pattern.]
Description [Returns 1 if such pattern is found.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SelectBestPat( Fra_Man_t * p )
{
unsigned * pSims;
Dar_Obj_t * pObj;
int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
for ( i = 1; i < nLimit; i++ )
{
if ( MaxScore < p->pPatScores[i] )
{
MaxScore = p->pPatScores[i];
BestPat = i;
}
}
if ( MaxScore == 0 )
return 0;
// if ( MaxScore > p->pPars->MaxScore )
// printf( "Max score is %3d. ", MaxScore );
// copy the best pattern into the selected pattern
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Dar_ManForEachPi( p->pManAig, pObj, i )
{
pSims = Fra_ObjSim(pObj);
if ( Dar_InfoHasBit(pSims, BestPat) )
Dar_InfoSetBit(p->pPatWords, i);
}
return MaxScore;
}
/**Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SimulateOne( Fra_Man_t * p )
{
Dar_Obj_t * pObj;
int i, clk;
clk = clock();
Dar_ManForEachNode( p->pManAig, pObj, i )
{
Fra_NodeSimulate( p, pObj );
/*
if ( Dar_ObjFraig(pObj) == NULL )
printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
else
printf( "%3d %3d %2d %d : ", pObj->Id, Dar_Regular(Dar_ObjFraig(pObj))->Id, Dar_ObjSatNum(Dar_Regular(Dar_ObjFraig(pObj))), pObj->fPhase );
Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 );
printf( "\n" );
*/
}
p->timeSim += clock() - clk;
p->nSimRounds++;
}
/**Function*************************************************************
Synopsis [Resimulates fraiging manager after finding a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_Resimulate( Fra_Man_t * p )
{
int nChanges;
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
if ( p->pPars->fPatScores )
Fra_CleanPatScores( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
return;
if ( nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
if ( !p->pPars->fPatScores )
return;
// perform additional simulation using dist1 patterns derived from successful patterns
while ( Fra_SelectBestPat(p) > p->pPars->MaxScore )
{
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
Fra_CleanPatScores( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
return;
//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
if ( nChanges == 0 )
break;
}
}
/**Function*************************************************************
Synopsis [Performs simulation of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_Simulate( Fra_Man_t * p )
{
int nChanges, nClasses;
// start the classes
Fra_AssignRandom( p );
Fra_SimulateOne( p );
Fra_CreateClasses( p );
//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
// refine classes by walking 0/1 patterns
Fra_SavePattern0( p );
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
Fra_SavePattern1( p );
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
// refine classes by random simulation
do {
Fra_AssignRandom( p );
Fra_SimulateOne( p );
nClasses = Vec_PtrSize(p->vClasses);
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
// Fra_PrintSimClasses( p );
}
/**Function*************************************************************
Synopsis [Creates the counter-example from the successful pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
{
unsigned * pSims;
int i, k, BestPat, * pModel;
// find the word of the pattern
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims[i] )
break;
assert( i < p->nSimWords );
// find the bit of the pattern
for ( k = 0; k < 32; k++ )
if ( pSims[i] & (1 << k) )
break;
assert( k < 32 );
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
pModel = ALLOC( int, Dar_ManPiNum(p->pManFraig) );
Dar_ManForEachPi( p->pManAig, pObj, i )
{
pModel[i] = Dar_InfoHasBit(Fra_ObjSim(pObj), BestPat);
// printf( "%d", pModel[i] );
}
// printf( "\n" );
// set the model
assert( p->pManFraig->pData == NULL );
p->pManFraig->pData = pModel;
return;
}
/**Function*************************************************************
Synopsis [Returns 1 if the one of the output is already non-constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_CheckOutputSims( Fra_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Dar_ManPo( p->pManAig, 0 );
assert( Dar_ObjFanin0(pObj)->fPhase == (unsigned)Dar_ObjFaninC0(pObj) ); // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) == 0
Dar_ManForEachPo( p->pManAig, pObj, i )
{
// complement simulation info
// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) // Dar_ObjFaninPhase(Dar_ObjChild0(pObj))
// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
// check
if ( !Fra_NodeHasZeroSim( p, Dar_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
Fra_CheckOutputSimsSavePattern( p, Dar_ObjFanin0(pObj) );
return 1;
}
// complement simulation info
// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) )
// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
}
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

48
src/aig/fra/fra_.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [fra_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fra_.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2750
src/aig/fra/ivyFraig.c Normal file

File diff suppressed because it is too large Load Diff

7
src/aig/fra/module.make Normal file
View File

@ -0,0 +1,7 @@
SRC += src/aig/fra/fraAnd.c \
src/aig/fra/fraClass.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSim.c

View File

@ -331,7 +331,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
Dar_LibStart();
{
extern void Dar_LibStart();
Dar_LibStart();
}
}
/**Function*************************************************************
@ -347,7 +350,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
***********************************************************************/
void Abc_End()
{
Dar_LibStop();
{
extern void Dar_LibStop();
Dar_LibStop();
}
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
@ -2915,7 +2921,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
memset( pPars, 0, sizeof(Lut_Par_t) );
pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure
pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC
pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars)
pPars->nVarsShared = 3; // (S) the maximum number of shared variables (crossbars)
pPars->nGrowthLevel = 1;
pPars->fSatur = 1;
pPars->fZeroCost = 0;
@ -5942,6 +5948,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -6057,7 +6064,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Network should be strashed. Command has failed.\n" );
return 1;
}
pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );

View File

@ -20,6 +20,7 @@
#include "abc.h"
#include "dar.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -317,6 +318,130 @@ Dar_CnfFree( pCnf );
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
Dar_Obj_t * pObj, * pLeaf;
Cnf_Cut_t * pCut;
Vec_Int_t * vCover;
unsigned uTruth;
int i, k, nDupGates;
// create the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
// make the mapper point to the new network
Dar_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
Abc_NtkForEachCi( pNtk, pNode, i )
Dar_ManPi(p->pManAig, i)->pData = pNode->pCopy;
// process the nodes in topological order
vCover = Vec_IntAlloc( 1 << 16 );
Vec_PtrForEachEntry( vMapped, pObj, i )
{
// create new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add fanins according to the cut
pCut = pObj->pData;
Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
// add logic function
if ( pCut->nFanins < 5 )
{
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
}
else
pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
// save the node
pObj->pData = pNodeNew;
}
Vec_IntFree( vCover );
// add the CO drivers
Abc_NtkForEachCo( pNtk, pNode, i )
{
pObj = Dar_ManPo(p->pManAig, i);
pNodeNew = Abc_ObjNotCond( Dar_ObjFanin0(pObj)->pData, Dar_ObjFaninC0(pObj) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
// remove the constant node if not used
pNodeNew = (Abc_Obj_t *)Dar_ManConst1(p->pManAig)->pData;
if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
Abc_NtkDeleteObj( pNodeNew );
// minimize the node
// Abc_NtkSweep( pNtkNew, 0 );
// decouple the PO driver nodes to reduce the number of levels
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
// if ( nDupGates && If_ManReadVerbose(pIfMan) )
// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
{
Abc_Ntk_t * pNtkNew = NULL;
Cnf_Man_t * pCnf;
Dar_Man_t * pMan;
Cnf_Dat_t * pData;
assert( Abc_NtkIsStrash(pNtk) );
// convert to the AIG manager
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
if ( !Dar_ManCheck( pMan ) )
{
printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
Dar_ManStop( pMan );
return NULL;
}
// perform balance
Dar_ManPrintStats( pMan );
// derive CNF
pCnf = Cnf_ManStart();
pData = Cnf_Derive( pCnf, pMan );
{
Vec_Ptr_t * vMapped;
vMapped = Cnf_ManScanMapping( pCnf, 1 );
pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped );
Vec_PtrFree( vMapped );
}
Dar_ManStop( pMan );
Cnf_ManStop( pCnf );
// write CNF into a file
// Cnf_DataWriteIntoFile( pData, pFileName );
Cnf_DataFree( pData );
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

View File

@ -69,6 +69,7 @@ struct Lut_Man_t_
Vec_Int_t * vCover;
Vec_Vec_t * vLevels;
// temporary variables
int fCofactoring; // working in the cofactoring mode
int pRefs[LUT_SIZE_MAX]; // fanin reference counters
int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation
@ -106,6 +107,8 @@ static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((un
extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
static If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -1003,62 +1006,81 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit
SeeAlso []
***********************************************************************/
/*
int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
{
Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
// Kit_DsdObj_t * pRoot;
unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
unsigned i, * pTruth;
int MaxBlock
Verbose = 0;
int RetValue = 0;
Kit_DsdNtk_t * pNtk0, * pNtk1;//, * pTemp;
unsigned * pCofs2[3] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars), pNtk->pMem + 2 * Kit_TruthWordNum(pNtk->nVars) };
int i, MaxBlock0, MaxBlock1, MaxBlockBest = 1000, VarBest = -1;
int fVerbose = 1;
if ( fVerbose )
{
printf( "Function: " );
// printf( "Function: " );
// Extra_PrintBinary( stdout, pTruth, (1 << nVars) );
Extra_PrintHexadecimal( stdout, pTruth, nVars );
// Extra_PrintHexadecimal( stdout, pTruth, nVars );
printf( "\n" );
printf( "\n" );
printf( "V =%2d: ", pNtk->nVars );
Kit_DsdPrint( stdout, pNtk );
}
for ( i = 0; i < nVars; i++ )
{
Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
Kit_DsdNtkFree( pTemp );
Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
Kit_TruthXor( pCofs2[2], pCofs2[0], pCofs2[1], nVars );
pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
MaxBlock0 = Kit_DsdNonDsdSizeMax( pNtk0 );
// pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
// Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Variable %2d: Diff = %6d.\n", i, Kit_TruthCountOnes(pCofs2[2], nVars) );
printf( "Cof%d0: ", i );
Kit_DsdPrint( stdout, pNtk0 );
}
Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
Kit_DsdNtkFree( pTemp );
MaxBlock1 = Kit_DsdNonDsdSizeMax( pNtk1 );
// pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
// Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d1: ", i );
Kit_DsdPrint( stdout, pNtk1 );
}
if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
RetValue = 1;
if ( fVerbose )
{
printf( "MaxBlock0 = %2d. MaxBlock1 = %2d. ", MaxBlock0, MaxBlock1 );
if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
printf( " feasible\n" );
else
printf( "infeasible\n" );
}
if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
{
if ( MaxBlockBest > ABC_MAX(MaxBlock0, MaxBlock1) )
{
MaxBlockBest = ABC_MAX(MaxBlock0, MaxBlock1);
VarBest = i;
}
}
Kit_DsdNtkFree( pNtk0 );
Kit_DsdNtkFree( pNtk1 );
}
if ( fVerbose )
{
printf( "Best variable = %d.\n", VarBest );
printf( "\n" );
return RetValue;
}
return VarBest;
}
*/
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
@ -1070,7 +1092,7 @@ int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * p
SeeAlso []
***********************************************************************/
If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit, If_Obj_t * pResult )
{
Kit_Graph_t * pGraph;
Kit_DsdObj_t * pObj;
@ -1092,8 +1114,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
if ( pObj->Type == KIT_DSD_AND )
{
assert( pObj->nFans == 2 );
pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
return NULL;
pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) );
@ -1102,8 +1124,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
if ( pObj->Type == KIT_DSD_XOR )
{
assert( pObj->nFans == 2 );
pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
return NULL;
fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
@ -1116,11 +1138,22 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
// solve for the inputs
Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
{
pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin );
if ( i == 0 )
pFansNew[i] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
else
pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
if ( pFansNew[i] == NULL )
return NULL;
}
// find best cofactoring variable
// if ( pObj->nFans > 3 )
// Kit_DsdCofactoring( Kit_DsdObjTruth(pObj), pObj->nFans, NULL, 4, 1 );
if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
// return Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
// derive the factored form
pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
if ( pGraph == NULL )
@ -1194,7 +1227,7 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
If_ManSetupCiCutSets( p->pIfMan );
// create the internal nodes
// pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root );
pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root );
pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root, NULL );
if ( pDriver == NULL )
return 0;
// create the PO node
@ -1460,6 +1493,280 @@ int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
return 1;
}
/**Function*************************************************************
Synopsis [Records variable order.]
Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_LutCreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
{
Kit_DsdObj_t * pObj;
unsigned uSuppFanins, k;
int Above[16], Below[16];
int nAbove, nBelow, iFaninLit, i, x, y;
// iterate through the nodes
Kit_DsdNtkForEachObj( pNtk, pObj, i )
{
// collect fanin support of this node
nAbove = 0;
uSuppFanins = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
{
if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
else
uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
}
// find the below variables
nBelow = 0;
for ( y = 0; y < 16; y++ )
if ( uSuppFanins & (1 << y) )
Below[nBelow++] = y;
// create all pairs
for ( x = 0; x < nAbove; x++ )
for ( y = 0; y < nBelow; y++ )
pTable[Above[x]][Below[y]]++;
}
}
/**Function*************************************************************
Synopsis [Creates commmon variable order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_LutCreateCommonOrder( char pTable[][16], int pOrder[], int nLeaves )
{
int Score[16] = {0};
int i, y, x;
// compute scores for each leaf
for ( i = 0; i < nLeaves; i++ )
{
for ( y = 0; y < nLeaves; y++ )
Score[i] += pTable[i][y];
for ( x = 0; x < nLeaves; x++ )
Score[i] -= pTable[x][i];
}
/*
printf( "Scores: " );
for ( i = 0; i < nLeaves; i++ )
printf( "%d ", Score[i] );
printf( "\n" );
*/
// sort the scores
Extra_BubbleSort( pOrder, Score, nLeaves, 0 );
/*
printf( "Scores: " );
for ( i = 0; i < nLeaves; i++ )
printf( "%d ", Score[pOrder[i]] );
printf( "\n" );
*/
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Abc_LutIfManMapMulti_rec( Lut_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pOrder )
{
Kit_DsdObj_t * pObj;
If_Obj_t * pObjsNew[4][8], * pResPrev;
unsigned uSupps[8], uSuppFanin;
int piLitsNew[8], pDecision[8] = {0};
int i, v, k, nSize = (1 << nCBars);
// find which of the variables is highest in the order
// go though non-trivial components
for ( i = 0; i < nSize; i++ )
{
if ( piLits[i] == -1 )
continue;
pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
uSuppFanin = pObj? Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ) : 0;
uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
}
// find the variable that appears the highest in the order
for ( v = 0; v < nLeaves; v++ )
{
for ( i = 0; i < nSize; i++ )
if ( uSupps[i] & (1 << pOrder[v]) )
break;
}
assert( v < nLeaves );
// pull out all components that have this variable
for ( i = 0; i < nSize; i++ )
pDecision[i] = ( uSupps[i] & (1 << pOrder[v]) );
// iterate over the nodes
for ( i = 0; i < nSize; i++ )
{
pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
if ( pDecision[i] )
piLitsNew[i] = pObj->pFans[0];
else
piLitsNew[i] = piLits[i];
}
// call again
pResPrev = Abc_LutIfManMapMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pOrder );
// create new set of nodes
for ( i = 0; i < nSize; i++ )
{
if ( pDecision[i] )
pObjsNew[nCBars][i] = Abc_LutIfManMap_rec( p, ppNtks[i], piLits[i], pResPrev );
else
pObjsNew[nCBars][i] = pResPrev;
}
// create MUX using these outputs
for ( k = nCBars; k > 0; k-- )
{
nSize /= 2;
for ( i = 0; i < nSize; i++ )
pObjsNew[k-1][i] = If_ManCreateMnux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
}
assert( nCBars == 1 && nSize == 1 );
return If_NotCond( pObjsNew[0][0], nCBars & 1 );
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
If_Obj_t * pResult;
Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
int piCofVar[4], pOrder[16] = {0}, pPrios[16], pFreqs[16] = {0}, piLits[16];
int i, k, nCBars, nSize, nMemSize;
unsigned * ppCofs[4][8], uSupport;
char pTable[16][16] = {0};
int fVerbose = 1;
// allocate storage for cofactors
nMemSize = Kit_TruthWordNum(nVars);
ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
nSize = 0;
for ( i = 0; i < 4; i++ )
for ( k = 0; k < 8; k++ )
ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
assert( nSize == 32 );
// find the best cofactoring variables
nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
// copy the function
Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
// decompose w.r.t. these variables
for ( k = 0; k < nCBars; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
nSize = (1 << nCBars);
// compute variable frequences
for ( i = 0; i < nSize; i++ )
{
uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
for ( k = 0; k < nVars; k++ )
if ( uSupport & (1<<k) )
pFreqs[k]++;
}
// compute DSD networks
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nCBars, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
}
free( ppCofs[0][0] );
// find common variable order
for ( i = 0; i < nSize; i++ )
{
Kit_DsdGetSupports( ppNtks[i] );
Abc_LutCreateVarOrder( ppNtks[i], pTable );
}
Abc_LutCreateCommonOrder( pTable, pOrder, nVars );
printf( "Common variable order: " );
for ( i = 0; i < nVars; i++ )
printf( "%c ", 'a' + pOrder[i] );
printf( "\n" );
// derive variable priority
for ( i = 0; i < 16; i++ )
pPrios[i] = 16;
for ( i = 0; i < nVars; i++ )
pPrios[pOrder[i]] = i;
// transform all networks according to the variable order
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
Kit_DsdNtkFree( pTemp );
Kit_DsdGetSupports( ppNtks[i] );
// undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
Kit_DsdRotate( ppNtks[i], pFreqs );
// collect the roots
piLits[i] = ppNtks[i]->Root;
}
/*
p->fCofactoring = 1;
pResult = Abc_LutIfManMapMulti_rec( p, ppNtks[nCBars], piLits, piCofVar, nCBars, ppLeaves, nVars, pOrder );
p->fCofactoring = 0;
*/
// free the networks
for ( i = 0; i < 8; i++ )
if ( ppNtks[i] )
Kit_DsdNtkFree( ppNtks[i] );
return pResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1414,13 +1414,19 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
char * pFileName;
int c;
int fAllPrimes;
int fNewAlgo;
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
fNewAlgo = 1;
fAllPrimes = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF )
{
switch ( c )
{
case 'n':
fNewAlgo ^= 1;
break;
case 'p':
fAllPrimes ^= 1;
break;
@ -1441,15 +1447,18 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
}
// call the corresponding file writer
if ( fAllPrimes )
if ( fNewAlgo )
Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName );
else if ( fAllPrimes )
Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
else
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" );
fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" );
fprintf( pAbc->Err, "\t write the miter cone into a CNF file\n" );
fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );

View File

@ -337,6 +337,7 @@ extern If_Obj_t * If_ManCreateCi( If_Man_t * p );
extern If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
extern If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
extern If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl );
extern void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
extern void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
extern void If_ManSetupCiCutSets( If_Man_t * p );

View File

@ -235,6 +235,25 @@ If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
}
/**Function*************************************************************
Synopsis [Create the new node assuming it does not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl )
{
If_Obj_t * pRes1, * pRes2;
pRes1 = If_ManCreateAnd( p, pFan0, 0, pCtrl, 1 );
pRes2 = If_ManCreateAnd( p, pFan1, 0, pCtrl, 0 );
return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
}
/**Function*************************************************************
Synopsis [Creates the choice node.]

View File

@ -405,6 +405,8 @@ extern void ** Extra_ArrayAlloc( int nCols, int nRows, int Size );
extern unsigned short ** Extra_TruthPerm43();
extern unsigned ** Extra_TruthPerm53();
extern unsigned ** Extra_TruthPerm54();
/* bubble sort for small number of entries */
extern void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing );
/* for independence from CUDD */
extern unsigned int Cudd_PrimeCopy( unsigned int p );

View File

@ -2068,6 +2068,55 @@ unsigned ** Extra_Truths8()
return (unsigned **)puResult;
}
/**Function*************************************************************
Synopsis [Bubble-sorts components by scores in increasing order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_BubbleSort( int Order[], int Costs[], int nSize, int fIncreasing )
{
int i, Temp, fChanges;
assert( nSize < 1000 );
for ( i = 0; i < nSize; i++ )
Order[i] = i;
if ( fIncreasing )
{
do {
fChanges = 0;
for ( i = 0; i < nSize - 1; i++ )
{
if ( Costs[Order[i]] <= Costs[Order[i+1]] )
continue;
Temp = Order[i];
Order[i] = Order[i+1];
Order[i+1] = Temp;
fChanges = 1;
}
} while ( fChanges );
}
else
{
do {
fChanges = 0;
for ( i = 0; i < nSize - 1; i++ )
{
if ( Costs[Order[i]] >= Costs[Order[i+1]] )
continue;
Temp = Order[i];
Order[i] = Order[i+1];
Order[i+1] = Temp;
fChanges = 1;
}
} while ( fChanges );
}
}
/**Function*************************************************************
Synopsis [Returns the smallest prime larger than the number.]
@ -2104,7 +2153,6 @@ unsigned int Cudd_PrimeCopy( unsigned int p)
} /* end of Cudd_Prime */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/

View File

@ -163,7 +163,7 @@ static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->nCap = pVec->nSize;
p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
return p;

View File

@ -120,6 +120,7 @@ struct Kit_DsdNtk_t_
unsigned char nNodes; // the number of nodes
unsigned char Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?)
unsigned * pSupps; // supports of the nodes
Kit_DsdObj_t * pNodes[0]; // the nodes
};
@ -142,8 +143,10 @@ static inline int Kit_DsdLitRegular( int Lit ) { return Li
static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
static inline int Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit ) { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit ) { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return pNtk->pSupps? (Id < pNtk->nVars? (1 << Id) : pNtk->pSupps[Id - pNtk->nVars]) : 0; }
#define Kit_DsdNtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
@ -398,6 +401,12 @@ static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned
pOut[w] = pIn0[w] & pIn1[w];
}
}
static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
}
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
@ -428,6 +437,11 @@ extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
extern void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] );
extern int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose );
/*=== kitFactor.c ==========================================================*/
extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
/*=== kitGraph.c ==========================================================*/
@ -478,7 +492,7 @@ extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );

View File

@ -153,6 +153,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
unsigned i;
Kit_DsdNtkForEachObj( pNtk, pObj, i )
free( pObj );
FREE( pNtk->pSupps );
free( pNtk->pMem );
free( pNtk );
}
@ -643,6 +644,296 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Sorts the literals by their support.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars )
{
int nSuppSizes[16], Priority[16], pOrder[16], Temp[16];
int i, k, iVarBest, SuppMax, PrioMin;
// compute support sizes and priorities of the components
for ( i = 0; i < nVars; i++ )
{
Temp[i] = piLitsNew[i];
pOrder[i] = i;
Priority[i] = 16;
nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
for ( k = 0; k < 16; k++ )
if ( uSupps[i] & (1 << k) )
Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
assert( Priority[i] != 16 );
}
// find the component by with largest size and smallest priority
iVarBest = -1;
SuppMax = 0;
PrioMin = 16;
for ( i = 0; i < nVars; i++ )
{
if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) )
{
SuppMax = nSuppSizes[i];
PrioMin = Priority[i];
iVarBest = i;
}
}
// sort the components by pririty
Extra_BubbleSort( pOrder, Priority, nVars, 1 );
// copy the resulting literals
k = 0;
piLitsNew[k++] = piLitsNew[iVarBest];
for ( i = 0; i < nVars; i++ )
{
if ( pOrder[i] == iVarBest )
continue;
piLitsNew[k++] = piLitsNew[pOrder[i]];
}
}
/**Function*************************************************************
Synopsis [Shrinks multi-input nodes.]
Description [Takes the array of variable priorities pPrios.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPrios[] )
{
Kit_DsdObj_t * pObj, * pObjNew;
unsigned * pTruth, * pTruthNew;
unsigned i, piLitsNew[16], uSupps[16];
int fCompl, iLitFanin, iLitNew;
// remember the complement
fCompl = Kit_DsdLitIsCompl(iLit);
iLit = Kit_DsdLitRegular(iLit);
assert( !Kit_DsdLitIsCompl(iLit) );
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return Kit_DsdLitNotCond( iLit, fCompl );
if ( pObj->Type == KIT_DSD_AND )
{
if ( pObj->nFans == 2 )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
}
else
{
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
piLitsNew[i] = iLitFanin;
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
// put the largest component first
// sort other components in the increasing order of the highest variable
Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
pObjNew->pFans[0] = iLitNew;
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
}
return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
}
if ( pObj->Type == KIT_DSD_XOR )
{
if ( pObj->nFans == 2 )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
}
else
{
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
piLitsNew[i] = iLitFanin;
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
// put the largest component first
// sort other components in the increasing order of the highest variable
Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
pObjNew->pFans[0] = iLitNew;
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
}
return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
}
assert( pObj->Type == KIT_DSD_PRIME );
// create new PRIME node
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
// copy the truth table
pTruth = Kit_DsdObjTruth( pObj );
pTruthNew = Kit_DsdObjTruth( pObjNew );
Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
// create fanins
Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
{
pObjNew->pFans[i] = Kit_DsdShrink_rec( pNew, p, iLitFanin, pPrios );
// complement the corresponding inputs of the truth table
if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) )
{
pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]);
Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
}
}
// if the incoming phase is complemented, absorb it into the prime node
if ( fCompl )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
/**Function*************************************************************
Synopsis [Shrinks the network.]
Description [Transforms the network to have two-input nodes so that the
higher-ordered nodes were decomposed out first.]
SideEffects []
SeeAlso []
***********************************************************************/
Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] )
{
Kit_DsdNtk_t * pNew;
Kit_DsdObj_t * pObjNew;
assert( p->nVars <= 16 );
// create a new network
pNew = Kit_DsdNtkAlloc( p->nVars );
// consider simple special cases
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
return pNew;
}
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
return pNew;
}
// convert the root node
pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
return pNew;
}
/**Function*************************************************************
Synopsis [Rotates the network.]
Description [Transforms prime nodes to have the fanin with the
highest frequency of supports go first.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
{
Kit_DsdObj_t * pObj;
unsigned * pIn, * pOut, * pTemp, k;
int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
int Weights[16];
// go through the prime nodes
Kit_DsdNtkForEachObj( p, pObj, i )
{
if ( pObj->Type != KIT_DSD_PRIME )
continue;
// count the fanin frequencies
Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
{
uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
Weights[k] = 0;
for ( v = 0; v < 16; v++ )
if ( uSuppFanin & (1 << v) )
Weights[k] += pFreqs[v];
}
// find the most frequent fanin
WeightMax = FaninMax = 0;
for ( k = 0; k < pObj->nFans; k++ )
if ( WeightMax < Weights[k] )
{
WeightMax = Weights[k];
FaninMax = k;
}
assert( k < pObj->nFans );
// move the fanins number k to the first place
nSwaps = 0;
pIn = Kit_DsdObjTruth(pObj);
pOut = p->pSupps;
for ( v = k-1; v >= 0; v-- )
{
// swap the fanins
Temp = pObj->pFans[v];
pObj->pFans[v] = pObj->pFans[v+1];
pObj->pFans[v+1] = Temp;
// swap the truth table variables
Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
pTemp = pIn; pIn = pOut; pOut = pTemp;
nSwaps++;
}
if ( nSwaps & 1)
Kit_TruthCopy( pIn, pOut, pObj->nFans );
}
}
/**Function*************************************************************
Synopsis [Compute the support.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
{
Kit_DsdObj_t * pObj;
unsigned uSupport, k;
int iFaninLit, i;
p->pSupps = ALLOC( unsigned, p->nNodes );
Kit_DsdNtkForEachObj( p, pObj, i )
{
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
uSupport |= Kit_DsdLitSupport( p, iFaninLit );
p->pSupps[pObj->Id - p->nVars] = uSupport;
}
}
/**Function*************************************************************
Synopsis [Returns 1 if there is a component with more than 3 inputs.]
@ -926,10 +1217,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
// update the node
// if ( fEquals[0][0] && fEquals[0][1] )
// Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
// Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
// else
// Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
Kit_TruthMux( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
// Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
if ( fEquals[1][0] && fEquals[1][1] )
pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
// decompose the remainder
@ -967,17 +1258,17 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
{
pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
Kit_TruthMuxVar( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
}
else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
{
pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
}
else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
{
pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
}
else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
{
@ -986,7 +1277,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
// unsigned uSupp;
// Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
// Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
// uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
// Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
}
@ -994,7 +1285,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
{
assert( fPairs[0][3] && fPairs[1][2] );
pRes->Type = KIT_DSD_XOR;;
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
}
// decompose the remainder
Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
@ -1317,6 +1608,170 @@ void Kit_DsdPrecompute4Vars()
printf( "non-DSD = %d implementable = %d\n", Counter1, Counter2 );
}
/**Function*************************************************************
Synopsis [Returns the set of cofactoring variables.]
Description [If there is no DSD components returns 0.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdCofactoringGetVars( Kit_DsdNtk_t ** ppNtk, int nSize, int * pVars )
{
Kit_DsdObj_t * pObj;
unsigned m;
int i, k, v, Var, nVars, iFaninLit;
// go through all the networks
nVars = 0;
for ( i = 0; i < nSize; i++ )
{
// go through the prime objects of each networks
Kit_DsdNtkForEachObj( ppNtk[i], pObj, k )
{
if ( pObj->Type != KIT_DSD_PRIME )
continue;
if ( pObj->nFans == 3 )
continue;
// collect direct fanin variables
Kit_DsdObjForEachFanin( ppNtk[i], pObj, iFaninLit, m )
{
if ( !Kit_DsdLitIsLeaf(ppNtk[i], iFaninLit) )
continue;
// add it to the array
Var = Kit_DsdLit2Var( iFaninLit );
for ( v = 0; v < nVars; v++ )
if ( pVars[v] == Var )
break;
if ( v == nVars )
pVars[nVars++] = Var;
}
}
}
return nVars;
}
/**Function*************************************************************
Synopsis [Canonical decomposition into completely DSD-structure.]
Description [Returns the number of cofactoring steps. Also returns
the cofactoring variables in pVars.]
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose )
{
Kit_DsdNtk_t * ppNtks[5][16] = {0}, * pTemp;
unsigned * ppCofs[5][16];
int pTryVars[16], nTryVars;
int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
int nSuppSizeMin, nSuppSizeMax, iVarBest;
int i, k, v, nStep, nSize, nMemSize;
assert( nLimit < 5 );
// allocate storage for cofactors
nMemSize = Kit_TruthWordNum(nVars);
ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
nSize = 0;
for ( i = 0; i < 5; i++ )
for ( k = 0; k < 16; k++ )
ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
assert( nSize == 80 );
// copy the function
Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
if ( fVerbose )
printf( "\nProcessing prime function with %d support variables:\n", nVars );
// perform recursive cofactoring
for ( nStep = 0; nStep < nLimit; nStep++ )
{
nSize = (1 << nStep);
// find the variables to use in the cofactoring step
nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
if ( nTryVars == 0 )
break;
// cofactor w.r.t. the above variables
iVarBest = -1;
nPrimeSizeMin = 10000;
nSuppSizeMin = 10000;
for ( v = 0; v < nTryVars; v++ )
{
nPrimeSizeMax = 0;
nSuppSizeMax = 0;
for ( i = 0; i < nSize; i++ )
{
// cofactor and decompose cofactors
Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
// compute the largest non-decomp block
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
// compute the sum total of supports
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
// free the networks
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
}
// find the min max support size of the prime component
if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
{
nPrimeSizeMin = nPrimeSizeMax;
nSuppSizeMin = nSuppSizeMax;
iVarBest = pTryVars[v];
}
}
assert( iVarBest != -1 );
// save the variable
if ( pCofVars )
pCofVars[nStep] = iVarBest;
// cofactor w.r.t. the best
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
if ( fVerbose )
{
ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
Kit_DsdNtkFree( pTemp );
ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
Kit_DsdNtkFree( pTemp );
printf( "Cof%d%d: ", nStep+1, 2*i+0 );
Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] );
printf( "Cof%d%d: ", nStep+1, 2*i+1 );
Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] );
}
}
}
// free the networks
for ( i = 0; i < 5; i++ )
for ( k = 0; k < 16; k++ )
if ( ppNtks[i][k] )
Kit_DsdNtkFree( ppNtks[i][k] );
free( ppCofs[0][0] );
assert( nStep <= nLimit );
return nStep;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -854,7 +854,7 @@ void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned
SeeAlso []
***********************************************************************/
void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;