XISA Spec Coverage
ISA specification content on this page is derived from the
Xsight Labs XISA specification
, licensed under the
Mozilla Public License 2.0.
Section numbers refer to the official white paper.
# 3 Parser Programming Model
# 3.12.1 NXTP
Done
function clause pexecute(PNXTP(rs, src_offset_bits, size_bits)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let sz : nat = unsigned(size_bits);
let extracted = extract_bits(src_val, soff, sz);
// Protocol key is up to 24 bits — truncate to bits24.
let key : bits24 = sail_mask(24, extracted);
nxtp_matched = transition_lookup(parser_state, key);
RETIRE_SUCCESS
}
# 3.12.2 PSEEK, PSEEKNXTP
Done — No PSEEK_ERROR/trap, no .CD. Fixed hdr length per entry
function clause pexecute(PPSEEK(rd, dest_offset_bits, rs, src_offset_bits, size_bits, class_id)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let sz : nat = unsigned(size_bits);
let doff : nat = unsigned(dest_offset_bits);
// Extract initial protocol value from source register
let initial = extract_bits(src_val, soff, sz);
var proto : bits16 = sail_mask(16, initial);
var current_size : nat = sz;
// Scan loop: keep skipping while protocol matches a PSEEK entry
var scanning : bool = true;
while scanning do {
let entry_idx = pseek_lookup(class_id, proto);
if entry_idx < 0 then {
// No match — stop scanning
scanning = false
} else {
// Match: advance cursor by header length
let hdr_len : bits8 = read_pseek_hdr_length(entry_idx);
pcursor = pcursor + hdr_len;
// Extract next protocol from packet
let next_off : int = unsigned(pcursor) + unsigned(read_pseek_next_proto_off(entry_idx));
let next_sz : nat = unsigned(read_pseek_next_proto_size(entry_idx));
proto = pseek_extract_proto(next_off, next_sz);
current_size = next_sz
}
};
// Store final protocol value in DestReg at DestOffsetBits
let dst_val = read_preg(rd);
let proto_128 : bits128 = sail_zero_extend(proto, 128);
let result = insert_bits(dst_val, doff, current_size, proto_128);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PPSEEKNXTP(rd, dest_offset_bits, rs, src_offset_bits, size_bits, class_id)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let sz : nat = unsigned(size_bits);
let doff : nat = unsigned(dest_offset_bits);
// Extract initial protocol value from source register
let initial = extract_bits(src_val, soff, sz);
var proto : bits16 = sail_mask(16, initial);
var current_size : nat = sz;
// Scan loop (same as PSEEK)
var scanning : bool = true;
while scanning do {
let entry_idx = pseek_lookup(class_id, proto);
if entry_idx < 0 then {
scanning = false
} else {
let hdr_len : bits8 = read_pseek_hdr_length(entry_idx);
pcursor = pcursor + hdr_len;
let next_off : int = unsigned(pcursor) + unsigned(read_pseek_next_proto_off(entry_idx));
let next_sz : nat = unsigned(read_pseek_next_proto_size(entry_idx));
proto = pseek_extract_proto(next_off, next_sz);
current_size = next_sz
}
};
// Store final protocol value in DestReg
let dst_val = read_preg(rd);
let proto_128 : bits128 = sail_zero_extend(proto, 128);
let result = insert_bits(dst_val, doff, current_size, proto_128);
write_preg(rd, result);
// NXTP lookup with final protocol
let key : bits24 = sail_zero_extend(proto, 24);
nxtp_matched = transition_lookup(parser_state, key);
RETIRE_SUCCESS
}
# 3.12.3 EXT, EXTNXTP
Done — .CD supported. No .PR, .SCSM, .ECSM yet
function clause pexecute(PEXT(rd, dest_offset, src_offset_bits, size_bits, clear_dest)) = {
let doff = unsigned(dest_offset);
let soff = unsigned(src_offset_bits);
let sz = unsigned(size_bits);
let cursor_bit_offset = unsigned(pcursor) * 8;
let packet_bit_offset = cursor_bit_offset + soff;
// Compute byte index and bit-within-byte using bitvector shift/mask (avoids int division).
let pbo_bv : bits(20) = get_slice_int(20, packet_bit_offset, 0);
let start_byte = unsigned(sail_shiftright(pbo_bv, 3));
let bit_in_byte = unsigned(pbo_bv & 0x00007);
// bytes_needed = ceil((bit_in_byte + sz) / 8)
let sum_bv : bits(20) = get_slice_int(20, bit_in_byte + sz + 7, 0);
let bytes_needed = unsigned(sail_shiftright(sum_bv, 3));
// Accumulate bytes into a 128-bit value (big-endian).
var acc : bits128 = sail_zeros(128);
var i : int = 0;
while i < bytes_needed do {
let byte_idx : int = start_byte + i;
let byte_val : bits128 = sail_zero_extend(read_packet_byte(byte_idx), 128);
// Place this byte: first byte is most significant
acc = acc | sail_shiftleft(byte_val, 8 * (bytes_needed - 1 - i));
i = i + 1
};
// Shift right to align the extracted bits, then mask to sz bits.
let shift_amount : int = bytes_needed * 8 - bit_in_byte - sz;
let extracted : bits128 = sail_shiftright(acc, shift_amount) & sail_mask(128, sail_ones(sz));
// Write to destination register
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, doff, sz, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PEXTNXTP(rd, src_offset_bits, size_bits, clear_dest)) = {
let soff = unsigned(src_offset_bits);
let sz = unsigned(size_bits);
let cursor_bit_offset = unsigned(pcursor) * 8;
let packet_bit_offset = cursor_bit_offset + soff;
// Packet extraction logic (same as EXT)
let pbo_bv : bits(20) = get_slice_int(20, packet_bit_offset, 0);
let start_byte = unsigned(sail_shiftright(pbo_bv, 3));
let bit_in_byte = unsigned(pbo_bv & 0x00007);
let sum_bv : bits(20) = get_slice_int(20, bit_in_byte + sz + 7, 0);
let bytes_needed = unsigned(sail_shiftright(sum_bv, 3));
var acc : bits128 = sail_zeros(128);
var i : int = 0;
while i < bytes_needed do {
let byte_idx : int = start_byte + i;
let byte_val : bits128 = sail_zero_extend(read_packet_byte(byte_idx), 128);
acc = acc | sail_shiftleft(byte_val, 8 * (bytes_needed - 1 - i));
i = i + 1
};
let shift_amount : int = bytes_needed * 8 - bit_in_byte - sz;
let extracted : bits128 = sail_shiftright(acc, shift_amount) & sail_mask(128, sail_ones(sz));
// Write to destination register at offset 0
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, 0, sz, extracted);
write_preg(rd, result);
// NXTP: use extracted value as transition key (up to 24 bits)
let key : bits24 = sail_mask(24, extracted);
nxtp_matched = transition_lookup(parser_state, key);
RETIRE_SUCCESS
}
# 3.12.4 EXTMAP
Done — No .PR, .SCSM, .ECSM yet
function clause pexecute(PEXTMAP(map_idx, dest_offset, pkt_offset_bits, size_bits)) = {
let midx : int = unsigned(map_idx);
let doff = unsigned(dest_offset);
let soff = unsigned(pkt_offset_bits);
let sz = unsigned(size_bits);
let cursor_bit_offset = unsigned(pcursor) * 8;
let packet_bit_offset = cursor_bit_offset + soff;
// Compute byte index and bit-within-byte (same as EXT).
let pbo_bv : bits(20) = get_slice_int(20, packet_bit_offset, 0);
let start_byte = unsigned(sail_shiftright(pbo_bv, 3));
let bit_in_byte = unsigned(pbo_bv & 0x00007);
// bytes_needed = ceil((bit_in_byte + sz) / 8)
let sum_bv : bits(20) = get_slice_int(20, bit_in_byte + sz + 7, 0);
let bytes_needed = unsigned(sail_shiftright(sum_bv, 3));
// Accumulate bytes into a 128-bit value (big-endian).
var acc : bits128 = sail_zeros(128);
var i : int = 0;
while i < bytes_needed do {
let byte_idx : int = start_byte + i;
let byte_val : bits128 = sail_zero_extend(read_packet_byte(byte_idx), 128);
acc = acc | sail_shiftleft(byte_val, 8 * (bytes_needed - 1 - i));
i = i + 1
};
// Shift right to align the extracted bits, then mask to sz bits.
let shift_amount : int = bytes_needed * 8 - bit_in_byte - sz;
let extracted : bits128 = sail_shiftright(acc, shift_amount) & sail_mask(128, sail_ones(sz));
// Write to MAP register
let dst_val = read_mapreg(midx);
let result = insert_bits(dst_val, doff, sz, extracted);
write_mapreg(midx, result);
RETIRE_SUCCESS
}
# 3.12.5 MOVMAP
Done — No .HDR modifier yet
function clause pexecute(PMOVMAP(map_idx, dest_offset, rs, src_offset, size_bits)) = {
let midx : int = unsigned(map_idx);
let doff : nat = unsigned(dest_offset);
let soff : nat = unsigned(src_offset);
let sz : nat = unsigned(size_bits);
let src_val = read_preg(rs);
let extracted = extract_bits(src_val, soff, sz);
let dst_val = read_mapreg(midx);
let result = insert_bits(dst_val, doff, sz, extracted);
write_mapreg(midx, result);
RETIRE_SUCCESS
}
# 3.12.6 CNCTBY, CNCTBI
Done — .CD supported
function clause pexecute(PCNCTBY(
rd,
dest_offset_bytes,
rs1,
src1_offset_bytes,
src1_size_bytes,
rs2,
src2_offset_bytes,
src2_size_bytes,
clear_dest,
)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset_bytes) * 8;
let s1off : nat = unsigned(src1_offset_bytes) * 8;
let s1sz : nat = unsigned(src1_size_bytes) * 8;
let s2off : nat = unsigned(src2_offset_bytes) * 8;
let s2sz : nat = unsigned(src2_size_bytes) * 8;
let part1 = extract_bits(s1_val, s1off, s1sz);
let part2 = extract_bits(s2_val, s2off, s2sz);
let combined : bits128 = sail_shiftleft(part1, s2sz) | part2;
let total_sz : nat = s1sz + s2sz;
let result = insert_bits(dst_val, doff, total_sz, combined);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PCNCTBI(
rd,
dest_offset_bits,
rs1,
src1_offset_bits,
src1_size_bits,
rs2,
src2_offset_bits,
src2_size_bits,
clear_dest,
)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset_bits);
let s1off : nat = unsigned(src1_offset_bits);
let s1sz : nat = unsigned(src1_size_bits);
let s2off : nat = unsigned(src2_offset_bits);
let s2sz : nat = unsigned(src2_size_bits);
let part1 = extract_bits(s1_val, s1off, s1sz);
let part2 = extract_bits(s2_val, s2off, s2sz);
let combined : bits128 = sail_shiftleft(part1, s2sz) | part2;
let total_sz : nat = s1sz + s2sz;
let result = insert_bits(dst_val, doff, total_sz, combined);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.7 STH
Done — .H supported. No JumpMode, .SCSM, .ECSM yet
function clause pexecute(PSTH(present_id, offset_id, halt)) = {
set_hdr(present_id, offset_id);
if halt then {
parser_halted = true;
RETIRE_HALT
} else {
RETIRE_SUCCESS
}
}
# 3.12.8 STC, STCI
Done — No JumpMode, .SCSM, .ECSM yet
function clause pexecute(PSTC(rs, src_offset_bits, src_size_bits, src_shift, additional_incr)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let sz : nat = unsigned(src_size_bits);
let extracted = extract_bits(src_val, soff, sz);
let base : bits8 = sail_mask(8, extracted) + sail_mask(8, additional_incr);
let shift_amount : nat = unsigned(src_shift);
let shifted : bits8 = sail_shiftleft(base, shift_amount);
pcursor = pcursor + shifted;
RETIRE_SUCCESS
}
function clause pexecute(PSTCI(incr_value)) = {
let incr_8 : bits8 = sail_mask(8, incr_value);
pcursor = pcursor + incr_8;
RETIRE_SUCCESS
}
# 3.12.9 STCH, STHC
Done — .H supported (STCH). No JumpMode, .SCSM, .ECSM yet
function clause pexecute(PSTCH(incr_value, present_id, offset_id, halt)) = {
let incr_8 : bits8 = sail_mask(8, incr_value);
pcursor = pcursor + incr_8;
set_hdr(present_id, offset_id);
if halt then {
parser_halted = true;
RETIRE_HALT
} else {
RETIRE_SUCCESS
}
}
function clause pexecute(PSTHC(incr_value, present_id, offset_id)) = {
set_hdr(present_id, offset_id);
let incr_8 : bits8 = sail_mask(8, incr_value);
pcursor = pcursor + incr_8;
RETIRE_SUCCESS
}
# 3.12.10 ST, STI
Done — .H supported (ST). HW bits 6-31 restriction not enforced
function clause pexecute(PST(rs, src_offset_bits, struct_offset_bits, size_bits, halt)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let doff : nat = unsigned(struct_offset_bits);
let sz : nat = unsigned(size_bits);
let extracted = extract_bits(src_val, soff, sz);
struct0 = insert_bits(struct0, doff, sz, extracted);
if halt then {
parser_halted = true;
RETIRE_HALT
} else {
RETIRE_SUCCESS
}
}
function clause pexecute(PSTI(immediate, struct_offset_bits, size_bits)) = {
let doff : nat = unsigned(struct_offset_bits);
let sz : nat = unsigned(size_bits);
let imm_128 : bits128 = sail_zero_extend(immediate, 128);
struct0 = insert_bits(struct0, doff, sz, imm_128);
RETIRE_SUCCESS
}
# 3.12.11 MOV, MOVI
Done — .CD supported
function clause pexecute(PMOV(rd, dest_offset, rs, src_offset, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset);
let soff : nat = unsigned(src_offset);
let sz : nat = unsigned(size_bits);
let extracted = extract_bits(src_val, soff, sz);
let result = insert_bits(dst_val, doff, sz, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVI(rd, dest_offset_bytes, immediate, size_bits, clear_dest)) = {
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset_bytes) * 8;
let sz : nat = unsigned(size_bits);
let imm_128 : bits128 = sail_zero_extend(immediate, 128);
let result = insert_bits(dst_val, doff, sz, imm_128);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.12 MOVL, MOVLI, MOVLII, MOVR, MOVRI, MOVRII
Done — .CD supported
function clause pexecute(PMOVL(rd, rs1, offs1, size1, rs2, offs2, size2, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let o1 : nat = unsigned(offs1);
let sz1 : nat = unsigned(size1);
let o2 : nat = unsigned(offs2);
let sz2 : nat = unsigned(size2);
let dynamic_offset : nat = unsigned(extract_bits(s2_val, o2, sz2));
let k : nat = dynamic_offset + o1;
let extracted = extract_bits(s1_val, o1, sz1);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, k, sz1, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVLI(rd, rs, offs, size_bits, imm_value, clear_dest)) = {
let src_val = read_preg(rs);
let o : nat = unsigned(offs);
let sz : nat = unsigned(size_bits);
let imm : nat = unsigned(imm_value);
let k : nat = imm + o;
let extracted = extract_bits(src_val, o, sz);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, k, sz, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVLII(rd, rs, offs, size_bits, imm_value, imm_value_size, clear_dest)) = {
let src_val = read_preg(rs);
let o : nat = unsigned(offs);
let sz : nat = unsigned(size_bits);
let imm_sz : nat = unsigned(imm_value_size);
let k : nat = unsigned(extract_bits(src_val, o, sz));
let imm_128 : bits128 = sail_zero_extend(sail_mask(128, imm_value), 128);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, k, imm_sz, imm_128);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVR(rd, rs1, offs1, size1, rs2, offs2, size2, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let o1 : nat = unsigned(offs1);
let sz1 : nat = unsigned(size1);
let o2 : nat = unsigned(offs2);
let sz2 : nat = unsigned(size2);
let dynamic_offset : nat = unsigned(extract_bits(s2_val, o2, sz2));
let k : int = o1 - dynamic_offset;
let k_clamped : nat = if k < 0 then { 0 } else { k };
let extracted = extract_bits(s1_val, o1, sz1);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, k_clamped, sz1, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVRI(rd, rs, offs, size_bits, imm_value, clear_dest)) = {
let src_val = read_preg(rs);
let o : nat = unsigned(offs);
let sz : nat = unsigned(size_bits);
let imm : nat = unsigned(imm_value);
let k : int = o - imm;
let k_clamped : nat = if k < 0 then { 0 } else { k };
let extracted = extract_bits(src_val, o, sz);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, k_clamped, sz, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PMOVRII(rd, rs, offs, size_bits, imm_value, imm_value_size, clear_dest)) = {
let src_val = read_preg(rs);
let o : nat = unsigned(offs);
let sz : nat = unsigned(size_bits);
let imm_sz : nat = unsigned(imm_value_size);
let reg_offset : nat = unsigned(extract_bits(src_val, o, sz));
let data_size : int = imm_sz - reg_offset;
let data_size_nat : nat = if data_size < 0 then { 0 } else { data_size };
// Extract from ImmValue starting at bit reg_offset, for data_size_nat bits
let imm_128 : bits128 = sail_zero_extend(sail_mask(128, imm_value), 128);
let extracted = extract_bits(imm_128, reg_offset, data_size_nat);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let result = insert_bits(dst_val, 0, data_size_nat, extracted);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.13 ADD, ADDI
Done — .CD supported
function clause pexecute(PADD(rd, dest_offset, rs1, src1_offset, rs2, src2_offset, size_bits, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset);
let s1off : nat = unsigned(src1_offset);
let s2off : nat = unsigned(src2_offset);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(s1_val, s1off, sz);
let op2 = extract_bits(s2_val, s2off, sz);
let sum : bits128 = sail_mask(128, sail_ones(sz)) & (op1 + op2);
pflag_z = sum == sail_zeros(128);
let result = insert_bits(dst_val, doff, sz, sum);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PADDI(rd, rs, immediate, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, 0, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let sum : bits128 = sail_mask(128, sail_ones(sz)) & (op1 + op2);
pflag_z = sum == sail_zeros(128);
let result = insert_bits(dst_val, 0, sz, sum);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.14 SUB, SUBI, SUBII
Done — .CD supported
function clause pexecute(PSUB(rd, dest_offset, rs1, src1_offset, rs2, src2_offset, size_bits, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset);
let s1off : nat = unsigned(src1_offset);
let s2off : nat = unsigned(src2_offset);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(s1_val, s1off, sz);
let op2 = extract_bits(s2_val, s2off, sz);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
let result = insert_bits(dst_val, doff, sz, diff);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PSUBI(rd, rs, immediate, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, 0, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
let result = insert_bits(dst_val, 0, sz, diff);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PSUBII(rd, immediate, rs, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let sz : nat = unsigned(size_bits);
let op1 : bits128 = sail_zero_extend(immediate, 128);
let op2 = extract_bits(src_val, 0, sz);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
let result = insert_bits(dst_val, 0, sz, diff);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.15 AND, ANDI
Done — .CD supported
function clause pexecute(PAND(rd, dest_offset, rs1, src1_offset, rs2, src2_offset, size_bits, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset);
let s1off : nat = unsigned(src1_offset);
let s2off : nat = unsigned(src2_offset);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(s1_val, s1off, sz);
let op2 = extract_bits(s2_val, s2off, sz);
let res : bits128 = op1 & op2;
pflag_z = res == sail_zeros(128);
let result = insert_bits(dst_val, doff, sz, res);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PANDI(rd, rs, immediate, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, 0, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let res : bits128 = op1 & op2;
pflag_z = res == sail_zeros(128);
let result = insert_bits(dst_val, 0, sz, res);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.16 OR, ORI
Done — .CD supported
function clause pexecute(POR(rd, dest_offset, rs1, src1_offset, rs2, src2_offset, size_bits, clear_dest)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let doff : nat = unsigned(dest_offset);
let s1off : nat = unsigned(src1_offset);
let s2off : nat = unsigned(src2_offset);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(s1_val, s1off, sz);
let op2 = extract_bits(s2_val, s2off, sz);
let res : bits128 = op1 | op2;
pflag_z = res == sail_zeros(128);
let result = insert_bits(dst_val, doff, sz, res);
write_preg(rd, result);
RETIRE_SUCCESS
}
function clause pexecute(PORI(rd, rs, immediate, size_bits, clear_dest)) = {
let src_val = read_preg(rs);
let dst_val : bits128 = if clear_dest then {
sail_zeros(128)
} else {
read_preg(rd)
};
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, 0, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let res : bits128 = op1 | op2;
pflag_z = res == sail_zeros(128);
let result = insert_bits(dst_val, 0, sz, res);
write_preg(rd, result);
RETIRE_SUCCESS
}
# 3.12.17 CMP, CMPIBY, CMPIBI
Done
function clause pexecute(PCMP(rs1, src1_offset, rs2, src2_offset, size_bits)) = {
let s1_val = read_preg(rs1);
let s2_val = read_preg(rs2);
let s1off : nat = unsigned(src1_offset);
let s2off : nat = unsigned(src2_offset);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(s1_val, s1off, sz);
let op2 = extract_bits(s2_val, s2off, sz);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
RETIRE_SUCCESS
}
function clause pexecute(PCMPIBY(rs, src_offset_bytes, immediate, size_bits)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bytes) * 8;
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, soff, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
RETIRE_SUCCESS
}
function clause pexecute(PCMPIBI(rs, src_offset_bits, immediate, size_bits)) = {
let src_val = read_preg(rs);
let soff : nat = unsigned(src_offset_bits);
let sz : nat = unsigned(size_bits);
let op1 = extract_bits(src_val, soff, sz);
let op2 : bits128 = sail_zero_extend(immediate, 128);
let diff : bits128 = sail_mask(128, sail_ones(sz)) & sub_bits(op1, op2);
pflag_z = diff == sail_zeros(128);
pflag_n = (sail_shiftright(diff, sz - 1) & sail_mask(128, 0x01)) != sail_zeros(128);
RETIRE_SUCCESS
}
# 3.12.18 BR, BRNS, BRBTST, BRNXTP, BRBTSTNXTP, BRBTSTNS
Done — JumpMode 100 (trap) deferred
function clause pexecute(PBR(cc, target)) = {
if eval_pcond(cc) then {
ppc = target
};
RETIRE_SUCCESS
}
function clause pexecute(PBRNS(cc, rule_num)) = {
if eval_pcond(cc) then {
let idx : int = unsigned(rule_num);
ppc = read_tt_next_pc(idx);
parser_state = read_tt_next_state(idx)
};
RETIRE_SUCCESS
}
function clause pexecute(PBRBTST(btcc, rs, bit_offset, target)) = {
let src_val = read_preg(rs);
let boff : nat = unsigned(bit_offset);
let bit_val = extract_bits(src_val, boff, 1);
let bit_is_set = bit_val != sail_zeros(128);
let take_branch : bool = match btcc {
PBT_CLR => not_bool(bit_is_set),
PBT_SET => bit_is_set,
};
if take_branch then {
ppc = target
};
RETIRE_SUCCESS
}
function clause pexecute(PBRNXTP(cc, jump_mode, addr_or_rule)) = {
if eval_pcond(cc) then {
if nxtp_matched then {
// Match: branch to NXTP result
ppc = nxtp_result_pc;
parser_state = nxtp_result_state
} else {
// No match: follow JumpMode
let mode : int = unsigned(jump_mode);
if mode == 0 then {
// 000: No jump
()
} else {
if mode == 1 then {
// 001: Continue to next instruction
()
} else {
if mode == 2 then {
// 010: Jump to explicit address
ppc = addr_or_rule
} else {
if mode == 3 then {
// 011: Transition to state from specified rule
let idx : int = unsigned(addr_or_rule);
ppc = read_tt_next_pc(idx);
parser_state = read_tt_next_state(idx)
} else {
// 100 (trap) and others: not yet supported
()
}
}
}
}
}
};
RETIRE_SUCCESS
}
function clause pexecute(PBRBTSTNXTP(btcc, rs, bit_offset, jump_mode, addr_or_rule)) = {
let src_val = read_preg(rs);
let boff : nat = unsigned(bit_offset);
let bit_val = extract_bits(src_val, boff, 1);
let bit_is_set = bit_val != sail_zeros(128);
let take_branch : bool = match btcc {
PBT_CLR => not_bool(bit_is_set),
PBT_SET => bit_is_set,
};
if take_branch then {
if nxtp_matched then {
ppc = nxtp_result_pc;
parser_state = nxtp_result_state
} else {
let mode : int = unsigned(jump_mode);
if mode == 0 then {
()
} else {
if mode == 1 then {
()
} else {
if mode == 2 then {
ppc = addr_or_rule
} else {
if mode == 3 then {
let idx : int = unsigned(addr_or_rule);
ppc = read_tt_next_pc(idx);
parser_state = read_tt_next_state(idx)
} else {
()
}
}
}
}
}
};
RETIRE_SUCCESS
}
function clause pexecute(PBRBTSTNS(btcc, rs, bit_offset, rule_num)) = {
let src_val = read_preg(rs);
let boff : nat = unsigned(bit_offset);
let bit_val = extract_bits(src_val, boff, 1);
let bit_is_set = bit_val != sail_zeros(128);
let take_branch : bool = match btcc {
PBT_CLR => not_bool(bit_is_set),
PBT_SET => bit_is_set,
};
if take_branch then {
let idx : int = unsigned(rule_num);
ppc = read_tt_next_pc(idx);
parser_state = read_tt_next_state(idx)
};
RETIRE_SUCCESS
}
# 3.12.19 HALT, HALTDROP
Done — No .RP or MAP-PC support yet
function clause pexecute(PHALT(drop)) = {
parser_halted = true;
if drop then {
parser_drop = true;
RETIRE_DROP
} else {
RETIRE_HALT
}
}
# 3.12.20 NOP
Done
function clause pexecute(PNOP()) = RETIRE_SUCCESS
# 4 MAP Programming Model
# 4.13.1 ADD, ADDI
Done — .F, .SX, .SH supported
function clause mexecute(MADD(rd, rw, rs1, sw1, s1off, s1sz, rs2, sw2, s2off, s2sz, set_flags, sign_extend, short_mode)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let w2 = read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2));
let op1 : bits(32) = if sign_extend then {
map_extract_sx(w1, unsigned(s1off), unsigned(s1sz))
} else {
map_extract(w1, unsigned(s1off), unsigned(s1sz))
};
let op2 : bits(32) = if sign_extend then {
map_extract_sx(w2, unsigned(s2off), unsigned(s2sz))
} else {
map_extract(w2, unsigned(s2off), unsigned(s2sz))
};
let mask : bits(32) = if short_mode then { 0x0000FFFF } else { 0xFFFFFFFF };
let result : bits(32) = (op1 + op2) & mask;
if set_flags then {
map_set_flags_add(op1, op2, result, short_mode)
};
map_write_result(rd_idx, rw_idx, result, short_mode);
RETIRE_SUCCESS
}
function clause mexecute(MADDI(rd, rw, rs1, sw1, s1off, s1sz, imm16, set_flags, sign_extend, short_mode)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let op1 : bits(32) = if sign_extend then {
map_extract_sx(w1, unsigned(s1off), unsigned(s1sz))
} else {
map_extract(w1, unsigned(s1off), unsigned(s1sz))
};
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let mask : bits(32) = if short_mode then { 0x0000FFFF } else { 0xFFFFFFFF };
let result : bits(32) = (op1 + op2) & mask;
if set_flags then {
map_set_flags_add(op1, op2, result, short_mode)
};
map_write_result(rd_idx, rw_idx, result, short_mode);
RETIRE_SUCCESS
}
# 4.13.2 SUB, SUBI
Done — .F, .SX, .SH supported
function clause mexecute(MSUB(rd, rw, rs1, sw1, s1off, s1sz, rs2, sw2, s2off, s2sz, set_flags, sign_extend, short_mode)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let w2 = read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2));
let op1 : bits(32) = if sign_extend then {
map_extract_sx(w1, unsigned(s1off), unsigned(s1sz))
} else {
map_extract(w1, unsigned(s1off), unsigned(s1sz))
};
let op2 : bits(32) = if sign_extend then {
map_extract_sx(w2, unsigned(s2off), unsigned(s2sz))
} else {
map_extract(w2, unsigned(s2off), unsigned(s2sz))
};
let mask : bits(32) = if short_mode then { 0x0000FFFF } else { 0xFFFFFFFF };
let result : bits(32) = sub_bits(op1, op2) & mask;
if set_flags then {
map_set_flags_sub(op1, op2, result, short_mode)
};
map_write_result(rd_idx, rw_idx, result, short_mode);
RETIRE_SUCCESS
}
function clause mexecute(MSUBI(rd, rw, rs1, sw1, s1off, s1sz, imm16, set_flags, sign_extend, short_mode)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let op1 : bits(32) = if sign_extend then {
map_extract_sx(w1, unsigned(s1off), unsigned(s1sz))
} else {
map_extract(w1, unsigned(s1off), unsigned(s1sz))
};
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let mask : bits(32) = if short_mode then { 0x0000FFFF } else { 0xFFFFFFFF };
let result : bits(32) = sub_bits(op1, op2) & mask;
if set_flags then {
map_set_flags_sub(op1, op2, result, short_mode)
};
map_write_result(rd_idx, rw_idx, result, short_mode);
RETIRE_SUCCESS
}
# 4.13.3 MOD, MODI
Not started — Async, needs LFLAG
# 4.13.4 CMP, CMPI
Done — Always sets Z, C
function clause mexecute(MCMP(rs1, sw1, s1off, rs2, sw2, s2off, sz)) = {
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let w2 = read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2));
let op1 = map_extract(w1, unsigned(s1off), unsigned(sz));
let op2 = map_extract(w2, unsigned(s2off), unsigned(sz));
let result : bits(32) = sub_bits(op1, op2);
mflag_z = result == 0x00000000;
mflag_c = unsigned(op1) < unsigned(op2);
RETIRE_SUCCESS
}
function clause mexecute(MCMPI(rs1, sw1, s1off, imm16, sz)) = {
let w1 = read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1));
let op1 = map_extract(w1, unsigned(s1off), unsigned(sz));
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let result : bits(32) = sub_bits(op1, op2);
mflag_z = result == 0x00000000;
mflag_c = unsigned(op1) < unsigned(op2);
RETIRE_SUCCESS
}
# 4.13.5 AND, ANDI
Done — .F supported
function clause mexecute(MAND(rd, rw, rs1, sw1, s1off, rs2, sw2, s2off, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 = map_extract(read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)), unsigned(s2off), unsigned(sz));
let result : bits(32) = op1 & op2;
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
function clause mexecute(MANDI(rd, rw, rs1, sw1, s1off, imm16, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let result : bits(32) = op1 & op2;
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
# 4.13.6 OR, ORI
Done — .F supported
function clause mexecute(MOR(rd, rw, rs1, sw1, s1off, rs2, sw2, s2off, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 = map_extract(read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)), unsigned(s2off), unsigned(sz));
let result : bits(32) = op1 | op2;
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
function clause mexecute(MORI(rd, rw, rs1, sw1, s1off, imm16, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let result : bits(32) = op1 | op2;
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
# 4.13.7 XOR, XORI
Done — .F supported
function clause mexecute(MXOR(rd, rw, rs1, sw1, s1off, rs2, sw2, s2off, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 = map_extract(read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)), unsigned(s2off), unsigned(sz));
let result : bits(32) = xor_vec(op1, op2);
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
function clause mexecute(MXORI(rd, rw, rs1, sw1, s1off, imm16, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(sz));
let op2 : bits(32) = sail_zero_extend(imm16, 32);
let result : bits(32) = xor_vec(op1, op2);
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
# 4.13.8 NOT
Done — .F supported
function clause mexecute(MNOT(rd, rw, rs, sw, soff, sz, set_flags)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let op1 = map_extract(read_mapword(mregidx_to_nat(rs), mwordsel_to_nat(sw)), unsigned(soff), unsigned(sz));
let result : bits(32) = not_vec(op1) & sail_mask(32, sail_ones(unsigned(sz)));
if set_flags then {
map_set_flags_logic(result)
};
let existing = read_mapword(rd_idx, rw_idx);
let mask : bits(32) = sail_mask(32, sail_ones(unsigned(sz)));
write_mapword(rd_idx, rw_idx, (existing & not_vec(mask)) | result);
RETIRE_SUCCESS
}
# 4.13.9 SHL, SHLI, SHR, SHRI
Done — 4B mode. .F, .CD supported
function clause mexecute(MSHL(rd, rw, rs1, sw1, s1off, s1sz, rs2, sw2, s2off, s2sz, set_flags, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let src_val = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(s1sz));
let shift_val = map_extract(
read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)),
unsigned(s2off),
unsigned(s2sz),
);
let k : nat = unsigned(shift_val);
let src_size : nat = unsigned(s1sz);
let m : int = k + src_size;
if clear_dest then {
write_mapword(rd_idx, rw_idx, 0x00000000)
};
if m > 0 & m <= 32 then {
let shifted : bits(32) = sail_shiftleft(src_val, k);
let existing = read_mapword(rd_idx, rw_idx);
let write_mask : bits(32) = sail_shiftleft(sail_mask(32, sail_ones(src_size)), k);
let result = (existing & not_vec(write_mask)) | (shifted & write_mask);
write_mapword(rd_idx, rw_idx, result);
if set_flags then {
map_set_flags_logic(shifted)
}
} else {
if set_flags then {
mflag_z = true;
mflag_n = false;
mflag_c = false;
mflag_v = false
}
};
RETIRE_SUCCESS
}
function clause mexecute(MSHLI(rd, rw, rs1, sw1, s1off, s1sz, shift_imm, set_flags, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let src_val = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(s1sz));
let k : nat = unsigned(shift_imm);
let src_size : nat = unsigned(s1sz);
let m : int = k + src_size;
if clear_dest then {
write_mapword(rd_idx, rw_idx, 0x00000000)
};
if m > 0 & m <= 32 then {
let shifted : bits(32) = sail_shiftleft(src_val, k);
let existing = read_mapword(rd_idx, rw_idx);
let write_mask : bits(32) = sail_shiftleft(sail_mask(32, sail_ones(src_size)), k);
let result = (existing & not_vec(write_mask)) | (shifted & write_mask);
write_mapword(rd_idx, rw_idx, result);
if set_flags then {
map_set_flags_logic(shifted)
}
} else {
if set_flags then {
mflag_z = true;
mflag_n = false;
mflag_c = false;
mflag_v = false
}
};
RETIRE_SUCCESS
}
function clause mexecute(MSHR(rd, rw, rs1, sw1, s1off, s1sz, rs2, sw2, s2off, s2sz, set_flags, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let src_val = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(s1sz));
let shift_val = map_extract(
read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)),
unsigned(s2off),
unsigned(s2sz),
);
let k : nat = unsigned(shift_val);
let src_size : nat = unsigned(s1sz);
let m : int = src_size - k;
if clear_dest then {
write_mapword(rd_idx, rw_idx, 0x00000000)
};
if m > 0 then {
let shifted : bits(32) = sail_shiftright(src_val, k);
let existing = read_mapword(rd_idx, rw_idx);
assert(m > 0);
let write_mask : bits(32) = sail_mask(32, sail_ones(m));
let result = (existing & not_vec(write_mask)) | (shifted & write_mask);
write_mapword(rd_idx, rw_idx, result);
if set_flags then {
map_set_flags_logic(shifted)
}
} else {
if set_flags then {
mflag_z = true;
mflag_n = false;
mflag_c = false;
mflag_v = false
}
};
RETIRE_SUCCESS
}
function clause mexecute(MSHRI(rd, rw, rs1, sw1, s1off, s1sz, shift_imm, set_flags, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let src_val = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(s1sz));
let k : nat = unsigned(shift_imm);
let src_size : nat = unsigned(s1sz);
let m : int = src_size - k;
if clear_dest then {
write_mapword(rd_idx, rw_idx, 0x00000000)
};
if m > 0 then {
let shifted : bits(32) = sail_shiftright(src_val, k);
let existing = read_mapword(rd_idx, rw_idx);
assert(m > 0);
let write_mask : bits(32) = sail_mask(32, sail_ones(m));
let result = (existing & not_vec(write_mask)) | (shifted & write_mask);
write_mapword(rd_idx, rw_idx, result);
if set_flags then {
map_set_flags_logic(shifted)
}
} else {
if set_flags then {
mflag_z = true;
mflag_n = false;
mflag_c = false;
mflag_v = false
}
};
RETIRE_SUCCESS
}
# 4.13.10 CONCAT
Done — .CD supported
function clause mexecute(MCONCAT(rd, rw, doff, rs1, sw1, s1off, s1sz, rs2, sw2, s2off, s2sz, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let part1 = map_extract(read_mapword(mregidx_to_nat(rs1), mwordsel_to_nat(sw1)), unsigned(s1off), unsigned(s1sz));
let part2 = map_extract(read_mapword(mregidx_to_nat(rs2), mwordsel_to_nat(sw2)), unsigned(s2off), unsigned(s2sz));
let combined : bits(32) = sail_shiftleft(part2, unsigned(s1sz)) | part1;
let total_size : nat = unsigned(s1sz) + unsigned(s2sz);
let dest_off : nat = unsigned(doff);
if clear_dest then {
write_mapword(rd_idx, rw_idx, 0x00000000)
};
let existing = read_mapword(rd_idx, rw_idx);
let write_mask : bits(32) = sail_shiftleft(sail_mask(32, sail_ones(total_size)), dest_off);
let placed : bits(32) = sail_shiftleft(combined & sail_mask(32, sail_ones(total_size)), dest_off);
write_mapword(rd_idx, rw_idx, (existing & not_vec(write_mask)) | placed);
RETIRE_SUCCESS
}
# 4.13.11 MOV, MOVI
Done — .CD supported
function clause mexecute(MMOV(rd, rw, rs, sw, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let rs_idx = mregidx_to_nat(rs);
let sw_idx = mwordsel_to_nat(sw);
if clear_dest then {
write_mapreg(rd_idx, sail_zeros(128))
};
let val32 = read_mapword(rs_idx, sw_idx);
write_mapword(rd_idx, rw_idx, val32);
RETIRE_SUCCESS
}
function clause mexecute(MMOVI(rd, rw, imm32, clear_dest)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
if clear_dest then {
write_mapreg(rd_idx, sail_zeros(128))
};
write_mapword(rd_idx, rw_idx, imm32);
RETIRE_SUCCESS
}
# 4.13.12 FFI
Done — .F supported
function clause mexecute(MFFI(rd, rw, vr, vw, ore, ow, field_size_imm, scan_dir)) = {
let rd_idx = mregidx_to_nat(rd);
let rw_idx = mwordsel_to_nat(rw);
let value = read_mapword(mregidx_to_nat(vr), mwordsel_to_nat(vw));
let start_offset : nat = unsigned(read_mapword(mregidx_to_nat(ore), mwordsel_to_nat(ow)) & 0x0000001F);
let fsz : nat = unsigned(field_size_imm) + 1;
var found : bool = false;
var result_offset : int = 0;
var result_content : bits(32) = 0x00000000;
// Use a simple bit-extraction approach: shift and mask
let field_mask : bits(32) = sail_mask(32, sail_ones(fsz));
if scan_dir then {
// LSb to MSb: scan upward from start_offset
var pos : int = start_offset;
while pos + fsz <= 32 & not_bool(found) do {
let field_val : bits(32) = sail_shiftright(value, pos) & field_mask;
if field_val != 0x00000000 then {
found = true;
result_offset = pos;
result_content = field_val
};
pos = pos + fsz
}
} else {
// MSb to LSb: scan downward from start_offset
var pos : int = start_offset;
while pos >= 0 & not_bool(found) do {
let field_start : int = pos - fsz + 1;
if field_start >= 0 then {
let field_val : bits(32) = sail_shiftright(value, field_start) & field_mask;
if field_val != 0x00000000 then {
found = true;
result_offset = field_start;
result_content = field_val
}
};
pos = pos - fsz
}
};
if found then {
let offset_bits : bits(32) = get_slice_int(32, result_offset, 0);
let dest_val : bits(32) = sail_shiftleft(result_content & 0x0000000F, 8) | (offset_bits & 0x0000001F);
write_mapword(rd_idx, rw_idx, dest_val);
mflag_z = false
} else {
mflag_z = true
};
RETIRE_SUCCESS
}
# 4.13.13 LD, LDD, LDDI, LDH, LDS, LDSP, LDSPI
Not started — Needs RAM/PMEM model
# 4.13.14 ST, STD, STDI, STH, STS, STSP, STSPI
Not started — Needs RAM/PMEM model
# 4.13.15 JTL
Not started
# 4.13.16 CALL
Not started
# 4.13.17 RET
Not started
# 4.13.18 BR, BRI, BRBTST
Done — All 11 condition codes
function clause mexecute(MBR(cc, rs, sw)) = {
if eval_mcond(cc) then {
let target = read_mapword(mregidx_to_nat(rs), mwordsel_to_nat(sw));
mpc = sail_mask(16, target)
};
RETIRE_SUCCESS
}
function clause mexecute(MBRI(cc, offset)) = {
if eval_mcond(cc) then {
mpc = mpc + offset
};
RETIRE_SUCCESS
}
function clause mexecute(MBRBTST(btcc, rs, sw, bit_offset, target)) = {
let word = read_mapword(mregidx_to_nat(rs), mwordsel_to_nat(sw));
let bit_val = (sail_shiftright(word, unsigned(bit_offset)) & 0x00000001) == 0x00000001;
let take_branch : bool = match btcc {
MBT_CLR => not_bool(bit_val),
MBT_SET => bit_val,
};
if take_branch then {
mpc = target
};
RETIRE_SUCCESS
}
# 4.13.19 HASH
Not started — Needs LFLAG
# 4.13.20 LKP, LKPLPM, LKPT, LKPTI
Not started — Needs LFLAG, TCAM model
# 4.13.21 SYNC, SYNCALL
Not started — Needs LFLAG
# 4.13.22 HALT
Done
function clause mexecute(MHALT()) = {
map_halted = true;
RETIRE_HALT
}
# 4.13.23–25 CP, CHKSUM, SEND
Not started — Needs frame memory model
# 4.13.26–30 COUNTER, METER, CAS, BW, DLB
Not started — Atomic operations
# 4.13.31–54 Misc (LDRTC..MCDONE)
Not started
# 4.13.51 NOP
Done
function clause mexecute(MNOP()) = RETIRE_SUCCESS
Sail semantics are auto-generated from the formal model. See the source repository for the full model.