- Sequential Circuits: Registers
- Verification with observer circuits
- More connection patterns
- Multipliers
- List comprehensions

- Delay
`delay`

`init``s`- Delays the signal

by one "clock cycle".`s` - The output during the first "clock cycle" is

.`init`

- Delays the signal

- Multiplexers
- From the Lava Library:
`mux :: (Signal Bool,(a,a)) -> a`

- From the Lava Library:

reg init (w,din)

**=**dout**where**dout**=**delay init m m**=**mux (w,(dout,din))

prop_Equivalent circ1 circ2 inp

**=**ok**where**out1**=**circ1 inp out2**=**circ2 inp ok**=**out1 <==> out2

- We can use a SAT solver to verify that
`ok`

is always true - Safety properties
- Bounded model checking

prop_AdderCommutative (as,bs)

**=**ok**where**out1**=**binAdder (as,bs) out2**=**binAdder (bs,as) ok**=**out1 <==> out2`smv prop_AdderCommutative`

does*not*work!

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.

prop_AdderCommutative_ForSize n

**=**prop_AdderCommutative (varList n "a",varList n "b")`smv (prop_AdderCommutative_ForSize 16)`

works!

- 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

- assume we have a circuit that works for
- Second version
- assume we have a circuit that works for
`n`bits, - build a circuit that works for 2
`n`bits. - Result: a balanced trees of 2-input gates

- assume we have a circuit that works for

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

zero_detect as=inv nzwherenz=nz_detect as nz_detect []=low nz_detect [a]=a nz_detect as=outwhere(as1,as2)=halveList as out1=nz_detect as1 out2=nz_detect as2 out=or2(out1,out2)

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

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

- The two halves are shorter than the whole lists,

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

`binTree`

`binTree :: ( (a,a)->a ) -> ( [a]->a )`

`binTree`

converts a circuit with two inputs into a circuit with an arbitrary number of inputs.

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

`two f = parl f f`

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 []**=**[]

riffle

**=**halveList ->- zipp ->- unpairunriffle

**=**pair ->- unzipp ->- append

`ilv f`

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

`ilv (ilv (ilv f))`

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

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

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.

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

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

- 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')

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?