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

Merged alanmi/abc into default

This commit is contained in:
Mathias Soeken 2016-12-07 10:08:44 +01:00
parent f9b7e92904 77ef610919
commit 5af44731bf
47 changed files with 7347 additions and 256 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -22,7 +22,7 @@ MODULES := \
src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/bool/rsb src/bool/rpo \

68
abclib.dsp
View File

@ -807,6 +807,10 @@ SOURCE=.\src\base\wlc\wlcStdin.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcWin.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcWriteVer.c
# End Source File
# End Group
@ -967,6 +971,10 @@ SOURCE=.\src\base\cba\cbaReadVer.c
# End Source File
# Begin Source File
SOURCE=.\src\base\cba\cbaTypes.h
# End Source File
# Begin Source File
SOURCE=.\src\base\cba\cbaWriteBlif.c
# End Source File
# Begin Source File
@ -2670,6 +2678,50 @@ SOURCE=.\src\opt\fxch\FxchMan.c
SOURCE=.\src\opt\fxch\FxchSCHashTable.c
# End Source File
# End Group
# Begin Group "dsc"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\dsc\dsc.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\dsc\dsc.h
# End Source File
# End Group
# Begin Group "sbd"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\sbd\sbd.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbd.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdSat.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdWin.c
# End Source File
# End Group
# End Group
# Begin Group "map"
@ -4525,6 +4577,10 @@ SOURCE=.\src\aig\gia\giaUtil.c
SOURCE=.\src\aig\miniaig\miniaig.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\miniaig\minilut.h
# End Source File
# End Group
# End Group
# Begin Group "bool"
@ -5359,6 +5415,10 @@ SOURCE=.\src\proof\acec\acec.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecCl.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecCo.c
# End Source File
# Begin Source File
@ -5383,6 +5443,10 @@ SOURCE=.\src\proof\acec\acecOrder.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecPa.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecPo.c
# End Source File
# Begin Source File
@ -5391,6 +5455,10 @@ SOURCE=.\src\proof\acec\acecPolyn.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecPool.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecRe.c
# End Source File
# Begin Source File

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

@ -1382,6 +1382,8 @@ extern Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pP
/*=== giaMini.c ===========================================================*/
extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName );
extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
extern Gia_Man_t * Gia_ManReadMiniLut( char * pFileName );
extern void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName );
/*=== giaMuxes.c ===========================================================*/
extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
extern void Gia_ManPrintMuxStats( Gia_Man_t * p );

182
src/aig/gia/giaMini.c
View File

@ -19,8 +19,10 @@
***********************************************************************/
#include "gia.h"
#include "opt/dau/dau.h"
#include "base/main/main.h"
#include "aig/miniaig/miniaig.h"
#include "aig/miniaig/minilut.h"
ABC_NAMESPACE_IMPL_START
@ -180,6 +182,186 @@ void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
Mini_AigStop( p );
}
/**Function*************************************************************
Synopsis [Converts MiniLUT into GIA.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p )
{
Gia_Man_t * pGia, * pTemp;
Vec_Int_t * vCopies;
Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
int i, k, Fan, iGiaLit, nNodes;
int LutSize = Abc_MaxInt( 2, Mini_LutSize(p) );
assert( LutSize <= 6 );
// get the number of nodes
nNodes = Mini_LutNodeNum(p);
// create ABC network
pGia = Gia_ManStart( 3 * nNodes );
pGia->pName = Abc_UtilStrsav( "MiniLut" );
// create mapping from MiniLUT objects into ABC objects
vCopies = Vec_IntAlloc( nNodes );
Vec_IntPush( vCopies, 0 );
Vec_IntPush( vCopies, 1 );
// iterate through the objects
Gia_ManHashAlloc( pGia );
for ( i = 2; i < nNodes; i++ )
{
if ( Mini_LutNodeIsPi( p, i ) )
iGiaLit = Gia_ManAppendCi(pGia);
else if ( Mini_LutNodeIsPo( p, i ) )
iGiaLit = Gia_ManAppendCo(pGia, Vec_IntEntry(vCopies, Mini_LutNodeFanin(p, i, 0)));
else if ( Mini_LutNodeIsNode( p, i ) )
{
unsigned * puTruth = Mini_LutNodeTruth( p, i );
word Truth = LutSize == 6 ? *(word *)puTruth : ((word)*puTruth << 32) | (word)*puTruth;
Vec_IntClear( vLits );
Mini_LutForEachFanin( p, i, Fan, k )
Vec_IntPush( vLits, Vec_IntEntry(vCopies, Fan) );
iGiaLit = Dsm_ManTruthToGia( pGia, &Truth, vLits, vCover );
}
else assert( 0 );
Vec_IntPush( vCopies, iGiaLit );
}
Vec_IntFree( vCover );
Vec_IntFree( vLits );
Gia_ManHashStop( pGia );
assert( Vec_IntSize(vCopies) == nNodes );
Vec_IntFree( vCopies );
Gia_ManSetRegNum( pGia, Mini_LutRegNum(p) );
pGia = Gia_ManCleanup( pTemp = pGia );
Gia_ManStop( pTemp );
return pGia;
}
/**Function*************************************************************
Synopsis [Converts GIA into MiniLUT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia )
{
Mini_Lut_t * p;
Vec_Wrd_t * vTruths;
Gia_Obj_t * pObj, * pFanin;
int i, k, LutSize, pVars[16];
word Truth;
assert( Gia_ManHasMapping(pGia) );
LutSize = Gia_ManLutSizeMax( pGia );
assert( LutSize >= 2 );
// create the manager
p = Mini_LutStart( LutSize );
// create primary inputs
Gia_ManFillValue( pGia );
Gia_ManForEachCi( pGia, pObj, i )
pObj->Value = Mini_LutCreatePi(p);
// create internal nodes
vTruths = Vec_WrdStart( Gia_ManObjNum(pGia) );
Gia_ManForEachLut( pGia, i )
{
pObj = Gia_ManObj( pGia, i );
Gia_LutForEachFaninObj( pGia, i, pFanin, k )
pVars[k] = pFanin->Value;
Truth = Gia_LutComputeTruth6( pGia, i, vTruths );
pObj->Value = Mini_LutCreateNode( p, Gia_ObjLutSize(pGia, i), pVars, (unsigned *)&Truth );
}
Vec_WrdFree( vTruths );
// create primary outputs
Gia_ManForEachCo( pGia, pObj, i )
{
if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(pGia) )
pObj->Value = Mini_LutCreatePo( p, Gia_ObjFaninC0(pObj) );
else if ( !Gia_ObjFaninC0(pObj) )
pObj->Value = Mini_LutCreatePo( p, Gia_ObjFanin0(pObj)->Value );
else // add inverter LUT
{
word TruthInv = ABC_CONST(0x5555555555555555);
int Fanin = Gia_ObjFanin0(pObj)->Value;
int LutInv = Mini_LutCreateNode( p, 1, &Fanin, (unsigned *)&TruthInv );
pObj->Value = Mini_LutCreatePo( p, LutInv );
}
}
// set registers
Mini_LutSetRegNum( p, Gia_ManRegNum(pGia) );
//Mini_LutPrintStats( p );
return p;
}
/**Function*************************************************************
Synopsis [Procedures to input/output MiniAIG into/from internal GIA.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * p )
{
Gia_Man_t * pGia;
if ( pAbc == NULL )
printf( "ABC framework is not initialized by calling Abc_Start()\n" );
pGia = Gia_ManFromMiniLut( (Mini_Lut_t *)p );
Abc_FrameUpdateGia( pAbc, pGia );
// Gia_ManDelete( pGia );
}
void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc )
{
Gia_Man_t * pGia;
if ( pAbc == NULL )
printf( "ABC framework is not initialized by calling Abc_Start()\n" );
pGia = Abc_FrameReadGia( pAbc );
if ( pGia == NULL )
printf( "Current network in ABC framework is not defined.\n" );
return Gia_ManToMiniLut( pGia );
}
/**Function*************************************************************
Synopsis [Procedures to read/write GIA to/from MiniAIG file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManReadMiniLut( char * pFileName )
{
Mini_Lut_t * p = Mini_LutLoad( pFileName );
Gia_Man_t * pGia = Gia_ManFromMiniLut( p );
ABC_FREE( pGia->pName );
pGia->pName = Extra_FileNameGeneric( pFileName );
Mini_LutStop( p );
return pGia;
}
void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName )
{
Mini_Lut_t * p = Gia_ManToMiniLut( pGia );
Mini_LutDump( p, pFileName );
Mini_LutStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/gia/giaMuxes.c
View File

@ -100,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC, * pSiblNew, * pObjNew;
int i;
assert( p->pMuxes == NULL );
assert( Limit >= 1 ); // allows to create AIG with XORs without MUXes
assert( Limit >= 0 ); // allows to create AIG with XORs without MUXes
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
// start the new manager

2
src/aig/gia/giaSatMap.c
View File

@ -489,7 +489,7 @@ int Sbm_ManTestSat( void * pMan )
StartSol = Vec_IntSize(p->vSolCuts);
// StartSol = 30;
while ( fKeepTrying )
while ( fKeepTrying && StartSol-fKeepTrying > 0 )
{
printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
// for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )

4
src/aig/miniaig/abcapis.h
View File

@ -54,6 +54,10 @@ extern void Abc_NtkInputMiniAig( void * pAbc, void * pMiniAig );
extern void * Abc_NtkOutputMiniAig( void * pAbc );
extern void Abc_NtkSetFlopNum( void * pAbc, int nFlops );
// procedures to input/output 'mini AIG'
extern void Abc_NtkInputMiniLut( void * pAbc, void * pMiniLut );
extern void * Abc_NtkOutputMiniLut( void * pAbc );
// procedures to set CI/CO arrival/required times
extern void Abc_NtkSetCiArrivalTime( void * pAbc, int iCi, float Rise, float Fall );
extern void Abc_NtkSetCoRequiredTime( void * pAbc, int iCo, float Rise, float Fall );

1
src/aig/miniaig/miniaig.h
View File

@ -78,6 +78,7 @@ static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 )
{
if ( p->nSize + 2 > p->nCap )
{
assert( p->nSize < MINI_AIG_NULL/4 );
if ( p->nCap < MINI_AIG_START_SIZE )
Mini_AigGrow( p, MINI_AIG_START_SIZE );
else

288
src/aig/miniaig/minilut.h Normal file
View File

@ -0,0 +1,288 @@
/**CFile****************************************************************
FileName [minilut.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Minimalistic representation of LUT mapped network.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 29, 2012.]
Revision [$Id: minilut.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef MINI_LUT__mini_lut_h
#define MINI_LUT__mini_lut_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define MINI_LUT_NULL (0x7FFFFFFF)
#define MINI_LUT_NULL2 (0x7FFFFFFE)
#define MINI_LUT_START_SIZE (0x000000FF)
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Mini_Lut_t_ Mini_Lut_t;
struct Mini_Lut_t_
{
int nCap;
int nSize;
int nRegs;
int LutSize;
int * pArray;
unsigned * pTruths;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// memory management
#define MINI_LUT_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#define MINI_LUT_CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
#define MINI_LUT_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
#define MINI_LUT_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#define MINI_LUT_REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
// compute truth table size measured in unsigned's
static int Mini_LutWordNum( int LutSize )
{
return LutSize > 5 ? 1 << (LutSize-5) : 1;
}
// internal procedures
static void Mini_LutGrow( Mini_Lut_t * p, int nCapMin )
{
if ( p->nCap >= nCapMin )
return;
p->pArray = MINI_LUT_REALLOC( int, p->pArray, nCapMin * p->LutSize );
p->pTruths = MINI_LUT_REALLOC( unsigned, p->pTruths, nCapMin * Mini_LutWordNum(p->LutSize) );
p->nCap = nCapMin;
assert( p->pArray );
assert( p->pTruths );
}
static void Mini_LutPush( Mini_Lut_t * p, int nVars, int * pVars, unsigned * pTruth )
{
int i, nWords = Mini_LutWordNum(p->LutSize);
if ( p->nSize == p->nCap )
{
assert( p->LutSize*p->nSize < MINI_LUT_NULL/2 );
if ( p->nCap < MINI_LUT_START_SIZE )
Mini_LutGrow( p, MINI_LUT_START_SIZE );
else
Mini_LutGrow( p, 2 * p->nCap );
}
for ( i = 0; i < nVars; i++ )
p->pArray[p->LutSize * p->nSize + i] = pVars[i];
for ( ; i < p->LutSize; i++ )
p->pArray[p->LutSize * p->nSize + i] = MINI_LUT_NULL;
for ( i = 0; i < nWords; i++ )
p->pTruths[nWords * p->nSize + i] = pTruth? pTruth[i] : 0;
p->nSize++;
}
// accessing fanins
static int Mini_LutNodeFanin( Mini_Lut_t * p, int Id, int k )
{
assert( Id >= 0 && Id < p->nSize );
return p->pArray[p->LutSize*Id+k];
}
static unsigned * Mini_LutNodeTruth( Mini_Lut_t * p, int Id )
{
assert( Id >= 0 && Id < p->nSize );
return p->pTruths + Id * Mini_LutWordNum(p->LutSize);
}
// working with LUTs
static int Mini_LutNodeConst0() { return 0; }
static int Mini_LutNodeConst1() { return 1; }
static int Mini_LutNodeNum( Mini_Lut_t * p ) { return p->nSize; }
static int Mini_LutNodeIsConst( Mini_Lut_t * p, int Id ) { assert( Id >= 0 ); return Id == 0 || Id == 1; }
static int Mini_LutNodeIsPi( Mini_Lut_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) == MINI_LUT_NULL; }
static int Mini_LutNodeIsPo( Mini_Lut_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) == MINI_LUT_NULL2; }
static int Mini_LutNodeIsNode( Mini_Lut_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) != MINI_LUT_NULL2; }
static int Mini_LutSize( Mini_Lut_t * p ) { return p->LutSize; }
// working with sequential AIGs
static int Mini_LutRegNum( Mini_Lut_t * p ) { return p->nRegs; }
static void Mini_LutSetRegNum( Mini_Lut_t * p, int n ) { p->nRegs = n; }
// iterators through objects
#define Mini_LutForEachPi( p, i ) for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsPi(p, i) ) {} else
#define Mini_LutForEachPo( p, i ) for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsPo(p, i) ) {} else
#define Mini_LutForEachNode( p, i ) for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsNode(p, i) ) {} else
// iterator through fanins
#define Mini_LutForEachFanin( p, i, Fan, k ) for (k = 0; (k < p->LutSize) && (Fan = Mini_LutNodeFanin(p, i, k)) < MINI_LUT_NULL2; k++)
// constructor/destructor
static Mini_Lut_t * Mini_LutStart( int LutSize )
{
Mini_Lut_t * p; int i;
assert( LutSize >= 2 && LutSize <= 16 );
p = MINI_LUT_CALLOC( Mini_Lut_t, 1 );
p->LutSize = LutSize;
p->nCap = MINI_LUT_START_SIZE;
p->pArray = MINI_LUT_ALLOC( int, p->nCap * p->LutSize );
p->pTruths = MINI_LUT_ALLOC( unsigned, p->nCap * Mini_LutWordNum(p->LutSize) );
Mini_LutPush( p, 0, NULL, NULL ); // const0
Mini_LutPush( p, 0, NULL, NULL ); // const1
for ( i = 0; i < Mini_LutWordNum(p->LutSize); i++ )
p->pTruths[i] = 0;
for ( i = 0; i < Mini_LutWordNum(p->LutSize); i++ )
p->pTruths[Mini_LutWordNum(p->LutSize) + i] = ~0;
return p;
}
static void Mini_LutStop( Mini_Lut_t * p )
{
MINI_LUT_FREE( p->pArray );
MINI_LUT_FREE( p->pTruths );
MINI_LUT_FREE( p );
}
static void Mini_LutPrintStats( Mini_Lut_t * p )
{
int i, nPis, nPos, nNodes;
nPis = 0;
Mini_LutForEachPi( p, i )
nPis++;
nPos = 0;
Mini_LutForEachPo( p, i )
nPos++;
nNodes = 0;
Mini_LutForEachNode( p, i )
nNodes++;
printf( "PI = %d. PO = %d. LUT = %d.\n", nPis, nPos, nNodes );
}
// serialization
static void Mini_LutDump( Mini_Lut_t * p, char * pFileName )
{
FILE * pFile;
int RetValue;
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file for writing \"%s\".\n", pFileName );
return;
}
RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile );
RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile );
RetValue = fwrite( &p->LutSize, sizeof(int), 1, pFile );
RetValue = fwrite( p->pArray, sizeof(int), p->nSize * p->LutSize, pFile );
RetValue = fwrite( p->pTruths, sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile );
fclose( pFile );
}
static Mini_Lut_t * Mini_LutLoad( char * pFileName )
{
Mini_Lut_t * p;
FILE * pFile;
int RetValue, nSize;
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Cannot open file for reading \"%s\".\n", pFileName );
return NULL;
}
RetValue = fread( &nSize, sizeof(int), 1, pFile );
p = MINI_LUT_CALLOC( Mini_Lut_t, 1 );
p->nSize = p->nCap = nSize;
RetValue = fread( &p->nRegs, sizeof(int), 1, pFile );
RetValue = fread( &p->LutSize, sizeof(int), 1, pFile );
p->pArray = MINI_LUT_ALLOC( int, p->nCap * p->LutSize );
p->pTruths = MINI_LUT_ALLOC( unsigned, p->nCap * Mini_LutWordNum(p->LutSize) );
RetValue = fread( p->pArray, sizeof(int), p->nCap * p->LutSize, pFile );
RetValue = fread( p->pTruths, sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile );
fclose( pFile );
return p;
}
// creating nodes
// (constant nodes are created when LUT manager is created)
static int Mini_LutCreatePi( Mini_Lut_t * p )
{
Mini_LutPush( p, 0, NULL, NULL );
return p->nSize - 1;
}
static int Mini_LutCreatePo( Mini_Lut_t * p, int Var0 )
{
assert( Var0 >= 0 && Var0 < p->nSize );
Mini_LutPush( p, 1, &Var0, NULL );
// mark PO by setting its 2nd fanin to the special number
p->pArray[p->LutSize*(p->nSize - 1)+1] = MINI_LUT_NULL2;
return p->nSize - 1;
}
// create LUT
static int Mini_LutCreateNode( Mini_Lut_t * p, int nVars, int * pVars, unsigned * pTruth )
{
assert( nVars >= 0 && nVars <= p->LutSize );
Mini_LutPush( p, nVars, pVars, pTruth );
return p->nSize - 1;
}
// procedure to check the topological order during AIG construction
static int Mini_LutCheck( Mini_Lut_t * p )
{
int status = 1;
int i, k, iFaninVar;
Mini_LutForEachNode( p, i )
{
for ( k = 0; k < p->LutSize; k++ )
{
iFaninVar = Mini_LutNodeFanin( p, i, k );
if ( iFaninVar == MINI_LUT_NULL )
continue;
if ( iFaninVar >= p->LutSize * i )
printf( "Fanin %d of LUT node %d is not in a topological order.\n", k, i ), status = 0;
}
}
Mini_LutForEachPo( p, i )
{
iFaninVar = Mini_LutNodeFanin( p, i, 0 );
if ( iFaninVar >= p->LutSize * i )
printf( "Fanin %d of PO node %d is not in a topological order.\n", k, i ), status = 0;
}
return status;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -55,6 +55,7 @@
#include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h"
#include "opt/sfm/sfm.h"
#include "opt/sbd/sbd.h"
#include "bool/rpo/rpo.h"
#include "map/mpm/mpm.h"
#include "opt/fret/fretime.h"
@ -134,7 +135,7 @@ static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFaultClasses ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -778,7 +780,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 );
@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
@ -6212,6 +6215,9 @@ usage:
Abc_Print( -2, "\t 3: disjoint-support decomposition with cofactoring\n" );
Abc_Print( -2, "\t 4: updated disjoint-support decomposition with cofactoring\n" );
Abc_Print( -2, "\t 5: enumerating decomposable variable sets\n" );
Abc_Print( -2, "\t 6: disjoint-support decomposition with cofactoring and boolean difference analysis\n" );
Abc_Print( -2, "\t from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,\n");
Abc_Print( -2, "\t \"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis,\" ICCD'15.\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -7235,23 +7241,33 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandFaultClasses( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose );
extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose );
extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt );
Abc_Ntk_t * pNtk;
int c, fSeq = 0, fVerbose = 0;
int c, fGen = 0, fStuckAt = 0, fSeq = 0, fVerbose = 0, fVeryVerbose = 0;
pNtk = Abc_FrameReadNtk(pAbc);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "gcsvwh" ) ) != EOF )
{
switch ( c )
{
case 'g':
fGen ^= 1;
break;
case 'c':
fStuckAt ^= 1;
break;
case 's':
fSeq ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -7268,14 +7284,25 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Only applicable to a logic network.\n" );
return 1;
}
Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose );
if ( fGen )
{
char * pFileName = Extra_FileNameGenericAppend(Abc_NtkSpec(pNtk), "_faults.txt");
Abc_NtkGenFaultList( pNtk, pFileName, fStuckAt );
}
else
Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose, fVeryVerbose );
return 0;
usage:
Abc_Print( -2, "usage: detect [-svh]\n" );
Abc_Print( -2, "\t detects properties of internal nodes\n" );
Abc_Print( -2, "\t-s : toggle using sequential circuit information [default = %s]\n", fSeq? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "usage: faultclasses [-gcsvwh]\n" );
Abc_Print( -2, "\t computes equivalence classes of faults in the given mapped netlist;\n" );
Abc_Print( -2, "\t the fault list with faults in the format: <fault_id> <node_name> <fault_name>\n" );
Abc_Print( -2, "\t should be read by command \"read_fins\" before calling this command\n" );
Abc_Print( -2, "\t-g : toggle generating a fault list for the current mapped network [default = %s]\n", fGen? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using only stuck-at faults in the generated fault list [default = %s]\n", fStuckAt? "yes": "no" );
Abc_Print( -2, "\t-s : toggle detecting sequential equivalence classes [default = %s]\n", fSeq? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout during computation [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing of resulting fault equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -7443,7 +7470,7 @@ usage:
Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" );
Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %s]\n", nStartGates );
Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %d]\n", nStartGates );
Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts; turn off with 0 [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
Abc_Print( -2, "\t-t : run test suite\n" );
@ -11840,7 +11867,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
//Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int nCutMax = 1;
int nLeafMax = 4;
int nDivMax = 2;
@ -12047,8 +12074,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// extern void Cba_PrsReadBlifTest();
// Cba_PrsReadBlifTest();
extern void Sfm_TimTest( Abc_Ntk_t * pNtk );
Sfm_TimTest( pNtk );
}
return 0;
usage:
@ -26971,12 +26996,13 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
char * FileName, * pTemp;
int c, nArgcNew;
int fUseMini = 0;
int fMiniAig = 0;
int fMiniLut = 0;
int fVerbose = 0;
int fGiaSimple = 0;
int fSkipStrash = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "csmlvh" ) ) != EOF )
{
switch ( c )
{
@ -26987,7 +27013,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
fSkipStrash ^= 1;
break;
case 'm':
fUseMini ^= 1;
fMiniAig ^= 1;
break;
case 'l':
fMiniLut ^= 1;
break;
case 'v':
fVerbose ^= 1;
@ -27020,8 +27049,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
fclose( pFile );
if ( fUseMini )
if ( fMiniAig )
pAig = Gia_ManReadMiniAig( FileName );
else if ( fMiniLut )
pAig = Gia_ManReadMiniLut( FileName );
// else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
// Abc3_ReadShowHie( FileName, fSkipStrash );
else
@ -27031,11 +27062,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &r [-csmvh] <file>\n" );
Abc_Print( -2, "usage: &r [-csmlvh] <file>\n" );
Abc_Print( -2, "\t reads the current AIG from the AIGER file\n" );
Abc_Print( -2, "\t-c : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-s : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fMiniAig? "yes": "no" );
Abc_Print( -2, "\t-l : toggles reading MiniLUT rather than AIGER file [default = %s]\n", fMiniLut? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n");
@ -27616,6 +27648,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
*pnBestLuts = nCurLuts;
*pnBestEdges = nCurEdges;
*pnBestLevels = nCurLevels;
//printf( "\nUpdating best (%d %d %d).\n\n", nCurLuts, nCurEdges, nCurLevels );
return 1;
}
return 0;
@ -27815,9 +27848,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUnique = 0;
int fMiniAig = 0;
int fMiniLut = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "umvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "umlvh" ) ) != EOF )
{
switch ( c )
{
@ -27827,6 +27861,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMiniAig ^= 1;
break;
case 'l':
fMiniLut ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -27857,15 +27894,18 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else if ( fMiniAig )
Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
else if ( fMiniLut )
Gia_ManWriteMiniLut( pAbc->pGia, pFileName );
else
Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
return 0;
usage:
Abc_Print( -2, "usage: &w [-umvh] <file>\n" );
Abc_Print( -2, "usage: &w [-umlvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n");
@ -28193,9 +28233,10 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Gia_ManMuxProfiling( Gia_Man_t * p );
extern void Gia_ManProfileStructures( Gia_Man_t * p, int nLimit, int fVerbose );
extern void Acec_StatsCollect( Gia_Man_t * p, int fVerbose );
int c, fNpn = 0, fMuxes = 0, nLimit = 0, fVerbose = 0;
extern void Acec_ManProfile( Gia_Man_t * p, int fVerbose );
int c, fNpn = 0, fMuxes = 0, fAdders = 0, nLimit = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmavh" ) ) != EOF )
{
switch ( c )
{
@ -28216,6 +28257,9 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMuxes ^= 1;
break;
case 'a':
fAdders ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -28241,16 +28285,19 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else if ( fMuxes )
Gia_ManMuxProfiling( pAbc->pGia );
else if ( fAdders )
Acec_ManProfile( pAbc->pGia, fVerbose );
else
Gia_ManProfileStructures( pAbc->pGia, nLimit, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &profile [-N num] [-nmvh]\n" );
Abc_Print( -2, "usage: &profile [-N num] [-nmavh]\n" );
Abc_Print( -2, "\t profile gate structures appearing in the AIG\n" );
Abc_Print( -2, "\t-N num : limit on class size to show [default = %d]\n", nLimit );
Abc_Print( -2, "\t-n : toggle profiling NPN-classes (for 3-LUT mapped AIGs) [default = %s]\n", fNpn? "yes": "no" );
Abc_Print( -2, "\t-m : toggle profiling MUX structures [default = %s]\n", fMuxes? "yes": "no" );
Abc_Print( -2, "\t-a : toggle profiling adder structures [default = %s]\n", fAdders? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -30989,7 +31036,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -40800,6 +40847,136 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars );
Gia_Man_t * pTemp; int c;
Sbd_Par_t Pars, * pPars = &Pars;
Sbd_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
pPars->nLutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLutSize < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTfoLevels = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTfoLevels < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTfoFanMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTfoFanMax < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinSizeMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'c':
pPars->fCover ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManBufNum(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
return 1;
}
if ( Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
return 0;
}
pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" );
Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax );
Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-c : toggle using complete slow covering procedure [default = %s]\n", pPars->fCover? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

22
src/base/abci/abcDec.c
View File

@ -26,6 +26,7 @@
#include "bool/kit/kit.h"
#include "opt/dau/dau.h"
#include "misc/util/utilTruth.h"
#include "opt/dsc/dsc.h"
ABC_NAMESPACE_IMPL_START
@ -484,6 +485,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
pAlgoName = "fast DSD";
else if ( DecType == 5 )
pAlgoName = "analysis";
else if ( DecType == 6 )
pAlgoName = "DSD ICCD'15";
if ( pAlgoName )
printf( "Applying %-10s to %8d func%s of %2d vars... ",
@ -577,6 +580,23 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
if ( fVerbose )
printf( "\n" );
}
} else if ( DecType == 6 )
{
char pDsd[DSC_MAX_STR];
/* memory pool with a capacity of storing 3*nVars
truth-tables for negative and positive cofactors and
the boolean difference for each input variable */
word *mem_pool = Dsc_alloc_pool(p->nVars);
for ( i = 0; i < p->nFuncs; i++ )
{
if ( fVerbose )
printf( "%7d : ", i );
Dsc_Decompose(p->pFuncs[i], p->nVars, pDsd, mem_pool);
if ( fVerbose )
printf( "%s\n", pDsd[0] ? pDsd : "NULL");
nNodes += Dsc_CountAnds( pDsd );
}
Dsc_free_pool(mem_pool);
}
else assert( 0 );
@ -629,7 +649,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
if ( DecType == 0 )
{ if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); }
else if ( DecType >= 1 && DecType <= 5 )
else if ( DecType >= 1 && DecType <= 6 )
Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose );
else
printf( "Unknown decomposition type value (%d).\n", DecType );

1067
src/base/abci/abcDetect.c
View File

File diff suppressed because it is too large Load Diff

111
src/base/cba/cba.h
View File

@ -29,6 +29,7 @@
#include "misc/extra/extra.h"
#include "misc/util/utilNam.h"
#include "misc/vec/vecHash.h"
#include "cbaTypes.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -40,116 +41,6 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// network objects
typedef enum {
CBA_OBJ_NONE = 0, // 00: unused
CBA_OBJ_PI, // 01: input
CBA_OBJ_PO, // 02: output
CBA_OBJ_BOX, // 03: box
CBA_BOX_CF, // 04:
CBA_BOX_CT, // 05:
CBA_BOX_CX, // 06:
CBA_BOX_CZ, // 07:
CBA_BOX_BUF, // 08:
CBA_BOX_INV, // 09:
CBA_BOX_AND, // 10:
CBA_BOX_NAND, // 11:
CBA_BOX_OR, // 12:
CBA_BOX_NOR, // 13:
CBA_BOX_XOR, // 14:
CBA_BOX_XNOR, // 15:
CBA_BOX_SHARP, // 16:
CBA_BOX_SHARPL, // 17:
CBA_BOX_MUX, // 18:
CBA_BOX_MAJ, // 19:
CBA_BOX_ABC, // 20:
CBA_BOX_BA, // 21:
CBA_BOX_BO, // 22:
CBA_BOX_BX, // 23:
CBA_BOX_BN, // 24:
CBA_BOX_BAO, // 25:
CBA_BOX_BOA, // 26:
CBA_BOX_RAND, // 27:
CBA_BOX_RNAND, // 28:
CBA_BOX_ROR, // 29:
CBA_BOX_RNOR, // 30:
CBA_BOX_RXOR, // 31:
CBA_BOX_RXNOR, // 32:
CBA_BOX_LNOT, // 33
CBA_BOX_LAND, // 34:
CBA_BOX_LNAND, // 35:
CBA_BOX_LOR, // 36:
CBA_BOX_LNOR, // 37:
CBA_BOX_LXOR, // 38:
CBA_BOX_LXNOR, // 39:
CBA_BOX_NMUX, // 40:
CBA_BOX_SEL, // 41:
CBA_BOX_PSEL, // 42:
CBA_BOX_ENC, // 43:
CBA_BOX_PENC, // 44:
CBA_BOX_DEC, // 45:
CBA_BOX_EDEC, // 46:
CBA_BOX_ADD, // 47:
CBA_BOX_SUB, // 48:
CBA_BOX_MUL, // 49:
CBA_BOX_SMUL, // 50:
CBA_BOX_DIV, // 51:
CBA_BOX_MOD, // 52:
CBA_BOX_REM, // 53:
CBA_BOX_POW, // 54:
CBA_BOX_MIN, // 55:
CBA_BOX_SQRT, // 56:
CBA_BOX_ABS, // 57:
CBA_BOX_SLTHAN, // 58:
CBA_BOX_LTHAN, // 59:
CBA_BOX_LETHAN, // 60:
CBA_BOX_METHAN, // 61:
CBA_BOX_MTHAN, // 62:
CBA_BOX_EQU, // 63:
CBA_BOX_NEQU, // 64:
CBA_BOX_SHIL, // 65:
CBA_BOX_SHIR, // 66:
CBA_BOX_SHILA, // 67:
CBA_BOX_SHIRA, // 68:
CBA_BOX_ROTL, // 69:
CBA_BOX_ROTR, // 70:
CBA_BOX_NODE, // 71:
CBA_BOX_LUT, // 72:
CBA_BOX_GATE, // 73:
CBA_BOX_TABLE, // 74:
CBA_BOX_TRI, // 75:
CBA_BOX_RAM, // 76:
CBA_BOX_RAMR, // 77:
CBA_BOX_RAMW, // 78:
CBA_BOX_RAMWC, // 79:
CBA_BOX_RAML, // 80:
CBA_BOX_RAMS, // 81:
CBA_BOX_RAMBOX, // 82:
CBA_BOX_LATCH, // 83:
CBA_BOX_LATCHRS, // 84:
CBA_BOX_DFF, // 85:
CBA_BOX_DFFCPL, // 86:
CBA_BOX_DFFRS, // 87:
CBA_BOX_SLICE, // 88:
CBA_BOX_CONCAT, // 89:
CBA_BOX_LAST // 90
} Cba_ObjType_t;
typedef struct Cba_Ntk_t_ Cba_Ntk_t;
typedef struct Cba_Man_t_ Cba_Man_t;

169
src/base/cba/cbaTypes.h Normal file
View File

@ -0,0 +1,169 @@
/**CFile****************************************************************
FileName [cbaTypes.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Hierarchical word-level netlist.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 21, 2015.]
Revision [$Id: cbaTypes.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__base__cba__cba__types_h
#define ABC__base__cba__cba__types_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// network objects
typedef enum {
CBA_OBJ_NONE = 0, // 00: unused
CBA_OBJ_PI, // 01: input
CBA_OBJ_PO, // 02: output
CBA_OBJ_BOX, // 03: box
CBA_BOX_CF, // 04:
CBA_BOX_CT, // 05:
CBA_BOX_CX, // 06:
CBA_BOX_CZ, // 07:
CBA_BOX_BUF, // 08:
CBA_BOX_INV, // 09:
CBA_BOX_AND, // 10:
CBA_BOX_NAND, // 11:
CBA_BOX_OR, // 12:
CBA_BOX_NOR, // 13:
CBA_BOX_XOR, // 14:
CBA_BOX_XNOR, // 15:
CBA_BOX_SHARP, // 16:
CBA_BOX_SHARPL, // 17:
CBA_BOX_MUX, // 18:
CBA_BOX_MAJ, // 19:
CBA_BOX_ABC, // 20:
CBA_BOX_BA, // 21:
CBA_BOX_BO, // 22:
CBA_BOX_BX, // 23:
CBA_BOX_BN, // 24:
CBA_BOX_BAO, // 25:
CBA_BOX_BOA, // 26:
CBA_BOX_RAND, // 27:
CBA_BOX_RNAND, // 28:
CBA_BOX_ROR, // 29:
CBA_BOX_RNOR, // 30:
CBA_BOX_RXOR, // 31:
CBA_BOX_RXNOR, // 32:
CBA_BOX_LNOT, // 33
CBA_BOX_LAND, // 34:
CBA_BOX_LNAND, // 35:
CBA_BOX_LOR, // 36:
CBA_BOX_LNOR, // 37:
CBA_BOX_LXOR, // 38:
CBA_BOX_LXNOR, // 39:
CBA_BOX_NMUX, // 40:
CBA_BOX_SEL, // 41:
CBA_BOX_PSEL, // 42:
CBA_BOX_ENC, // 43:
CBA_BOX_PENC, // 44:
CBA_BOX_DEC, // 45:
CBA_BOX_EDEC, // 46:
CBA_BOX_ADD, // 47:
CBA_BOX_SUB, // 48:
CBA_BOX_MUL, // 49:
CBA_BOX_SMUL, // 50:
CBA_BOX_DIV, // 51:
CBA_BOX_MOD, // 52:
CBA_BOX_REM, // 53:
CBA_BOX_POW, // 54:
CBA_BOX_MIN, // 55:
CBA_BOX_SQRT, // 56:
CBA_BOX_ABS, // 57:
CBA_BOX_SLTHAN, // 58:
CBA_BOX_LTHAN, // 59:
CBA_BOX_LETHAN, // 60:
CBA_BOX_METHAN, // 61:
CBA_BOX_MTHAN, // 62:
CBA_BOX_EQU, // 63:
CBA_BOX_NEQU, // 64:
CBA_BOX_SHIL, // 65:
CBA_BOX_SHIR, // 66:
CBA_BOX_SHILA, // 67:
CBA_BOX_SHIRA, // 68:
CBA_BOX_ROTL, // 69:
CBA_BOX_ROTR, // 70:
CBA_BOX_NODE, // 71:
CBA_BOX_LUT, // 72:
CBA_BOX_GATE, // 73:
CBA_BOX_TABLE, // 74:
CBA_BOX_TRI, // 75:
CBA_BOX_RAM, // 76:
CBA_BOX_RAMR, // 77:
CBA_BOX_RAMW, // 78:
CBA_BOX_RAMWC, // 79:
CBA_BOX_RAML, // 80:
CBA_BOX_RAMS, // 81:
CBA_BOX_RAMBOX, // 82:
CBA_BOX_LATCH, // 83:
CBA_BOX_LATCHRS, // 84:
CBA_BOX_DFF, // 85:
CBA_BOX_DFFCPL, // 86:
CBA_BOX_DFFRS, // 87:
CBA_BOX_SLICE, // 88:
CBA_BOX_CONCAT, // 89:
CBA_BOX_LAST // 90
} Cba_ObjType_t;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

3
src/base/io/io.c
View File

@ -2378,6 +2378,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_Obj_t * pObj;
FILE * pFile;
int i, f;
/*
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
@ -2385,7 +2386,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
return 1;
}
*/
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{

2
src/base/io/ioWriteDot.c
View File

@ -74,7 +74,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
Abc_Obj_t * pNode, * pFanin;
char * pSopString;
int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
int Limit = 300;
int Limit = 500;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );

1
src/base/wlc/module.make
View File

@ -8,4 +8,5 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcReadVer.c \
src/base/wlc/wlcSim.c \
src/base/wlc/wlcStdin.c \
src/base/wlc/wlcWin.c \
src/base/wlc/wlcWriteVer.c

6
src/base/wlc/wlc.h
View File

@ -244,6 +244,8 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
#define Wlc_ObjForEachFanin( pObj, iFanin, i ) \
for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )
#define Wlc_ObjForEachFaninObj( p, pObj, pFanin, i ) \
for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((pFanin) = Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, i))), 1); i++ )
#define Wlc_ObjForEachFaninReverse( pObj, iFanin, i ) \
for ( i = Wlc_ObjFaninNum(pObj) - 1; (i >= 0) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i-- )
@ -272,6 +274,8 @@ extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
extern void Wlc_NtkFree( Wlc_Ntk_t * p );
extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p );
@ -287,6 +291,8 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
/*=== wlcReadVer.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
/*=== wlcWin.c =============================================================*/
extern void Wlc_WinProfileArith( Wlc_Ntk_t * p );
/*=== wlcWriteVer.c ========================================================*/
extern void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops );

11
src/base/wlc/wlcBlast.c
View File

@ -292,6 +292,10 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
{
int fUseXor = 0;
int fCompl = (a == 1 || b == 1 || c == 1);
// propagate complement through the FA - helps generate less redundant logic
if ( fCompl )
a = Abc_LitNot(a), b = Abc_LitNot(b), c = Abc_LitNot(c);
if ( fUseXor )
{
int Xor = Gia_ManHashXor(pNew, a, b);
@ -310,6 +314,8 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
*ps = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
*pc = Gia_ManHashOr (pNew, And1, And2);
}
if ( fCompl )
*ps = Abc_LitNot(*ps), *pc = Abc_LitNot(*pc);
}
void Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
{
@ -412,6 +418,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
assert( fSigned == 0 || fSigned == 1 );
// prepare result
Vec_IntFill( vRes, nArgA + nArgB, 0 );
//Vec_IntFill( vRes, nArgA + nArgB + 1, 0 );
pRes = Vec_IntArray( vRes );
// prepare intermediate storage
Vec_IntFill( vTemp, 2 * nArgA, 0 );
@ -426,6 +433,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
pArgS[nArgA-1] = fSigned;
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
//Vec_IntWriteEntry( vRes, nArgA + nArgB, Carry );
}
void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
{
@ -804,7 +812,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
Vec_WecPush( vLevels, k, 0 );
}
//Vec_WecPrint( vProds, 0 );
//printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
Vec_WecFree( vProds );
@ -1360,6 +1368,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManDupRemapLiterals( vBits, pTemp );
//printf( "Cutoff ID %d became %d.\n", 75, Abc_Lit2Var(Gia_ManObj(pTemp, 73)->Value) );
Gia_ManStop( pTemp );
}
// transform AIG with init state

48
src/base/wlc/wlcCom.c
View File

@ -34,6 +34,7 @@ static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
@ -67,6 +68,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
}
@ -543,6 +545,50 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
return 0;
}
Wlc_WinProfileArith( pNtk );
return 0;
usage:
Abc_Print( -2, "usage: %%profile [-vh]\n" );
Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis []
@ -575,7 +621,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pNtk == NULL )
{
Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
return 0;
}
// transform

73
src/base/wlc/wlcNtk.c
View File

@ -44,8 +44,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
">>>", // 10: shift right (arithmetic)
"<<", // 11: shift left
"<<<", // 12: shift left (arithmetic)
"rotateR", // 13: rotate right
"rotateL", // 14: rotate left
"rotR", // 13: rotate right
"rotL", // 14: rotate left
"~", // 15: bitwise NOT
"&", // 16: bitwise AND
"|", // 17: bitwise OR
@ -55,8 +55,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"~^", // 21: bitwise NXOR
"[:]", // 22: bit selection
"{,}", // 23: bit concatenation
"zeroPad", // 24: zero padding
"signExt", // 25: sign extension
"zPad", // 24: zero padding
"sExt", // 25: sign extension
"!", // 26: logic NOT
"=>", // 27: logic implication
"&&", // 28: logic AND
@ -83,7 +83,7 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"**", // 49: arithmetic power
"-", // 50: arithmetic minus
"sqrt", // 51: integer square root
"square", // 52: integer square
"squar", // 52: integer square
"table", // 53: bit table
NULL // 54: unused
};
@ -471,6 +471,57 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
Vec_VecFree( (Vec_Vec_t *)vOccurs );
Vec_IntFree( vAnds );
}
void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
{
printf( "%8d : ", Wlc_ObjId(p, pObj) );
printf( "%3d%s", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
if ( pObj->Type == WLC_OBJ_CONST )
printf( " " );
else
{
printf( " = %3d%s %5s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] );
if ( Wlc_ObjFaninNum(pObj) > 1 )
printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
else
printf( " " );
if ( Wlc_ObjFaninNum(pObj) > 2 )
printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " );
else
printf( " " );
}
printf( " : " );
printf( "%-12s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
if ( pObj->Type == WLC_OBJ_CONST )
{
printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
if ( pObj->fXConst )
{
int k;
for ( k = 0; k < (Wlc_ObjRange(pObj) + 3) / 4; k++ )
printf( "x" );
}
else
Abc_TtPrintHexArrayRev( stdout, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
}
else
{
printf( " = %-12s %5s ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[(int)pObj->Type] );
if ( Wlc_ObjFaninNum(pObj) > 1 )
printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
else
printf( " " );
if ( Wlc_ObjFaninNum(pObj) > 2 )
printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)) );
}
printf( "\n" );
}
void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray )
{
Wlc_Obj_t * pObj;
int i;
Wlc_NtkForEachObjVec( vArray, p, pObj, i )
Wlc_NtkPrintNode( p, pObj );
}
void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
{
Wlc_Obj_t * pObj;
@ -480,16 +531,8 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
{
if ( (int)pObj->Type != Type )
continue;
printf( "%8d :", Counter++ );
printf( "%8d : ", i );
printf( "%3d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
printf( "%3d%s %s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[Type] );
printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
printf( " : " );
printf( "%-12s = ", Wlc_ObjName(p, i) );
printf( "%-12s %s ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[Type] );
printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
printf( "\n" );
printf( "%8d :", Counter++ );
Wlc_NtkPrintNode( p, pObj );
}
}
void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )

166
src/base/wlc/wlcWin.c Normal file
View File

@ -0,0 +1,166 @@
/**CFile****************************************************************
FileName [wlcWin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Parses several flavors of word-level Verilog.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 22, 2014.]
Revision [$Id: wlcWin.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
***********************************************************************/
#include "wlc.h"
#include "base/abc/abc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collect arithmetic nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Wlc_ObjIsArithm( Wlc_Obj_t * pObj )
{
return pObj->Type == WLC_OBJ_CONST ||
pObj->Type == WLC_OBJ_BUF || pObj->Type == WLC_OBJ_BIT_NOT ||
pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT ||
// pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_BIT_CONCAT ||
pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
}
int Wlc_ObjIsArithmReal( Wlc_Obj_t * pObj )
{
return pObj->Type == WLC_OBJ_BIT_NOT ||
pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
}
int Wlc_ManCountArithmReal( Wlc_Ntk_t * p, Vec_Int_t * vNodes )
{
Wlc_Obj_t * pObj;
int i, Counter = 0;
Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
Counter += Wlc_ObjIsArithmReal( pObj );
return Counter;
}
int Wlc_ObjHasArithm_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
{
if ( pObj->Type == WLC_OBJ_CONST )
return 0;
if ( pObj->Type == WLC_OBJ_BUF || pObj->Type == WLC_OBJ_BIT_NOT ||
pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
return Wlc_ObjHasArithm_rec( p, Wlc_ObjFanin0(p, pObj) );
return pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
}
int Wlc_ObjHasArithmFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
{
Wlc_Obj_t * pFanin; int i;
assert( !Wlc_ObjHasArithm_rec(p, pObj) );
Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
if ( Wlc_ObjHasArithm_rec(p, pFanin) )
return 1;
return 0;
}
void Wlc_WinCompute_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
Wlc_Obj_t * pFanin; int i;
if ( pObj->Mark )
return;
pObj->Mark = 1;
if ( !Wlc_ObjIsArithm(pObj) )
{
Vec_IntPush( vLeaves, Wlc_ObjId(p, pObj) );
return;
}
Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
Wlc_WinCompute_rec( p, pFanin, vLeaves, vNodes );
Vec_IntPush( vNodes, Wlc_ObjId(p, pObj) );
}
void Wlc_WinCleanMark_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
{
Wlc_Obj_t * pFanin; int i;
if ( !pObj->Mark )
return;
pObj->Mark = 0;
Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
Wlc_WinCleanMark_rec( p, pFanin );
}
void Wlc_WinCompute( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
Vec_IntClear( vLeaves );
Vec_IntClear( vNodes );
if ( Wlc_ObjHasArithm_rec(p, pObj) )
{
Wlc_WinCompute_rec( p, pObj, vLeaves, vNodes );
Wlc_WinCleanMark_rec( p, pObj );
}
else if ( Wlc_ObjHasArithmFanins(p, pObj) )
{
Wlc_Obj_t * pFanin; int i;
Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
if ( Wlc_ObjHasArithm_rec(p, pFanin) )
Wlc_WinCompute_rec( p, pFanin, vLeaves, vNodes );
Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
if ( Wlc_ObjHasArithm_rec(p, pFanin) )
Wlc_WinCleanMark_rec( p, pFanin );
}
else assert( 0 );
}
void Wlc_WinProfileArith( Wlc_Ntk_t * p )
{
Vec_Int_t * vLeaves = Vec_IntAlloc( 1000 );
Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
Wlc_Obj_t * pObj; int i, Count = 0;
Wlc_NtkForEachObj( p, pObj, i )
pObj->Mark = 0;
Wlc_NtkForEachObj( p, pObj, i )
if ( Wlc_ObjHasArithm_rec(p, pObj) ? Wlc_ObjIsCo(pObj) : Wlc_ObjHasArithmFanins(p, pObj) )
{
Wlc_WinCompute( p, pObj, vLeaves, vNodes );
if ( Wlc_ManCountArithmReal(p, vNodes) < 2 )
continue;
printf( "Arithmetic cone of node %d (%s):\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
Wlc_NtkPrintNode( p, pObj );
Vec_IntReverseOrder( vNodes );
Wlc_NtkPrintNodeArray( p, vNodes );
printf( "\n" );
Count++;
}
Wlc_NtkForEachObj( p, pObj, i )
assert( pObj->Mark == 0 );
printf( "Finished printing %d arithmetic cones.\n", Count );
Vec_IntFree( vLeaves );
Vec_IntFree( vNodes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/map/mio/mio.h
View File

@ -112,6 +112,7 @@ extern char * Mio_LibraryReadName ( Mio_Library_t * pLib );
extern int Mio_LibraryReadGateNum ( Mio_Library_t * pLib );
extern Mio_Gate_t * Mio_LibraryReadGates ( Mio_Library_t * pLib );
extern Mio_Gate_t ** Mio_LibraryReadGateArray ( Mio_Library_t * pLib );
extern Mio_Gate_t * Mio_LibraryReadGateById ( Mio_Library_t * pLib, int iD );
extern Mio_Gate_t * Mio_LibraryReadGateByName ( Mio_Library_t * pLib, char * pName, char * pOutName );
extern char * Mio_LibraryReadSopByName ( Mio_Library_t * pLib, char * pName );
extern Mio_Gate_t * Mio_LibraryReadGateByTruth( Mio_Library_t * pLib, word t );

1
src/map/mio/mioApi.c
View File

@ -44,6 +44,7 @@ char * Mio_LibraryReadName ( Mio_Library_t * pLib ) { retur
int Mio_LibraryReadGateNum ( Mio_Library_t * pLib ) { return pLib->nGates; }
Mio_Gate_t * Mio_LibraryReadGates ( Mio_Library_t * pLib ) { return pLib->pGates; }
Mio_Gate_t ** Mio_LibraryReadGateArray ( Mio_Library_t * pLib ) { return pLib->ppGatesName;}
Mio_Gate_t * Mio_LibraryReadGateById ( Mio_Library_t * pLib, int Id ) { assert( pLib->ppGates0[Id]->Cell == Id ); return pLib->ppGates0[Id];}
Mio_Gate_t * Mio_LibraryReadBuf ( Mio_Library_t * pLib ) { return pLib->pGateBuf; }
Mio_Gate_t * Mio_LibraryReadInv ( Mio_Library_t * pLib ) { return pLib->pGateInv; }
Mio_Gate_t * Mio_LibraryReadConst0 ( Mio_Library_t * pLib ) { return pLib->pGate0; }

3
src/map/mio/mioRead.c
View File

@ -586,7 +586,10 @@ void Mio_LibrarySortGates( Mio_Library_t * pLib )
int i = 0;
ppGates = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
Mio_LibraryForEachGate( pLib, pGate )
{
pGate->Cell = i;
ppGates[i++] = pGate;
}
assert( i == pLib->nGates );
// sort gates by name
pLib->ppGates0 = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );

4
src/map/scl/sclLiberty.c
View File

@ -1614,10 +1614,14 @@ Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbos
Vec_Flt_t * vArray;
assert( Vec_PtrSize(vTemples) % 4 == 0 );
Vec_PtrForEachEntry( Vec_Flt_t *, vTemples, vArray, i )
{
if ( vArray == NULL )
continue;
if ( i % 4 == 0 )
ABC_FREE( vArray );
else if ( i % 4 == 2 || i % 4 == 3 )
Vec_FltFree( vArray );
}
Vec_PtrFree( vTemples );
}
if ( fVerbose )

36
src/misc/util/utilTruth.h
View File

@ -266,6 +266,28 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] & pIn2[w];
}
static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords )
{
int w;
if ( fCompl1 )
{
if ( fCompl2 )
for ( w = 0; w < nWords; w++ )
pOut[w] = ~pIn1[w] & ~pIn2[w];
else
for ( w = 0; w < nWords; w++ )
pOut[w] = ~pIn1[w] & pIn2[w];
}
else
{
if ( fCompl2 )
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] & ~pIn2[w];
else
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] & pIn2[w];
}
}
static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
{
int w;
@ -288,6 +310,12 @@ static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] | pIn2[w];
}
static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords )
{
int w;
for ( w = 0; w < nWords; w++ )
pOut[w] |= pIn1[w] ^ pIn2[w];
}
static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
{
int w;
@ -1603,6 +1631,14 @@ static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
return 64*w + Abc_Tt6FirstBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
for ( w = 0; w < nWords; w++ )
if ( pIn1[w] ^ pIn2[w] )
return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);

50
src/opt/dau/dauGia.c
View File

@ -238,12 +238,28 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
assert( nFans > 1 );
iFan0 = pFans[--nFans];
iFan1 = pFans[--nFans];
if ( fAnd )
iFan = Gia_ManHashAnd( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
iFan = Gia_ManHashXorReal( pGia, iFan0, iFan1 );
else
iFan = Gia_ManHashXor( pGia, iFan0, iFan1 );
if ( pGia->pHTable == NULL )
{
if ( fAnd )
iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
{
int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
iFan = Gia_ManAppendXorReal( pGia, Abc_LitRegular(iFan0), Abc_LitRegular(iFan1) );
iFan = Abc_LitNotCond( iFan, fCompl );
}
else
iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
}
else
{
if ( fAnd )
iFan = Gia_ManHashAnd( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
iFan = Gia_ManHashXorReal( pGia, iFan0, iFan1 );
else
iFan = Gia_ManHashXor( pGia, iFan0, iFan1 );
}
pObj = Gia_ManObj(pGia, Abc_Lit2Var(iFan));
if ( Gia_ObjIsAnd(pObj) )
{
@ -340,14 +356,24 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
assert( **p == '{' && *q == '}' );
*p = q;
}
if ( pGia->pMuxes )
Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
if ( pGia->pHTable == NULL )
{
if ( pGia->pMuxes )
Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
else
Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
}
else
Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
{
if ( pGia->pMuxes )
Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
else
Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
}
pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
if ( Gia_ObjIsAnd(pObj) )
{
if ( pGia->pMuxes )
if ( pGia->pMuxes && pGia->pHTable != NULL )
Gia_ObjSetMuxLevel( pGia, pObj );
else
{
@ -377,7 +403,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
vLeaves.nSize = nVars;
vLeaves.pArray = Fanins;
nObjOld = Gia_ManObjNum(pGia);
Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, 1 );
Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, pGia->pHTable != NULL );
// assert( nVars <= 6 );
// Res = Dau_DsdToGiaCompose_rec( pGia, pFunc[0], Fanins, nVars );
for ( i = nObjOld; i < Gia_ManObjNum(pGia); i++ )
@ -434,7 +460,7 @@ int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t *
if ( nSizeNonDec )
m_NonDsd++;
// printf( "%s\n", pDsd );
if ( fDelayBalance )
if ( fDelayBalance && pGia->vLevels )
return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
else
return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );

525
src/opt/dsc/dsc.c Normal file
View File

@ -0,0 +1,525 @@
/**CFile****************************************************************
FileName [dsc.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Disjoint support decomposition - ICCD'15]
Synopsis [Disjoint-support decomposition with cofactoring and boolean difference analysis
from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
Author [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
Date [Ver. 1.0. Started - October 24, 2014.]
Revision [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
***********************************************************************/
#include "dsc.h"
#include <assert.h>
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*
This code performs truth-table-based decomposition for 6-variable functions.
Representation of operations:
! = not;
(ab) = a and b;
[ab] = a xor b;
*/
typedef struct Dsc_node_t_ Dsc_node_t;
struct Dsc_node_t_
{
word *pNegCof;
word *pPosCof;
word *pBoolDiff;
unsigned int on[DSC_MAX_VAR+1]; // pos cofactor spec - first element denotes the size of the array
unsigned int off[DSC_MAX_VAR+1]; // neg cofactor spec - first element denotes the size of the array
char exp[DSC_MAX_STR];
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
inline void xorInPlace( word * pOut, word * pIn2, int nWords)
{
int w;
for ( w = 0; w < nWords; w++ )
pOut[w] ^= pIn2[w];
}
void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
int i;
printf("Node:\t%s\n",pNode->exp);
printf("\tneg cof:\t");Abc_TtPrintHexRev(stdout, pNode->pNegCof, nVars);
printf("\tpos cof:\t");Abc_TtPrintHexRev(stdout, pNode->pPosCof, nVars);
printf("\tbool diff:\t");Abc_TtPrintHexRev(stdout, pNode->pBoolDiff, nVars);
printf("\toff:\t");
for (i=1;i<=(int)pNode->off[0];i++) {
printf("%c%c", (pNode->off[i] & 1U) ? ' ' : '!', 'a'+(pNode->off[i] >> 1));
}
printf("\ton:\t");
for (i=1;i<=(int)pNode->on[0];i++) {
printf("%c%c", (pNode->on[i] & 1U) ? ' ' : '!', 'a'+(pNode->on[i] >> 1));
}
printf("\n");
}
inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, int* ci, int* cj) {
if (Abc_TtEqual(ni->pNegCof, nj->pNegCof, TRUTH_WORDS)) {*ci=1; *cj=1; return 1;}
else if (Abc_TtEqual(ni->pNegCof, nj->pPosCof, TRUTH_WORDS)) {*ci=1; *cj=0; return 1;}
else if (Abc_TtEqual(ni->pPosCof, nj->pNegCof, TRUTH_WORDS)) {*ci=0; *cj=1; return 1;}
else if (Abc_TtEqual(ni->pPosCof, nj->pPosCof, TRUTH_WORDS)) {*ci=0; *cj=0; return 1;}
return 0;
}
inline int dsc_xor_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS) {
return Abc_TtEqual(ni->pBoolDiff, nj->pBoolDiff, TRUTH_WORDS);
}
void concat(char* target, char begin, char end, char* s1, int s1Polarity, char* s2, int s2Polarity) {
*target++ = begin;
//s1
if (!s1Polarity)
*target++ = '!';
while (*s1 != '\0')
*target++ = *s1++;
// s2
if (!s2Polarity)
*target++ = '!';
while (*s2 != '\0')
*target++ = *s2++;
// end
*target++ = end;
*target = '\0';
}
void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const int TRUTH_WORDS) {
int size = cubeCof[0];
int i;
for (i = 1; i <= size; i++) {
unsigned int c = cubeCof[i];
if (c & 1U) {
Abc_TtCofactor1(pTruth, TRUTH_WORDS, c >> 1);
} else {
Abc_TtCofactor0(pTruth, TRUTH_WORDS, c >> 1);
}
}
}
void merge(unsigned int * const pOut, const unsigned int * const pIn) {
const int elementsToCopy = pIn[0];
int i, j;
for (i = pOut[0]+1, j = 1; j <= elementsToCopy; i++, j++) {
pOut[i] = pIn[j];
}
pOut[0] += elementsToCopy;
}
void dsc_and_group(Dsc_node_t * pOut, Dsc_node_t * ni, int niPolarity, Dsc_node_t * nj, int njPolarity, int nVars, const int TRUTH_WORDS) {
unsigned int* xiOFF, * xiON, * xjOFF, * xjON;
// expression
concat(pOut->exp, '(', ')', ni->exp, niPolarity, nj->exp, njPolarity);
// ON-OFF
if (niPolarity) {
xiOFF = ni->off;
xiON = ni->on;
} else {
xiOFF = ni->on;
xiON = ni->off;
}
if (njPolarity) {
xjOFF = nj->off;
xjON = nj->on;
} else {
xjOFF = nj->on;
xjON = nj->off;
}
// creating both the new OFF specification and negative cofactor of the new group
{
// first element of the array represents the size of the cube-cofactor
int xiOFFSize = xiOFF[0];
int xjOFFSize = xjOFF[0];
if (xiOFFSize <= xjOFFSize) {
int i;
pOut->off[0] = xiOFFSize; // set the number of elements
for (i = 1; i <= xiOFFSize; i++) {
pOut->off[i] = xiOFF[i];
}
} else {
int i;
pOut->off[0] = xjOFFSize; // set the number of elements
for (i = 1; i <= xjOFFSize; i++) {
pOut->off[i] = xjOFF[i];
}
}
// set the negative cofactor of the new group
pOut->pNegCof = niPolarity ? ni->pNegCof : ni->pPosCof;
}
// creating both new ON specification and positive cofactor of the new group
{
int i;
int j;
unsigned int xiONSize = xiON[0];
unsigned int xjONSize = xjON[0];
pOut->on[0] = xiONSize + xjONSize;
for (i = 1; i <= (int)xiONSize; i++) {
pOut->on[i] = xiON[i];
}
for (j = 1; j <= (int)xjONSize; j++) {
pOut->on[i++] = xjON[j];
}
// set the positive cofactor of the new group
if (xiONSize >= xjONSize) {
pOut->pPosCof = niPolarity ? ni->pPosCof : ni->pNegCof;
cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
} else {
pOut->pPosCof = njPolarity ? nj->pPosCof : nj->pNegCof;
cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
}
}
// set the boolean difference of the new group
pOut->pBoolDiff = njPolarity ? nj->pNegCof : nj->pPosCof;
xorInPlace(pOut->pBoolDiff, pOut->pPosCof, TRUTH_WORDS);
}
void dsc_xor_group(Dsc_node_t * pOut, Dsc_node_t * ni, Dsc_node_t * nj, int nVars, const int TRUTH_WORDS) {
//
const unsigned int * xiOFF = ni->off;
const unsigned int * xiON = ni->on;
const unsigned int * xjOFF = nj->off;
const unsigned int * xjON = nj->on;
//
const int xiOFFSize = xiOFF[0];
const int xiONSize = xiON[0];
const int xjOFFSize = xjOFF[0];
const int xjONSize = xjON[0];
// minCubeCofs
int minCCSize = xiOFFSize;
int minCCPolarity = 0;
Dsc_node_t * minCCNode = ni;
// expression
concat(pOut->exp, '[', ']', ni->exp, 1, nj->exp, 1);
if (minCCSize > xiONSize) {
minCCSize = xiONSize;
minCCPolarity = 1;
//minCCNode = ni;
}
if (minCCSize > xjOFFSize) {
minCCSize = xjOFFSize;
minCCPolarity = 0;
minCCNode = nj;
}
if (minCCSize > xjONSize) {
minCCSize = xjONSize;
minCCPolarity = 1;
minCCNode = nj;
}
//
if (minCCNode == ni) {
if (minCCPolarity) {
// gOFF = xiON, xjON
pOut->pNegCof = nj->pPosCof;
cubeCofactor(pOut->pNegCof, xiON, TRUTH_WORDS);
// gON = xiON, xjOFF
pOut->pPosCof = nj->pNegCof;
cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
} else {
// gOFF = xiOFF, xjOFF
pOut->pNegCof = nj->pNegCof;
cubeCofactor(pOut->pNegCof, xiOFF, TRUTH_WORDS);
// gON = xiOFF, xjON
pOut->pPosCof = nj->pPosCof;
cubeCofactor(pOut->pPosCof, xiOFF, TRUTH_WORDS);
}
}else {
if (minCCPolarity) {
// gOFF = xjON, xiON
pOut->pNegCof = ni->pPosCof;
cubeCofactor(pOut->pNegCof, xjON, TRUTH_WORDS);
// gON = xjON, xiOFF
pOut->pPosCof = ni->pNegCof;
cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
} else {
// gOFF = xjOFF, xiOFF
pOut->pNegCof = ni->pNegCof;
cubeCofactor(pOut->pNegCof, xjOFF, TRUTH_WORDS);
// gON = xjOFF, xiON
pOut->pPosCof = ni->pPosCof;
cubeCofactor(pOut->pPosCof, xjOFF, TRUTH_WORDS);
}
}
// bool diff
pOut->pBoolDiff = ni->pBoolDiff;
// evaluating specs
// off spec
pOut->off[0] = 0;
if ((xiOFFSize+xjOFFSize) <= (xiONSize+xjONSize)) {
merge(pOut->off, xiOFF);
merge(pOut->off, xjOFF);
} else {
merge(pOut->off, xiON);
merge(pOut->off, xjON);
}
// on spec
pOut->on[0] = 0;
if ((xiOFFSize+xjONSize) <= (xiONSize+xjOFFSize)) {
merge(pOut->on, xiOFF);
merge(pOut->on, xjON);
} else {
merge(pOut->on, xiON);
merge(pOut->on, xjOFF);
}
}
/**
* memory allocator with a capacity of storing 3*nVars
* truth-tables for negative and positive cofactors and
* the boolean difference for each input variable
*/
extern word * Dsc_alloc_pool(int nVars) {
return ABC_ALLOC(word, 3 * Abc_TtWordNum(nVars) * nVars);
}
/**
* just free the memory pool
*/
extern void Dsc_free_pool(word * pool) {
ABC_FREE(pool);
}
/**
* This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
* entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
* pTruth: pointer for the truth table representing the target function.
* nVarsInit: the number of variables of the truth table of the target function.
* pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
* pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
* (the results presented on ICCD paper are running this method with NULL for the memory pool).
* The method returns 0 if a full decomposition was found and a negative value otherwise.
*/
extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool) {
const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
const int NEED_POOL_ALLOC = (pool == NULL);
Dsc_node_t nodes[DSC_MAX_VAR];
Dsc_node_t *newNodes[DSC_MAX_VAR];
Dsc_node_t *oldNodes[DSC_MAX_VAR];
Dsc_node_t freeNodes[DSC_MAX_VAR]; // N is the maximum number of possible groups.
int f = 0; // f represent the next free position in the freeNodes array
int o = 0; // o stands for the number of already tested nodes
int n = 0; // n will represent the number of current nodes (i.e. support)
pRes[0] = '\0';
pRes[1] = '\0';
if (NEED_POOL_ALLOC)
pool = ABC_ALLOC(word, 3 * TRUTH_WORDS * nVarsInit);
// block for the node data allocation
{
// pointer for the next free truth word
word *pNextTruth = pool;
int iVar;
for (iVar = 0; iVar < nVarsInit; iVar++) {
// negative cofactor
Abc_TtCofactor0p(pNextTruth, pTruth, TRUTH_WORDS, iVar);
// dont care test
if (!Abc_TtEqual(pNextTruth, pTruth, TRUTH_WORDS)) {
Dsc_node_t *node = &nodes[iVar];
node->pNegCof = pNextTruth;
// increment next truth pointer
pNextTruth += TRUTH_WORDS;
// positive cofactor
node->pPosCof = pNextTruth;
Abc_TtCofactor1p(node->pPosCof, pTruth, TRUTH_WORDS, iVar);
// increment next truth pointer
pNextTruth += TRUTH_WORDS;
// boolean difference
node->pBoolDiff = pNextTruth;
Abc_TtXor(node->pBoolDiff, node->pNegCof, node->pPosCof, TRUTH_WORDS, 0);
// increment next truth pointer
pNextTruth += TRUTH_WORDS;
// define on spec -
node->on[0] = 1; node->on[1] = (iVar << 1) | 1u; // lit = i*2+1, when polarity=true
// define off spec
node->off[0] = 1; node->off[1] = iVar << 1;// lit=i*2 otherwise
// store the node expression
node->exp[0] = 'a'+iVar; // TODO fix the variable names
node->exp[1] = '\0';
// add the node to the newNodes array
newNodes[n++] = node;
}
}
}
//const int initialSupport = n;
if (n == 0) {
if (NEED_POOL_ALLOC)
ABC_FREE(pool);
if (Abc_TtIsConst0(pTruth, TRUTH_WORDS)) {
{ if ( pRes ) pRes[0] = '0', pRes[1] = '\0'; }
return 0;
} else if (Abc_TtIsConst1(pTruth, TRUTH_WORDS)) {
{ if ( pRes ) pRes[0] = '1', pRes[1] = '\0'; }
return 0;
} else {
Abc_Print(-1, "ERROR. No variable in the support of f, but f isn't constant!\n");
return -1;
}
}
while (n > 0) {
int tempN = 0;
int i, j, iPolarity, jPolarity;
Dsc_node_t *ni, *nj, *newNode = NULL;
for (i = 0; i < n; i++) {
ni = newNodes[i];
newNode = NULL;
j = 0;
while (j < o) {
nj = oldNodes[j];
if (dsc_and_test(ni, nj, TRUTH_WORDS, &iPolarity, &jPolarity)) {
newNode = &freeNodes[f++];
dsc_and_group(newNode, ni, iPolarity, nj, jPolarity, nVarsInit, TRUTH_WORDS);
}
// XOR test
if ((newNode == NULL) && (dsc_xor_test(ni, nj, TRUTH_WORDS))) {
newNode = &freeNodes[f++];
dsc_xor_group(newNode, ni, nj, nVarsInit, TRUTH_WORDS);
}
if (newNode != NULL) {
oldNodes[j] = oldNodes[--o];
break;
} else {
j++;
}
}
if (newNode != NULL) {
newNodes[tempN++] = newNode;
} else {
oldNodes[o++] = ni;
}
}
n = tempN;
}
if (o == 1) {
Dsc_node_t * solution = oldNodes[0];
if (Abc_TtIsConst0(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst1(solution->pPosCof, TRUTH_WORDS)) {
// Direct solution found
if ( pRes )
strcpy( pRes, solution->exp);
if (NEED_POOL_ALLOC)
ABC_FREE(pool);
return 0;
} else if (Abc_TtIsConst1(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst0(solution->pPosCof, TRUTH_WORDS)) {
// Complementary solution found
if ( pRes ) {
pRes[0] = '!';
strcpy( &pRes[1], solution->exp);
}
if (NEED_POOL_ALLOC)
ABC_FREE(pool);
return 0;
} else {
printf("DSC ERROR: Final DSC node found, but differs from target function.\n");
if (NEED_POOL_ALLOC)
ABC_FREE(pool);
return -1;
}
}
if (NEED_POOL_ALLOC)
ABC_FREE(pool);
return -1;
}
/**Function*************************************************************
Synopsis [DSD formula manipulation.]
Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
***********************************************************************/
int * Dsc_ComputeMatches( char * p )
{
static int pMatches[DSC_MAX_VAR];
int pNested[DSC_MAX_VAR];
int v, nNested = 0;
for ( v = 0; p[v]; v++ )
{
pMatches[v] = 0;
if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
pNested[nNested++] = v;
else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
pMatches[pNested[--nNested]] = v;
assert( nNested < DSC_MAX_VAR );
}
assert( nNested == 0 );
return pMatches;
}
/**Function*************************************************************
Synopsis [DSD formula manipulation.]
Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
***********************************************************************/
int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches )
{
if ( **p == '!' )
(*p)++;
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
(*p)++;
if ( **p == '<' )
{
char * q = pStr + pMatches[*p - pStr];
if ( *(q+1) == '{' )
*p = q+1;
}
if ( **p >= 'a' && **p <= 'z' ) // var
return 0;
if ( **p == '(' || **p == '[' ) // and/or/xor
{
int Counter = 0, AddOn = (**p == '(')? 1 : 3;
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
Counter += AddOn + Dsc_CountAnds_rec( pStr, p, pMatches );
assert( *p == q );
return Counter - AddOn;
}
if ( **p == '<' || **p == '{' ) // mux
{
int Counter = 3;
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
Counter += Dsc_CountAnds_rec( pStr, p, pMatches );
assert( *p == q );
return Counter;
}
assert( 0 );
return 0;
}
/**Function*************************************************************
Synopsis [DSD formula manipulation.]
Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
***********************************************************************/
extern int Dsc_CountAnds( char * pDsd )
{
if ( pDsd[1] == 0 )
return 0;
return Dsc_CountAnds_rec( pDsd, &pDsd, Dsc_ComputeMatches(pDsd) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

91
src/opt/dsc/dsc.h Normal file
View File

@ -0,0 +1,91 @@
/**CFile****************************************************************
FileName [dsc.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Disjoint support decomposition - ICCD'15]
Synopsis [Disjoint-support decomposition with cofactoring and boolean difference analysis
from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
Author [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
Date [Ver. 1.0. Started - October 24, 2014.]
Revision [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
***********************************************************************/
#ifndef ABC__DSC___h
#define ABC__DSC___h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <string.h>
#include "misc/util/abc_global.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
#define DSC_MAX_VAR 16 // should be 6 or more, i.e. DSC_MAX_VAR >= 6
#define DSC_MAX_STR DSC_MAX_VAR << 2 // DSC_MAX_VAR * 4
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== dsc.c ==========================================================*/
/**
* memory allocator with a capacity of storing 3*nVars
* truth-tables for negative and positive cofactors and
* the boolean difference for each input variable
*/
extern word * Dsc_alloc_pool(int nVars);
/**
* This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
* entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
* pTruth: pointer for the truth table representing the target function.
* nVarsInit: the number of variables of the truth table of the target function.
* pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
* pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
* (the results presented on ICCD paper are running this method with NULL for the memory pool).
* The method returns 0 if a full decomposition was found and a negative value otherwise.
*/
extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool);
/**
* just free the memory pool
*/
extern void Dsc_free_pool(word * pool);
int * Dsc_ComputeMatches( char * p );
int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches );
extern int Dsc_CountAnds( char * pDsd );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/opt/dsc/module.make Normal file
View File

@ -0,0 +1 @@
SRC += src/opt/dsc/dsc.c

5
src/opt/sbd/module.make Normal file
View File

@ -0,0 +1,5 @@
SRC += src/opt/sbd/sbd.c \
src/opt/sbd/sbdCnf.c \
src/opt/sbd/sbdCore.c \
src/opt/sbd/sbdSat.c \
src/opt/sbd/sbdWin.c

53
src/opt/sbd/sbd.c Normal file
View File

@ -0,0 +1,53 @@
/**CFile****************************************************************
FileName [sbd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

75
src/opt/sbd/sbd.h Normal file
View File

@ -0,0 +1,75 @@
/**CFile****************************************************************
FileName [sbd.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__opt_sbd__h
#define ABC__opt_sbd__h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Sbd_Par_t_ Sbd_Par_t;
struct Sbd_Par_t_
{
int nLutSize; // target LUT size
int nTfoLevels; // the number of TFO levels (windowing)
int nTfoFanMax; // the max number of fanouts (windowing)
int nWinSizeMax; // maximum window size (windowing)
int nBTLimit; // maximum number of SAT conflicts
int nWords; // simulation word count
int fArea; // area-oriented optimization
int fCover; // use complete cover procedure
int fVerbose; // verbose flag
int fVeryVerbose; // verbose flag
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sbdCnf.c ==========================================================*/
/*=== sbdCore.c ==========================================================*/
extern void Sbd_ParSetDefault( Sbd_Par_t * pPars );
extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * p, Sbd_Par_t * pPars );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

147
src/opt/sbd/sbdCnf.c Normal file
View File

@ -0,0 +1,147 @@
/**CFile****************************************************************
FileName [sbdCnf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis [CNF computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_PrintCnf( Vec_Str_t * vCnf )
{
char Entry;
int i, Lit;
Vec_StrForEachEntry( vCnf, Entry, i )
{
Lit = (int)Entry;
if ( Lit == -1 )
printf( "\n" );
else
printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
{
Vec_StrClear( vCnf );
if ( Truth == 0 || ~Truth == 0 )
{
// assert( nVars == 0 );
Vec_StrPush( vCnf, (char)(Truth == 0) );
Vec_StrPush( vCnf, (char)-1 );
return 1;
}
else
{
int i, k, c, RetValue, Literal, Cube, nCubes = 0;
assert( nVars > 0 );
for ( c = 0; c < 2; c ++ )
{
Truth = c ? ~Truth : Truth;
RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
assert( RetValue == 0 );
nCubes += Vec_IntSize( vCover );
Vec_IntForEachEntry( vCover, Cube, i )
{
for ( k = 0; k < nVars; k++ )
{
Literal = 3 & (Cube >> (k << 1));
if ( Literal == 1 ) // '0' -> pos lit
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
else if ( Literal == 2 ) // '1' -> neg lit
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
else if ( Literal != 0 )
assert( 0 );
}
Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
Vec_StrPush( vCnf, (char)-1 );
}
}
return nCubes;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
{
Vec_Int_t * vClause;
char Entry;
int i, Lit;
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
Vec_StrForEachEntry( vCnf, Entry, i )
{
if ( (int)Entry == -1 )
{
vClause = Vec_WecPushLevel( vRes );
continue;
}
Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
Vec_IntPush( vClause, Lit );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1520
src/opt/sbd/sbdCore.c Normal file
View File

File diff suppressed because it is too large Load Diff

78
src/opt/sbd/sbdInt.h Normal file
View File

@ -0,0 +1,78 @@
/**CFile****************************************************************
FileName [rsbInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__opt_sbdInt__h
#define ABC__opt_sbdInt__h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "sat/bsat/satSolver.h"
#include "misc/util/utilNam.h"
#include "misc/util/utilTruth.h"
#include "map/scl/sclLib.h"
#include "map/scl/sclCon.h"
#include "bool/kit/kit.h"
#include "misc/st/st.h"
#include "map/mio/mio.h"
#include "base/abc/abc.h"
#include "sbd.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
#define SBD_SAT_UNDEC 0x1234567812345678
#define SBD_SAT_SAT 0x8765432187654321
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sbdCnf.c ==========================================================*/
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

797
src/opt/sbd/sbdSat.c Normal file
View File

@ -0,0 +1,797 @@
/**CFile****************************************************************
FileName [sbd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MAX_M 8 // max inputs
#define MAX_N 30 // max nodes
#define MAX_K 6 // max lutsize
#define MAX_D 8 // max delays
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define SBD_LUTS_MAX 2
#define SBD_SIZE_MAX 4
#define SBD_DIV_MAX 16
// new AIG manager
typedef struct Sbd_Pro_t_ Sbd_Pro_t;
struct Sbd_Pro_t_
{
int nLuts; // LUT count
int nSize; // LUT size
int nDivs; // divisor count
int nVars; // intermediate variables (nLuts * nSize)
int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs)
int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters
int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters
int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables
int pDivs[SBD_DIV_MAX]; // divisor variables (external)
};
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
{
Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
int i, k, d, v, n, iVar = 0;
assert( nLuts >= 1 && nLuts <= 2 );
memset( p, 0, sizeof(Sbd_Pro_t) );
p->nLuts = nLuts;
p->nSize = nSize;
p->nDivs = nDivs;
p->nVars = nLuts * nSize;
p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
// set parameters
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < (1 << nSize); k++ )
p->pPars1[i][k] = iVar++;
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
p->pPars2[i][k][d] = iVar++;
// set intermediate variables
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < nSize; k++ )
p->pVars[i][k] = iVar++;
// set top variables
for ( i = 1; i < nLuts; i++ )
p->pVars[i][nSize] = p->pVars[i-1][0];
// set divisor variables
for ( d = 0; d < nDivs; d++ )
p->pDivs[d] = iVar++;
assert( iVar == p->nPars + p->nVars + p->nDivs );
// input compatiblity clauses
for ( i = 0; i < nLuts; i++ )
for ( k = (i > 0); k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
for ( n = 0; n < nDivs; n++ )
{
if ( n < d )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
Vec_IntPush( vCnf, -1 );
}
else if ( k < nSize-1 )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
Vec_IntPush( vCnf, -1 );
}
}
// create LUT clauses
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < (1 << nSize); k++ )
for ( n = 0; n < 2; n++ )
{
for ( v = 0; v < nSize; v++ )
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
Vec_IntPush( vCnf, -1 );
}
// create input clauses
for ( i = 0; i < nLuts; i++ )
for ( k = (i > 0); k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
for ( n = 0; n < 2; n++ )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
Vec_IntPush( vCnf, -1 );
}
return vCnf;
}
// add clauses to the don't-care computation solver
void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
{
int pLits[8], nLits, i, k, iLit, RetValue;
int ThisTopVar = p->pVars[0][p->nSize];
int FirstDivVar = p->nPars + p->nVars;
// add clauses
for ( i = 0; i < Vec_IntSize(vCnf); i++ )
{
assert( Vec_IntEntry(vCnf, i) != -1 );
for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
if ( Vec_IntEntry(vCnf, i) == -1 )
break;
nLits = 0;
Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
if ( Abc_Lit2Var(iLit) == ThisTopVar )
pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
else
pLits[nLits++] = iLit + 2 * iStartVar;
}
assert( nLits <= 8 );
RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
assert( RetValue );
}
}
// add clauses to the functionality evaluation solver
void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
{
Vec_Int_t * vLevel;
int pLits[8], nLits, i, k, iLit, RetValue;
int ThisTopVar = p->pVars[0][p->nSize];
int FirstDivVar = p->nPars + p->nVars;
int FirstIntVar = p->nPars;
// add clauses
Vec_WecForEachLevel( vCnf, vLevel, i )
{
nLits = 0;
Vec_IntForEachEntry( vLevel, iLit, k ) {
if ( Abc_Lit2Var(iLit) == ThisTopVar )
{
if ( Abc_LitIsCompl(iLit) == iTopVarValue )
break;
continue;
}
else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
{
if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
break;
continue;
}
else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
pLits[nLits++] = iLit + 2 * iStartVar;
else
pLits[nLits++] = iLit;
}
if ( k < Vec_IntSize(vLevel) )
continue;
assert( nLits <= 8 );
RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
assert( RetValue );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize
{
sat_solver * pSat = NULL;
Vec_Int_t * vTemp = Vec_IntAlloc(100);
// assign vars
int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+N; i++ )
for ( k = 0; k < K; k++ )
pVars[n][i][k] = -1;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
pVars[n][i][k] = nVars++;
printf( "Number of topo vars = %d.\n", nVars );
*pnVars = nVars;
// add constraints
pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
// each node is used
for ( i = 0; i < M+N-1; i++ )
{
Vec_IntClear( vTemp );
for ( n = 0; n < N; n++ )
for ( k = 0; k < K; k++ )
if ( pVars[n][i][k] >= 0 )
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
printf( "Added %d node connectivity constraints.\n", i );
// each fanin of each node is connected exactly once
Count = 0;
for ( n = 0; n < N; n++ )
for ( k = 0; k < K; k++ )
{
// connected
Vec_IntClear( vTemp );
for ( i = 0; i < M+n; i++ )
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
// exactly once
for ( i = 0; i < M+n; i++ )
for ( j = i+1; j < M+n; j++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
}
printf( "Added %d fanin connectivity constraints.\n", Count );
// node fanins are unique
Count = 0;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
for ( j = i; j < M+n; j++ )
for ( k2 = k+1; k2 < K; k2++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
printf( "Added %d fanin exclusivity constraints.\n", Count );
// nodes are ordered
Count = 0;
for ( n = 1; n < N; n++ )
for ( i = 0; i < M+n-1; i++ )
{
// first of n cannot be smaller than first of n-1 (but can be equal)
for ( j = i+1; j < M+n-1; j++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
// if first nodes of n and n-1 are equal, second nodes are ordered
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) );
for ( j = 0; j < i; j++ )
for ( j2 = j+1; j2 < i; j2++ )
{
Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Vec_IntShrink( vTemp, 2 );
Count++;
}
}
printf( "Added %d node ordering constraints.\n", Count );
// exclude fanins of two-input nodes
Count = 0;
if ( K == 2 )
for ( n = 1; n < N; n++ )
for ( i = M; i < M+n; i++ )
for ( j = 0; j < i; j++ )
for ( k = 0; k < K; k++ )
{
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
printf( "Added %d two-node non-triviality constraints.\n", Count );
// assign delay vars
assert( Req < MAX_D-1 );
for ( i = 0; i < M+N; i++ )
for ( d = 0; d < MAX_D; d++ )
pVars2[i][d] = nVars++;
printf( "Number of total vars = %d.\n", nVars );
// set input delays
for ( i = 0; i < M; i++ )
{
assert( pDelays[i] < MAX_D-2 );
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
// set output delay
for ( k = Req; k < MAX_D; k++ )
{
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
// set internal nodes
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
for ( d = 0; d < MAX_D-1; d++ )
{
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
Vec_IntFree( vTemp );
return pSat;
}
void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
{
int n, i, k;
printf( "Solution:\n" );
printf( " | " );
for ( n = 0; n < N; n++ )
printf( "%2d ", M+n );
printf( "\n" );
for ( i = M+N-2; i >= 0; i-- )
{
printf( "%2d %c | ", i, i < M ? 'i' : ' ' );
for ( n = 0; n < N; n++ )
{
for ( k = K-1; k >= 0; k-- )
if ( pVars[n][i][k] == -1 )
printf( " " );
else
printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
printf( " " );
}
printf( "\n" );
}
}
void Sbd_SolverTopoTest()
{
int M = 8; // 6; // inputs
int N = 3; // 16; // nodes
int K = 4; // 2; // lutsize
int status, v, nVars, nIter, nSols = 0;
int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840
int pDelays[MAX_M] = {1,0,0,0,1};
abctime clk = Abc_Clock();
Vec_Int_t * vLits = Vec_IntAlloc(100);
sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars );
for ( nIter = 0; nIter < 1000000; nIter++ )
{
// find onset minterm
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_Undef )
break;
if ( status == l_False )
break;
assert( status == l_True );
nSols++;
// print solution
if ( nIter < 5 )
Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
// remember variable values
Vec_IntClear( vLits );
for ( v = 0; v < nVars; v++ )
if ( sat_solver_var_value(pSat, v) )
Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
// add breaking clause
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
if ( status == 0 )
break;
//if ( nIter == 5 )
// break;
}
sat_solver_delete( pSat );
Vec_IntFree( vLits );
printf( "Found %d solutions. ", nSols );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis [Synthesize random topology.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] )
{
int Used[MAX_M+MAX_N] = {0};
int nUnused = M;
int n, iFan0, iFan1;
srand( time(NULL) );
for ( n = 0; nUnused < N - n; n++ )
{
iFan0 = iFan1 = 0;
while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) )
;
pLuts[n][0] = iFan0;
pLuts[n][1] = iFan1;
if ( Used[iFan0] == 0 )
{
Used[iFan0] = 1;
nUnused--;
}
if ( Used[iFan1] == 0 )
{
Used[iFan1] = 1;
nUnused--;
}
nUnused++;
}
if ( nUnused == N - n )
{
// undo the first one
for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
if ( Used[iFan0] )
{
Used[iFan0] = 0;
nUnused++;
break;
}
}
assert( nUnused == N - n + 1 );
for ( ; n < N; n++ )
{
for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
if ( Used[iFan0] == 0 )
{
Used[iFan0] = 1;
break;
}
assert( iFan0 < M+n );
for ( iFan1 = 0; iFan1 < M+n; iFan1++ )
if ( Used[iFan1] == 0 )
{
Used[iFan1] = 1;
break;
}
assert( iFan1 < M+n );
pLuts[n][0] = iFan0;
pLuts[n][1] = iFan1;
}
printf( "{\n" );
for ( n = 0; n < N; n++ )
printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n );
printf( "};\n" );
}
/**Function*************************************************************
Synopsis [Compute truth table for the given parameter settings.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] )
{
int i, k, v, nLutPars = (1 << K) - 1;
word Truths[MAX_M+MAX_N];
assert( M <= 6 && N <= MAX_N );
for ( i = 0; i < M; i++ )
Truths[i] = s_Truths6[i];
for ( i = 0; i < N; i++ )
{
word Truth = 0, Mint;
for ( k = 1; k <= nLutPars; k++ )
{
if ( !pValues[i*nLutPars+k-1] )
continue;
Mint = ~(word)0;
for ( v = 0; v < K; v++ )
Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] : ~Truths[pLuts[i][v]];
Truth |= Mint;
}
Truths[M+i] = Truth;
}
return Truths[M+N-1];
}
word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl )
{
int i, k, v, nLutPars = (1 << K) - 1;
int nWords = Abc_TtWordNum( M );
word * pRes = pTruthsElem + (M+N-1)*nWords;
assert( M <= MAX_M && N <= MAX_N );
for ( i = 0; i < N; i++ )
{
word * pMint, * pTruth = pTruthsElem + (M+i)*nWords;
Abc_TtClear( pTruth, nWords );
for ( k = 1; k <= nLutPars; k++ )
{
if ( !pValues[i*nLutPars+k-1] )
continue;
pMint = pTruthsElem + (M+N)*nWords;
Abc_TtFill( pMint, nWords );
for ( v = 0; v < K; v++ )
{
word * pFanin = pTruthsElem + pLuts[i][v]*nWords;
Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 );
}
Abc_TtOr( pTruth, pTruth, pMint, nWords );
}
}
if ( fCompl )
Abc_TtNot( pRes, nWords );
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues )
{
int fVerbose = 0;
abctime clk = Abc_Clock();
abctime clk2, clkOther = 0;
sat_solver * pSat = NULL;
int nWords = Abc_TtWordNum(M);
int pLits[MAX_K+2], pLits2[MAX_K+2], nLits;
int nLutPars = (1 << K) - 1, nVars = N * nLutPars;
int i, k, m, status, iMint, Iter, fCompl = (int)(pTruthInit[0] & 1);
// create truth tables
word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) );
Abc_TtElemInit2( pTruths, M );
// create solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
// start with the last minterm
// iMint = (1 << M) - 1;
iMint = 1;
for ( Iter = 0; Iter < (1 << M); Iter++ )
{
// assign the first intermediate variable
int nVarStart = sat_solver_nvars(pSat);
sat_solver_setnvars( pSat, nVarStart + N - 1 );
// add clauses for nodes
//if ( fVerbose )
printf( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) );
for ( i = 0; i < N; i++ )
for ( m = 0; m <= nLutPars; m++ )
{
if ( fVerbose )
printf( "i = %d. m = %d.\n", i, m );
// selector variables
nLits = 0;
for ( k = 0; k < K; k++ )
{
if ( pLuts[i][k] >= M )
{
assert( pLuts[i][k] - M < N - 1 );
pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 );
nLits++;
}
else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) )
break;
}
if ( k < K )
continue;
// add parameter
if ( m )
{
pLits[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 1 );
pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 );
nLits++;
}
// node variable
if ( i != N - 1 )
{
pLits[nLits] = Abc_Var2Lit( nVarStart + i, 0 );
pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 );
nLits++;
}
// add clauses
if ( i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) != fCompl )
{
status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
if ( status == 0 )
{
fCompl = -1;
goto finish;
}
}
if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == fCompl) && m > 0 )
{
status = sat_solver_addclause( pSat, pLits, pLits + nLits );
if ( status == 0 )
{
fCompl = -1;
goto finish;
}
}
}
// run SAT solver
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_Undef )
break;
if ( status == l_False )
{
fCompl = -1;
goto finish;
}
assert( status == l_True );
// collect values
for ( i = 0; i < nVars; i++ )
pValues[i] = sat_solver_var_value(pSat, i);
clk2 = Abc_Clock();
pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl );
clkOther += Abc_Clock() - clk2;
if ( fVerbose )
{
for ( i = 0; i < nVars; i++ )
printf( "%d=%d ", i, pValues[i] );
printf( " " );
for ( i = nVars; i < sat_solver_nvars(pSat); i++ )
printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pTruthInit, (1 << M) ); printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" );
}
if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) )
break;
// get new minterm
iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M );
}
finish:
printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) );
sat_solver_delete( pSat );
ABC_FREE( pTruths );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time", clkOther );
return fCompl;
}
void Sbd_SolverFuncTest()
{
// int M = 4; // 6; // inputs
// int N = 3; // 16; // nodes
// int K = 2; // 2; // lutsize
// word Truth = ~((word)3 << 8);
// int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
/*
int M = 6; // 6; // inputs
int N = 19; // 16; // nodes
int K = 2; // 2; // lutsize
word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 };
int pLuts[MAX_N][MAX_K] = {
{3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9},
{0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14},
{10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13},
{20, 7}, {19, 21}, {4, 16}, {23, 22}
};
*/
/*
int M = 6; // 6; // inputs
int N = 5; // 16; // nodes
int K = 4; // 2; // lutsize
word Truth = ABC_CONST(0x9ef7a8d9c7193a0f);
int pLuts[MAX_N][MAX_K] = {
{0, 1, 2, 3}, // 6
{1, 2, 3, 4}, // 7
{2, 3, 4, 5}, // 8
{0, 1, 4, 5}, // 9
{6, 7, 8, 9} // 10
};
*/
/*
int M = 8; // 6; // inputs
int N = 7; // 16; // nodes
int K = 2; // 2; // lutsize
// word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) };
// word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 };
word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) };
int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
*/
int M = 8; // 6; // inputs
int N = 7; // 16; // nodes
int K = 2; // 2; // lutsize
word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) };
int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
int pValues[MAX_N*((1<<MAX_K)-1)];
int Res, i, k, nLutPars = (1 << K) - 1;
//Sbd_SolverSynth( M, N, K, pLuts );
Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, pValues );
if ( Res == -1 )
{
printf( "Solution does not exist.\n" );
return;
}
printf( "Result (compl = %d):\n", Res );
for ( i = 0; i < N; i++ )
{
for ( k = nLutPars-1; k >= 0; k-- )
printf( "%d", pValues[i*nLutPars+k] );
printf( "0\n" );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

310
src/opt/sbd/sbdSim.c Normal file
View File

@ -0,0 +1,310 @@
/**CFile****************************************************************
FileName [sbdSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis [Simulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbdSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline word * Sbd_ObjSims( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims, p->iPatsPi * i ); }
static inline word * Sbd_ObjCtrl( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSimsPi, p->iPatsPi * i ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This does not work.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_GiaSimRoundBack2( Gia_Man_t * p )
{
int nWords = p->iPatsPi;
Gia_Obj_t * pObj;
int w, i, Id;
// init primary outputs
Gia_ManForEachCoId( p, Id, i )
for ( w = 0; w < nWords; w++ )
Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0);
// transfer to nodes
Gia_ManForEachCo( p, pObj, i )
{
word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) );
}
// simulate nodes
Gia_ManForEachAndReverse( p, pObj, i )
{
word * pSims = Sbd_ObjSims(p, i);
word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i));
word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i));
word Rand = Gia_ManRandomW(0);
for ( w = 0; w < nWords; w++ )
{
pSims0[w] = pSims[w] | Rand;
pSims1[w] = pSims[w] | ~Rand;
}
if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords );
if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords );
}
// primary inputs are initialized
}
/**Function*************************************************************
Synopsis [Tries to falsify a sequence of two-literal SAT problems.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_GiaSatOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, int fFirst, int iPat )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return (int)pObj->fMark0 == Value;
Gia_ObjSetTravIdCurrent(p, pObj);
pObj->fMark0 = Value;
if ( Gia_ObjIsCi(pObj) )
{
word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
if ( Abc_TtGetBit( pSims, iPat ) != Value )
Abc_TtXorBit( pSims, iPat );
return 1;
}
assert( Gia_ObjIsAnd(pObj) );
assert( !Gia_ObjIsXor(pObj) );
if ( Value )
return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) &&
Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat );
if ( fFirst )
return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat );
else
return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat );
}
int Sbd_GiaSatOne( Gia_Man_t * p, Vec_Int_t * vPairs )
{
int k, n, Var1, Var2, iPat = 0;
//Gia_ManSetPhase( p );
Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k )
{
Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 );
Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 );
assert( Var2 > 0 );
if ( Var1 == 0 )
{
for ( n = 0; n < 2; n++ )
{
Gia_ManIncrementTravId( p );
if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
{
iPat++;
break;
}
}
printf( "%c", n == 2 ? '.' : 'c' );
}
else
{
for ( n = 0; n < 2; n++ )
{
Gia_ManIncrementTravId( p );
if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) )
{
iPat++;
break;
}
Gia_ManIncrementTravId( p );
if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
{
iPat++;
break;
}
}
printf( "%c", n == 2 ? '.' : 'e' );
}
if ( iPat == 64 * p->iPatsPi - 1 )
break;
}
printf( "\n" );
return iPat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_GiaSimRoundBack( Gia_Man_t * p )
{
extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap );
Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) );
Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
Vec_Int_t * vMap; // maps each node into its class
int i, nConsts = 0, nClasses = 0, nPats;
Sbd_GiaSimRound( p, 0, &vMap );
Gia_ManForEachAndId( p, i )
{
if ( Vec_IntEntry(vMap, i) == 0 )
Vec_IntPushTwo( vPairs, 0, i ), nConsts++;
else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 )
Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i );
else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 )
{
Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i );
Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 );
nClasses++;
}
}
Vec_IntFree( vMap );
Vec_IntFree( vReprs );
printf( "Constants = %d. Classes = %d.\n", nConsts, nClasses );
nPats = Sbd_GiaSatOne( p, vPairs );
Vec_IntFree( vPairs );
printf( "Generated %d patterns.\n", nPats );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap )
{
int nWords = p->iPatsPi;
Vec_Mem_t * vStore;
Gia_Obj_t * pObj;
Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) );
int w, i, Id, fCompl, RetValue;
// init primary inputs
if ( fTry )
{
Sbd_GiaSimRoundBack( p );
Gia_ManForEachCiId( p, Id, i )
Sbd_ObjSims(p, Id)[0] <<= 1;
}
else
{
Gia_ManForEachCiId( p, Id, i )
for ( w = 0; w < nWords; w++ )
Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w;
}
// simulate internal nodes
vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page
Vec_MemHashAlloc( vStore, 1 << 16 );
RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero
assert( RetValue == 0 );
Gia_ManForEachAnd( p, pObj, i )
{
word * pSims = Sbd_ObjSims(p, i);
if ( Gia_ObjIsXor(pObj) )
Abc_TtXor( pSims,
Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)),
Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)),
nWords,
Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
else
Abc_TtAndCompl( pSims,
Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj),
Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj),
nWords );
// hash sim info
fCompl = (int)(pSims[0] & 1);
if ( fCompl ) Abc_TtNot( pSims, nWords );
Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) );
if ( fCompl ) Abc_TtNot( pSims, nWords );
}
Gia_ManForEachCo( p, pObj, i )
{
word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) );
// printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) );
assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) );
}
// printf( "\n" );
Vec_MemHashFree( vStore );
Vec_MemFree( vStore );
printf( "Objects = %6d. Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) );
if ( pvMap )
*pvMap = vMap;
else
Vec_IntFree( vMap );
}
void Sbd_GiaSimTest( Gia_Man_t * pGia )
{
Gia_ManSetPhase( pGia );
// allocate simulation info
pGia->iPatsPi = 32;
pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
Gia_ManRandom( 1 );
Sbd_GiaSimRound( pGia, 0, NULL );
Sbd_GiaSimRound( pGia, 0, NULL );
Sbd_GiaSimRound( pGia, 0, NULL );
printf( "\n" );
Sbd_GiaSimRound( pGia, 1, NULL );
printf( "\n" );
Sbd_GiaSimRound( pGia, 1, NULL );
printf( "\n" );
Sbd_GiaSimRound( pGia, 1, NULL );
Vec_WrdFreeP( &pGia->vSims );
Vec_WrdFreeP( &pGia->vSimsPi );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

283
src/opt/sbd/sbdWin.c Normal file
View File

@ -0,0 +1,283 @@
/**CFile****************************************************************
FileName [sbd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Constructs SAT solver for the window.]
Description [The window for the pivot node (Pivot) is represented as
a DFS ordered array of objects (vWinObjs) whose indexed in the array
(which will be used as SAT variables) are given in array vObj2Var.
The TFO nodes are listed as the last ones in vWinObjs. The root nodes
are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.]
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
{
Gia_Obj_t * pObj;
int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
//Vec_IntPrint( vWinObjs );
//Vec_IntPrint( vTfo );
//Vec_IntPrint( vRoots );
// create SAT solver
if ( pSat == NULL )
pSat = sat_solver_new();
else
sat_solver_restart( pSat );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
// create constant 0 clause
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
// add clauses for all nodes
Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
{
pObj = Gia_ManObj( p, iObj );
if ( Gia_ObjIsCi(pObj) )
continue;
assert( Gia_ObjIsAnd(pObj) );
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
Node = Vec_IntEntry( vObj2Var, iObj );
Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
if ( Gia_ObjIsXor(pObj) )
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
else
sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
}
// add second clauses for the TFO
Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
{
pObj = Gia_ManObj( p, iObj );
assert( Gia_ObjIsAnd(pObj) );
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
if ( Gia_ObjIsXor(pObj) )
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
else
sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
}
if ( Vec_IntSize(vRoots) > 0 )
{
// create XOR clauses for the roots
int nVars = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo);
Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
Vec_IntForEachEntry( vRoots, iObj, i )
{
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
Node = Vec_IntEntry( vObj2Var, iObj );
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
}
// make OR clause for the last nRoots variables
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
Vec_IntFree( vFaninVars );
if ( RetValue == 0 )
{
sat_solver_delete( pSat );
return NULL;
}
assert( sat_solver_nvars(pSat) == nVars + 32 );
}
// finalize
RetValue = sat_solver_simplify( pSat );
if ( RetValue == 0 )
{
sat_solver_delete( pSat );
return NULL;
}
return pSat;
}
/**Function*************************************************************
Synopsis [Solves one SAT problem.]
Description [Computes node function for PivotVar with fanins in vDivVars
using don't-care represented in the SAT solver. Uses array vValues to
return the values of the first Vec_IntSize(vValues) SAT variables in case
the implementation of the node with the given fanins does not exist.]
SideEffects []
SeeAlso []
***********************************************************************/
word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp )
{
int nBTLimit = 0;
word uCube, uTruth = 0;
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
assert( FreeVar < sat_solver_nvars(pSat) );
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
while ( 1 )
{
// find onset minterm
status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SBD_SAT_UNDEC;
if ( status == l_False )
return uTruth;
assert( status == l_True );
// remember variable values
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
// collect divisor literals
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SBD_SAT_UNDEC;
if ( status == l_True )
break;
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal );
uCube = ~(word)0;
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
for ( i = 0; i < nFinal; i++ )
{
if ( pFinal[i] == pLits[0] )
continue;
Vec_IntPush( vTemp, pFinal[i] );
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
assert( status );
nIter++;
}
assert( status == l_True );
// store the counter-example
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntAddToEntry( vValues, i, 0xC );
/*
// reduce the counter example
for ( n = 0; n < 2; n++ )
{
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1 (expanding offset against onset)
for ( i = 0; i < Vec_IntSize(vValues); i++ )
Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal );
for ( i = 0; i < nFinal; i++ )
if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
}
*/
return SBD_SAT_SAT;
}
/**Function*************************************************************
Synopsis [Returns a bunch of positive/negative random care minterms.]
Description [Returns 0/1 if the functions is const 0/1.]
SideEffects []
SeeAlso []
***********************************************************************/
static void sat_solver_random_polarity(sat_solver* s)
{
int i, k;
for ( i = 0; i < s->size; i += 64 )
{
word Polar = Gia_ManRandomW(0);
for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
}
}
int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
{
int nBTLimit = 0;
int i, Ind;
assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
Vec_IntForEachEntry( vInds, Ind, i )
{
int fOffSet = (int)(i < nCareMints[0]);
int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
sat_solver_random_polarity( pSat );
status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -2;
if ( status == l_False )
return fOffSet;
for ( k = 0; k <= PivotVar; k++ )
if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
Abc_TtXorBit(pVarSims[k], Ind);
}
return -1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

55
src/proof/acec/acecCl.c Normal file
View File

@ -0,0 +1,55 @@
/**CFile****************************************************************
FileName [acecCl.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CEC for arithmetic circuits.]
Synopsis [Core procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: acecCl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

158
src/proof/acec/acecCo.c
View File

@ -44,11 +44,14 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Gia_PolynCoreNonXors_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vXorPairs )
{
extern int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj );
Gia_Obj_t * pFan0, * pFan1;
if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
return;
Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan0), vXorPairs );
Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan1), vXorPairs );
//if ( Gia_ManSuppSizeOne(pGia, pObj) > 4 )
//if ( Gia_ObjId(pGia, pObj) >= 73 )
Vec_IntPushTwo( vXorPairs, Gia_ObjId(pGia, Gia_Regular(pFan0)), Gia_ObjId(pGia, Gia_Regular(pFan1)) );
}
Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
@ -87,38 +90,30 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts )
Vec_Wec_t * Gia_PolynComputeMap( Vec_Int_t * vAdds, int nObjs )
{
Vec_Int_t * vOrder = Vec_IntAlloc( 1000 );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
Vec_Int_t * vRoots = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) );
Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) );
int i, k, Index, Driver, Entry1, Entry2 = -1;
// nodes driven by adders into adder indexes
for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
// map nodes driven by adders into adder indexes
Vec_Wec_t * vMap = Vec_WecStart( nObjs ); int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
Entry1 = Vec_IntEntry( vAdds, 5*i + 3 );
Entry2 = Vec_IntEntry( vAdds, 5*i + 4 );
int Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
int Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
Vec_WecPush( vMap, Entry1, i );
Vec_WecPush( vMap, Entry1, Entry2 );
Vec_WecPush( vMap, Entry2, i );
Vec_WecPush( vMap, Entry2, Entry1 );
}
// collect roots
Gia_ManForEachCoDriverId( pGia, Driver, i )
{
Vec_IntPush( vRoots, Driver );
return vMap;
}
Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Int_t * vRoots, Vec_Int_t ** pvIns )
{
Vec_Int_t * vOrder = Vec_IntAlloc( 1000 );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
int i, k, Index, Driver, Entry1, Entry2 = -1;
// mark roots
Vec_IntForEachEntry( vRoots, Driver, i )
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
}
// collect additional outputs
Vec_IntForEachEntry( vAddCos, Driver, i )
{
Vec_IntPush( vRoots, Driver );
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
}
// detect full adder tree
*pvOuts = Vec_IntDup( vRoots );
// collect boxes
while ( 1 )
{
// iterate through boxes driving this one
@ -140,9 +135,9 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
Vec_IntRemove( vRoots, Entry1 );
Vec_IntRemove( vRoots, Entry2 );
// set new marks
Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
Driver = Vec_IntEntry( vAdds, 5*Index + 2 );
Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
Driver = Vec_IntEntry( vAdds, 6*Index + 2 );
Vec_BitWriteEntry( vIsRoot, Entry1, 1 );
Vec_BitWriteEntry( vIsRoot, Entry2, 1 );
Vec_BitWriteEntry( vIsRoot, Driver, 1 );
@ -155,17 +150,97 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
break;
}
// collect remaining leaves
Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
if ( Driver )
Vec_IntPush( vLeaves, i );
*pvIns = vLeaves;
// cleanup
if ( pvIns )
{
*pvIns = Vec_IntAlloc( Vec_BitSize(vIsRoot) );
Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 )
if ( Driver )
Vec_IntPush( *pvIns, i );
}
Vec_BitFree( vIsRoot );
return vOrder;
}
Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts )
{
Vec_Int_t * vOrder;
Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
Vec_Int_t * vRoots = Vec_IntAlloc( Gia_ManCoNum(pGia) );
int i, Driver;
// collect roots
Gia_ManForEachCoDriverId( pGia, Driver, i )
Vec_IntPush( vRoots, Driver );
// collect additional outputs
if ( vAddCos )
Vec_IntForEachEntry( vAddCos, Driver, i )
Vec_IntPush( vRoots, Driver );
// remember roots
if ( pvOuts )
*pvOuts = Vec_IntDup( vRoots );
// create order
vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, pvIns );
Vec_IntFree( vRoots );
Vec_WecFree( vMap );
printf( "Collected %d boxes.\n", Vec_IntSize(vOrder) );
return vOrder;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_PolyCollectRoots_rec( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
{
int k;
for ( k = 0; k < 3; k++ )
{
int i, Index, Sum, Carry = Vec_IntEntry( vAdds, 6*iBox+k );
Vec_Int_t * vLevel = Vec_WecEntry( vMap, Carry );
if ( Carry == 0 )
continue;
Vec_IntForEachEntryDouble( vLevel, Index, Sum, i )
if ( Vec_IntEntry(vAdds, 6*Index+4) == Carry && !Vec_BitEntry(vMarks, Sum) )
{
Vec_IntPush( vRoots, Sum );
Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, Index, vRoots );
}
}
}
void Gia_PolyCollectRoots( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots )
{
Vec_IntClear( vRoots );
Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+3) );
Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+4) );
Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, iBox, vRoots );
}
Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes )
{
extern Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds );
Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( pGia, vAdds );
Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) );
Vec_Wec_t * vRes = Vec_WecStart( Vec_IntSize(vRootBoxes) );
Vec_Int_t * vRoots = Vec_IntAlloc( 64 );
Vec_Int_t * vOrder;
int i, iBox;
Vec_IntForEachEntry( vRootBoxes, iBox, i )
{
Gia_PolyCollectRoots( vAdds, vMap, vMarks, iBox, vRoots );
vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, NULL );
Vec_IntAppend( Vec_WecEntry(vRes, i), vOrder );
Vec_IntFree( vOrder );
}
Vec_BitFree( vMarks );
Vec_IntFree( vRoots );
Vec_WecFree( vMap );
return vRes;
}
/**Function*************************************************************
Synopsis [Collect internal node order.]
@ -194,15 +269,15 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t
Vec_IntForEachEntryReverse( vOrder, Index, i )
{
// mark inputs
Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 );
Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 );
Entry3 = Vec_IntEntry( vAdds, 5*Index + 2 );
Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 );
Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 );
Entry3 = Vec_IntEntry( vAdds, 6*Index + 2 );
Vec_BitWriteEntry( vVisited, Entry1, 1 );
Vec_BitWriteEntry( vVisited, Entry2, 1 );
Vec_BitWriteEntry( vVisited, Entry3, 1 );
// traverse from outputs
Entry1 = Vec_IntEntry( vAdds, 5*Index + 3 );
Entry2 = Vec_IntEntry( vAdds, 5*Index + 4 );
Entry1 = Vec_IntEntry( vAdds, 6*Index + 3 );
Entry2 = Vec_IntEntry( vAdds, 6*Index + 4 );
Gia_PolynCoreCollect_rec( pGia, Entry1, vNodes, vVisited );
Gia_PolynCoreCollect_rec( pGia, Entry2, vNodes, vVisited );
}
@ -312,14 +387,17 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t
***********************************************************************/
Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, int fAddCones, int fVerbose )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
abctime clk = Abc_Clock();
Gia_Man_t * pNew;
Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, 1 );
Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, NULL, 1 );
Vec_Int_t * vLeaves, * vRoots, * vOrder = Gia_PolynCoreOrder( pGia, vAdds, vAddCos, &vLeaves, &vRoots );
Vec_Int_t * vNodes = Gia_PolynCoreCollect( pGia, vAdds, vOrder );
//Gia_ManShow( pGia, vNodes, 0 );
printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ",
Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
Vec_IntSize(vAdds)/6, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose );

282
src/proof/acec/acecPa.c Normal file
View File

@ -0,0 +1,282 @@
/**CFile****************************************************************
FileName [acecPa.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CEC for arithmetic circuits.]
Synopsis [Core procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: acecPa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pas_ManVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int Truth0, Truth1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return pObj->Value;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
assert( !Gia_ObjIsXor(pObj) );
Truth0 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
Truth1 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
return (pObj->Value = Truth0 & Truth1);
}
void Pas_ManVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
{
Gia_Obj_t * pObj;
unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
if ( !fFadd )
return;
Gia_ManIncrementTravId( p );
for ( k = 0; k < 3; k++ )
{
iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
pObj = Gia_ManObj( p, iObj );
pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
Gia_ObjSetTravIdCurrent( p, pObj );
}
iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
TruthXor = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
if ( fFadd ) // FADD
{
if ( TruthXor != 0x96 )
printf( "Fadd %d sum is wrong.\n", iBox );
if ( TruthMaj != 0xE8 )
printf( "Fadd %d carry is wrong.\n", iBox );
}
else
{
if ( TruthXor != 0x66 )
printf( "Hadd %d sum is wrong.\n", iBox );
if ( TruthMaj != 0x88 )
printf( "Hadd %d carry is wrong.\n", iBox );
}
}
void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase )
{
int k, iBox;
Vec_IntForEachEntry( vOrder, iBox, k )
Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase )
{
int k, iBox, iXor, Sign, fXorPhase;
assert( pObj != Gia_ManConst0(p) );
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( fPhase )
Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase );
if ( !Gia_ObjIsAnd(pObj) )
return;
iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) );
if ( iBox == -1 )
return;
iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
fXorPhase = ((Sign >> 3) & 1);
// remember complemented HADD
if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase )
Vec_BitWriteEntry( vConstPhase, iBox, 1 );
for ( k = 0; k < 3; k++ )
{
int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
int fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
fXorPhase ^= fPhaseThis;
if ( iObj == 0 )
continue;
Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase );
}
Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
}
Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase )
{
Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) );
Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 );
int i, iRoot;
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vRoots, iRoot, i )
Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase );
*pvConstPhase = vConstPhase;
return vPhase;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts )
{
Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
Vec_Bit_t * vPhase, * vConstPhase;
int i, k, Entry, nTrees;
// map carries into adder indexes and mark driven nodes
Vec_IntForEachEntry( vOrder, i, k )
{
int Carry = Vec_IntEntry(vAdds, 6*i+4);
if ( Vec_BitEntry(vUnique, Carry) )
printf( "Carry %d participates more than once.\n", Carry );
Vec_BitWriteEntry( vUnique, Carry, 1 );
Vec_IntWriteEntry( vMap, Carry, i );
// mark driven
Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 );
Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 );
Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 );
}
// collect carries that do not drive other adders
for ( i = 0; i < Gia_ManObjNum(p); i++ )
if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) )
Vec_IntPush( vRoots, i );
nTrees = Vec_IntSize( vRoots );
Vec_IntPrint( vRoots );
// compute phases
if ( Vec_IntSize(vRoots) > 0 )
{
int nCompls = 0;
vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase );
Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase );
printf( "Outputs: " );
Vec_IntForEachEntry( vOuts, Entry, i )
printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
printf( "\n" );
printf( "Inputs: " );
Vec_IntForEachEntry( vIns, Entry, i )
{
printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
nCompls += Vec_BitEntry(vPhase, Entry);
}
printf( " Compl = %d\n", nCompls );
Vec_BitFreeP( &vPhase );
Vec_BitFreeP( &vConstPhase );
}
Vec_IntFree( vRoots );
Vec_IntFree( vMap );
Vec_BitFree( vUnique );
Vec_BitFree( vUsed );
return nTrees;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pas_ManComputeCutsTest( Gia_Man_t * p )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts );
extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
abctime clk = Abc_Clock();
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
Vec_Int_t * vIns, * vOuts;
Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts );
int nTrees, nFadds = Ree_ManCountFadds( vAdds );
//Ree_ManPrintAdders( vAdds, 1 );
printf( "Detected %d FAs and %d HAs. Collected %d adders. ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// detect trees
clk = Abc_Clock();
nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts );
Vec_IntFree( vAdds );
Vec_IntFree( vOrder );
Vec_IntFree( vIns );
Vec_IntFree( vOuts );
printf( "Detected %d adder trees. ", nTrees );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

2
src/proof/acec/acecPolyn.c
View File

@ -429,7 +429,7 @@ void Gia_PolynBuild2( Gia_Man_t * pGia, int fSigned, int fVerbose, int fVeryVerb
{
Hsh_VecMan_t * pHashC = Hsh_VecManStart( 1000 ); // hash table for constants
Hsh_VecMan_t * pHashM = Hsh_VecManStart( 1000 ); // hash table for monomials
Vec_Wec_t * vLit2Mono = Vec_WecStart( Gia_ManObjNum(pGia) * 2 );
//Vec_Wec_t * vLit2Mono = Vec_WecStart( Gia_ManObjNum(pGia) * 2 );
Hsh_VecManStop( pHashC );
Hsh_VecManStop( pHashM );

445
src/proof/acec/acecPool.c Normal file
View File

@ -0,0 +1,445 @@
/**CFile****************************************************************
FileName [acecPool.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CEC for arithmetic circuits.]
Synopsis [Core procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: acecPool.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acec_ManCreateCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds )
{
// map carries into their boxes
Vec_Int_t * vCarryMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
Vec_IntWriteEntry( vCarryMap, Vec_IntEntry(vAdds, 6*i+4), i );
return vCarryMap;
}
int Acec_ManCheckCarryMap( Gia_Man_t * p, int Carry, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap )
{
int iBox = Vec_IntEntry( vCarryMap, Carry );
assert( iBox >= 0 );
return Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+0) ) >= 0 ||
Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+1) ) >= 0 ||
Vec_IntEntry( vCarryMap, Vec_IntEntry(vAdds, 6*iBox+2) ) >= 0;
}
Vec_Int_t * Acec_ManCollectCarryRoots( Gia_Man_t * p, Vec_Int_t * vAdds )
{
Vec_Int_t * vCarryRoots = Vec_IntAlloc( 100 );
Vec_Bit_t * vIns = Vec_BitStart( Gia_ManObjNum(p) ); int i;
// marks box inputs
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+0), 1 );
Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+1), 1 );
Vec_BitWriteEntry( vIns, Vec_IntEntry(vAdds, 6*i+2), 1 );
}
// collect roots
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
if ( !Vec_BitEntry(vIns, Vec_IntEntry(vAdds, 6*i+4)) )
Vec_IntPush( vCarryRoots, Vec_IntEntry(vAdds, 6*i+4) );
Vec_BitFree( vIns );
return vCarryRoots;
}
Vec_Int_t * Acec_ManCollectXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
{
Vec_Int_t * vXorRoots = Vec_IntAlloc( 100 );
Vec_Bit_t * vIns = Vec_BitStart( Gia_ManObjNum(p) ); int i;
// marks box inputs
for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
{
Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+1), 1 );
Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+2), 1 );
Vec_BitWriteEntry( vIns, Vec_IntEntry(vXors, 4*i+3), 1 );
}
// collect roots
for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
if ( !Vec_BitEntry(vIns, Vec_IntEntry(vXors, 4*i)) )
Vec_IntPush( vXorRoots, Vec_IntEntry(vXors, 4*i) );
Vec_BitFree( vIns );
return vXorRoots;
}
void Acec_ManCountXorTreeInputs_rec( Gia_Man_t * p, int Node, Vec_Int_t * vXors, Vec_Int_t * vXorMap, Vec_Bit_t * vIsCarryRoot, Vec_Int_t * vCarryRootSet, Vec_Int_t * vXorSet )
{
int k, iXorBox;
if ( Node == 0 || Gia_ObjIsTravIdCurrentId(p, Node) )
return;
Gia_ObjSetTravIdCurrentId(p, Node);
iXorBox = Vec_IntEntry( vXorMap, Node );
if ( iXorBox == -1 )
{
if ( Vec_BitEntry(vIsCarryRoot, Node) )
Vec_IntPush( vCarryRootSet, Node );
return;
}
for ( k = 1; k < 4; k++ )
Acec_ManCountXorTreeInputs_rec( p, Vec_IntEntry(vXors, 4*iXorBox+k), vXors, vXorMap, vIsCarryRoot, vCarryRootSet, vXorSet );
Vec_IntPush( vXorSet, Vec_IntEntry(vXors, 4*iXorBox) );
}
Vec_Wec_t * Acec_ManCollectCarryRootSets( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap, Vec_Int_t * vXors, Vec_Int_t * vXorRoots, Vec_Int_t * vCarryRoots )
{
Vec_Wec_t * vCarryRootSets = Vec_WecAlloc( 100 ); // XorBoxes, CarryRoots, AdderBoxes, Ins/Ranks, Outs/Ranks
Vec_Int_t * vCarryRootSet = Vec_IntAlloc( 100 );
Vec_Bit_t * vIsCarryRoot = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vXorSet = Vec_IntAlloc( 100 ), * vLevel;
int i, k, XorRoot, CarryRoot;
// map XORs into their cuts
Vec_Int_t * vXorMap = Vec_IntStartFull( Gia_ManObjNum(p) );
for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
Vec_IntWriteEntry( vXorMap, Vec_IntEntry(vXors, 4*i), i );
// create carry root marks
Vec_IntForEachEntry( vCarryRoots, CarryRoot, i )
Vec_BitWriteEntry( vIsCarryRoot, CarryRoot, 1 );
// collect carry roots attached to each XOR root
Vec_IntForEachEntry( vXorRoots, XorRoot, i )
{
Vec_IntClear( vXorSet );
Vec_IntClear( vCarryRootSet );
Gia_ManIncrementTravId( p );
Acec_ManCountXorTreeInputs_rec( p, XorRoot, vXors, vXorMap, vIsCarryRoot, vCarryRootSet, vXorSet );
// skip trivial
Vec_IntForEachEntry( vCarryRootSet, CarryRoot, k )
if ( Acec_ManCheckCarryMap(p, CarryRoot, vAdds, vCarryMap) )
break;
if ( k == Vec_IntSize(vCarryRootSet) )
continue;
Vec_IntSort( vCarryRootSet, 0 );
vLevel = Vec_WecPushLevel( vCarryRootSets );
Vec_IntAppend( vLevel, vXorSet );
vLevel = Vec_WecPushLevel( vCarryRootSets );
Vec_IntAppend( vLevel, vCarryRootSet );
vLevel = Vec_WecPushLevel( vCarryRootSets );
vLevel = Vec_WecPushLevel( vCarryRootSets );
vLevel = Vec_WecPushLevel( vCarryRootSets );
// unmark carry root set
Vec_IntForEachEntry( vCarryRootSet, CarryRoot, k )
{
assert( Vec_BitEntry(vIsCarryRoot, CarryRoot) );
Vec_BitWriteEntry( vIsCarryRoot, CarryRoot, 0 );
}
}
Vec_IntFree( vCarryRootSet );
Vec_IntFree( vXorSet );
Vec_IntFree( vXorMap );
// collect unmarked carry roots
Vec_IntForEachEntry( vCarryRoots, CarryRoot, k )
{
if ( !Vec_BitEntry(vIsCarryRoot, CarryRoot) )
continue;
if ( !Acec_ManCheckCarryMap(p, CarryRoot, vAdds, vCarryMap) )
continue;
vLevel = Vec_WecPushLevel( vCarryRootSets );
vLevel = Vec_WecPushLevel( vCarryRootSets );
Vec_IntFill( vLevel, 1, CarryRoot );
vLevel = Vec_WecPushLevel( vCarryRootSets );
vLevel = Vec_WecPushLevel( vCarryRootSets );
vLevel = Vec_WecPushLevel( vCarryRootSets );
}
Vec_BitFree( vIsCarryRoot );
return vCarryRootSets;
}
int Acec_ManCompareTwo( int * pPair0, int * pPair1 )
{
if ( pPair0[1] < pPair1[1] ) return -1;
if ( pPair0[1] > pPair1[1] ) return 1;
return 0;
}
void Acec_ManCollectInsOuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vBoxes, Vec_Int_t * vBoxRanks, Vec_Bit_t * vBoxIns, Vec_Bit_t * vBoxOuts, Vec_Int_t * vResIns, Vec_Int_t * vResOuts )
{
int i, k, iBox, iObj, Rank, RankMax = 0;
// mark box inputs/outputs
Vec_IntForEachEntry( vBoxes, iBox, i )
{
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+0), 1 );
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+1), 1 );
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+2), 1 );
Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+3), 1 );
Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+4), 1 );
}
// collect unmarked inputs/output and their ranks
Vec_IntForEachEntry( vBoxes, iBox, i )
{
for ( k = 0; k < 3; k++ )
if ( !Vec_BitEntry(vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+k)) )
Vec_IntPushTwo( vResIns, Vec_IntEntry(vAdds, 6*iBox+k), Vec_IntEntry(vBoxRanks, iBox) );
for ( k = 3; k < 5; k++ )
if ( Vec_IntEntry(vAdds, 6*iBox+k) && !Vec_BitEntry(vBoxIns, Vec_IntEntry(vAdds, 6*iBox+k)) )
Vec_IntPushTwo( vResOuts, Vec_IntEntry(vAdds, 6*iBox+k), Vec_IntEntry(vBoxRanks, iBox)-(int)(k==4) );
}
// unmark box inputs/outputs
Vec_IntForEachEntry( vBoxes, iBox, i )
{
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+0), 0 );
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+1), 0 );
Vec_BitWriteEntry( vBoxIns, Vec_IntEntry(vAdds, 6*iBox+2), 0 );
Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+3), 0 );
Vec_BitWriteEntry( vBoxOuts, Vec_IntEntry(vAdds, 6*iBox+4), 0 );
}
// normalize ranks
Vec_IntForEachEntryDouble( vResIns, iObj, Rank, k )
RankMax = Abc_MaxInt( RankMax, Rank );
Vec_IntForEachEntryDouble( vResOuts, iObj, Rank, k )
RankMax = Abc_MaxInt( RankMax, Rank );
Vec_IntForEachEntryDouble( vResIns, iObj, Rank, k )
Vec_IntWriteEntry( vResIns, k+1, 1 + RankMax - Rank );
Vec_IntForEachEntryDouble( vResOuts, iObj, Rank, k )
Vec_IntWriteEntry( vResOuts, k+1, 1 + RankMax - Rank );
// sort by rank
qsort( Vec_IntArray(vResIns), Vec_IntSize(vResIns)/2, 8, (int (*)(const void *, const void *))Acec_ManCompareTwo );
qsort( Vec_IntArray(vResOuts), Vec_IntSize(vResOuts)/2, 8, (int (*)(const void *, const void *))Acec_ManCompareTwo );
}
void Acec_ManCollectBoxSets_rec( Gia_Man_t * p, int Carry, int iRank, Vec_Int_t * vAdds, Vec_Int_t * vCarryMap, Vec_Int_t * vBoxes, Vec_Int_t * vBoxRanks )
{
int iBox = Vec_IntEntry( vCarryMap, Carry );
if ( iBox == -1 )
return;
Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+0), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+1), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
if ( Vec_IntEntry(vAdds, 6*iBox+2) )
Acec_ManCollectBoxSets_rec( p, Vec_IntEntry(vAdds, 6*iBox+2), iRank+1, vAdds, vCarryMap, vBoxes, vBoxRanks );
Vec_IntPush( vBoxes, iBox );
Vec_IntWriteEntry( vBoxRanks, iBox, iRank );
}
Vec_Wec_t * Acec_ManCollectBoxSets( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXors )
{
Vec_Int_t * vCarryMap = Acec_ManCreateCarryMap( p, vAdds );
Vec_Int_t * vCarryRoots = Acec_ManCollectCarryRoots( p, vAdds );
Vec_Int_t * vXorRoots = Acec_ManCollectXorRoots( p, vXors );
Vec_Wec_t * vBoxSets = Acec_ManCollectCarryRootSets( p, vAdds, vCarryMap, vXors, vXorRoots, vCarryRoots );
Vec_Int_t * vBoxRanks = Vec_IntStart( Vec_IntSize(vAdds)/6 );
Vec_Bit_t * vBoxIns = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vBoxOuts = Vec_BitStart( Gia_ManObjNum(p) ); int i, k, Root;
Vec_IntFree( vCarryRoots );
Vec_IntFree( vXorRoots );
// collect boxes for each carry set
assert( Vec_WecSize(vBoxSets) % 5 == 0 );
for ( i = 0; 5*i < Vec_WecSize(vBoxSets); i++ )
{
Vec_Int_t * vRoots = Vec_WecEntry( vBoxSets, 5*i+1 );
Vec_Int_t * vBoxes = Vec_WecEntry( vBoxSets, 5*i+2 );
Vec_Int_t * vIns = Vec_WecEntry( vBoxSets, 5*i+3 );
Vec_Int_t * vOuts = Vec_WecEntry( vBoxSets, 5*i+4 );
Vec_IntForEachEntry( vRoots, Root, k )
Acec_ManCollectBoxSets_rec( p, Root, 1, vAdds, vCarryMap, vBoxes, vBoxRanks );
Acec_ManCollectInsOuts( p, vAdds, vBoxes, vBoxRanks, vBoxIns, vBoxOuts, vIns, vOuts );
}
Vec_IntFree( vBoxRanks );
Vec_BitFree( vBoxIns );
Vec_BitFree( vBoxOuts );
Vec_IntFree( vCarryMap );
return vBoxSets;
}
void Acec_ManPrintRanks2( Vec_Int_t * vPairs )
{
int k, iObj, Rank;
Vec_IntForEachEntryDouble( vPairs, iObj, Rank, k )
printf( "%d ", Rank );
printf( "\n" );
}
void Acec_ManPrintRanks( Vec_Int_t * vPairs )
{
int k, iObj, Count, Rank, RankMax = 0;
Vec_Int_t * vCounts = Vec_IntStart( 100 );
Vec_IntForEachEntryDouble( vPairs, iObj, Rank, k )
{
Vec_IntFillExtra( vCounts, Rank+1, 0 );
Vec_IntAddToEntry( vCounts, Rank, 1 );
RankMax = Abc_MaxInt( RankMax, Rank );
}
Vec_IntForEachEntryStartStop( vCounts, Count, Rank, 1, RankMax+1 )
printf( "%2d=%2d ", Rank, Count );
printf( "\n" );
Vec_IntFree( vCounts );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_ManProfile( Gia_Man_t * p, int fVerbose )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
abctime clk = Abc_Clock();
Vec_Wec_t * vBoxes; int i;
Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, fVerbose );
Ree_ManRemoveTrivial( p, vAdds );
Ree_ManRemoveContained( p, vAdds );
//Ree_ManPrintAdders( vAdds, 1 );
printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
vBoxes = Acec_ManCollectBoxSets( p, vAdds, vXors );
printf( "Detected %d adder-tree%s. ", Vec_WecSize(vBoxes)/5, Vec_WecSize(vBoxes)/5 > 1 ? "s":"" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
for ( i = 0; 5*i < Vec_WecSize(vBoxes); i++ )
{
printf( "Tree %3d : ", i );
printf( "Xor = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+0)) );
printf( "Root = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+1)) );
//printf( "(Top = %5d) ", Vec_IntEntryLast(Vec_WecEntry(vBoxes,5*i+1)) );
printf( "Adder = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+2)) );
printf( "In = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+3))/2 );
printf( "Out = %4d ", Vec_IntSize(Vec_WecEntry(vBoxes,5*i+4))/2 );
printf( "\n" );
printf( " Ins: " );
Acec_ManPrintRanks( Vec_WecEntry(vBoxes,5*i+3) );
printf( " Outs: " );
Acec_ManPrintRanks( Vec_WecEntry(vBoxes,5*i+4) );
}
Vec_IntFree( vXors );
Vec_IntFree( vAdds );
Vec_WecFree( vBoxes );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds )
{
Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(p) );
int i, k;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
for ( k = 0; k < 3; k++ )
Vec_BitWriteEntry( vMarks, Vec_IntEntry(vAdds, 6*i+k), 1 );
return vMarks;
}
Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
{
int i, k, iTop, fVerbose = 0;
Vec_Int_t * vTops = Vec_IntAlloc( 1000 );
Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( p, vAdds );
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
if ( !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+3)) &&
!Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+4)) )
Vec_IntPush( vTops, i );
if ( fVerbose )
Vec_IntForEachEntry( vTops, iTop, i )
{
printf( "%4d : ", iTop );
for ( k = 0; k < 3; k++ )
printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
printf( " -> " );
for ( k = 3; k < 5; k++ )
printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
printf( "\n" );
}
Vec_BitFree( vMarks );
return vTops;
}
void Acec_ManPool( Gia_Man_t * p )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
Vec_Int_t * vTops, * vTree;
Vec_Wec_t * vTrees;
abctime clk = Abc_Clock();
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
int i, nFadds = Ree_ManCountFadds( vAdds );
printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
Ree_ManRemoveTrivial( p, vAdds );
Ree_ManRemoveContained( p, vAdds );
nFadds = Ree_ManCountFadds( vAdds );
printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Ree_ManPrintAdders( vAdds, 1 );
// detect topmost nodes
vTops = Acec_ManPoolTopMost( p, vAdds );
printf( "Detected %d topmost adder%s.\n", Vec_IntSize(vTops), Vec_IntSize(vTops) > 1 ? "s":"" );
// collect adder trees
vTrees = Gia_PolynCoreOrderArray( p, vAdds, vTops );
Vec_WecForEachLevel( vTrees, vTree, i )
printf( "Adder %5d : Tree with %5d nodes.\n", Vec_IntEntry(vTops, i), Vec_IntSize(vTree) );
Vec_WecFree( vTrees );
Vec_IntFree( vAdds );
Vec_IntFree( vTops );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

215
src/proof/acec/acecRe.c
View File

@ -69,6 +69,18 @@ void Ree_TruthPrecompute()
}
printf( "\n" );
}
void Ree_TruthPrecompute2()
{
int i, b;
for ( i = 0; i < 8; i++ )
{
word Truth = 0xE8;
for ( b = 0; b < 3; b++ )
if ( (i >> b) & 1 )
Truth = Abc_Tt6Flip( Truth, b );
printf( "%d = %X\n", i, 0xFF & (int)Truth );
}
}
/**Function*************************************************************
@ -236,10 +248,11 @@ void Ree_ManCutPrint( int * pCut, int Count, word Truth )
Abc_TtPrintHexRev( stdout, &Truth, 3 );
printf( "\n" );
}
void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData )
void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData, Vec_Int_t * vXors )
{
int fVerbose = 0;
int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[5], Count = 0;
int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[6], Count = 0;
int iXor2 = -1, iXor3 = -1;
if ( fVerbose )
printf( "Object %d\n", iObj );
Vec_IntFill( vCuts, 2, 1 );
@ -254,12 +267,16 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
continue;
Truth = TruthC = Ree_ManCutTruth(Gia_ManObj(p, iObj), pCut0, pCut1, pCut);
//assert( Truth == Ree_ObjComputeTruth(p, iObj, pCut) );
if ( Truth & 0x80 )
Truth = 0xFF & ~Truth;
if ( Truth == 0x66 && iXor2 == -1 )
iXor2 = Vec_IntSize(vCuts);
else if ( Truth == 0x69 && iXor3 == -1 )
iXor3 = Vec_IntSize(vCuts);
Vec_IntAddToEntry( vCuts, 0, 1 );
for ( c = 0; c <= pCut[0]; c++ )
Vec_IntPush( vCuts, pCut[c] );
Vec_IntPush( vCuts, Truth );
if ( Truth & 0x80 )
Truth = 0xFF & ~Truth;
Vec_IntPush( vCuts, TruthC );
if ( (Truth == 0x66 || Truth == 0x11 || Truth == 0x22 || Truth == 0x44 || Truth == 0x77) && pCut[0] == 2 )
{
assert( pCut[0] == 2 );
@ -275,6 +292,19 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
if ( fVerbose )
Ree_ManCutPrint( pCut, ++Count, TruthC );
}
if ( !vXors )
return;
if ( iXor2 > 0 )
pCut0 = Vec_IntEntryP( vCuts, iXor2 );
else if ( iXor3 > 0 )
pCut0 = Vec_IntEntryP( vCuts, iXor3 );
else
return;
Vec_IntPush( vXors, iObj );
for ( c = 1; c <= pCut0[0]; c++ )
Vec_IntPush( vXors, pCut0[c] );
if ( pCut0[0] == 2 )
Vec_IntPush( vXors, 0 );
}
/**Function*************************************************************
@ -288,9 +318,9 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
SeeAlso []
***********************************************************************/
Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbose )
{
int i, j, k, iObj, iObj2, Value, Truth, CountX, CountM, Index = 0;
int i, j, k, iObj, iObj2, Value, Truth, Truth2, CountX, CountM, Index = 0;
int nEntries = Hash_IntManEntryNum(p);
Vec_Int_t * vAdds = Vec_IntAlloc( 1000 );
Vec_Int_t * vXors = Vec_IntStart( nEntries + 1 );
@ -315,7 +345,8 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
}
Vec_IntFree( vXors );
Vec_IntFree( vMajs );
printf( "Detected %d shared cuts among %d hashed cuts.\n", Index, nEntries );
//if ( fVerbose )
// printf( "Detected %d shared cuts among %d hashed cuts.\n", Index, nEntries );
// collect nodes
vXorMap = Vec_WecStart( Index );
vMajMap = Vec_WecStart( Index );
@ -325,9 +356,9 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
if ( Index == -1 )
continue;
if ( Truth == 0x66 || Truth == 0x99 || Truth == 0x69 || Truth == 0x96 )
Vec_WecPush( vXorMap, Index, iObj );
Vec_IntPushTwo( Vec_WecEntry(vXorMap, Index), iObj, Truth );
else
Vec_WecPush( vMajMap, Index, iObj );
Vec_IntPushTwo( Vec_WecEntry(vMajMap, Index), iObj, Truth );
}
Vec_IntFree( vIndex );
// create pairs
@ -336,11 +367,22 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_Int_t * vXorOne = Vec_WecEntry( vXorMap, i );
Vec_Int_t * vMajOne = Vec_WecEntry( vMajMap, i );
Hash_IntObj_t * pObj = Hash_IntObj( p, Value );
Vec_IntForEachEntry( vXorOne, iObj, j )
Vec_IntForEachEntry( vMajOne, iObj2, k )
Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
{
int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17};
int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3;
for ( n = 0; n < 8; n++ )
if ( Truth2 == SignMaj[n] )
break;
if ( n == 8 )
for ( n = 0; n < 8; n++ )
if ( Truth2 == SignAnd[n] )
break;
assert( n < 8 );
Vec_IntPushThree( vAdds, pObj->iData0, pObj->iData1, pObj->iData2 );
Vec_IntPushTwo( vAdds, iObj, iObj2 );
Vec_IntPushThree( vAdds, iObj, iObj2, SignXor | n );
}
}
Vec_IntFree( vIndexRev );
@ -348,7 +390,7 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_WecFree( vMajMap );
return vAdds;
}
Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose )
{
Gia_Obj_t * pObj;
int * pList0, * pList1, i, nCuts = 0;
@ -367,29 +409,76 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
Vec_IntPush( vCuts, Gia_ObjId(p, pObj) );
Vec_IntPush( vCuts, 0xAA );
}
if ( pvXors ) *pvXors = Vec_IntAlloc( 1000 );
Gia_ManForEachAnd( p, pObj, i )
{
pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) );
pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) );
Ree_ManCutMerge( p, i, pList0, pList1, vTemp, pHash, vData );
Ree_ManCutMerge( p, i, pList0, pList1, vTemp, pHash, vData, pvXors ? *pvXors : NULL );
Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) );
Vec_IntAppend( vCuts, vTemp );
nCuts += Vec_IntEntry( vTemp, 0 );
}
if ( fVerbose )
printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n",
printf( "AIG nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n",
Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) );
Vec_IntFree( vTemp );
Vec_IntFree( vCuts );
vAdds = Ree_ManDeriveAdds( pHash, vData );
vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose );
if ( fVerbose )
printf( "Adds = %d. Total = %d. Hashed = %d. Hashed/Adds = %.2f.\n",
Vec_IntSize(vAdds)/5, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 5.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
printf( "Adders = %d. Total cuts = %d. Hashed cuts = %d. Hashed/Adders = %.2f.\n",
Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
Vec_IntFree( vData );
Hash_IntManStop( pHash );
return vAdds;
}
/**Function*************************************************************
Synopsis [Highlight nodes inside FAs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ree_CollectInsiders_rec( Gia_Man_t * pGia, int iObj, Vec_Bit_t * vVisited, Vec_Bit_t * vInsiders )
{
if ( Vec_BitEntry(vVisited, iObj) )
return;
Vec_BitSetEntry( vVisited, iObj, 1 );
Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId0p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId1p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
Vec_BitSetEntry( vInsiders, iObj, 1 );
}
Vec_Bit_t * Ree_CollectInsiders( Gia_Man_t * pGia, Vec_Int_t * vAdds )
{
Vec_Bit_t * vVisited = Vec_BitStart( Gia_ManObjNum(pGia) );
Vec_Bit_t * vInsiders = Vec_BitStart( Gia_ManObjNum(pGia) );
int i, Entry1, Entry2, Entry3;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
continue;
// mark inputs
Entry1 = Vec_IntEntry( vAdds, 6*i + 0 );
Entry2 = Vec_IntEntry( vAdds, 6*i + 1 );
Entry3 = Vec_IntEntry( vAdds, 6*i + 2 );
Vec_BitWriteEntry( vVisited, Entry1, 1 );
Vec_BitWriteEntry( vVisited, Entry2, 1 );
Vec_BitWriteEntry( vVisited, Entry3, 1 );
// traverse from outputs
Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
Ree_CollectInsiders_rec( pGia, Entry1, vVisited, vInsiders );
Ree_CollectInsiders_rec( pGia, Entry2, vVisited, vInsiders );
}
Vec_BitFree( vVisited );
return vInsiders;
}
/**Function*************************************************************
Synopsis []
@ -401,28 +490,80 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
// removes HAs whose AND2 is part of XOR2 without additional fanout
void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
{
Gia_Obj_t * pObjX, * pObjM;
int i, k = 0;
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
{
pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
continue;
}
memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
}
assert( k <= i );
Vec_IntShrink( vAdds, 6*k );
}
// removes HAs fully contained inside FAs
void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds )
{
Vec_Bit_t * vInsiders = Ree_CollectInsiders( p, vAdds );
int i, k = 0;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
if ( Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+4)) )
continue;
memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
}
assert( k <= i );
Vec_IntShrink( vAdds, 6*k );
Vec_BitFree( vInsiders );
}
int Ree_ManCountFadds( Vec_Int_t * vAdds )
{
int i, Count = 0;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
if ( Vec_IntEntry(vAdds, 6*i+2) != 0 )
Count++;
return Count;
}
void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose )
{
int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
//if ( Vec_IntEntry(vAdds, 6*i+2) == 0 )
// continue;
if ( !fVerbose )
continue;
printf( "%6d : ", i );
printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) );
printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) );
printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) );
printf( " -> " );
printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) );
printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) );
printf( " (%d)", Vec_IntEntry(vAdds, 6*i+5) );
printf( "\n" );
}
}
void Ree_ManComputeCutsTest( Gia_Man_t * p )
{
abctime clk = Abc_Clock();
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
int i, Count = 0;
for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
{
if ( Vec_IntEntry(vAdds, 5*i+2) == 0 )
continue;
Count++;
continue;
printf( "%6d : ", i );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+0) );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+1) );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+2) );
printf( " -> " );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) );
printf( "\n" );
}
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
int nFadds = Ree_ManCountFadds( vAdds );
Ree_ManPrintAdders( vAdds, 1 );
printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
Vec_IntFree( vAdds );
printf( "Detected %d FAs and %d HAs. ", Count, Vec_IntSize(vAdds)/5-Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

5
src/proof/acec/module.make
View File

@ -1,7 +1,10 @@
SRC += src/proof/acec/acecCore.c \
SRC += src/proof/acec/acecCl.c \
src/proof/acec/acecCore.c \
src/proof/acec/acecCo.c \
src/proof/acec/acecRe.c \
src/proof/acec/acecPa.c \
src/proof/acec/acecPo.c \
src/proof/acec/acecPool.c \
src/proof/acec/acecCover.c \
src/proof/acec/acecFadds.c \
src/proof/acec/acecOrder.c \