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

Adding dump of trivial abstraction map at the beginning in &gla -m.

This commit is contained in:
Alan Mishchenko 2017-02-25 09:49:31 -08:00
parent 06797fb611
commit 80773b9522
2 changed files with 82 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
src/opt/sbd/sbd.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "sbdInt.h"
#include "misc/vec/vecHsh.h"
ABC_NAMESPACE_IMPL_START
@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
{
int i, k, Entry = 0, Entry2, Count = 0, Below;
int Prev = Vec_IntEntry( vSet, 0 );
Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
{
assert( 2*Prev >= Entry );
if ( 2*Prev == Entry )
{
Prev = Entry;
continue;
}
Below = nVars;
Vec_IntForEachEntryStart( vSet, Entry2, k, i )
Below += Entry2;
Count += Below * (2*Prev - 1);
Prev = Entry;
}
Count += nVars * 2*Prev;
return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
}
void Sbd_CountTopos()
{
Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
Vec_Int_t * vSet = Vec_IntAlloc( 100 );
int i, k, e, Start, Stop;
Start = Hsh_VecManAdd( p, vSet );
for ( i = 1; i < 9; i++ )
{
Stop = Hsh_VecSize( p );
for ( e = Start; e < Stop; e++ )
{
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
Vec_IntClear( vSet );
Vec_IntAppend( vSet, vTemp );
for ( k = 0; k < Vec_IntSize(vSet); k++ )
{
// skip if the number of entries on this level is equal to the number of fanins on the previous level
if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
continue;
Vec_IntAddToEntry( vSet, k, 1 );
Hsh_VecManAdd( p, vSet );
Vec_IntAddToEntry( vSet, k, -1 );
}
Vec_IntPush( vSet, 1 );
Hsh_VecManAdd( p, vSet );
}
printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
if ( 0 )
{
for ( e = Stop; e < Hsh_VecSize(p); e++ )
{
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, 5) );
Vec_IntPrint( vTemp );
}
}
Start = Stop;
}
Vec_IntFree( vSet );
Hsh_VecManStop( p );
}
////////////////////////////////////////////////////////////////////////

20
src/proof/abs/absGla.c
View File

@ -1539,9 +1539,27 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
if ( pPars->fDumpVabs || pPars->fDumpMabs )
Abc_Print( 1, "%s will be dumped into file \"%s\".\n",
Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n",
pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
if ( pPars->fDumpMabs )
{
// create trivial abstraction map
Gia_Obj_t * pObj;
char * pFileName = Ga2_GlaGetFileName(p, 0);
Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
Gia_ManForEachAnd( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
Gia_AigerWrite( pAig, pFileName, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
}
Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}
// iterate unrolling