Hello and welcome to lecture six. In this lecture, we will see the important concept of multi threading as applied to concurrent assertions. We'll also see how formals and actions work. And also these are billing of assertions how they work. Okay, let's start with multi threading. I will go back to my good old example of sequence property and how the property is asserted.

Here's the clock. Here's the C start signal. Here's the request and here's the grant signal. Let's say that this was edge of clock, see start is asserted, it is sampled Hi. As you know in this property if see started, sample high. The overlapping implication says that the requests are Someone we sample hi at that clock edge so we see that happening here and do clocks later grant should be sample Hi.

And we see that happening here and the assertion passes. Now let's see what happens the very next clock edge see start is sample low. And since it is simple low this application won't fire this property won't fire because he's already is not high. Okay moving along and I call the first as as one thread. Now at this clock edge, Sr disabled Hi again. But before I show as you can see the relationship here, but not the very first thing you note here is that the first thread as one completes the same cloth that the next thread starts that is multi threading.

It's not like because the first read was ending here that it will ignore the second thread. So the second thread starts the same clock as the first thread completes, and it will go through this property and sequence exactly like the first one, and it will pass at this clock edge. Now, s3 thread starts the very next clock. And at that clock, the thread has to was still executing, it has not ended yet. That being the case, s3 will still start, it won't be ignored, and it will go through its transitions. And in this particular example, I'm showing the transition such that all the three threats pass.

So the point is with concurrent assertions you really don't need to worry about when the antecedent will fire when the operator Regular thread that started with the firing of the antecedent will complete not complete could be the middle of the execution, and how the very second firing of the same property, same assertion will affect the preceding assertion, you don't have to worry about any of those things. This is a very important concept that you need to understand. As you can see, there are more complications when we will see this, this one round two is called the delay operator. And we'll see what happens when you have range based delay operator, then the multi threading becomes even more complex. But let's keep that aside for now. Right now, just understand how the multi threading works for non range based block delay operators.

Now let's move on to formal arguments. You might be familiar with some of this from you Regular Verilog knowledge or system Verilog knowledge. So here are the formal arguments sequence is the same property as sequence again and you have a B as a formal arguments and you have formal arguments logic ba and BB. And from this property as you know we call the sequence as r1 and we pass p NPV as actuals to to the NPV formula. So these are the actual p APB and request and grant. So when we call the proper DPR, when we pass a request in grant, which gets these actuals gets assigned to the formal PHP and the PNP as actuals get assigned to the forms of the sequence, and this should be straightforward.

And if you do Do not declare a type for a formal, then it will take the type of the actual, which makes sense. So, here's a practical real life application where basically you create sequences which are of quote unquote, generic nature and then you or generic nature which are parameterised then use the same sequence or the same property for that matter repeatedly with different assertions. So, for example, I have this property called no change sake, which has three what I call parameters or formals. Be Glock ref SIG and stable sake. What it says is at bondage of claw, if ref SIG is not asserted that the stables say should be stable. Now what I'm doing is I'm taking this property and asserting it here a set property, no change sake, but I'm passing it says clock, output enable and read data.

And so these three actuals will take place of these three formulas. And whenever output enable is low, that means output is enabled, then read data should be stable. Now, without changing anything, I said the same property, but with write enable. So it's a very simple concept with which you may apply to your projects where what you normally do is you create a library of quote unquote, generic properties or sequences, which has formals and then you keep changing the actuals for the same sequence with different signals. Some more points on formals and actuals, you can have a default on a formal, and then you can connect quote unquote actuals with the formals. Using position base, this is very similar to Verilog.

Or you can use name based connections to connect the former's initials. And this is the same example again, the point I'm making here is, since that is a default assigned to a net ENB here, you can simply skip connecting that particular formal in this particular property, or, if it's position based connection, this is name base, this is position base, you can simply leave the position empty, but followed by a comma and then because in grant This does not need to go into detail because this is very, very similar to what you are familiar with in Verilog. Here's a very powerful feature that I use a lot. So here's a property, which is a formal called CC, you have it enable and the same logic PNP. But see what I'm doing. I'm inside the property I'm saying at cc whenever cc changes pause or neglige.

And implies the consequent antecedent implies the consequent. I use seasick formal into my sampling edge, sampling edge, being seasick here. Then what I do here is I'm taking borders of clock. You can have an actual which isn't even gain control. That's very powerful. You take the position of clock and you pass it as an actual to seasick.

So now seasick will be pauses of clock. So, at pauses of clock, you do that. So the assertion and to pass an event control will make it very easy for you to create again, a generic set of properties or sequences, where you can even change the event control the event the sampling age, directly from outside of the property, and keep the property generic. Now this concept I am I'm laying out here, even though we have not used local variables, we do not know what a local variable is, at least up to this lecture. The point I'm making here is the law insider property you have available Goal l data, which is of size D size to zero. And what I'm saying is I'm passing the former DEA size to size this variable l data.

And then I'm passing take the 31 to size to declare this L data which will be 31 colon zero, but you cannot do this you cannot use a formal to size a local variable in a property. The size can only be a constant or parameter constant because it needs to be known at the elaboration time. So, this is a mistake people make when they're again trying to create a set of properties and sequences which are of genetic nature. For example, in this case, the bus can be of different size and you can you can pass different register sizes to size a register inside The property, but that is illegal. So be careful of it. Now let's see so far I haven't shown you the disabling condition of an assertion.

Now, this is a sort of complex assertion, but we don't need to understand the complexity of it. The only thing we need to understand is that here's antecedent dollar fail burst mode, which implies non overlapping that the data act will remain asserted within the sov sequence. This sequence remains true within the sequence. Let's not worry about how within words and let's not worry about any of the complexity of the property here. What is important is I'm saying that do not execute or do not do not even look at this incident. Every set is active low and Reset is low, disable, if if and only if reset is low.

Do not execute this every day reset is not low execute this. Let me show you what happens if reset is low. So here's the simulation log of this particular assertion. And very quickly, the reset remains high throughout the execution of this assertion. And obviously, I have designed this such that the assertion v. diff passes. I haven't shown the assert statement here.

But it's the name of the assertion here is PDF and the property PDF or the assertion PDF passes. Now let's see what happens if the reset goes low. In this on the right hand side of the log you See the reset goes low. During the execution, this is exactly the same from 20 to 120. During the execution of this logic, this properties assertion goes low. Now, important thing to note here is, it will discard this entire assertion.

If the reset goes low in the middle of the property, it's not that it discards and gives you a fail indication, it won't give you a fail indication. Obviously, it won't give you a pass indication, it will simply discard it. So be careful on on Venu. Let's say reset is a very typical example. When you assert the reset, make sure you're not executing a property. I mean you can but then also know that if the last property which was executing during reset, you wouldn't know whether it pass or fail.

So that's how the disabled live works. Note that it's all it always needs to be before the antecedent This is our antecedent, you have to declare the property before it you cannot declare it after it or you cannot declare it in the consequent and the disable if is only allowed in a property and is not allowed in a sequence again sequences are very generic are very, they are temporal domain and they can only have Boolean expressions. But, that is one of the difference between property and sequence use. You will see throughout this course, the differences between sequence sequences and properties like I showed you earlier that, you know if the if the property passes you can have a display statement or whatever a procedural block here for pass, else if it fails, you can have a fail action brought by you default, it is considered a runtime error.

This is the default according to the LRM. And you can if you want to quit the simulation, because this is a major assertion failure, then you have to use dollar fatal, just like shown here, else dollar fatal and so on and so forth. If you don't say anything, you simply say hello, and semicolon then it will by default use dollar error. So, again, this is a short lecture and we have gone through some of the basics of concurrent assertion and I will thank you for attending the lecture and I will see you soon in the next lecture.