Skip to content

A
abc
Commit d62ee0a9 by Alan Mishchenko
Options

Version abc70911

parent e8cf8415
Showing with 519 additions and 47 deletions
abc.dsp
......@@ -2930,6 +2930,10 @@ SOURCE=.\src\aig\aig\aigTable.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigTime.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigTiming.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -50,6 +50,7 @@ typedef struct Aig_Obj_t_ Aig_Obj_t;
typedef struct Aig_MmFixed_t_ Aig_MmFixed_t;
typedef struct Aig_MmFlex_t_ Aig_MmFlex_t;
typedef struct Aig_MmStep_t_ Aig_MmStep_t;
typedef struct Aig_TMan_t_ Aig_TMan_t;
// object types
typedef enum {
......@@ -131,6 +132,7 @@ struct Aig_Man_t_
Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes
void (*pImpFunc) (void*, void*); // implication checking precedure
void * pImpData; // implication checking data
Aig_TMan_t * pManTime; // the timing manager
// timing statistics
int time1;
int time2;
......@@ -520,6 +522,19 @@ extern char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
extern void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
extern int Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
/*=== aigTime.c ===========================================================*/
extern Aig_TMan_t * Aig_TManStart( int nPis, int nPos );
extern void Aig_TManStop( Aig_TMan_t * p );
extern void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
extern void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
extern void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
extern void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
extern void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
extern void Aig_TManIncrementTravId( Aig_TMan_t * p );
extern float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
extern float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
#ifdef __cplusplus
}
#endif
......
src/aig/aig/aigMan.c
......@@ -229,6 +229,9 @@ void Aig_ManStop( Aig_Man_t * p )
// print time
if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); }
// delete timing
if ( p->pManTime )
Aig_TManStop( p->pManTime );
// delete fanout
if ( p->pFanData )
Aig_ManFanoutStop( p );
......@@ -304,6 +307,8 @@ void Aig_ManPrintStats( Aig_Man_t * p )
// printf( "Lev = %3d. ", Aig_ManCountLevels(p) );
printf( "Max = %7d. ", Aig_ManObjNumMax(p) );
printf( "Lev = %3d. ", Aig_ManLevels(p) );
if ( Aig_ManRegNum(p) )
printf( "Lat = %5d. ", Aig_ManRegNum(p) );
printf( "\n" );
}
......
src/aig/aig/aigScl.c
......@@ -157,12 +157,21 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Aig_ManForEachPi( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCis, pObj );
else
{
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
// Aig_ManRecycleMemory( p, pObj );
}
vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCos, pObj );
else
{
Aig_ObjDisconnect( p, pObj );
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
// Aig_ManRecycleMemory( p, pObj );
}
// remember the number of true PIs/POs
nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
......
src/aig/aig/aigTime.c 0 → 100644
/**CFile****************************************************************
FileName [aigTime.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Representation of timing information.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigTime.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_TBox_t_ Aig_TBox_t;
typedef struct Aig_TObj_t_ Aig_TObj_t;
// timing manager
struct Aig_TMan_t_
{
Vec_Ptr_t * vBoxes; // the timing boxes
Aig_MmFlex_t * pMemObj; // memory manager for boxes
int nTravIds; // traversal ID of the manager
int nPis; // the number of PIs
int nPos; // the number of POs
Aig_TObj_t * pPis; // timing info for the PIs
Aig_TObj_t * pPos; // timing info for the POs
};
// timing box
struct Aig_TBox_t_
{
int iBox; // the unique ID of this box
int TravId; // traversal ID of this box
int nInputs; // the number of box inputs
int nOutputs; // the number of box outputs
int Inouts[0]; // the int numbers of PIs and POs
};
// timing object
struct Aig_TObj_t_
{
int iObj2Box; // mapping of the object into its box
float timeOffset; // the static timing of the node
float timeActual; // the actual timing of the node
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the network manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
{
Aig_TMan_t * p;
int i;
p = ALLOC( Aig_TMan_t, 1 );
memset( p, 0, sizeof(Aig_TMan_t) );
p->pMemObj = Aig_MmFlexStart();
p->vBoxes = Vec_PtrAlloc( 100 );
Vec_PtrPush( p->vBoxes, NULL );
p->nPis = nPis;
p->nPos = nPos;
p->pPis = ALLOC( Aig_TObj_t, nPis );
memset( p->pPis, 0, sizeof(Aig_TObj_t) * nPis );
p->pPos = ALLOC( Aig_TObj_t, nPos );
memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
for ( i = 0; i < nPis; i++ )
p->pPis[i].iObj2Box = -1;
for ( i = 0; i < nPos; i++ )
p->pPos[i].iObj2Box = -1;
return p;
}
/**Function*************************************************************
Synopsis [Stops the network manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManStop( Aig_TMan_t * p )
{
Vec_PtrFree( p->vBoxes );
Aig_MmFlexStop( p->pMemObj, 0 );
free( p->pPis );
free( p->pPos );
free( p );
}
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes )
{
Aig_TBox_t * pBox;
int i;
pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) );
memset( pBox, 0, sizeof(Aig_TBox_t) );
pBox->iBox = Vec_PtrSize( p->vBoxes );
Vec_PtrPush( p->vBoxes, pBox );
pBox->nInputs = nPis;
pBox->nOutputs = nPos;
for ( i = 0; i < nPis; i++ )
{
assert( pPis[i] < p->nPis );
pBox->Inouts[i] = pPis[i];
Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] );
p->pPis[pPis[i]].iObj2Box = pBox->iBox;
}
for ( i = 0; i < nPos; i++ )
{
assert( pPos[i] < p->nPos );
pBox->Inouts[nPis+i] = pPos[i];
Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] );
p->pPos[pPos[i]].iObj2Box = pBox->iBox;
}
}
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
{
assert( iPi < p->nPis );
p->pPis[iPi].timeActual = Delay;
}
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
{
assert( iPo < p->nPos );
p->pPos[iPo].timeActual = Delay;
}
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
{
assert( iPi < p->nPis );
p->pPis[iPi].timeOffset = Delay;
}
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
{
assert( iPo < p->nPos );
p->pPos[iPo].timeOffset = Delay;
}
/**Function*************************************************************
Synopsis [Increments the trav ID of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TManIncrementTravId( Aig_TMan_t * p )
{
p->nTravIds++;
}
/**Function*************************************************************
Synopsis [Returns PI arrival time.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
{
Aig_TBox_t * pBox;
Aig_TObj_t * pObj;
float DelayMax;
int i;
assert( iPi < p->nPis );
if ( p->pPis[iPi].iObj2Box < 0 )
return p->pPis[iPi].timeOffset;
pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
// check if box timing is updated
if ( pBox->TravId == p->nTravIds )
return p->pPis[iPi].timeOffset;
pBox->TravId = p->nTravIds;
// update box timing
DelayMax = -1.0e+20F;
for ( i = 0; i < pBox->nOutputs; i++ )
{
pObj = p->pPos + pBox->Inouts[pBox->nInputs+i];
DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset );
}
for ( i = 0; i < pBox->nInputs; i++ )
{
pObj = p->pPis + pBox->Inouts[i];
pObj->timeActual = DelayMax + pObj->timeOffset;
}
return p->pPis[iPi].timeActual;
}
/**Function*************************************************************
Synopsis [Returns PO required time.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo )
{
return 0.0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/fra/fra.h
......@@ -111,6 +111,7 @@ struct Fra_Sml_t_
int nWordsFrame; // the number of words in each time frame
int nWordsTotal; // the total number of words at a node
int nWordsPref; // the number of word in the prefix
int fNonConstOut; // have seen a non-const-0 output during simulation
int nSimRounds; // statistics
int timeSim; // statistics
unsigned pData[0]; // simulation data for the nodes
......@@ -256,7 +257,7 @@ extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pN
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
......
src/aig/fra/fraBmc.c
......@@ -128,7 +128,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
{
if ( Imp == 0 )
continue;
Left = Fra_ImpLeft(Imp);
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
// get the corresponding nodes
pLeft = Aig_ManObj( pBmc->pAig, Left );
......@@ -136,7 +136,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
// iterate through the timeframes
for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
{
// get timeframes nodes
// get timeframe nodes
pLeftT = Bmc_ObjFrames( pLeft, f );
pRightT = Bmc_ObjFrames( pRight, f );
// get the corresponding FRAIG nodes
......@@ -148,14 +148,21 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
if ( fComplL != fComplR )
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
if ( fComplL == fComplR ) // x => x - always true
continue;
assert( fComplL != fComplR );
// consider 4 possibilities:
// NOT(1) => 1 or 0 => 1 - always true
// 1 => NOT(1) or 1 => 0 - never true
// NOT(x) => x or x - not always true
// x => NOT(x) or NOT(x) - not always true
if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
continue;
// disproved implication
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
break;
}
// check the implication
// - if true, a clause is added
// - if false, a cex is simulated
// make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
{
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
......@@ -320,7 +327,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
if ( p->pCla->vImps )
printf( "Imp = %5d. ", nImpsOld );
printf( "\n" );
}
......@@ -338,7 +345,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
if ( p->pCla->vImps )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
......
src/aig/fra/fraImp.c
......@@ -96,7 +96,7 @@ static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
Synopsis [Counts the number of 1s in the reverse implication.]
Synopsis [Counts the number of 1s in the complement of the implication.]
Description []
......@@ -118,7 +118,7 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
Synopsis [Counts the number of 1s in the reverse implication.]
Synopsis [Computes the complement of the implication.]
Description []
......@@ -495,7 +495,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
{
Aig_Obj_t * pLeft, * pRight;
Aig_Obj_t * pLeftF, * pRightF;
int i, Imp, Left, Right, Max;
int i, Imp, Left, Right, Max, RetValue;
int fComplL, fComplR;
Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
{
......@@ -519,18 +519,31 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
if ( fComplL != fComplR )
Vec_IntWriteEntry( vImps, i, 0 );
if ( fComplL == fComplR ) // x => x - always true
continue;
assert( fComplL != fComplR );
// consider 4 possibilities:
// NOT(1) => 1 or 0 => 1 - always true
// 1 => NOT(1) or 1 => 0 - never true
// NOT(x) => x or x - not always true
// x => NOT(x) or NOT(x) - not always true
if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
continue;
// disproved implication
p->pCla->fRefinement = 1;
Vec_IntWriteEntry( vImps, i, 0 );
continue;
}
// check the implication
// - if true, a clause is added
// - if false, a cex is simulated
// make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
if ( RetValue != 1 )
{
p->pCla->fRefinement = 1;
Fra_SmlResimulate( p );
if ( RetValue == 0 )
Fra_SmlResimulate( p );
if ( Vec_IntEntry(vImps, i) != 0 )
printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
assert( Vec_IntEntry(vImps, i) == 0 );
......@@ -642,14 +655,15 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
***********************************************************************/
int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
{
int nSimWords = 2000;
int nFrames = 2000;
int nSimWords = 8;
Fra_Sml_t * pSeq;
char * pfFails;
int Left, Right, Imp, i, Counter;
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return 0;
// simulate the AIG manager with combinational patterns
pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
// go through the implications and check how many of them do not hold
pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
......@@ -664,6 +678,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
Counter += pfFails[i];
free( pfFails );
Fra_SmlStop( pSeq );
return Counter;
}
......
src/aig/fra/fraInd.c
......@@ -257,7 +257,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew;
int nNodesBeg, nRegsBeg, Temp;
int nNodesBeg, nRegsBeg;
int nIter, i, clk = clock(), clk2;
if ( Aig_ManNodeNum(pManAig) == 0 )
......@@ -424,17 +424,18 @@ PRT( "Time", clock() - clk );
break;
}
}
/*
// check implications using simulation
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
int clk = clock();
int Temp, clk = clock();
if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
PRT( "Time", clock() - clk );
}
*/
// move the classes into representatives and reduce AIG
clk2 = clock();
......
src/aig/fra/fraLcr.c
......@@ -500,17 +500,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
{
int nPartSize = 200;
int fReprSelect = 0;
Fra_Lcr_t * p;
Fra_Sml_t * pSml;
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Vec_Int_t * vPart;
// Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
int i, nIter, clk = clock(), clk2, clk3;
int i, nIter, timeSim, clk = clock(), clk2, clk3;
if ( Aig_ManNodeNum(pAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
......@@ -519,23 +520,33 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
assert( Aig_ManLatchNum(pAig) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
// start the manager
p = Lcr_ManAlloc( pAig );
p->nFramesP = nFramesP;
p->fVerbose = fVerbose;
// simulate the AIG
clk2 = clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
pTemp = Fra_LcrAigPrepare( p->pAig );
pTemp->pBmc = (Fra_Bmc_t *)p;
pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 );
pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 );
if ( fVerbose )
{
PRT( "Time", clock() - clk2 );
p->timeSim += clock() - clk2;
timeSim = clock() - clk2;
}
// check if simulation discovered non-constant-0 POs
if ( fProve && pSml->fNonConstOut )
{
Fra_SmlStop( pSml );
return NULL;
}
// start the manager
p = Lcr_ManAlloc( pAig );
p->nFramesP = nFramesP;
p->fVerbose = fVerbose;
p->timeSim += timeSim;
pTemp = Fra_LcrAigPrepare( pAig );
pTemp->pBmc = (Fra_Bmc_t *)p;
pTemp->pSml = pSml;
// get preliminary info about equivalence classes
pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
Fra_ClassesPrepare( p->pCla, 1 );
......
src/aig/fra/fraSat.c
......@@ -75,6 +75,9 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
......@@ -232,6 +235,9 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
......@@ -318,6 +324,9 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
......
src/aig/fra/fraSec.c
......@@ -103,6 +103,7 @@ PRT( "Time", clock() - clkTotal );
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
......@@ -148,8 +149,16 @@ clk = clock();
{
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
if ( pNew == NULL )
{
RetValue = 0;
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
return RetValue;
}
if ( fVerbose )
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
......@@ -196,7 +205,7 @@ clk = clock();
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
}
// perform retiming
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
......@@ -211,6 +220,26 @@ PRT( "Time", clock() - clk );
}
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
// perform sequential simulation
clk = clock();
pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) );
if ( fVerbose )
{
printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( pSml->fNonConstOut )
{
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
return RetValue;
}
Fra_SmlStop( pSml );
}
// get the miter status
......
src/aig/fra/fraSim.c
......@@ -137,6 +137,28 @@ int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
return Counter;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(p, pObj->Id);
for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
......@@ -550,6 +572,27 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
/**Function*************************************************************
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
int i;
Aig_ManForEachPoSeq( p->pAig, pObj, i )
if ( !Fra_SmlNodeIsZero(p, pObj) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
......@@ -569,14 +612,16 @@ clk = clock();
// simulate the nodes
Aig_ManForEachNode( p->pAig, pObj, i )
Fra_SmlNodeSimulate( p, pObj, f );
// copy simulation info into outputs
Aig_ManForEachPoSeq( p->pAig, pObj, i )
Fra_SmlNodeCopyFanin( p, pObj, f );
// quit if this is the last timeframe
if ( f == p->nFrames - 1 )
break;
// copy simulation info into outputs
Aig_ManForEachLiSeq( p->pAig, pObj, i )
Fra_SmlNodeCopyFanin( p, pObj, f );
// copy simulation info into the inputs
// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
// Fra_SmlNodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
}
......@@ -768,6 +813,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
Fra_SmlInitialize( p, 1 );
Fra_SmlSimulateOne( p );
p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
return p;
}
......
src/aig/ivy/ivyFraig.c
......@@ -2100,6 +2100,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
......@@ -2231,6 +2234,9 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is reserved for const1 node - add the clause
pLits[0] = toLit( 0 );
sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
......
src/aig/kit/kitDsd.c
......@@ -48,7 +48,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
p->dd = Cloud_Init( 16, 13 );
p->dd = Cloud_Init( 16, 14 );
p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
p->vNodes = Vec_IntAlloc( 512 );
return p;
......
src/base/abci/abc.c
......@@ -3095,7 +3095,7 @@ usage:
fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
......
src/base/abci/abcDar.c
......@@ -49,10 +49,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
Aig_Man_t * pMan;
Aig_Obj_t * pObjNew;
Abc_Obj_t * pObj;
int i, nNodes;
int i, nNodes, nDontCares;
// make sure the latches follow PIs/POs
if ( fRegisters )
{
if ( fRegisters )
{
assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
if ( i < Abc_NtkPiNum(pNtk) )
......@@ -64,6 +64,21 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
assert( Abc_ObjIsPo(pObj) );
else
assert( Abc_ObjIsBi(pObj) );
// print warning about initial values
nDontCares = 0;
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_LatchIsInitDc(pObj) )
{
Abc_LatchSetInit0(pObj);
nDontCares++;
}
if ( nDontCares )
{
printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
printf( "Use command \"print_latch\" to see the init values of registers.\n" );
printf( "Use command \"init\" to change the values.\n" );
}
}
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
......@@ -985,7 +1000,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
......
src/base/abci/abcStrash.c
......@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
}
//timeRetime = clock() - timeRetime;
// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
return pNtkAig;
}
......@@ -145,7 +145,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
}
//timeRetime = clock() - timeRetime;
// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
return pNtkAig;
}
......
src/base/seq/seqCreate.c
......@@ -82,7 +82,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsDfsOrdered(pNtk) );
if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// start the network
......
src/base/seq/seqRetCore.c
......@@ -99,7 +99,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
// make sure it is an AIG without self-feeding latches
assert( !Abc_NtkHasAig(pNtk) );
if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// remove the dangling nodes
......
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