Verity

The programming language of GOS is called Verity. It is an Algol-like language, in its idealized form due to John Reynolds. This means that:
  • its functional fragment is the call-by-name Lambda calculus, which is extremely similar (observationally equivalent) to that of the Haskell programming language
  • it has (higher-order, affine) recursion
  • its imperative fragment is based on local effects (local variables and assignments, local control and exceptions, etc.)
  • it is an expressive programming language with no hardware specific features
  • ok, it has one hardware-specific feature, it allows you to specify arbitrary data widths for integers. 

A Quick FAQ

  1. Q: What is the coolest thing about GOS/Verity?
    A: Full support for functions, no in-lining.

  2. Q: Why are functions so cool? 
    A: Because you can do high-level functional-style programming, which is compact, elegant and less buggy. And because you can support libraries and foreign-function interfaces (FFI).

  3. Q: Why is FFI important?
    A: How else are you going to interface with legacy IP-cores or low-level drivers which cannot be implemented in the high-level language? 

  4. Q: Why not C?
    A: For two reasons. First, the support for (higher order and anonymous) functions in C is clumsy and we can simply do better, with no performance penalty. Second, C is heavily oriented on programming the global memory (pointers), which we don't really have in hardware synthesis. A global memory can be used via function calls, but no syntactic language support for pointers is provided. 

  5. Q: Why not OCaml?
    A: Function calls in OCaml, which are call-by-value, are sequential. This is built into the semantics of the language and it is unclear how it could be changed. In a hardware-oriented language we are aiming at parallelism, and call-by-name seems more suitable. Also, the effect model of OCaml is global rather than local which seems unsuitable for static hardware, which lacks a global memory. Finally, it is not possible to implement OCaml without a garbage collector which is both complicated in hardware and, yet again, demanding of a global memory.

  6. Q: Why not Haskell?
    A: The call-by-need model of Haskell seems compatible with hardware, but we don't know how to implement it efficiently yet. This is an area of ongoing research. Note that the only difference between Verity and Haskell is efficieny: Verity re-evaluates the argument whereas Haskell caches it. This makes the Haskell approach much more efficient, but also somewhat incompatible with side-effects (assignments, control). There are ways in which tension can be reconciled, but this is the object of ongoing research. Also, we don't quite like monads as they represent a way to globalise effects. We are more interested in type systems which localise effects, such as Reynolds's SCI.
     
  7. Q: How do you handle memory management?
    A: Verity has no primitives for memory management, such as pointers, allocation, deallocation or garbage collection. We don't believe that in a language targeted towards synthesis language-support for memory management is appropriate because memory can be on- or off-chip, and the distinction between the two is critical. We believe the best way to handle memory management is through libraries which are aware of the particular design needs and memory hierarchy used by a particular system (e.g. cached vs. scratchpad). 

  8. Q: Why "Verity"?
    A: Because we love monoidal categories!

Examples

Here is a simple example of Verity code which calculates the 5th Fibonacci number:

import <print>

print(
(fix \fib.\n.
   new n1 in
   new n2 in
   new n3 in (
   n1 := n;
   if !n1 < 2 then 1$32
   else (n2 := fib(!n1 - 1$32); n3 := fib(!n1 - 2$32); !n2 + !n3)
))(5))

In the trees.ia file attached below there is a more complicated example involving tree operations.