The best way to use Lava is to run it in GHCi, which the
interactive system for Haskell included in the
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,
ghci in another window at the same time.
Here is an example of a source file 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.
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
You can get a list of more commands by typing
:?, but you will not need more than the ones described
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):
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).
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
Lava.Patterns. We just add the line
import Lava.Patternsto 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
:browsecommand in GHCi, e.g.
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.
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.
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.
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,
Note that in this implementation it is clear that both an and gate and an or gate are always present.
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:
Warning, erroneous code:|
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,
mux2 are not arguments to
satzoo, but rather to
prop_Equivalent. What you want to write is the following:
(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
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:
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:
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
cIn2 are different signals.
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.
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
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
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
Bool (i.e. it should be a signal) and not
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
simulateSeq (row halfAdd)
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
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
fullAdd are predefined in
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)
Patternsinto 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: