Skip to content

A
abc
Commit b51685d6 by Alan Mishchenko
Options

Version abc80416

parent 45827110
Showing with 1182 additions and 22 deletions
abc.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
......@@ -3229,6 +3229,18 @@ SOURCE=.\src\aig\mfx\mfxStrash.c
SOURCE=.\src\aig\mfx\mfxWin.c
# End Source File
# End Group
# Begin Group "saig"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\saig\saig.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# End Group
# End Group
# End Group
# Begin Group "Header Files"
......
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 );
......
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 []
......
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 );
}
......
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
......
src/aig/saig/saig.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigPhase.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saig_.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
......@@ -184,6 +184,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -431,6 +432,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
......@@ -4944,7 +4946,7 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkLatchNum(pNtk2) )
{
fprintf( pErr, "The second network has latches. Appending does not work for such networks.\n" );
return 1;
return 0;
}
// get the new network
......@@ -12683,7 +12685,7 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
return 1;
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
......@@ -12774,8 +12776,8 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
// modify the current network
pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fVerbose );
......@@ -12865,8 +12867,8 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
if ( Abc_NtkIsStrash(pNtk) )
......@@ -12960,8 +12962,8 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
return 0;
......@@ -13056,8 +13058,8 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
FREE( pNtk->pSeqModel );
......@@ -13074,6 +13076,111 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nFrames;
int fIgnore;
int fPrint;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 0;
fIgnore = 0;
fPrint = 0;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fipvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'i':
fIgnore ^= 1;
break;
case 'p':
fPrint ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for structrally hashed networks.\n" );
return 1;
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
if ( fPrint )
{
Abc_NtkPhaseAbstract( pNtk, 0, fIgnore, 1, fVerbose );
return 0;
}
// modify the current network
pNtkRes = Abc_NtkPhaseAbstract( pNtk, nFrames, fIgnore, 0, fVerbose );
if ( pNtkRes == NULL )
{
// fprintf( pErr, "Phase abstraction has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: phase [-F <num>] [-ipvh]\n" );
fprintf( pErr, "\t performs sequential cleanup of the current network\n" );
fprintf( pErr, "\t by removing nodes and latches that do not feed into POs\n" );
fprintf( pErr, "\t-F num : the number of frames to abstract [default = %d]\n", nFrames );
fprintf( pErr, "\t-i : toggle ignoring the initial state [default = %s]\n", fIgnore? "yes": "no" );
fprintf( pErr, "\t-p : toggle printing statistics about generators [default = %s]\n", fPrint? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
......@@ -14474,8 +14581,8 @@ int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
......@@ -14568,8 +14675,8 @@ int Abc_CommandEnlarge( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
......
src/base/abci/abcDar.c
......@@ -326,6 +326,77 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Synopsis [Converts the network from the AIG manager into ABC.]
Description [This procedure should be called after seq sweeping,
which changes the number of registers.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i;
assert( pMan->nAsserts == 0 );
// perform strashing
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
// create PIs
Aig_ManForEachPiSeq( pMan, pObj, i )
{
pObjNew = Abc_NtkCreatePi( pNtkNew );
Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
pObj->pData = pObjNew;
}
// create POs
Aig_ManForEachPoSeq( pMan, pObj, i )
{
pObjNew = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
pObj->pData = pObjNew;
}
assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
// create as many latches as there are registers in the manager
Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
{
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
Abc_ObjAddFanin( pObjNew, pObjLi->pData );
Abc_ObjAddFanin( pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjLi->pData), NULL );
Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjLo->pData), NULL );
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan, 1 );
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
{
pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
}
// check the resulting AIG
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
......@@ -463,8 +534,14 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
assert( Abc_LatchIsInit1(pLatch) == 0 );
Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
if ( Abc_LatchIsInit0(pLatch) )
Vec_IntPush( vInits, 0 );
else if ( Abc_LatchIsInit1(pLatch) )
Vec_IntPush( vInits, 1 );
else if ( Abc_LatchIsInitDc(pLatch) )
Vec_IntPush( vInits, 2 );
else
assert( 0 );
}
return vInits;
}
......@@ -1721,6 +1798,42 @@ Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose
}
/**Function*************************************************************
Synopsis [Performs phase abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose )
{
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
Vec_Int_t * vInits;
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
if ( pMan == NULL )
return NULL;
vInits = Abc_NtkGetLatchValues(pNtk);
pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, fIgnore, fPrint, fVerbose );
Vec_IntFree( vInits );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment