How to Use the Lava System

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:

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:

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):

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

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

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:

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:

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):

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:

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:

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:

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:

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.

• LavaIntro.hs:81:16:
      Couldn't match expected type `[Bool]'
             against inferred type `(Bool, Bool)'
      In the first argument of `and', namely `(a, b)'
      In the expression: and (a, b)
      In the definition of `mistake':
          mistake a = and (a, b)
                    where
                        b = not a
  

  This is a type error. The message points you to the line where the system thinks the error is. This is often correct, but not always. In this case, we mistakenly used and instead of and2. Since and is a haskell function which takes a list of booleans and return the conjunction of them all, you get a type error if you use it instead of and2.

• ERROR "adders.hs" (line 19): Type error in function binding
*** Term           : carryIn
*** Type           : Signal Bool -> Signal Bool
*** Does not match : Signal Bool


  This is another type error. It occured when we forgot the low in the line line carryIn = delay low carryOut in the definition of seqAdd. The function delay takes two argument, and since haskell is a functional language, it is ok to just apply it one argument. However, the result is another function, which takes one argument (the one we didn't supply). That would make carryIn a function, but since we use it as a signal in the line above, that is not possible. Hence, the system says that the type of carryIn should be Signal Bool (i.e. it should be a signal) and not Signal Bool -> Signal Bool (which is a function which takes a boolean signal and gives you back a boolean signal).

• ERROR "adders.hs" (line 6): Undefined variable "xor"
  

  In this example, we wrote xor instead of xor2. There is nothing defined with the name xor, and therefore the system says that xor is undefined. It may be confusing that the system says "Undefined variable", when it is obviously a function or a circuit. However, in a higher order language (as haskell is), functions are variables too.

• ERROR "adders.hs" (line 5): Undefined constructor function "HalfAdd"

  Only constructors may start with a capital letter. If you don't know what a constructor is, don't bother, you won't need them in this course. The solution to this problem is to use a name that starts with a lowercase letter.

• Program error: combining incompatible structures

  This error occured when we typed the following in the system: simulateSeq (row halfAdd) [(high,[low,low,high,high]),(high,[low,high,high])]. The error here is that we force the adder to be of size four in the first cycle, and then only supply it with three input signals in the second. Of course, the actual size of the circuit may not change during the simulation. If the circuit is of a specific size at one point, it must have that size throughout the whole simulation.

• ERROR "adders.hs" (line 5): Definition of variable "halfAdd" clashes with import

  There is something in our code with the same name as something in an imported module. In our case, the problem arose when we tried to import Lava.Arithmetic in the file with the adders examples above. It turns out that both halfAdd, and fullAdd are predefined in the module Lava.Arithmetic. The solution to this problem is to rename our circuits, or to explicitly exclude the functions from the import:

  import Lava.Arithmetic hiding (halfAdd,fullAdd)
  
  
• If you load the module Patterns into the Lava system, and type simulate riffle [1..16] you get the following strange error message:
  ERROR: Unresolved overloading
*** Type       : (Enum a, Num a, Generic a) => [a]
*** Expression : simulate riffle (enumFromTo 1 16)


  Haskell has two types of integers, namely Int (finite, 32-bit integers) and Integer (for which the only upper bound is the memory of the computer). If you just type in a number, hugs will not be able to determine which of these two types you mean. The solution is to tell this to hugs. You can explicitly force a value (say x) to be of type t by typing x::t instead of just x. In this case we can say either of the following:

  • simulate riffle [1..16::Signal Int]
  • simulate riffle [1..16]::[Signal Int]