-
-
Notifications
You must be signed in to change notification settings - Fork 11
Description
@burgholzer Assuming that we are synthesizing the following SyReC program:
module main(inout a(3))
for $i = (#a - 1) to 0 do
if ($i > 0) then
a.$i <=> a.($i - 1)
else
skip
fi ($i > 0)
rof
The synthesis of the ForStatement will fail in the iteration in which $i=0 because of an index of ouf range access when trying to synthesis the AssignStatement of the true branch of the IfStatement due to the VariableAccess a.($i - 1) accessing a bit outside of the valid bitrange [0, 2].
A simple solution would be to perform a dead code elimination during synthesis which in our example would remove the faulty assignment in iteration $i = 0 due to the guard expression evaluating to a boolean constant. However, if a non-compile time constant expression like a.1 != a.2 would be used as the guard expression, the index out of range error of the AssignStatement would still be raised. Since no optimizations are currently applied, the synthesis of both guard expression variants would result in the same error.
The question is, should there be a difference in behaviour between non-/compile-time constant expressions?