Hello and welcome to this lecture where I'll explain the concepts of strong and big sequences and the followed by always and eventually operators. So, so far in all the lectures that we have seen, I have not use any specific indication of whether properties strong or weak. So, what we have done is for example, this is a sequence where B should follow a after one clock or after any number of crops. Now, so, far what we have gotten is via set the property and we say a implies a and ascorbate B, I have not used a strong or V for that matter operator. So, the way it works and LRM is to be honest, not very clear on it. But after a lot of simulation This is what it means.

So if you say a implies strong a way B, then and let's say that if a B does not meet its requirement that means B never arrives after a. And if you run out of simulation time takes most likely at the end of the simulation, then this property will fail. And so far what we have seen is without a strong operator, if this sequence does not meet as requirements, then the property will not fail. But depending on the simulator, you will get an indication that the property is incomplete. That is dependent on the simulator. lrm does not say what should happen if the property is weak.

So remember that in certain properties by default V, as we have said all the time, but you can make it strong and make it fail. Governor on the other hand is just the opposite. Color is strong by default. And so far we have never used a weak operator when we cover a property. So by default, strong means that if this sequence does not meet these requirements, then the property will not be considered cover. Because it could be a wrong indication.

That's by default. But if you say weak, then the property again, the simulator may give an indication that the property is not covered and is incomplete. So, in my opinion, that default behavior is quite good, unless you want to make it specific to what you require. So I basically leave it as default. But if you want strong indication in either the server or the cover Then you can change the behavior by using strong or weak operator. Okay let's look at the followed by property.

After bad followed by property is like any implication property, but with one major difference. So there are two types of followed by operators, one is pound dash pound, and another is pound equal to pound. This means that is an overlapping implication. This means non overlapping. So let's see how this works. Followed by means that both the sequence expression which is the antecedent and the property expression which is the consequent must be true for the property to pass either of the either the sequence or the property exploration is false.

It does not mean it's requirements that apply. property will fade. Now, let's if you replace bound dash bomb for example, with an overlapping operator like we have seen many times, then what's going to happen is as we know, if the sequence expression does not match, then the property will pass vacuously please refer to my lecture completely devoted to what are vacuous passes. So, with implication if the sequence expression does not match then the property passes vacuously but in the followed by operator if the sequence x version does not match, then the property will fail. And so, this is like an overlapping implication and this is similar but non overlapping implication many if the sequence expression matches then starting next clock property expression should be true. So, that is The big difference between implication operator and followed by operator.

So here's an example. I'm saying a should be non overlapping, followed by B. And I'm passing it as sequence request consecutively asserted for five calls and grant. So, what that means is requests should be asserted consequently 4545 clocks and then grant should be set at the next clock. Now, if request is not a set it for five blocks consecutively, then the property will fail. Or if the request is asserted for five blocks consecutively and then grant also arise one block later then the property will pass or if the grant never arrived in the property will fail.

So again, both the sequence exploration followed by property exploration, both the sequence operation and property exploration should match. So that is a fundamental difference. So what, as a grace just replace this with a non overlapping V and see what happens if that request is not a survey for five consecutive across? The answer I'll give you is that the property will vacuously pass so that's the main difference between forward bi and implication operator. So this is another example and he said should be asserted consecutively from for minimum one clock or forever until a reset goes low. And if with the implication operator, let's say he said never go slow.

It he said always remains high. Then this robber D will never fire the consequent, but it will pass vacuously as we have seen before, but if you replace the overlapping of non overlapping operator with the followed by non overlapping operator, and if we said never goes low then this property will fail. So, depending on what you're trying to accomplish, please use either the non non overlapping implication operator or non overlapping followed by operator. So, in this example I already use the operator always but I haven't shown you how it works. It is quite intuitive, really. So, here's the operator always and strong always property.

So when you say always it's of the form, but and you can have Have a constant range expiration also this is all vague form and this constant range expression must be unbounded or it can be unbounded, but when you go with strong always the constant rate must be bounded. And so this is the strong version of always and just like I explained, it will act according to my definition of how strong properties work. So, here's an example for the power said should remain consecutively asserted for five clocks or 10 clocks. And whenever that happens, starting next roguery should reset should and remain low always forever. Now, note that when you do, for example, use a positive clock always be strapped should remain equal to zero. You put it this way.

This is Have you done done with this particular property? Because as we know, when you say at positive clock we strap one equal to zero at every pauses of clock we are going to check that we strap one is equal to zero which is the same as saying always check for reset one equal to zero. So without an implication operator always is many times or most of the time redundant. Now let's look at this example where I'm saying that a certain property and reset should remain high Kentucky daily for five clogs and then starting next glob, it should remain low. Always. What I like to for you to do is try the same property but but remove the always operator and see what happens you will get a different result.

Always one same. dissident fires it will continuously check for reset to be low. here once the antecedent passes next rocket reject for reset will be low, but it will not check for reset or below always, it will again wait for reset to be consequently asserted for five graphs and then again check what he said to be no. So it's a subtle difference, but I strongly urge you to try with always and without always and this is simply to show that strong always cannot have an unbounded range, it must be bounded like two to five to 10 etc. And here's another example, which simply shows that when a stroll goes high at least once because of the go to operator then it should Then data should be meant not be unknown and it should remain stable forever. So, as soon as this antecedent fires this will not continuously check for the consequent to follow the always property.

And my quiz here is that how would you model the same sequence without the always operator because all this time I've shown you ways to do the same thing with the concurrent operators that we have seen so far. And when you do it without the orders operator, my hint is use consecutive reputation operator. So please try it because that will really show you a hammer always. Operator words. Similarly there is any venture the operator That is a weak form eventually. And that is a strong form eventually.

And the way it works is, you simply say for example srong. Eventually, for after two clocks, or after any number of clocks frame showed fall, that means, once at least once eventually we don't know when frame should fall. And this property simply says that eventually, when a falls that often falls eventually sorry, when is true, that often it is found through the first time it should always remain true. So that's what I've shown here, that this is the diamond we start the property, then eventually the sequence expression should be true. And once it is true, it should be Metro forever. So it's quite intuitive.

A we have seen how to model the same using other operators, but in 2012 LRM they added this and it makes it a lot more intuitive and easier to model. And here are a couple of simulation performance efficiency trips. So, you can always say advantage of cloth six should be high and every passage of clock keep checking to see ciggies high, you can also sorry, you should also you can also assert the same thing by saying add positive talk always sick. So when you use the always operator, the simulation performance from what I have seen gives you a better simulation performance. The simulator runs much faster So everyone in a dirty Curlin, but this will be will perform faster in simulation. Similarly, here we are saying request implies from one clock to 10,000.

Clocks grant should be asserted should be high. So via have a long constant delay range here. But you can do the same thing by saying that request implies eventually, Grant should go high. So, is the same thing both are identical Well, if it goes after 10,000 plots, and this will actually fail, but this would simply look for grand to be true whenever, but if, let's say does fall in 10,000 plots, this way of modeling will be inefficient, while as eventually doing the same thing will be more efficient. So, that's all for this lecture. Simple and short lecture, please try all these small quizzes that I have given.

And I'll see you in the next lecture. Thank you.