summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaAbs.c40
-rw-r--r--src/aig/gia/giaDup.c75
3 files changed, 82 insertions, 34 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 195abcc9..3beed711 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -656,6 +656,7 @@ 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_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 7a4e51f4..2f7959a8 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -120,12 +120,12 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
+Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops )
{
Gia_Man_t * pGia;
Aig_Man_t * pNew, * pTemp;
pNew = Gia_ManToAig( p, 0 );
- pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops );
+ pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops );
Aig_ManStop( pTemp );
pGia = Gia_ManFromAig( pNew );
// pGia->vCiNumsOrig = pNew->vCiNumsOrig;
@@ -168,32 +168,6 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
/**Function*************************************************************
- Synopsis [Derives abstraction using the latch map.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia )
-{
- Vec_Int_t * vFlops;
- Gia_Man_t * pAbs = NULL;
- if ( pGia->vFlopClasses == NULL )
- {
- printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" );
- return NULL;
- }
- vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
- pAbs = Gia_ManCexAbstraction( pGia, vFlops );
- Vec_IntFree( vFlops );
- return pAbs;
-}
-
-/**Function*************************************************************
-
Synopsis [Refines abstraction using the latch map.]
Description []
@@ -273,8 +247,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
return 0;
}
// derive abstraction
- vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
- pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+ pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
@@ -283,6 +256,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
// 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 );
@@ -292,7 +266,6 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
Vec_IntFree( vFlops );
return 1;
}
- Vec_IntFree( vFlops );
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;
@@ -321,8 +294,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
}
// derive abstraction
- vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
- pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+ pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
@@ -331,6 +303,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
// derive new classes
if ( vFlopsNew != NULL )
{
+ vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
// vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew );
vSelected = NULL;
Vec_IntFree( pGia->vFlopClasses );
@@ -341,7 +314,6 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
Vec_IntFree( vFlops );
return 1;
}
- Vec_IntFree( vFlops );
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 0c9e2fb7..9942d37f 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1506,6 +1506,81 @@ 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_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
+{
+ if ( ~pObj->Value )
+ return;
+ Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
+ Gia_ManDupAbstraction_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_ManDupAbstraction( 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 = Gia_UtilStrsav( p->pName );
+ // 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_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ // create RIs
+ Gia_ManForEachRi( p, pObj, i )
+ if ( Vec_IntEntry(vFlopClasses, i) )
+ {
+ Gia_ManDupAbstraction_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;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-31 17:07:47 +0000