From e2e3f6a2281b65632a139933cfc5021a84257a3a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 May 2011 20:33:06 -0700 Subject: Improvements in sequential verification. --- src/aig/saig/saigMiter.c | 20 +++++++++++++++----- src/base/abci/abc.c | 24 ++++++++++++++++++------ src/base/abci/abcDar.c | 37 ++++++++++++++++++++++++++++++++----- 3 files changed, 65 insertions(+), 16 deletions(-) diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index b470333d..4d775314 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -870,8 +870,11 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe int iOut, nOuts; Aig_Man_t * pMiterCec; int RetValue, clkTotal = clock(); - Aig_ManPrintStats( pPart0 ); - Aig_ManPrintStats( pPart1 ); + if ( fVerbose ) + { + Aig_ManPrintStats( pPart0 ); + Aig_ManPrintStats( pPart1 ); + } // Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); // Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); @@ -879,8 +882,8 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe { printf( "Warning: The design after synthesis is smaller!\n" ); printf( "This warning may indicate that the order of designs is changed.\n" ); - printf( "The solver expects the original disign as first argument and\n" ); - printf( "the modified design as the second argument in Ssw_SecSpecial().\n" ); + printf( "The solver expects the original design as first argument and\n" ); + printf( "the modified design as the second argument in \"absec\".\n" ); } // create two-level miter pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames ); @@ -950,7 +953,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbo Aig_Man_t * pPart0, * pPart1; int RetValue; if ( fVerbose ) - printf( "Performing sequential verification combinational A/B miter.\n" ); + printf( "Performing sequential verification using combinational A/B miter.\n" ); // consider the case when a miter is given if ( p1 == NULL ) { @@ -964,6 +967,13 @@ int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbo printf( "Demitering has failed.\n" ); return -1; } + if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) ) + { + Aig_ManStop( pPart0 ); + Aig_ManStop( pPart1 ); + printf( "After demitering AIGs have different number of flops. Quitting.\n" ); + return -1; + } } else { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 10360809..e1398722 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17011,12 +17011,12 @@ int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fMiter, nFrames, fVerbose, c; extern int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose ); - + pNtk = Abc_FrameReadNtk(pAbc); // set defaults fMiter = 1; nFrames = 2; - fVerbose = 1; + fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF ) { @@ -17033,7 +17033,7 @@ int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFrames < 0 ) goto usage; break; - case 'm': + case 'm': fMiter ^= 1; break; case 'v': @@ -17044,14 +17044,26 @@ int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( fMiter ) + if ( fMiter ) { + if ( argc == globalUtilOptind + 1 ) + { + pNtk = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 ); + if ( pNtk == NULL ) + { + Abc_Print( -1, "Cannot read network from file \"%s\".\n", argv[globalUtilOptind] ); + return 0; + } + } + else + pNtk = Abc_NtkDup( pNtk ); if ( !Abc_NtkIsStrash(pNtk) ) { - Abc_Print( -1, "This command works only for structrally hashed networks. Run \"st\".\n" ); - return 0; + pNtk = Abc_NtkStrash( pNtk2 = pNtk, 0, 1, 0 ); + Abc_NtkDelete( pNtk2 ); } Abc_NtkDarAbSec( pNtk, NULL, nFrames, fVerbose ); + Abc_NtkDelete( pNtk ); } else { diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index d443c5e5..34306fd8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2017,6 +2017,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t * ***********************************************************************/ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk ) { + char * pFileNameGeneric, pFileName0[1000], pFileName1[1000]; Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter; // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); @@ -2031,15 +2032,20 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk ) printf( "Demitering has failed.\n" ); return 0; } - Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); - Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); - printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); + // create file names + pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec ); + sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" ); + sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" ); + ABC_FREE( pFileNameGeneric ); + // dump files + Ioa_WriteAiger( pPart0, pFileName0, 0, 0 ); + Ioa_WriteAiger( pPart1, pFileName1, 0, 0 ); + printf( "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 ); // create two-level miter // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 ); // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL ); // Aig_ManStop( pMiter ); // printf( "The new miter is written into file \"%s\".\n", "miter01.blif" ); - Aig_ManStop( pPart0 ); Aig_ManStop( pPart1 ); Aig_ManStop( pMan ); @@ -2315,12 +2321,33 @@ int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVer pMan2 = Abc_NtkToDar( pNtk2, 0, 1 ); if ( pMan2 == NULL ) { + Aig_ManStop( pMan1 ); printf( "Converting miter into AIG has failed.\n" ); return -1; } assert( Aig_ManRegNum(pMan2) > 0 ); + if ( Saig_ManPiNum(pMan1) != Saig_ManPiNum(pMan2) ) + { + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + printf( "The networks have different number of PIs.\n" ); + return -1; + } + if ( Saig_ManPoNum(pMan1) != Saig_ManPoNum(pMan2) ) + { + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + printf( "The networks have different number of POs.\n" ); + return -1; + } + if ( Aig_ManRegNum(pMan1) != Aig_ManRegNum(pMan2) ) + { + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + printf( "The networks have different number of flops.\n" ); + return -1; + } } - // perform verification RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose ); Aig_ManStop( pMan1 ); -- cgit v1.2.3