Page 1

Lava 3

Hardware Description and Verification

Thomas Hallgren

2009-05-05

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

Remember Last Time

Exercise: Zero detection

Examples of recursively defined circuits

Page 11

Two versions of the zero detection circuit

Linear chain

Page 12
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 13
Two versions of the zero detection circuit

Balanced tree, alternate style

Page 14

About halveList

Page 15

Tree shaped circuits

Page 16
Tree shaped circuits

Type of binTree

Page 17

More connection patterns

parl f g

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

Page 18
More connection patterns

two f

two f = parl f f

Page 19
More connection patterns
Page 20
More connection patterns
Page 21
More connection patterns

Interleave


ilv f

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

Page 22
More connection patterns → Interleave


ilv (ilv (ilv f))

Page 23
More connection patterns

There are even more connection patterns in the Lava library

Page 24

Multipliers

Page 25

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 26

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 27

Multiplication in Lava

From the Lava library

Multiplying by a single bit

Page 28
Multiplication in Lava

Adding up the partial products

Page 29

Circuit transformation

Page 30

Multiplication in Lava

Adding up the partial products, version 2