Click here for the answer.

This is one of those quiz questions that makes perfect sense to me, but also a question that many individuals taking this quiz have struggled to answer. Saying that it follows from the discussion at the end of the induction lesson doesn’t help much for those who haven’t necessarily read through the formal courseware slides. So let me explain the question a bit more.

The first point to note is that the trace shown above is really irrelevant to the question. It was drawn from a trace of a clock switch, but like I said that’s irrelevant to the question. Indeed, I’m not sure there even is a bug in the trace. What is important to note when answering this question is that the image represents an arbitrary trace that was generated from an induction check, and that it was generated from a formal property check. This is not a simulation generated trace. That’s an important key to understanding the question.

Next, let me explain the three areas in this trace, starting from the end of the trace and moving towards the beginning. First, there’s the area marked “C”. This is the last time step in the trace. The next area, “B”, is one formal time step prior to “C”. Like “C”, “B” is also only a single time step in width. The “A” area is therefore everything else in the trace. It extends from the beginning of the trace to the penultimate formal timestep.

By the time you get to this trace, the formal tool will have told you that there’s an assertion failure in either area “B” or “C”. According to the question, however, when you looked into this trace you found something wrong in area “A”. It didn’t trigger an assertion failure, but it was definitely wrong. What was wrong? The design wasn’t doing what it was supposed to be doing–whatever that was. The question, then, is not what is wrong with the trace above, but rather how do you address this problem in general?

If you’ve never dealt with something like this before, then beware that it is a common induction problem when working with an SMT based solver, and so if you work with formal methods you are likely to see it again and again.