@@ -354,13 +388,6 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
...
@@ -354,13 +388,6 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
if(!fFixedPoint)
if(!fFixedPoint)
fprintf(stdout,"Reachability analysis stopped after %d iterations.\n",nIters);
fprintf(stdout,"Reachability analysis stopped after %d iterations.\n",nIters);
// report the stats
if(fVerbose)
{
// nMints = 1;
// fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
}
// complement the output to represent the set of unreachable states
// complement the output to represent the set of unreachable states
Abc_ObjXorFaninC(Abc_NtkPo(pNtkReached,0),0);
Abc_ObjXorFaninC(Abc_NtkPo(pNtkReached,0),0);
...
@@ -372,7 +399,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
...
@@ -372,7 +399,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
Abc_NtkDeleteObj(pObj);
Abc_NtkDeleteObj(pObj);
}
}
// make sure that everything is okay
// check consistency of the network
if(!Abc_NtkCheck(pNtkReached))
if(!Abc_NtkCheck(pNtkReached))
{
{
printf("Abc_NtkReachability: The network check has failed.\n");
printf("Abc_NtkReachability: The network check has failed.\n");
// convert from the blackbox into the network with local functions representated by AIGs
if(pNtk->ntkFunc==ABC_FUNC_BLACKBOX)
{
// change network type
assert(pNtk->pManFunc==NULL);
pNtk->ntkFunc=ABC_FUNC_MAP;
pNtk->pManFunc=pMan->pDesign->pGenlib;
}
elseif(pNtk->ntkFunc!=ABC_FUNC_MAP)
{
sprintf(pMan->sError,"The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.",pNtk->pName);
Ver_ParsePrintErrorMessage(pMan);
return0;
}
}
else
{
// convert from the blackbox into the network with local functions representated by AIGs
if(pNtk->ntkFunc==ABC_FUNC_BLACKBOX)
{
// change network type
assert(pNtk->pManFunc==NULL);
pNtk->ntkFunc=ABC_FUNC_AIG;
pNtk->pManFunc=pMan->pDesign->pManFunc;
}
elseif(pNtk->ntkFunc!=ABC_FUNC_AIG)
{
sprintf(pMan->sError,"The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.",pNtk->pName);
// convert from the mapped netlist into the BDD netlist
if(pNtk->ntkFunc==ABC_FUNC_BLACKBOX)
{
pNtk->ntkFunc=ABC_FUNC_AIG;
assert(pNtk->pManFunc==NULL);
pNtk->pManFunc=pMan->pDesign->pManFunc;
}
elseif(pNtk->ntkFunc!=ABC_FUNC_AIG)
{
sprintf(pMan->sError,"The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.",pMan->pNtkCur);
Ver_ParsePrintErrorMessage(pMan);
return0;
return0;
}
if(pWord[0]=='@')
while(1)
{
{
// get the name of the output signal
Ver_StreamSkipToChars(p,")");
Ver_StreamPopChar(p);
// parse the directive
pWord=Ver_ParseGetName(pMan);
pWord=Ver_ParseGetName(pMan);
if(pWord==NULL)
if(pWord==NULL)
return0;
return0;
// consider the case of reduction operations
}
fReduction=0;
// decide how many statements to parse
if(pWord[0]=='{'&&!pMan->fNameLast)
fStopAfterOne=0;
fReduction=1;
if(strcmp(pWord,"begin"))
if(fReduction)
fStopAfterOne=1;
// iterate over the initial states
while(1)
{
if(!fStopAfterOne)
{
{
pWord++;
// get the name of the output signal
pWord[strlen(pWord)-1]=0;
pWord=Ver_ParseGetName(pMan);
assert(pWord[0]!='\\');
if(pWord==NULL)
return0;
// look for the end of directive
if(!strcmp(pWord,"end"))
break;
}
}
// get the fanout net
// get the fanout net
pNet=Abc_NtkFindNet(pNtk,pWord);
pNet=Ver_ParseFindNet(pNtk,pWord);
if(pNet==NULL)
if(pNet==NULL)
{
{
sprintf(pMan->sError,"Cannot read the assign statement for %s (output wire is not defined).",pWord);
sprintf(pMan->sError,"Cannot read the always statement for %s (output wire is not defined).",pWord);
Ver_ParsePrintErrorMessage(pMan);
Ver_ParsePrintErrorMessage(pMan);
return0;
return0;
}
}
// get the equality sign
// get the equality sign
if(Ver_StreamPopChar(p)!='=')
Symbol=Ver_StreamPopChar(p);
if(Symbol!='<'&&Symbol!='=')
{
{
sprintf(pMan->sError,"Cannot read the assign statement for %s (expected equality sign).",pWord);
sprintf(pMan->sError,"Cannot read the assign statement for %s (expected <= or =).",pWord);
Ver_ParsePrintErrorMessage(pMan);
Ver_ParsePrintErrorMessage(pMan);
return0;
return0;
}
}
if(Symbol=='<')
Ver_StreamPopChar(p);
// skip the comments
// skip the comments
if(!Ver_ParseSkipComments(pMan))
if(!Ver_ParseSkipComments(pMan))
return0;
return0;
// get the second name
// get the second name
if(fReduction)
pWord2=Ver_ParseGetName(pMan);
pEquation=Ver_StreamGetWord(p,";");
if(pWord2==NULL)
else
pEquation=Ver_StreamGetWord(p,",;");
if(pEquation==NULL)
{
sprintf(pMan->sError,"Cannot read the equation for %s.",Abc_ObjName(pNet));
