Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Zvbb extension #558

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
60 changes: 4 additions & 56 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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_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

Expand Down Expand Up @@ -128,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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should these OCaml removal changes be part of this PR? We recently removed it the OCaml simulator, not sure if these were missed or just an artifact of a rebase commit.


SAIL_FLAGS += --require-version 0.18
SAIL_FLAGS += --strict-var
SAIL_FLAGS += -dno_cast
Expand Down Expand Up @@ -208,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
Expand All @@ -230,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
Expand All @@ -284,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)

Expand Down Expand Up @@ -470,34 +436,16 @@ 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
-rm -f handwritten_support/riscv_extras.vo handwritten_support/riscv_extras.vos handwritten_support/riscv_extras.vok handwritten_support/riscv_extras.glob handwritten_support/.riscv_extras.aux
-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
137 changes: 137 additions & 0 deletions model/riscv_insts_zvbb.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
/*=======================================================================================*/
/* 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

mapping vm_name : bits(1) <-> string = {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wondering if we have this mapping already somewhere?

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)

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('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);

foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
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_widen, LMUL_pow, vd, result);
};
vstart = zeros();
RETIRE_SUCCESS
}

union clause ast = VWSLL_VX : (bits(1), regidx, regidx, regidx)

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)

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('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);

foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
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_widen, LMUL_pow, vd, result);
};
vstart = zeros();
RETIRE_SUCCESS
}

union clause ast = VWSLL_VI : (bits(1), regidx, bits(5), regidx)

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 = 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 (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 SEW_widen = SEW * 2;
let LMUL_pow_widen = LMUL_pow + 1;

let 'n = num_elem;
let 'm = SEW;
let 'o = SEW_widen;

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);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I recently refactored this into:

let (initial_result, mask)  = init_masked_result(num_elem, SEW_widen, LMUL_pow - 1, vd_val, vm_val);
var result = initial_result;

elsewhere, so we can remove the = undefined lines. Would be good to make this consistent.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(also same for the above instructions)


foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
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_widen, LMUL_pow, vd, result);
};
vstart = zeros();
RETIRE_SUCCESS
}
Loading