The language · and how the toolchain reads it

Writing hardware

A sysr design is a set of modules, functions and types written as s-expressions. Each signal has exactly one definition, each value an explicit width, and each module the properties it must keep. This page goes through the language as a designer meets it, then follows a design through the parts of the toolchain that read it, type it and check its structure. The reference is the complete definition.

Modules and declarations

A design is a sequence of module, struct, enum, fn and spec definitions; anything else at the top level is an error (P003). A module is (module Name (params...) declarations...), and its declarations are an unordered set: any of them may refer to any other, as wires do in hardware. There are only these:

One defining form per signal

There is no assignment statement in sysr. A signal is defined, once, by the form that declares it: a let gives a combinational value, a reg a register's reset and next values, a drive an output's value. There is nothing to assign "in some branches only", so a latch cannot be written, and a design never needs a default: to avoid one. What remains to check is mechanical: an output with no drive is D001, one driven twice is D002, an instance input not connected (or connected twice) is D004, and signals that depend on each other within one cycle are a combinational loop, D003. The figure at the end of this page lets you make each of them.

Clock and reset

A module with a register, directly or inside an instance, is sequential: it has the implicit ports clk and rst, synchronous and active high, which no expression can name and no declaration can take (N002). At each rising edge, every register takes its next value, or its reset value when rst is 1. A module without registers is combinational and has neither port. Here is the tour's counter; give it clock edges and watch count.

Widths and types

A value is a bit vector (bits w), unsigned, with (bits 1) as the boolean; an array (array n (bits w)); a struct; or an enum. Widths are constant expressions: naturals, parameters, and +, -, * and clog2 of them, evaluated during elaboration (eval-width in types.rkt; a width that comes out below 1 is T007).

There are no implicit conversions. The operands of +, ==, and and the other binary operators have equal widths, or the design is rejected with T001, which carries the expected and actual types and suggests trunc, zext or a wrapping operator. A literal takes the width its context expects, so (== count 9) compares two 4-bit values; so does a constant such as (- depth 1), computed in the checker. A literal that does not fit is T005; one with nothing to give it a width is T008. + and - are proven never to carry or borrow; +%, -% and *% wrap on purpose.

Arrays and memories

A small memory is a register of array type, with a reset value: get reads an element, put makes the array with one element replaced, fill makes one with every element equal. Every index is proven in range (V003).

A larger one is a mem: it has no reset value, so nothing is proven from its contents; it is read only with get and written at most once per cycle, so its next value is itself, one put of itself, or an if of these (T011 otherwise). A read that is a register's next value becomes a block-RAM read port.

Structs, enums and match

A struct groups fields of bit vectors, structs or enums: (struct Pair (lo (bits 4)) (hi (bits 4))), built with (new Pair (lo a) (hi b)) and read with (. p lo). In sysr 0.13.0 a field cannot be an array, and array elements are bit vectors.

An enum names the values of a state. It is encoded in (clog2 n) bits, at least one; it has ==, !=, if and match but no ordering and no literals, and it cannot be a port. A match names each variant at most once and covers them all, or ends with (_ expr) for the rest; a _ with nothing left to cover is also an error (all three are T010). The checker lowers a match to a chain of ifs on ==, so it has exactly the meaning and the obligations of that chain. A register holding an enum gets one more obligation: it never holds a code that is not a variant (V006), which matters when the variants do not fill their encoding, as Light's three do not fill two bits.

Functions and spec functions

(fn name ((param type) ...) result-type expr) names combinational logic. A body sees only its parameters, enum values and other functions, and is checked once, before any module. A call is that checked body with the arguments put in place of the parameters (subst in check.rkt): it has the same meaning, the same hardware and the same obligations as if the body were written there, and each call's obligations are reported at the call. A function may not call itself, directly or through others (D006).

A spec is written the same way but may be called only in properties and other spec functions (T006), where past and forall are allowed too. It says what a design must compute; an ensures proves the design equal to it:

This is how the RV64IM core is proven: its units' ensures name the spec functions of isa.sysr (isa.sysr: what is proven).

Parameters and instances

Parameters are naturals with defaults, (module fifo ((width 8) (depth 4)) ...), constants inside the module. An instance may override them, and --param depth=16 overrides the top module's. Each distinct (module, parameters) pair is checked and verified once; a child with non-default parameters gets its own Verilog name, such as fifo__depth_16__width_8. The top is the one module nothing instantiates, or the one --top names; the other modules are checked too, with their defaults. A parent knows an instance only by its contract, its requires and ensures (How designs are proven).

How the toolchain reads a design

Between the text and the verifier, a design passes through six files. Each stage stops the run if it reported an error.

The structure checks, live

Here is a small module with choices in it. Change a line and the figure redraws its dependency graph and lists what sysr check would report, computed in this page the way check.rkt and structure.rkt compute it, with their messages. Solid arrows are reads in the same cycle; the dashed arrow is a register's next value, read a cycle later, which is why a register breaks a loop.

Two places find loops. A loop among lets is found while their types are worked out: check.rkt marks a let as busy while typing it, and meeting a busy one again is D003, with the path. A loop through an output or an instance is found by structure.rkt, which walks the combinational graph and, for every module, summarizes which outputs follow which inputs within a cycle, so that a parent can see a loop through a child (tests/corpus/d003_through_instance.sysr: a pass-through instance whose output feeds its own input).

The tests that hold it

tests/reader-test.rkt checks sysr's view of sysp's reader: its operator tokens read as symbols, spans are 1-based lines and columns, reader errors arrive as P001 and P002, and 300 random scraps of malformed input never make it raise. tests/check-test.rkt runs every corpus design that is not about verification and requires exactly the codes its first line expects; it also checks the detail of a width mismatch, an undriven output's fix ((drive r ?r)), a loop's path, a hole's expected type and the signals in scope, the JSON report's shape, that every code in the registry has a corpus design, and --param. tests/functions-test.rkt covers feature 003: match rules, enum values, enum registers and traces, functions, calls with their own obligations, spec functions and forall. The corpus has 48 designs.