From f6ca84063b232673570e4a45f5582e464cb82b65 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 16 Sep 2024 05:16:43 +0800 Subject: [PATCH 01/14] Add zvbc extension --- Makefile | 2 + model/riscv_insts_zvbc.sail | 150 ++++++++++++++++++++++++++++++++++++ 2 files changed, 152 insertions(+) create mode 100644 model/riscv_insts_zvbc.sail diff --git a/Makefile b/Makefile index f19b6d591..dbfb1dea3 100644 --- a/Makefile +++ b/Makefile @@ -64,6 +64,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail SAIL_DEFAULT_INST += riscv_insts_zicbom.sail SAIL_DEFAULT_INST += riscv_insts_zicboz.sail +SAIL_DEFAULT_INST += riscv_insts_zvbc.sail + SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail diff --git a/model/riscv_insts_zvbc.sail b/model/riscv_insts_zvbc.sail new file mode 100644 index 000000000..9d5f7a3a4 --- /dev/null +++ b/model/riscv_insts_zvbc.sail @@ -0,0 +1,150 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +enum clause extension = Ext_Zvbc +function clause extensionEnabled(Ext_Zvbc) = true + +union clause ast = VCLMUL_VV : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VCLMUL_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) + <-> 0b001100 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + +function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let VLEN = unsigned(vlenb) * 8; + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + let 'num_elem_single : int = VLEN / SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + foreach (n from 0 to (SEW - 1)) + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] << n); + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; +}; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VCLMUL_VX : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VCLMUL_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) + <-> 0b001100 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + +function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + foreach (n from 0 to (SEW - 1)) + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val << n); + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VCLMULH_VV : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VCLMULH_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) + <-> 0b001101 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + +function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let VLEN = unsigned(vlenb) * 8; + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + let 'num_elem_single : int = VLEN / SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + foreach (n from 0 to (SEW - 1)) + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] >> n); + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VCLMULH_VX : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VCLMULH_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) + <-> 0b001101 @ vm @ vs2 @ rs1 @ 0b111 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + +function clause execute (VCLMULH_VX(vm, vs2, rs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + foreach (n from 0 to (SEW - 1)) + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val >> n); + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + }; + vstart = zeros(); + RETIRE_SUCCESS +} From c79262f4ab928928f5efa6881c778bb4c8fdcbae Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 16 Sep 2024 18:14:52 +0800 Subject: [PATCH 02/14] Add zvbc extension --- model/riscv_insts_zvbc.sail | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/model/riscv_insts_zvbc.sail b/model/riscv_insts_zvbc.sail index 9d5f7a3a4..e5071b465 100644 --- a/model/riscv_insts_zvbc.sail +++ b/model/riscv_insts_zvbc.sail @@ -9,11 +9,19 @@ enum clause extension = Ext_Zvbc function clause extensionEnabled(Ext_Zvbc) = true +mapping vm_name : bits(1) <-> string = { + 0b0 <-> "0", + 0b1 <-> "1" +} + union clause ast = VCLMUL_VV : (bits(1), regidx, regidx, regidx) mapping clause encdec = VCLMUL_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) <-> 0b001100 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) +mapping clause assembly = VCLMUL_VV (vm, vs2, vs1, vd) + <-> "vclmul.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) + function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); @@ -26,7 +34,7 @@ function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { var result : vector('n, dec, bits('m)) = undefined; var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); @@ -50,6 +58,9 @@ union clause ast = VCLMUL_VX : (bits(1), regidx, regidx, regidx) mapping clause encdec = VCLMUL_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) <-> 0b001100 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) +mapping clause assembly = VCLMUL_VX (vm, vs2, rs1, vd) + <-> "vclmul.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) + function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); @@ -60,7 +71,7 @@ function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { var result : vector('n, dec, bits('m)) = undefined; var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); @@ -84,6 +95,9 @@ union clause ast = VCLMULH_VV : (bits(1), regidx, regidx, regidx) mapping clause encdec = VCLMULH_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) <-> 0b001101 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) +mapping clause assembly = VCLMULH_VV (vm, vs2, vs1, vd) + <-> "vclmulh.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) + function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); @@ -96,7 +110,7 @@ function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { var result : vector('n, dec, bits('m)) = undefined; var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); @@ -107,7 +121,7 @@ function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] >> n); + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] >> (SEW - n)); write_vreg(num_elem, SEW, LMUL_pow, vd, result); }; }; @@ -118,7 +132,10 @@ function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { union clause ast = VCLMULH_VX : (bits(1), regidx, regidx, regidx) mapping clause encdec = VCLMULH_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) - <-> 0b001101 @ vm @ vs2 @ rs1 @ 0b111 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + <-> 0b001101 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) + +mapping clause assembly = VCLMULH_VX (vm, vs2, rs1, vd) + <-> "vclmulh.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) function clause execute (VCLMULH_VX(vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -130,7 +147,7 @@ function clause execute (VCLMULH_VX(vm, vs2, rs1, vd)) = { var result : vector('n, dec, bits('m)) = undefined; var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); @@ -141,7 +158,7 @@ function clause execute (VCLMULH_VX(vm, vs2, rs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val >> n); + if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val >> (SEW - n)); write_vreg(num_elem, SEW, LMUL_pow, vd, result); }; }; From 601a58cfacf98b637d5f92d0901c7a6af99fed6a Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Tue, 17 Sep 2024 02:42:18 +0800 Subject: [PATCH 03/14] Add zvbb extension --- model/riscv_insts_zvbb.sail | 120 ++++++++++++++++++++++++++++++++++++ model/riscv_insts_zvbc.sail | 2 +- 2 files changed, 121 insertions(+), 1 deletion(-) create mode 100644 model/riscv_insts_zvbb.sail diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail new file mode 100644 index 000000000..b2846d22a --- /dev/null +++ b/model/riscv_insts_zvbb.sail @@ -0,0 +1,120 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +enum clause extension = Ext_Zvbb +function clause extensionEnabled(Ext_Zvbb) = true + +union clause ast = VANDN_VV : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VANDN_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b000001 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VCLMUL_VV (vm, vs2, vs1, vd) + <-> "vandn.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) + +function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + result[i] = vs2_val[i] & ~vs1_val[i]; + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VANDN_VX : (bits(1), regidx, regidx, regidx) + +mapping clause encdec = VANDN_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b000001 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VCLMUL_VX (vm, vs2, rs1, vd) + <-> "vandn.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(rs1) ^ sep() ^ vm_name(vm) + +function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let rs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, rs1); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + result[i] = vs2_val[i] & ~rs1_val[i]; + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VBREV_V : (bits(1), regidx, regidx) + +mapping clause encdec = VBREV_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b010010 @ vm @ vs2 @ 01010 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VBREV_V (vm, vs2, vd) + <-> "vbrev.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vm_name(vm) + +function clause execute (VBREV_V(vm, vs2, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + result[i] = reverse(vs2_val[i]); + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VBREV8_V : (bits(1), regidx, regidx) + +mapping clause encdec = VBREV8_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b010010 @ vm @ vs2 @ 01000 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VBREV8_V (vm, vs2, vd) + <-> "vbrev8.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vm_name(vm) + +function clause execute (VBREV8_V (vm, vs2, vd)) = { + +}; diff --git a/model/riscv_insts_zvbc.sail b/model/riscv_insts_zvbc.sail index e5071b465..6b98216ac 100644 --- a/model/riscv_insts_zvbc.sail +++ b/model/riscv_insts_zvbc.sail @@ -48,7 +48,7 @@ function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] << n); write_vreg(num_elem, SEW, LMUL_pow, vd, result); }; -}; + }; vstart = zeros(); RETIRE_SUCCESS } From 923153ac02e6a383d0c2a4169a9df182cb935dec Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 23 Sep 2024 01:03:40 +0800 Subject: [PATCH 04/14] Add zvbb extenson's vwsll --- Makefile | 60 +----------------- model/riscv_insts_zvbb.sail | 119 ++++++++++++++++++++---------------- 2 files changed, 71 insertions(+), 108 deletions(-) diff --git a/Makefile b/Makefile index dbfb1dea3..ac7d38165 100644 --- a/Makefile +++ b/Makefile @@ -64,7 +64,7 @@ SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail SAIL_DEFAULT_INST += riscv_insts_zicbom.sail SAIL_DEFAULT_INST += riscv_insts_zicboz.sail -SAIL_DEFAULT_INST += riscv_insts_zvbc.sail +SAIL_DEFAULT_INST += riscv_insts_zvbb.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail @@ -130,8 +130,6 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(S SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS)) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS)) -PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml) - SAIL_FLAGS += --require-version 0.18 SAIL_FLAGS += --strict-var SAIL_FLAGS += -dno_cast @@ -210,7 +208,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) .PHONY: -all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) +all: c_emulator/riscv_sim_$(ARCH) .PHONY: all # the following ensures empty sail-generated .c files don't hang around and @@ -232,44 +230,12 @@ riscv.smt_model: $(SAIL_SRCS) cgen: $(SAIL_SRCS) model/main.sail $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile - mkdir -p generated_definitions/ocaml/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS) - -# cp -f is required because the generated_definitions/ocaml/$ARCH/*.ml files can -# be read-only, which would otherwise make subsequent builds fail. -ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile - mkdir -p ocaml_emulator/_sbuild - cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild - cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild - cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native - -ocaml_emulator/_sbuild/coverage.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile - mkdir -p ocaml_emulator/_sbuild - cp $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild - cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild - cp ocaml_emulator/_tags.bisect ocaml_emulator/_sbuild/_tags - cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native - -ocaml_emulator/riscv_ocaml_sim_$(ARCH): ocaml_emulator/_sbuild/riscv_ocaml_sim.native - rm -f $@ && cp -L $^ $@ && rm -f $^ - -ocaml_emulator/coverage_$(ARCH): ocaml_emulator/_sbuild/coverage.native - rm -f ocaml_emulator/riscv_ocaml_sim_$(ARCH) && cp -L $^ ocaml_emulator/riscv_ocaml_sim_$(ARCH) # since the test scripts runs this file - rm -rf bisect*.out bisect ocaml_emulator/coverage_$(ARCH) $^ - ./test/run_tests.sh # this will generate bisect*.out files in this directory - mkdir ocaml_emulator/bisect && mv bisect*.out bisect/ - mkdir ocaml_emulator/coverage_$(ARCH) && bisect-ppx-report -html ocaml_emulator/coverage_$(ARCH)/ -I ocaml_emulator/_sbuild/ bisect/bisect*.out - cloc: cloc --by-file --force-lang C,sail $(SAIL_SRCS) gcovr: gcovr -r . --html --html-detail -o index.html -ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml - ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ - c_preserve_fns=-c_preserve _set_Misa_C generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile @@ -286,8 +252,6 @@ $(SOFTFLOAT_LIBS): # convenience target .PHONY: csim csim: c_emulator/riscv_sim_$(ARCH) -.PHONY: osim -osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH) .PHONY: rvfi rvfi: c_emulator/riscv_rvfi_$(ARCH) @@ -472,29 +436,12 @@ sail-riscv.install: FORCE echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install -opam-build: - $(MAKE) ARCH=64 c_emulator/riscv_sim_RV64 - $(MAKE) ARCH=32 c_emulator/riscv_sim_RV32 - $(MAKE) riscv_rmem - -opam-install: - if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi - mkdir -p $(INSTALL_DIR)/bin - cp c_emulator/riscv_sim_RV64 $(INSTALL_DIR)/bin - cp c_emulator/riscv_sim_RV32 $(INSTALL_DIR)/bin - -opam-uninstall: - if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi - rm $(INSTALL_DIR)/bin/riscv_sim_RV64 - rm $(INSTALL_DIR)/bin/riscv_sim_RV32 - clean: - -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* + -rm -rf generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* -$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64 - -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda -rm -f z3_problems -Holmake cleanAll @@ -502,4 +449,3 @@ clean: -rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.vos handwritten_support/mem_metadata.vok handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux -rm -f sail_doc/riscv_RV32.json -rm -f sail_doc/riscv_RV64.json - ocamlbuild -clean diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index b2846d22a..523daf85c 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -9,112 +9,129 @@ enum clause extension = Ext_Zvbb function clause extensionEnabled(Ext_Zvbb) = true -union clause ast = VANDN_VV : (bits(1), regidx, regidx, regidx) +mapping vm_name : bits(1) <-> string = { + 0b0 <-> "0", + 0b1 <-> "1" +} + +union clause ast = VWSLL_VV : (bits(1), regidx, regidx, regidx) -mapping clause encdec = VANDN_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbb) - <-> 0b000001 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) +mapping clause encdec = VWSLL_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b110101 @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) -mapping clause assembly = VCLMUL_VV (vm, vs2, vs1, vd) - <-> "vandn.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) +mapping clause assembly = VWSLL_VV (vm, vs2, vs1, vd) + <-> "vwsll.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) -function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { +function clause execute (VWSLL_VV(vm, vs2, vs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + let SEW_widen = SEW * 2; + let LMUL_pow_widen = LMUL_pow + 1; let 'n = num_elem; let 'm = SEW; + let 'o = SEW_widen; - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + var result : vector('n, dec, bits('o)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + let vs1_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - result[i] = vs2_val[i] & ~vs1_val[i]; + let SEW_widen_bits = to_bits(SEW_widen, 'o); + let vs1_val : bits('o) = zero_extend(vs1_val_vec[i]); + let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); + result[i] = vs2_val << (vs1_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); }; vstart = zeros(); RETIRE_SUCCESS } -union clause ast = VANDN_VX : (bits(1), regidx, regidx, regidx) +union clause ast = VWSLL_VX : (bits(1), regidx, regidx, regidx) -mapping clause encdec = VANDN_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbb) - <-> 0b000001 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) +mapping clause encdec = VWSLL_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b110101 @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) -mapping clause assembly = VCLMUL_VX (vm, vs2, rs1, vd) - <-> "vandn.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(rs1) ^ sep() ^ vm_name(vm) +mapping clause assembly = VWSLL_VX (vm, vs2, rs1, vd) + <-> "vwsll.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) -function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { +function clause execute (VWSLL_VX(vm, vs2, rs1, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + let SEW_widen = SEW * 2; + let LMUL_pow_widen = LMUL_pow + 1; let 'n = num_elem; let 'm = SEW; + let 'o = SEW_widen; - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let rs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, rs1); + var result : vector('n, dec, bits('o)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + let rs1_val : bits('o) = zero_extend(get_scalar(rs1, SEW)); + let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - result[i] = vs2_val[i] & ~rs1_val[i]; + let SEW_widen_bits = to_bits(SEW_widen, 'o); + let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); + result[i] = vs2_val << (rs1_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); }; vstart = zeros(); RETIRE_SUCCESS } -union clause ast = VBREV_V : (bits(1), regidx, regidx) +union clause ast = VWSLL_VI : (bits(1), regidx, bits(5), regidx) -mapping clause encdec = VBREV_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) - <-> 0b010010 @ vm @ vs2 @ 01010 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) +mapping clause encdec = VWSLL_VI (vm, vs2, uimm, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b110101 @ vm @ vs2 @ uimm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) -mapping clause assembly = VBREV_V (vm, vs2, vd) - <-> "vbrev.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vm_name(vm) +mapping clause assembly = VWSLL_VI (vm, vs2, uimm, vd) + <-> "vwsll.vi" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ hex_bits_signed_5(uimm) ^ sep() ^ vm_name(vm) -function clause execute (VBREV_V(vm, vs2, vd)) = { +function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); + let num_elem = get_num_elem(LMUL_pow, SEW); + let SEW_widen = SEW * 2; + let LMUL_pow_widen = LMUL_pow + 1; let 'n = num_elem; let 'm = SEW; + let 'o = SEW_widen; - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let uimm_val: bits('o) = zero_extend(uimm); - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + var mask : vector('n, dec, bool) = undefined; + var result : vector('n, dec, bits('o)) = undefined; + let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + + (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - result[i] = reverse(vs2_val[i]); + let SEW_widen_bits = to_bits(SEW_widen, 'o); + let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); + result[i] = vs2_val << (uimm_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); }; vstart = zeros(); RETIRE_SUCCESS } - -union clause ast = VBREV8_V : (bits(1), regidx, regidx) - -mapping clause encdec = VBREV8_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) - <-> 0b010010 @ vm @ vs2 @ 01000 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) - -mapping clause assembly = VBREV8_V (vm, vs2, vd) - <-> "vbrev8.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vm_name(vm) - -function clause execute (VBREV8_V (vm, vs2, vd)) = { - -}; From d253911f578600ccfa81fde2e435c1b7950431fa Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 23 Sep 2024 01:18:36 +0800 Subject: [PATCH 05/14] Add zvbb extenson's vwsll --- model/riscv_insts_zvbc.sail | 167 ------------------------------------ 1 file changed, 167 deletions(-) delete mode 100644 model/riscv_insts_zvbc.sail diff --git a/model/riscv_insts_zvbc.sail b/model/riscv_insts_zvbc.sail deleted file mode 100644 index 6b98216ac..000000000 --- a/model/riscv_insts_zvbc.sail +++ /dev/null @@ -1,167 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -enum clause extension = Ext_Zvbc -function clause extensionEnabled(Ext_Zvbc) = true - -mapping vm_name : bits(1) <-> string = { - 0b0 <-> "0", - 0b1 <-> "1" -} - -union clause ast = VCLMUL_VV : (bits(1), regidx, regidx, regidx) - -mapping clause encdec = VCLMUL_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) - <-> 0b001100 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) - -mapping clause assembly = VCLMUL_VV (vm, vs2, vs1, vd) - <-> "vclmul.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) - -function clause execute (VCLMUL_VV(vm, vs2, vs1, vd)) = { - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let VLEN = unsigned(vlenb) * 8; - let num_elem = get_num_elem(LMUL_pow, SEW); - - let 'n = num_elem; - let 'm = SEW; - let 'num_elem_single : int = VLEN / SEW; - - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - - let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] << n); - write_vreg(num_elem, SEW, LMUL_pow, vd, result); - }; - }; - vstart = zeros(); - RETIRE_SUCCESS -} - -union clause ast = VCLMUL_VX : (bits(1), regidx, regidx, regidx) - -mapping clause encdec = VCLMUL_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) - <-> 0b001100 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) - -mapping clause assembly = VCLMUL_VX (vm, vs2, rs1, vd) - <-> "vclmul.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) - -function clause execute (VCLMUL_VX(vm, vs2, rs1, vd)) = { - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); - - let 'n = num_elem; - let 'm = SEW; - - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - - let rs1_val : bits('m) = get_scalar(rs1, SEW); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val << n); - write_vreg(num_elem, SEW, LMUL_pow, vd, result); - }; - }; - vstart = zeros(); - RETIRE_SUCCESS -} - -union clause ast = VCLMULH_VV : (bits(1), regidx, regidx, regidx) - -mapping clause encdec = VCLMULH_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbc) - <-> 0b001101 @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) - -mapping clause assembly = VCLMULH_VV (vm, vs2, vs1, vd) - <-> "vclmulh.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) - -function clause execute (VCLMULH_VV(vm, vs2, vs1, vd)) = { - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let VLEN = unsigned(vlenb) * 8; - let num_elem = get_num_elem(LMUL_pow, SEW); - - let 'n = num_elem; - let 'm = SEW; - let 'num_elem_single : int = VLEN / SEW; - - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - - let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (vs1_val[i] >> (SEW - n)); - write_vreg(num_elem, SEW, LMUL_pow, vd, result); - }; - }; - vstart = zeros(); - RETIRE_SUCCESS -} - -union clause ast = VCLMULH_VX : (bits(1), regidx, regidx, regidx) - -mapping clause encdec = VCLMULH_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbc) - <-> 0b001101 @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbc) - -mapping clause assembly = VCLMULH_VX (vm, vs2, rs1, vd) - <-> "vclmulh.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) - -function clause execute (VCLMULH_VX(vm, vs2, rs1, vd)) = { - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); - - let 'n = num_elem; - let 'm = SEW; - - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - - let rs1_val : bits('m) = get_scalar(rs1, SEW); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - foreach (n from 0 to (SEW - 1)) - if vs2_val[i][n] == bitone then result[i] = result[i] ^ (rs1_val >> (SEW - n)); - write_vreg(num_elem, SEW, LMUL_pow, vd, result); - }; - }; - vstart = zeros(); - RETIRE_SUCCESS -} From d306c71fc502973c0f00266aac6bdb5449190073 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 23 Sep 2024 12:54:30 +0800 Subject: [PATCH 06/14] Add zvbb extenson's vwsll --- Makefile | 58 +++++++++++++++++++++++++++++++++++-- model/riscv_insts_zvbb.sail | 26 ++++++----------- 2 files changed, 65 insertions(+), 19 deletions(-) diff --git a/Makefile b/Makefile index ac7d38165..8e1395f69 100644 --- a/Makefile +++ b/Makefile @@ -130,6 +130,8 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(S SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS)) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS)) +PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml) + SAIL_FLAGS += --require-version 0.18 SAIL_FLAGS += --strict-var SAIL_FLAGS += -dno_cast @@ -208,7 +210,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) .PHONY: -all: c_emulator/riscv_sim_$(ARCH) +all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) .PHONY: all # the following ensures empty sail-generated .c files don't hang around and @@ -230,12 +232,44 @@ riscv.smt_model: $(SAIL_SRCS) cgen: $(SAIL_SRCS) model/main.sail $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail +generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile + mkdir -p generated_definitions/ocaml/$(ARCH) + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS) + +# cp -f is required because the generated_definitions/ocaml/$ARCH/*.ml files can +# be read-only, which would otherwise make subsequent builds fail. +ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile + mkdir -p ocaml_emulator/_sbuild + cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild + cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild + cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native + +ocaml_emulator/_sbuild/coverage.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile + mkdir -p ocaml_emulator/_sbuild + cp $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild + cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild + cp ocaml_emulator/_tags.bisect ocaml_emulator/_sbuild/_tags + cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native + +ocaml_emulator/riscv_ocaml_sim_$(ARCH): ocaml_emulator/_sbuild/riscv_ocaml_sim.native + rm -f $@ && cp -L $^ $@ && rm -f $^ + +ocaml_emulator/coverage_$(ARCH): ocaml_emulator/_sbuild/coverage.native + rm -f ocaml_emulator/riscv_ocaml_sim_$(ARCH) && cp -L $^ ocaml_emulator/riscv_ocaml_sim_$(ARCH) # since the test scripts runs this file + rm -rf bisect*.out bisect ocaml_emulator/coverage_$(ARCH) $^ + ./test/run_tests.sh # this will generate bisect*.out files in this directory + mkdir ocaml_emulator/bisect && mv bisect*.out bisect/ + mkdir ocaml_emulator/coverage_$(ARCH) && bisect-ppx-report -html ocaml_emulator/coverage_$(ARCH)/ -I ocaml_emulator/_sbuild/ bisect/bisect*.out + cloc: cloc --by-file --force-lang C,sail $(SAIL_SRCS) gcovr: gcovr -r . --html --html-detail -o index.html +ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml + ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ + c_preserve_fns=-c_preserve _set_Misa_C generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile @@ -252,6 +286,8 @@ $(SOFTFLOAT_LIBS): # convenience target .PHONY: csim csim: c_emulator/riscv_sim_$(ARCH) +.PHONY: osim +osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH) .PHONY: rvfi rvfi: c_emulator/riscv_rvfi_$(ARCH) @@ -436,12 +472,29 @@ sail-riscv.install: FORCE echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install +opam-build: + $(MAKE) ARCH=64 c_emulator/riscv_sim_RV64 + $(MAKE) ARCH=32 c_emulator/riscv_sim_RV32 + $(MAKE) riscv_rmem + +opam-install: + if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi + mkdir -p $(INSTALL_DIR)/bin + cp c_emulator/riscv_sim_RV64 $(INSTALL_DIR)/bin + cp c_emulator/riscv_sim_RV32 $(INSTALL_DIR)/bin + +opam-uninstall: + if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi + rm $(INSTALL_DIR)/bin/riscv_sim_RV64 + rm $(INSTALL_DIR)/bin/riscv_sim_RV32 + clean: - -rm -rf generated_definitions/c/* generated_definitions/latex/* + -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* -$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64 + -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda -rm -f z3_problems -Holmake cleanAll @@ -449,3 +502,4 @@ clean: -rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.vos handwritten_support/mem_metadata.vok handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux -rm -f sail_doc/riscv_RV32.json -rm -f sail_doc/riscv_RV64.json + ocamlbuild -clean diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index 523daf85c..89b69ec62 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -9,18 +9,13 @@ enum clause extension = Ext_Zvbb function clause extensionEnabled(Ext_Zvbb) = true -mapping vm_name : bits(1) <-> string = { - 0b0 <-> "0", - 0b1 <-> "1" -} - union clause ast = VWSLL_VV : (bits(1), regidx, regidx, regidx) mapping clause encdec = VWSLL_VV (vm, vs2, vs1, vd) if extensionEnabled(Ext_Zvbb) <-> 0b110101 @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) mapping clause assembly = VWSLL_VV (vm, vs2, vs1, vd) - <-> "vwsll.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ vm_name(vm) + <-> "vwsll.vv" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ sep() ^ maybe_vmask(vm) function clause execute (VWSLL_VV(vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -33,14 +28,13 @@ function clause execute (VWSLL_VV(vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - var result : vector('n, dec, bits('o)) = undefined; - var mask : vector('n, dec, bool) = undefined; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); let vs1_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { @@ -61,7 +55,7 @@ mapping clause encdec = VWSLL_VX (vm, vs2, rs1, vd) if extensionEnabled(Ext_Zvbb <-> 0b110101 @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) mapping clause assembly = VWSLL_VX (vm, vs2, rs1, vd) - <-> "vwsll.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ vm_name(vm) + <-> "vwsll.vx" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ sep() ^ maybe_vmask(vm) function clause execute (VWSLL_VX(vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -74,14 +68,13 @@ function clause execute (VWSLL_VX(vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - var result : vector('n, dec, bits('o)) = undefined; - var mask : vector('n, dec, bool) = undefined; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); let rs1_val : bits('o) = zero_extend(get_scalar(rs1, SEW)); let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { @@ -101,7 +94,7 @@ mapping clause encdec = VWSLL_VI (vm, vs2, uimm, vd) if extensionEnabled(Ext_Zvb <-> 0b110101 @ vm @ vs2 @ uimm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) mapping clause assembly = VWSLL_VI (vm, vs2, uimm, vd) - <-> "vwsll.vi" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ hex_bits_signed_5(uimm) ^ sep() ^ vm_name(vm) + <-> "vwsll.vi" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ hex_bits_signed_5(uimm) ^ sep() ^ maybe_vmask(vm) function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let SEW = get_sew(); @@ -117,12 +110,11 @@ function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let uimm_val: bits('o) = zero_extend(uimm); - var mask : vector('n, dec, bool) = undefined; - var result : vector('n, dec, bits('o)) = undefined; let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); - (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { From 9247139ce4a0ca861bb0f37c6331e5261392e2a2 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 25 Sep 2024 10:57:47 +0800 Subject: [PATCH 07/14] Add zvbb extenson's vwsll --- .vscode/settings.json | 5 +++++ model/riscv_insts_zvbb.sail | 20 ++++++++++---------- sail-riscv.install | 2 -- 3 files changed, 15 insertions(+), 12 deletions(-) create mode 100644 .vscode/settings.json delete mode 100644 sail-riscv.install diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..5488acecc --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,5 @@ +{ + "files.watcherExclude": { + "**/target": true + } +} diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index 89b69ec62..6077ad1db 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -29,11 +29,11 @@ function clause execute (VWSLL_VV(vm, vs2, vs1, vd)) = { let 'o = SEW_widen; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -43,7 +43,7 @@ function clause execute (VWSLL_VV(vm, vs2, vs1, vd)) = { let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); result[i] = vs2_val << (vs1_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd, result); }; vstart = zeros(); RETIRE_SUCCESS @@ -69,11 +69,11 @@ function clause execute (VWSLL_VX(vm, vs2, rs1, vd)) = { let 'o = SEW_widen; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('o) = zero_extend(get_scalar(rs1, SEW)); let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -82,7 +82,7 @@ function clause execute (VWSLL_VX(vm, vs2, rs1, vd)) = { let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); result[i] = vs2_val << (rs1_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd, result); }; vstart = zeros(); RETIRE_SUCCESS @@ -99,7 +99,7 @@ mapping clause assembly = VWSLL_VI (vm, vs2, uimm, vd) function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); + let num_elem = get_num_elem(LMUL_pow, SEW); let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; @@ -111,9 +111,9 @@ function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let uimm_val: bits('o) = zero_extend(uimm); let vs2_val_vec : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow, vd); + let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val); var result = initial_result; foreach (i from 0 to (num_elem - 1)) { @@ -122,7 +122,7 @@ function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { let vs2_val : bits('o) = zero_extend(vs2_val_vec[i]); result[i] = vs2_val << (uimm_val & zero_extend(SEW_widen_bits - 1)); }; - write_vreg(num_elem, SEW_widen, LMUL_pow, vd, result); + write_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd, result); }; vstart = zeros(); RETIRE_SUCCESS diff --git a/sail-riscv.install b/sail-riscv.install deleted file mode 100644 index 7a539dfb5..000000000 --- a/sail-riscv.install +++ /dev/null @@ -1,2 +0,0 @@ -bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] From 2c98dbb5512171d63bd631ca8e23f1203c32bd30 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 25 Sep 2024 11:14:01 +0800 Subject: [PATCH 08/14] Add zvbb extenson's vwsll --- .vscode/settings.json | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 .vscode/settings.json diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 5488acecc..000000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,5 +0,0 @@ -{ - "files.watcherExclude": { - "**/target": true - } -} From 247a51adb2b9b359bb2d00f7de719e89ca734aae Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 25 Sep 2024 11:15:50 +0800 Subject: [PATCH 09/14] Add zvbb extenson's vwsll --- sail-riscv.install | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 sail-riscv.install diff --git a/sail-riscv.install b/sail-riscv.install new file mode 100644 index 000000000..7a539dfb5 --- /dev/null +++ b/sail-riscv.install @@ -0,0 +1,2 @@ +bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] From bd00193679fbb68247f67cdc5bd4865f9fb44993 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 9 Oct 2024 00:21:41 +0800 Subject: [PATCH 10/14] Add vctz vclz instruction --- model/riscv_insts_vext_vset.sail | 2 +- model/riscv_insts_zvbb.sail | 80 ++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 1 deletion(-) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 7e73d5724..2378ecc5b 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -61,7 +61,7 @@ function calculate_new_vl(AVL, VLMAX) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), VLMAX) else to_bits(sizeof(xlen), VLMAX) } diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index 6077ad1db..c54034329 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -127,3 +127,83 @@ function clause execute (VWSLL_VI(vm, vs2, uimm, vd)) = { vstart = zeros(); RETIRE_SUCCESS } + +val count_trailing_zeros : forall 'n, 'n >= 0 . (bits('n)) -> range(0, 'n) +function count_trailing_zeros(x) = { + foreach (i from 0 to ('n - 1)) { + if x[i] == bitone then return i + }; + 'n +} + +union clause ast = VCLZ_V : (bits(1), regidx, regidx) + +mapping clause encdec = VCLZ_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b010010 @ vm @ vs2 @ 0b01100 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VCLZ_V (vm, vs2, vd) + <-> "vclz.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ maybe_vmask(vm) + +function clause execute (VCLZ_V(vm, vs2, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + let clz = count_leading_zeros(vs2_val[i]); + result[i] = to_bits('m, clz); + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} + +union clause ast = VCTZ_V : (bits(1), regidx, regidx) + +mapping clause encdec = VCTZ_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b010010 @ vm @ vs2 @ 0b01101 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VCTZ_V (vm, vs2, vd) + <-> "vctz.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ maybe_vmask(vm) + +function clause execute (VCTZ_V(vm, vs2, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + var result : vector('n, dec, bits('m)) = undefined; + var mask : vector('n, dec, bool) = undefined; + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + let ctz = count_trailing_zeros(vs2_val[i]); + result[i] = to_bits('m, ctz); + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} From e1006a0ed2944f8927b95de6e09bd213c9d372e9 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 9 Oct 2024 00:22:10 +0800 Subject: [PATCH 11/14] Add vctz vclz instruction --- model/riscv_insts_vext_vset.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 2378ecc5b..7e73d5724 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -61,7 +61,7 @@ function calculate_new_vl(AVL, VLMAX) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), VLMAX) + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) else to_bits(sizeof(xlen), VLMAX) } From 54f7f169eafe888120bc028684136640669c270e Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Wed, 9 Oct 2024 00:44:43 +0800 Subject: [PATCH 12/14] Add vctz vclz instruction --- model/riscv_insts_zvbb.sail | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index c54034329..b88a69090 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -152,14 +152,12 @@ function clause execute (VCLZ_V(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { @@ -188,14 +186,13 @@ function clause execute (VCTZ_V(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - var result : vector('n, dec, bits('m)) = undefined; - var mask : vector('n, dec, bool) = undefined; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + var result = initial_result; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { From 585db3b9b1712e4a5236cbcbd12c69de8bd4e13e Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Fri, 11 Oct 2024 00:22:04 +0800 Subject: [PATCH 13/14] Add vcpop instruction --- model/riscv_insts_vext_vset.sail | 2 +- model/riscv_insts_zvbb.sail | 38 ++++++++++++++++++++++++++++++++ 2 files changed, 39 insertions(+), 1 deletion(-) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 7e73d5724..2378ecc5b 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -61,7 +61,7 @@ function calculate_new_vl(AVL, VLMAX) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), VLMAX) else to_bits(sizeof(xlen), VLMAX) } diff --git a/model/riscv_insts_zvbb.sail b/model/riscv_insts_zvbb.sail index b88a69090..c5107d692 100644 --- a/model/riscv_insts_zvbb.sail +++ b/model/riscv_insts_zvbb.sail @@ -204,3 +204,41 @@ function clause execute (VCTZ_V(vm, vs2, vd)) = { vstart = zeros(); RETIRE_SUCCESS } + +union clause ast = VCPOP_V : (bits(1), regidx, regidx) + +mapping clause encdec = VCPOP_V (vm, vs2, vd) if extensionEnabled(Ext_Zvbb) + <-> 0b010010 @ vm @ vs2 @ 0b01110 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_Zvbb) + +mapping clause assembly = VCPOP_V (vm, vs2, vd) + <-> "vcpop.v" ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ maybe_vmask(vm) + +function clause execute (VCPOP_V(vm, vs2, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + let 'n = num_elem; + let 'm = SEW; + + + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + + let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + var result = initial_result; + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + foreach (j from 0 to (SEW - 1)) { + if vs2_val[i][j] == bitone then { + result[i] = result[i] + 1; + }; + } + }; + write_vreg(num_elem, SEW, LMUL_pow, vd, result); + }; + vstart = zeros(); + RETIRE_SUCCESS +} From 037daa68a3e99ac3ccab13801d975f9045ea9a1e Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Fri, 11 Oct 2024 00:22:34 +0800 Subject: [PATCH 14/14] Add vcpop instruction --- model/riscv_insts_vext_vset.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 2378ecc5b..7e73d5724 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -61,7 +61,7 @@ function calculate_new_vl(AVL, VLMAX) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), VLMAX) + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) else to_bits(sizeof(xlen), VLMAX) }