mirror of https://github.com/YosysHQ/abc.git
Version abc80912
This commit is contained in:
Alan Mishchenko
parent
4db8655072
commit
75d6d6abd1
4
abc.dsp
4
abc.dsp
|
|
@ -3306,6 +3306,10 @@ SOURCE=.\src\aig\saig\saigScl.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\saig\saigSynch.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\saig\saigTrans.c
|
||||
# End Source File
|
||||
# End Group
|
||||
|
|
|
|||
4
abc.rc
4
abc.rc
|
|
@ -1,8 +1,8 @@
|
|||
# global parameters
|
||||
#set check # checks intermediate networks
|
||||
#set checkfio # prints warnings when fanins/fanouts are duplicated
|
||||
#set checkread # checks new networks after reading from file
|
||||
#set backup # saves backup networks retrived by "undo" and "recall"
|
||||
set checkread # checks new networks after reading from file
|
||||
set backup # saves backup networks retrived by "undo" and "recall"
|
||||
set savesteps 1 # sets the maximum number of backup networks to save
|
||||
set progressbar # display the progress bar
|
||||
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@
|
|||
#include "fra.h"
|
||||
#include "ioa.h"
|
||||
#include "int.h"
|
||||
#include "ssw.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -75,6 +76,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
|
|||
***********************************************************************/
|
||||
int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
|
||||
{
|
||||
Ssw_Pars_t Pars2, * pPars2 = &Pars2;
|
||||
Fra_Ssw_t Pars, * pPars = &Pars;
|
||||
Fra_Sml_t * pSml;
|
||||
Aig_Man_t * pNew, * pTemp;
|
||||
|
|
@ -89,6 +91,8 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
|
|||
if ( RetValue >= 0 )
|
||||
goto finish;
|
||||
|
||||
// prepare parameters
|
||||
Ssw_ManSetDefaultParams( pPars2 );
|
||||
// prepare parameters
|
||||
memset( pPars, 0, sizeof(Fra_Ssw_t) );
|
||||
pPars->fLatchCorr = fLatchCorr;
|
||||
|
|
@ -288,12 +292,17 @@ PRT( "Time", clock() - clk );
|
|||
goto finish;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
clk = clock();
|
||||
pPars->nFramesK = nFrames;
|
||||
pPars->TimeLimit = TimeLeft;
|
||||
pPars->fSilent = pParSec->fSilent;
|
||||
pNew = Fra_FraigInduction( pTemp = pNew, pPars );
|
||||
// pNew = Fra_FraigInduction( pTemp = pNew, pPars );
|
||||
|
||||
pPars2->nFramesK = nFrames;
|
||||
pPars2->nBTLimit = 1000 * nFrames;
|
||||
Aig_ManSetRegNum( pNew, pNew->nRegs );
|
||||
pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
|
||||
if ( pNew == NULL )
|
||||
{
|
||||
pNew = pTemp;
|
||||
|
|
@ -306,7 +315,7 @@ clk = clock();
|
|||
if ( pParSec->fVerbose )
|
||||
{
|
||||
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
|
||||
nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
|
||||
nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
if ( RetValue != -1 )
|
||||
|
|
|
|||
|
|
@ -89,6 +89,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
|
|||
extern int Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
|
||||
/*=== saigMiter.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
|
||||
extern Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p );
|
||||
/*=== saigPhase.c ==========================================================*/
|
||||
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
|
||||
/*=== saigRetFwd.c ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -48,6 +48,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
|
|||
assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) );
|
||||
assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) );
|
||||
pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
|
||||
pNew->pName = Aig_UtilStrsav( "miter" );
|
||||
// map constant nodes
|
||||
Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
|
||||
Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
|
||||
|
|
@ -88,6 +89,40 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
|
|||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates the AIG to have constant-0 initial state.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p )
|
||||
{
|
||||
Aig_Man_t * pNew;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
|
||||
pNew->pName = Aig_UtilStrsav( p->pName );
|
||||
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
|
||||
Saig_ManForEachPi( p, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pNew );
|
||||
Saig_ManForEachLo( p, pObj, i )
|
||||
pObj->pData = Aig_NotCond( Aig_ObjCreatePi( pNew ), pObj->fMarkA );
|
||||
Aig_ManForEachNode( p, pObj, i )
|
||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
Saig_ManForEachPo( p, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
Saig_ManForEachLi( p, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) );
|
||||
Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
|
||||
assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
|
|
|
|||
|
|
@ -0,0 +1,623 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [saigSynch.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Sequential AIG package.]
|
||||
|
||||
Synopsis [Computation of synchronizing sequence.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: saigSynch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "saig.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// 0 1 x
|
||||
// 00 01 11
|
||||
// 0 00 00 00 00
|
||||
// 1 01 00 01 11
|
||||
// x 11 00 11 11
|
||||
|
||||
static inline unsigned Saig_SynchNot( unsigned w )
|
||||
{
|
||||
return w^((~(w&(w>>1)))&0x55555555);
|
||||
}
|
||||
static inline unsigned Saig_SynchAnd( unsigned u, unsigned w )
|
||||
{
|
||||
return (u&w)|((((u&(u>>1)&w&~(w>>1))|(w&(w>>1)&u&~(u>>1)))&0x55555555)<<1);
|
||||
}
|
||||
static inline unsigned Saig_SynchRandomBinary()
|
||||
{
|
||||
return Aig_ManRandom(0) & 0x55555555;
|
||||
}
|
||||
static inline unsigned Saig_SynchRandomTernary()
|
||||
{
|
||||
unsigned w = Aig_ManRandom(0);
|
||||
return w^((~w)&(w>>1)&0x55555555);
|
||||
}
|
||||
static inline unsigned Saig_SynchTernary( int v )
|
||||
{
|
||||
assert( v == 0 || v == 1 || v == 3 );
|
||||
return v? ((v==1)? 0x55555555 : 0xffffffff) : 0;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Initializes registers to the ternary state.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchSetConstant1( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int w;
|
||||
pObj = Aig_ManConst1( pAig );
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = 0x55555555;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Initializes registers to the ternary state.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchInitRegsTernary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int i, w;
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = 0xffffffff;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Initializes registers to the given binary state.]
|
||||
|
||||
Description [The binary state is stored in pObj->fMarkA.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchInitRegsBinary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int i, w;
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchTernary( pObj->fMarkA );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Initializes random binary primary inputs.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchInitPisRandom( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int i, w;
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchRandomBinary();
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Initializes random binary primary inputs.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchInitPisGiven( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, char * pValues )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int i, w;
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchTernary( pValues[i] );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs ternary simulation of the nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchTernarySimulate( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim0, * pSim1, * pSim;
|
||||
int i, w;
|
||||
// simulate nodes
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
pSim0 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
|
||||
pSim1 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId1(pObj) );
|
||||
if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), Saig_SynchNot(pSim1[w]) );
|
||||
}
|
||||
else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchAnd( pSim0[w], Saig_SynchNot(pSim1[w]) );
|
||||
}
|
||||
else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), pSim1[w] );
|
||||
}
|
||||
else // if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchAnd( pSim0[w], pSim1[w] );
|
||||
}
|
||||
}
|
||||
// transfer values to register inputs
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
pSim0 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
|
||||
if ( Aig_ObjFaninC0(pObj) )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchNot( pSim0[w] );
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = pSim0[w];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs ternary simulation of the nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_SynchTernaryTransferState( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
|
||||
{
|
||||
Aig_Obj_t * pObjLi, * pObjLo;
|
||||
unsigned * pSim0, * pSim1;
|
||||
int i, w;
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
{
|
||||
pSim0 = Vec_PtrEntry( vSimInfo, pObjLi->Id );
|
||||
pSim1 = Vec_PtrEntry( vSimInfo, pObjLo->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim1[w] = pSim0[w];
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the number of Xs in the smallest ternary pattern.]
|
||||
|
||||
Description [Returns the number of this pattern.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * piPat )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int * pCounters, i, w, b;
|
||||
int iPatBest, iTernMin;
|
||||
// count the number of ternary values in each pattern
|
||||
pCounters = CALLOC( int, nWords * 16 );
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
for ( b = 0; b < 16; b++ )
|
||||
if ( ((pSim[w] >> (b << 1)) & 3) == 3 )
|
||||
pCounters[16 * w + b]++;
|
||||
}
|
||||
// get the best pattern
|
||||
iPatBest = -1;
|
||||
iTernMin = 1 + Saig_ManRegNum(pAig);
|
||||
for ( b = 0; b < 16 * nWords; b++ )
|
||||
if ( iTernMin > pCounters[b] )
|
||||
{
|
||||
iTernMin = pCounters[b];
|
||||
iPatBest = b;
|
||||
if ( iTernMin == 0 )
|
||||
break;
|
||||
}
|
||||
free( pCounters );
|
||||
*piPat = iPatBest;
|
||||
return iTernMin;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Saves the best pattern found and initializes the registers.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Saig_SynchSavePattern( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int iPat, Vec_Str_t * vSequence )
|
||||
{
|
||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||
unsigned * pSim;
|
||||
int Counter, Value, i, w;
|
||||
assert( iPat < 16 * nWords );
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
|
||||
Vec_StrPush( vSequence, (char)Value );
|
||||
// printf( "%d ", Value );
|
||||
}
|
||||
// printf( "\n" );
|
||||
Counter = 0;
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObjLi->Id );
|
||||
Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
|
||||
Counter += (Value == 3);
|
||||
// save patern in the same register
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObjLo->Id );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pSim[w] = Saig_SynchTernary( Value );
|
||||
}
|
||||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Implement synchronizing sequence.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Saig_SynchSequenceRun( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, Vec_Str_t * vSequence, int fTernary )
|
||||
{
|
||||
unsigned * pSim;
|
||||
Aig_Obj_t * pObj;
|
||||
int Counter, nIters, Value, i;
|
||||
assert( Vec_StrSize(vSequence) % Saig_ManPiNum(pAig) == 0 );
|
||||
nIters = Vec_StrSize(vSequence) / Saig_ManPiNum(pAig);
|
||||
Saig_SynchSetConstant1( pAig, vSimInfo, 1 );
|
||||
if ( fTernary )
|
||||
Saig_SynchInitRegsTernary( pAig, vSimInfo, 1 );
|
||||
else
|
||||
Saig_SynchInitRegsBinary( pAig, vSimInfo, 1 );
|
||||
for ( i = 0; i < nIters; i++ )
|
||||
{
|
||||
Saig_SynchInitPisGiven( pAig, vSimInfo, 1, Vec_StrArray(vSequence) + i * Saig_ManPiNum(pAig) );
|
||||
Saig_SynchTernarySimulate( pAig, vSimInfo, 1 );
|
||||
Saig_SynchTernaryTransferState( pAig, vSimInfo, 1 );
|
||||
}
|
||||
// save the resulting state in the registers
|
||||
Counter = 0;
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
{
|
||||
pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
|
||||
Value = pSim[0] & 3;
|
||||
assert( Value != 2 );
|
||||
Counter += (Value == 3);
|
||||
pObj->fMarkA = Value;
|
||||
}
|
||||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Determines synchronizing sequence using ternary simulation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Str_t * Saig_SynchSequence( Aig_Man_t * pAig, int nWords )
|
||||
{
|
||||
int nStepsMax = 100; // the maximum number of simulation steps
|
||||
int nTriesMax = 100; // the maximum number of attempts at each step
|
||||
int fVerify = 1; // verify the resulting pattern
|
||||
Vec_Str_t * vSequence;
|
||||
Vec_Ptr_t * vSimInfo;
|
||||
int nTerPrev, nTerCur, nTerCur2;
|
||||
int iPatBest, RetValue, s, t;
|
||||
assert( Saig_ManRegNum(pAig) > 0 );
|
||||
// reset random numbers
|
||||
Aig_ManRandom( 1 );
|
||||
// start the sequence
|
||||
vSequence = Vec_StrAlloc( 20 * Saig_ManRegNum(pAig) );
|
||||
// create sim info and init registers
|
||||
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
|
||||
Saig_SynchSetConstant1( pAig, vSimInfo, nWords );
|
||||
// iterate over the timeframes
|
||||
nTerPrev = Saig_ManRegNum(pAig);
|
||||
Saig_SynchInitRegsTernary( pAig, vSimInfo, nWords );
|
||||
for ( s = 0; s < nStepsMax && nTerPrev > 0; s++ )
|
||||
{
|
||||
for ( t = 0; t < nTriesMax; t++ )
|
||||
{
|
||||
Saig_SynchInitPisRandom( pAig, vSimInfo, nWords );
|
||||
Saig_SynchTernarySimulate( pAig, vSimInfo, nWords );
|
||||
nTerCur = Saig_SynchCountX( pAig, vSimInfo, nWords, &iPatBest );
|
||||
if ( nTerCur < nTerPrev )
|
||||
break;
|
||||
}
|
||||
if ( t == nTriesMax )
|
||||
break;
|
||||
nTerCur2 = Saig_SynchSavePattern( pAig, vSimInfo, nWords, iPatBest, vSequence );
|
||||
assert( nTerCur == nTerCur2 );
|
||||
nTerPrev = nTerCur;
|
||||
}
|
||||
if ( nTerPrev > 0 )
|
||||
{
|
||||
printf( "Count not initialize %d registers.\n", nTerPrev );
|
||||
Vec_PtrFree( vSimInfo );
|
||||
Vec_StrFree( vSequence );
|
||||
return NULL;
|
||||
}
|
||||
// verify that the sequence is correct
|
||||
if ( fVerify )
|
||||
{
|
||||
RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
|
||||
assert( RetValue == 0 );
|
||||
Aig_ManCleanMarkA( pAig );
|
||||
}
|
||||
Vec_PtrFree( vSimInfo );
|
||||
return vSequence;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Determines synchronizing sequence using ternary simulation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pAigZero;
|
||||
Vec_Str_t * vSequence;
|
||||
Vec_Ptr_t * vSimInfo;
|
||||
int RetValue, clk;
|
||||
|
||||
clk = clock();
|
||||
// derive synchronization sequence
|
||||
vSequence = Saig_SynchSequence( pAig, nWords );
|
||||
if ( vSequence == NULL )
|
||||
printf( "Design 1: Synchronizing sequence is not found. " );
|
||||
else if ( fVerbose )
|
||||
printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) );
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
else
|
||||
printf( "\n" );
|
||||
if ( vSequence == NULL )
|
||||
{
|
||||
printf( "Quitting synchronization.\n" );
|
||||
return NULL;
|
||||
}
|
||||
|
||||
// apply synchronization sequence
|
||||
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), 1 );
|
||||
RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
|
||||
assert( RetValue == 0 );
|
||||
// duplicate
|
||||
pAigZero = Saig_ManDupInitZero( pAig );
|
||||
// cleanup
|
||||
Vec_PtrFree( vSimInfo );
|
||||
Vec_StrFree( vSequence );
|
||||
Aig_ManCleanMarkA( pAig );
|
||||
return pAigZero;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates SEC miter for two designs without initial state.]
|
||||
|
||||
Description [The designs (pAig1 and pAig2) are assumed to have ternary
|
||||
initial state. Determines synchronizing sequences using ternary simulation.
|
||||
Simulates the sequences on both designs to come up with equivalent binary
|
||||
initial states. Create seq miter for the designs starting in these states.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pAig1z, * pAig2z, * pMiter;
|
||||
Vec_Str_t * vSeq1, * vSeq2;
|
||||
Vec_Ptr_t * vSimInfo;
|
||||
int RetValue, clk;
|
||||
/*
|
||||
{
|
||||
unsigned u = Saig_SynchRandomTernary();
|
||||
unsigned w = Saig_SynchRandomTernary();
|
||||
unsigned x = Saig_SynchNot( u );
|
||||
unsigned y = Saig_SynchNot( w );
|
||||
unsigned z = Saig_SynchAnd( x, y );
|
||||
|
||||
Extra_PrintBinary( stdout, &u, 32 ); printf( "\n" );
|
||||
Extra_PrintBinary( stdout, &w, 32 ); printf( "\n" ); printf( "\n" );
|
||||
Extra_PrintBinary( stdout, &x, 32 ); printf( "\n" );
|
||||
Extra_PrintBinary( stdout, &y, 32 ); printf( "\n" ); printf( "\n" );
|
||||
Extra_PrintBinary( stdout, &z, 32 ); printf( "\n" );
|
||||
}
|
||||
*/
|
||||
// report statistics
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Design 1: " );
|
||||
Aig_ManPrintStats( pAig1 );
|
||||
printf( "Design 2: " );
|
||||
Aig_ManPrintStats( pAig2 );
|
||||
}
|
||||
|
||||
// synchronize the first design
|
||||
clk = clock();
|
||||
vSeq1 = Saig_SynchSequence( pAig1, nWords );
|
||||
if ( vSeq1 == NULL )
|
||||
printf( "Design 1: Synchronizing sequence is not found. " );
|
||||
else if ( fVerbose )
|
||||
printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) );
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
else
|
||||
printf( "\n" );
|
||||
|
||||
// synchronize the first design
|
||||
clk = clock();
|
||||
vSeq2 = Saig_SynchSequence( pAig2, nWords );
|
||||
if ( vSeq2 == NULL )
|
||||
printf( "Design 2: Synchronizing sequence is not found. " );
|
||||
else if ( fVerbose )
|
||||
printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) );
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
else
|
||||
printf( "\n" );
|
||||
|
||||
// quit if one of the designs cannot be synchronized
|
||||
if ( vSeq1 == NULL || vSeq2 == NULL )
|
||||
{
|
||||
printf( "Quitting synchronization.\n" );
|
||||
if ( vSeq1 ) Vec_StrFree( vSeq1 );
|
||||
if ( vSeq2 ) Vec_StrFree( vSeq2 );
|
||||
return NULL;
|
||||
}
|
||||
clk = clock();
|
||||
vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
|
||||
|
||||
// process Design 1
|
||||
RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );
|
||||
assert( RetValue == 0 );
|
||||
RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq2, 0 );
|
||||
assert( RetValue == 0 );
|
||||
|
||||
// process Design 2
|
||||
RetValue = Saig_SynchSequenceRun( pAig2, vSimInfo, vSeq2, 1 );
|
||||
assert( RetValue == 0 );
|
||||
|
||||
// duplicate designs
|
||||
pAig1z = Saig_ManDupInitZero( pAig1 );
|
||||
pAig2z = Saig_ManDupInitZero( pAig2 );
|
||||
pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
|
||||
Aig_ManStop( pAig1z );
|
||||
Aig_ManStop( pAig2z );
|
||||
|
||||
// cleanup
|
||||
Vec_PtrFree( vSimInfo );
|
||||
Vec_StrFree( vSeq1 );
|
||||
Vec_StrFree( vSeq2 );
|
||||
Aig_ManCleanMarkA( pAig1 );
|
||||
Aig_ManCleanMarkA( pAig2 );
|
||||
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Miter of the synchronized designs is constructed. " );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
return pMiter;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -139,8 +139,9 @@ clk = clock();
|
|||
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
|
||||
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
|
||||
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
|
||||
printf( "Use = %5d. Skip = %5d. ",
|
||||
p->nRefUse, p->nRefSkip );
|
||||
if ( p->pPars->fSkipCheck )
|
||||
printf( "Use = %5d. Skip = %5d. ",
|
||||
p->nRefUse, p->nRefSkip );
|
||||
PRT( "T", clock() - clk );
|
||||
}
|
||||
Ssw_ManCleanup( p );
|
||||
|
|
|
|||
|
|
@ -47,14 +47,14 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
|
|||
Aig_ManFanoutStart( pAig );
|
||||
Aig_ManSetPioNumbers( pAig );
|
||||
// create interpolation manager
|
||||
p = ALLOC( Ssw_Man_t, 1 );
|
||||
p = ALLOC( Ssw_Man_t, 1 );
|
||||
memset( p, 0, sizeof(Ssw_Man_t) );
|
||||
p->pPars = pPars;
|
||||
p->pAig = pAig;
|
||||
p->nFrames = pPars->nFramesK + 1;
|
||||
p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
// SAT solving
|
||||
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
|
||||
p->vFanins = Vec_PtrAlloc( 100 );
|
||||
p->vSimRoots = Vec_PtrAlloc( 1000 );
|
||||
p->vSimClasses = Vec_PtrAlloc( 1000 );
|
||||
|
|
@ -99,8 +99,8 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
|
|||
{
|
||||
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
|
||||
|
||||
printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
|
||||
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
|
||||
printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
|
||||
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
|
||||
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
|
||||
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
|
||||
p->nSatVarsTotal/p->pPars->nIters );
|
||||
|
|
@ -149,7 +149,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
|
|||
p->nSatVarsTotal += p->pSat->size;
|
||||
sat_solver_delete( p->pSat );
|
||||
p->pSat = NULL;
|
||||
memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
|
||||
memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
|
||||
}
|
||||
p->nConstrTotal = 0;
|
||||
p->nConstrReduced = 0;
|
||||
|
|
|
|||
|
|
@ -234,7 +234,6 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
|
|||
// set the PI simulation information
|
||||
Aig_ManConst1(p->pAig)->fMarkB = 1;
|
||||
Aig_ManForEachPi( p->pAig, pObj, i )
|
||||
// pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
|
||||
pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
|
||||
// simulate internal nodes
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
|
|
@ -244,10 +243,18 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
|
|||
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
|
||||
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
|
||||
// make sure refinement happened
|
||||
if ( Aig_ObjIsConst1(pRepr) )
|
||||
if ( Aig_ObjIsConst1(pRepr) )
|
||||
{
|
||||
assert( RetValue1 );
|
||||
if ( RetValue1 == 0 )
|
||||
printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( RetValue2 );
|
||||
if ( RetValue2 == 0 )
|
||||
printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" );
|
||||
}
|
||||
p->timeSimSat += clock() - clk;
|
||||
}
|
||||
|
||||
|
|
@ -266,8 +273,6 @@ p->timeSimSat += clock() - clk;
|
|||
void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
|
||||
{
|
||||
int RetValue1, RetValue2, clk = clock();
|
||||
// save the counter-example
|
||||
// Ssw_SmlSavePatternAig( p, f );
|
||||
// set the PI simulation information
|
||||
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
|
||||
// simulate internal nodes
|
||||
|
|
@ -277,9 +282,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
|
|||
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
|
||||
// make sure refinement happened
|
||||
if ( Aig_ObjIsConst1(pRepr) )
|
||||
{
|
||||
assert( RetValue1 );
|
||||
if ( RetValue1 == 0 )
|
||||
printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( RetValue2 );
|
||||
if ( RetValue2 == 0 )
|
||||
printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" );
|
||||
}
|
||||
p->timeSimSat += clock() - clk;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -222,6 +222,7 @@ clk = clock();
|
|||
p->fRefined = 0;
|
||||
if ( p->pPars->fVerbose )
|
||||
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
|
||||
Ssw_ManStartSolver( p );
|
||||
for ( f = 0; f < p->pPars->nFramesK; f++ )
|
||||
{
|
||||
// map constants and PIs
|
||||
|
|
@ -241,8 +242,13 @@ clk = clock();
|
|||
if ( f == p->pPars->nFramesK - 1 )
|
||||
break;
|
||||
// transfer latch input to the latch outputs
|
||||
// build logic cones for register outputs
|
||||
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
|
||||
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
|
||||
{
|
||||
pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
|
||||
Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew );
|
||||
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
|
||||
}
|
||||
}
|
||||
if ( p->pPars->fVerbose )
|
||||
Bar_ProgressStop( pProgress );
|
||||
|
|
|
|||
|
|
@ -199,6 +199,7 @@ static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** arg
|
|||
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_CommandSynch ( 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 );
|
||||
|
|
@ -463,6 +464,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
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, "Sequential", "synch", Abc_CommandSynch, 1 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
|
||||
|
|
@ -4862,7 +4864,6 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
|
||||
return 1;
|
||||
|
||||
// compute the miter
|
||||
pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic, fMulti );
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
|
|
@ -14424,6 +14425,121 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandSynch( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
FILE * pOut, * pErr;
|
||||
Abc_Ntk_t * pNtkRes, * pNtk1, * pNtk2, * pNtk;
|
||||
char ** pArgvNew;
|
||||
int nArgcNew;
|
||||
int fDelete1, fDelete2;
|
||||
int c;
|
||||
int nWords;
|
||||
int fVerbose;
|
||||
|
||||
extern Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose );
|
||||
extern Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
nWords = 32;
|
||||
fVerbose = 1;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'W':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nWords = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nWords <= 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
|
||||
pArgvNew = argv + globalUtilOptind;
|
||||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( nArgcNew == 0 )
|
||||
{
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pErr, "Empty network.\n" );
|
||||
return 1;
|
||||
}
|
||||
pNtkRes = Abc_NtkDarSynchOne( pNtk, nWords, fVerbose );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
|
||||
return 1;
|
||||
if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
|
||||
{
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
|
||||
printf( "The network has no latches..\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
// modify the current network
|
||||
pNtkRes = Abc_NtkDarSynch( pNtk1, pNtk2, nWords, fVerbose );
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
|
||||
}
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Synchronization has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: synch [-W <num>] [-vh] <file1> <file2>\n" );
|
||||
fprintf( pErr, "\t derives and applies synchronization sequence\n" );
|
||||
fprintf( pErr, "\t-W num : the number of simulation words [default = %d]\n", nWords );
|
||||
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
fprintf( pErr, "\tfile1 : (optional) the file with the first design\n");
|
||||
fprintf( pErr, "\tfile2 : (optional) the file with the second design\n\n");
|
||||
fprintf( pErr, "\t If no designs are given on the command line,\n" );
|
||||
fprintf( pErr, "\t assumes the current network has no initial state,\n" );
|
||||
fprintf( pErr, "\t derives synchronization sequence and applies it.\n\n" );
|
||||
fprintf( pErr, "\t If two designs are given on the command line\n" );
|
||||
fprintf( pErr, "\t assumes both of them have no initial state,\n" );
|
||||
fprintf( pErr, "\t derives sequences for both designs, synchorinizes\n" );
|
||||
fprintf( pErr, "\t them, and creates SEC miter comparing two designs.\n\n" );
|
||||
fprintf( pErr, "\t If only one design is given on the command line,\n" );
|
||||
fprintf( pErr, "\t considers the second design to be the current network,\n" );
|
||||
fprintf( pErr, "\t and derives SEC miter for them, as described above.\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -14842,6 +14958,8 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
|
||||
if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
|
||||
{
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
|
||||
printf( "The network has no latches. Used combinational command \"cec\".\n" );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -14960,9 +15078,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
|
||||
return 1;
|
||||
|
||||
if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
|
||||
{
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
|
||||
printf( "The network has no latches. Used combinational command \"cec\".\n" );
|
||||
return 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2184,6 +2184,71 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
|
|||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs phase abstraction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
|
||||
{
|
||||
extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
pMan = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
|
||||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs phase abstraction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose )
|
||||
{
|
||||
extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose );
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pMan1, * pMan2, * pMan;
|
||||
pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
|
||||
if ( pMan1 == NULL )
|
||||
return NULL;
|
||||
pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
|
||||
if ( pMan2 == NULL )
|
||||
{
|
||||
Aig_ManStop( pMan1 );
|
||||
return NULL;
|
||||
}
|
||||
pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose );
|
||||
Aig_ManStop( pMan1 );
|
||||
Aig_ManStop( pMan2 );
|
||||
if ( pMan == NULL )
|
||||
return NULL;
|
||||
pNtkAig = Abc_NtkFromAigPhase( pMan );
|
||||
pNtkAig->pName = Extra_UtilStrsav("miter");
|
||||
pNtkAig->pSpec = NULL;
|
||||
Aig_ManStop( pMan );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs phase abstraction.]
|
||||
|
|
|
|||
|
|
@ -146,7 +146,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
|
|||
// start the file reader
|
||||
p = Io_MvAlloc();
|
||||
p->fBlifMv = fBlifMv;
|
||||
p->fUseReset = 0;
|
||||
p->fUseReset = 1;
|
||||
p->pFileName = pFileName;
|
||||
p->pBuffer = Io_MvLoadFile( pFileName );
|
||||
if ( p->pBuffer == NULL )
|
||||
|
|
@ -704,7 +704,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
|
|||
int i, k;
|
||||
// iterate through the models
|
||||
Vec_PtrForEachEntry( p->vModels, pMod, i )
|
||||
{
|
||||
{
|
||||
// check if there any MV lines
|
||||
if ( Vec_PtrSize(pMod->vMvs) > 0 )
|
||||
Abc_NtkStartMvVars( pMod->pNtk );
|
||||
|
|
|
|||
|
|
@ -362,6 +362,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
|
|||
|
||||
default:
|
||||
// scan the next name
|
||||
/*
|
||||
fFound = 0;
|
||||
for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n'; i++ )
|
||||
{
|
||||
|
|
@ -375,13 +376,31 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
|
|||
if ( fFound )
|
||||
break;
|
||||
}
|
||||
*/
|
||||
// bug fix by SV (9/11/08)
|
||||
fFound = 0;
|
||||
for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
|
||||
pTemp[i] != PARSE_SYM_AND1 && pTemp[i] != PARSE_SYM_AND2 && pTemp[i] != PARSE_SYM_XOR1 &&
|
||||
pTemp[i] != PARSE_SYM_XOR2 && pTemp[i] != PARSE_SYM_XOR3 && pTemp[i] != PARSE_SYM_XOR &&
|
||||
pTemp[i] != PARSE_SYM_OR1 && pTemp[i] != PARSE_SYM_OR2 && pTemp[i] != PARSE_SYM_CLOSE;
|
||||
i++ )
|
||||
{}
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
{
|
||||
if ( strncmp( pTemp, ppVarNames[v], i ) == 0 && strlen(ppVarNames[v]) == (unsigned)(i) )
|
||||
{
|
||||
pTemp += i-1;
|
||||
fFound = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if ( !fFound )
|
||||
{
|
||||
fprintf( pOutput, "Parse_FormulaParser(): The parser cannot find var \"%s\" in the input var list.\n", pTemp );
|
||||
Flag = PARSE_FLAG_ERROR;
|
||||
break;
|
||||
}
|
||||
|
||||
// assume operation AND, if vars follow one another
|
||||
if ( Flag == PARSE_FLAG_VAR )
|
||||
Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
|
||||
|
|
|
|||
Loading…
Reference in New Issue