SV: Add partial mapping test case and run in CI

.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

.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

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), "<n> 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

test/c/partial_mapping.expect

@@ -0,0 +1 @@
+ok

test/c/partial_mapping.sail

@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+
+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"),
+    _ => (),
+  }
+}

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"

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)