Use of approximate_model_check

• Previous message: hadi afshar: "vl2mv converter problem!"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

 
Hello,

I've tried to check an ACTL formula on the same design with approximate_model_check and model_check commands. I was surprised because results were differents :
- approximate_model_check proved the formula TRUE while model_check found a counter example in a debug trace.
- I've then look at my design and found a bug proving that the approximate model checking wasn't correct.
(As there is no determinism in my design, I've set the amc_prove_false to yes for the approximate model checking)

I thougth that approximations were made on the FSM and on the computation of the transition relation between states but should always lead to a correct proof result in approximate model checking. Perhaps I'm wrong.

Could approximate_model_check lead to incorrect result if not used with good options ?
Could approximate_model_check lead to incorrect result in known cases ?
Could this be a bug ?
Does the ardc level could lead to a wrong result ?

Thanks in advance for your response.

Jean-Luc Mercadier

• Next message: Jean-Luc Mercadier: "More about the use of approximate_model_check"
• Previous message: hadi afshar: "vl2mv converter problem!"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2b30 : Mon Jun 24 2002 - 02:29:43 MDT