Can't run check_invariant -A4 (The puresat algorithm)

From: Zaher S Andraus (zandrawi_at_eecs.umich.edu)
Date: Fri Mar 30 2007 - 08:57:54 MDT


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.

My Verilog input is:

module design1(clk);
    input clk;

    reg [1:0] cnt;
    initial cnt = 2'b00;
    always @(posedge clk)
      cnt = cnt+1;

    reg sample;
    initial sample = 1'b0;
    always @(posedge clk)
      sample = cnt==2'b10;

    wire prop = sample;
  endmodule // design1

VIS's output is:
Warning: Some variables are unused in model design1.
vis> vis> WARNING : floating node prop
vis> array: object size mismatch
Fatal error: file ./src/array/array.c, line 242
array package error

MV file:
.model design1
.root design1
.latch _n11<0> cnt<0>
.reset cnt$raw_n0<0> ->cnt<0>
.default 0
1 1
.latch _n11<1> cnt<1>
.reset cnt$raw_n0<1> ->cnt<1>
.default 0
1 1
.latch _n13 sample
.reset sample$raw_n8 ->sample
0 0
1 1
.table ->_n1<0>
0
.table ->_n1<1>
0
.table _n1<0> ->cnt$raw_n0<0>
- =_n1<0>
.table _n1<1> ->cnt$raw_n0<1>
- =_n1<1>
.table ->_n3<0>
1
.table ->_n3<1>
0
.table ->_n5
0
.table cnt<0> _n3<0> _n5 ->_n4<0>
.default 0
0 0 1 1
0 1 0 1
1 0 0 1
1 1 1 1
.table ->_n7
0
.table cnt<0> _n3<0> _n7 ->_n6
.default 0
0 1 1 1
1 0 1 1
1 1 0 1
1 1 1 1
.table cnt<1> _n3<1> _n6 ->_n4<1>
.default 0
0 0 1 1
0 1 0 1
1 0 0 1
1 1 1 1
.table _n4<0> ->cnt$raw_n2<0>
- =_n4<0>
.table _n4<1> ->cnt$raw_n2<1>
- =_n4<1>
.table ->_n9
0
.table _n9 ->sample$raw_n8
- =_n9
.table ->_nc<0>
0
.table ->_nc<1>
1
.table cnt<0> _nc<0> ->_nd<0>
.default 0
0 1 1
1 0 1
.table cnt<1> _nc<1> ->_nd<1>
.default 0
0 1 1
1 0 1
.table _nd<0> _nd<1> ->_ne
.default 1
0 0 0
.table _ne ->_nb
0 1
1 0
.table _nb ->sample$raw_na
- =_nb
.table sample ->prop$raw_nf
- =sample
.table prop$raw_nf ->prop
0 0
1 1
.table ->_n10
.default 0
1
.table _n10 cnt$raw_n2<0> cnt$raw_n2<1> ->_n11<0> _n11<1>
.default 0 0
1 - - =cnt$raw_n2<0> =cnt$raw_n2<1>
.table ->_n12
.default 0
1
.table _n12 sample$raw_na ->_n13
.default 0
1 0 0
1 1 1
.end

Can anyone help?

Thanks,
-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



This archive was generated by hypermail 2.1.7 : Fri Mar 30 2007 - 09:04:17 MDT