Hello and welcome to this lecture on recursive property. This is a bit complicated topic, but you will get the hang of it once we are done with the lecture. So the origin code official definition of a recursive property is that the name property is recursive if it's declaration involved and instantiation of itself. So what does that mean? Let's look at this property. I'm saying assert property on the falling edge of reset.
See that RC one property holds and Bravo DRC but takes as an input a signal called v strap. And it basically says that that this and of these two sequences must be true. Now here, we understand v strap as one of the secrets is V strap must be true. The other side simply says that NPC then being always true imply the same property again. So, we are basically recursing the property in this loop here and every time we come in we make sure that we strap is true. If at one point in time we strap is not true, then this property this ad will fail and so with this property, so, in some sense with the recursion, what we have made sure that our signal in this case remains true after a certain given entity antecedent.
So, this is just to reiterate, this particular part of the sequence is coded simply to recurse on itself. Here antecedent is always true, which implies at the next ball of cloth, call the same property again, and that Gabriel repeating this until we strap is false when it's false that the property will fail. So, in in this example, the bottom example is identical property only that I have changed the non overlapping with that overlapping. Now, think about this, when you enter this property and you say call RC when again, we are not advancing the clock because this is overlapping. So, in some sense we have now recursed or created and in finite lo at the same body clock time does not advance is repeating itself in zero time and that will give you a runtime error. So, the point is you must have either a non overlapping operator or some kind of time advancement before you recurse on the property itself.
Now let's make this a little bit more interesting in in this particular example, all we did was made sure that a signal remained high after a certain antecedent was true. But let's say in real life you have a specification which says interrupt must be held true. Until I EQ is asserted. That means interrupt must be acknowledged before it can be taken off. So how will we do that? So here I'm setting a property RC one and I'm giving it two inputs interrupt and I and in the property are seven I'm saying two things one is, I should be true or this entire sequence should be true.
And in this entire sequence, I'm saying interrupt must be true and this side must be true. And this this part of the code is lit. Simply Created so that you can call the property recursively. That's why the antecedent is true. That means every time go ahead and add the next positive clock call the same property again. So this particular part of the code is simply to recurse on the property itself.
And then let's say I it goes Hi, let's look at the lo fi. So interrupt is high. And every clock we are making sure that it remains high and is it remains high and one fine clock Ayah goes high. Now since this is an AR, and since I agree and high the property will complete and pass, but let's say for example, I act does not go high, as shown here. And at the same time interrupt goes low. That means a drop did not say hi long enough for it to go high.
So interrupt low. So, these and will fail and I case loads. So, both sides of the order are false and the property will fail. So, in this case essentially we have used an R and an N with recursion crack on Polish a particular specification property. Now, let's take this one step further and look at a very real life application. So, the specification says that for D cache right me miss this is from a typical CPU, D cache, cache subsystem example for a D cache right Miss start Miss allocation because you miss the right the next clock and issue a mem read or read Ma'am, one clock later.
And then see that about matches And on a match, make sure that raw data is held until me, memory completes. Okay? Seems like a bit complicated specification, but it really is not. So let's take it step by step. First thing that, as I've already said, break down the specification into smaller sequences. So the first sequence I'm creating is is for this part of this sequence.
Michelob says that Miss D cache, if it's through one calculator, a log star should be true at one clock, like a read maps should be true. So I've created a sequence called Mesa walk. Now what I'm doing is I'm saying assert property s underscore RC one. Okay? And in s underscore RC one, I'm bossing the entire sequence missile. I've shown in my other lectures that you can pause and entice.
Sequence as an actual to a formal. So here I'm saying that in SRC one day This means hello sequence. And when it is true when we have Gundam is a law, fire RC one. The next clock fired RC one and RC one I'm sending two inputs, right data H and read C. Now this is the recursive part of the property. So it's exactly identical to the previous example, what I'm saying is d c should be high or this part of the sequence should be high. And here I'm basically saying that right data should be high, every claw, because I'm recursing back to the same property, right data and recurs, right data and recurs so as long as our read is Not high, we continue to look to make sure I data is high.
And as soon as the rate complete is high, we don't care for our data high anymore, identical to the previous slide example. So this is one way you can break down the specification and effectively use recursive property to see if a signal is held high or low for that matter, until something else is true, and so on and so forth. So, look at this slide carefully. It may look a little complicated, but it really is not. A couple of things. Here again, you're passing an entire sequence as to a formal called genetic sequence.
And then I'm calling a property which continues to recurse itself or do some conditions are true. A couple of restrictions. You cannot have a knot in recursive property instance. So here I have a property are illegal. And I'm saying c implies a an recurse on itself would be the not. So not is not allowed.
It doesn't make sense actually. And this is similar to the point I made in the very first slide you cannot recurse on a property with an overlapping operator, you will get the error that you're not advancing time you are stuck in a zero delay loop. So overlapping operator or bom, bom zero or anything that does not advance time will give you an error. This is just one more of the ones that if if you want to disable recursive property, based on our standard disable if operative It's not possible you cannot say visible if B and Danny no kill this recursion, you cannot do that. So the solution is very simple. You simply say property are illegal and in that you say disable if B are legal.
So all I'm doing is I'm splitting this property into two and then our legal literally goes on to recurse on itself. And this recursion will stop as long as as soon as B becomes true. So this is just a simple points telling you how to get around the disable construct for recursive property. And one final point that not only can you recurse a property on itself, but you can recurse between two properties also. So your property see phase one does no recovers on itself, but he says go to see phase two and C phase two does not recurse in itself, but goes says go to C phase one. So, here now we are going from C phase 122222122 and going in, in finite loop and that is an advisement of time because of the non overlapping operator here.
So, this is a legal way to do mutual recursion among recursive properties. So, that's all, hopefully, recursive properties are clear to you. Do revisit this lecture if you have any doubts or confusion and always send me questions if you're not clear on anything. Thank you.