One-week intensive course on
Hardware Description Languages for Synchronous Circuits

Gordon Pace, Koen Claessen

Exercises: Designing Circuits in Lava

Wednesday 6th September

1. A Stack
Yesterday and the day before yesterday, we have seen how to design a stack, and how to describe it in Verilog. Today, you are going to describe the stack structurally in Lava.

Exercises
a. Describe the stack you designed Monday, that is the stack where the data element is one bit, and the size of the stack is 4. You may add any of the extension outputs if you like.

b. Change your description so that you can store data elements larger than one bit.

c. Change your description so that it has an extra parameter, the size of the stack.

2. (*) Verification
We are now ready to formulate and maybe prove properties about the stack. The kind of properties we will state are safety properties; properties which should hold at all times.

Exercises
a. Express the property from the Monday question 4d. Test if it is correct. Then verify it using vis.

b. Express, test and verify the property that if you push an element on the stack, and then pop, the top element has not changed. What goes wrong? How can you fix this?