From: Sunil Rafeeque K.P. (srafeeque_at_yahoo.com)
Date: Fri Mar 30 2007 - 19:31:01 MDT
hi all,
Can some one tell me how to remove my id from this mailing list
thanks
Sunil
Fabio Somenzi <Fabio_at_Colorado.EDU> wrote: Zaher,
I tried your example on both a stock 2.1 distribution and the current
development version. I cannot reproduce the problem on a Pentium IV.
What architecture are you running vis on?
Thanks
Fabio
>>>>> "ZSA" == Zaher S Andraus writes:
ZSA> Oh, sorry, how did I miss that!
ZSA> The property file is called design1.inv and it has just
ZSA> prop=1;
ZSA> The VIS commands:
ZSA> read_verilog design1.v
ZSA> init_verify
ZSA> build_partition_maigs
ZSA> check_invariant -A4 design1.inv
ZSA> quit
ZSA> Thanks for responding,
ZSA> -x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x
ZSA> Zaher S. Andraus
ZSA> Advanced Computer Architecture Laboratory in EECS
ZSA> University of Michigan - Ann Arbor
ZSA> http://www.eecs.umich.edu/~zandrawi/academic.htm
ZSA> -x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x
ZSA> On Sat, 31 Mar 2007, Andrea Fedeli wrote:
>> HI Zaher,
>>
>> Zaher S Andraus wrote:
>>
>>>
>>> Hi,
>>>
>>> VIS seems to function correctly w/ the default model checking
>>> mode, or with -A3 (Grab algorithm). I am having a problem with
>>> the -A4 option (PureSAT algorithm). VIS is crashing.
>>
>> [...]
>>
>>> Can anyone help?
>>
>>
>> I would need a bit of extra info from you:
>>
>> 1) The property file
>> 2) The commands you executed.
>>
>> With the information you gave it's not easy to dig into your issue.
>>
>> Cheers,
>>
>> Andrea.
>>
>> --
>> Andrea Fedeli
>>
>>
>> A computer, to print out a fact,
>> Will divide, multiply, and subtract.
>> But this output can be
>> No more than debris,
>> If the input was short of exact.
>> -- Gigo
>>
---------------------------------
Don't get soaked. Take a quick peek at the forecast
with theYahoo! Search weather shortcut.
This archive was generated by hypermail 2.1.7 : Fri Mar 30 2007 - 19:32:00 MDT