Using CTL formula involving non constant or latch signals

From: Laurent Arditi (larditi@ti.com)
Date: Mon May 21 2001 - 10:03:24 MDT

  • Next message: Roderick Bloem: "Re: Using CTL formula involving non constant or latch signals"

    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:08:45 MDT