Commit acdfc3cc by Alan Mishchenko

Recognizing async reset in blasting.

parent f215b1bb
......@@ -142,11 +142,13 @@ struct Wlc_Ntk_t_
Vec_Int_t vCos; // combinational outputs
Vec_Int_t vFfs; // flops
Vec_Int_t vFfs2; // flops
Vec_Int_t * vArsts; // async resets
Vec_Int_t * vInits; // initial values
char * pInits; // initial values
int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
int fSmtLib; // the network comes from an SMT-LIB file
int fAsyncRst; // the network has asynchronous reset
int fMemPorts; // the network contains memory ports
int fEasyFfs; // the network contains simple flops
int nAssert; // the number of asserts
......
......@@ -2112,7 +2112,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
char Buffer[1000];
sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
printf( "Writing %s\n", Buffer );
//printf( "Writing %s\n", Buffer );
}
}
if ( p->pInits )
......
......@@ -1133,6 +1133,11 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
return 0;
}
if ( pNtk->fAsyncRst )
{
Abc_Print( 1, "Abc_CommandBlast(): Trying to bit-blast network with asynchronous reset.\n" );
return 0;
}
if ( fPrintInputInfo )
Wlc_NtkPrintInputInfo(pNtk);
if ( pPar->fMulti )
......
......@@ -141,6 +141,7 @@ Wlc_Ntk_t * Wlc_NtkMemBlast( Wlc_Ntk_t * p )
vFanins = Vec_IntAlloc( 100 );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
Wlc_NtkForEachCi( p, pObj, i )
......@@ -529,6 +530,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
pNew->vInits = Vec_IntAlloc( 100 );
......@@ -1399,6 +1401,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose )
Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
pNew->vInits = Vec_IntAlloc( 100 );
......
......@@ -266,6 +266,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
ABC_FREE( p->vFfs.pArray );
ABC_FREE( p->vFfs2.pArray );
Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vArsts );
ABC_FREE( p->vTravIds.pArray );
ABC_FREE( p->vNameIds.pArray );
ABC_FREE( p->vValues.pArray );
......@@ -961,6 +962,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
vFanins = Vec_IntAlloc( 100 );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
Wlc_NtkForEachCi( p, pObj, i )
......@@ -989,6 +991,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
Wlc_NtkForEachCi( p, pObj, i )
......@@ -1056,6 +1059,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vP
Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
......@@ -1239,6 +1243,7 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
vFanins = Vec_IntAlloc( 100 );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
pNew->fAsyncRst = p->fAsyncRst;
pNew->fMemPorts = p->fMemPorts;
pNew->fEasyFfs = p->fEasyFfs;
Wlc_NtkForEachObj( p, pObj, i )
......
......@@ -481,6 +481,32 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
SeeAlso []
***********************************************************************/
int Wlc_PrsCheckBitConst0( Wlc_Ntk_t * p, int NameId )
{
Wlc_Obj_t * pObj = Wlc_NtkObj( p, NameId );
int * pInits;
if ( Wlc_ObjRange(pObj) != 1 )
return 0;
while ( pObj->Type == WLC_OBJ_BUF )
pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
if ( pObj->Type != WLC_OBJ_CONST )
return 0;
pInits = Wlc_ObjConstValue(pObj);
return Abc_InfoHasBit((unsigned *)pInits, 0) == 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char * Wlc_PrsFindRange( char * pStr, int * End, int * Beg )
{
*End = *Beg = 0;
......@@ -1033,6 +1059,18 @@ startword:
p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
//printf( "%s\n", p->pNtk->pInits );
}
if ( p->pNtk->vArsts )
{
int i, NameIdArst;
Vec_IntForEachEntry( p->pNtk->vArsts, NameIdArst, i )
{
if ( Wlc_PrsCheckBitConst0(p->pNtk, NameIdArst) )
continue;
p->pNtk->fAsyncRst = 1;
printf( "Detected async reset \"%s\".\n", Abc_NamStr(p->pNtk->pManName, NameIdArst) );
break;
}
}
if ( p->vPoPairs )
{
assert( Vec_StrEntryLast(p->vPoPairs) == 0 );
......@@ -1236,6 +1274,21 @@ startword:
if ( pStart == NULL )
break;
pStart = Wlc_PrsSkipSpaces( pStart+1 );
if ( !p->pNtk->fAsyncRst && !strncmp(pStart, "arst", 4) && pStart[4] != 'v' )
{
int NameIdArst;
pStart = Wlc_PrsFindSymbol( pStart, '(' );
if ( pStart == NULL )
return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis in the flop description." );
pStart = Wlc_PrsFindName( pStart+1, &pName );
if ( pStart == NULL )
return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
NameIdArst = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
if ( p->pNtk->vArsts == NULL )
p->pNtk->vArsts = Vec_IntAlloc( 100 );
Vec_IntPushUnique( p->pNtk->vArsts, NameIdArst );
continue;
}
if ( pStart[0] != 'd' && (pStart[0] != 'q' || pStart[1] == 'b') && strncmp(pStart, "arstval", 7) )
continue;
fFlopIn = (pStart[0] == 'd');
......
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