aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_jalr_rmem.sail
blob: cd8174ec5ce6b2b00c16fc2316f4811b9720f1bb (plain)
1
2
3
4
5
6
7
8
9
10
/* The definition for the memory model. */

function clause execute (RISCV_JALR(imm, rs1, rd)) = {
  /* FIXME: this does not check for a misaligned target address. See riscv_jalr_seq.sail. */
  /* write rd before anything else to prevent unintended strength */
  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
  let newPC : xlenbits = X(rs1) + EXTS(imm);
  nextPC = newPC[(sizeof(xlen) - 1) .. 1] @ 0b0;
  true
}