Page 1

Lava 3

Hardware Description and Verification

Thomas Hallgren

2010-05-04

Page 2

Today

Page 3

A quick peek at sequential circuits again

Page 4
A quick peek at sequential circuits again

Registers

Page 5

Verification

Equivalence checking

Page 6
Verification

Generalizing...

Page 7
Verification

Verifying properties

Page 8
Verification

Verifying generic circuits

Page 9
Verification → Verifying generic circuits
Page 10
Verification

Verifying generic circuits, alternative solution

Page 11

Remember Last Time

Exercise: Zero detection

Examples of recursively defined circuits

Page 12

Two versions of the zero detection circuit

Linear chain

Page 13
Two versions of the zero detection circuit

Balanced tree

zero_detect as = inv nz
  where
    nz = nz_detect as

nz_detect [] = low
nz_detect [a] = a
nz_detect as = out
  where
    (as1,as2) = halveList as
    out1 = nz_detect as1
    out2 = nz_detect as2
    out = or2(out1,out2)


Page 14
Two versions of the zero detection circuit

Balanced tree, alternate style

Page 15

About halveList

Page 16

Tree shaped circuits

Page 17
Tree shaped circuits

Type of binTree

Page 18

More connection patterns

parl f g

parl f g = halveList ->- (f -|- g) ->- append

Page 19
More connection patterns

two f

two f = parl f f

Page 20
More connection patterns
Page 21
More connection patterns
Page 22
More connection patterns

Interleave


ilv f

ilv circ = unriffle ->- two circ -> riffle

Page 23
More connection patterns → Interleave


ilv (ilv (ilv f))

Page 24
More connection patterns

There are even more connection patterns in the Lava library

Page 25

Multipliers

Page 26

Multiplication in base 10

Example

      1 2 3 4
   ×    5 6 7
   ──────────
      8 6 3 8 
    7 4 0 4
+ 6 1 7 0      
─────────────
  6 9 9 6 7 8

Page 27

Multiplication in base 2

Example

      1 0 1 1
   ×    1 0 1
   ──────────
      1 0 1 1 
    0 0 0 0
+ 1 0 1 1      
─────────────
  1 1 0 1 1 1

Page 28

Multiplication in Lava

From the Lava library

Multiplying by a single bit

Page 29
Multiplication in Lava

Adding up the partial products

Page 30

Circuit transformation

Page 31

Multiplication in Lava

Adding up the partial products, version 2