summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h2
-rw-r--r--src/aig/aig/module.make4
-rw-r--r--src/aig/dar/darCut.c2
-rw-r--r--src/aig/fra/fra.h5
-rw-r--r--src/aig/fra/fraClass.c6
-rw-r--r--src/aig/fra/fraInd.c7
-rw-r--r--src/aig/fra/fraLcr.c2
-rw-r--r--src/aig/fra/fraSec.c6
-rw-r--r--src/aig/fra/fraSim.c2
-rw-r--r--src/aig/fra/module.make3
-rw-r--r--src/aig/ntl/module.make10
-rw-r--r--src/aig/ntl/ntl.h3
-rw-r--r--src/aig/ntl/ntlMan.c1
-rw-r--r--src/aig/ntl/ntlReadBlif.c86
-rw-r--r--src/aig/ntl/ntlTable.c39
15 files changed, 164 insertions, 14 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 03574655..6b34e853 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -160,6 +160,8 @@ struct Aig_Man_t_
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
+static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
+static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Aig_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline char * Aig_UtilStrsav( char * s ) { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; }
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index c35e7121..48d29115 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -1,6 +1,8 @@
SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigDfs.c \
src/aig/aig/aigFanout.c \
+ src/aig/aig/aigFrames.c \
+ src/aig/aig/aigHaig.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
src/aig/aig/aigMffc.c \
@@ -10,8 +12,10 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigPart.c \
src/aig/aig/aigRepr.c \
src/aig/aig/aigRet.c \
+ src/aig/aig/aigRetF.c \
src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
+ src/aig/aig/aigShow.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTime.c \
src/aig/aig/aigTiming.c \
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index 08bd77a9..b0aff095 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -479,7 +479,7 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
int i, k, nLeaves;
assert( pCut->fUsed );
- // compute the truth support of the cut's function
+ // compute the support of the cut's function
nLeaves = pCut->nLeaves;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
if ( (uTruth & uMasks[i][0]) == ((uTruth & uMasks[i][1]) >> (1 << i)) )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 8cd677d1..8d7116c7 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -76,6 +76,7 @@ struct Fra_Par_t_
int nFramesP; // the number of timeframes to in the prefix
int nFramesK; // the number of timeframes to unroll
int nMaxImps; // the maximum number of implications to consider
+ int nMaxLevs; // the maximum number of levels to consider
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
@@ -245,7 +246,7 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
+extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
@@ -274,7 +275,7 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
-extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
+extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 962e7f7b..2d03e65d 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -270,7 +270,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
SeeAlso []
***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
+void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
Aig_Obj_t ** ppTable, ** ppNexts;
Aig_Obj_t * pObj, * pTemp;
@@ -296,8 +296,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// skip the node with more that the given number of levels
-// if ( pObj->Level > 3 )
-// continue;
+ if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+ continue;
}
// hash the node by its simulation info
iEntry = p->pFuncNodeHash( pObj, nTableSize );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index dbc6401f..1c2140bb 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
@@ -282,12 +282,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
pPars->nFramesP = nFramesP;
pPars->nFramesK = nFramesK;
pPars->nMaxImps = nMaxImps;
+ pPars->nMaxLevs = nMaxLevs;
pPars->fVerbose = fVerbose;
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
pPars->fUseImps = fUseImps;
pPars->fWriteImps = fWriteImps;
-
+
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using K initialized frames
@@ -313,7 +314,7 @@ if ( fVerbose )
{
PRT( "Time", clock() - clk );
}
- Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+ Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
// allocate new simulation manager for simulating counter-examples
Fra_SmlStop( p->pSml );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index daa789a8..a6460ed7 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -550,7 +550,7 @@ timeSim = clock() - clk2;
// get preliminary info about equivalence classes
pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
- Fra_ClassesPrepare( p->pCla, 1 );
+ Fra_ClassesPrepare( p->pCla, 1, 0 );
p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
Fra_SmlStop( pTemp->pSml );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 17a7335c..4ccb48e3 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
}
else
{
@@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
@@ -185,7 +185,7 @@ PRT( "Time", clock() - clk );
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
- pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 3e8f2da1..1ad2d4f7 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -685,7 +685,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
Fra_SmlSimulateOne( p->pSml );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
- Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+ Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
// Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index e7264fdc..ffaca75c 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,12 +1,15 @@
SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraCec.c \
src/aig/fra/fraClass.c \
+ src/aig/fra/fraClau.c \
+ src/aig/fra/fraClaus.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
+ src/aig/fra/fraPart.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
src/aig/fra/fraSim.c
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
new file mode 100644
index 00000000..ea6070a4
--- /dev/null
+++ b/src/aig/ntl/module.make
@@ -0,0 +1,10 @@
+SRC += src/aig/mem/ntlAig.c \
+ src/aig/mem/ntlCheck.c \
+ src/aig/mem/ntlDfs.c \
+ src/aig/mem/ntlMan.c \
+ src/aig/mem/ntlMap.c \
+ src/aig/mem/ntlObj.c \
+ src/aig/mem/ntlReadBlif.c \
+ src/aig/mem/ntlTable.c \
+ src/aig/mem/ntlWriteBlif.c
+
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index e58047ae..af1e114d 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -86,6 +86,8 @@ struct Ntl_Mod_t_
Ntl_Net_t ** pTable; // the hash table of names into nets
int nTableSize; // the allocated table size
int nEntries; // the number of entries in the hash table
+ // delay information
+ Vec_Int_t * vDelays;
};
struct Ntl_Obj_t_
@@ -242,6 +244,7 @@ extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
/*=== ntlReadBlif.c ==========================================================*/
extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index cc9bd029..6d71adb2 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -152,6 +152,7 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
+ if ( p->vDelays ) Vec_IntFree( p->vDelays );
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index feb8e488..7c6ed069 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -36,6 +36,7 @@ struct Ioa_ReadMod_t_
Vec_Ptr_t * vLatches; // .latch lines
Vec_Ptr_t * vNames; // .names lines
Vec_Ptr_t * vSubckts; // .subckt lines
+ Vec_Ptr_t * vDelays; // .delay lines
int fBlackBox; // indicates blackbox model
// the resulting network
Ntl_Mod_t * pNtk;
@@ -79,6 +80,7 @@ static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLin
static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
+static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; }
@@ -245,6 +247,7 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
p->vLatches = Vec_PtrAlloc( 512 );
p->vNames = Vec_PtrAlloc( 512 );
p->vSubckts = Vec_PtrAlloc( 512 );
+ p->vDelays = Vec_PtrAlloc( 512 );
return p;
}
@@ -266,6 +269,7 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
Vec_PtrFree( p->vLatches );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vSubckts );
+ Vec_PtrFree( p->vDelays );
free( p );
}
@@ -492,6 +496,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
Vec_PtrPush( p->pLatest->vOutputs, pCur );
else if ( !strncmp(pCur, "subckt", 6) )
Vec_PtrPush( p->pLatest->vSubckts, pCur );
+ else if ( !strncmp(pCur, "delay", 5) )
+ Vec_PtrPush( p->pLatest->vDelays, pCur );
else if ( !strncmp(pCur, "blackbox", 8) )
p->pLatest->fBlackBox = 1;
else if ( !strncmp(pCur, "model", 5) )
@@ -551,6 +557,10 @@ static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
return;
+ // parse the delay info
+ Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
+ if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
+ return;
}
}
@@ -841,6 +851,82 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Parses the subckt line.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
+{
+ Vec_Ptr_t * vTokens = p->pMan->vTokens;
+ int RetValue1, RetValue2, Number1, Number2, Temp;
+ char * pToken;
+ float Delay;
+ assert( sizeof(float) == sizeof(int) );
+ Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+ pToken = Vec_PtrEntry(vTokens,0);
+ assert( !strcmp(pToken, "delay") );
+ if ( Vec_PtrSize(vTokens) < 2 && Vec_PtrSize(vTokens) > 4 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (1, 2, or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
+ return 0;
+ }
+ // find the delay number
+ Delay = atof( Vec_PtrEntryLast(vTokens) );
+ if ( Delay < 0.0 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
+ return 0;
+ }
+ // find the PI/PO numbers
+ RetValue1 = 0; Number1 = -1;
+ if ( Vec_PtrSize(vTokens) > 2 )
+ {
+ RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 );
+ if ( RetValue1 == 0 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+ return 0;
+ }
+ }
+ RetValue2 = 0; Number2 = -1;
+ if ( Vec_PtrSize(vTokens) > 3 )
+ {
+ RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 );
+ if ( RetValue2 == 0 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) );
+ return 0;
+ }
+ }
+ if ( RetValue1 == RetValue2 && RetValue1 )
+ {
+ sprintf( p->pMan->sError, "Line %d: Both signals \"%s\" and \"%s\" listed appear to be PIs or POs.",
+ Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), Vec_PtrEntry(vTokens, 2) );
+ return 0;
+ }
+ if ( RetValue2 < RetValue1 )
+ {
+ Temp = RetValue2; RetValue2 = RetValue1; RetValue1 = Temp;
+ Temp = Number2; Number2 = Number1; Number1 = Temp;
+ }
+ assert( RetValue1 == 0 || RetValue1 == -1 );
+ assert( RetValue2 == 0 || RetValue2 == 1 );
+ // store the values
+ if ( p->pNtk->vDelays == NULL )
+ p->pNtk->vDelays = Vec_IntAlloc( 100 );
+ Vec_IntPush( p->pNtk->vDelays, Number1 );
+ Vec_IntPush( p->pNtk->vDelays, Number2 );
+ Vec_IntPush( p->pNtk->vDelays, Aig_Float2Int(Delay) );
+ return 1;
+}
+
/**Function*************************************************************
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index 87048f10..b84ac1a5 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -171,6 +171,45 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
+{
+ Ntl_Net_t * pNet;
+ Ntl_Obj_t * pObj;
+ int i;
+ *pNumber = -1;
+ pNet = Ntl_ModelFindNet( p, pName );
+ if ( pNet == NULL )
+ return 0;
+ Ntl_ModelForEachPo( p, pObj, i )
+ {
+ if ( Ntl_ObjFanin0(pObj) == pNet )
+ {
+ *pNumber = i;
+ return 1;
+ }
+ }
+ Ntl_ModelForEachPi( p, pObj, i )
+ {
+ if ( Ntl_ObjFanout0(pObj) == pNet )
+ {
+ *pNumber = i;
+ return -1;
+ }
+ }
+ return 0;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////