Hardware Description and Verification TDA956, LP4, VT2008

News and Updates

  • (080824) The retake of the Lava Take Home exam is now up on the assignments page. Get in touch if you have problems.

  • (080808) Note that the written reexam is on Aug. 28 morning in the V building. Only ONE student is currently registered for this, and I was expecting at least two :) So you should register if you plan to take the exam. There will also be a new Lava take home exam during that same exam week. Please mail Mary (ms at chalmers.se) now if you want to take that. I will plan to put it up on Aug. 24.

  • (080608) I have finished marking the written exams. I am pleased to say that everyone who sat the written exam passed it :)

  • (080526) This is a short study guide, to help with preparation for friday's written exam. It refers to the written exam from 2003 and partial solutions. Here are also partial solutions to Lava parts of the exam.

  • (080522) On p. 4 of the pdf file for the take home exam, replace {\tt wrap2} by wrap2. (I put up a new version with this fixed.)

  • (080522) One of the students asked me about the number of points for each task on the take home exam. The following is the initial assignment of points: A1 and A2 3 points each, A3 4 points, A4 2 points, A5 3 points, A6 4 points, A7 6 points, A8 5 points. I reserve the right to change this assignment of points to tasks, but not in a way that will reduce the grade of a student. So, my suggestion for order of tasks would be A1, A2, A3, A4, A7, A6, A5, A8, but now you have the info. to make your own choice. This supersedes my previous attempt to guide you about which tasks to attempt.

  • (080520) Because some of you are under pressure from another project deadline, and a few are really struggling with the tasks on the take home exam, I have decided to 1) Extend the deadline to sunday at 18:00 and 2) ask that you do A1 to A3, A7 and ONE of (A4 or A6) to pass. Keep an eye on this news page in case there are general hints that I decide to post in response to questions.

  • (080519) I also added a few more example runs of functions to Efile08.hs (and for the second time fixed a typo right at the end, see saturday's news. Argh).

  • (080519) As promised, I have put up the description of the masters thesis project at Saab Space. See top of the Links page.

  • (080519) In response to some questions from a student, I have modified the take home exam to contain a little extra explanation in the pdf file, and have added some more info. (mostly example runs of functions) to the Haskell file. What you are asked to do is completely unchanged. But please fetch the two new files from the exam web page. The new pdf file has date May 18 on the front.

  • (080517) I noticed a typo right at the end of Efile08.hs (file associated with the take home exam). I have fixed it and you should download a new version of the file if you dowloaded your version before 9.49 on saturday morning.

  • (080516) The Lava take home exam is now available. See the Assignments page.

  • (080506) Some of you have asked about tasks A10 and A11 on the Lava lab. I was not clear about this, but you should only attempt these extra tasks if you have completed A1 to A9. (I will modify the Lab PM accordingly, but please also spread the word.) For the lab, the "extra credit" will not take the form of extra marks to add to your total marks, but rather "a good point in your favour" that I may use to raise your grade if you are at a borderline.

  • (080506) There is no lecture today, but at 13.15 there is a supervised lab in room 6225. You should be getting started on the Lava Lab. Also, don't forget thursday's lecture by Wolfgang Kunz (an outstanding researcher who is giving an invited lecture).

  • (080430) The mid-course course evaluation meeting was held today and here are the minutes of the meeting.

  • (080430) There will be no supervised labs this thursday and friday as they are holidays. Next week and the week after (weeks 19 and 20) there will be lab supervision on thursday 15-17 and friday 13-15 in room 3507.

  • (080430) The Lava lab is available on the Assignments page. Those who are not familiar with Haskell should start by reading the Lava Tutorial and doing the exercises given there. If you have problems, mail Mary and Joel (not Emil because his hours on the course are used up).

  • (080430) On the Tools page, we have put a version of Lava for Linux and related instructions, in case you want to put Lava on your own computer. We'll put a Windows version there once we have one working satisfactorily.

  • (080421) The specification of the fifo is not complete. This means that you have to interpret it somehow. I suggest that you pick the interpretation that gives you the simplest code/properties.

  • (080421) The comment in fifoRemoved.vhdl said that only rIn and outputs should be assigned. But of course, you can also use local variables in the process. Furthermore, the comment is really just a hint to avoid some problems that students have got into in previous years, you are free to do it differently if you want.

  • (080418) The take-home exam is now available.

  • (080417) Important:The assignments should be submitted through the Fire system.

  • (080415) Mary has lost her voice completely, so tomorrow's lecture on CTL model checking is moved to tuesday next week, while the BMC and SAT-based verification lecture is moved to thursday. There was some slack, so this is not a problem for the overall course plan.

  • (080415) The file stopwatchRemoved.vhdl has been updated with a reset input to the state machine (the old reset output has been renamed to countReset). This signal should be used to put the design in a legal state. Note that this is not necessarily a problem for all of you, but we encourage you to use a proper reset just in case. More info can be found on the Jasper Gold page.

  • (080415) The Jasper Gold page has been updated with information about reset, preconditions and type constraints. This information is important for the formal verification in the first lab.

  • (080414) The given statemachine entity is not sufficient for verification with Jasper Gold; it's lacking a reset input that can be used to put the circuit in a well-defined state.

  • (080410) The slides from the lecture by Řystein Kolsrud (from Jasper) on an Intro. to industrial formal verification using JasperGold are now available on the schedule page.

  • (080408) For those having trouble logging in to the servers, new accounts will be available at the lecture today (tuesday).

  • (080407) We have removed the echo command from the .tcshrc script, since this caused problems for people using sftp.

  • (080402) The first supervised lab session will be tomorrow (thursday) at 15.15 in room 3507. (Tomorrow, there is also a lecture at 10.00 in room ES51.)

  • (080323) The first lecture is on tuesday April 1 at 13.15 in room ES51. The Schedule page will contain information about what is happening when, as well as deadlines and handouts.

  • Home | Schedule | Literature | Assignments | Tools | Links | Course M. Sheeran, E. Axelsson, J. Svensson, April 21, 2008