summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAbs.c36
-rw-r--r--src/aig/gia/giaAig.c1
-rw-r--r--src/aig/gia/giaDup.c117
-rw-r--r--src/aig/gia/giaMan.c46
5 files changed, 165 insertions, 37 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2d677638..f53d05f3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -603,6 +603,7 @@ 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 );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
@@ -659,6 +660,7 @@ 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 Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
/*=== 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 f5327f8f..511f418c 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -366,6 +366,42 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
}
+/**Function*************************************************************
+
+ Synopsis [Derive unrolled timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars )
+{
+ extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
+ Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
+ Vec_Int_t * vGateClasses;
+ Aig_Man_t * pAig;
+/*
+ // check if flop classes are given
+ if ( pGia->vGateClasses == NULL )
+ {
+ Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
+ pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
+ }
+*/
+ // perform abstraction
+ pAig = Gia_ManToAigSimple( pGia );
+ vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
+ Aig_ManStop( pAig );
+
+ // update the map
+ Vec_IntFreeP( &pGia->vGateClasses );
+ pGia->vGateClasses = vGateClasses;
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index a38cf083..221593a1 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -350,6 +350,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
else
assert( 0 );
pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
+ assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
}
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
ABC_FREE( ppNodes );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index fdf94837..b879cb05 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1586,8 +1586,8 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
- Description [The array contains PIs, LOs, and internal nodes included.
- 0=unsed, 1=PI, 2=PPI, 3=FF, 4=AND.]
+ Description [The array contains 1 for those objects (const, RO, AND)
+ that are included in the abstraction; 0, otherwise.]
SideEffects []
@@ -1596,51 +1596,110 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
+ Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 );
- Gia_ManFillValue( p );
+ assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
+
+ // create included objects and their fanins
+ vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
+
+ // create additional arrays
+ vPis = Vec_IntAlloc( 1000 );
+ vPPis = Vec_IntAlloc( 1000 );
+ vFlops = Vec_IntAlloc( 1000 );
+ vNodes = Vec_IntAlloc( 1000 );
+ Gia_ManForEachObjVec( vAssigned, p, pObj, i )
+ {
+ if ( Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
+ else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsRo(p, pObj) )
+ Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
+ else assert( Gia_ObjIsConst0(pObj) );
+ }
+
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName );
- // create PIs
+ // create constant
+ Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
- Gia_ManForEachPi( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 1 )
- pObj->Value = Gia_ManAppendCi(pNew);
+ // create PIs
+ Gia_ManForEachObjVec( vPis, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
- Gia_ManForEachPi( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 2 )
- pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachObjVec( vPPis, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
- Gia_ManForEachRo( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 )
- pObj->Value = Gia_ManAppendCi(pNew);
- // create POs
- Gia_ManHashAlloc( pNew );
+ 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) );
+ // create PO
Gia_ManForEachPo( p, pObj, i )
- {
- Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- }
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// create RIs
- Gia_ManForEachRo( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 )
- {
- pObj = Gia_ObjRoToRi(p, pObj);
- Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- nFlops++;
- }
- Gia_ManHashStop( pNew );
- Gia_ManSetRegNum( pNew, nFlops );
+ 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 );
+ assert( Gia_ManObjNum(pTemp) == Gia_ManObjNum(pNew) );
Gia_ManStop( pTemp );
+
+ Vec_IntFree( vPis );
+ Vec_IntFree( vPPis );
+ Vec_IntFree( vFlops );
+ Vec_IntFree( vNodes );
+ Vec_IntFree( vAssigned );
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 == 1 );
+ 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;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index ab0c9bc1..f09ca7b5 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -179,7 +179,8 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
}
Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
- printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d ", Counter0, Counter1 );
+ 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" );
@@ -198,7 +199,10 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
- int i, Counter[5];
+ Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
+ Gia_Obj_t * pObj;
+ int i;
+
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@@ -206,12 +210,38 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
- for ( i = 0; i < 5; i++ )
- Counter[i] = Vec_IntCountEntry( p->vGateClasses, i );
- printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d AND = %d Unused = %d\n",
- Counter[1], Counter[2], Counter[3], Counter[4], Counter[0] );
- if ( Counter[0] + Counter[1] + Counter[2] + Counter[3] + Counter[4] != Gia_ManObjNum(p) )
- printf( "Gia_ManPrintGateClasses(): Mismatch in the object count.\n" );
+
+ // create included objects and their fanins
+ vAssigned = Gia_GlaCollectAssigned( p, p->vGateClasses );
+
+ // create additional arrays
+ vPis = Vec_IntAlloc( 1000 );
+ vPPis = Vec_IntAlloc( 1000 );
+ vFlops = Vec_IntAlloc( 1000 );
+ vNodes = Vec_IntAlloc( 1000 );
+ Gia_ManForEachObjVec( vAssigned, p, pObj, i )
+ {
+ if ( Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
+ else if ( !Vec_IntEntry(p->vGateClasses, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsRo(p, pObj) )
+ Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
+ else assert( Gia_ObjIsConst0(pObj) );
+ }
+
+ printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %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) );
+
+ Vec_IntFree( vPis );
+ Vec_IntFree( vPPis );
+ Vec_IntFree( vFlops );
+ Vec_IntFree( vNodes );
+ Vec_IntFree( vAssigned );
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:48:22 +0000