Simulink Design Verifier must be able to infer a loop bound in order to translate the loop correctly for property proving. If you have a loop as shown below:
for idx=1:n
...
end
Simulink Design Verifier will not be able to translate the loop to a specific limit because it does not have any knowledge about n. If you know that n is normally bounded by some value, say 100, you can recode your design as shown below:
for idx=1:100
if idx<=n
...
end
end
You can also do this type of rewriting to get proof results based on the assumption that n<=100.
Also R2008a supports Embedded MATLAB scripts which will make the rewrite easier.
