summaryrefslogtreecommitdiffstats
path: root/src/proof/fra/fra.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-08-24 11:12:51 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-08-24 11:12:51 -0700
commit942600414dba2e32bf2529517e17eaee5991d29c (patch)
treee58e0f65b13952d1773f11731c48a955a7068206 /src/proof/fra/fra.h
parent12c776ed6e5a17a491fdb986ccce99649a06850e (diff)
downloadabc-942600414dba2e32bf2529517e17eaee5991d29c.tar.gz
abc-942600414dba2e32bf2529517e17eaee5991d29c.tar.bz2
abc-942600414dba2e32bf2529517e17eaee5991d29c.zip
Added simulation of comb circuits with user-specified patterns in command 'sim'.
Diffstat (limited to 'src/proof/fra/fra.h')
-rw-r--r--src/proof/fra/fra.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 1690b463..b1fdb539 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -371,8 +371,9 @@ extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit );
extern void Fra_SmlResimulate( Fra_Man_t * p );
extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Fra_SmlStop( Fra_Sml_t * p );
+extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter );
+extern Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose );
extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
-extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );