diff --git a/doc/asciidoc/riscv.adoc b/doc/asciidoc/riscv.adoc index 6d5c254c8..a48edd43f 100644 --- a/doc/asciidoc/riscv.adoc +++ b/doc/asciidoc/riscv.adoc @@ -18,7 +18,7 @@ this example we define zero-extension and sign-extension functions as: [source,sail] ---- include::sail:EXTZ[from=riscv-code,type=val] -include::sail:EXTS[from=riscv-code,type=function] +include::sail:EXTZ[from=riscv-code,type=function] include::sail:EXTS[from=riscv-code,type=val] include::sail:EXTS[from=riscv-code,type=function] @@ -71,6 +71,8 @@ include::sail:rX[from=riscv-code,type=function] include::sail:wX[from=riscv-code,type=val] include::sail:wX[from=riscv-code,type=function] + +include::sail:XOVERLOAD[from=riscv-code,type=span] ---- We also give a function `MEMr` for reading memory, this function just diff --git a/doc/examples/riscv_duopod.sail b/doc/examples/riscv_duopod.sail index a29ee05dc..6c2f24d0e 100644 --- a/doc/examples/riscv_duopod.sail +++ b/doc/examples/riscv_duopod.sail @@ -111,7 +111,9 @@ function wX(r, v) = Xs[unsigned(r)] = v; } +$span start XOVERLOAD overload X = {rX, wX} +$span end /* Accessors for memory */ val MEMr = monadic { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. diff --git a/doc/manual.html b/doc/manual.html index f2d86a888..fe97cf4a1 100644 --- a/doc/manual.html +++ b/doc/manual.html @@ -4,7 +4,7 @@ - +