From: Zaher S Andraus (zandrawi_at_eecs.umich.edu)
Date: Fri Mar 30 2007 - 16:27:37 MDT
Oh, sorry, how did I miss that!
The property file is called design1.inv and it has just
prop=1;
The VIS commands:
read_verilog design1.v
init_verify
build_partition_maigs
check_invariant -A4 design1.inv
quit
Thanks for responding,
-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
Zaher S. Andraus
Advanced Computer Architecture Laboratory in EECS
University of Michigan - Ann Arbor
http://www.eecs.umich.edu/~zandrawi/academic.htm
-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
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
>
This archive was generated by hypermail 2.1.7 : Fri Mar 30 2007 - 16:28:19 MDT