summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAbs.c3
-rw-r--r--src/aig/saig/saigAbs.c4
-rw-r--r--src/aig/saig/saigAbsCba.c125
3 files changed, 122 insertions, 10 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 533ba6a1..fca680a5 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -322,9 +322,8 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
// check if flop classes are given
if ( pGia->vFlopClasses == NULL )
{
- printf( "Gia_ManCbaPerform(): Empty abstraction is started.\n" );
+ Abc_Print( 0, "Initial flop map is not given. Trivial abstraction is assumed.\n" );
pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
- Vec_IntWriteEntry( pGia->vFlopClasses, 0, 1 );
}
// derive abstraction
pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index cf7e6809..19dbe0fd 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -19,10 +19,6 @@
***********************************************************************/
#include "saig.h"
-#include "ssw.h"
-#include "fra.h"
-#include "bbr.h"
-#include "pdr.h"
ABC_NAMESPACE_IMPL_START
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 169ff213..e317f80d 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -20,6 +20,7 @@
#include "saig.h"
#include "giaAig.h"
+#include "ioa.h"
ABC_NAMESPACE_IMPL_START
@@ -39,6 +40,9 @@ struct Saig_ManCba_t_
// unrolling
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs
+ // additional information
+ Vec_Vec_t * vReg2Frame; // register to frame mapping
+ Vec_Vec_t * vReg2Value; // register to value mapping
};
////////////////////////////////////////////////////////////////////////
@@ -47,6 +51,55 @@ struct Saig_ManCba_t_
/**Function*************************************************************
+ Synopsis [Duplicate with literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
+{
+ Vec_Int_t * vLevel;
+ Aig_Man_t * pAigNew;
+ Aig_Obj_t * pObj, * pMiter;
+ int i, k, Lit;
+ assert( pAig->nConstrs == 0 );
+ // start the new manager
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // create variables for PIs
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs for cubes
+ Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
+ {
+ pMiter = Aig_ManConst1( pAigNew );
+ Vec_IntForEachEntry( vLevel, Lit, k )
+ {
+ pObj = Saig_ManLi( pAig, Aig_Lit2Var(Lit) );
+ pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Aig_LitIsCompl(Lit)) );
+ }
+ Aig_ObjCreatePo( pAigNew, pMiter );
+ }
+ // transfer to register outputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ // finalize
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Maps array of frame PI IDs into array of additional PI IDs.]
Description []
@@ -205,13 +258,15 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
}
// check the property output
pObj = Aig_ManPo( p->pFrames, 0 );
- assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) );
+ pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+ assert( !pObj->fPhase );
// select the reason
vReasons = Vec_IntAlloc( 100 );
Aig_ManIncrementTravId( p->pFrames );
Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
Vec_IntFree( vPrios );
+ assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
return vReasons;
}
@@ -255,7 +310,7 @@ void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A )
+Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A, Vec_Vec_t ** pvReg2Frame )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
@@ -328,7 +383,14 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
// transfer
vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f );
Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+ {
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
+ if ( *pvReg2Frame )
+ {
+ Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) ); // record LO
+ Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjRealLit((Aig_Obj_t *)pObj->pData) ); // record its literal
+ }
+ }
}
// create output
pObj = Aig_ManPo( pAig, pCex->iPo );
@@ -362,7 +424,6 @@ Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput
p->pCex = pCex;
p->nInputs = nInputs;
p->fVerbose = fVerbose;
- p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A );
return p;
}
@@ -379,6 +440,8 @@ Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput
***********************************************************************/
void Saig_ManCbaStop( Saig_ManCba_t * p )
{
+ Vec_VecFreeP( &p->vReg2Frame );
+ Vec_VecFreeP( &p->vReg2Value );
Aig_ManStopP( &p->pFrames );
Vec_IntFreeP( &p->vMapPiF2A );
ABC_FREE( p );
@@ -386,6 +449,50 @@ void Saig_ManCbaStop( Saig_ManCba_t * p )
/**Function*************************************************************
+ Synopsis [Destroys refinement manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManCbaShrink( Saig_ManCba_t * p )
+{
+ Aig_Man_t * pManNew;
+ Aig_Obj_t * pObjLi, * pObjFrame;
+ Vec_Int_t * vLevel, * vLevel2;
+ int f, k, ObjId, Lit;
+ // assuming that important objects are labeled in Saig_ManCbaFindReason()
+ Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f )
+ {
+ Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k )
+ {
+ pObjFrame = Aig_ManObj( p->pFrames, Aig_Lit2Var(Lit) );
+ if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) )
+ continue;
+ pObjLi = Aig_ManObj( p->pAig, ObjId );
+ assert( Saig_ObjIsLi(p->pAig, pObjLi) );
+ Vec_VecPushInt( p->vReg2Value, f, Aig_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Aig_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
+ }
+ }
+ // print statistics
+ Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k )
+ {
+ vLevel2 = (Vec_Int_t *)Vec_VecEntry( p->vReg2Value, k );
+ printf( "Level = %4d StateBits = %4d (%6.2f %%) CareBits = %4d (%6.2f %%)\n", k,
+ Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig),
+ Vec_IntSize(vLevel2), 100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) );
+ }
+ // try reducing the frames
+ pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
+ Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
+ Aig_ManStop( pManNew );
+}
+
+/**Function*************************************************************
+
Synopsis [SAT-based refinement of the counter-example.]
Description [The first parameter (nInputs) indicates how many first
@@ -406,7 +513,14 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
clk = clock();
p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
+
+// p->vReg2Frame = Vec_VecStart( pCex->iFrame );
+// p->vReg2Value = Vec_VecStart( pCex->iFrame );
+ p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
vReasons = Saig_ManCbaFindReason( p );
+ if ( p->vReg2Frame )
+ Saig_ManCbaShrink( p );
+
if ( fVerbose )
Aig_ManPrintStats( p->pFrames );
@@ -458,6 +572,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex
clk = clock();
p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
+ p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
vReasons = Saig_ManCbaFindReason( p );
vRes = Saig_ManCbaReason2Inputs( p, vReasons );
if ( fVerbose )
@@ -492,7 +607,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
{
Vec_Int_t * vAbsFfsToAdd;
int RetValue, clk = clock();
- assert( pAbs->nRegs > 0 );
+// assert( pAbs->nRegs > 0 );
// perform BMC
RetValue = Saig_ManBmcScalable( pAbs, pPars );
if ( RetValue == -1 ) // time out - nothing to add
@@ -500,6 +615,8 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
assert( pAbs->pSeqModel == NULL );
return Vec_IntAlloc( 0 );
}
+ if ( pPars->fVerbose )
+ Abc_CexPrintStats( pAbs->pSeqModel );
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-01 09:44:12 +0000