How to Use the Lava System (2010)

The best way to use Lava is to run it in GHCi, which the interactive system for Haskell included in the Haskell Platform. You start it by typing ghci, optionally followed by a filename. It is rather convenient to have the source code open in a text editor (such as gedit or emacs) in one window, and ghci in another window at the same time.

Here is an example of a source file in emacs:

Syntax highlighting in Emacs

If you don't have syntax highlighting for Lava (Haskell) programs in emacs, and want to have it, look at Haskell Mode for Emacs. A quick guide to short commands in emacs is available here.

Working with Lava

Since lava files are really Haskell files, they have .hs as extension. If your file is called adders.hs, you can load it into the lava system entering the command :load adders.hs in GHCi (:load can be abbreviated to :l). You can always reload the latest file you loaded by typing :reload or :r. You can get a list of more commands by typing :?, but you will not need more than the ones described here.

Now we can test this circuit in the lava system. The text in italics below is the text that the user enters:

Main> simulate halfAdd (low,high)
simulateSeq halfAdd [(low,low),(low,high),(high,low),(high,high)]

Since this is a combinational circuit, simulateSeq gives the same result as a number of calls to simulate. Let's make a sequential circuit to test it on. Here is a serial:

import Lava

halfAdd (a,b) = (sum,carry)
    sum = xor2 (a,b)
    carry = and2 (a,b)

fullAdd (carryIn, (a,b)) = (sum, carryOut)
    (sum1, carry1) = halfAdd (a,b)
    (sum, carry2) = halfAdd (carryIn, sum1)
    carryOut = xor2 (carry1, carry2)

seqAdd (a,b) = sum
    (sum, carryOut) = fullAdd (carryIn, (a,b))
    carryIn = delay low carryOut

We can now reload the file with the new circuitry into the lava system by typing :r. We try to add the numbers 13 (01101) and 6 (00110):

Main> simulateSeq seqAdd [(high,low),(low,high),(high,high),(high,low),(low,low)]

The answer is indeed 19 (10011, remember that we write binary numbers in the opposite direction of how sequential circuits represent them).

Simpler notation

Testing the sequential adder in the example above required the input to be a list of pairs. However, it would be a lot easier if this was a pair of lists instead. Indeed, there is a standard haskell function, that takes two lists (which is not a pair of lists, but close enough) and produces a list of pairs. The name of this function is zip. So, we can now replace the example above with:

Main> simulateSeq seqAdd (zip [high,low,high,high,low] [low,high,high,low,low])

If we want to use the connection patterns presented in the lectures, we can import the module Lava.Patterns. We just add the line import Lava.Patterns to the source file, directly below the line import Lava. If you want to see what functions are exported from a Lava module, you can use the :browse command in GHCi, e.g. :browse Lava or :browse Lava.Patterns.

Here is an example of an inserter, implemented using connection patterns:

import Lava
import Lava.Patterns

comp (a,b) = (minab, maxab)
    minab = imin (a,b)
    maxab = imax (a,b)

insert (x,xs) = (ys,y)
    (ys,y) = row comp (x,xs)

testInsert = simulate insert (3, [1..5])

This inserter uses the row pattern, and takes the item to be inserted as the single input at the left. At the top, it takes the (sorted) input list of items. The new list is outputted at the bottom, but since it must have the same length as the input list, the largest element is outputed to the right.

In the example above we gave a name to the test (testInsert), and hence we only have to type testInsert to perform this test in the lava system.

Hints and Well known pitfalls

Trying to make circuits where the structure depends on the input values

A very common mistake that beginners do to try to make circuits that reconfigure themselves for different inputs. Especially people that already know haskell tend to do this. Consider the following, erroneous, piece of code. It contains two erroneous attempts to implement a unit which, if its first input is high outputs the conjunction of the other two inputs, and their disjunction otherwise:

--Warning: the following two components are erroneous

import Lava

andOrOr :: (Signal Bool, (Signal Bool, Signal Bool)) -> Signal Bool
andOrOr (high, (a,b)) = and2 (a,b)
andOrOr (low, (a,b)) = or2 (a,b)

andOrOr2 :: (Signal Bool, (Signal Bool, Signal Bool)) -> Signal Bool
andOrOr2 (selector, (a,b)) = if selector == high
                             then and2(a,b)
                             else or2(a,b)

Simulation reveals that andOrOr always works like an and gate, and andOrOr2 most often works like an or gate. The error in both cases is that it is an attempt to make a piece of hardware that consists of an and-gate if the value of the first input signal is high, and an or-gate if the value of the first input signal is low. Hence, the physical structure of the circuit would depend on what values that input signals have. Clearly, that's not possible.

In andOrOr, there seems to be pattern matching going on at first. If the input signal is high one may expect the first definition to be chosen, otherwise the second one. However, high is not a constructor - it begins with a lowercase letter! Thus, high matches anything, so if you try to use high in the circuit, it does not denote the constantly high signal, but the signal that was passed in as an argument. That is also why andorOr always works like an and gate - the first definition always matches the input.

In andOrOr2, it seems like we investigate if the selector is high, and then act accordingly. However, what we're actually comparing is that if the signal called selector is the same signal as high - you might look at this as we investigate whether they have the same driver, or possibly even whether they are the same physical wire. Therefore, if we give the signal high as the selector argument, this comparison will evaluate to true, but for any other signal (e.g. and2(high,high)), the comparison will render false, even if the signal has a constantly high value.

The correct solution to this problem is to use the builtin multiplexer, mux:

correctAndOrOr :: (Signal Bool, (Signal Bool, Signal Bool)) -> Signal Bool
correctAndOrOr (selector, (a,b)) = out
  conj = and2(a,b)
  disj = or2(a,b)
  out = mux (selector, (conj, disj))

Note that in this implementation it is clear that both an and gate and an or gate are always present.

Getting the higher order functions right

The following piece of code can be found in the lava tutorial (chapter 4):

prop_Equivalent circ1 circ2 a = ok
    out1 = circ1 a
    out2 = circ2 a
    ok   = out1 <==> out2

Many of you have realized that prop_Equivalent can be used to verify that the two mux'es in the lava lab are equivalent. However, it's common to attempt to write something like the following:

Warning, erroneous code:

satzoo prop_Equivalent mux1 mux2

When the haskell system sees something like this it assumes that the first identifier (i.e. satzoo) is a function, and that all the following identifiers (i.e. prop_Equivalent mux1 mux2) are arguments to that function. However, mux1 and mux2 are not arguments to satzoo, but rather to prop_Equivalent. What you want to write is the following:

Correct code:

satzoo (prop_Equivalent mux1 mux2)

Here, (prop_Equivalent mux1 mux2) returns a circuit (which, in haskell terms, is a function from some signals to some other signals), which is given as an argument to satzoo.

A pair of lists or a list of pairs?

When you make a row foo, the circuit you get takes a list of inputs on the top. This list has element of whatever type the top inputs of foo have. Specifically, when you write raw fullAdd, you get a circuit which takes in a list of pairs of bits on the top, since fullAdd takes a pair of bits. Many of you would probably prefer your adder to take two list of bits as inputs instead of the single list of pairs. There are two useful haskell functions, that can be used in situations like these: zip and unzip. The function zip takes two lists (not as a pair) of pairs, and returns a list of pairs, while unzip takes a list of pairs and gives back a pair of lists. To make the adder that takes a pair of lists instead of a list of pairs, you can write the following:

adder (cIn, (as, bs)) = (rs, cOut)
  abs = zip as bs
  (rs, cOut) = row fullAdd (cIn, abs)

Distributing a signals to all elements in a row

Sometimes we would like to make a row of components, where one specific signal is distributed to all components. This can, for instance, be a reset signal, or some sort of control signal. Suppose, for instance, that we have a circuit called resettable that takes a carry in, a reset signal, and some parameter a in the following shape: (cIn, (reset, a)). Now, if we just make a row resettable, we get back a circuit which takes in one reset signal for each component. This is probably not what we wanted. Instead, we might want to do something like the following:

rowOfResettable (cIn, (reset, as)) = (rs, cout)
  resettable' (cIn2, a) = resettable (cIn2, (reset, a))
  (rs, cout) = row resettable' (cIn, as)

What we do here is that we define a local version of resettable (which we call resettable'), where we have already connected the reset signal to the reset signal of rowOfResettable. Then we make a row out of that component instead. It is not necessary to add the character 2 to cIn2, but I did it here to make it clearer that cIn and cIn2 are different signals.

Rows without carries

There is a connection pattern which is similar to row, except that there is no carry chain. It is called map. It's really not a special lava function, but is defined in the haskell standard prelude, and has a more general purpose. That's why it's name is map, and not bus or something more hardware-like.

Error messages

The error messages of the lava systems can sometimes be hard to interpret, especially if you don't know haskell. Here are a few classical ones. If you have problems with error messages, you can always mail us.