- Take a look at the schedule
- First half of the course: Industry standard languages and tools
- VHDL
- PSL
- Jasper Gold

- Hardware designs are becoming more and more complex
- There is a need to control low-level details even at high levels of design
- Better languages are needed
- Transfer progress in programming languages to Hardware Description Languages

- Monday, May 4
- Wolfgang Kunz (TU Kaiserslautern): SoC verification

- Tuesday, May 12
- Satnam Singh (Microsoft): current trends, FPGAs in Bluespec

- Thursday, May 14
- Emil Axelsson, Joel Svensson (Chalmers)

- Advantages of Functional Languages:
- Provide a concise notation
- Powerful abstraction mechanisms to deal with complexity
- Good support for generic hardware descriptions
- Equational style supports reasoning and rewrites

- What are people doing?
- See the HFL workshop

- Examples
- Lava (Chalmers)
- Lava (Xilinx)
- Hawk
- Bluespec

- In this course
- Lava (Chalmers)

- Haskell is a purely functional programming language.
- Like VHDL, Haskell is a strongly typed language.
- A compiler (GHC) and two interactive systems (Hugs, ghci) are available.
- Everything about Haskell: www.haskell.org.

- describing circuits,
- simulating circuits,
- feeding circuits to other tools, e.g. for formal verification
- We will use SMV

- The Lava Tutorial introduces Lava without requiring previous knowledge of Haskell.
- There is also the guide How to Use the Lava System.
- Instructions for accessing the tools have recently been updated.

**entity**halfAdder**is****port**(a,b :**in**bit; sum,carry :**out**bit);**end**halfAdder;**architecture**ha_beh**of**halfAdder**is****begin**sum**<=**a**xor**b; c_out**<=**a**and**b;**end**ha_beh;- Just to have something to compare to

halfAdder (a, b)

**=**(sum, carry)**where**sum**=**xor2 (a, b) carry**=**and2 (a, b)- Note: it's a direct transcription of the circuit diagram!

halfAdder

**::**(**Signal****Bool**,**Signal****Bool**)**->**(**Signal****Bool**,**Signal****Bool**) halfAdder (a,b)**=**(sum,carry)**where**...- The first line is the type signature for halfAdder.
- A circuit is represented as a
**function**from input to output

: a function with input of type`A`->`B``A`and output of type`B``(`

: a pair. Pairing allows several signals to be grouped together and treated as one signal.`A`_{1}`,``A`_{2}`)``Signal`

: signals carrying values of type`A``A``Bool`

: boolean values,`False`

or`True`

- Introducing a shorter name for the type of boolean signals
**type****Bit****=****Signal****Bool**low, high**::****Bit**

- We can now write
halfAdder

**::**(**Bit**,**Bit**)**->**(**Bit**,**Bit**) halfAdder (a,b)**=**(sum,carry)**where**...

- Simulating a single cycle
`simulate`

`circuit``input`

- Example:
`simulate halfAdder (low,high)`

(high,low)`simulate halfAdder (high,high)`

(low,high)

- More later

- From Appendix A (Quick Reference) in the Lava Tutorial:
id, inv

**::****Bit****->****Bit**and2, nand2, or2, nor2, xor2, equiv, impl**::**(**Bit**,**Bit**)**->****Bit**<&>, <|>, <#>, <=>, ==>**::**(**Bit**,**Bit**)**->****Bit**`a <&> b`

is the same as`and2 (a,b)`

, etc.

halfAdder (a, b)

**=**(sum, carry)**where**sum**=**xor2 (a, b) carry**=**and2 (a, b)- In functional languages, you can substitute equals for equals:
halfAdder (a, b)

**=**(xor2 (a,b),and2(a,b))- Using the alternative infix operators:
halfAddder (a,b)

**=**(a <#> b, a <&> b)

**entity**fullAdder**is****port**(a,b,carryIn :**in**bit; sum,carryOut :**out**bit);**end**fullAdder;**architecture**fa_beh**of**fullAdder**is****signal**s1,c1,c2 : bit;**begin***-- fa_beh*ha1:**entity**work.halfAdder**port****map**(a, b, s1, c1); ha2:**entity**work.halfAdder**port****map**(carryIn, s1, sum, c2); xor1: carryOut**<=**c1**xor**c2;**end**fa_beh;- A structural description that refers to the previously defined entity halfAdder.

fullAdder (carryIn, (a,b))

**=**(sum, carryOut)**where**(s1, c1)**=**halfAdder (a, b) (sum, c2)**=**halfAdder (carryIn,s1) carryOut**=**xor2 (c2, c1)- Again, it should be a direct transcription of the circuit diagram.
- Using previously defined components is just as easy as using basic gates.

fullAdder

**::**(**Bit**,(**Bit**,**Bit**))**->**(**Bit**,**Bit**) fullAdder (carryIn, (a,b))**=**(sum, carryOut)**where**...- The first line is the type signature of function fullAdder.
- It is inferred automatically if you leave it out.

- A row of full adders form a ripple carry adder
- We will write a generic implemention

**entity**rippleCarryAdder**is****generic**(n : natural);**port**( carryIn :**in**bit; a, b :**in**bit_vector(n-1**downto**0); sum :**out**bit_vector(n-1**downto**0); carryOut :**out**bit);**end**rippleCarryAdder;**architecture**rca_beh**of**rippleCarryAdder**is****signal**c : bit_vector(0**to**n);**begin**c(0)**<=**carryIn; adders:**for**i**in**0**to**n-1**generate****begin**bit :**entity**work.fullAdder**port****map**(c(i),a(i),b(i),sum(i),c(i+1));**end****generate**; carryOut**<=**c(n);**end**rca_beh;- A structural description that refers to the previously defined entity fullAdder.

rippleCarryAdder (carryIn, (as,bs))

**=**(sum,carryOut)**where**(sum,carryOut)**=**row fullAdder (carryIn,zipp (as,bs))`row`

is a*connection pattern*that does exactly what we need here.`zipp`

takes care of pairing up the bits at corresponding positions in the two input bit vectors`as`

and`bs`

.

rippleCarryAdder

**::**(**Bit**,([**Bit**],[**Bit**]))**->**([**Bit**],**Bit**) rippleCarryAdder (carryIn, (as,bs))**=**(sum,carryOut)**where**(sum,carryOut)**=**row fullAdder (carryIn,zipp (as,bs))- [
`A`]: lists of values of type`A`. Examples of lists:`[]`

(empty list)`[low,high,low,low] :: [Bit]`

`[(low,high),(low,low)] :: [(Bit,Bit)]`

`domain`

enumerates all values of a finite type

- List are used both for sequences in time and for parallel signals (busses).
- Length can be arbitrary and is not indicated in the type.

- Rearranging input:
`zipp :: ([a],[b]) -> [(a,b)]`

, where`a`and`b`are arbitrary types`unzipp :: [(a,b)] -> ([a],[b])`

- Replicating circuits:
`map :: (a->b) -> ([a] -> [b])`

`row :: ((c, a) -> (b, c)) -> (c, [a]) -> ([b], c)`

- It's easy to define new connection patterns in Lava

- Single cycle
`simulate`

`circuit``input`

- Simulating a sequence
`simulateSeq`

`circuit``list_of_inputs`

- Examples:
`simulate fullAdder (high,(low,high))`

(low,high)`simulate rippleCarryAdder (low,([low,high],[high,high]))`

([high,low],high)`simulateSeq fullAdder domain`

`[(low,low),(high,low),(high,low),(low,high),(high,low),(low,high),(low,high),(high,high)]`

- In the simplest case
writeVhdl "fullAdder" fullAdder

- Assigning names to the inputs
writeVhdlInput "fullAdder" fullAdder (var "carryIn",(var "a",var "b"))

- Assigning names also to the outputs
writeVhdlInputOutput "fullAdder" fullAdder (var "carryIn",(var "a",var "b")) (var "sum",var "carryOut")

- Generic circuits are not supported, so you need to pick a size
writeVhdlInputOutput "rippleCarryAdder" rippleCarryAdder (var "carryIn",(varList 8 "a",varList 8 "b")) (varList 8 "sum",var "carryOut")

- The VHDL translator assumes all components need a clock signal. There is a newer version of the translator that allows you to omit the clock.
- Put
`import VhdlNew08`

in your source file. - Add
`NoClk`

to the end of the function name - Example
writeVhdlNoClk "fullAdder" fullAdder

`smv`

`property`- For verifying safety properties, the
`property`can a circuit with- a number of inputs of fixed size
- a single boolean output

- For verifying generic circuits, a size has to be chosen...

- Our own implementation of exclusive or:
xor (a,b)

**=**(a <|> b) <&> inv (a <&> b)

- Specifying correctness:
prop_xor

**=**prop_Equivalent xor xor2

- Exhaustive testing
test_xor

**=**simulateSeq prop_xor domain

- Formal verification using SMV
vrfy_xor

**=**smv prop_xor

- includes the two circuits to be checked for equivalence
- feeds the same input to both circuits
- compares the output

- Checking a specific circuit:
prop_xor (a,b)

**=**ok**where**out1**=**xor (a,b) out2**=**xor2 (a,b) ok**=**out1 <==> out2

- We can capture this pattern in a more general function:
prop_Equivalent circ1 circ2 inp

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

**=**prop_Equivalent xor xor2

- The examples from this lecture:
- Next
- Sequential circuits
- Connection patterns
- Multipliers
- Parallel prefix
- Wired and Obsidian