Cava Reference

Details the main building blocks of circuits in Cava, for easy scanning and searching. Everything detailed here is available with Require Import Cava.Cava unless stated otherwise. For a more thorough introduction to Cava, check out the tutorial.

Core Infrastructure

Simulation

Netlist Generation

Circuit Subcomponents and Signals

All Signal Types

Booleans

Vectors

Constructing

Adding and Removing Elements

Resizing

Indexing

Rearranging Elements

Convert to and from Vector.t

Higher-order functions

Bit-Vectors

All bit vector arithmetic treats the bit vectors as unsigned and little-endian.

Circuit Combinators

Tuple Manipulation

These are especially useful with monad composition (_ >=> _).

4-sided Tile Combinators

The diagrams below illustrate the below and col combinators visually.

diagrams of the below and col tile combinators

Tree Combinators

Lookup Tables

Netlist-specific

These operations affect the generated SystemVerilog but not generally the functional behavior of the circuit, but can be used for fine-grained control over resource usage.

Circuit Constructors

These constructors are the building blocks for Circuits.

Generally, we recommend writing the purely combinational components of circuits using monadic functions, and then using these constructors to combine non-combinational parts.

Circuit diagram for Loop constructor

Proof Automation

These tactics and rewrite databases will greatly simplify Cava proofs; they’re not mandatory, but it’s a good idea to know that they exist and roughly what they do. This list is not exhaustive.

For more detail on a particular tactic, try searching the codebase for other places where it’s used, or for the tactic’s test cases.

Tactics

simpl_ident: transforms an expression in terms of the identity monad (this will be practically all circuit proofs) and/or circuit simulations into a non-monadic expression, which will be easier to reason about.

length_hammer : solves most goals relating to list lengths (e.g. length (firstn n (a ++ b)) < 4).

destruct_pair_let : Coq’s let '(x,y) := _ in syntax is convenient but doesn’t simplify away easily in proofs. This tactic simplifies it for you, so that an expression like foo (let '(x,y,z) := p in z) becomes foo (snd p).

logical_simplify : performs a few commonly-needed simplifications to the hypotheses in context. For instance, if you have H : exists x, P x /\ exists y, Q x y, this tactic will give you a context with new variables for x and y, and the two hypotheses P x and Q x y.

constant_vector_simpl v: if v is a constant-length vector in the current context, destructs it into its elements (so instead of Vector.t nat 4, you have 4 variables of type nat)

constant_bitvec_cases v: if v is a boolean vector of constant length in the current context, creates a subgoal for each possible value of v. For instance, if v has the type Vector.t bool 3, you will get 8 subgoals (one for v = [false;false;false], one for v=[true;false;false], etc.). Useful for situations in which you have a limited number of cases and want to prove each one by computation.

Autorewrite databases

Autorewrite databases in Coq (see the manual entries on autorewrite and Hint Rewrite are powerful and often underused tools for automatic reasoning in Coq. For those new to the idea, it works like this:

Hint Rewrite @app_length using solve [eauto] : push_length.
Hint Rewrite @nil_length using solve [eauto] : push_length.
Hint Rewrite @repeat_length using solve [eauto] : push_length.

Goal (forall T (x : T) n m, length (repeat x n ++ [] ++ repeat x m) = n + mw).
intros.
(* Goal: length (repeat x n ++ [] ++ repeat x m) = n + m *)
autorewrite with push_length.
(* Goal : n + (0 + m) = n + m *)
Abort.

Basically, you can add a whole bunch of lemmas to the hint database, and then use autorewrite to rewrite with them in whatever order works. The solve [eauto] can be replaced with any tactic that you want to apply to the rewrite’s side conditions; for a lemma with an arithmetic side condition, you might want lia. It’s good practice to make sure that the tactic won’t leave unsolved goals (hence solve [eauto] even though none of the lemmas above actually generate side conditions).

Cava defines a number of autorewrite databases that you can use and add to, including the push_length one in the example. Some of the tactics mentioned above actually use autorewrite databases, too; if you add a lemma to the push_length hint database, for instance, the length_hammer tactic will know about your lemma and use it to solve list-length goals.

One final note: many autorewrite databases are named push_foo, for some definition foo. This means that lemmas added to that database “push” the foo definition further into the expression, or eliminate it. For instance, the lemma app_length, which has the type forall {A} (l l' : list A), length (l ++ l') = length l + length l', has length as the outermost expression on the left-hand side, but has add as the outermost expression on the right-hand side, with length deeper in the expression tree. The lemma nil_length, which has the type length [] = 0, removes a length invocation.

The most useful autorewrite databases defined by Cava are:

Notations

Monad Notations

In Cava circuits, combinational functions are written using an abstract monad called cava to record sharing. As a result, there are a few monad notations that are helpful to know:

Each is discussed in more detail below.

Return

ret

Simply wraps any expression in a monad (return).

Examples: ret 5, ret (x, y), ret (foo (bar x, y))

Basic Bind

_ <- _ ;; _

Assigns an expression to a name. x <- foo ;; ... binds foo to the name x, and the expression after the ;; can use the name x. This operator is right-associative: x <- foo ;; y <- bar ;; ... is interpreted as x <- foo ;; (y <- bar ;; (...)).

You’ll often see a newline after the ;;, which is stylistically preferred but not strictly necessary; whitespace, as for all Coq notations, is ignored.

Examples

Return the sum of two numbers:

sum <- addN (a, b) ;;
ret sum

Xor four bits (a ^ b ^ c ^ d):

ab <- xor2 (a, b) ;;
abc <- xor2 (ab, c) ;;
xor2 (abc, d)

Patterned Bind

'(_, ... , _) <- _ ;; _

Very similar to _ <- _ ;; _, except that this version names elements of pairs individually. '(x,y,z) <- foo ;; ... is equivalent to xyz <- foo ;; let '(x,y,z) := xyz in ...

You can write an underscore _ to avoid naming an element of a pair that you do not intend to use.

Examples

Add with carry, return carry and sum in reverse order:

'(sum, cout) <- addC (a, b, cin) ;;
ret (cout, sum)

Add with carry, but ignore the carry out and just return the sum:

'(sum, _) <- addC (a, b, cin) ;;
ret sum

Compose

_ >=> _

Compose two monadic functions. (f >=> g) x is equivalent to y <- f x ;; g y. Not to be confused with the analogous operation for sequential circuits, which has two equal signs, _ >==> _.

Examples

Get the third element of a Vec (Vec.hd (Vec.tl (Vec.tl v))):

(Vec.tl >=> Vec.tl >=> Vec.hd) v

Less-than-or-equal function for bits, in terms of less-than. An equivalent function in plain Coq syntax would be fun '(a, b) => inv (ltb (b, a)).

swap >=> ltb >=> inv

Alternate Bind

x >>= f

OR

f >>= x

Both are equivalent to y <- x ;; f y. This binding notation is used less frequently than the others, but still comes up occasionally.

Examples

Invert x twice (inv (inv x)):

inv x >>= inv

Circuit Notations

Optional; import with Import Circuit.Notations.

Circuit Compose

_ >==> _

Notation for Circuit.Compose. Very similar to _ >=> _, except that it composes Circuits (which may have sequential components) instead of monadic functions (guaranteed to be combinational). Comb f >==> Comb g (composition of two purely combinational circuits) is equivalent to Comb (f >=> g).

Examples

Duplicate a 1-bit signal, then invert one of the resulting wires (equivalent to fun i : signal Bit => '(i0, i1) <- fork2 i ;; not_i0 <- inv i0 ;; ret (not_i0, i1)):

Comb fork2 >==> First (Comb inv)

Duplicate a signal, and then add a delay to one of the resulting wires:

Comb fork2 >==> First Delay

Invert a bit vector signal and then feed the result to a counter:

Comb Vec.inv >==> Loop (Comb (addN >=> fork2))

Bit-Vector Notations

Import with Import Vec.BitVecNotations.

And

_ & ... & _

a & b & c & d is equivalent to Vec.and (Vec.and (Vec.and a b) c) d

Or

_ | ... |  _

a | b | c | d is equivalent to Vec.or (Vec.or (Vec.or a b) c) d

Xor

_ ^ ... ^  _

a ^ b ^ c ^ d is equivalent to Vec.xor (Vec.xor (Vec.xor a b) c) d