lang-empty problem

From: Fang Wang (f_wang@ece.concordia.ca)
Date: Wed Feb 20 2002 - 19:12:55 MST

  • Next message: Roderick Bloem: "Re: lang-empty problem"

    Dear vis,

    I still had some problem in using vis "lang_empty".
    My problem is as follwing.

    I used `tlc` example in the package in the path "\examples\tlc"
    and try to verify an LTL property

    "G(((car_present = YES) * (timer.state = LONG)) -> F(farm_light =
    GREEN))"

    First, I used "Wring-1.1.0" generated a verilog file "foo.v" in which
    I replace
        "car_present = YES" with "p = 1"
        "timer.state = LONG" with "q = 1"
        "farm_light = GREEN" with "r = 1"

    then I try to use vis "lang_empty" to verify it,
    but I donot know how to put in both "tlc.mv" and "foo.mv".

    Could you please tell me how to do this property check.

    Regards!

    fang

    This archive was generated by hypermail 2b30 : Wed Feb 20 2002 - 19:19:39 MST