From 2f90e5e15d8308a9cbebdc15976f5b5b8d3d8032 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Wed, 22 Feb 2017 15:37:49 -0800 Subject: added an option -m for %pdra --- src/base/wlc/wlc.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 686d9f00..abb75f5e 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -172,6 +172,7 @@ struct Wlc_Par_t_ 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 fMFFC; // Refine the entire MFFC of a PPI int fVerbose; // verbose output int fPdrVerbose; // verbose output }; -- cgit v1.2.3 From d5bbf9188c4ea4ded22afe67b18290b148bf1d88 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 23 Feb 2017 08:48:53 -0800 Subject: added %pdra -a: run with pdr -nct --- src/base/wlc/wlc.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index abb75f5e..cb84a70d 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -173,6 +173,7 @@ struct Wlc_Par_t_ int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI + int fPdra; // Use pdr -nct int fVerbose; // verbose output int fPdrVerbose; // verbose output }; -- cgit v1.2.3 From a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 18:32:43 -0800 Subject: added an option -b to %pdra --- src/base/wlc/wlc.h | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index cb84a70d..71273f98 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -174,6 +174,7 @@ struct Wlc_Par_t_ int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI int fPdra; // Use pdr -nct + int fProofRefine; // Use proof-based refinement int fVerbose; // verbose output int fPdrVerbose; // verbose output }; @@ -311,6 +312,7 @@ extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ); +extern Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p ); extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ); extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p ); -- cgit v1.2.3 From 86b3cb3da999b1d5f3e59ff7dacfca00e9c321d6 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 26 Feb 2017 15:39:48 -0800 Subject: added an option -L to %pdra for limiting the number of muxes --- src/base/wlc/wlc.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 71273f98..49ad5bf0 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -169,6 +169,7 @@ struct Wlc_Par_t_ int nBitsMux; // MUX bit-width int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations + int nMuxLimit; // the max number of muxes int fXorOutput; // XOR outputs of word-level miter int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace -- cgit v1.2.3 From 9195192f65bed0c5f3ca2fd8f8b51b34b94f47b3 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 27 Feb 2017 14:31:59 -0800 Subject: %pdra -L: now applies to all types --- src/base/wlc/wlc.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 49ad5bf0..1a2bc505 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -169,7 +169,7 @@ struct Wlc_Par_t_ int nBitsMux; // MUX bit-width int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations - int nMuxLimit; // the max number of muxes + int nLimit; // the max number of signals int fXorOutput; // XOR outputs of word-level miter int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace -- cgit v1.2.3 From 902a78eeb883cb97131e03cc31cf0892787e806e Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 18:05:58 -0800 Subject: added an option -r to %pdra: proof-based refinement only --- src/base/wlc/wlc.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 1a2bc505..f5dbba42 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -171,11 +171,12 @@ struct Wlc_Par_t_ int nIterMax; // the max number of iterations int nLimit; // the max number of signals 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 fMFFC; // Refine the entire MFFC of a PPI - int fPdra; // Use pdr -nct + int fCheckClauses; // Check clauses in the reloaded trace + int fPushClauses; // Push clauses in the reloaded trace + int fMFFC; // Refine the entire MFFC of a PPI + int fPdra; // Use pdr -nct int fProofRefine; // Use proof-based refinement + int fHybrid; // Use a hybrid of CBR and PBR int fVerbose; // verbose output int fPdrVerbose; // verbose output }; -- cgit v1.2.3