diff --git a/spec/book.typ b/spec/book.typ index 2fd6d8767..7ad75ba9d 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,6 +9,7 @@ summary: ( ("memory.typ", [Memory argument], ), ("variables.typ", [Variables], ), + ("signatures.typ", [Signatures], ), ("is_bit.typ", [IS_BIT template], ), ("sign.typ", [SIGN template], ), ("add.typ", [ADD/SUB template], ), diff --git a/spec/signatures.typ b/spec/signatures.typ new file mode 100644 index 000000000..5673cdcf6 --- /dev/null +++ b/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", +) diff --git a/spec/src.typ b/spec/src.typ index 8200b47c1..6328c4665 100644 --- a/spec/src.typ +++ b/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 diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml new file mode 100644 index 000000000..ba233f1e6 --- /dev/null +++ b/spec/src/signatures.toml @@ -0,0 +1,178 @@ +# cond => IS_BIT +[[signatures]] +tag = "IS_BIT" +kind = "template" +input = ["BaseField"] +cond = "BaseField" + +# cond => ADD +[[signatures]] +tag = "ADD" +kind = "template" +input = ["DWordWL", "DWordWL"] +output = "DWordWL" +cond = "BaseField" + +# cond => SUB +[[signatures]] +tag = "SUB" +kind = "template" +input = ["DWordWL", "DWordWL"] +output = "DWordWL" +cond = "BaseField" + +# cond => NEG +[[signatures]] +tag = "NEG" +kind = "template" +input = ["DWordHL"] +output = "DWordWL" +cond = "Bit" + +# SIGN +[[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" \ No newline at end of file