summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h3
-rw-r--r--src/aig/aig/aigMan.c35
-rw-r--r--src/aig/aig/aigScl.c2
-rw-r--r--src/aig/ntl/ntlExtract.c4
-rw-r--r--src/aig/saig/saig.h82
-rw-r--r--src/aig/saig/saigPhase.c763
-rw-r--r--src/aig/saig/saig_.c47
7 files changed, 932 insertions, 4 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 9d6bde98..8593fd76 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -99,6 +99,8 @@ struct Aig_Man_t_
Aig_Obj_t * pConst1; // the constant 1 node
Aig_Obj_t Ghost; // the ghost node
int nRegs; // the number of registers (registers are last POs)
+ int nTruePis; // the number of registers (registers are last POs)
+ int nTruePos; // the number of registers (registers are last POs)
int nAsserts; // the number of asserts among POs (asserts are first POs)
// AIG node counters
int nObjs[AIG_OBJ_VOID];// the number of objects by type
@@ -486,6 +488,7 @@ extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
+extern int Aig_ManPiCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 4c4b7aad..ee782423 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -222,9 +222,9 @@ void Aig_ManStop( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Returns the number of dangling nodes removed.]
+ Synopsis [Removes combinational logic that does not feed into POs.]
- Description []
+ Description [Returns the number of dangling nodes removed.]
SideEffects []
@@ -251,6 +251,37 @@ int Aig_ManCleanup( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Removes PIs without fanouts.]
+
+ Description [Returns the number of PIs removed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManPiCleanup( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, k = 0, nPisOld = Aig_ManPiNum(p);
+ Vec_PtrForEachEntry( p->vPis, pObj, i )
+ {
+ if ( i >= Aig_ManPiNum(p) - Aig_ManRegNum(p) )
+ Vec_PtrWriteEntry( p->vPis, k++, pObj );
+ else if ( Aig_ObjRefs(pObj) > 0 )
+ Vec_PtrWriteEntry( p->vPis, k++, pObj );
+ else
+ Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+ }
+ Vec_PtrShrink( p->vPis, k );
+ p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+ if ( Aig_ManRegNum(p) )
+ p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+ return nPisOld - Aig_ManPiNum(p);
+}
+
+/**Function*************************************************************
+
Synopsis [Performs one iteration of AIG rewriting.]
Description []
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index c32f2f4f..34b3482d 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -230,6 +230,8 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
}
Vec_PtrFree( vNodes );
+ p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+ p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
// remove dangling nodes
return Aig_ManCleanup( p );
}
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index d474b4dd..18ca1a53 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -288,8 +288,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
}
// report the number of dangling objects
nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
- if ( nUselessObjects )
- printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
+// if ( nUselessObjects )
+// printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
// cleanup the AIG
Aig_ManCleanup( p->pAig );
// extract the timing manager
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
new file mode 100644
index 00000000..ce09fd32
--- /dev/null
+++ b/src/aig/saig/saig.h
@@ -0,0 +1,82 @@
+/**CFile****************************************************************
+
+ FileName [saig.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SAIG_H__
+#define __SAIG_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Saig_ManPiNum( Aig_Man_t * p ) { return p->nTruePis; }
+static inline int Saig_ManPoNum( Aig_Man_t * p ) { return p->nTruePos; }
+static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
+static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); }
+static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); }
+
+// iterator over the primary inputs/outputs
+#define Saig_ManForEachPi( p, pObj, i ) \
+ Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) )
+#define Saig_ManForEachPo( p, pObj, i ) \
+ Vec_PtrForEachEntryStop( p->vPos, pObj, i, Saig_ManPoNum(p) )
+// iterator over the latch inputs/outputs
+#define Saig_ManForEachLo( p, pObj, i ) \
+ for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPis, i+Saig_ManPiNum(p))), 1); i++ )
+#define Saig_ManForEachLi( p, pObj, i ) \
+ for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPos, i+Saig_ManPoNum(p))), 1); i++ )
+// iterator over the latch input and outputs
+#define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) \
+ for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \
+ && (((pObjLo)=Saig_ManLo(p, i)), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== saigPhase.c ==========================================================*/
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
new file mode 100644
index 00000000..f83666c4
--- /dev/null
+++ b/src/aig/saig/saigPhase.c
@@ -0,0 +1,763 @@
+/**CFile****************************************************************
+
+ FileName [saigPhase.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Automated phase abstraction.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigPhase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+/*
+ The algorithm is described in the paper: Per Bjesse and Jim Kukula,
+ "Automatic Phase Abstraction for Formal Verification", ICCAD 2005
+ http://www.iccad.com/data2/iccad/iccad_05acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1701ecf34b149e958725702f00708828?OpenDocument
+*/
+
+// the maximum number of cycles of termiry simulation
+#define TSIM_MAX_ROUNDS 10000
+#define TSIM_ONE_SERIES 3000
+
+#define SAIG_XVS0 1
+#define SAIG_XVS1 2
+#define SAIG_XVSX 3
+
+static inline int Saig_XsimConvertValue( int v ) { return v == 0? SAIG_XVS0 : (v == 1? SAIG_XVS1 : (v == 2? SAIG_XVSX : -1)); }
+
+static inline void Saig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
+static inline int Saig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
+static inline int Saig_XsimInv( int Value )
+{
+ if ( Value == SAIG_XVS0 )
+ return SAIG_XVS1;
+ if ( Value == SAIG_XVS1 )
+ return SAIG_XVS0;
+ assert( Value == SAIG_XVSX );
+ return SAIG_XVSX;
+}
+static inline int Saig_XsimAnd( int Value0, int Value1 )
+{
+ if ( Value0 == SAIG_XVS0 || Value1 == SAIG_XVS0 )
+ return SAIG_XVS0;
+ if ( Value0 == SAIG_XVSX || Value1 == SAIG_XVSX )
+ return SAIG_XVSX;
+ assert( Value0 == SAIG_XVS1 && Value1 == SAIG_XVS1 );
+ return SAIG_XVS1;
+}
+static inline int Saig_XsimRand2()
+{
+ return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0;
+}
+static inline int Saig_XsimRand3()
+{
+ int RetValue;
+ do {
+ RetValue = rand() & 3;
+ } while ( RetValue == 0 );
+ return RetValue;
+}
+static inline int Saig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Saig_ObjGetXsim(Aig_ObjFanin0(pObj));
+ return Aig_ObjFaninC0(pObj)? Saig_XsimInv(RetValue) : RetValue;
+}
+static inline int Saig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Saig_ObjGetXsim(Aig_ObjFanin1(pObj));
+ return Aig_ObjFaninC1(pObj)? Saig_XsimInv(RetValue) : RetValue;
+}
+static inline void Saig_XsimPrint( FILE * pFile, int Value )
+{
+ if ( Value == SAIG_XVS0 )
+ {
+ fprintf( pFile, "0" );
+ return;
+ }
+ if ( Value == SAIG_XVS1 )
+ {
+ fprintf( pFile, "1" );
+ return;
+ }
+ assert( Value == SAIG_XVSX );
+ fprintf( pFile, "x" );
+}
+
+// simulation manager
+typedef struct Saig_Tsim_t_ Saig_Tsim_t;
+struct Saig_Tsim_t_
+{
+ Aig_Man_t * pAig; // the original AIG manager
+ int nWords; // the number of words in the states
+ // ternary state representation
+ Vec_Ptr_t * vStates; // the collection of ternary states
+ Aig_MmFixed_t * pMem; // memory for ternary states
+ int nPrefix; // prefix of the ternary state space
+ int nCycle; // cycle of the ternary state space
+ int nNonXRegs; // the number of candidate registers
+ Vec_Int_t * vNonXRegs; // the candidate registers
+ // hash table for terminary states
+ unsigned ** pBins;
+ int nBins;
+};
+
+static inline unsigned * Saig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
+static inline void Saig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig )
+{
+ Saig_Tsim_t * p;
+ p = (Saig_Tsim_t *)malloc( sizeof(Saig_Tsim_t) );
+ memset( p, 0, sizeof(Saig_Tsim_t) );
+ p->pAig = pAig;
+ p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
+ p->vStates = Vec_PtrAlloc( 1000 );
+ p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
+ p->nBins = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2);
+ p->pBins = ALLOC( unsigned *, p->nBins );
+ memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_TsiStop( Saig_Tsim_t * p )
+{
+ if ( p->vNonXRegs )
+ Vec_IntFree( p->vNonXRegs );
+ Aig_MmFixedStop( p->pMem, 0 );
+ Vec_PtrFree( p->vStates );
+ free( p->pBins );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value of the node using its simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
+{
+ static int s_FPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ unsigned uHash;
+ int i;
+ uHash = 0;
+ for ( i = 0; i < nWords; i++ )
+ uHash ^= pState[i] * s_FPrimes[i & 0x7F];
+ return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count non-X-valued registers in the simulation data.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords )
+{
+ unsigned * pState;
+ int nRegs = p->pAig->nRegs;
+ int Value, i, k;
+ assert( p->vNonXRegs == NULL );
+ p->vNonXRegs = Vec_IntAlloc( 10 );
+ for ( i = 0; i < nRegs; i++ )
+ {
+ Vec_PtrForEachEntry( p->vStates, pState, k )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ assert( Value != 0 );
+ if ( Value == SAIG_XVSX )
+ break;
+ }
+ if ( k == Vec_PtrSize(p->vStates) )
+ Vec_IntPush( p->vNonXRegs, i );
+ }
+ return Vec_IntSize(p->vNonXRegs);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count non-X-valued registers in the simulation data.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
+{
+ unsigned * pState;
+ int nRegs = p->pAig->nRegs;
+ int Value, i, k, Counter = 0;
+ if ( Vec_PtrSize(p->vStates) > 80 )
+ return;
+ for ( i = 0; i < nRegs; i++ )
+ {
+ Vec_PtrForEachEntry( p->vStates, pState, k )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ if ( Value == SAIG_XVSX )
+ break;
+ }
+ if ( k == Vec_PtrSize(p->vStates) )
+ Counter++;
+ else
+ continue;
+ // print trace
+ printf( "%5d : %5d ", Counter, i );
+ Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ if ( Value == SAIG_XVS0 )
+ printf( "0" );
+ else if ( Value == SAIG_XVS1 )
+ printf( "1" );
+ else if ( Value == SAIG_XVSX )
+ printf( "x" );
+ else
+ assert( 0 );
+ if ( k == nPrefix - 1 )
+ printf( " " );
+ }
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of the state.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_TsiComputePrefix( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+ unsigned * pEntry, * pPrev;
+ int Hash, i;
+ Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+ for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
+ if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+ {
+ Vec_PtrForEachEntry( p->vStates, pPrev, i )
+ {
+ if ( pPrev == pEntry )
+ return i;
+ }
+ assert( 0 );
+ return -1;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the value exists in the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_TsiStateLookup( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+ unsigned * pEntry;
+ int Hash;
+ Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+ for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
+ if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_TsiStateInsert( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+ int Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+ assert( !Saig_TsiStateLookup( p, pState, nWords ) );
+ Saig_TsiSetNext( pState, nWords, p->pBins[Hash] );
+ p->pBins[Hash] = pState;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Saig_TsiStateNew( Saig_Tsim_t * p )
+{
+ unsigned * pState;
+ pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
+ memset( pState, 0, sizeof(unsigned) * p->nWords );
+ Vec_PtrPush( p->vStates, pState );
+ return pState;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState )
+{
+ int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
+ for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ if ( Value == SAIG_XVS0 )
+ printf( "0" ), nZeros++;
+ else if ( Value == SAIG_XVS1 )
+ printf( "1" ), nOnes++;
+ else if ( Value == SAIG_XVSX )
+ printf( "x" ), nDcs++;
+ else
+ assert( 0 );
+ }
+ printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count constant values in the state.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState )
+{
+ Aig_Obj_t * pObjLi, * pObjLo;
+ int i, Value, nCounter = 0;
+ Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1);
+ }
+ return nCounter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count constant values in the state.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState )
+{
+ unsigned * pPrev;
+ int i, k;
+ Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+ {
+ for ( k = 0; k < pTsi->nWords; k++ )
+ pState[k] |= pPrev[k];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cycles the circuit to create a new initial state.]
+
+ Description [Simulates the circuit with random input for the given
+ number of timeframes to get a better initial state.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
+{
+ Saig_Tsim_t * pTsi;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ unsigned * pState;
+ int i, f, Value, nCounter;
+ // allocate the simulation manager
+ pTsi = Saig_TsiStart( p );
+ // initialize the values
+ Saig_ObjSetXsim( Aig_ManConst1(p), SAIG_XVS1 );
+ Saig_ManForEachPi( p, pObj, i )
+ Saig_ObjSetXsim( pObj, SAIG_XVSX );
+ if ( vInits )
+ {
+ Saig_ManForEachLo( p, pObj, i )
+ Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
+ }
+ else
+ {
+ Saig_ManForEachLo( p, pObj, i )
+ Saig_ObjSetXsim( pObj, SAIG_XVS0 );
+ }
+ // simulate for the given number of timeframes
+ for ( f = 0; f < TSIM_MAX_ROUNDS; f++ )
+ {
+ // collect this state
+ pState = Saig_TsiStateNew( pTsi );
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ {
+ Value = Saig_ObjGetXsim(pObjLo);
+ if ( Value & 1 )
+ Aig_InfoSetBit( pState, 2 * i );
+ if ( Value & 2 )
+ Aig_InfoSetBit( pState, 2 * i + 1 );
+ }
+// printf( "%d ", Saig_TsiStateCount(pTsi, pState) );
+// Saig_TsiStatePrint( pTsi, pState );
+ // check if this state exists
+ if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
+ return pTsi;
+ // insert this state
+ Saig_TsiStateInsert( pTsi, pState, pTsi->nWords );
+ // simulate internal nodes
+ Aig_ManForEachNode( p, pObj, i )
+ Saig_ObjSetXsim( pObj, Saig_XsimAnd(Saig_ObjGetXsimFanin0(pObj), Saig_ObjGetXsimFanin1(pObj)) );
+ // transfer the latch values
+ Saig_ManForEachLi( p, pObj, i )
+ Saig_ObjSetXsim( pObj, Saig_ObjGetXsimFanin0(pObj) );
+ nCounter = 0;
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ {
+ if ( f < TSIM_ONE_SERIES )
+ Saig_ObjSetXsim( pObjLo, Saig_ObjGetXsim(pObjLi) );
+ else
+ {
+ if ( Saig_ObjGetXsim(pObjLi) != Saig_ObjGetXsim(pObjLo) )
+ Saig_ObjSetXsim( pObjLo, SAIG_XVSX );
+ }
+ nCounter += (Saig_ObjGetXsim(pObjLo) == SAIG_XVS0);
+ }
+ }
+ printf( "Saig_ManReachableTernary(): Did not reach a fixed point after %d iterations (not a bug).\n", TSIM_MAX_ROUNDS );
+ Saig_TsiStop( pTsi );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds the registers to phase-abstract.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
+{
+ int Values[256];
+ unsigned * pState;
+ int r, i, k, Reg, Value;
+ int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
+ assert( nFrames < 256 );
+ r = 0;
+ Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
+ {
+ for ( k = 0; k < nTests; k++ )
+ {
+ if ( k < pTsi->nPrefix + pTsi->nCycle )
+ pState = Vec_PtrEntry( pTsi->vStates, k );
+ else
+ pState = Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle );
+ Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
+ assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
+ if ( k < nFrames || (fIgnore && k == nFrames) )
+ Values[k % nFrames] = Value;
+ else if ( Values[k % nFrames] != Value )
+ break;
+ }
+ if ( k < nTests )
+ continue;
+ // skip stuck at
+ if ( fIgnore )
+ {
+ for ( k = 1; k < nFrames; k++ )
+ if ( Values[k] != Values[0] )
+ break;
+ if ( k == nFrames )
+ continue;
+ }
+ // report useful register
+ Vec_IntWriteEntry( pTsi->vNonXRegs, r++, Reg );
+ if ( fVerbose )
+ {
+ printf( "Register %5d has generator: [", Reg );
+ for ( k = 0; k < nFrames; k++ )
+ Saig_XsimPrint( stdout, Values[k] );
+ printf( "]\n" );
+ }
+ }
+ Vec_IntShrink( pTsi->vNonXRegs, r );
+ if ( fVerbose )
+ printf( "Found %3d useful registers.\n", Vec_IntSize(pTsi->vNonXRegs) );
+ return Vec_IntSize(pTsi->vNonXRegs);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Mapping of AIG nodes into frames nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Aig_Obj_t * Saig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
+static inline void Saig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Saig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Saig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction by unrolling the circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVerbose )
+{
+ Aig_Man_t * pFrames, * pAig = pTsi->pAig;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+ Aig_Obj_t ** pObjMap;
+ unsigned * pState;
+ int i, f, Reg, Value;
+
+ assert( Vec_IntSize(pTsi->vNonXRegs) > 0 );
+
+ // create mapping for the frames nodes
+ pObjMap = ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+ memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) );
+
+ // start the fraig package
+ pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+ pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+ // map constant nodes
+ for ( f = 0; f < nFrames; f++ )
+ Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+ // create PI nodes for the frames
+ for ( f = 0; f < nFrames; f++ )
+ Aig_ManForEachPiSeq( pAig, pObj, i )
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
+ // create the latches
+ Aig_ManForEachLoSeq( pAig, pObj, i )
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
+
+ // add timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // replace abstracted registers by constants
+ Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
+ {
+ pObj = Saig_ManLo( pAig, Reg );
+ pState = Vec_PtrEntry( pTsi->vStates, f );
+ Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
+ assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
+ pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+ }
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ pObjNew = Aig_And( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Saig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+ }
+ // set the latch inputs and copy them into the latch outputs of the next frame
+ Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Saig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+ if ( f < nFrames - 1 )
+ Saig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+ }
+ }
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Aig_ManForEachPoSeq( pAig, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+ }
+ }
+ pFrames->nRegs = pAig->nRegs;
+ pFrames->nTruePis = Aig_ManPiNum(pFrames) - Aig_ManRegNum(pFrames);
+ pFrames->nTruePos = Aig_ManPoNum(pFrames) - Aig_ManRegNum(pFrames);
+ Aig_ManForEachLiSeq( pAig, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) );
+ Saig_ObjSetFrames( pObjMap, nFrames, pObj, nFrames-1, pObjNew );
+ }
+//Aig_ManPrintStats( pFrames );
+ Aig_ManSeqCleanup( pFrames );
+//Aig_ManPrintStats( pFrames );
+ Aig_ManPiCleanup( pFrames );
+//Aig_ManPrintStats( pFrames );
+ free( pObjMap );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs automated phase abstraction.]
+
+ Description [Takes the AIG manager and the array of initial states.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose )
+{
+ Aig_Man_t * pNew = NULL;
+ Saig_Tsim_t * pTsi;
+ assert( Saig_ManRegNum(p) );
+ assert( Saig_ManPiNum(p) );
+ assert( Saig_ManPoNum(p) );
+ // perform terminary simulation
+ pTsi = Saig_ManReachableTernary( p, vInits );
+ if ( pTsi == NULL )
+ return NULL;
+ // derive information
+ pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+ pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
+ pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords);
+ // print statistics
+ if ( fVerbose )
+ {
+ printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n",
+ pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
+ if ( pTsi->nNonXRegs < 100 )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+ }
+ if ( fPrint )
+ printf( "Print-out finished. Phase assignment is not performed.\n" );
+ else if ( nFrames < 2 )
+ printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+ else if ( pTsi->nCycle == 0 )
+ printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
+ else if ( pTsi->nCycle % nFrames != 0 )
+ printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
+ else if ( pTsi->nNonXRegs == 0 )
+ printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
+ else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
+ printf( "There is no registers to abstract with %d frames.\n", nFrames );
+ else
+ pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
+ Saig_TsiStop( pTsi );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saig_.c b/src/aig/saig/saig_.c
new file mode 100644
index 00000000..255639e6
--- /dev/null
+++ b/src/aig/saig/saig_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [saig_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saig_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-17 23:17:20 +0000