Page 1

Hardware description in Functional Languages and Introduction to Lava

Hardware Description and Verification

Thomas Hallgren

2010-04-26

Page 2

Where are we?

Page 3
Where are we?

Second half of the course: a peek at what comes next...

Page 4

Guests Lectures

Page 5

Better Hardware Description Languages?

Page 6

Hardware Description in Functional Languages

Page 7
Hardware Description in Functional Languages
Page 8

What is Lava?

Lava is a hardware description language embedded in Haskell

Page 9
What is Lava?

Lava is essentially a Haskell library from which you can import types and functions for

Page 10

Lava Documentation

Page 11

A First Example: a Half Adder

[Half Adder]

abcs
0000
0101
1001
1110

Page 12

Half Adder implementation

[Half Adder]

abcs
0000
0101
1001
1110

Page 13

Half Adder in VHDL

Page 14

Half Adder in Lava

Page 15

Half Adder Interface

Page 16

What Haskell types does Lava use to represent circuits?

Page 17

Half Adder Interface

Page 18

Simulating Lava circuits

Page 19

Logical Gates in the Lava library

Page 20

Half Adder in Lava, alternate versions

Page 21

A Second Example: a Full Adder

[Full Adder]

Page 22

Full Adder implementation

[Full Adder]

Page 23

Full Adder in VHDL

Page 24

Full adder in Lava

Page 25

Full Adder Interface

Page 26

A third example: a Ripple Carry Adder

Page 27

Ripple Carry Adder in VHDL

Page 28

Ripple Carry Adder in Lava

Page 29

Ripple Carry Adder Interface

Page 30

Lists and Connection patterns

Page 31

Simulating Lava circuits

Page 32

Generating VHDL from Lava circuits

Page 33

VHDL for combinational circuits

Page 34

Formal Verification of Lava circuits

Page 35

FV example

Page 36

Equivalence Checking

What does prop_Equivalent do?

Creates a bigger circuit

Page 37

Equivalence checking

Page 38

Conclusion