Question 4.2 of the exam

[Dan Karlsson]

Wasn't question 4.2 outside the scope of what has been thought in this
course? I can't find anything in the course lectures etc. about using
smv to verify properties in Lava over several clock cycles...

/ Dan

[Thomas Hallgren]

Hi,

On 2009-05-27 17:05, Dan Karlsson wrote:
> Wasn't question 4.2 outside the scope of what has been thought in this
> course?

I included this question, because I wanted some of the questions in the
exam to be a little bit challenging! And it's only 4 points, so you can
get a 5 (or VG) even if you skip this question.

It is true that we didn't look much at sequential circuits in Lava, and
I think the only example of how to verify sequential circuits was
question 5.2 in the 2008 exam that we looked at in the last lecture. But
observer circuits showed up in combination with sequential circuits in
the Lava 3 lecture, including the idea that they can be used to verify
safety properties using bounded model checking.

http://www.cse.chalmers.se/edu/course/TDA956/TH/l11.html

> I can't find anything in the course lectures etc. about using
> smv to verify properties in Lava over several clock cycles...
>

That's why I put the hint that you need to use the delay element!

Mvh Thomas H