• Ticc
• BugClosed
• Ranges that are not powers of 2

Ranges that are not powers of 2

• Submitted by: Marco
• Date: 20 Dec 2005
• Assigned to: nobody

Bug details

Arithmetic expressions do not work properly when variables have ranges that are not of the type [0..(2^n)-1]. This is due to the fact that temporary variables (as provided by the module Symtemp) always have that sort of range. So, if original variables and temporary variables are mixed, Glu complains about them having different ranges.

Luca says: this is worse than it seems. Even if we limit ourselves to ranges that are of the form 2^n, because of the way we try to avoid range overflows, intermediate variables will still have different (larger) ranges. Can we pinpoint at least which glu functions complain? Is there a workaround? It would be a big mess (well, relatively) to fix this.

Marco says: here is the situation:

The following code gives rise to the error.

var x: [0..4];
module Tryme:
    output a { true ==> x' = x -1; }
endmodule

Calling Ticc.mk_sym "Tryme" triggers the error:

mdd_func2c_mod: Cannot operate with two different ranges

The error does not occur if we replace [0..4] with [0..3], or we replace -1 with +1.

The error is raised by a call to Mlglu.mdd_eq_minus_c_mod in Symbuild. It is due to the fact that the temporary variable that is created to hold "x - 1" ha range 0..7, and Mlglu.mdd_eq_minus_c_mod cannot handle two variables with different ranges. Notice that Mlglu.mdd_eq_plus can.

Solutions:

1. Create temporary variables with arbitrary ranges. This would make the module Symtemp quite more complex.
2. Find out why mdd_eq_minus_c_mod cannot handle a result variable with more bits than necessary, and possibly remove such restriction.