blob: 333f3851d8df1bc5fa9bb4690a4c77d42b15cdcd (
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[(xlen - 1) .. 1] @ 0b0;
true
}
|