Laurent,
The restriction allows vis to effectively delete the input in some
cases, which leads to improved efficiency. The workaround consists of
latching the input. See question 8 of the FAQ at
http://vlsi.colorado.edu/~vis/doc/html/vis-faq.html.
Let us know if you have any more problems.
Roderick Bloem
Laurent Arditi wrote:
>
> I doing some experiments with VIS version 1.4 and getting stopped
> by the following problem:
>
> CTL formula containing signals driven by primary inputs
> are not accepted. The error message says only constants
> and latchs can drive those signals.
> This is also clearly written in the documentation of model_check:
> "Note that the support of any wire referred to in a formula should
> consist only of latches."
>
> I don't understand this restriction. What would be the workaround, if
> any ?
>
> --
> ============================================================ |\/\/\/|
> Laurent Arditi Texas Instruments. MS. 21, BP 5 | |
> Email: larditi@ti.com 06271 Villeneuve-Loubet Cedex ( O O )
> Tel: +33 (0)4 9322 2856 FRANCE | o |
This archive was generated by hypermail 2b30 : Mon May 21 2001 - 10:33:40 MDT