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

Created new abstraction package from the code that was all over the place.

This commit is contained in:
Alan Mishchenko 2012-09-15 23:27:46 -07:00
parent ec95f569dd
commit 69bbfa9856
36 changed files with 2273 additions and 3585 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Makefile
View File

@ -23,6 +23,7 @@ MODULES := \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/proof/abs \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/python

168
abclib.dsp
View File

@ -3223,26 +3223,6 @@ SOURCE=.\src\aig\saig\saig.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsCba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsPba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsStart.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsVfa.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigBmc.c
# End Source File
# Begin Source File
@ -3279,18 +3259,6 @@ SOURCE=.\src\aig\saig\saigDup.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigGlaCba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigGlaPba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigGlaPba2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigHaig.c
# End Source File
# Begin Source File
@ -3327,10 +3295,6 @@ SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigRefSat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigRetFwd.c
# End Source File
# Begin Source File
@ -3347,14 +3311,6 @@ SOURCE=.\src\aig\saig\saigScl.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigSimExt.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigSimExt2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigSimFast.c
# End Source File
# Begin Source File
@ -3403,54 +3359,6 @@ SOURCE=.\src\aig\gia\gia.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbs.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsGla.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsGla2.c
# End Source File
# Begin Source File
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\giaAbsPth.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsRef.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsRef.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsRef2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsRef2.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAbsVta.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAig.c
# End Source File
# Begin Source File
@ -4398,6 +4306,82 @@ SOURCE=.\src\proof\ssw\sswSweep.c
SOURCE=.\src\proof\ssw\sswUnique.c
# End Source File
# End Group
# Begin Group "abs"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\proof\abs\abs.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\abs.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absDup.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absGla.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absGlaOld.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absIter.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absOldCex.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absOldRef.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absOldSat.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absOldSim.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absOut.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absPth.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absRef.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absRef.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absRef2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absRef2.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absVta.c
# End Source File
# End Group
# End Group
# End Group
# Begin Group "Header Files"

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

@ -33,17 +33,14 @@
#include "misc/vec/vec.h"
#include "misc/util/utilCex.h"
#include "giaAbs.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
#define GIA_NONE 0x1FFFFFFF
#define GIA_VOID 0x0FFFFFFF
@ -208,41 +205,6 @@ struct Gia_ParSim_t_
int iOutFail; // index of the failed output
};
// abstraction parameters
typedef struct Gia_ParVta_t_ Gia_ParVta_t;
struct Gia_ParVta_t_
{
int nFramesMax; // maximum frames
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nLearnedMax; // max number of learned clauses
int nLearnedStart; // max number of learned clauses
int nLearnedDelta; // delta increase of learned clauses
int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
int nRatioMax; // restart when the number of abstracted object is more than this
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers
int fUseSkip; // skip proving intermediate timeframes
int fUseSimple; // use simple CNF construction
int fSkipHash; // skip hashing CNF while unrolling
int fUseFullProof; // use full proof for UNSAT cores
int fDumpVabs; // dumps the abstracted model
int fDumpMabs; // dumps the original AIG with abstraction map
int fCallProver; // calls the prover
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
int fVeryVerbose; // print additional information
int iFrame; // the number of frames covered
int iFrameProved; // the number of frames proved
int nFramesNoChange; // the number of last frames without changes
int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
};
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; }
static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); }
@ -717,26 +679,6 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== giaAbs.c ===========================================================*/
extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars );
Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
/*=== giaAbsGla.c ===========================================================*/
extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
extern int Ga2_ManPerform( Gia_Man_t * p, Gia_ParVta_t * pPars );
/*=== giaAbsVta.c ===========================================================*/
extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
@ -800,9 +742,6 @@ extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );

746
src/aig/gia/giaAbs.c
View File

@ -1,746 +0,0 @@
/**CFile****************************************************************
FileName [giaAbs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Counter-example-guided abstraction refinement.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p )
{
memset( p, 0, sizeof(Gia_ParAbs_t) );
p->Algo = 0; // algorithm: CBA
p->nFramesMax = 10; // timeframes for PBA
p->nConfMax = 10000; // conflicts for PBA
p->fDynamic = 1; // dynamic unfolding for PBA
p->fConstr = 0; // use constraints
p->nFramesBmc = 250; // timeframes for BMC
p->nConfMaxBmc = 5000; // conflicts for BMC
p->nStableMax = 1000000; // the number of stable frames to quit
p->nRatio = 10; // ratio of flops to quit
p->nBobPar = 1000000; // the number of frames before trying to quit
p->fUseBdds = 0; // use BDDs to refine abstraction
p->fUseDprove = 0; // use 'dprove' to refine abstraction
p->fUseStart = 1; // use starting frame
p->fVerbose = 0; // verbose output
p->fVeryVerbose= 0; // printing additional information
p->Status = -1; // the problem status
p->nFramesDone = -1; // the number of rames covered
}
/**Function*************************************************************
Synopsis [Transform flop list into flop map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops )
{
Vec_Int_t * vFlopClasses;
int i, Entry;
vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
Vec_IntForEachEntry( vFlops, Entry, i )
Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
return vFlopClasses;
}
/**Function*************************************************************
Synopsis [Transform flop map into flop list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
{
Vec_Int_t * vFlops;
int i, Entry;
vFlops = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry )
Vec_IntPush( vFlops, i );
return vFlops;
}
/**Function*************************************************************
Synopsis [Starts abstraction by computing latch map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
{
Vec_Int_t * vFlops;
Aig_Man_t * pNew;
if ( pGia->vFlopClasses != NULL )
{
printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" );
Vec_IntFreeP( &pGia->vFlopClasses );
}
pNew = Gia_ManToAig( pGia, 0 );
vFlops = Saig_ManCexAbstractionFlops( pNew, pPars );
pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
Aig_ManStop( pNew );
if ( vFlops )
{
pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
Vec_IntFree( vFlops );
}
}
/**Function*************************************************************
Synopsis [Refines abstraction using the latch map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
{
Aig_Man_t * pNew;
Vec_Int_t * vFlops;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" );
return -1;
}
pNew = Gia_ManToAig( pGia, 0 );
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
{
pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
Vec_IntFree( vFlops );
Aig_ManStop( pNew );
return 0;
}
Vec_IntFree( pGia->vFlopClasses );
pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
Vec_IntFree( vFlops );
Aig_ManStop( pNew );
return -1;
}
/**Function*************************************************************
Synopsis [Transform flop list into flop map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew )
{
Vec_Int_t * vSelected;
int i, Entry;
vSelected = Vec_IntAlloc( Vec_IntSize(vFlopsNew) );
Vec_IntForEachEntry( vFlopsNew, Entry, i )
Vec_IntPush( vSelected, Vec_IntEntry(vFlops, Entry) );
return vSelected;
}
/**Function*************************************************************
Synopsis [Adds flops that should be present in the abstraction.]
Description [The second argument (vAbsFfsToAdd) is the array of numbers
of previously abstrated flops (flops replaced by PIs in the abstracted model)
that should be present in the abstraction as real flops.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd )
{
Vec_Int_t * vMapEntries;
int i, Entry, iFlopNum;
// map previously abstracted flops into their original numbers
vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry == 0 )
Vec_IntPush( vMapEntries, i );
// add these flops as real flops
Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
{
iFlopNum = Vec_IntEntry( vMapEntries, Entry );
assert( Vec_IntEntry( vFlopClasses, iFlopNum ) == 0 );
Vec_IntWriteEntry( vFlopClasses, iFlopNum, 1 );
}
Vec_IntFree( vMapEntries );
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
{
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vAbsFfsToAdd, * vAbsFfsToAddBest;
// check if flop classes are given
if ( pGia->vFlopClasses == NULL )
{
Abc_Print( 0, "Initial flop map is not given. Trivial abstraction is assumed.\n" );
pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
}
// derive abstraction
pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses );
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
// refine abstraction using CBA
vAbsFfsToAdd = Saig_ManCbaPerform( pAig, Gia_ManPiNum(pGia), p );
if ( vAbsFfsToAdd == NULL ) // found true CEX
{
assert( pAig->pSeqModel != NULL );
printf( "Refinement did not happen. Discovered a true counter-example.\n" );
printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) );
// derive new counter-example
pOrig = Gia_ManToAigSimple( pGia );
pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel );
Aig_ManStop( pOrig );
Aig_ManStop( pAig );
return 0;
}
// select the most useful flops among those to be added
if ( p->nFfToAddMax > 0 && Vec_IntSize(vAbsFfsToAdd) > p->nFfToAddMax )
{
// compute new flops
Aig_Man_t * pAigBig = Gia_ManToAigSimple( pGia );
vAbsFfsToAddBest = Saig_ManCbaFilterFlops( pAigBig, pAig->pSeqModel, pGia->vFlopClasses, vAbsFfsToAdd, p->nFfToAddMax );
Aig_ManStop( pAigBig );
assert( Vec_IntSize(vAbsFfsToAddBest) == p->nFfToAddMax );
if ( p->fVerbose )
printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vAbsFfsToAdd), Vec_IntSize(vAbsFfsToAddBest) );
// update
Vec_IntFree( vAbsFfsToAdd );
vAbsFfsToAdd = vAbsFfsToAddBest;
}
Aig_ManStop( pAig );
// update flop classes
Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
Vec_IntFree( vAbsFfsToAdd );
if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0, 0 );
return -1;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
int RetValue;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
return 0;
}
// derive abstraction
pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, nTimeLimit, fVerbose, piFrame );
// derive new classes
if ( pAig->pSeqModel == NULL )
{
// check if there is no timeout
if ( vFlopsNew != NULL )
{
// the problem is UNSAT
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
Vec_IntFree( pGia->vFlopClasses );
pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
Vec_IntFree( vSelected );
Vec_IntFree( vFlopsNew );
Vec_IntFree( vFlops );
}
RetValue = -1;
}
else if ( vFlopsNew == NULL )
{
// found real counter-example
assert( pAig->pSeqModel != NULL );
printf( "Refinement did not happen. Discovered a true counter-example.\n" );
printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) );
// derive new counter-example
pOrig = Gia_ManToAigSimple( pGia );
pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel );
Aig_ManStop( pOrig );
RetValue = 0;
}
else
{
// found counter-eample for the abstracted model
// update flop classes
Vec_Int_t * vAbsFfsToAdd = vFlopsNew;
Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
Vec_IntFree( vAbsFfsToAdd );
RetValue = -1;
}
Aig_ManStop( pAig );
if ( fVerbose )
Gia_ManPrintStats( pGia, 0, 0 );
return RetValue;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
{
extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
Aig_Man_t * pAig;
// check if flop classes are given
if ( pGia->vGateClasses == NULL )
Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
else
{
Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
vGateClassesOld = pGia->vGateClasses; pGia->vGateClasses = NULL;
fNaiveCnf = 1;
}
// perform abstraction
p->iFrame = -1;
pAig = Gia_ManToAigSimple( pGia );
assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose, &p->iFrame );
Aig_ManStop( pAig );
// update the map
Vec_IntFreeP( &vGateClassesOld );
pGia->vGateClasses = vGateClasses;
if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0, 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
{
extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
extern Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Gia_Man_t * pGiaAbs;
Aig_Man_t * pAig;
// check if flop classes are given
if ( pGia->vGateClasses == NULL )
{
Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
pAig = Gia_ManToAigSimple( pGia );
}
else
{
Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
pAig = Gia_ManToAigSimple( pGiaAbs );
Gia_ManStop( pGiaAbs );
}
// perform abstraction
if ( fNewSolver )
vGateClasses = Aig_Gla3ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
else
vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
Aig_ManStop( pAig );
// update the BMC depth
if ( vGateClasses )
p->iFrame = p->nFramesMax;
// update the abstraction map (hint: AIG and GIA have one-to-one obj ID match)
if ( pGia->vGateClasses && vGateClasses )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachObj1( pGia, pObj, i )
{
if ( !~pObj->Value )
continue;
if ( !Vec_IntEntry(pGia->vGateClasses, i) )
continue;
// this obj was abstracted before
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) );
// if corresponding AIG object is not abstracted, remove abstraction
if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) )
{
Vec_IntWriteEntry( pGia->vGateClasses, i, 0 );
Counter++;
}
}
Vec_IntFree( vGateClasses );
if ( p->fVerbose )
Abc_Print( 1, "Repetition of abstraction removed %d entries from the old abstraction map.\n", Counter );
}
else
{
Vec_IntFreeP( &pGia->vGateClasses );
pGia->vGateClasses = vGateClasses;
}
// clean up the abstraction map
if ( pGia->vGateClasses )
{
pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
Gia_ManStop( pGiaAbs );
}
if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0, 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Converting VTA vector to GLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
{
Gia_Obj_t * pObj;
Vec_Int_t * vGla;
int nObjMask, nObjs = Gia_ManObjNum(p);
int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
// get the bitmask
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vGla = Vec_IntStart( nObjs );
Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
{
pObj = Gia_ManObj( p, (Entry & nObjMask) );
assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 );
}
Vec_IntWriteEntry( vGla, 0, nFrames );
return vGla;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to VTA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
{
Vec_Int_t * vVta;
int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
int i, k, j, Entry, Counter, nGlaSize;
//. get the GLA size
nGlaSize = Vec_IntSum(vGla);
// get the bitmask
nObjBits = Abc_Base2Log(nObjs);
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vVta = Vec_IntAlloc( 1000 );
Vec_IntPush( vVta, nFrames );
Counter = nFrames + 2;
for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
Vec_IntPush( vVta, Counter );
for ( i = 0; i < nFrames; i++ )
for ( k = 0; k <= i; k++ )
Vec_IntForEachEntry( vGla, Entry, j )
if ( Entry )
Vec_IntPush( vVta, (k << nObjBits) | j );
Counter = Vec_IntEntry(vVta, nFrames+1);
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
return vVta;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to FLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
if ( Gia_ObjIsRo(p, pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
}
/**Function*************************************************************
Synopsis [Converting FLA vector to GLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
{
Vec_Int_t * vGla;
Gia_Obj_t * pObj;
int i;
// mark const0 and relevant CI objects
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetTravIdCurrent(p, pObj);
Gia_ManForEachRo( p, pObj, i )
if ( !Vec_IntEntry(vFla, i) )
Gia_ObjSetTravIdCurrent(p, pObj);
// label all objects reachable from the PO and selected flops
vGla = Vec_IntStart( Gia_ManObjNum(p) );
Vec_IntWriteEntry( vGla, 0, 1 );
Gia_ManForEachPo( p, pObj, i )
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
Gia_ManForEachRi( p, pObj, i )
if ( Vec_IntEntry(vFla, i) )
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
return vGla;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to FLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
{
Vec_Int_t * vFla;
Gia_Obj_t * pObj;
int i;
vFla = Vec_IntStart( Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Vec_IntWriteEntry( vFla, i, 1 );
return vFla;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose )
{
int i, Entry, CountUpTo, CountAll, CountRem, * pCounts;
int nFrames = Vec_IntEntry( p->vGateClasses, 0 );
if ( nFrames < 2 )
{
printf( "Gate-level abstraction is missing object count information.\n" );
return;
}
// collect info
CountAll = 0;
pCounts = ABC_CALLOC( int, nFrames + 1 );
assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
{
Entry = Vec_IntEntry( p->vGateClasses, i );
assert( Entry >= 0 && Entry <= nFrames );
if ( Entry == 0 )
continue;
CountAll++;
pCounts[Entry]++;
}
// print entries
CountUpTo = 0;
for ( i = 0; i <= nFrames; i++ )
printf( "%d=%d(%d) ", i, pCounts[i], CountUpTo += pCounts[i] );
printf( "\n" );
// removing entries appearing only ones
CountRem = 0;
for ( i = 0; i < Gia_ManObjNum(p); i++ )
{
if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
continue;
if ( Vec_IntEntry( p->vGateClasses, i ) <= nPurifyRatio )
{
CountRem++;
Vec_IntWriteEntry( p->vGateClasses, i, 0 );
}
}
printf( "Removed %d entries appearing less or equal than %d times (out of %d).\n", CountRem, nPurifyRatio, CountAll );
ABC_FREE( pCounts );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla )
{
Gia_Obj_t * pObj;
int i, Count = 0;
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Count++;
return Count;
}
int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
{
Gia_Obj_t * pObj;
int i, Count = 0;
Gia_ManForEachAnd( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Count++;
return Count;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

89
src/aig/gia/giaAbs.h
View File

@ -1,89 +0,0 @@
/**CFile****************************************************************
FileName [giaAbs.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__gia__giaAbs_h
#define ABC__aig__gia__giaAbs_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// abstraction parameters
typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
struct Gia_ParAbs_t_
{
int Algo; // the algorithm to be used
int nFramesMax; // timeframes for PBA
int nConfMax; // conflicts for PBA
int fDynamic; // dynamic unfolding for PBA
int fConstr; // use constraints
int nFramesBmc; // timeframes for BMC
int nConfMaxBmc; // conflicts for BMC
int nStableMax; // the number of stable frames to quit
int nRatio; // ratio of flops to quit
int TimeOut; // approximate timeout in seconds
int TimeOutVT; // approximate timeout in seconds
int nBobPar; // Bob's parameter
int fUseBdds; // use BDDs to refine abstraction
int fUseDprove; // use 'dprove' to refine abstraction
int fUseStart; // use starting frame
int fVerbose; // verbose output
int fVeryVerbose; // printing additional information
int Status; // the problem status
int nFramesDone; // the number of frames covered
};
extern void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

257
src/aig/gia/giaDup.c
View File

@ -1663,263 +1663,6 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included flops.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nFlops = 0;
Gia_ManFillValue( p );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create PIs
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
Gia_ManForEachRo( p, pObj, i )
if ( !Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create POs
Gia_ManHashAlloc( pNew );
Gia_ManForEachPo( p, pObj, i )
{
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
// create RIs
Gia_ManForEachRi( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
{
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
nFlops++;
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, nFlops );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry > 0 );
pObj = Gia_ManObj( p, i );
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Collects PIs and PPIs of the abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
if ( pvPis ) *pvPis = Vec_IntAlloc( 100 );
if ( pvPPis ) *pvPPis = Vec_IntAlloc( 100 );
if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 );
if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
{ if ( pvPis ) Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) ); }
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
{ if ( pvPPis ) Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsRo(p, pObj) )
{ if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsAnd(pObj) )
{ if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); }
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntFree( vAssigned );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
Description [The array contains 1 for those objects (const, RO, AND)
that are included in the abstraction; 0, otherwise.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pCopy;
int i;//, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create additional arrays
Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create constant
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
// create PIs
Gia_ManForEachObjVec( vPis, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
Gia_ManForEachObjVec( vPPis, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
Gia_ManForEachObjVec( vFlops, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create internal nodes
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// Gia_ManDupAbsGates_rec( pNew, pObj );
// create PO
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// create RIs
Gia_ManForEachObjVec( vFlops, p, pObj, i )
Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
// transfer copy values: (p -> pTemp -> pNew) => (p -> pNew)
if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) )
{
// printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
Gia_ManForEachObj( p, pObj, i )
{
if ( !~pObj->Value )
continue;
assert( !Abc_LitIsCompl(pObj->Value) );
pCopy = Gia_ObjCopy( pTemp, pObj );
if ( !~pCopy->Value )
{
Vec_IntWriteEntry( vGateClasses, i, 0 );
pObj->Value = ~0;
continue;
}
assert( !Abc_LitIsCompl(pCopy->Value) );
pObj->Value = pCopy->Value;
}
}
Gia_ManStop( pTemp );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
return pNew;
}
/**Function*************************************************************
Synopsis [Copy an AIG structure related to the selected POs.]

150
src/aig/gia/giaMan.c
View File

@ -20,6 +20,7 @@
#include "gia.h"
#include "misc/tim/tim.h"
#include "proof/abs/abs.h"
ABC_NAMESPACE_IMPL_START
@ -165,155 +166,6 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p )
}
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintFlopClasses( Gia_Man_t * p )
{
int Counter0, Counter1;
if ( p->vFlopClasses == NULL )
return;
if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) )
{
printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ",
Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
printf( "and there are other FF classes..." );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
int nTotal;
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
{
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
// create additional arrays
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1),
nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintObjClasses( Gia_Man_t * p )
{
Vec_Int_t * vSeens; // objects seen so far
Vec_Int_t * vAbs = p->vObjClasses;
int i, k, Entry, iStart, iStop = -1, nFrames;
int nObjBits, nObjMask, iObj, iFrame, nWords;
unsigned * pInfo;
int * pCountAll, * pCountUni;
if ( vAbs == NULL )
return;
nFrames = Vec_IntEntry( vAbs, 0 );
assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
pCountAll = ABC_ALLOC( int, nFrames + 1 );
pCountUni = ABC_ALLOC( int, nFrames + 1 );
// start storage for seen objects
nWords = Abc_BitWordNum( nFrames );
vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
// get the bitmasks
nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask );
// print info about frames
printf( "Frame Core F0 F1 F2 F3 ...\n" );
for ( i = 0; i < nFrames; i++ )
{
iStart = Vec_IntEntry( vAbs, i+1 );
iStop = Vec_IntEntry( vAbs, i+2 );
memset( pCountAll, 0, sizeof(int) * (nFrames + 1) );
memset( pCountUni, 0, sizeof(int) * (nFrames + 1) );
Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
{
iObj = (Entry & nObjMask);
iFrame = (Entry >> nObjBits);
pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
{
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
}
assert( pCountAll[0] == (iStop - iStart) );
// printf( "%5d%5d ", pCountAll[0], pCountUni[0] );
printf( "%3d :", i );
printf( "%7d", pCountAll[0] );
if ( i >= 10 )
{
for ( k = 0; k < 4; k++ )
printf( "%5d", pCountAll[k+1] );
printf( " ..." );
for ( k = i-4; k <= i; k++ )
printf( "%5d", pCountAll[k+1] );
}
else
{
for ( k = 0; k <= i; k++ )
if ( k <= i )
printf( "%5d", pCountAll[k+1] );
}
// for ( k = 0; k < nFrames; k++ )
// if ( k <= i )
// printf( "%5d", pCountAll[k+1] );
printf( "\n" );
}
assert( iStop == Vec_IntSize(vAbs) );
Vec_IntFree( vSeens );
ABC_FREE( pCountAll );
ABC_FREE( pCountUni );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]

9
src/aig/gia/module.make
View File

@ -1,13 +1,4 @@
SRC += src/aig/gia/gia.c \
src/aig/gia/giaAbs.c \
src/aig/gia/giaAbsGla.c \
src/aig/gia/giaAbsGla2.c \
src/aig/gia/giaAbsIter.c \
src/aig/gia/giaAbsOut.c \
src/aig/gia/giaAbsPth.c \
src/aig/gia/giaAbsRef.c \
src/aig/gia/giaAbsRef2.c \
src/aig/gia/giaAbsVta.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaBidec.c \

13
src/aig/saig/module.make
View File

@ -1,9 +1,4 @@
SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigAbsCba.c \
src/aig/saig/saigAbsPba.c \
src/aig/saig/saigAbsStart.c \
src/aig/saig/saigAbsVfa.c \
src/aig/saig/saigBmc.c \
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigBmc2.c \
src/aig/saig/saigBmc3.c \
src/aig/saig/saigCexMin.c \
@ -12,9 +7,6 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigConstr2.c \
src/aig/saig/saigDual.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigGlaCba.c \
src/aig/saig/saigGlaPba.c \
src/aig/saig/saigGlaPba2.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \
@ -24,13 +16,10 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigOutDec.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRefSat.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
src/aig/saig/saigRetStep.c \
src/aig/saig/saigScl.c \
src/aig/saig/saigSimExt.c \
src/aig/saig/saigSimExt2.c \
src/aig/saig/saigSimFast.c \
src/aig/saig/saigSimMv.c \
src/aig/saig/saigSimSeq.c \

26
src/aig/saig/saig.h
View File

@ -27,7 +27,6 @@
////////////////////////////////////////////////////////////////////////
#include "aig/aig/aig.h"
#include "aig/gia/giaAbs.h"
ABC_NAMESPACE_HEADER_START
@ -35,10 +34,6 @@ ABC_NAMESPACE_HEADER_START
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define SAIG_ZER 1
#define SAIG_ONE 2
#define SAIG_UND 3
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@ -131,20 +126,6 @@ static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) {
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
extern Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses );
extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
extern Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs );
/*=== sswAbsCba.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
/*=== sswAbsPba.c ==========================================================*/
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
/*=== sswAbsStart.c ==========================================================*/
extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
@ -203,8 +184,6 @@ extern int Saig_ManDemiterNew( Aig_Man_t * pMan );
extern Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose );
/*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
/*=== saigRefSat.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/
extern void Saig_ManMarkAutonomous( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
@ -215,11 +194,6 @@ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in
extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
/*=== saigSimExt.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose );
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose );
/*=== saigSimExt.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
/*=== saigSimMv.c ==========================================================*/
extern Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
/*=== saigStrSim.c ==========================================================*/

133
src/aig/saig/saigAbs.c
View File

@ -1,133 +0,0 @@
/**CFile****************************************************************
FileName [saigAbs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Intergrated abstraction procedure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Transform flop map into flop list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses )
{
Vec_Int_t * vFlops;
int i, Entry;
vFlops = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry )
Vec_IntPush( vFlops, i );
return vFlops;
}
/**Function*************************************************************
Synopsis [Transform flop list into flop map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops )
{
Vec_Int_t * vFlopClasses;
int i, Entry;
vFlopClasses = Vec_IntStart( nRegs );
Vec_IntForEachEntry( vFlops, Entry, i )
Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
return vFlopClasses;
}
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, f;
if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
// else
// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
// start the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
for ( f = 0; f <= pCexAbs->iFrame; f++ )
{
Saig_ManForEachPi( pAbs, pObj, i )
{
if ( i == Saig_ManPiNum(p) )
break;
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
}
}
// verify the counter example
if ( !Saig_ManVerifyCex( p, pCex ) )
{
printf( "Saig_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 of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
}
return pCex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

374
src/aig/saig/saigAbsPba.c
View File

@ -1,374 +0,0 @@
/**CFile****************************************************************
FileName [saigAbsPba.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Proof-based abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbsPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collect nodes in the unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsCo(pObj) )
Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
else if ( Aig_ObjIsNode(pObj) )
{
Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
}
if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
Vec_IntPush( vObjs, Aig_ObjId(pObj) );
}
/**Function*************************************************************
Synopsis [Derives unrolled timeframes for PBA.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
Vec_Vec_t * vFrameObjs; // the list of objects per frame
Vec_Int_t * vRoots, * vObjs;
Aig_Obj_t * pObj, * pObjNew;
int i, f;
assert( nStart <= nFrames );
// collect COs and Objs visited in each frame
vFrameCos = Vec_VecStart( nFrames );
vFrameObjs = Vec_VecStart( nFrames );
for ( f = nFrames-1; f >= 0; f-- )
{
// add POs of this frame
vRoots = Vec_VecEntryInt( vFrameCos, f );
Saig_ManForEachPo( pAig, pObj, i )
Vec_IntPush( vRoots, Aig_ObjId(pObj) );
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManUnrollForPba_rec( pAig, pObj,
Vec_VecEntryInt( vFrameObjs, f ),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
}
// derive unrolled timeframes
pFrames = Aig_ManStart( 10000 );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// create activation variables
Saig_ManForEachLo( pAig, pObj, i )
Aig_ObjCreateCi( pFrames );
// initialize the flops
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,i), Aig_ObjCreateCi(pFrames), Aig_ManConst0(pFrames) );
// iterate through the frames
*pvPiVarMap = Vec_IntStartFull( nFrames * Saig_ManPiNum(pAig) );
pObjNew = Aig_ManConst0(pFrames);
for ( f = 0; f < nFrames; f++ )
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else if ( Aig_ObjIsCo(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Saig_ObjIsPi(pAig, pObj) )
{
Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjCioId(pObj), Aig_ManCiNum(pFrames) );
pObj->pData = Aig_ObjCreateCi( pFrames );
}
else if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pFrames);
else if ( !Saig_ObjIsLo(pAig, pObj) )
assert( 0 );
}
// create output
if ( f >= nStart )
{
Saig_ManForEachPo( pAig, pObj, i )
pObjNew = Aig_Or( pFrames, pObjNew, (Aig_Obj_t *)pObj->pData );
}
// transfer
if ( f == nFrames - 1 )
break;
vRoots = Vec_VecEntryInt( vFrameCos, f );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
{
if ( Saig_ObjIsLi(pAig, pObj) )
{
int iFlopNum = Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig);
assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) );
Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData );
}
}
}
// cleanup
Vec_VecFree( vFrameCos );
Vec_VecFree( vFrameObjs );
// create output
Aig_ObjCreateCo( pFrames, pObjNew );
Aig_ManSetRegNum( pFrames, 0 );
// finallize
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Derives the counter-example from the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int i, f, Entry, iBit = 0;
pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
pCex->iPo = -1;
pCex->iFrame = -1;
Vec_IntForEachEntry( vPiVarMap, Entry, i )
{
if ( Entry >= 0 )
{
int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManCi(pCnf->pMan, Entry)) ];
if ( sat_solver_var_value( pSat, iSatVar ) )
Abc_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i );
}
}
// check what frame has failed
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++);
for ( f = 0; f < nFrames; f++ )
{
// compute new state
Saig_ManForEachPi( pAig, pObj, i )
pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++);
Aig_ManForEachNode( pAig, pObj, i )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachCo( pAig, pObj, i )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
pObjRo->fMarkB = pObjRi->fMarkB;
// check the outputs
Saig_ManForEachPo( pAig, pObj, i )
{
if ( pObj->fMarkB )
{
pCex->iPo = i;
pCex->iFrame = f;
pCex->nBits = pCex->nRegs + pCex->nPis * (f+1);
break;
}
}
if ( i < Saig_ManPoNum(pAig) )
break;
}
Aig_ManCleanMarkB(pAig);
if ( f == nFrames )
{
Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
if ( !Saig_ManVerifyCex( pAig, pCex ) )
{
Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int TimeLimit, int fVerbose, int * piFrame )
{
Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
int nCoreLits, * pCoreLits;
int i, iVar, RetValue;
clock_t clk;
if ( fVerbose )
{
if ( TimeLimit )
printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFrames, TimeLimit );
else
printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFrames );
}
// create SAT solver
clk = clock();
pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap );
if ( fVerbose )
Aig_ManPrintStats( pFrames );
// pCnf = Cnf_DeriveSimple( pFrames, 0 );
// pCnf = Cnf_Derive( pFrames, 0 );
pCnf = Cnf_DeriveFast( pFrames, 0 );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
return NULL;
}
if ( fVerbose )
Abc_PrintTime( 1, "Preparing", clock() - clk );
// map activation variables into flop numbers
vAssumps = Vec_IntAlloc( Aig_ManRegNum(pAig) );
vMapVar2FF = Vec_IntStartFull( pCnf->nVars );
Aig_ManForEachCi( pFrames, pObj, i )
{
if ( i >= Aig_ManRegNum(pAig) )
break;
iVar = pCnf->pVarNums[Aig_ObjId(pObj)];
Vec_IntPush( vAssumps, toLitCond(iVar, 1) );
Vec_IntWriteEntry( vMapVar2FF, iVar, i );
}
// set runtime limit
if ( TimeLimit )
sat_solver_set_runtime_limit( pSat, TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0 );
// run SAT solver
clk = clock();
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( fVerbose )
Abc_PrintTime( 1, "Solving", clock() - clk );
if ( RetValue != l_False )
{
if ( RetValue == l_True )
{
Vec_Int_t * vAbsFfsToAdd;
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame );
*piFrame = pAig->pSeqModel->iFrame;
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
{
Vec_IntFree( vAbsFfsToAdd );
goto finish;
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
vFlops = vAbsFfsToAdd;
}
else
{
printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" );
}
goto finish;
}
assert( RetValue == l_False ); // UNSAT
*piFrame = nFrames;
// get relevant SAT literals
nCoreLits = sat_solver_final( pSat, &pCoreLits );
assert( nCoreLits > 0 );
if ( fVerbose )
printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n",
nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
// collect flops
vFlops = Vec_IntAlloc( nCoreLits );
for ( i = 0; i < nCoreLits; i++ )
{
iVar = Vec_IntEntry( vMapVar2FF, lit_var(pCoreLits[i]) );
assert( iVar >= 0 && iVar < Aig_ManRegNum(pAig) );
Vec_IntPush( vFlops, iVar );
}
Vec_IntSort( vFlops, 0 );
// cleanup
finish:
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Aig_ManStop( pFrames );
return vFlops;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

329
src/aig/saig/saigAbsVfa.c
View File

@ -1,329 +0,0 @@
/**CFile****************************************************************
FileName [saigAbsVfa.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Intergrated abstraction procedure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbsVfa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Abs_VfaMan_t_ Abs_VfaMan_t;
struct Abs_VfaMan_t_
{
Aig_Man_t * pAig;
int nConfLimit;
int fVerbose;
// unrolling info
int iFrame;
int nFrames;
Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
Vec_Int_t * vFra2Var; // maps frame number into the first variable
// SAT solver
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Vec_Int_t * vAssumps;
Vec_Int_t * vCore;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds CNF clauses for the MUX.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_VfaManSatMux( sat_solver * pSat, int VarF, int VarI, int VarT, int VarE )
{
int RetValue, pLits[3];
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
assert( VarT != VarE );
pLits[0] = toLitCond(VarT, 0);
pLits[1] = toLitCond(VarE, 0);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarT, 1);
pLits[1] = toLitCond(VarE, 1);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( RetValue );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abs_VfaManAddVar( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f, int * pfNew )
{
int i, SatId, VecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
*pfNew = 0;
if ( VecId == -1 )
return -1;
if ( VecId == 0 )
{
VecId = Vec_IntSize( p->vVec2Var ) / p->nFrames;
for ( i = 0; i < p->nFrames; i++ )
Vec_IntPush( p->vVec2Var, 0 );
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), VecId );
}
SatId = Vec_IntEntry( p->vVec2Var, p->nFrames * VecId + f );
if ( SatId )
return SatId;
SatId = Vec_IntSize( p->vVar2Inf ) / 2;
// save SatId
Vec_IntWriteEntry( p->vVec2Var, p->nFrames * VecId + f, SatId );
Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
Vec_IntPush( p->vVar2Inf, f );
if ( Saig_ObjIsLo( p->pAig, pObj ) ) // reserve IDs for aux vars
{
Vec_IntPush( p->vVar2Inf, -1 );
Vec_IntPush( p->vVar2Inf, f );
Vec_IntPush( p->vVar2Inf, -2 );
Vec_IntPush( p->vVar2Inf, f );
}
*pfNew = 1;
return SatId;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f )
{
int SatVar, fNew;
if ( Aig_ObjIsConst1(pObj) )
return -1;
SatVar = Abs_VfaManAddVar( p, pObj, f, &fNew );
if ( (SatVar > 0 && !fNew) || Saig_ObjIsPi(p->pAig, pObj) || (Aig_ObjIsCi(pObj) && f==0) )
return SatVar;
if ( Aig_ObjIsCo(pObj) )
return Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f );
if ( Aig_ObjIsCi(pObj) )
return Abs_VfaManCreateFrame_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1 );
assert( Aig_ObjIsAnd(pObj) );
Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f );
Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin1(pObj), f );
return SatVar;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_VfaManCreateFrame( Abs_VfaMan_t * p, int f )
{
Aig_Obj_t * pObj;
int i;
clock_t clk = clock();
Saig_ManForEachPo( p->pAig, pObj, i )
Abs_VfaManCreateFrame_rec( p, pObj, f );
Vec_IntPush( p->vFra2Var, Vec_IntSize( p->vVar2Inf ) / 2 );
printf( "Frame = %3d : ", f );
printf( "Vecs = %8d ", Vec_IntSize( p->vVec2Var ) / p->nFrames );
printf( "Vars = %8d ", Vec_IntSize( p->vVar2Inf ) / 2 );
Abc_PrintTime( 1, "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abs_VfaMan_t * Abs_VfaManStart( Aig_Man_t * pAig )
{
Abs_VfaMan_t * p;
int i;
p = ABC_CALLOC( Abs_VfaMan_t, 1 );
p->pAig = pAig;
p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
p->vVec2Var = Vec_IntAlloc( 1 << 20 );
p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
p->vFra2Var = Vec_IntStart( 1 );
// skip the first variable
Vec_IntPush( p->vVar2Inf, -3 );
Vec_IntPush( p->vVar2Inf, -3 );
for ( i = 0; i < p->nFrames; i++ )
Vec_IntPush( p->vVec2Var, -1 );
// transfer values from CNF
p->pCnf = Cnf_DeriveOther( pAig, 0 );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
if ( p->pCnf->pObj2Clause[i] == -1 )
Vec_IntWriteEntry( p->vObj2Vec, i, -1 );
p->vAssumps = Vec_IntAlloc( 100 );
p->vCore = Vec_IntAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_VfaManStop( Abs_VfaMan_t * p )
{
Vec_IntFreeP( &p->vObj2Vec );
Vec_IntFreeP( &p->vVec2Var );
Vec_IntFreeP( &p->vVar2Inf );
Vec_IntFreeP( &p->vFra2Var );
Vec_IntFreeP( &p->vAssumps );
Vec_IntFreeP( &p->vCore );
if ( p->pCnf )
Cnf_DataFree( p->pCnf );
if ( p->pSat )
sat_solver_delete( p->pSat );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Perform variable frame abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose )
{
Abs_VfaMan_t * p;
int i;
p = Abs_VfaManStart( pAig );
p->nFrames = nFrames;
p->nConfLimit = nConfLimit;
p->fVerbose = fVerbose;
// create unrolling for the given number of frames
for ( i = 0; i < p->nFrames; i++ )
Abs_VfaManCreateFrame( p, i );
Abs_VfaManStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

556
src/aig/saig/saigSimExt.c
View File

@ -1,556 +0,0 @@
/**CFile****************************************************************
FileName [saigSimExt.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Extending simulation trace to contain ternary values.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigSimExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "proof/ssw/ssw.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Saig_ManSimInfoNot( int Value )
{
if ( Value == SAIG_ZER )
return SAIG_ONE;
if ( Value == SAIG_ONE )
return SAIG_ZER;
return SAIG_UND;
}
static inline int Saig_ManSimInfoAnd( int Value0, int Value1 )
{
if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER )
return SAIG_ZER;
if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE )
return SAIG_ONE;
return SAIG_UND;
}
static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
}
static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
{
unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
assert( Value >= SAIG_ZER && Value <= SAIG_UND );
Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs ternary simulation for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
{
int Value0, Value1, Value;
Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
if ( Aig_ObjFaninC0(pObj) )
Value0 = Saig_ManSimInfoNot( Value0 );
if ( Aig_ObjIsCo(pObj) )
{
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
return Value0;
}
assert( Aig_ObjIsNode(pObj) );
Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
if ( Aig_ObjFaninC1(pObj) )
Value1 = Saig_ManSimInfoNot( Value1 );
Value = Saig_ManSimInfoAnd( Value0, Value1 );
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
return Value;
}
/**Function*************************************************************
Synopsis [Performs ternary simulation for one design.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f, Entry, iBit = 0;
Saig_ManForEachLo( p, pObj, i )
Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
Saig_ManForEachPi( p, pObj, i )
Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
if ( vRes )
Vec_IntForEachEntry( vRes, Entry, i )
Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND );
Aig_ManForEachNode( p, pObj, i )
Saig_ManExtendOneEval( vSimInfo, pObj, f );
Aig_ManForEachCo( p, pObj, i )
Saig_ManExtendOneEval( vSimInfo, pObj, f );
if ( f == pCex->iFrame )
break;
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
}
// make sure the output of the property failed
pObj = Aig_ManCo( p, pCex->iPo );
return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
}
/**Function*************************************************************
Synopsis [Tries to assign ternary value to one of the primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo,
int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 )
{
Aig_Obj_t * pFanout, * pObj = Aig_ManCi(p, iPi);
int i, k, f, iFanout = -1, Value, Value2, Entry;
// save original value
Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
assert( Value == SAIG_ZER || Value == SAIG_ONE );
Vec_IntPush( vUndo, Aig_ObjId(pObj) );
Vec_IntPush( vUndo, iFrame );
Vec_IntPush( vUndo, Value );
// update original value
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, SAIG_UND );
// traverse
Vec_IntClear( vVis );
Vec_IntPush( vVis, Aig_ObjId(pObj) );
for ( f = iFrame; f <= pCex->iFrame; f++ )
{
Vec_IntClear( vVis2 );
Vec_IntForEachEntry( vVis, Entry, i )
{
pObj = Aig_ManObj( p, Entry );
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
{
assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
Value = Saig_ManSimInfoGet( vSimInfo, pFanout, f );
if ( Value == SAIG_UND )
continue;
Value2 = Saig_ManExtendOneEval( vSimInfo, pFanout, f );
if ( Value2 == Value )
continue;
assert( Value2 == SAIG_UND );
// assert( Vec_IntFind(vVis, Aig_ObjId(pFanout)) == -1 );
if ( Aig_ObjIsNode(pFanout) )
Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
else if ( Saig_ObjIsLi(p, pFanout) )
Vec_IntPush( vVis2, Aig_ObjId(pFanout) );
Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
Vec_IntPush( vUndo, f );
Vec_IntPush( vUndo, Value );
}
}
if ( Vec_IntSize(vVis2) == 0 )
break;
if ( f == pCex->iFrame )
break;
// transfer
Vec_IntClear( vVis );
Vec_IntForEachEntry( vVis2, Entry, i )
{
pObj = Aig_ManObj( p, Entry );
assert( Saig_ObjIsLi(p, pObj) );
pFanout = Saig_ObjLiToLo( p, pObj );
Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
Value = Saig_ManSimInfoGet( vSimInfo, pObj, f );
Saig_ManSimInfoSet( vSimInfo, pFanout, f+1, Value );
}
}
// check the output
pObj = Aig_ManCo( p, pCex->iPo );
Value = Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
assert( Value == SAIG_ONE || Value == SAIG_UND );
return (int)(Value == SAIG_ONE);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo )
{
Aig_Obj_t * pObj;
int i, iFrame, Value;
for ( i = 0; i < Vec_IntSize(vUndo); i += 3 )
{
pObj = Aig_ManObj( p, Vec_IntEntry(vUndo, i) );
iFrame = Vec_IntEntry(vUndo, i+1);
Value = Vec_IntEntry(vUndo, i+2);
assert( Saig_ManSimInfoGet(vSimInfo, pObj, iFrame) == SAIG_UND );
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
}
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExample0( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
assert( Value == SAIG_ONE );
// select the result
vRes = Vec_IntAlloc( 1000 );
vResInv = Vec_IntAlloc( 1000 );
vVis = Vec_IntAlloc( 1000 );
vVis2 = Vec_IntAlloc( 1000 );
vUndo = Vec_IntAlloc( 1000 );
for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
{
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
Vec_IntFree( vVis );
Vec_IntFree( vVis2 );
Vec_IntFree( vUndo );
// resimulate to make sure it is valid
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
assert( Value == SAIG_ONE );
Vec_IntFree( vResInv );
return vRes;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExample1( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
assert( Value == SAIG_ONE );
// select the result
vRes = Vec_IntAlloc( 1000 );
vResInv = Vec_IntAlloc( 1000 );
vVis = Vec_IntAlloc( 1000 );
vVis2 = Vec_IntAlloc( 1000 );
vUndo = Vec_IntAlloc( 1000 );
for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
{
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
Vec_IntFree( vVis );
Vec_IntFree( vVis2 );
Vec_IntFree( vUndo );
// resimulate to make sure it is valid
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
assert( Value == SAIG_ONE );
Vec_IntFree( vResInv );
return vRes;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExample2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
assert( Value == SAIG_ONE );
// select the result
vRes = Vec_IntAlloc( 1000 );
vResInv = Vec_IntAlloc( 1000 );
vVis = Vec_IntAlloc( 1000 );
vVis2 = Vec_IntAlloc( 1000 );
vUndo = Vec_IntAlloc( 1000 );
for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
{
if ( i % 2 == 0 )
continue;
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
{
if ( i % 2 == 1 )
continue;
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
Vec_IntFree( vVis );
Vec_IntFree( vVis2 );
Vec_IntFree( vUndo );
// resimulate to make sure it is valid
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
assert( Value == SAIG_ONE );
Vec_IntFree( vResInv );
return vRes;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExample3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
assert( Value == SAIG_ONE );
// select the result
vRes = Vec_IntAlloc( 1000 );
vResInv = Vec_IntAlloc( 1000 );
vVis = Vec_IntAlloc( 1000 );
vVis2 = Vec_IntAlloc( 1000 );
vUndo = Vec_IntAlloc( 1000 );
for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
{
if ( i % 2 == 0 )
continue;
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- )
{
if ( i % 2 == 1 )
continue;
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) )
{
Saig_ManExtendUndo( p, vSimInfo, vUndo );
break;
}
if ( f >= 0 )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
Vec_IntFree( vVis );
Vec_IntFree( vVis2 );
Vec_IntFree( vUndo );
// resimulate to make sure it is valid
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
assert( Value == SAIG_ONE );
Vec_IntFree( vResInv );
return vRes;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes0 = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
Vec_Int_t * vRes1 = Saig_ManExtendCounterExample1( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
Vec_Int_t * vRes2 = Saig_ManExtendCounterExample2( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
Vec_Int_t * vRes3 = Saig_ManExtendCounterExample3( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
Vec_Int_t * vRes = vRes0;
// if ( fVerbose )
printf( "Removable flops: Order0 =%3d. Order1 =%3d. Order2 =%3d. Order3 =%3d.\n",
Vec_IntSize(vRes0), Vec_IntSize(vRes1), Vec_IntSize(vRes2), Vec_IntSize(vRes3) );
if ( Vec_IntSize(vRes1) < Vec_IntSize(vRes) )
vRes = vRes1;
if ( Vec_IntSize(vRes2) < Vec_IntSize(vRes) )
vRes = vRes2;
if ( Vec_IntSize(vRes3) < Vec_IntSize(vRes) )
vRes = vRes3;
vRes = Vec_IntDup( vRes );
Vec_IntFree( vRes0 );
Vec_IntFree( vRes1 );
Vec_IntFree( vRes2 );
Vec_IntFree( vRes3 );
return vRes;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose )
{
Vec_Int_t * vRes;
Vec_Ptr_t * vSimInfo;
clock_t clk;
if ( Saig_ManPiNum(p) != pCex->nPis )
{
printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n",
Aig_ManCiNum(p), pCex->nPis );
return NULL;
}
Aig_ManFanoutStart( p );
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );
clk = clock();
if ( fTryFour )
vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
else
vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
if ( fVerbose )
{
printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
}
Vec_PtrFree( vSimInfo );
Aig_ManFanoutStop( p );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -49,6 +49,7 @@
#include "proof/bbr/bbr.h"
#include "map/cov/cov.h"
#include "base/cmd/cmd.h"
#include "proof/abs/abs.h"
#ifdef _WIN32
//#include <io.h>
@ -350,14 +351,12 @@ static int Abc_CommandAbc9Trace ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9AbsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaPurify ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaShrink ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -811,14 +810,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&speedup", Abc_CommandAbc9Speedup, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&era", Abc_CommandAbc9Era, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dch", Abc_CommandAbc9Dch, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&abs_start", Abc_CommandAbc9AbsStart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_refine", Abc_CommandAbc9AbsRefine, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_purify", Abc_CommandAbc9GlaPurify, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_shrink", Abc_CommandAbc9GlaShrink, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
@ -27245,127 +27242,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9AbsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParAbs_t Pars, * pPars = &Pars;
int c;
// set defaults
Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCRrpfvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesBmc < 0 )
goto usage;
break;
/*
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStableMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStableMax < 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->nConfMaxBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfMaxBmc < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRatio < 0 )
goto usage;
break;
case 'r':
pPars->fUseBdds ^= 1;
break;
case 'p':
pPars->fUseDprove ^= 1;
break;
case 'f':
pPars->fUseStart ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStart(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStart(): The AIG is combinational.\n" );
return 0;
}
if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStart(): Wrong value of parameter \"-R <num>\".\n" );
return 0;
}
Gia_ManCexAbstractionStart( pAbc->pGia, pPars );
pAbc->Status = pPars->Status;
pAbc->nFrames = pPars->nFramesDone;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &abs_start [-FCR num] [-rpfvh]\n" );
Abc_Print( -2, "\t initializes flop map using cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
// Abc_Print( -2, "\t-S num : the max number of stable frames for BMC [default = %d]\n", pPars->nStableMax );
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -27504,6 +27380,8 @@ usage:
return 1;
}
#if 0
/**Function*************************************************************
Synopsis []
@ -27737,6 +27615,8 @@ usage:
return 1;
}
#endif
/**Function*************************************************************
Synopsis []
@ -27885,75 +27765,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GlaPurify( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose );
int fMinCut = 0;
int nPurifyRatio = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Rmvh" ) ) != EOF )
{
switch ( c )
{
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nPurifyRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nPurifyRatio < 0 )
goto usage;
break;
case 'm':
fMinCut ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no AIG.\n" );
return 1;
}
if ( pAbc->pGia->vGateClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no gate-level abstraction.\n" );
return 0;
}
Gia_ManGlaPurify( pAbc->pGia, nPurifyRatio, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &gla_purify [-R num] [-vh]\n" );
Abc_Print( -2, "\t purifies gate-level abstraction by removing less frequent objects\n" );
// Abc_Print( -2, "\t-R num : the percetage of rare objects to remove [default = %d]\n", nPurifyRatio );
Abc_Print( -2, "\t-R num : remove objects with usage count less or equal than this [default = %d]\n", nPurifyRatio );
// 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;
}
/**Function*************************************************************
Synopsis []
@ -27967,7 +27778,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
int fUsePdr = 0;
int fUseSat = 1;
int fUseBdd = 0;
@ -28029,7 +27839,7 @@ int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no gate-level abstraction.\n" );
return 0;
}
Gia_IterImprove( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose );
Gia_ManShrinkGla( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose );
return 0;
usage:
@ -28045,274 +27855,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
int c, fNaiveCnf = 0;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 0;
pPars->nConfLimit = 0;
pPars->nTimeOut = 60;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTcvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStart < 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->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 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->nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimit < 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->nFfToAddMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFfToAddMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'c':
fNaiveCnf ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 0 )
{
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nStart > 0 && pPars->nFramesMax > 0 && pPars->nStart >= pPars->nFramesMax )
{
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
// if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &gla_cba [-SFCT num] [-cvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll (0=unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
// Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
Abc_Print( -2, "\t-T num : an approximate timeout in seconds (0=unused) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
int c;
int fNewSolver = 0;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0;
pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10;
pPars->nConfLimit = 0;
pPars->fSkipRand = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrnvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStart < 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->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 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->nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'r':
pPars->fSkipRand ^= 1;
break;
case 'n':
fNewSolver ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 1 )
{
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nStart >= pPars->nFramesMax )
{
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
if ( pPars->nStart )
Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" );
pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars, fNewSolver );
// if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rnvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-r : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" );
Abc_Print( -2, "\t-n : toggle using on-the-fly proof-logging [default = %s]\n", fNewSolver? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -28327,9 +27869,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParVta_t Pars, * pPars = &Pars;
Abs_Par_t Pars, * pPars = &Pars;
int c, fStartVta = 0, fNewAlgo = 1;
Gia_VtaSetDefaultParams( pPars );
Abs_ParSetDefaults( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF )
{
@ -28533,9 +28075,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( fNewAlgo )
pAbc->Status = Ga2_ManPerform( pAbc->pGia, pPars );
pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
else
pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, fStartVta );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
@ -28585,9 +28127,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParVta_t Pars, * pPars = &Pars;
Abs_Par_t Pars, * pPars = &Pars;
int c;
Gia_VtaSetDefaultParams( pPars );
Abs_ParSetDefaults( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtradvh" ) ) != EOF )
{

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

@ -21,6 +21,7 @@
#include "ioAbc.h"
#include "base/main/mainInt.h"
#include "aig/saig/saig.h"
#include "proof/abs/abs.h"
ABC_NAMESPACE_IMPL_START

2
src/opt/nwk/nwkAig.c
View File

@ -105,7 +105,7 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose
#include "aig/gia/gia.h"
#include "proof/abs/abs.h"
/**Function*************************************************************

52
src/proof/abs/abs.c Normal file
View File

@ -0,0 +1,52 @@
/**CFile****************************************************************
FileName [abs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

131
src/proof/abs/abs.h Normal file
View File

@ -0,0 +1,131 @@
/**CFile****************************************************************
FileName [abs.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__proof_abs__Abs_h
#define ABC__proof_abs__Abs_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// abstraction parameters
typedef struct Abs_Par_t_ Abs_Par_t;
struct Abs_Par_t_
{
int nFramesMax; // maximum frames
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nLearnedMax; // max number of learned clauses
int nLearnedStart; // max number of learned clauses
int nLearnedDelta; // delta increase of learned clauses
int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
int nRatioMax; // restart when the number of abstracted object is more than this
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers
int fUseSkip; // skip proving intermediate timeframes
int fUseSimple; // use simple CNF construction
int fSkipHash; // skip hashing CNF while unrolling
int fUseFullProof; // use full proof for UNSAT cores
int fDumpVabs; // dumps the abstracted model
int fDumpMabs; // dumps the original AIG with abstraction map
int fCallProver; // calls the prover
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
int fVeryVerbose; // print additional information
int iFrame; // the number of frames covered
int iFrameProved; // the number of frames proved
int nFramesNoChange; // the number of last frames without changes
int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== abs.c =========================================================*/
/*=== absDup.c =========================================================*/
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern void Gia_ManPrintFlopClasses( Gia_Man_t * p );
extern void Gia_ManPrintObjClasses( Gia_Man_t * p );
extern void Gia_ManPrintGateClasses( Gia_Man_t * p );
/*=== absGla.c =========================================================*/
extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
/*=== absGlaOld.c =========================================================*/
extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
/*=== absIter.c =========================================================*/
extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
/*=== absVta.c =========================================================*/
extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
/*=== absUtil.c =========================================================*/
extern void Abs_ParSetDefaults( Abs_Par_t * p );
extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
/*=== absOldCex.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
/*=== absOldRef.c ==========================================================*/
extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
/*=== absOldSat.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
/*=== absOldSim.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

445
src/proof/abs/absDup.c Normal file
View File

@ -0,0 +1,445 @@
/**CFile****************************************************************
FileName [absDup.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [Duplication procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: absDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included flops.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nFlops = 0;
Gia_ManFillValue( p );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create PIs
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
Gia_ManForEachRo( p, pObj, i )
if ( !Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
pObj->Value = Gia_ManAppendCi(pNew);
// create POs
Gia_ManHashAlloc( pNew );
Gia_ManForEachPo( p, pObj, i )
{
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
// create RIs
Gia_ManForEachRi( p, pObj, i )
if ( Vec_IntEntry(vFlopClasses, i) )
{
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
nFlops++;
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, nFlops );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry > 0 );
pObj = Gia_ManObj( p, i );
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Collects PIs and PPIs of the abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
if ( pvPis ) *pvPis = Vec_IntAlloc( 100 );
if ( pvPPis ) *pvPPis = Vec_IntAlloc( 100 );
if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 );
if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
{ if ( pvPis ) Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) ); }
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
{ if ( pvPPis ) Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsRo(p, pObj) )
{ if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsAnd(pObj) )
{ if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); }
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntFree( vAssigned );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
Description [The array contains 1 for those objects (const, RO, AND)
that are included in the abstraction; 0, otherwise.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pCopy;
int i;//, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create additional arrays
Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// create constant
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
// create PIs
Gia_ManForEachObjVec( vPis, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
Gia_ManForEachObjVec( vPPis, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
Gia_ManForEachObjVec( vFlops, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create internal nodes
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// Gia_ManDupAbsGates_rec( pNew, pObj );
// create PO
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// create RIs
Gia_ManForEachObjVec( vFlops, p, pObj, i )
Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
// transfer copy values: (p -> pTemp -> pNew) => (p -> pNew)
if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) )
{
// printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
Gia_ManForEachObj( p, pObj, i )
{
if ( !~pObj->Value )
continue;
assert( !Abc_LitIsCompl(pObj->Value) );
pCopy = Gia_ObjCopy( pTemp, pObj );
if ( !~pCopy->Value )
{
Vec_IntWriteEntry( vGateClasses, i, 0 );
pObj->Value = ~0;
continue;
}
assert( !Abc_LitIsCompl(pCopy->Value) );
pObj->Value = pCopy->Value;
}
}
Gia_ManStop( pTemp );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
return pNew;
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintFlopClasses( Gia_Man_t * p )
{
int Counter0, Counter1;
if ( p->vFlopClasses == NULL )
return;
if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) )
{
printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ",
Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
printf( "and there are other FF classes..." );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
int nTotal;
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
{
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
// create additional arrays
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1),
nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintObjClasses( Gia_Man_t * p )
{
Vec_Int_t * vSeens; // objects seen so far
Vec_Int_t * vAbs = p->vObjClasses;
int i, k, Entry, iStart, iStop = -1, nFrames;
int nObjBits, nObjMask, iObj, iFrame, nWords;
unsigned * pInfo;
int * pCountAll, * pCountUni;
if ( vAbs == NULL )
return;
nFrames = Vec_IntEntry( vAbs, 0 );
assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
pCountAll = ABC_ALLOC( int, nFrames + 1 );
pCountUni = ABC_ALLOC( int, nFrames + 1 );
// start storage for seen objects
nWords = Abc_BitWordNum( nFrames );
vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
// get the bitmasks
nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask );
// print info about frames
printf( "Frame Core F0 F1 F2 F3 ...\n" );
for ( i = 0; i < nFrames; i++ )
{
iStart = Vec_IntEntry( vAbs, i+1 );
iStop = Vec_IntEntry( vAbs, i+2 );
memset( pCountAll, 0, sizeof(int) * (nFrames + 1) );
memset( pCountUni, 0, sizeof(int) * (nFrames + 1) );
Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
{
iObj = (Entry & nObjMask);
iFrame = (Entry >> nObjBits);
pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
{
Abc_InfoSetBit( pInfo, iFrame );
pCountUni[iFrame+1]++;
pCountUni[0]++;
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
}
assert( pCountAll[0] == (iStop - iStart) );
// printf( "%5d%5d ", pCountAll[0], pCountUni[0] );
printf( "%3d :", i );
printf( "%7d", pCountAll[0] );
if ( i >= 10 )
{
for ( k = 0; k < 4; k++ )
printf( "%5d", pCountAll[k+1] );
printf( " ..." );
for ( k = i-4; k <= i; k++ )
printf( "%5d", pCountAll[k+1] );
}
else
{
for ( k = 0; k <= i; k++ )
if ( k <= i )
printf( "%5d", pCountAll[k+1] );
}
// for ( k = 0; k < nFrames; k++ )
// if ( k <= i )
// printf( "%5d", pCountAll[k+1] );
printf( "\n" );
}
assert( iStop == Vec_IntSize(vAbs) );
Vec_IntFree( vSeens );
ABC_FREE( pCountAll );
ABC_FREE( pCountUni );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

22
src/aig/gia/giaAbsGla2.c → src/proof/abs/absGla.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [gia.c]
FileName [absGla2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Scalable gate-level abstraction.]
@ -14,16 +14,16 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absGla2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAbsRef.h"
//#include "giaAbsRef2.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
#include "abs.h"
#include "absRef.h"
//#include "absRef2.h"
ABC_NAMESPACE_IMPL_START
@ -38,7 +38,7 @@ struct Ga2_Man_t_
{
// user data
Gia_Man_t * pGia; // working AIG manager
Gia_ParVta_t * pPars; // parameters
Abs_Par_t * pPars; // parameters
// markings
Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1
// abstraction
@ -378,7 +378,7 @@ void Ga2_ManComputeTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
{
Ga2_Man_t * p;
p = ABC_CALLOC( Ga2_Man_t, 1 );
@ -415,7 +415,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
return p;
}
void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN )
void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN )
{
FILE * pFile;
char pFileName[32];
@ -1525,7 +1525,7 @@ void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
{
int fUseSecondCore = 1;
Ga2_Man_t * p;
@ -1866,7 +1866,7 @@ finish:
if ( p->pPars->fVerbose )
Abc_Print( 1, "\n" );
if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" );
Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
Abc_Print( 1, "True counter-example detected in frame %d. ", f );
p->pPars->iFrame = f - 1;
Vec_IntFreeP( &pAig->vGateClasses );

25
src/aig/gia/giaAbsGla.c → src/proof/abs/absGlaOld.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsGla.c]
FileName [absGla.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Gate-level abstraction.]
@ -14,16 +14,15 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "giaAbsRef.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
#include "abs.h"
#include "absRef.h"
ABC_NAMESPACE_IMPL_START
@ -65,7 +64,7 @@ struct Gla_Man_t_
// user data
Gia_Man_t * pGia0; // starting AIG manager
Gia_Man_t * pGia; // working AIG manager
Gia_ParVta_t* pPars; // parameters
Abs_Par_t * pPars; // parameters
// internal data
Vec_Int_t * vAbs; // abstracted objects
Gla_Obj_t * pObjRoot; // the primary output
@ -823,7 +822,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
SeeAlso []
***********************************************************************/
Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Abs_Par_t * pPars )
{
Gla_Man_t * p;
Aig_Man_t * pAig;
@ -1000,7 +999,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
SeeAlso []
***********************************************************************/
Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Abs_Par_t * pPars )
{
Gla_Man_t * p;
Aig_Man_t * pAig;
@ -1637,10 +1636,10 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
{
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars );
extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
Gla_Man_t * p;
Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
Abc_Cex_t * pCex = NULL;
@ -1925,7 +1924,7 @@ finish:
ABC_FREE( pAig->pCexSeq );
pAig->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) )
Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" );
Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
Vec_IntFreeP( &pAig->vGateClasses );

12
src/aig/gia/giaAbsIter.c → src/proof/abs/absIter.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaIter.c]
FileName [absIter.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Iterative improvement of abstraction.]
@ -14,12 +14,11 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "abs.h"
ABC_NAMESPACE_IMPL_START
@ -49,7 +48,6 @@ static inline void Gia_ObjRemFromGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_In
***********************************************************************/
int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 )
{
extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
Gia_Man_t * pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
Aig_Man_t * pAig = Gia_ManToAigSimple( pAbs );
int nStart = 0;
@ -65,7 +63,7 @@ int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 )
Gia_ManStop( pAbs );
return iFrame;
}
Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose )
Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose )
{
Gia_Obj_t * pObj;
int i, iFrame0, iFrame;

6
src/aig/saig/saigAbsCba.c → src/proof/abs/absOldCex.c
View File

@ -18,9 +18,7 @@
***********************************************************************/
#include "saig.h"
#include "aig/gia/giaAig.h"
#include "aig/ioa/ioa.h"
#include "abs.h"
ABC_NAMESPACE_IMPL_START
@ -582,7 +580,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p )
}
// try reducing the frames
pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
// Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
Aig_ManStop( pManNew );
}

173
src/aig/saig/saigAbsStart.c → src/proof/abs/absOldRef.c
View File

@ -18,7 +18,7 @@
***********************************************************************/
#include "saig.h"
#include "abs.h"
#include "proof/ssw/ssw.h"
#include "proof/fra/fra.h"
#include "proof/bbr/bbr.h"
@ -35,6 +35,56 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, f;
if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
// else
// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
// start the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
for ( f = 0; f <= pCexAbs->iFrame; f++ )
{
Saig_ManForEachPi( pAbs, pObj, i )
{
if ( i == Saig_ManPiNum(p) )
break;
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
}
}
// verify the counter example
if ( !Saig_ManVerifyCex( p, pCex ) )
{
printf( "Saig_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 of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
}
return pCex;
}
/**Function*************************************************************
Synopsis [Find the first PI corresponding to the flop.]
@ -72,7 +122,6 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
***********************************************************************/
Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
{
extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
Vec_Int_t * vFlopsNew;
int i, Entry, RetValue;
*piRetValue = -1;
@ -233,73 +282,83 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC
/**Function*************************************************************
Synopsis [Computes the flops to remain after abstraction.]
Synopsis [Transform flop map into flop list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
{
int nUseStart = 0;
Aig_Man_t * pAbs, * pTemp;
Vec_Int_t * vFlops;
int Iter;//, clk = clock(), clk2 = clock();//, iFlop;
assert( Aig_ManRegNum(p) > 0 );
if ( pPars->fVerbose )
printf( "Performing counter-example-based refinement.\n" );
Aig_ManSetCioIds( p );
vFlops = Vec_IntStartNatural( 1 );
/*
iFlop = Saig_ManFindFirstFlop( p );
assert( iFlop >= 0 );
vFlops = Vec_IntAlloc( 1 );
Vec_IntPush( vFlops, iFlop );
*/
// create the resulting AIG
pAbs = Saig_ManDupAbstraction( p, vFlops );
if ( !pPars->fVerbose )
{
printf( "Init : " );
Aig_ManPrintStats( pAbs );
}
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
if ( pTemp == NULL )
{
ABC_FREE( p->pSeqModel );
p->pSeqModel = pAbs->pSeqModel;
pAbs->pSeqModel = NULL;
Aig_ManStop( pAbs );
break;
}
Aig_ManStop( pAbs );
pAbs = pTemp;
printf( "ITER %4d : ", Iter );
if ( !pPars->fVerbose )
Aig_ManPrintStats( pAbs );
// output the intermediate result of abstraction
Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
// check if the ratio is reached
if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
{
printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
Aig_ManStop( pAbs );
pAbs = NULL;
Vec_IntFree( vFlops );
vFlops = NULL;
break;
}
}
int i, Entry;
vFlops = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry )
Vec_IntPush( vFlops, i );
return vFlops;
}
/**Function*************************************************************
Synopsis [Transform flop list into flop map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops )
{
Vec_Int_t * vFlopClasses;
int i, Entry;
vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
Vec_IntForEachEntry( vFlops, Entry, i )
Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
return vFlopClasses;
}
/**Function*************************************************************
Synopsis [Refines abstraction using the latch map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )
{
Aig_Man_t * pNew;
Vec_Int_t * vFlops;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" );
return -1;
}
pNew = Gia_ManToAig( pGia, 0 );
vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
{
pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
Vec_IntFree( vFlops );
Aig_ManStop( pNew );
return 0;
}
Vec_IntFree( pGia->vFlopClasses );
pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
Vec_IntFree( vFlops );
Aig_ManStop( pNew );
return -1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

986
src/proof/abs/absOldSat.c Normal file
View File

@ -0,0 +1,986 @@
/**CFile****************************************************************
FileName [saigRefSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [SAT based refinement of a counter-example.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigRefSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// local manager
typedef struct Saig_RefMan_t_ Saig_RefMan_t;
struct Saig_RefMan_t_
{
// user data
Aig_Man_t * pAig; // user's AIG
Abc_Cex_t * pCex; // user's CEX
int nInputs; // the number of first inputs to skip
int fVerbose; // verbose flag
// unrolling
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs
};
// performs ternary simulation
extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Maps array of frame PI IDs into array of original PI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_RefManReason2Inputs( Saig_RefMan_t * p, Vec_Int_t * vReasons )
{
Vec_Int_t * vOriginal, * vVisited;
int i, Entry;
vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) );
vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
Vec_IntForEachEntry( vReasons, Entry, i )
{
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
assert( iInput >= 0 && iInput < Aig_ManCiNum(p->pAig) );
if ( Vec_IntEntry(vVisited, iInput) == 0 )
Vec_IntPush( vOriginal, iInput );
Vec_IntAddToEntry( vVisited, iInput, 1 );
}
Vec_IntFree( vVisited );
return vOriginal;
}
/**Function*************************************************************
Synopsis [Creates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons )
{
Abc_Cex_t * pCare;
int i, Entry, iInput, iFrame;
pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
Vec_IntForEachEntry( vReasons, Entry, i )
{
assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
}
return pCare;
}
/**Function*************************************************************
Synopsis [Returns reasons for the property to fail.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsCi(pObj) )
{
Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
return;
}
assert( Aig_ObjIsNode(pObj) );
if ( pObj->fPhase )
{
Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
}
else
{
int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
assert( !fPhase0 || !fPhase1 );
if ( !fPhase0 && fPhase1 )
Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
else if ( fPhase0 && !fPhase1 )
Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
else
{
int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
if ( iPrio0 <= iPrio1 )
Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
else
Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
}
}
}
/**Function*************************************************************
Synopsis [Returns reasons for the property to fail.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p )
{
Aig_Obj_t * pObj;
Vec_Int_t * vPrios, * vPi2Prio, * vReasons;
int i, CountPrios;
vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
// set PI values according to CEX
CountPrios = 0;
Aig_ManConst1(p->pFrames)->fPhase = 1;
Aig_ManForEachCi( p->pFrames, pObj, i )
{
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
// assign priority
if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 )
Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ );
// Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) );
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
}
// printf( "Priority numbers = %d.\n", CountPrios );
Vec_IntFree( vPi2Prio );
// traverse and set the priority
Aig_ManForEachNode( p->pFrames, pObj, i )
{
int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
pObj->fPhase = fPhase0 && fPhase1;
if ( fPhase0 && fPhase1 ) // both are one
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
else if ( !fPhase0 && fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
else if ( fPhase0 && !fPhase1 )
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
else // both are zero
Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
}
// check the property output
pObj = Aig_ManCo( p->pFrames, 0 );
assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) );
// select the reason
vReasons = Vec_IntAlloc( 100 );
Aig_ManIncrementTravId( p->pFrames );
if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
Vec_IntFree( vPrios );
return vReasons;
}
/**Function*************************************************************
Synopsis [Collect nodes in the unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
{
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
if ( Aig_ObjIsCo(pObj) )
Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
else if ( Aig_ObjIsNode(pObj) )
{
Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
}
if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
Vec_IntPush( vObjs, Aig_ObjId(pObj) );
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
Vec_Vec_t * vFrameObjs; // the list of objects per frame
Vec_Int_t * vRoots, * vObjs;
Aig_Obj_t * pObj;
int i, f;
// sanity checks
assert( Saig_ManPiNum(pAig) == pCex->nPis );
assert( Saig_ManRegNum(pAig) == pCex->nRegs );
assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
// map PIs of the unrolled frames into PIs of the original design
*pvMapPiF2A = Vec_IntAlloc( 1000 );
// collect COs and Objs visited in each frame
vFrameCos = Vec_VecStart( pCex->iFrame+1 );
vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
// initialized the topmost frame
pObj = Aig_ManCo( pAig, pCex->iPo );
Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
for ( f = pCex->iFrame; f >= 0; f-- )
{
// collect nodes starting from the roots
Aig_ManIncrementTravId( pAig );
vRoots = Vec_VecEntryInt( vFrameCos, f );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ManUnrollCollect_rec( pAig, pObj,
Vec_VecEntryInt(vFrameObjs, f),
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
}
// derive unrolled timeframes
pFrames = Aig_ManStart( 10000 );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
// initialize the flops
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
// iterate through the frames
for ( f = 0; f <= pCex->iFrame; f++ )
{
// construct
vObjs = Vec_VecEntryInt( vFrameObjs, f );
Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else if ( Aig_ObjIsCo(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pFrames);
else if ( Saig_ObjIsPi(pAig, pObj) )
{
if ( Aig_ObjCioId(pObj) < nInputs )
{
int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
}
else
{
pObj->pData = Aig_ObjCreateCi( pFrames );
Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
Vec_IntPush( *pvMapPiF2A, f );
}
}
}
if ( f == pCex->iFrame )
break;
// transfer
vRoots = Vec_VecEntryInt( vFrameCos, f );
Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
}
// create output
pObj = Aig_ManCo( pAig, pCex->iPo );
Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
Aig_ManSetRegNum( pFrames, 0 );
// cleanup
Vec_VecFree( vFrameCos );
Vec_VecFree( vFrameObjs );
// finallize
Aig_ManCleanup( pFrames );
// return
return pFrames;
}
/**Function*************************************************************
Synopsis [Creates refinement manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
Saig_RefMan_t * p;
p = ABC_CALLOC( Saig_RefMan_t, 1 );
p->pAig = pAig;
p->pCex = pCex;
p->nInputs = nInputs;
p->fVerbose = fVerbose;
p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A );
return p;
}
/**Function*************************************************************
Synopsis [Destroys refinement manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_RefManStop( Saig_RefMan_t * p )
{
Aig_ManStopP( &p->pFrames );
Vec_IntFreeP( &p->vMapPiF2A );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Sets phase bits in the timeframe AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 )
{
Aig_Obj_t * pObj;
int i, iFrame, iInput;
Aig_ManConst1( p->pFrames )->fPhase = 1;
Aig_ManForEachCi( p->pFrames, pObj, i )
{
iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
// update value if it is a don't-care
if ( pCare && !Abc_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) )
pObj->fPhase = fValue1;
}
Aig_ManForEachNode( p->pFrames, pObj, i )
pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
Aig_ManForEachCo( p->pFrames, pObj, i )
pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) );
pObj = Aig_ManCo( p->pFrames, 0 );
return pObj->fPhase;
}
/**Function*************************************************************
Synopsis [Tries to remove literals from abstraction.]
Description [The literals are sorted more desirable first.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps )
{
Vec_Vec_t * vLits;
Vec_Int_t * vVar2New;
int i, Entry, iInput, iFrame;
// collect literals
vLits = Vec_VecAlloc( 100 );
vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
Vec_IntForEachEntry( vAssumps, Entry, i )
{
int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
// Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
if ( Vec_IntEntry( vVar2New, iInput ) == ~0 )
Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) );
Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry );
}
Vec_IntFree( vVar2New );
return vLits;
}
/**Function*************************************************************
Synopsis [Generate the care set using SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps )
{
Abc_Cex_t * pCare;
int i, Entry, iInput, iFrame;
// create counter-example
pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
Vec_IntForEachEntry( vAssumps, Entry, i )
{
int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
}
return pCare;
}
/**Function*************************************************************
Synopsis [Generate the care set using SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
{
int nConfLimit = 1000000;
Abc_Cex_t * pCare;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
Vec_Vec_t * vLits = NULL;
Vec_Int_t * vAssumps, * vVar2PiId;
int i, k, Entry, RetValue;//, f = 0, Counter = 0;
int nCoreLits, * pCoreLits;
clock_t clk = clock();
// create CNF
assert( Aig_ManRegNum(p->pFrames) == 0 );
// pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
RetValue = Saig_RefManSetPhases( p, NULL, 0 );
if ( RetValue )
{
printf( "Constructed frames are incorrect.\n" );
Cnf_DataFree( pCnf );
return NULL;
}
Cnf_DataTranformPolarity( pCnf, 0 );
// create SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
Cnf_DataFree( pCnf );
return NULL;
}
//Abc_PrintTime( 1, "Preparing", clock() - clk );
// look for a true counter-example
if ( p->nInputs > 0 )
{
RetValue = sat_solver_solve( pSat, NULL, NULL,
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
{
printf( "The problem is trivially UNSAT. The CEX is real.\n" );
// create counter-example
pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
return pCare;
}
// the problem is SAT - it is expected
}
// create assumptions
vVar2PiId = Vec_IntStartFull( pCnf->nVars );
vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
Aig_ManForEachCi( p->pFrames, pObj, i )
{
// RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
// Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
}
// reverse the order of assumptions
// if ( fNewOrder )
// Vec_IntReverseOrder( vAssumps );
if ( fNewOrder )
{
// create literals
vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
// sort literals
Vec_VecSort( vLits, 1 );
// save literals
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
Vec_IntPush( vAssumps, Entry );
for ( i = 0; i < Vec_VecSize(vLits); i++ )
printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
printf( "\n" );
if ( p->fVerbose )
printf( "Total PIs = %d. Essential PIs = %d.\n",
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
}
// solve
clk = clock();
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
//Abc_PrintTime( 1, "Solving", clock() - clk );
if ( RetValue != l_False )
{
if ( RetValue == l_True )
printf( "Internal Error!!! The resulting problem is SAT.\n" );
else
printf( "Internal Error!!! SAT solver timed out.\n" );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_IntFree( vAssumps );
Vec_IntFree( vVar2PiId );
return NULL;
}
assert( RetValue == l_False ); // UNSAT
// get relevant SAT literals
nCoreLits = sat_solver_final( pSat, &pCoreLits );
assert( nCoreLits > 0 );
if ( p->fVerbose )
printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n",
nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
// save literals
Vec_IntClear( vAssumps );
for ( i = 0; i < nCoreLits; i++ )
Vec_IntPush( vAssumps, pCoreLits[i] );
// create literals
vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
// sort literals
// Vec_VecSort( vLits, 0 );
// save literals
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
Vec_IntPush( vAssumps, Entry );
// for ( i = 0; i < Vec_VecSize(vLits); i++ )
// printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
// printf( "\n" );
if ( p->fVerbose )
printf( "Total PIs = %d. Essential PIs = %d.\n",
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
/*
// try assumptions in different order
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
// create different sets of assumptions
Counter = Vec_VecSize(vLits);
for ( f = 0; f < Vec_VecSize(vLits); f++ )
{
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
if ( i != f )
Vec_IntPush( vAssumps, Entry );
// try the new assumptions
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
if ( RetValue != l_False )
continue;
// UNSAT - remove literals
Vec_IntClear( Vec_VecEntryInt(vLits, f) );
Counter--;
}
for ( i = 0; i < Vec_VecSize(vLits); i++ )
printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
printf( "\n" );
if ( p->fVerbose )
printf( "Total PIs = %d. Essential PIs = %d.\n",
Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
// save literals
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
Vec_IntPush( vAssumps, Entry );
*/
// create counter-example
pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps );
// cleanup
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_IntFree( vAssumps );
Vec_IntFree( vVar2PiId );
Vec_VecFreeP( &vLits );
// verify counter-example
RetValue = Saig_RefManSetPhases( p, pCare, 0 );
if ( RetValue )
printf( "Reduced CEX verification has failed.\n" );
RetValue = Saig_RefManSetPhases( p, pCare, 1 );
if ( RetValue )
printf( "Reduced CEX verification has failed.\n" );
return pCare;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis )
{
int nConfLimit = 1000000;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
Vec_Vec_t * vLits;
Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId;
int i, k, f, Entry, RetValue, Counter;
// create CNF and SAT solver
pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
Cnf_DataFree( pCnf );
return NULL;
}
// mark used AIG inputs
vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
Vec_IntForEachEntry( vAigPis, Entry, i )
{
assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pAig) );
Vec_IntWriteEntry( vVisited, Entry, 1 );
}
// create assumptions
vVar2PiId = Vec_IntStartFull( pCnf->nVars );
vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
Aig_ManForEachCi( p->pFrames, pObj, i )
{
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
if ( Vec_IntEntry(vVisited, iInput) == 0 )
continue;
RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
// Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
}
Vec_IntFree( vVisited );
// try assumptions in different order
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
/*
// AnalizeFinal does not work because it implications propagate directly
// and SAT solver does not kick in (the number of conflicts in 0).
// count the number of lits in the unsat core
{
int nCoreLits, * pCoreLits;
nCoreLits = sat_solver_final( pSat, &pCoreLits );
assert( nCoreLits > 0 );
// count the number of flops
vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
for ( i = 0; i < nCoreLits; i++ )
{
int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
Vec_IntWriteEntry( vVisited, iInput, 1 );
}
// count the number of entries
Counter = 0;
Vec_IntForEachEntry( vVisited, Entry, i )
Counter += Entry;
Vec_IntFree( vVisited );
// if ( p->fVerbose )
printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n",
nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts );
}
*/
// derive literals
vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
for ( i = 0; i < Vec_VecSize(vLits); i++ )
printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
printf( "\n" );
// create different sets of assumptions
Counter = Vec_VecSize(vLits);
for ( f = 0; f < Vec_VecSize(vLits); f++ )
{
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
if ( i != f )
Vec_IntPush( vAssumps, Entry );
// try the new assumptions
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
if ( RetValue != l_False )
continue;
// UNSAT - remove literals
Vec_IntClear( Vec_VecEntryInt(vLits, f) );
Counter--;
}
for ( i = 0; i < Vec_VecSize(vLits); i++ )
printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
printf( "\n" );
// create assumptions
Vec_IntClear( vAssumps );
Vec_VecForEachEntryInt( vLits, Entry, i, k )
Vec_IntPush( vAssumps, Entry );
// try assumptions in different order
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
// if ( p->fVerbose )
// printf( "Total PIs = %d. Essential PIs = %d.\n",
// Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
// transform assumptions into reasons
vReasons = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vAssumps, Entry, i )
{
int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
Vec_IntPush( vReasons, iPiNum );
}
// cleanup
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_IntFree( vAssumps );
Vec_IntFree( vVar2PiId );
Vec_VecFreeP( &vLits );
return vReasons;
}
/**Function*************************************************************
Synopsis [SAT-based refinement of the counter-example.]
Description [The first parameter (nInputs) indicates how many first
primary inputs to skip without considering as care candidates.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose )
{
Saig_RefMan_t * p;
Vec_Int_t * vReasons;
Abc_Cex_t * pCare;
clock_t clk = clock();
clk = clock();
p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
vReasons = Saig_RefManFindReason( p );
if ( fVerbose )
Aig_ManPrintStats( p->pFrames );
// if ( fVerbose )
{
Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons );
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
Vec_IntFree( vRes );
/*
////////////////////////////////////
Vec_IntFree( vReasons );
vReasons = Saig_RefManRefineWithSat( p, vRes );
////////////////////////////////////
Vec_IntFree( vRes );
vRes = Saig_RefManReason2Inputs( p, vReasons );
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
Vec_IntFree( vRes );
ABC_PRT( "Time", clock() - clk );
*/
}
pCare = Saig_RefManReason2Cex( p, vReasons );
Vec_IntFree( vReasons );
Saig_RefManStop( p );
if ( fVerbose )
Abc_CexPrintStats( pCex );
if ( fVerbose )
Abc_CexPrintStats( pCare );
return pCare;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
{
Saig_RefMan_t * p;
Vec_Int_t * vRes, * vReasons;
clock_t clk;
if ( Saig_ManPiNum(pAig) != pCex->nPis )
{
printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n",
Aig_ManCiNum(pAig), pCex->nPis );
return NULL;
}
clk = clock();
p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
vReasons = Saig_RefManFindReason( p );
vRes = Saig_RefManReason2Inputs( p, vReasons );
// if ( fVerbose )
{
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
}
/*
////////////////////////////////////
Vec_IntFree( vReasons );
vReasons = Saig_RefManRefineWithSat( p, vRes );
////////////////////////////////////
// derive new result
Vec_IntFree( vRes );
vRes = Saig_RefManReason2Inputs( p, vReasons );
// if ( fVerbose )
{
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
}
*/
Vec_IntFree( vReasons );
Saig_RefManStop( p );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

224
src/aig/saig/saigSimExt2.c → src/proof/abs/absOldSim.c
View File

@ -18,8 +18,7 @@
***********************************************************************/
#include "saig.h"
#include "proof/ssw/ssw.h"
#include "abs.h"
ABC_NAMESPACE_IMPL_START
@ -28,6 +27,44 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define SAIG_ZER 1
#define SAIG_ONE 2
#define SAIG_UND 3
static inline int Saig_ManSimInfoNot( int Value )
{
if ( Value == SAIG_ZER )
return SAIG_ONE;
if ( Value == SAIG_ONE )
return SAIG_ZER;
return SAIG_UND;
}
static inline int Saig_ManSimInfoAnd( int Value0, int Value1 )
{
if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER )
return SAIG_ZER;
if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE )
return SAIG_ONE;
return SAIG_UND;
}
static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
}
static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
{
unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
assert( Value >= SAIG_ZER && Value <= SAIG_UND );
Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
}
#define SAIG_ZER_NEW 0 // 0 not visited
#define SAIG_ONE_NEW 1 // 1 not visited
#define SAIG_ZER_OLD 2 // 0 visited
@ -86,12 +123,82 @@ static inline void Saig_ManSimInfo2Set( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj,
}
// performs ternary simulation
extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
//extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs ternary simulation for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
{
int Value0, Value1, Value;
Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
if ( Aig_ObjFaninC0(pObj) )
Value0 = Saig_ManSimInfoNot( Value0 );
if ( Aig_ObjIsCo(pObj) )
{
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
return Value0;
}
assert( Aig_ObjIsNode(pObj) );
Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
if ( Aig_ObjFaninC1(pObj) )
Value1 = Saig_ManSimInfoNot( Value1 );
Value = Saig_ManSimInfoAnd( Value0, Value1 );
Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
return Value;
}
/**Function*************************************************************
Synopsis [Performs ternary simulation for one design.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f, Entry, iBit = 0;
Saig_ManForEachLo( p, pObj, i )
Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
Saig_ManForEachPi( p, pObj, i )
Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
if ( vRes )
Vec_IntForEachEntry( vRes, Entry, i )
Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND );
Aig_ManForEachNode( p, pObj, i )
Saig_ManExtendOneEval( vSimInfo, pObj, f );
Aig_ManForEachCo( p, pObj, i )
Saig_ManExtendOneEval( vSimInfo, pObj, f );
if ( f == pCex->iFrame )
break;
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
}
// make sure the output of the property failed
pObj = Aig_ManCo( p, pCex->iPo );
return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
}
/**Function*************************************************************
Synopsis [Performs ternary simulation for one node.]
@ -361,117 +468,6 @@ ABC_PRT( "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Abc_Cex_t * pCare;
Aig_Obj_t * pObj;
Vec_Int_t * vRes, * vResInv;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
// start simulation data
Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
assert( Value == SAIG_ONE_NEW );
// derive implications of constants and primary inputs
Saig_ManForEachLo( p, pObj, i )
Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
for ( f = pCex->iFrame; f >= 0; f-- )
{
Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );
for ( i = 0; i < iFirstFlopPi; i++ )
Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo );
}
// recursively compute justification
Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo );
// create CEX
pCare = Abc_CexDup( pCex, pCex->nRegs );
memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
// select the result
vRes = Vec_IntAlloc( 1000 );
vResInv = Vec_IntAlloc( 1000 );
for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
{
int fFound = 0;
for ( f = pCex->iFrame; f >= 0; f-- )
{
Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f );
if ( Saig_ManSimInfo2IsOld( Value ) )
{
fFound = 1;
Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i );
}
}
if ( fFound )
Vec_IntPush( vRes, i );
else
Vec_IntPush( vResInv, i );
}
// resimulate to make sure it is valid
Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
assert( Value == SAIG_ONE );
Vec_IntFree( vResInv );
Vec_IntFree( vRes );
return pCare;
}
/**Function*************************************************************
Synopsis [Returns the array of PIs for flops that should not be absracted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose )
{
Abc_Cex_t * pCare;
Vec_Ptr_t * vSimInfo;
clock_t clk;
if ( Saig_ManPiNum(p) != pCex->nPis )
{
printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n",
Aig_ManCiNum(p), pCex->nPis );
return NULL;
}
Aig_ManFanoutStart( p );
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );
clk = clock();
pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
if ( fVerbose )
{
// printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
Abc_CexPrintStats( pCex );
Abc_CexPrintStats( pCare );
ABC_PRT( "Time", clock() - clk );
}
Vec_PtrFree( vSimInfo );
Aig_ManFanoutStop( p );
return pCare;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

17
src/aig/gia/giaAbsOut.c → src/proof/abs/absOut.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsOut.c]
FileName [absOut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Abstraction refinement outside of abstraction engines.]
@ -14,13 +14,11 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
#include "aig/saig/saig.h"
#include "abs.h"
ABC_NAMESPACE_IMPL_START
@ -92,7 +90,6 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi
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;
@ -431,11 +428,11 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra
pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
// perform abstraction for the new AIG
{
Gia_ParVta_t Pars, * pPars = &Pars;
Gia_VtaSetDefaultParams( pPars );
Abs_Par_t Pars, * pPars = &Pars;
Abs_ParSetDefaults( pPars );
pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra;
pPars->fVerbose = fVerbose;
RetValue = Ga2_ManPerform( pNew, pPars );
RetValue = Gia_ManPerformGla( pNew, pPars );
if ( RetValue == 0 ) // spurious SAT
{
Vec_IntFreeP( &pNew->vGateClasses );

6
src/aig/gia/giaAbsPth.c → src/proof/abs/absPth.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsPth.c]
FileName [absPth.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Interface to pthreads.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/

10
src/aig/gia/giaAbsRef.c → src/proof/abs/absRef.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsRef.c]
FileName [absRef.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Refinement manager.]
@ -14,13 +14,13 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAbsRef.h"
#include "sat/bsat/satSolver2.h"
#include "abs.h"
#include "absRef.h"
ABC_NAMESPACE_IMPL_START

10
src/aig/gia/giaAbsRef.h → src/proof/abs/absRef.h
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsRef.h]
FileName [absRef.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Refinement manager.]
@ -14,12 +14,12 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__gia__giaAbsRef_h
#define ABC__aig__gia__giaAbsRef_h
#ifndef ABC__proof_abs__AbsRef_h
#define ABC__proof_abs__AbsRef_h
////////////////////////////////////////////////////////////////////////

10
src/aig/gia/giaAbsRef2.c → src/proof/abs/absRef2.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsRef2.c]
FileName [absRef2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Refinement manager.]
@ -14,12 +14,12 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAbsRef2.h"
#include "abs.h"
#include "absRef2.h"
ABC_NAMESPACE_IMPL_START

10
src/aig/gia/giaAbsRef2.h → src/proof/abs/absRef2.h
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsRef2.h]
FileName [absRef2.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Refinement manager.]
@ -14,12 +14,12 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__gia__giaAbsRef2_h
#define ABC__aig__gia__giaAbsRef2_h
#ifndef ABC__proof_abs__AbsRef2_h
#define ABC__proof_abs__AbsRef2_h
////////////////////////////////////////////////////////////////////////

257
src/proof/abs/absUtil.c Normal file
View File

@ -0,0 +1,257 @@
/**CFile****************************************************************
FileName [absUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [Interface to pthreads.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: absUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_ParSetDefaults( Abs_Par_t * p )
{
memset( p, 0, sizeof(Abs_Par_t) );
p->nFramesMax = 0; // maximum frames
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearnedMax = 1000; // max number of learned clauses
p->nLearnedStart = 1000; // max number of learned clauses
p->nLearnedDelta = 200; // max number of learned clauses
p->nLearnedPerce = 70; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 0; // stop when less than this % of object is abstracted
p->nRatioMax = 30; // restart when more than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fPropFanout = 1; // propagate fanouts during refinement
p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
p->iFrameProved = -1; // the number of frames proved
p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction
}
/**Function*************************************************************
Synopsis [Converting VTA vector to GLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
{
Gia_Obj_t * pObj;
Vec_Int_t * vGla;
int nObjMask, nObjs = Gia_ManObjNum(p);
int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
// get the bitmask
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vGla = Vec_IntStart( nObjs );
Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
{
pObj = Gia_ManObj( p, (Entry & nObjMask) );
assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 );
}
Vec_IntWriteEntry( vGla, 0, nFrames );
return vGla;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to VTA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
{
Vec_Int_t * vVta;
int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
int i, k, j, Entry, Counter, nGlaSize;
//. get the GLA size
nGlaSize = Vec_IntSum(vGla);
// get the bitmask
nObjBits = Abc_Base2Log(nObjs);
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vVta = Vec_IntAlloc( 1000 );
Vec_IntPush( vVta, nFrames );
Counter = nFrames + 2;
for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
Vec_IntPush( vVta, Counter );
for ( i = 0; i < nFrames; i++ )
for ( k = 0; k <= i; k++ )
Vec_IntForEachEntry( vGla, Entry, j )
if ( Entry )
Vec_IntPush( vVta, (k << nObjBits) | j );
Counter = Vec_IntEntry(vVta, nFrames+1);
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
return vVta;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to FLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
if ( Gia_ObjIsRo(p, pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
}
/**Function*************************************************************
Synopsis [Converting FLA vector to GLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
{
Vec_Int_t * vGla;
Gia_Obj_t * pObj;
int i;
// mark const0 and relevant CI objects
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetTravIdCurrent(p, pObj);
Gia_ManForEachRo( p, pObj, i )
if ( !Vec_IntEntry(vFla, i) )
Gia_ObjSetTravIdCurrent(p, pObj);
// label all objects reachable from the PO and selected flops
vGla = Vec_IntStart( Gia_ManObjNum(p) );
Vec_IntWriteEntry( vGla, 0, 1 );
Gia_ManForEachPo( p, pObj, i )
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
Gia_ManForEachRi( p, pObj, i )
if ( Vec_IntEntry(vFla, i) )
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
return vGla;
}
/**Function*************************************************************
Synopsis [Converting GLA vector to FLA vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
{
Vec_Int_t * vFla;
Gia_Obj_t * pObj;
int i;
vFla = Vec_IntStart( Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Vec_IntWriteEntry( vFla, i, 1 );
return vFla;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla )
{
Gia_Obj_t * pObj;
int i, Count = 0;
Gia_ManForEachRo( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Count++;
return Count;
}
int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
{
Gia_Obj_t * pObj;
int i, Count = 0;
Gia_ManForEachAnd( p, pObj, i )
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
Count++;
return Count;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

50
src/aig/gia/giaAbsVta.c → src/proof/abs/absVta.c
View File

@ -1,10 +1,10 @@
/**CFile****************************************************************
FileName [giaAbsVta.c]
FileName [absVta.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
PackageName [Abstraction package.]
Synopsis [Variable time-frame abstraction.]
@ -14,13 +14,13 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbsVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: absVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
#include "abs.h"
ABC_NAMESPACE_IMPL_START
@ -47,7 +47,7 @@ struct Vta_Man_t_
{
// user data
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
Abs_Par_t * pPars; // parameters
// internal data
int nObjs; // the number of objects
int nObjsAlloc; // the number of objects allocated
@ -134,40 +134,6 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesMax = 0; // maximum frames
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearnedMax = 1000; // max number of learned clauses
p->nLearnedStart = 1000; // max number of learned clauses
p->nLearnedDelta = 200; // max number of learned clauses
p->nLearnedPerce = 70; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 0; // stop when less than this % of object is abstracted
p->nRatioMax = 30; // restart when more than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fPropFanout = 1; // propagate fanouts during refinement
p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
p->iFrameProved = -1; // the number of frames proved
p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction
}
/**Function*************************************************************
Synopsis [Converting from one array to per-frame arrays.]
@ -1014,7 +980,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
SeeAlso []
***********************************************************************/
Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
{
Vta_Man_t * p;
p = ABC_CALLOC( Vta_Man_t, 1 );
@ -1524,7 +1490,7 @@ void Gia_VtaPrintMemory( Vta_Man_t * p )
SeeAlso []
***********************************************************************/
int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
{
Vta_Man_t * p;
Vec_Int_t * vCore;
@ -1775,7 +1741,7 @@ finish:
SeeAlso []
***********************************************************************/
int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars )
{
int RetValue = -1;
if ( pAig->vObjClasses == NULL && pPars->fUseRollback )

15
src/proof/abs/module.make Normal file
View File

@ -0,0 +1,15 @@
SRC += src/proof/abs/abs.c \
src/proof/abs/absDup.c \
src/proof/abs/absGla.c \
src/proof/abs/absGlaOld.c \
src/proof/abs/absIter.c \
src/proof/abs/absOldCex.c \
src/proof/abs/absOldRef.c \
src/proof/abs/absOldSat.c \
src/proof/abs/absOldSim.c \
src/proof/abs/absOut.c \
src/proof/abs/absPth.c \
src/proof/abs/absRef.c \
src/proof/abs/absRef2.c \
src/proof/abs/absVta.c \
src/proof/abs/absUtil.c