Hello and welcome to lecture number 12. Continuing with our discussion on operators, let's look at two more operators that roll out and within. So, throughout as as the name suggests, t throughout sequence one T is a signal and as soon show you more on that, so, t throw out sequence matches on the finite interval of consecutive clock ticks as in here, so, t must remain true throughout sequence one provided sequence one matches along that interval and T evaluates true at each clock tick of that interval. This this is the interval we are talking about. So, what we are saying that D must remain true throughout sequence one Now t can be an expression or a signal, but it cannot be another sequence. We'll look at within and we'll see that that problem will be solved.

And as you can see, D must remain true and sequence also must match during the time interval when t is expected to match. So, T must remain true throughout sequence one provided that the sequence one also matches along the intervals which makes sense Otherwise, why should t remain true if sequence one is not remaining true. And then once it is true throughout a sequence one, then the property will pass. Okay, the best way to explain throughout is to take an application. So, let's take this application. This is the spec which says that when in burst mode is asserted, output enable and data ack must be asserted and these are active low signal or because of the underscore.

So, that means they must remain low they must be asserted they should go low within two blocks and then output enable and diac must remain asserted for minimum four trucks. So, after the burst mode is asserted, which makes says output enable and data must be inserted into clocks. And then once they are set a they must remain asserted for minimum of four talks and burst mode must remain asserted throughout the duration of output enable and D which is a very standard spec when you want to do burst mode operation but small goes high. output enable and direct goes low which basically means that output is enabled to transfer data and let's say the boss mode is of four then output enable NDA will remain low for for cross sending for data transfers and burst mode cannot go high when these data are being transferred. So let's see how would we write such an assertion?

First of all, like I've said many times before, think of an antecedent. If you look at this carefully, everything seems to start when B mode is asserted, meaning when it goes low. So, we I will start with Dollar fell B mode as my antecedent. Now I have said before, that here, there are three different components of the spec. The best way to write an assertion is not write the entire assertion right here. Just break down each of the spec components into smaller sequences.

So let's See how we do that. So what I've done first is one of the one part of the spec says that output enable and direct must remain asserted for minimum four clocks consecutively. So instead of looking at the rest of the spec, I said, Okay, I must have a sequence that does this, because if this sequence fails, the whole property is going to fail. So what I did was sequence I call it data transfer. And these these output enable and direct must be asserted within two clocks. I'm waiting for two clocks.

And then I'm looking to see if deaq is asserted, and output enable is asserted goes low, and that this entire Boolean logical and remains asserted for for costs. That's it. I'm not looking at throughout. I'm not looking at anything else right now. So I broken down and taken one part of the spec and Model T as you see here, Now, I'm going to tie things together. What we are asking is that burst mode muslimin asserted throughout the duration of this whole end assertion.

The End assertion is captured in this sequence data transfer. So now all I have to do is after the B mode goes low, I go to the sequence check B mode. And the check the mode says that we mode once it falls muslimin load throughout data transfers and data transfer is what I just described. So, as you can see, once you break down the sequences, it is much more easier to model complex assertions. So, let's see how the whole thing works. Once the BMR goes low, this is where we start the whole assertion or the entire process.

So, to say Once it is asserted, we then look for wait for two clocks, maximum two clocks. And then we see that both output enable and diac are asserted, which is as you can see here, first output enable goes low and then DHEA goes low. So basically, by the end of second clock both lb lb two Bo da can output enabler asserted. And then we make sure with the star four that they remain asserted for one clock, two clocks, three clouds and four clocks. And then we make sure that burst mode remains low, it has gone low here. Draw data transfer so this 1234 are the for data transfers.

And as you can see, birth small, was low doesn't matter. But during the data transfer 123 and 480 minutes low once the data transfer is over, output enable will go high deac will go high and soul will be more this property can also be made a lot more complicated for example, we can say that after four data transfers are complete direct Moscow high the next clock or you must go high the next clock and and be more go goes high. The next book I have removed some of the complexity but in in typical spag you may see those requirements as well. So, you can clearly see how throughout can be very successfully used in many timing diagrams or AC specs as the one that I've just shown here. Okay, let's look at the next operator within if you notice in the throughout Here this was a signal or an expression, it could not have been a sequence, but the within is different from throughout, but both both of the sequences are allowed one within and one the larger one one needs to be contained within the other one and both of them can be sequences.

So, it matches along a finite interval of consecutive clock ticks provided a sequence two matches here is the sequence two matches along the interval and sequence one matches along some sub interval of consecutive clock ticks. So, here again both are sequences and one is contained within the other. The start point of when we say in sub sub interval the start point of the match of sequence one must be no earlier obviously, we are trying to see if sequence One is within sequence two. And similarly the endpoint cannot be later than the endpoint of sequence two again, intuitively that makes sense. If sequence one is within sequence two, then when the sequence two ends, the property will pass, not when the sequence one ends, then the sequence students because we need to make sure the sequence two is longer on both sides than the than the sequence one.

Again, let's let's look at a similar example. But with different specs. Again, let's say assertion Oberst small requires that monster transaction and target x cycles. Follow the protocol below, okay after the burst mode assertion, so monster transaction dictates that MTR x must assert the clock after we mode and demain asserted for nine talks. Okay, Master transaction must remain asserted For nine clocks. Now target acknowledgment for for the master transaction, it was a minor circuit for seven clocks within the master transaction, MT RX.

Okay that that is a spec. Let's see how we would model this. Again, I'm going to break it down. Okay. So tick target act, I'm going to take this part and model it targeted Muslim and asserted for seven clocks. That's it.

That's all I care for in this sequence because if this particular spec is violated, then the whole property will fail, regardless of the relationship with within. So I'm going to say that whenever he falls, it must starting that claw bond bound zero it must remain asserted for seven talks. That's it. I don't go for that. So this bank right now I'm just taking get off one photo spec. The second thing I look at is that MTR x must remain asserted for nine clocks.

That's my other condition. So I have to make sure D agreements asserted for seven clock MTR x remains asserted for nine clock. So all I'm doing here is MTR x, once it falls starting the same clock. It remains asserted or remains low for nine clocks. So I'm still not worried about the vision part. So now I'm going to tie the two together.

Again, the antecedent everything seems to start once the burst mode goes look. So that's my antecedent. Now what I'm going to do is as this thing requires that D it must be true, quote unquote, within MTR x. So I'm going to take the Teac relationship that I established here, and then I'm going to say that Dad tear must remain true within master transaction. So as you can see you break it down, then you tie them together with a intelligent as I call it antecedent. here's here's how the whole thing works, this is your AC specs, Dollar fell be more, then there is the non overlapping operator, then basically MTR x falls, MDX falls and it remains a survey for nine o'clock we have to make sure and that is made sure by this sequence here.

Then, then TX falls and TX remains a certified for seven clocks that is made sure by this sequence stack and what we are and then the stack within it 70 Rx is here, the Teac remains low for seven clocks, Master transaction mt RX is low for nine clocks. And as you can see, here both are signals but one one can be a sequence actually, both are sequences. Sorry about that. So, one sequence Teac remains or is true within the largest sequence, SM Derrick's. So Diego is a signal name and s ta K is what I call sequence for the EC and this is the sequence for MTR x. So you can clearly see that the AC spec looks pretty complicated.

But if you break it down and if you use operators such as throughout our ViDan, then it's much more convenient and much more actually readable to write the assertion Okay, I'm going to stop this lecture right here through our end within which are very useful operators. Thank you for attending the lecture, and I'll see you soon in the next lecture.