Skip to content

A
abc
Commit 548e0419 by Alan Mishchenko
Options

Updating &gla_refine to perform suffic refinement.

parent 0b8e07bd
Showing with 24 additions and 214 deletions
abclib.dsp
......@@ -3419,6 +3419,10 @@ SOURCE=.\src\aig\gia\giaAbsIter.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsOut.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsRef.c
# End Source File
# Begin Source File
......
src/aig/gia/giaAbsGla.c
......@@ -24,7 +24,6 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
#include "aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
......@@ -130,7 +129,7 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
// some lessons learned from debugging mismatches between GIA and mapped CNF
// - inputs/output of AND-node maybe PPIs (have SAT vars), but the node is not included in the abstraction
// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction
// - some logic node can be a PPI of one LUT and an internal node of another LUT
////////////////////////////////////////////////////////////////////////
......@@ -139,213 +138,6 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
{
Abc_Cex_t * pCex;
int i, f, iPiNum;
assert( pCexAbs->iPo == 0 );
// start the counter-example
pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
for ( f = 0; f <= pCexAbs->iFrame; f++ )
for ( i = 0; i < Vec_IntSize(vPis); i++ )
{
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
{
iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
}
}
// verify the counter example
if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
{
Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
else
{
Abc_Print( 1, "Counter-example verification is successful.\n" );
Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
}
return pCex;
}
/**Function*************************************************************
Synopsis [Refines gate-level abstraction using the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
{
extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
// extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
int fAddOneLayer = 1;
Abc_Cex_t * pCexNew = NULL;
Gia_Man_t * pAbs;
Aig_Man_t * pAig;
Abc_Cex_t * pCare;
Vec_Int_t * vPis, * vPPis;
int f, i, iObjId;
clock_t clk = clock();
int nOnes = 0, Counter = 0;
if ( p->vGateClasses == NULL )
{
Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
return -1;
}
// derive abstraction
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
Gia_ManStop( pAbs );
pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
if ( Gia_ManPiNum(pAbs) != pCex->nPis )
{
Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
Gia_ManStop( pAbs );
return -1;
}
if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
{
Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
// Gia_ManStop( pAbs );
// return -1;
}
// else
// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
// get inputs
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
// add missing logic
if ( fAddOneLayer )
{
Gia_Obj_t * pObj;
// check if this is a real counter-example
Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Gia_ManForEachPi( pAbs, pObj, i )
{
if ( i >= Vec_IntSize(vPis) ) // PPIs
Gia_ObjTerSimSetX( pObj );
else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachRo( pAbs, pObj, i )
{
if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( pAbs, pObj );
}
Gia_ManForEachAnd( pAbs, pObj, i )
Gia_ObjTerSimAnd( pObj );
Gia_ManForEachCo( pAbs, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( pAbs, 0 );
if ( Gia_ObjTerSimGet1(pObj) )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
// else
// Abc_Print( 1, "CEX is not real.\n" );
Gia_ManForEachObj( pAbs, pObj, i )
Gia_ObjTerSimSetC( pObj );
if ( pCexNew == NULL )
{
// grow one layer
Vec_IntForEachEntry( vPPis, iObjId, i )
{
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
}
if ( fVerbose )
{
Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
}
}
else
{
// minimize the CEX
pAig = Gia_ManToAigSimple( pAbs );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
Aig_ManStop( pAig );
if ( pCare == NULL )
Abc_Print( 1, "Counter-example minimization has failed.\n" );
// add new objects to the map
iObjId = -1;
for ( f = 0; f <= pCare->iFrame; f++ )
for ( i = 0; i < pCare->nPis; i++ )
if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
{
nOnes++;
assert( i >= Vec_IntSize(vPis) );
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
continue;
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
// Abc_Print( 1, "Adding object %d.\n", iObjId );
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
Counter++;
}
Abc_CexFree( pCare );
if ( fVerbose )
{
Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// consider the case of SAT
if ( iObjId == -1 )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
}
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Gia_ManStop( pAbs );
if ( pCexNew )
{
ABC_FREE( p->pCexSeq );
p->pCexSeq = pCexNew;
return 0;
}
// extract abstraction to include min-cut
if ( fMinCut )
Nwk_ManDeriveMinCut( p, fVerbose );
return -1;
}
/**Function*************************************************************
Synopsis [Prepares CEX and vMap for refinement.]
Description []
......
src/aig/gia/module.make
......@@ -3,6 +3,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAbsGla.c \
src/aig/gia/giaAbsGla2.c \
src/aig/gia/giaAbsIter.c \
src/aig/gia/giaAbsOut.c \
src/aig/gia/giaAbsRef.c \
src/aig/gia/giaAbsRef2.c \
src/aig/gia/giaAbsVta.c \
......
src/base/abci/abc.c
......@@ -27820,14 +27820,26 @@ usage:
***********************************************************************/
int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose );
extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose );
int iFrameStart = 0;
int fMinCut = 1;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
iFrameStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iFrameStart < 0 )
goto usage;
break;
case 'm':
fMinCut ^= 1;
break;
......@@ -27855,14 +27867,15 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" );
return 1;
}
pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose );
pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, fVerbose );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &gla_refine [-mvh]\n" );
Abc_Print( -2, "usage: &gla_refine [-F num] [-vh]\n" );
Abc_Print( -2, "\t refines the pre-computed gate map using the counter-example\n" );
Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
Abc_Print( -2, "\t-F num : starting timeframe for suffix refinement [default = %d]\n", iFrameStart );
// Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment