spec: signatures

spec/book.typ

@@ -9,6 +9,7 @@
   summary: (
     ("memory.typ", [Memory argument], <memory>),
     ("variables.typ", [Variables], <vars>),
+    ("signatures.typ", [Signatures], <signatures>),
     ("is_bit.typ", [IS_BIT template], <isbit>),
     ("sign.typ", [SIGN template], <sign>),
     ("add.typ", [ADD/SUB template], <add>),

spec/signatures.typ

@@ -0,0 +1,90 @@
+#import "/book.typ": book-page
+#import "/src.typ": load_signatures, load_config
+
+#show: book-page("signatures.typ")
+
+#let config = load_config()
+#let signatures = load_signatures(config)
+
+// Render a signature
+#let render_signature(sig) = {
+  let (lb, rb) = if sig.kind == "interaction" {
+    (`[`, `]`)
+  } else if sig.kind == "template" {
+    (`<`, `>`)
+  }
+
+  let cond = sig.at("cond", default: none)
+  let cond_str = if cond != none {
+    raw(cond) + ` => `
+  } else {``}
+
+  let input_str = sig.input.map(elt => {
+    if type(elt) == array {
+      raw(elt.at(0)) + `[` + raw(str(elt.at(1))) + `]`
+    } else {
+      raw(elt)
+    }
+  }).join(`, `)
+
+  let output = sig.at("output", default: none)
+  let output_str = if output != none {
+    if type(output) == array {
+      raw(output.at(0)) + `[` + raw(str(output.at(1))) + `]`
+    } else {
+      raw(output)
+    } + `; `
+  } else {``}
+
+  return [#cond_str#raw(sig.tag)#lb#output_str#input_str#rb]
+}
+
+// Compute the bus size of an interaction
+#let interaction_bus_size(sig) = {
+  let vars = sig.input + if "output" in sig { (sig.output, )} else {()}
+
+  return vars.map(v => {
+    let (label, factor) = if type(v) == array {
+      (v.at(0), v.at(1))
+    } else {
+      (v, 1)
+    }
+    config.variables.types.filter(type => type.label == label).first().subtypes.len() * factor
+  })
+  .sum()
+}
+
+#let interactions = signatures.signatures.filter(s => s.kind == "interaction")
+The following lists signatures of the #interactions.len() interactions in this VM.
+#figure(
+  table(
+    columns: (1fr, auto),
+    inset: 7pt,
+    align: (top+left, center),
+    stroke: none,
+    table.header([*Signature*], [*Bus size*]),
+    table.hline(stroke: 1pt),
+    table.vline(stroke: 1pt, x: 1),
+    ..for sig in interactions {
+      ([#render_signature(sig)], [#interaction_bus_size(sig)])
+    },
+  ),
+  caption: "Signature overview of interactions",
+)
+
+#let templates = signatures.signatures.filter(s => s.kind == "template")
+Below, we list the signatures of the #templates.len() templates in this VM.
+#figure(
+  table(
+    columns: 1fr,
+    inset: 7pt,
+    align: (top+left, center),
+    stroke: none,
+    table.header([*Signature*]),
+    table.hline(stroke: 1pt),
+    ..for sig in templates {
+      ([#render_signature(sig)], )
+    },
+  ),
+  caption: "Signature overview of templates",
+)

spec/src.typ

@@ -1,5 +1,7 @@
 /// Path to the config file.
 #let CONFIG_PATH = "src/config.toml"
+/// Path to the signatures file
+#let SIGNATURES_PATH = "src/signatures.toml"
 
 /// Check the configuration object for internal consistency.
 #let _check_config(config) = {
@@ -31,6 +33,55 @@
   return config
 }
 
+
+// Validate the `signatures` overview
+#let _check_signatures(signatures, config) = {
+  let var_labels = config.variables.types.map(t => t.label)
+
+  // Verify that `var` is a valid variable.
+  let verify_variable(var) = {
+    if type(var) == array {
+        assert(var.at(0) in var_labels, message: "Invalid var type: " + repr(var))
+        assert(type(var.at(1)) == int, message: "Invalid var type: " + repr(var))
+    } else if type(var) == str {
+      assert(var in var_labels, message: "Invalid var type: " + repr(var))
+    } else {
+      assert(false, message: "Invalid var type: " + repr(var))
+    }
+  }
+
+  assert("signatures" in signatures, message: "No signatures listed")
+  for sig in signatures.signatures {
+    assert("tag" in sig, message: "No tag associated with " + repr(sig))
+    assert(type(sig.tag) == str, message: "Tag is not of type str: " + repr(sig.tag))
+
+    assert("kind" in sig, message: "No kind associated with " + repr(sig))
+    assert(type(sig.kind) == str, message: "kind is not of type str: " + repr(sig.kind))
+    assert(sig.kind in ("interaction", "template"), message: "Invalid kind: " + repr(sig.kind))
+
+    if "cond" in sig {
+      assert(sig.kind != "interaction", message: "Invalid condition for interaction: " + repr(sig))
+      verify_variable(sig.cond)      
+    }    
+
+    assert("input" in sig, message: "No input associated with " + repr(sig))
+    assert(type(sig.input) == array, message: "Invalid input type: " + repr(sig.input))
+    sig.input.map(i => verify_variable(i))
+
+    if "output" in sig {
+      verify_variable(sig.output)
+    }
+  }
+}
+
+// Load the signatures from file
+#let load_signatures(config) = {
+  let signatures = toml(SIGNATURES_PATH)
+  _check_signatures(signatures, config)
+  return signatures
+}
+
+
 /// Check a chip object for internal consistency.
 #let _check_chip(chip, config) = {
   // Check that all variable categories are valid

spec/src/signatures.toml

@@ -0,0 +1,178 @@
+# cond => IS_BIT<X>
+[[signatures]]
+tag = "IS_BIT"
+kind = "template"
+input = ["BaseField"]
+cond = "BaseField"
+
+# cond => ADD<sum; lhs, rhs>
+[[signatures]]
+tag = "ADD"
+kind = "template"
+input = ["DWordWL", "DWordWL"]
+output = "DWordWL"
+cond = "BaseField"
+
+# cond => SUB<diff; lhs, rhs>
+[[signatures]]
+tag = "SUB"
+kind = "template"
+input = ["DWordWL", "DWordWL"]
+output = "DWordWL"
+cond = "BaseField"
+
+# cond => NEG<neg; X>
+[[signatures]]
+tag = "NEG"
+kind = "template"
+input = ["DWordHL"]
+output = "DWordWL"
+cond = "Bit"
+
+# SIGN<sign; X, signed>
+[[signatures]]
+tag = "SIGN"
+kind = "template"
+input = ["Half", "Bit"]
+output = "Bit"
+
+# DECODE[pc, imm, packed_decode]
+[[signatures]]
+tag = "DECODE"
+kind = "interaction"
+input = ["DWordWL", "DWordWL", "BaseField"]
+
+# SHIFT[out; in, shift, direction, signed, word_instr]
+[[signatures]]
+tag = "SHIFT"
+kind = "interaction"
+input = ["DWordHL", "Byte", "Bit", "Bit", "Bit"]
+output = "DWordWL"
+
+# BRANCH[next_pc; pc, offset, register, JALR]
+[[signatures]]
+tag = "BRANCH"
+kind = "interaction"
+input = ["DWordWL", "Word", "DWordWL", "Bit"]
+output = "DWordWL"
+
+# MEMW[old; is_register, base_address, value, timestamp, write2, write4, write8]
+[[signatures]]
+tag = "MEMW"
+kind = "interaction"
+input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"]
+output = ["BaseField", 8]
+
+# MEMW[is_register, base_address, value, timestamp, write2, write4, write8]
+[[signatures]]
+tag = "MEMW"
+kind = "interaction"
+input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"]
+
+# LT[lt; lhs, rhs, signed]
+[[signatures]]
+tag = "LT"
+kind = "interaction"
+input = ["DWordWL", "DWordWL", "Bit"]
+output = "Bit"
+
+# MUL[lo/hi; lhs, lhs_signed, rhs, rhs_signed, 0/1]
+[[signatures]]
+tag = "MUL"
+kind = "interaction"
+input = ["DWordHL", "Bit", "DWordHL", "Bit", "Bit"]
+output = "DWordWL"
+
+# DVRM[q/r; n, d, signed, 0/1]
+[[signatures]]
+tag = "DVRM"
+kind = "interaction"
+input = ["DWordHL", "DWordHL", "Bit", "Bit"]
+output = "DWordWL"
+
+# LOAD[res; base_address, timestamp, read2, read4, read8, signed]
+[[signatures]]
+tag = "LOAD"
+kind = "interaction"
+input = ["DWordWL", "DWordWL", "Bit", "Bit", "Bit", "Bit"]
+output = "DWordWL"
+
+# ECALL[timestamp, syscallnr]
+[[signatures]]
+tag = "ECALL"
+kind = "interaction"
+input = ["DWordWL", "DWordWL"]
+
+# AND_BYTE[res; X, Y]
+[[signatures]]
+tag = "AND_BYTE"
+kind = "interaction"
+input = ["Byte", "Byte"]
+output = "Byte"
+
+# OR_BYTE[res; X, Y]
+[[signatures]]
+tag = "OR_BYTE"
+kind = "interaction"
+input = ["Byte", "Byte"]
+output = "Byte"
+
+# XOR_BYTE[res; X, Y]
+[[signatures]]
+tag = "XOR_BYTE"
+kind = "interaction"
+input = ["Byte", "Byte"]
+output = "Byte"
+
+# MSB8[msb; X]
+[[signatures]]
+tag = "MSB8"
+kind = "interaction"
+input = ["Byte"]
+output = "Bit"
+
+# MSB16[msb; X]
+[[signatures]]
+tag = "MSB16"
+kind = "interaction"
+input = ["Half"]
+output = "Bit"
+
+# ZERO[is_zero; X]
+[[signatures]]
+tag = "ZERO"
+kind = "interaction"
+input = ["B20"]
+output = "Bit"
+
+# IS_BYTE[X]
+[[signatures]]
+tag = "IS_BYTE"
+kind = "interaction"
+input = ["Byte"]
+
+# IS_HALF[X]
+[[signatures]]
+tag = "IS_HALF"
+kind = "interaction"
+input = ["Half"]
+
+# IS_B20[X]
+[[signatures]]
+tag = "IS_B20"
+kind = "interaction"
+input = ["B20"]
+
+# HWSL[res; X, shift]
+[[signatures]]
+tag = "HWSL"
+kind = "interaction"
+input = ["Half", "B4"]
+output = "Half"
+
+# HWSLC[res; X, shift]
+[[signatures]]
+tag = "HWSLC"
+kind = "interaction"
+input = ["Half", "B4"]
+output = "Half"