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

New SAT-based optimization package.

This commit is contained in:
Alan Mishchenko 2016-11-27 11:56:40 -08:00
parent de71ef44cd
commit 53adc97675
2 changed files with 376 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

93
src/opt/sbd/sbdCore.c
View File

@ -48,6 +48,7 @@ struct Sbd_Man_t_
Vec_Int_t * vTfo; // TFO (excludes node, includes roots)
Vec_Int_t * vLeaves; // leaves (TFI leaves + extended leaves)
Vec_Int_t * vTfi; // TFI (TFI + node + extended TFI)
Vec_Int_t * vDivs; // divisors
Vec_Int_t * vCounts[2]; // counters of zeros and ones
};
@ -76,7 +77,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
{
memset( pPars, 0, sizeof(Sbd_Par_t) );
pPars->nLutSize = 4; // target LUT size
pPars->nTfoLevels = 4; // the number of TFO levels (windowing)
pPars->nTfoLevels = 3; // the number of TFO levels (windowing)
pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
pPars->nWinSizeMax = 0; // maximum window size (windowing)
pPars->nBTLimit = 0; // maximum number of SAT conflicts
@ -102,6 +103,7 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked
Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage
Vec_Int_t * vNodes, * vNodes0, * vNodes1;
Vec_Bit_t * vPoDrivers = Vec_BitStart( Gia_ManObjNum(p) );
int i, k, k2, Id, Fan;
Gia_ManLevelNum( p );
Gia_ManCreateRefs( p );
@ -112,13 +114,15 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
Vec_IntGrow( vNodes, 1 );
Vec_IntPush( vNodes, Id );
}
Gia_ManForEachCoDriverId( p, Id, i )
Vec_BitWriteEntry( vPoDrivers, Id, 1 );
Gia_ManForEachAndId( p, Id )
{
int fAlwaysRoot = Gia_ObjRefNumId(p, Id) >= nTfoFanMax;
int fAlwaysRoot = Vec_BitEntry(vPoDrivers, Id) || (Gia_ObjRefNumId(p, Id) >= nTfoFanMax);
vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) );
vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) );
vNodes = Vec_WecEntry( vTemp, Id );
Vec_IntTwoMerge2( vNodes, vNodes0, vNodes1 );
Vec_IntTwoMerge2( vNodes0, vNodes1, vNodes );
k2 = 0;
Vec_IntForEachEntry( vNodes, Fan, k )
{
@ -127,10 +131,16 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan );
}
Vec_IntShrink( vNodes, k2 );
Vec_IntPush( vNodes, Id );
if ( fAlwaysRoot )
Vec_WecPush( vTfos, Id, Abc_Var2Lit(Id, 1) );
else
Vec_IntPush( vNodes, Id );
}
Vec_WecFree( vTemp );
Vec_BitFree( vPoDrivers );
// print the results
if ( 1 )
Vec_WecForEachLevel( vTfos, vNodes, i )
{
if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
@ -139,8 +149,8 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
Vec_IntForEachEntry( vNodes, Fan, k )
printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" );
printf( "\n" );
}
return vTfos;
}
@ -171,6 +181,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
p->vCover = Vec_IntStart( 100 );
p->vLeaves = Vec_IntAlloc( Gia_ManCiNum(pGia) );
p->vTfi = Vec_IntAlloc( Gia_ManAndNum(pGia) );
p->vDivs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
p->vCounts[0] = Vec_IntAlloc( 100 );
p->vCounts[1] = Vec_IntAlloc( 100 );
// start input cuts
@ -199,8 +210,10 @@ void Sbd_ManStop( Sbd_Man_t * p )
Vec_IntFree( p->vCover );
Vec_IntFree( p->vLeaves );
Vec_IntFree( p->vTfi );
Vec_IntFree( p->vDivs );
Vec_IntFree( p->vCounts[0] );
Vec_IntFree( p->vCounts[1] );
ABC_FREE( p );
}
@ -234,20 +247,38 @@ void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node )
Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
Vec_IntPush( p->vTfi, Node );
// simulate
Abc_TtAndCompl( Sbd_ObjSim0(p, Node),
Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
p->pPars->nWords );
if ( pObj->fMark0 )
Abc_TtAndCompl( Sbd_ObjSim1(p, Node),
Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
if ( Gia_ObjIsXor(pObj) )
{
Abc_TtXor( Sbd_ObjSim0(p, Node),
Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
p->pPars->nWords,
Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
if ( pObj->fMark0 )
Abc_TtXor( Sbd_ObjSim1(p, Node),
Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
p->pPars->nWords,
Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
}
else
{
Abc_TtAndCompl( Sbd_ObjSim0(p, Node),
Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
p->pPars->nWords );
if ( pObj->fMark0 )
Abc_TtAndCompl( Sbd_ObjSim1(p, Node),
Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
p->pPars->nWords );
}
}
void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
{
int iObj0 = Gia_ObjFaninId0(Gia_ManObj(p->pGia, Node), Node);
int iObj1 = Gia_ObjFaninId1(Gia_ManObj(p->pGia, Node), Node);
Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node);
int iObj0 = Gia_ObjFaninId0(pNode, Node);
int iObj1 = Gia_ObjFaninId1(pNode, Node);
word * pCtrl = Sbd_ObjSim2(p, Node);
word * pCtrl0 = Sbd_ObjSim2(p, iObj0);
word * pCtrl1 = Sbd_ObjSim2(p, iObj1);
@ -255,10 +286,13 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
word * pSims0 = Sbd_ObjSim0(p, iObj0);
word * pSims1 = Sbd_ObjSim0(p, iObj1);
int w;
// printf( "Node %2d : %d %d\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
for ( w = 0; w < p->pPars->nWords; w++ )
{
pCtrl0[w] = pCtrl[w] & (pSims[w] | pSims1[w]);
pCtrl1[w] = pCtrl[w] & (pSims[w] | pSims0[w] | (~pSims0[w] & ~pSims1[w]));
word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w];
word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w];
pCtrl0[w] = pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
pCtrl1[w] = pCtrl[w] & (pSims[w] | Sim0);
}
}
void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
@ -269,11 +303,14 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
Vec_IntClear( p->vLeaves );
Vec_IntClear( p->vTfi );
Vec_IntClear( p->vDivs );
// simulate TFI cone
Gia_ManIncrementTravId( p->pGia );
Sbd_ManWindowSim_rec( p, Pivot );
p->nTfiLeaves = Vec_IntSize( p->vLeaves );
p->nTfiNodes = Vec_IntSize( p->vTfi );
Vec_IntAppend( p->vDivs, p->vLeaves );
Vec_IntAppend( p->vDivs, p->vTfi );
// simulate node
Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
@ -282,7 +319,7 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
{
Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1;
if ( Abc_LitIsCompl(Node) )
Sbd_ManWindowSim_rec( p, Node );
Sbd_ManWindowSim_rec( p, Abc_Lit2Var(Node) );
}
// remove marks
Gia_ManObj(p->pGia, Pivot)->fMark0 = 0;
@ -292,9 +329,9 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
Vec_IntForEachEntry( p->vTfo, Node, i )
if ( Abc_LitIsCompl(Node) ) // root
Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Node), Sbd_ObjSim1(p, Node), p->pPars->nWords );
// propagate controlability to TFI
for ( i = p->nTfiNodes; i >= 0 && (Node = Vec_IntEntry(p->vTfi, i)); i-- )
Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords );
// propagate controlability to fanins for the TFI nodes starting from the pivot
for ( i = p->nTfiLeaves + p->nTfiNodes - 1; i >= p->nTfiLeaves && ((Node = Vec_IntEntry(p->vDivs, i)), 1); i-- )
Sbd_ManPropagateControl( p, Node );
}
@ -319,11 +356,11 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
for ( k = 0; k < p->pPars->nWords * 64; k++ )
{
printf( "%3d : ", k );
Vec_IntForEachEntry( p->vTfi, Id, i )
Vec_IntForEachEntry( p->vDivs, Id, i )
{
word * pSims = Sbd_ObjSim0( p, Id );
word * pCtrl = Sbd_ObjSim2( p, Id );
if ( i == Vec_IntSize(p->vTfi)-1 )
if ( i == Vec_IntSize(p->vDivs)-1 )
{
if ( Abc_TtGetBit(pCtrl, k) )
Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
@ -335,15 +372,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
}
// covering table
printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) );
Vec_IntForEachEntry( p->vCounts[0], Bit0, k0 )
Vec_IntForEachEntry( p->vCounts[1], Bit1, k1 )
Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, 5 )
Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, 5 )
{
printf( "%3d %3d : ", Bit0, Bit1 );
Vec_IntForEachEntry( p->vTfi, Id, i )
Vec_IntForEachEntry( p->vDivs, Id, i )
{
word * pSims = Sbd_ObjSim0( p, Id );
word * pCtrl = Sbd_ObjSim2( p, Id );
if ( i == Vec_IntSize(p->vTfi)-1 )
if ( i == Vec_IntSize(p->vDivs)-1 )
printf( " " );
printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' );
}
@ -512,9 +549,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
if ( Sbd_ManComputeCut( p, Pivot ) )
continue;
printf( "Looking at node %d\n", Pivot );
Sbd_ManWindow( p, Pivot );
if ( Sbd_ManExplore( p, Pivot, pCut, &Truth ) )
Sbd_ManImplement( p, Pivot, pCut, Truth );
break;
}
pNew = Sbd_ManDerive( pGia, p->vMirrors );
Sbd_ManStop( p );

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