summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/wlc/wlc.h3
-rw-r--r--src/base/wlc/wlcAbs.c158
-rw-r--r--src/base/wlc/wlcCom.c125
-rw-r--r--src/base/wlc/wlcNtk.c2
4 files changed, 285 insertions, 3 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 91dc0573..686d9f00 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -170,6 +170,8 @@ struct Wlc_Par_t_
int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations
int fXorOutput; // XOR outputs of word-level miter
+ int fCheckClauses; // Check clauses in the reloaded trace
+ int fPushClauses; // Push clauses in the reloaded trace
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
@@ -277,6 +279,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
/*=== wlcAbs.c ========================================================*/
extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcAbs2.c ========================================================*/
extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcBlast.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 318df4dd..1e5df918 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -20,6 +20,7 @@
#include "wlc.h"
#include "proof/pdr/pdr.h"
+#include "proof/pdr/pdrInt.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"
@@ -29,6 +30,10 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
+extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses );
+extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -128,6 +133,17 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
Wlc_NtkCleanMarks( p );
Wlc_NtkForEachCo( p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+
+
+ Vec_IntClear(vFlops);
+ Wlc_NtkForEachCi( p, pObj, i ) {
+ if ( !Wlc_ObjIsPi(pObj) ) {
+ Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+ pObj->Mark = 1;
+ }
+ }
+
+
Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
Wlc_NtkForEachObj( p, pObj, i )
@@ -285,6 +301,141 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
/**Function*************************************************************
+ Synopsis [Performs PDR with word-level abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ abctime clk = Abc_Clock();
+ abctime pdrClk;
+ Pdr_Man_t * pPdr;
+ Vec_Vec_t * vClauses = NULL;
+ int nIters, nNodes, nDcFlops, RetValue = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ pPdrPars->fVeryVerbose = 0;
+
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
+ {
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
+ {
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
+ }
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+
+ pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
+ pdrClk = Abc_Clock();
+
+ if ( vClauses ) {
+ assert( Vec_VecSize( vClauses) >= 2 );
+ IPdr_ManRestore( pPdr, vClauses );
+ }
+
+ RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
+ pPdr->tTotal += Abc_Clock() - pdrClk;
+
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ Pdr_ManStop( pPdr );
+ Aig_ManStop( pAig );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ Pdr_ManStop( pPdr );
+ Aig_ManStop( pAig );
+ break;
+ }
+
+ // spurious CEX, continue solving
+ vClauses = IPdr_ManSaveClauses( pPdr, 0 );
+
+ Pdr_ManStop( pPdr );
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
+ Aig_ManStop( pAig );
+ }
+
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs abstraction.]
Description [Derives initial abstraction based on user-specified
@@ -309,11 +460,12 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
// set up parameters to run PDR
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
- pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
- pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
- pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
+ //pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
//pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
pPdrPars->fVerbose = pPars->fPdrVerbose;
+ pPdrPars->fVeryVerbose = 0;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 97717b09..df736e70 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -33,6 +33,7 @@ static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv )
static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -75,6 +76,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
@@ -453,6 +455,129 @@ usage:
SeeAlso []
******************************************************************************/
+int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Wlc_Par_t Pars, * pPars = &Pars;
+ int c;
+ Wlc_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsAdd < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMul < 0 )
+ goto usage;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMux < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsFlop < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
+ case 'c':
+ pPars->fCheckClauses ^= 1;
+ break;
+ case 'p':
+ pPars->fPushClauses ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkPdrAbs( pNtk, pPars );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+ Abc_Print( -2, "\t abstraction for word-level networks\n" );
+ Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+ Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
+ Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
+ Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index e6ab0739..c8fc15a7 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -114,6 +114,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
pPars->nIterMax = 1000; // the max number of iterations
pPars->fXorOutput = 1; // XOR outputs of word-level miter
+ pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
+ pPars->fPushClauses = 0; // Push clauses in the reloaded trace
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 16:53:30 +0000