summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcUnreach.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcUnreach.c')
-rw-r--r--src/base/abci/abcUnreach.c70
1 files changed, 42 insertions, 28 deletions
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index abc02cc3..ea0a4cd2 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -30,7 +30,7 @@ static DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk,
static Abc_Ntk_t * Abc_NtkConstructExdc ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFITIONS ///
+/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -58,11 +58,11 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
}
// compute the global BDDs of the latches
- dd = Abc_NtkGlobalBdds( pNtk, 1 );
+ dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
if ( dd == NULL )
return 0;
if ( fVerbose )
- printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+ printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// create the transition relation (dereferenced global BDDs)
bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose ); Cudd_Ref( bRelation );
@@ -87,13 +87,15 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
// allocate ZDD variables
Cudd_zddVarsFromBddVars( dd, 2 );
// create the EXDC network representing the unreachable states
+ if ( pNtk->pExdc )
+ Abc_NtkDelete( pNtk->pExdc );
pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
Cudd_RecursiveDeref( dd, bUnreach );
Extra_StopManager( dd );
- pNtk->pManGlob = NULL;
+// pNtk->pManGlob = NULL;
// make sure that everything is okay
- if ( !Abc_NtkCheck( pNtk->pExdc ) )
+ if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) )
{
printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
Abc_NtkDelete( pNtk->pExdc );
@@ -135,13 +137,15 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
Abc_NtkForEachLatch( pNtk, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
- bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd );
+// bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd );
+ bProd = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( bProd );
bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
// free the global BDDs
- Abc_NtkFreeGlobalBdds( pNtk );
+// Abc_NtkFreeGlobalBdds( pNtk );
+ Abc_NtkFreeGlobalBdds( pNtk, 0 );
// quantify the PI variables
bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs );
@@ -217,7 +221,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
{
DdNode * bRelation, * bReached, * bCubeCs;
DdNode * bCurrent, * bNext, * bTemp;
- int nIters;
+ int nIters, nMints;
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
@@ -254,9 +258,9 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
// report the stats
if ( fVerbose )
{
- fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
- fprintf( stdout, "The number of minterms in the reachable state set = %d.\n",
- (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) );
+ nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
+ fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+ fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
}
//PRB( dd, bReached );
Cudd_Deref( bReached );
@@ -282,15 +286,19 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
int i;
// start the new network
- pNtkNew = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_BDD );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
+ pNtkNew->pName = Extra_UtilStrsav( "exdc" );
+ pNtkNew->pSpec = NULL;
+
// create PIs corresponding to LOs
- Abc_NtkForEachLatch( pNtk, pNode, i )
- pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
+ Abc_NtkForEachLatchOutput( pNtk, pNode, i )
+ Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL );
+ // cannot ADD POs here because pLatch->pCopy point to the PIs
// create a new node
pNodeNew = Abc_NtkCreateNode(pNtkNew);
// add the fanins corresponding to latch outputs
- Abc_NtkForEachLatch( pNtk, pNode, i )
+ Abc_NtkForEachLatchOutput( pNtk, pNode, i )
Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
// create the logic function
@@ -304,28 +312,34 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
free( pPermute );
Abc_NodeMinimumBase( pNodeNew );
- // make the new node drive all the COs
- Abc_NtkForEachCo( pNtk, pNode, i )
- Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+ // for each CO, create PO (skip POs equal to CIs because of name conflict)
+ Abc_NtkForEachPo( pNtk, pNode, i )
+ if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+ Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
+ Abc_NtkForEachLatchInput( pNtk, pNode, i )
+ Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
- // store the PI names of the EXDC network
- Abc_NtkForEachLatch( pNtk, pNode, i )
- Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
- // store the PO names of the EXDC network
+ // link to the POs of the network
Abc_NtkForEachPo( pNtk, pNode, i )
- Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
- Abc_NtkForEachLatch( pNtk, pNode, i )
- Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") );
+ if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+ Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+ Abc_NtkForEachLatchInput( pNtk, pNode, i )
+ Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
- // make the network minimum base
- Abc_NtkMinimumBase( pNtkNew );
+ // remove the extra nodes
+ Abc_AigCleanup( pNtkNew->pManFunc );
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// transform the network to the SOP representation
- Abc_NtkBddToSop( pNtkNew );
+ if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+ {
+ printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
+ return NULL;
+ }
return pNtkNew;
+// return NULL;
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 15:52:09 +0000