Hello, and welcome to lecture number 14. Let's continue with our operators. In this lecture, we'll go and look at first match if then else. If and only if I FF and implies implies is a new operator that was added in 2009 lRn. Let's look at first match, first match. As as the name says it only matches the very first or possibly multiple matches of the sequence a given sequence.

Now, right there, you can see that it makes sense to use a sequence with delay range. So what delay range tells you is that there can be multiple matches within the delay range. And then what you care for is the very first match. On the first match. You want to take some action So let's look at an application. So the concept is very clearly solidified.

What we are saying is that the very first time PCI bus goes idle, that the state machine should transition to biocidal. State the very first time. And the PCI protocol says that when both frame and Id are high, that the bus goes to bus idle. And now the key is as soon as the frame and Id go high, that bus the the state machine should go to Boise, Idaho State, not one clock later, not one clock. After very next clock, it should go to most idle state and not wait for a few clocks before going to this idle state. So here's the property on the antecedent side.

I'm saying that first match, first match in this sequence bus idol On the first match of bus idol, the very next clock stage should go to versatile and I'm setting the property every time frame false frame false starts the cycle. And I'm saying on the side of the cycle check for bus idol Check. Check for I mean, the FMS property should hold. And FMS property says look at the bus idle check sequence and on the first match of frame and it going Hi, anytime to clubs to forever meaning the PDCA cycle can go on forever. But as soon as framing ID our DS are dead meaning both of them go high that we want to make sure that the state is versatile. So first match with Do the very first timeframe and I already go Hi, that antecedent matches and as soon as the antecedent matches, we will go and make sure that the state goes into biocidal state.

Now, one point, I want to point out that we have used the first marriage in this example on the antecedent side and in most or all cases you will have the maximum benefit of using first match on the antecedent side. Why? Because the consequent meaning the right hand side of a property behaves exactly like first match by definition. The consequent is not evaluated. If you go back and look at all the all the applications and properties that we have looked the consequent is not available. wants its first matches found that is by default.

So on the consequences side, you don't really need to use first match, but on the antecedent side, it really makes sense to use it. So, in this case going back to this case, the first time framing idea hi we look for biocidal sake, but note that framing I ready can remain high for many, many, many clocks. And you've had not used for smash if he had simply said that bus I will check implies the next state should good bus idle, then every clock it will keep doing this check because for many cycles, the bus can remain in bus idle state. So, to avoid all the redundant checks, which will also affect the performance of your simulator, we need to make a Use first match or you should use first match, you can accomplish the same epic property and the spec without the first match, but first match is when in this case first match is a must.

Because the very first time this framing it to go high that the bush stage should go to recital not after the second or third match, but the very first match. The NOT operator is very intuitive. If you look at this example, let's say positive clock A naught C D. That means if CD is true, then this will be false and property will fail if CD matches the property fails, which is maybe contrary to intuitive to sound but it's it's very straightforward if you want to feel the property If you want to discard that and find the property at the match of CD, then you put a knot in front. That's this is a similar simulation log if equal to one and then C, D and E, follow the sequence CDE. spec, that the property will fail. It's it's very intuitive and you will use it quite often frequently, if then else is pretty much like any procedural programming language if and else that is nothing quite new here.

For the sake of completeness, here we are saying in this property that at pauses of clock is high and one clock later either B or C is high, at least once. If you recall this operation At least nonconsecutive go to Soviet saying if as high one or greater B or C should remain high, at least should become high at least once. If that matches then it implies overlapping. If we then one clock later they should be high else if else one clock later he should be, which is this is quite intuitive and quite straightforward the same as what you might have used in procedural languages. And here's the simulation log which pretty much tells you that after a B goes high, B or C should go high B goes high, at least once one clock later, at least once and one clock later anytime, at least once and if we goes higher than they should be true and these are true and the property passes.

So, this is a simulation log on this particular property is very intuitive as you can see. And he has an example where C does go high, and if C goes high, and this one's that he should go high, but he does not and the property fears that are, we have already seen if and only if it's called an equivalence operator. As in the examples that we have seen, so far we have said disable if and only if reset. So it is similar here. So it's true, even if p if and only if q means that properties P and Q are both true. These two If and only if q is true.

And so that's the equivalence between P and Q. More interesting. operator is implies, again implies was added in 2009 LRM continuing to 2012. Now so far we have seen implication operator for example, overlapping implication operator that I'm showing here. What's the difference between this operator implies and the implication operator, the one sound the same. In case of the implication operator like overlapping here that we have seen through all the lectures.

What we are saying here is that evaluation of Q starts only when the antecedent is true. We have seen this all the time. If the antecedent is true, it implies that you should hold but in case of P implies Q, Both P and Q start evaluating at the same time, very different again and be overlapping implication q we say that start evaluating q once p matches, but in P implies Q, both P and Q start evaluating at the same time. And the truth results are computed using the logical operator implies. So, there is no notion of you know a match of antecedent to trigger the consequent. That's the big difference between the implication operator and implies operator for example, we say that x lb lb to y implies a pawn pawn to B, versus, we remove the implication operator and we put implies operator.

So, the case of implication operator evaluation of a pawn pawn to be stars only when x to cross a divide is true, if x to cross letter Y is not true, we do nothing, because the antecedent has not matched. But in the case of implies, if x to cross otherwise not true, the whole property phase. And similarly, if a translate a B is not true the property phase, in this case only when a not a, b is not there to crocs after a that the property will fail. If this does not, if this property does not match, we do nothing. It's an antecedent. So, that's basically the big difference between implication operator that we have used so far and implies operators.

So, that's pretty much it for this lecture. What we are going to do is in the next two lectures, I will present Two quizzes. One is synchronous FIFO. And another is a counter. And I will pose the questions. And I will also provide the answers and explain the answers.

So, that's all for this lecture, folks. Thank you so much for attending and I'll see you soon increase number one