Page 1

Hardware description in Functional Languages and Introduction to Lava

Hardware Description and Verification

Thomas Hallgren


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

Hardware Description in Functional Language

Page 6

Hardware Description in Functional Languages

Page 7

What is Lava?

Lava is a hardware description language embedded in Haskell

Page 8
What is Lava?

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

Page 9

Lava Documentation

Page 10

A First Example: a Half Adder

[Half Adder]

Page 11

Half Adder implementation

[Half Adder]

Page 12

Half Adder in VHDL

Page 13

Half Adder in Lava

Page 14

Half Adder Interface

Page 15
Half Adder Interface
Page 16

Simulating Lava circuits

Page 17

Logical Gates in the Lava library

Page 18

Half Adder in Lava, alternate versions

Page 19

A Second Example: a Full Adder

[Full Adder]

Page 20

Full Adder implementation

[Full Adder]

Page 21

Full Adder in VHDL

Page 22

Full adder in Lava

Page 23

Full Adder Interface

Page 24

A third example: a Ripple Carry Adder

Page 25

Ripple Carry Adder in VHDL

Page 26

Ripple Carry Adder in Lava

Page 27

Ripple Carry Adder Interface

Page 28

Lists and Connection patterns

Page 29

Simulating Lava circuits

Page 30

Generating VHDL from Lava circuits

Page 31

VHDL for combinational circuits

Page 32

Formal Verification of Lava circuits

Page 33

FV example

Page 34

Equivalence Checking

What does prop_Equivalent do?

Creates a bigger circuit

Page 35

Equivalence checking

Page 36