So this is a fun lecture. The name itself may confuse you, but don't panic. I bail explained. So let's start with a very simple property as we have seen in previous lectures. I have a property br one and I'm simply saying it bothered of crop request should be followed by Grant after two clocks. If the property passes and said display pass, Elle's display fade.
Very simple. Now let's see what happens when we simulate this property. So at time 10, request is equal to zero and see what happens the property fails. At time 30 request goes high, and two clocks later, grant is still zero. So property fails. But guess what since request is zero property fails again.
You will get to display statements telling you that the property have failed. So how can this be? What we are saying is if request is true, then grant would be true to clocks later. No, that's not what we're saying. As a sequence specified this way simply says that pause edge of clock request be true. Request must be true, and then look for grant to clocks later.
If the request is not true, right off the bat, the property fails. When I was learning as VA, this really confused the heck out of me. And I don't want you to go through this. So that's why I'm explaining this. And at time 90 Look at this. request is zero.
But grantee is one because request was one at 52 clocks later on. Grant is one so guess what the property passes. But because request zero property also fails. So at 1090, you'll get two display statements, one for failed one for pass. How can that be? So again, without an implication operator, when you simply say request to cleanslate a grant, whenever a request is low, property will fail.
Okay, so no big deal. Let's put an implication operator in the middle. So now we are saying if request is true, if the antecedent is true, then check for grant to grok. Like they sound very reasonable to me. If the property passes display pass as display fail. Now see what happens at time 10 requests is zero.
So you would think that the antecedent is zero. So consequent will not fire make sense, but don't Because the request is zero the property will now tell you it has passed and so on and so forth. Anytime request is zero property will pass and you can get to pass or two passes also just like to fails in the previous slide. So, what is going on? How are you supposed to model a property so far I have shown you this way of modeling and it is correct, but you get this pass anytime request is zero. That makes no sense.
That's where vacuous bias comes into picture. The way backers bias works is anytime NDC antecedent is not true, the property will pass vacuously as written in the LRM if that is no match of that dissidents sequence expression, then the evaluation of the implication sexes vacuously and returns true. So what if I want this property to work the way I want it to work only when grant doesn't come after two clocks, it should fail. If the grant comes after two o'clock it should pass. So that is a solution. This is a solution that we used before 2012 LRM.
And I'll tell you how, finally, the language developers fix this the right way. But here is the same property. I'm not changing anything. All I'm doing is when I assert the property, I don't put any past statement here. So if there is a vacuous, pass it you won't know it. More importantly, I also cover the property.
Just like we saw in previous lectures, covered property will pass whenever this sequence is true. Attach sequence and property antecedent and consequent have satisfied the requirements for cover, there is no fail action block. So what I'm saying is, so this property if it fails, tell me that it failed and covered the property when the property is satisfied. Tell me that it has passed it has been covered. So now in the log, you see that the request is zero, you don't get any vacuous pass indication anymore because I don't have a display there. And when the crutches one and two crops later grant is one the property passes, every question is one and took off later grant is not one the property phase.
This makes sense. This is what you want to see. So this was a workaround and offer a lot of heartache. Everyone started using this and this is what I've shown you in previous slides, but to our sq. Now they have added an execution control class. So, if you simply say assert vacuous off, then it will turn off the pass indication based on a vacuous access.
So you won't get a pass whenever their request is zero, like we saw in this case and, and you can also have, so, the other thing you can do is if you want to turn on only the non vacuous paths, which is what we want, then you can use this execution control task which says assert non vacuous on. So this assert vacuous off is your Savior. So, you can use an antecedent and you can have an antecedent that is not true, and still you won't get a vacuous fast indication. So, as I say, This is a fun lecture. And it's a very simple lecture, but very easy to miss, especially when you're starting off with learning system or log assertions. Thank you.