For the specification of the load multiple instruction of AArch32 it would be nice to have working slices which use the index of a forall statement. I would like to specify the following code:
if regs(0) = 1 then
R(0) := MEM<4>(addr)
forall i : SIntW in 1..15 do
if regs(i) = 1 then
R(i) := MEM<4>(addr + VADL::cob(regs(i-1..0)) << 2)
but I get the following error message:
error: Constant value required
╭── aarch32.vadl:660:52
│
660 │ R(i) := MEM<4>(addr + VADL::cob(regs(i-1..0)) << 2)
│ ^ Cannot evaluate identifier with origin of vadl.ast.ForallStatement
but as the index of a forall is constant this could be evaluated.
It is cumbersome to unroll manually (but the cob could be replaced by a more efficient conditional add).
For the specification of the load multiple instruction of AArch32 it would be nice to have working slices which use the index of a forall statement. I would like to specify the following code:
but I get the following error message:
but as the index of a forall is constant this could be evaluated.
It is cumbersome to unroll manually (but the
cobcould be replaced by a more efficient conditional add).