Hello and welcome to lecture number 19. So far we have seen assert and cover for the assertion statements. In this lecture we'll cover expect and assume. And then we'll also look at how a blocking action block affects your goal. The expects statement is a procedural blocking statement. If you recall when we say immediate assert, which is non temporal, so it's immediately executed.

If you say assert property to fire a concurrent assertion from a procedural blog, then it fires itself and the code moves to the next statement without waiting for the asset property to complete because assert property will execute in balance. To the procedural code as opposed to assert and cover and immediate assert. And also the defer immediate assert. Expect statement is a blocking statement. So, it has the same syntax as that for a certain property. And let's look at this example to make sure we understand what a blocking statement means.

So I have a simple initial block, and I'm displaying before calling the expect that I am indeed before expect expect at policies of clock c implies starting that clock c followed to clock letter D and to crops letter E. So there is a temporal domain here you're going to consume at his four clocks in this particular property. And then of course, we have exit blocks if it passes or if it fails, then what I did was after expect I put another display saying goodbye after expect this is to show whether they expect is blocking or non blocking. Expect is blocking as I just say. So, in the log file if you see Hello before expect, then we wait for C, D and E according to the requirements in the property and they all arrive exactly as required. So, they expect will pass and then we get goodbye after expect.

So, you can see that the procedural code after expect was blocked until expect was done. So, here's my question again what would happen if you change expect within assert. So, instead of expecting to set a certain property and the And then the property is this property, then the execution will started display Hello before expect, let's say hello before assert assert will be fired and it will start executing in parallel to the procedural code. And the very next statement that will be executed would be this other display goodbye our ex after expect. So in short if you looked at a log file, and if you had an assert here instead of expect you'll see Hello before expect and goodbye after expect both at time zero. Goodbye after an extract will not wait for a search to complete.

So that's pretty much it as far as the expert statement is concerned. It makes sense to have such a blocking segment because there are many times we simply want a particular property to pass or fail before we do anything else. If it runs in parallel, then you have to continually check to see if the parallel lowly running properties passing or failing. So that's the reason for an expect statement. Some rules on the semantic. Here's the property, dp.

And what I'm doing in the initial block is I am excited expecting a ball at pauses of clock, ABC to hold and this is ABC here. Now this is okay because one thing that expect requires is to have an explicit clock edge that is associated with the expect state. Here we do have one so that's okay. This is okay too. Even though you don't really see our explicit clock is right here. Because dp property or has a positive clock, so that's okay too.

This is not okay. Because expect ABC x spec does not have any explicit clock edge associated with it. And neither does ABC sequence ABC sequel doesn't have a clock edge either the clock gauge is specified before expect is called that's no good. It has to be with expect so that's why this gives an error. The similar to this again we have expect ABC in this code always a positive clock begin expect ABC. So normally you would assume based on our previous asserting our semantics, that if there is no clock specified here, it will inherit the clock from the preceding always block not true.

With expect you will get an error. Again the point being with expect you need to explicitly provide a clock for it Eyes your posture compliance. So, these are just some basic rules on how to use expect and and we covered the semantics in the previous slide. Okay, let's look at assume, assume basically allows properties to be considered as assumptions. Why do we need as you There are two main reasons for assume one is static formal, and some call it formal or constrained random simulation. Just quickly, semi formal is a huge field in itself and is beyond the scope of this course.

But let me just give a brief overview. Static formal is a tool and it's a methodology and technique where you take a certain corner of logic, let's say it has 10 inputs, and then outputs and you tell the static formal algorithm to exercise all possible combinations of those 10 inputs, both in combinatorial domain as well as temporal domain. And let's say the, the, the block of logic is maybe 10,000 Gates is not so big, but it's not so small either. What happens during the so called former analysis is that there is something called logic cone explosion problem. You can imagine that when you want to try all possible combinations, combinatorial combinations are to raise to 10. And that's manageable, but it's a temporal many at this clock.

If input a is one, then the next log input B could be zero or one so on and so forth. And this whole evaluation just explodes. And many times the tool just will either give up or it will, it will just take so long that you will give up So, in order to avoid this logic static cone explosion, assume is assumed statement was added to the LRM. So, what it will do is, you will say assume a certain relationship, either a temporal relationship or a combinatorial relationship. And now what formal analysis tools will do is a set of trying all possible combinations of those 10 inputs I was just talking about, it will restrict or assume certain values and certain temporal conditions on certain inputs. So, as you can imagine, it doesn't have to try now all combinations, all possible permutations, it will only try those outside of the assume scope.

So, the former tool doesn't really Verify to make sure that what you have assumed is correct, whether that condition will indeed be met, it simply assumes what you have asked you to assume and move forward. But in simulation, let's say instead of assert cover, expect us to assume then that property must hold and just like in assert, if the property fails, then you will get a failure. So, in simulation, the assumed property is checked for formal it is not checked, it is checked only for the underlying assumption. So, in this simple example, we can say there is a property whenever grant is asserted Hi, the next clock request should be taken away. Now, this simple temporal condition will help the formal to tremendously in reducing its permutations. And this is also a simple example it says that IV Rank is asserted, it implies that it will remain a Saturday, consecutively, this is the consecutive reputation operator, Iraqis assert a rank will remain asserted until arrives.

So, if you have such a well defined assumption, then again, formal tools will be much more efficient. Now, quickly the same assumptions are very useful for constrained random dynamic simulation errors. constrained random basically means that you're going to constrain certain corner of logic and target it to a certain for example, you have 32 by database and you only want to exercise odd bytes, so, you can constrain the 32 by data bus to odd bytes. And you can assume that even bytes will never go out on the bus to show something like that, and this particular two examples, or temporal domain assumptions are also very helpful for constrained random to allow you to narrow down to a certain kind of logic, so, that you can be very effective in finding bugs in that kind of logic. So, as M is useful for setting formal as well as constrained random.

This is a topic which is not quite related to expect or assume, but it's very important all this time all these lectures that I have gone through in the so called action block. As you recall, when you assert a property, there is a section block here, held there's a fail action block and as I've said before these action blocks up, basically very low tasks, you can do anything you like in that very low task. So far, what I've done is I've simply shown you tasks, mostly displays that does not, quote unquote, consume time. It simply goes and says, okay, property, pass or property failed, and he's done with it. But what if you are actually assuming time in the cost, like a very low cost, we can do anything you like. So that's the idea behind what happens if your task is blocking.

Here's a property reg implies two clocks later grant, and we assert the property. If the property fails, we say call failed ask. Now note in the faders. What I'm doing is I'm waiting for one clock, two clocks, three clocks and forks. I'm actually waiting for some time, some time is advancing here. Before I'm done with fate ask.

Now let's see what happens for in the log. So, at time 30 request those high to close rate a grant should go high, but it failed. It does not. So, the property phase, when property fails, it calls failed ask. Okay, now, keeping aside everything else we are in failed tasks and is going to start waiting for four drops. So it's going to wait for one clock.

Okay, from fate as zero is the first statement, then we are going to wait for 1234 clocks. So we're going to wait for one clock, two clocks, three clocks and four clocks. And then we are done with this property. Now see what happened here. When we were Waiting for 1234 clogs, guess what request came again. This request should fire this consequent.

Whenever a request is high we need to know for the consequent. But when we were waiting when the fate is when the actual blog was consuming time requests came again as as you can see here at time 110. We had already waited for one clog we are going to wait for three more clogs, but request came again. Well guess what? The the assertion is simply going to ignore the request because it has not yet exited the failed task. And so, this is something you need to be very careful.

Many people miss this point. They think that the actual blog is non blocking in the sense it is fired, it will continue its job and the property will Continue, it's so environment, not true. And you need to be very careful how you design your action blog if you're going to consume time in it. And so here for example, when request came again, two clocks later, Grant should have come and property would have passed. But grant does not come and property should have fake, but it doesn't show failure, because we are still consuming time in the first invocation of faders. So the second phase has doesn't even come into picture as you can see, nothing happens.

So you may you will miss certain triggers of your property, if you're consuming time, and the trigger happens at that time. So this is a short lecture, just one To expose you to some statements, and also the important part of action block being blocking. Thank you for attending the lecture, and I'll see you in the next lecture.