Re: Needing for more information about counter examples in approximate model checking

From: Fabio Somenzi (Fabio@colorado.edu)
Date: Tue May 28 2002 - 10:30:53 MDT

  • Next message: SouthworthEDA@aol.com: "Re: [Fwd: "VIS Optimization Question"]"

    >>>>> "JM" == Jean-Luc Mercadier <jean-luc.mercadier@tni-valiosys.com> writes:

     JM> Hello,

     JM> I would like to better understand why some of my CTL formulas
     JM> fails on the design I'm checking. I 've got enough information
     JM> when I use "- d 2" option with model-check command, but elapsed
     JM> time for the verification is sometime too long. (I've got
     JM> responses like "fails myVariable=1")

     JM> It seems impossible to obtain such information with the command
     JM> approximate_model_check. (I only got responses like "fails")

     JM> Is it possible to obtain as information as mc -d2 does when using
     JM> approximate_model_check ? If so, please, give me a tip.

     JM> Thanks for your response

     JM> Jean-Luc

    Jean-Luc,

    Unfortunately, approximate_model_check, incremental_ctl_verification,
    iterative_model_check, and model_check -F (forward model checking) do
    not provide counterexamples for failing formulae.

    Have you considered trying model_check -g?

    Fabio

    This archive was generated by hypermail 2b30 : Tue May 28 2002 - 10:49:10 MDT