Skip to content

A
abc
Commit 49df91f0 by Alan Mishchenko
Options

Several bug fixes.

parent 64f31f98
Showing with 163 additions and 59 deletions
src/aig/gia/giaAbs.c
......@@ -227,52 +227,6 @@ Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew )
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig;
Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
return 0;
}
// derive abstraction
pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
vFlopsNew = Saig_ManPbaDerive( pAig, nFrames, nConfLimit, fVerbose );
Aig_ManStop( pAig );
// derive new classes
if ( vFlopsNew != NULL )
{
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 );
return 1;
}
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;
}
/**Function*************************************************************
Synopsis [Adds flops that should be present in the abstraction.]
Description [The second argument (vAbsFfsToAdd) is the array of numbers
......@@ -350,6 +304,71 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
return -1;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
return 0;
}
// derive abstraction
pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose );
Aig_ManStop( pAig );
// derive new classes
if ( pAig->pSeqModel == 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 );
return -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_ManPiNum(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;
}
else
{
// found counter-eample for the abstracted model
// update flop classes
Vec_Int_t * vAbsFfsToAdd = vFlopsNew;
Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
Vec_IntFree( vAbsFfsToAdd );
return -1;
}
}
////////////////////////////////////////////////////////////////////////
......
src/aig/saig/saig.h
......@@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t
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 nFrames, int nConfLimit, int fVerbose );
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose );
/*=== sswAbsStart.c ==========================================================*/
extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
......
src/aig/saig/saigAbsPba.c
......@@ -72,7 +72,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
......@@ -107,6 +107,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreatePi(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++ )
{
......@@ -119,7 +120,10 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
else if ( Aig_ObjIsPo(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Saig_ObjIsPi(pAig, pObj) )
{
Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManPiNum(pFrames) );
pObj->pData = Aig_ObjCreatePi( pFrames );
}
else if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pFrames);
else if ( !Saig_ObjIsLo(pAig, pObj) )
......@@ -155,6 +159,37 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
/**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;
int i, f, Entry;
pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
Vec_IntForEachEntry( vPiVarMap, Entry, i )
if ( Entry >= 0 )
{
int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ];
if ( sat_solver_var_value( pSat, iSatVar ) )
Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i );
}
// check what frame has failed
for ( f = 0; f < nFrames; f++ )
{
// Aig_ManForEach
}
return pCex;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
......@@ -164,9 +199,9 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose )
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose )
{
Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps;
Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
......@@ -176,7 +211,7 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, in
// create SAT solver
clk = clock();
pFrames = Saig_ManUnrollForPba( pAig, nFrames );
pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap );
if ( fVerbose )
Aig_ManPrintStats( pFrames );
// pCnf = Cnf_DeriveSimple( pFrames, 0 );
......@@ -212,9 +247,29 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
if ( RetValue != l_False )
{
if ( RetValue == l_True )
printf( "Saig_ManPerformPba(): Internal Error!!! The resulting problem is SAT.\n" );
{
Vec_Int_t * vAbsFfsToAdd;
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
{
Vec_IntFree( vAbsFfsToAdd );
return NULL;
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 0, "Time", clock() - clk );
}
return vAbsFfsToAdd;
}
else
printf( "Saig_ManPerformPba(): SAT solver timed out.\n" );
{
printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" );
}
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
sat_solver_delete( pSat );
......@@ -242,6 +297,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
Vec_IntSort( vFlops, 0 );
// cleanup
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
sat_solver_delete( pSat );
......
src/aig/ssw/sswRarity.c
......@@ -899,7 +899,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
// check trivially SAT miters
if ( Ssw_RarCheckTrivial( pAig, fVerbose ) )
if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
return 0;
if ( fVerbose )
printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
......@@ -1006,7 +1006,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
// check trivially SAT miters
if ( Ssw_RarCheckTrivial( pAig, 1 ) )
if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
return 0;
if ( fVerbose )
printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
......
src/base/abci/abcDar.c
......@@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
// if ( pNtk->vSeqModelVec )
// Vec_PtrFreeFree( pNtk->vSeqModelVec );
// pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
else // if ( RetValue == 0 )
......@@ -1838,7 +1838,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
}
else
{
printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs );
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
printf( "All %d outputs are found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
printf( "None of the %d outputs is found to be SAT. ", nOutputs );
else
printf( "Some outputs (%d out of %d) are proved SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
ABC_PRT( "Time", clock() - clk );
......
src/misc/vec/vecPtr.h
......@@ -298,6 +298,25 @@ static inline int Vec_PtrSize( Vec_Ptr_t * p )
SeeAlso []
***********************************************************************/
static inline int Vec_PtrCountZero( Vec_Ptr_t * p )
{
int i, Counter = 0;
for ( i = 0; i < p->nSize; i++ )
Counter += (p->pArray[i] == NULL);
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment