summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-12-05 09:49:02 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-12-05 09:49:02 -0800
commite5d8335268eddf7d1bade6bfc8f91da677294674 (patch)
tree03950cc9b78395c01eebb18f8fdae7738f3884d2 /src/aig
parent1743979b75850820f3b8aec29a7191754b1bd2bd (diff)
downloadabc-e5d8335268eddf7d1bade6bfc8f91da677294674.tar.gz
abc-e5d8335268eddf7d1bade6bfc8f91da677294674.tar.bz2
abc-e5d8335268eddf7d1bade6bfc8f91da677294674.zip
Experiments with AIG-based simulation.
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h16
-rw-r--r--src/aig/gia/giaCSat.c4
-rw-r--r--src/aig/gia/giaSim.c235
3 files changed, 244 insertions, 11 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 20d64dfe..039628bf 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -203,6 +203,8 @@ struct Gia_Man_t_
int fBuiltInSim;
int iPatsPi;
int nSimWords;
+ int iPastPiMax;
+ int nSimWordsMax;
Vec_Wrd_t * vSims;
Vec_Wrd_t * vSimsPi;
Vec_Int_t * vClassOld;
@@ -692,7 +694,12 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
}
if ( p->fBuiltInSim )
+ {
+ Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
+ Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
+ pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) );
+ }
if ( p->vSuppWords )
Gia_ManQuantSetSuppAnd( p, pObj );
return Gia_ObjId( p, pObj ) << 1;
@@ -1208,6 +1215,8 @@ extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia );
extern void Cbs_ManStop( Cbs_Man_t * p );
extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
+extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p );
/*=== giaCTas.c ============================================================*/
extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCof.c =============================================================*/
@@ -1504,8 +1513,11 @@ extern void Gia_ManSimInfoTransfer( Gia_ManSim_t * p );
extern void Gia_ManSimulateRound( Gia_ManSim_t * p );
extern void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs );
extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj );
-extern int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 );
-extern int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs );
+extern int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 );
+extern int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 );
+extern void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 );
+extern void Gia_ManBuiltInSimResimulate( Gia_Man_t * p );
+extern int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat );
/*=== giaSpeedup.c ============================================================*/
extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 5f516e21..31f32e30 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -134,6 +134,10 @@ void Cbs_SetDefaultParams( Cbs_Par_t * pPars )
pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
pPars->fVerbose = 1; // print detailed statistics
}
+void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num )
+{
+ p->Pars.nBTLimit = Num;
+}
/**Function*************************************************************
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index aba7f712..192184c8 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "gia.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -760,51 +761,102 @@ void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut )
SeeAlso []
***********************************************************************/
+static inline word * Gia_ManBuiltInDataPi( Gia_Man_t * p, int iCiId )
+{
+ return Vec_WrdEntryP( p->vSimsPi, p->nSimWords * iCiId );
+}
static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
+static inline void Gia_ManBuiltInDataPrint( Gia_Man_t * p, int iObj )
+{
+// printf( "Obj %6d : ", iObj ); Extra_PrintBinary( stdout, Gia_ManBuiltInData(p, iObj), p->nSimWords * 64 ); printf( "\n" );
+}
void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs )
{
int i, k;
assert( !p->fBuiltInSim );
assert( Gia_ManAndNum(p) == 0 );
p->fBuiltInSim = 1;
+ p->iPatsPi = 0;
+ p->iPastPiMax = 0;
p->nSimWords = nWords;
+ p->nSimWordsMax = 8;
+ Gia_ManRandomW( 1 );
+ // init PI care info
+ p->vSimsPi = Vec_WrdAlloc( p->nSimWords * Gia_ManCiNum(p) );
+ Vec_WrdFill( p->vSimsPi, p->nSimWords * Gia_ManCiNum(p), 0 );
+ // init object sim info
p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
Vec_WrdFill( p->vSims, p->nSimWords, 0 );
- Gia_ManRandomW( 1 );
for ( i = 0; i < Gia_ManCiNum(p); i++ )
for ( k = 0; k < p->nSimWords; k++ )
Vec_WrdPush( p->vSims, Gia_ManRandomW(0) );
}
-void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj )
+void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj )
{
- Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); int w;
+ word * pInfo = Gia_ManBuiltInData( p, iObj );
word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
- word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); int w;
+ word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) );
assert( p->fBuiltInSim );
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
- Vec_WrdPush( p->vSims, ~(pInfo0[w] | pInfo1[w]) );
+ pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
else
for ( w = 0; w < p->nSimWords; w++ )
- Vec_WrdPush( p->vSims, ~pInfo0[w] & pInfo1[w] );
+ pInfo[w] = ~pInfo0[w] & pInfo1[w];
}
else
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
- Vec_WrdPush( p->vSims, pInfo0[w] & ~pInfo1[w] );
+ pInfo[w] = pInfo0[w] & ~pInfo1[w];
else
for ( w = 0; w < p->nSimWords; w++ )
- Vec_WrdPush( p->vSims, pInfo0[w] & pInfo1[w] );
+ pInfo[w] = pInfo0[w] & pInfo1[w];
}
assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords );
}
-int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 )
+void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj )
+{
+ int w;
+ for ( w = 0; w < p->nSimWords; w++ )
+ Vec_WrdPush( p->vSims, 0 );
+ Gia_ManBuiltInSimPerformInt( p, iObj );
+}
+
+void Gia_ManBuiltInSimResimulateCone_rec( Gia_Man_t * p, int iObj )
+{
+ Gia_Obj_t * pObj;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsCi(pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
+ Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
+ Gia_ManBuiltInSimPerformInt( p, iObj );
+}
+void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 )
+{
+ Gia_ManIncrementTravId( p );
+ Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit0) );
+ Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit1) );
+}
+void Gia_ManBuiltInSimResimulate( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj; int iObj;
+ Gia_ManForEachAnd( p, pObj, iObj )
+ Gia_ManBuiltInSimPerformInt( p, iObj );
+}
+
+int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
{
word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
@@ -818,28 +870,193 @@ int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 )
if ( Abc_LitIsCompl(iLit0) )
{
if ( Abc_LitIsCompl(iLit1) )
+ {
for ( w = 0; w < p->nSimWords; w++ )
if ( ~pInfo0[w] & ~pInfo1[w] )
return 1;
+ }
else
+ {
for ( w = 0; w < p->nSimWords; w++ )
if ( ~pInfo0[w] & pInfo1[w] )
return 1;
+ }
}
else
{
if ( Abc_LitIsCompl(iLit1) )
+ {
for ( w = 0; w < p->nSimWords; w++ )
if ( pInfo0[w] & ~pInfo1[w] )
return 1;
+ }
else
+ {
for ( w = 0; w < p->nSimWords; w++ )
if ( pInfo0[w] & pInfo1[w] )
return 1;
+ }
}
return 0;
}
+int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
+{
+ word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
+ word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
+ assert( p->fBuiltInSim );
+
+// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
+// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
+// Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
+// printf( "\n" );
+
+ if ( Abc_LitIsCompl(iLit0) )
+ {
+ if ( Abc_LitIsCompl(iLit1) )
+ {
+ for ( w = 0; w < p->nSimWords; w++ )
+ if ( ~pInfo0[w] != ~pInfo1[w] )
+ return 0;
+ }
+ else
+ {
+ for ( w = 0; w < p->nSimWords; w++ )
+ if ( ~pInfo0[w] != pInfo1[w] )
+ return 0;
+ }
+ }
+ else
+ {
+ if ( Abc_LitIsCompl(iLit1) )
+ {
+ for ( w = 0; w < p->nSimWords; w++ )
+ if ( pInfo0[w] != ~pInfo1[w] )
+ return 0;
+ }
+ else
+ {
+ for ( w = 0; w < p->nSimWords; w++ )
+ if ( pInfo0[w] != pInfo1[w] )
+ return 0;
+ }
+ }
+ return 1;
+}
+int Gia_ManBuiltInSimPack( Gia_Man_t * p, Vec_Int_t * vPat )
+{
+ int i, k, iLit;
+ assert( Vec_IntSize(vPat) > 0 );
+ //printf( "%d ", Vec_IntSize(vPat) );
+ for ( i = 0; i < p->iPatsPi; i++ )
+ {
+ Vec_IntForEachEntry( vPat, iLit, k )
+ if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), i) &&
+ Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), i) == Abc_LitIsCompl(iLit) )
+ break;
+ if ( k == Vec_IntSize(vPat) )
+ return i; // success
+ }
+ return -1; // failure
+}
+// adds PI pattern to storage; the pattern comes in terms of CiIds
+int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat )
+{
+ int Period = 0xF;
+ int fOverflow = p->iPatsPi == 64 * p->nSimWords && p->nSimWords == p->nSimWordsMax;
+ int k, iLit, iPat = Gia_ManBuiltInSimPack( p, vPat );
+ if ( iPat == -1 )
+ {
+ if ( fOverflow )
+ {
+ if ( (p->iPastPiMax & Period) == 0 )
+ Gia_ManBuiltInSimResimulate( p );
+ iPat = p->iPastPiMax;
+ //if ( p->iPastPiMax == 64 * p->nSimWordsMax - 1 )
+ // printf( "Completed the cycle.\n" );
+ p->iPastPiMax = p->iPastPiMax == 64 * p->nSimWordsMax - 1 ? 0 : p->iPastPiMax + 1;
+ }
+ else
+ {
+ if ( p->iPatsPi && (p->iPatsPi & Period) == 0 )
+ Gia_ManBuiltInSimResimulate( p );
+ if ( p->iPatsPi == 64 * p->nSimWords )
+ {
+ Vec_Wrd_t * vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSims) );
+ word Data; int w, Count = 0, iObj = 0;
+ Vec_WrdForEachEntry( p->vSims, Data, w )
+ {
+ Vec_WrdPush( vTemp, Data );
+ if ( ++Count == p->nSimWords )
+ {
+ Gia_Obj_t * pObj = Gia_ManObj(p, iObj++);
+ if ( Gia_ObjIsCi(pObj) )
+ Vec_WrdPush( vTemp, Gia_ManRandomW(0) ); // Vec_WrdPush( vTemp, 0 );
+ else if ( Gia_ObjIsAnd(pObj) )
+ Vec_WrdPush( vTemp, pObj->fPhase ? ~(word)0 : 0 );
+ else
+ Vec_WrdPush( vTemp, 0 );
+ Count = 0;
+ }
+ }
+ assert( iObj == Gia_ManObjNum(p) );
+ Vec_WrdFree( p->vSims );
+ p->vSims = vTemp;
+
+ vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSimsPi) );
+ Count = 0;
+ Vec_WrdForEachEntry( p->vSimsPi, Data, w )
+ {
+ Vec_WrdPush( vTemp, Data );
+ if ( ++Count == p->nSimWords )
+ {
+ Vec_WrdPush( vTemp, 0 );
+ Count = 0;
+ }
+ }
+ Vec_WrdFree( p->vSimsPi );
+ p->vSimsPi = vTemp;
+
+ // update the word count
+ p->nSimWords++;
+ assert( Vec_WrdSize(p->vSims) == p->nSimWords * Gia_ManObjNum(p) );
+ assert( Vec_WrdSize(p->vSimsPi) == p->nSimWords * Gia_ManCiNum(p) );
+ //printf( "Resizing to %d words.\n", p->nSimWords );
+ }
+ iPat = p->iPatsPi++;
+ }
+ }
+ assert( iPat >= 0 && iPat < p->iPatsPi );
+ // add literals
+ if ( fOverflow )
+ {
+ int iVar;
+ Vec_IntForEachEntry( &p->vSuppVars, iVar, k )
+ if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, iVar), iPat) )
+ Abc_TtXorBit(Gia_ManBuiltInDataPi(p, iVar), iPat);
+ Vec_IntForEachEntry( vPat, iLit, k )
+ {
+ if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
+ Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
+ Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
+ }
+ }
+ else
+ {
+ Vec_IntForEachEntry( vPat, iLit, k )
+ {
+ if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat) )
+ assert( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) != Abc_LitIsCompl(iLit) );
+ else
+ {
+ if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
+ Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
+ Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
+ }
+ }
+ }
+ return 1;
+}
/**Function*************************************************************