Page 1

Page 2

# Today

• Sequential Circuits: Registers
• Verification with observer circuits
• More connection patterns
• Multipliers
• List comprehensions
Page 3

# A quick peek at sequential circuits again

• Delay
• `delay init s`
• Delays the signal `s` by one "clock cycle".
• The output during the first "clock cycle" is `init`.
• Multiplexers
• From the Lava Library:
• `mux :: (Signal Bool,(a,a)) -> a`
Page 4

## Registers

• ```reg init (w,din) = dout
where
dout = delay init m
m = mux (w,(dout,din))
```
Page 5

# Verification

## Equivalence checking

• ```prop_Equivalent circ1 circ2 inp = ok
where
out1 = circ1 inp
out2 = circ2 inp
ok = out1 <==> out2
```
Page 6

Page 7

## Verifying properties

• We can use a SAT solver to verify that `ok` is always true
• Safety properties
• Bounded model checking
Page 8

## Verifying generic circuits

• ```prop_AdderCommutative (as,bs) = ok
where
out1 = binAdder (as,bs)
out2 = binAdder (bs,as)
ok = out1 <==> out2
```
• `smv prop_AdderCommutative` does not work!
Page 9
##### Verification → Verifying generic circuits
• ```prop_AdderCommutative_ForSize n =
forAll (list n) \$ \ as ->
forAll (list n) \$ \ bs ->
prop_AdderCommutative (as,bs)
```
• `smv (prop_AdderCommutative_ForSize 16)` works!
• See Chapter 4 in the Lava tutorial.
Page 10

## Verifying generic circuits, alternative solution

• ```prop_AdderCommutative_ForSize n =
prop_AdderCommutative (varList n "a",varList n "b")
```
• `smv (prop_AdderCommutative_ForSize 16)` works!
Page 11

# Remember Last Time

## Exercise: Zero detection

### Examples of recursively defined circuits

• First version
• assume we have a circuit that works for n bits,
• build a circuit that works for n+1 bits.
• Result: a linear chain of 2-input gates
• Second version
• assume we have a circuit that works for n bits,
• build a circuit that works for 2n bits.
• Result: a balanced trees of 2-input gates
Page 12

# Two versions of the zero detection circuit

## Linear chain

• ```zero_detect as = inv nz
where
nz = nz_detect as

nz_detect [] = low
nz_detect (a:as) = out
where
out = or2(a,out2)
out2 = nz_detect as
```

Page 13

Page 14

## Balanced tree, alternate style

• ```nz_detect [] = low
nz_detect [a] = a
nz_detect as = circ as
where
circ = halveList ->- (nz_detect -|- nz_detect) ->- or2
```
• Lava provides a compact notation for combining components without having to explicitly name all the internal signals
Page 15

# About halveList

• halveList: splits a list into two halves
• `halveList :: [a] -> ([a],[a])`
• Examples:
• ```havleList [1,2,3,4,5,6] = ([1,2,3],[4,5,6])
halveList [1,2,3] = ([1],[2,3])
halveList [1,2] = ([1],[2])
halveList [1] = ([],[1])
halveList [] = ([],[])```
• Note:
• The two halves are shorter than the whole lists, except when the input list contains less than two elements
• In recursive definitions (like nz_detect), make sure base cases prevent recursive calls for input lists with less than two elements.
Page 16

# Tree shaped circuits

• We can capture the tree pattern in nz_detect into a reusable function
• ```binTree c [] = error "binTree of empty list"
binTree c [a] = a
binTree c as = circ as
where circ = halveList ->- (binTree c -|- binTree c) ->- c
```
• New definition of nz_detect:
• ```nz_detect = binTree or2
```
• It's easier to use "canned" connection patterns than to define your own recursive function!
Page 17

## Type of `binTree`

• `binTree :: ( (a,a)->a ) -> ( [a]->a )`
• `binTree` converts a circuit with two inputs into a circuit with an arbitrary number of inputs.
Page 18

# More connection patterns

Page 19

## two f

### `two f = parl f f`

Page 20
##### More connection patterns
• ```pair :: [a] -> [(a,a)]
pair (x1:x2:xs) = (x1,x2):pair xs
pair xs = []
```
• ```unpair :: [(a,a)] -> [a]
unpair ((x,y):xys) = x:y:unpair xys
unpair [] = []
```
Page 21
##### More connection patterns
• ```riffle = halveList ->- zipp ->- unpair
```
• ```unriffle = pair ->- unzipp ->- append
```
Page 22

Page 23

Page 24

## There are even more connection patterns in the Lava library

• Add `import Lava.Patterns` at the top of the file to use them.
• Try `:browse Lava.Patterns` in the Lava interpreter.
• Combining circutis: -|-, ->-, map, row, column, grid, parl, two, ilv, ...
• Rearranging signals: halveList, append, zipp, unzipp, pair, unpair,reverse, swap, copy, riffle, unriffle, ...
• See Chapter 8 in the Lava tutorial.
Page 25

Page 26

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```

• Multiplying by a single bit is much easier than multiplying by a single decimal digit!
• Most of the work is adding the partial products.
Page 28

# Multiplication in Lava

## From the Lava library

### Multiplying by a single bit

• Using a list comprehension:
• ```bitMulti :: (Bit,[Bit]) -> [Bit]
bitMulti (a, bs) = [ and2 (a, b) | b <- bs ]
```
• Alternatively, using `map`:
• ```bitMulti (a,bs) = map and_a bs
where
and_a b = and2(a,b)
```
Page 29

## Adding up the partial products

• Remember bit order in Lava: least significant bit first
• ```multi :: ([Bit],[Bit]) -> [Bit]
multi ([],bs) = []
multi (a:as,bs) = sum
where
ps = bitMulti (a,bs)
qs = multi (as,bs)
sum = binAdder (low:qs,ps)
```
• A bit wasteful to feed a known input `low` to the adder
• Also consider `multi([a],bs)`
Page 30

# Circuit transformation

• Assume ps = p1:ps', then we have
• ```p1:ps' = bitMulti(a,bs)
sum = binAdder (low:qs,p1:ps')
```
• We can rewrite the last line to:
• ```sum = p1:binAdder(qs,ps')
```
Page 31

# Multiplication in Lava

## Adding up the partial products, version 2

•  ```multi :: ([Bit],[Bit]) -> [Bit] multi ([],bs) = [] multi (a:as,bs) = sum where p1:ps' = bitMulti (a,bs) qs = multi (as,bs) sum = p1:binAdder (qs,ps')```
• Simple circuit description, but not an optimal circuit...
• Output size?