Hi,
> 1. Sometimes variables used in original Verilog file are no longer
> visible to the CTL formula during
> model_check.
> Is there any workaround? Will it help if they are declared as
> output?
The command "model_check" automatically creates a reduced FSM that
contains
only the dependent variables to the formula.
So you don't have to do anything for reduction.
Just notice that there is -r option to make the reduced FSM with respect
to each formula
or to the conjunction of all formulae.
>
>
> 2. The debugger of model_check command does not show all the (output)
> variables.
> Is there any way we can direct it to show required information?
Currently, if you set the verbosity larger than 0, you can see the number
of latches
for both multi-valued and binary variables after reduction. But, it
doesn't print out
the names of the latches.
>
>
> Can the error trace generated by debugger be given to simulate
> command?
You have to do this manually.
Hope it helps.
In-Ho
This archive was generated by hypermail 2b29 : Mon Jul 17 2000 - 11:11:40 MDT