Merge pull request #317 from rems-project/systemverilog

Systemverilog backend

.gitignore

@@ -88,6 +88,11 @@ lib/hol/sail-heap
 /test/mono/test.cmi
 /test/mono/test.cmo
 /test/mono/test-output
+/test/sv/*.sv
+/test/sv/*.out
+/test/sv/*.result
+/test/sv/*.cpp
+/test/sv/obj_dir/
 
 /language/*.pdf
 /language/*.uo

dune-project

@@ -76,7 +76,13 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
   (name sail_smt_backend)
   (synopsis "Sail to C translation")
   (depends
-    (libsail (= :version))))    
+    (libsail (= :version))))
+
+(package
+  (name sail_sv_backend)
+  (synopsis "Sail to Systemverilog translation")
+  (depends
+    (libsail (= :version))))
 
 (package
   (name sail_lem_backend)
@@ -130,6 +136,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
     (sail_ocaml_backend (and (= :version) :post))
     (sail_c_backend (and (= :version) :post))
     (sail_smt_backend (and (= :version) :post))
+    (sail_sv_backend (and (= :version) :post))
     (sail_lem_backend (and (= :version) :post))
     (sail_coq_backend (and (= :version) :post))
     (sail_latex_backend (and (= :version) :post))

language/jib.ott

@@ -74,6 +74,7 @@ op :: '' ::=
   | and               :: :: band
   | hd                :: :: list_hd
   | tl                :: :: list_tl
+  | is_empty          :: :: list_is_empty
   | eq                :: :: eq
   | neq               :: :: neq
 % Integer ops
@@ -240,8 +241,7 @@ cdef :: 'CDEF_' ::=
     } :: :: register
   | ctype_def :: :: type
 
-% The first list of instructions sets up the global letbinding, while
-% the second clears it.
+% The list of instructions sets up the global letbinding
   | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = {
       instr0 ; ... ; instrm
     } :: :: let

lib/arith.sail

@@ -116,6 +116,11 @@ val print_int = pure "print_int" : (string, int) -> unit
 
 val prerr_int = pure "prerr_int" : (string, int) -> unit
 
+/*!
+We have special support for raising values to the power of two. Any Sail expression `2 ^ x` will be compiled to this builtin.
+*/
+val pow2 = pure "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
+
 // ***** Integer shifts *****
 
 /*!
@@ -206,4 +211,10 @@ val abs_int_plain = pure {
 
 overload abs_int = {abs_int_plain}
 
+val max_int = pure "max_int" : forall 'x 'y.
+  (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)}
+
+val min_int = pure "min_int" : forall 'x 'y.
+  (int('x), int('y)) -> {'z, ('x < 'y & 'z == 'x) | ('x >= 'y & 'z == 'y). int('z)}
+
 $endif

lib/concurrency_interface/common.sail

@@ -67,8 +67,8 @@
 
 $sail_internal
 
-$target_set emulator_or_isla isla c ocaml interpreter
-$target_set emulator c ocaml interpreter
+$target_set emulator_or_isla isla c ocaml interpreter systemverilog
+$target_set emulator c ocaml interpreter systemverilog
 $target_set prover lem coq
 
 $ifndef _CONCURRENCY_INTERFACE_COMMON

lib/concurrency_interface/emulator_memory.sail

@@ -83,6 +83,10 @@ $iftarget ocaml
 $define _EMULATOR_MEMORY_PRIMOPS
 $endif
 
+$iftarget systemverilog
+$define _EMULATOR_MEMORY_PRIMOPS
+$endif
+
 $ifdef INTERACTIVE
 $define _EMULATOR_MEMORY_PRIMOPS
 $endif

lib/string.sail

@@ -96,4 +96,8 @@ val print_endline = pure "print_endline" : string -> unit
 
 val prerr_endline = pure "prerr_endline" : string -> unit
 
+val print = pure "print" : string -> unit
+
+val prerr = pure "prerr" : string -> unit
+
 $endif

lib/sv/sail.sv

@@ -0,0 +1,81 @@
+`ifndef SAIL_LIBRARY
+`define SAIL_LIBRARY
+
+// The Sail unit type.
+typedef enum logic [0:0] {SAIL_UNIT=0} sail_unit;
+
+// The Sail zero-width bitvector.
+typedef enum logic [0:0] {SAIL_ZWBV=0} sail_zwbv;
+
+`ifdef SAIL_NOSTRINGS
+
+function automatic sail_unit sail_print_endline(sail_unit s);
+   return SAIL_UNIT;
+endfunction // sail_print_endline
+
+function automatic sail_unit sail_prerr_endline(sail_unit s);
+   return SAIL_UNIT;
+endfunction // sail_prerr_endline
+
+function automatic sail_unit sail_print(sail_unit s);
+   return SAIL_UNIT;
+endfunction // sail_print
+
+function automatic sail_unit sail_prerr(sail_unit s);
+   return SAIL_UNIT;
+endfunction // sail_prerr
+
+function automatic sail_unit sail_assert(bit b, sail_unit msg);
+   return SAIL_UNIT;
+endfunction // sail_assert
+
+function automatic bit sail_eq_string(sail_unit s1, sail_unit s2);
+   return 0;
+endfunction
+
+function automatic sail_unit sail_concat_str(sail_unit s1, sail_unit s2);
+   return SAIL_UNIT;
+endfunction
+
+`else
+
+function automatic sail_unit sail_print_endline(string s);
+   $display(s);
+   return SAIL_UNIT;
+endfunction // sail_print_endline
+
+function automatic sail_unit sail_prerr_endline(string s);
+   $display(s);
+   return SAIL_UNIT;
+endfunction // sail_prerr_endline
+
+function automatic sail_unit sail_print(string s);
+   $write(s);
+   return SAIL_UNIT;
+endfunction // sail_print
+
+function automatic sail_unit sail_prerr(string s);
+   $write(s);
+   return SAIL_UNIT;
+endfunction // sail_prerr
+
+function automatic sail_unit sail_assert(bit b, string msg);
+   if (!b) begin
+      $display("%s", msg);
+   end;
+   return SAIL_UNIT;
+endfunction // sail_assert
+
+function automatic bit sail_eq_string(string s1, string s2);
+   return s1 == s2;
+endfunction
+
+function automatic string sail_concat_str(string s1, string s2);
+   return {s1, s2};
+endfunction
+
+`endif
+
+typedef enum logic [0:0] {SAIL_REAL} sail_real;
+
+`endif //  `ifndef SAIL_LIBRARY

lib/sv/sail_memory.sv

@@ -0,0 +1,67 @@
+`ifndef SAIL_MEMORY
+`define SAIL_MEMORY
+
+logic [7:0] sail_memory [logic [63:0]];
+
+bit sail_tag_memory [logic [63:0]];
+
+function automatic sail_bits sail_emulator_read_mem(logic [63:0] addrsize, sail_bits addr, sail_int n);
+   logic [63:0] paddr;
+   logic [SAIL_BITS_WIDTH-1:0] buffer;
+   sail_int i;
+
+   paddr = addr.bits[63:0];
+
+   for (i = n; i > 0; i = i - 1) begin
+      buffer = buffer << 8;
+      buffer[7:0] = sail_memory[paddr + (i[63:0] - 1)];
+   end
+
+   return '{n[SAIL_INDEX_WIDTH-1:0] * 8, buffer};
+endfunction
+
+function automatic sail_bits sail_emulator_read_mem_ifetch(logic [63:0] addrsize, sail_bits addr, sail_int n);
+   return sail_emulator_read_mem(addrsize, addr, n);
+endfunction
+
+function automatic sail_bits sail_emulator_read_mem_exclusive(logic [63:0] addrsize, sail_bits addr, sail_int n);
+   return sail_emulator_read_mem(addrsize, addr, n);
+endfunction
+
+function automatic bit sail_emulator_write_mem(logic [63:0] addrsize, sail_bits addr, sail_int n, sail_bits value);
+   logic [63:0] paddr;
+   logic [SAIL_BITS_WIDTH-1:0] buffer;
+   sail_int i;
+
+   paddr = addr.bits[63:0];
+   buffer = value.bits;
+
+   for (i = 0; i < n; i = i + 1) begin
+      sail_memory[paddr + i[63:0]] = buffer[7:0];
+      buffer = buffer >> 8;
+   end
+
+   return 1'b1;
+endfunction
+
+function automatic bit sail_emulator_write_mem_exclusive(logic [63:0] addrsize, sail_bits addr, sail_int n, sail_bits value);
+   return sail_emulator_write_mem(addrsize, addr, n, value);
+endfunction
+
+function automatic bit sail_emulator_read_tag(logic [63:0] addrsize, sail_bits addr);
+   logic [63:0] paddr;
+   paddr = addr.bits[63:0];
+   if (sail_tag_memory.exists(paddr) == 1)
+     return sail_tag_memory[paddr];
+   else
+     return 1'b0;
+endfunction
+
+function automatic sail_unit sail_emulator_write_tag(logic [63:0] addrsize, sail_bits addr, bit tag);
+   logic [63:0] paddr;
+   paddr = addr.bits[63:0];
+   sail_tag_memory[paddr] = tag;
+   return SAIL_UNIT;
+endfunction
+
+`endif

sail.opam

@@ -36,6 +36,7 @@ depends: [
   "sail_ocaml_backend" {= version & post}
   "sail_c_backend" {= version & post}
   "sail_smt_backend" {= version & post}
+  "sail_sv_backend" {= version & post}
   "sail_lem_backend" {= version & post}
   "sail_coq_backend" {= version & post}
   "sail_latex_backend" {= version & post}

sail_sv_backend.opam

@@ -0,0 +1,42 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.16"
+synopsis: "Sail to Systemverilog translation"
+maintainer: ["Sail Devs <[email protected]>"]
+authors: [
+  "Alasdair Armstrong"
+  "Thomas Bauereiss"
+  "Brian Campbell"
+  "Shaked Flur"
+  "Jonathan French"
+  "Kathy Gray"
+  "Robert Norton"
+  "Christopher Pulte"
+  "Peter Sewell"
+  "Mark Wassell"
+]
+license: "BSD-2-Clause"
+homepage: "https://github.com/rems-project/sail"
+bug-reports: "https://github.com/rems-project/sail/issues"
+depends: [
+  "dune" {>= "3.0"}
+  "libsail" {= version}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/rems-project/sail.git"

src/bin/callgraph_commands.ml

@@ -95,7 +95,7 @@ let dot_of_ast out_chan ast =
   let module G = Graph.Make (Node) in
   let module NodeSet = Set.Make (Node) in
   let g = graph_of_ast ast in
-  G.make_dot (node_color NodeSet.empty) edge_color node_string out_chan g
+  G.make_dot ~node_color:(node_color NodeSet.empty) ~edge_color ~string_of_node:node_string out_chan g
 
 let node_of_id env =
   let lets = Type_check.Env.get_toplevel_lets env in

src/lib/graph.ml

@@ -114,7 +114,13 @@ module type S = sig
         components. *)
   val scc : ?original_order:node list -> graph -> node list list
 
-  val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
+  val make_dot :
+    node_color:(node -> string) ->
+    edge_color:(node -> node -> string) ->
+    string_of_node:(node -> string) ->
+    out_channel ->
+    graph ->
+    unit
 end
 
 module Make (Ord : OrderedType) = struct
@@ -285,7 +291,7 @@ module Make (Ord : OrderedType) = struct
     List.iter (fun v -> if not (Hashtbl.mem node_indices v) then visit_node v) nodes;
     List.rev !components
 
-  let make_dot node_color edge_color string_of_node out_chan graph =
+  let make_dot ~node_color ~edge_color ~string_of_node out_chan graph =
     Util.opt_colors := false;
     let to_string node = String.escaped (string_of_node node) in
     output_string out_chan "digraph DEPS {\n";

src/lib/graph.mli

@@ -116,7 +116,13 @@ module type S = sig
         components. *)
   val scc : ?original_order:node list -> graph -> node list list
 
-  val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
+  val make_dot :
+    node_color:(node -> string) ->
+    edge_color:(node -> node -> string) ->
+    string_of_node:(node -> string) ->
+    out_channel ->
+    graph ->
+    unit
 end
 
 module Make (Ord : OrderedType) :