bounded_model_check and counterexample

From: Fabio (fabio.marcone_at_libero.it)
Date: Sat Jul 10 2004 - 01:21:35 MDT

• Next message: Tom Bienmueller: "Calling check_inv several times"
• Previous message: Zaher S Andraus: "Re: help"
• In reply to: Charles Thangaraj: "RE: help"
• Next in thread: Fabio: "edif2blif"
• Reply: Fabio: "edif2blif"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

Hi!
I use bounded_model_check to verify a combinational circuit and I need to
have a counterexample when the ltl formula fails. is it possible? how?
Using "-d 1" option the answer is:

-State 0:
<unchanged>

because of my circuit doesn't have states (combinational).
I would have a counterexample showing inputs and outputs of my combinational
circuit.

Thanks to all,
Fabio Marcone

• Next message: Tom Bienmueller: "Calling check_inv several times"
• Previous message: Zaher S Andraus: "Re: help"
• In reply to: Charles Thangaraj: "RE: help"
• Next in thread: Fabio: "edif2blif"
• Reply: Fabio: "edif2blif"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Sat Jul 10 2004 - 01:22:46 MDT