The language · sysr build

Verilog out

sysr build writes Verilog-2005, and only for a design whose every obligation is proven. The output is plain on purpose: one assign per signal, one always block per register, a synchronous reset, memories as arrays Yosys maps to block RAM. Yosys synthesizes it without a warning, and the tests replay the verifier's traces on it in Icarus.

246lines in sysr/codegen.rkt, the whole backend
0Yosys warnings allowed on any reference or verified corpus design
106lines in sysr/fmt.rkt, the formatter
89test cases in make test, these among them

The counter, in Verilog

Here is the docs' counter (the tour checks it) and what sysr build wrote for it when the docs were built. Select a line on either side to see where it comes from or what it becomes.

docs/site/examples/counter.sysr

sysr build … -o counter.v

The order is always the same (module->verilog): the ports, clk and rst first if the module has a register anywhere in it; then the declarations (registers, memories, signals, instance outputs) and temporary wires; then each signal's assign, the outputs' assigns, the instances, one write port per memory, one always block per register, and an initial value per register. generate writes the top module and every module it reaches, children first, behind a one-line header. Properties (ensures, invariant, requires) are not in the output: they were proven, and a proven property needs no checking at run time.

Why Yosys has nothing to warn about

Most warnings a synthesizer gives a hand-written design are about mistakes sysr makes impossible before code generation, or about forms the generator never writes. The test below insists on it: for sysr's own output, not one line of Yosys output may contain "warning".

One defining form per signal

Each let becomes one assign, each reg one always @(posedge clk) block that assigns it on both branches, each output one assign. Nothing is assigned in part or twice, so there are no latches, and the checker has already refused undriven outputs, double drives and combinational loops (D001–D003).

Synchronous reset, power-up values

Every register is if (rst) … else … inside its clocked block, active high. Every register also gets an initial with its reset value, so an FPGA is in its reset state straight from configuration (feature 010). A memory has no reset and no initial, unless --mem-init NAME=FILE asks for $readmemh.

Widths stated, never inferred

Every compound subexpression is written inside { }, which makes Verilog size it by itself, so each operation wraps at exactly the width sysr gave it. Every vector has a range, [0:0] too. Literals are sized: 4'd9. A select on a computed value goes through a temporary wire (_t1, _t2, …), which Verilog-2005 requires.

Memories as block RAM

A mem is a Verilog array with one write port: the if tree of its update becomes one enable, address and data. A read that is a register's next value is the registered read Yosys maps to block RAM; a read used directly becomes distributed RAM. A small array register is instead one register per element (mem_0, mem_1, …) and a get a chain of comparisons, so Yosys sees no memory.

Everything else flattened

Functions are inlined where called; structs become one wire or register per field (name_field); signed comparisons and sra use $signed. An instance's outputs are wires named u__port, connected by name.

Names

sysr names may contain -; Verilog's may not, so - becomes _ (cname in sysr/elab.rkt). A name that is then a Verilog keyword gets a trailing _, so a port called out stays out but one called wire becomes wire_ (vid, with the keyword list in codegen.rkt). A child instantiated with parameters other than its defaults gets its own module, named after them in sorted order; the top module keeps its plain name even under --param. Try a name:

or a module with parameters:

How the generated Verilog is checked

tests/codegen-test.rkt holds the backend to three things:

  1. Synthesis, with no warning. Every benchmark reference (22 tasks) and every verified corpus design (tests/corpus/ok_*.sysr) is built and passed through the scorer's check (Yosys: hierarchy -check, proc, flatten, check -assert, and no latch cell of any kind), then through a fuller Yosys pass (proc; flatten; opt; memory; opt; techmap; opt; check) whose output may not contain the word "warning", and compiled by Icarus (iverilog -g2005).
  2. Replay of the verifier's traces. A failing check comes with a trace from reset: the inputs and registers, cycle by cycle (How designs are proven). For each such trace in the corpus (the v0* designs that are sequential, with no instances and no memory, since traces leave memories out), the test writes a testbench that drives the trace's inputs into the generated Verilog and, in every cycle, compares every register with the trace. Icarus must print PASS. At least 4 traces must be replayed, so the test cannot pass by finding none. This is what makes a trace trustworthy: the Verilog behaves as the verifier's model of the design says, register for register.
  3. Power-up values. Every register of ok_counter has its initial, and so do ok_fifo's count and an element of its array register.

Below is the testbench replay-bench writes, rebuilt in this page by the same rules for the trace the docs' buggy counter gets from reset (the one the tour shows; counter-bug.sysr is not itself in the corpus). Step through it: each cycle sets the inputs, waits 4 time units for them to settle, compares dut.count, then waits for the clock.

The trace (sysr check, depth 11)

The testbench (codegen-test.rkt's replay-bench)

The formatter: sysr fmt

Every .sysr file has one canonical layout, the one sysr fmt prints, so that a model's output and a person's look alike and a diff shows only real changes. sysr fmt FILE prints it, -w rewrites the file, --check fails if a file is not canonical; make fmt-check runs that over the benchmark, the corpus, the core, the devices and the boards. The layout algorithm is sysp's; the tables of how many arguments stay on a form's first line are sysr's (HEADER-ARGS in sysr/fmt.rkt). The rule is short:

  • A form that fits in the line width (88 columns), has no comment inside and is not a module is printed on one line.
  • Otherwise its head and as many of its first arguments as HEADER-ARGS allows (and as fit) stay on the first line, and each other argument goes on a line of its own, indented by two. A list that does not start with a name (a parameter list, a port connection) puts one item per line, aligned after its (.
  • Comments are kept, each on its own line before the item it precedes; top-level forms are separated by one blank line.

Edit the text and move the width to see the rule work; at 88 it is what sysr fmt prints. This is the page's transcription of pp and pp-broken into JavaScript, with the tables read from fmt.rkt; its reader is simpler than sysp's, so treat odd inputs with care.

88

tests/fmt-test.rkt checks that formatting is a fixed point (formatting the output again changes nothing) and keeps comments, that a reader error gives no text rather than a guess, and that every .sysr file in the repository is already canonical (except two corpus files that exist to fail parsing). The formatter's own promise, in its header: fmt(read(fmt(x))) = fmt(read(x)) for every design.