current:
let rs1 = EXTZ(X(rs1)[31..0];
let result = (rs1 >> shamt[4..0]) | (X(rs1) << (32 - shamt[4..0]));
X(rd) = EXTS(result[31..0]);
suggested:
let rs1_data = EXTZ(X(rs1)[31..0];
let result = (rs1_data >> shamt[4..0]) | ( rs1_data << (32 - shamt[4..0]));
X(rd) = EXTS(result[31..0]);
In general, I found the use of the same variable for index to register and content of the register ugly and dangerous. That occured in codes for several *w instructions.
Sail code in Chapter 2.31 for roiw has a bug:
current: let rs1 = EXTZ(X(rs1)[31..0]; let result = (rs1 >> shamt[4..0]) | (X(rs1) << (32 - shamt[4..0])); X(rd) = EXTS(result[31..0]);
suggested: let rs1_data = EXTZ(X(rs1)[31..0]; let result = (rs1_data >> shamt[4..0]) | ( rs1_data << (32 - shamt[4..0])); X(rd) = EXTS(result[31..0]);
In general, I found the use of the same variable for index to register and content of the register ugly and dangerous. That occured in codes for several *w instructions.