Functional Languages for Synchronous Hardware Design and Verification

Final Examination Questions

Gordon J. Pace

September 2006

Question 1:

Implement an n-bit multiplier in Lava (using a design of your choice). Use SMV and Lava to specify and verify that multiplying a 4-bit number by an even number always gives an even number.

Question 2:

Design a four-bit accumulator which has two inputs: update (one bit) and value (four-bits), and one output sum (four bits). The output starts off at 0, and is incremented by value whenever update is true.

Using the accumulator, implement a 4-bit counter, which starts off outputting zero, and increments its output with every clock tick (resetting to zero when it overflows).

Question 3:

Modify the compiled imperative language with emit given in part 4 of the course to also count the number of emits (using a 4-bit unsigned integer) happening at that instant of time eg at the initial moment, (emit; emit || emit) should output 3.

Add also an accumulator, which counts the total number of emits sent by the program.

Finally, make programs terminate whenever the program has output more than 10 emit signals (ignore overflows).

Question 4:

Explain and implement in Lava another parallel prefix network circuit implementation (different than the ones given in the slides). You may find this link useful.

Verify that with an and gate, your four-input prefix network is equivalent to the naive one, and the Sklansky one.

Submit, or send any questions to firstname.surname(at)

The deadline for the solutions is Friday, 20 October 2006.