Zalasr instruction assembly does not accept an immediate

[ThinkOpenly]

I may be reading things wrong, but my interpretation of the Sail code for the LOAD and STORE instructions in model/riscv_insts_base.sail is that they include mnemonics with the various suffixes actually defined by the Zalasr extension, which is not yet ratified. These instructions are:

• l{b,h,w,d}.{aq,aqrl}
• s{b,h,w,d}.{rl,aqrl}

The specified syntax in Sail is:

• LOAD:

  sail-riscv/model/riscv_insts_base.sail

  Lines 317 to 318 in 733accf

  	mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)
  	<-> "l" ^ size_mnemonic(width) ^ maybe_u(is_unsigned) ^ maybe_aqrl(aq, rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"

• STORE:

  sail-riscv/model/riscv_insts_base.sail

  Lines 341 to 342 in 733accf

  	mapping clause assembly = STORE(imm, rs2, rs1, width, aq, rl)
  	<-> "s" ^ size_mnemonic(width) ^ maybe_aqrl(aq, rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

The Zalasr syntax is currently shown here:

• loads: https://github.com/riscv/riscv-zalasr/blob/0fa67c355ea3dfb4f32dc6b141931472239965fc/chapter2.adoc?plain=1#L21-L27
• stores: https://github.com/riscv/riscv-zalasr/blob/0fa67c355ea3dfb4f32dc6b141931472239965fc/chapter2.adoc?plain=1#L74-L80

[Note to self: even though it appears to allow invalid mnemonics like "load-release" and "store-acquire", these are actually rejected in function clause execute (LOAD[...] match vmem_read[...] which eventually uses read_kind_of_flags and write_kind_of_flags to reject these.]

There is a basic issue that I see with the current Sail implementation: this syntax includes the generic (non-Zalasr) instructions that accepts an immediate offset value, but the Zalasr instructions apparently do not (per the links above), and the syntax does not exclude that case.

Zalasr is not ratified, adding a complication, but it is currently in "freeze" state.

[jordancarlin]

Well this is a weird one. PR #328 adds support for Zalasr. The model does not actually support it yet. Looking at the standard load/store instructions, it looks like the disassembly clause is set up to handle the aq/rl bits, but the encdec clause for load and store has them hardwired to false:

mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, width, false, false)
  <-> imm @ encdec_reg(rs1) @ bool_bits(is_unsigned) @ size_enc(width) @ encdec_reg(rd) @ 0b0000011
  when valid_load_encdec(width, is_unsigned)

It should be impossible to actually get it to output these instructions right now, but we should definitely clean that up.