Skip to content

Commit

Permalink
Use separate newtypes for vector registers
Browse files Browse the repository at this point in the history
  • Loading branch information
@nwf
nwf committed Dec 13, 2024
1 parent 087f33f commit b96a5b5
Show file tree
Hide file tree
Showing 11 changed files with 335 additions and 326 deletions.
200 changes: 100 additions & 100 deletions model/riscv_insts_vext_arith.sail
View file

Large diffs are not rendered by default.

106 changes: 53 additions & 53 deletions model/riscv_insts_vext_fp.sail
View file

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions model/riscv_insts_vext_fp_red.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
/* ******************************************************************************* */

/* ********************** OPFVV (Floating-Point Reduction) *********************** */
union clause ast = RFVVTYPE : (rfvvfunct6, bits(1), regidx, regidx, regidx)
union clause ast = RFVVTYPE : (rfvvfunct6, bits(1), vregidx, vregidx, vregidx)

mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = {
FVV_VFREDOSUM <-> 0b000011,
Expand All @@ -24,9 +24,9 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = {
}

mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
<-> encdec_rfvvfunct6(funct6) @ vm @ encdec_reg(vs2) @ encdec_reg(vs1) @ 0b001 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> encdec_rfvvfunct6(funct6) @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b001 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), vregidx, vregidx, vregidx, int('n), int('m), int('p)) -> Retired
function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
let rm_3b = fcsr[FRM];
let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */
Expand All @@ -40,7 +40,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
let 'd = num_elem_vd;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, zvreg);
let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd);
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
Expand All @@ -66,7 +66,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
RETIRE_SUCCESS
}

val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), vregidx, vregidx, vregidx, int('n), int('m), int('p)) -> Retired
function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
let rm_3b = fcsr[FRM];
let SEW_widen = SEW * 2;
Expand All @@ -83,7 +83,7 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow
let 'm = SEW;
let 'o = SEW_widen;

let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, zvreg);
let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd);
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_fp_utils.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,15 +23,15 @@ function valid_fp_op(SEW, rm_3b) = {
}

/* a. Normal check for floating-point instructions */
val illegal_fp_normal : (regidx, bits(1), {8, 16, 32, 64}, bits(3)) -> bool
val illegal_fp_normal : (vregidx, bits(1), {8, 16, 32, 64}, bits(3)) -> bool
function illegal_fp_normal(vd, vm, SEW, rm_3b) = {
not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b))
}

/* b. Masked check for floating-point instructions encoded with vm = 0 */
val illegal_fp_vd_masked : (regidx, {8, 16, 32, 64}, bits(3)) -> bool
val illegal_fp_vd_masked : (vregidx, {8, 16, 32, 64}, bits(3)) -> bool
function illegal_fp_vd_masked(vd, SEW, rm_3b) = {
not(valid_vtype()) | vd == zreg | not(valid_fp_op(SEW, rm_3b))
not(valid_vtype()) | vd == zvreg | not(valid_fp_op(SEW, rm_3b))
}

/* c. Unmasked check for floating-point instructions encoded with vm = 1 */
Expand All @@ -41,7 +41,7 @@ function illegal_fp_vd_unmasked(SEW, rm_3b) = {
}

/* d. Variable width check for floating-point widening/narrowing instructions */
val illegal_fp_variable_width : (regidx, bits(1), {8, 16, 32, 64}, bits(3), int, int) -> bool
val illegal_fp_variable_width : (vregidx, bits(1), {8, 16, 32, 64}, bits(3), int, int) -> bool
function illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_new, LMUL_pow_new) = {
not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) |
not(valid_eew_emul(SEW_new, LMUL_pow_new))
Expand Down
12 changes: 6 additions & 6 deletions model/riscv_insts_vext_fp_vm.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

/* ******************************* OPFVV (VVMTYPE) ******************************* */
/* FVVM instructions' destination is a mask register */
union clause ast = FVVMTYPE : (fvvmfunct6, bits(1), regidx, regidx, regidx)
union clause ast = FVVMTYPE : (fvvmfunct6, bits(1), vregidx, vregidx, vregidx)

mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = {
FVVM_VMFEQ <-> 0b011000,
Expand All @@ -23,7 +23,7 @@ mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = {
}

mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
<-> encdec_fvvmfunct6(funct6) @ vm @ encdec_reg(vs2) @ encdec_reg(vs1) @ 0b001 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> encdec_fvvmfunct6(funct6) @ vm @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b001 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
let rm_3b = fcsr[FRM];
Expand All @@ -37,7 +37,7 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd);
Expand Down Expand Up @@ -74,7 +74,7 @@ mapping clause assembly = FVVMTYPE(funct6, vm, vs2, vs1, vd)

/* ******************************* OPFVF (VFMTYPE) ******************************* */
/* VFM instructions' destination is a mask register */
union clause ast = FVFMTYPE : (fvfmfunct6, bits(1), regidx, regidx, regidx)
union clause ast = FVFMTYPE : (fvfmfunct6, bits(1), vregidx, regidx, vregidx)

mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = {
VFM_VMFEQ <-> 0b011000,
Expand All @@ -86,7 +86,7 @@ mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = {
}

mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
<-> encdec_fvfmfunct6(funct6) @ vm @ encdec_reg(vs2) @ encdec_reg(rs1) @ 0b101 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> encdec_fvfmfunct6(funct6) @ vm @ encdec_vreg(vs2) @ encdec_reg(rs1) @ 0b101 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
let rm_3b = fcsr[FRM];
Expand All @@ -100,7 +100,7 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let rs1_val : bits('m) = get_scalar_fp(rs1, 'm);
let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd);
Expand Down
46 changes: 23 additions & 23 deletions model/riscv_insts_vext_mask.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
/* ******************************************************************************* */

/* ******************************* OPMVV (MMTYPE) ******************************** */
union clause ast = MMTYPE : (mmfunct6, regidx, regidx, regidx)
union clause ast = MMTYPE : (mmfunct6, vregidx, vregidx, vregidx)

mapping encdec_mmfunct6 : mmfunct6 <-> bits(6) = {
MM_VMAND <-> 0b011001,
Expand All @@ -26,7 +26,7 @@ mapping encdec_mmfunct6 : mmfunct6 <-> bits(6) = {
}

mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
<-> encdec_mmfunct6(funct6) @ 0b1 @ encdec_reg(vs2) @ encdec_reg(vs1) @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> encdec_mmfunct6(funct6) @ 0b1 @ encdec_vreg(vs2) @ encdec_vreg(vs1) @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
let SEW = get_sew();
Expand Down Expand Up @@ -80,10 +80,10 @@ mapping clause assembly = MMTYPE(funct6, vs2, vs1, vd)
<-> mmtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1)

/* ************************* OPMVV (vpopc in VWXUNARY0) ************************** */
union clause ast = VCPOP_M : (bits(1), regidx, regidx)
union clause ast = VCPOP_M : (bits(1), vregidx, regidx)

mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V)
<-> 0b010000 @ vm @ encdec_reg(vs2) @ 0b10000 @ 0b010 @ encdec_reg(rd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010000 @ vm @ encdec_vreg(vs2) @ 0b10000 @ 0b010 @ encdec_reg(rd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VCPOP_M(vm, vs2, rd)) = {
let SEW = get_sew();
Expand All @@ -95,7 +95,7 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);

let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
Expand All @@ -114,10 +114,10 @@ mapping clause assembly = VCPOP_M(vm, vs2, rd)
<-> "vpopc.m" ^ spc() ^ reg_name(rd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* ************************* OPMVV (vfirst in VWXUNARY0) ************************* */
union clause ast = VFIRST_M : (bits(1), regidx, regidx)
union clause ast = VFIRST_M : (bits(1), vregidx, regidx)

mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V)
<-> 0b010000 @ vm @ encdec_reg(vs2) @ 0b10001 @ 0b010 @ encdec_reg(rd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010000 @ vm @ encdec_vreg(vs2) @ 0b10001 @ 0b010 @ encdec_reg(rd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VFIRST_M(vm, vs2, rd)) = {
let SEW = get_sew();
Expand All @@ -129,7 +129,7 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);

let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
Expand All @@ -150,10 +150,10 @@ mapping clause assembly = VFIRST_M(vm, vs2, rd)
<-> "vfirst.m" ^ spc() ^ reg_name(rd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* ************************** OPMVV (vmsbf in VMUNARY0) ************************** */
union clause ast = VMSBF_M : (bits(1), regidx, regidx)
union clause ast = VMSBF_M : (bits(1), vregidx, vregidx)

mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_reg(vs2) @ 0b00001 @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_vreg(vs2) @ 0b00001 @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VMSBF_M(vm, vs2, vd)) = {
let SEW = get_sew();
Expand All @@ -166,7 +166,7 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd);

Expand All @@ -190,10 +190,10 @@ mapping clause assembly = VMSBF_M(vm, vs2, vd)
<-> "vmsbf.m" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* ************************** OPMVV (vmsif in VMUNARY0) ************************** */
union clause ast = VMSIF_M : (bits(1), regidx, regidx)
union clause ast = VMSIF_M : (bits(1), vregidx, vregidx)

mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_reg(vs2) @ 0b00011 @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_vreg(vs2) @ 0b00011 @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VMSIF_M(vm, vs2, vd)) = {
let SEW = get_sew();
Expand All @@ -206,7 +206,7 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd);

Expand All @@ -230,10 +230,10 @@ mapping clause assembly = VMSIF_M(vm, vs2, vd)
<-> "vmsif.m" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* ************************** OPMVV (vmsof in VMUNARY0) ************************** */
union clause ast = VMSOF_M : (bits(1), regidx, regidx)
union clause ast = VMSOF_M : (bits(1), vregidx, vregidx)

mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_reg(vs2) @ 0b00010 @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_vreg(vs2) @ 0b00010 @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VMSOF_M(vm, vs2, vd)) = {
let SEW = get_sew();
Expand All @@ -246,7 +246,7 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd);

Expand Down Expand Up @@ -274,10 +274,10 @@ mapping clause assembly = VMSOF_M(vm, vs2, vd)
<-> "vmsof.m" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* ************************** OPMVV (viota in VMUNARY0) ************************** */
union clause ast = VIOTA_M : (bits(1), regidx, regidx)
union clause ast = VIOTA_M : (bits(1), vregidx, vregidx)

mapping clause encdec = VIOTA_M(vm, vs2, vd) if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_reg(vs2) @ 0b10000 @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ encdec_vreg(vs2) @ 0b10000 @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VIOTA_M(vm, vs2, vd)) = {
let SEW = get_sew();
Expand All @@ -290,7 +290,7 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2);
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);

Expand All @@ -314,10 +314,10 @@ mapping clause assembly = VIOTA_M(vm, vs2, vd)
<-> "viota.m" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ maybe_vmask(vm)

/* *************************** OPMVV (vid in VMUNARY0) *************************** */
union clause ast = VID_V : (bits(1), regidx)
union clause ast = VID_V : (bits(1), vregidx)

mapping clause encdec = VID_V(vm, vd) if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ encdec_reg(vd) @ 0b1010111 if extensionEnabled(Ext_V)
<-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ encdec_vreg(vd) @ 0b1010111 if extensionEnabled(Ext_V)

function clause execute(VID_V(vm, vd)) = {
let SEW = get_sew();
Expand All @@ -329,7 +329,7 @@ function clause execute(VID_V(vm, vd)) = {
let 'n = num_elem;
let 'm = SEW;

let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zreg);
let vm_val : vector('n, bool) = read_vmask(num_elem, vm, zvreg);
let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);

let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
Expand Down
Loading

0 comments on commit b96a5b5

Please sign in to comment.