From 2a56424d28163e625bb6723484e7b8cf2e244724 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 21 Nov 2024 15:56:08 +0000 Subject: [PATCH] SV: Add partial mapping test case and run in CI --- .github/workflows/build.yml | 2 +- .github/workflows/coverage.yml | 4 ++-- src/sail_sv_backend/sail_plugin_sv.ml | 7 ++++-- test/c/partial_mapping.expect | 1 + test/c/partial_mapping.sail | 34 +++++++++++++++++++++++++++ test/run_coverage_tests.sh | 6 +++++ test/sv/run_tests.py | 4 ++-- 7 files changed, 51 insertions(+), 7 deletions(-) create mode 100644 test/c/partial_mapping.expect create mode 100644 test/c/partial_mapping.sail diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 0114652d0..f4566e8ee 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -31,7 +31,7 @@ jobs: - name: System dependencies (macOS) if: startsWith(matrix.os, 'macOS') run: | - brew install gpatch gmp z3 pkg-config lzlib zlib opam + brew install --force --overwrite gpatch gmp z3 pkg-config lzlib zlib opam - name: Restore cached opam id: cache-opam-restore diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index c3275f1de..2d2f5282c 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -11,7 +11,7 @@ jobs: strategy: matrix: version: [4.08.1] - os: [ubuntu-latest] + os: [ubuntu-24.04] runs-on: ${{ matrix.os }} @@ -21,7 +21,7 @@ jobs: - name: System dependencies run: | sudo apt-get update - sudo apt-get -o Acquire::Retries=3 install build-essential libgmp-dev z3 cvc4 opam cargo + sudo apt-get -o Acquire::Retries=3 install build-essential libgmp-dev z3 cvc4 opam cargo verilator - name: Restore cached opam id: cache-opam-restore diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 457867f2b..69ee72278 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -74,6 +74,7 @@ let opt_verilate_args = ref None let opt_verilate_cflags = ref None let opt_verilate_ldflags = ref None let opt_verilate_link_sail_runtime = ref false +let opt_verilate_jobs = ref 0 let append_flag opt flag = match !opt with None -> opt := Some flag | Some flags -> opt := Some (flags ^ " " ^ flag) @@ -141,6 +142,7 @@ let verilog_options = Arg.Set opt_verilate_link_sail_runtime, " Link the Sail C runtime with the generated verilator C++" ); + ("-sv_verilate_jobs", Arg.Int (fun i -> opt_verilate_jobs := i), " Provide the -j option to verilator"); ("-sv_lines", Arg.Set opt_line_directives, " output `line directives"); ("-sv_comb", Arg.Set opt_comb, " output an always_comb block instead of initial block"); ("-sv_inregs", Arg.Set opt_inregs, " take register values from inputs"); @@ -674,8 +676,9 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = here, and just hope for the best. *) let verilator_command = sprintf - "verilator --cc --exe --build -j 0 --top-module sail_toplevel -I%s --Mdir %s_obj_dir sim_%s.cpp %s.sv%s%s%s" - sail_sv_libdir out out out extra cflags ldflags + "verilator --cc --exe --build -j %d --top-module sail_toplevel -I%s --Mdir %s_obj_dir sim_%s.cpp \ + %s.sv%s%s%s" + !opt_verilate_jobs sail_sv_libdir out out out extra cflags ldflags in print_endline ("Verilator command: " ^ verilator_command); let _ = Unix.system verilator_command in diff --git a/test/c/partial_mapping.expect b/test/c/partial_mapping.expect new file mode 100644 index 000000000..9766475a4 --- /dev/null +++ b/test/c/partial_mapping.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/partial_mapping.sail b/test/c/partial_mapping.sail new file mode 100644 index 000000000..5aa9a4885 --- /dev/null +++ b/test/c/partial_mapping.sail @@ -0,0 +1,34 @@ +default Order dec + +$include + +enum Uop = A | B + +mapping encdec_uop : Uop <-> bits(5) = { + A <-> 0b00001, + B <-> 0b00010 +} + +union Instr = { + I1 : Uop, + I2 : unit +} + +$[optimize_control_flow_order] +mapping encdec : Instr <-> bits(8) = { + I1(op) <-> 0b100 @ encdec_uop(op), + I2() <-> 0x00 +} + +register R : bits(8) = 0b1000_0001 + +val main : unit -> unit + +function main() = { + let i = encdec(R); + let _ = encdec(0x00); + match i { + I1(A) => print_endline("ok"), + _ => (), + } +} diff --git a/test/run_coverage_tests.sh b/test/run_coverage_tests.sh index 3e30c6651..9809b3ef0 100755 --- a/test/run_coverage_tests.sh +++ b/test/run_coverage_tests.sh @@ -49,6 +49,12 @@ printf "==========================================\n" ./smt/run_tests.py || returncode=1 +printf "\n==========================================\n" +printf "SystemVerilog tests\n" +printf "==========================================\n" + +./sv/run_tests.py || returncode=1 + printf "\n==========================================\n" printf "Lean tests\n" printf "==========================================\n" diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py index a6aa7c5ee..2a7baa497 100755 --- a/test/sv/run_tests.py +++ b/test/sv/run_tests.py @@ -50,9 +50,9 @@ def test_sv(name, opts, skip_list): if tests[filename] == 0: step('rm -rf {}_obj_dir'.format(basename)); if basename.startswith('fail'): - step('{} --no-warn --sv ../c/{} -o {} --sv-verilate compile{} > {}.out'.format(sail, filename, basename, opts, basename)) + step('{} --no-warn --sv ../c/{} -o {} --sv-verilate compile{} --sv-verilate-jobs 1 > {}.out'.format(sail, filename, basename, opts, basename)) else: - step('{} --no-warn --sv ../c/{} -o {} --sv-verilate run{} > {}.out'.format(sail, filename, basename, opts, basename)) + step('{} --no-warn --sv ../c/{} -o {} --sv-verilate run{} --sv-verilate-jobs 1 > {}.out'.format(sail, filename, basename, opts, basename)) step('awk \'/SAIL START/{{flag=1;next}}/SAIL END/{{flag=0}}flag\' {}.out > {}.result'.format(basename, basename)) step('diff ../c/{}.expect {}.result'.format(basename, basename)) print_ok(filename)