Thank you everyone.
I'm Cesar.
Sorry, those that can stay.
Sorry.
Sorry.
And I will talk about the introduction to formal verifications of digital circuits,
which I like very much and I hope you too.
So why do I, why do you need the formal verification or what,
why would you want to use formal verification?
So it's like a tool for finding bugs and finding bugs is what you want to do, right?
And simulation is another way to do it, to find bugs.
And it's complementary, but in truth, I find I'm using more and more formal verification and not so much simulation.
And it does help finding corner cases, which normal simulation you need to put many, many test vectors,
random test vectors to be able to even try to find these bugs.
Like you have a sequence, a bug which is trigger, maybe you forgot to reset a finite state machine, maybe.
And if you don't test in that sequence, you will miss the bug.
And the formal verification will find the bug.
It's really great.
So here is a comparison.
What does traditional simulation does and what does the formal verification equivalent or near approximation is?
So in traditional debugging simulation, you want, maybe you make a simulation a few steps.
When to look at the result, the traces to see if it's going all right.
The equivalent is the cover.
It's not like a software coverage.
No, it's something different.
You tell what you want to see.
So you don't drive the inputs.
You let the formal verification engine drive the inputs.
And you say, I want to see three transactions.
Every time there is a transaction, a write or a read, I count and I want that count to be three.
And the engine will go and do everything it can to find these three.
An input will give you these three transactions.
If it can't, it will complain, not able, not possible.
What is the equivalent to unit test?
In unit test, you put some test factors.
And you actually assert the result.
So it's automated.
It's not manually.
In formal verification, you have bounded model check.
You have your model in a bounded, in a limited number of steps.
I want to drive this model and simulate it and see if it reaches a bad state, an assertion.
But it's not like an assertion.
If I put input two, it needs to return four.
It's not like this.
You have to assert that given the inputs which are driven by the formal engine, what the output should be.
It's not a fixed number, not a fixed test.
Test fixture is when you don't start from the beginning.
Maybe you have several tests which share some common starting point.
And you start from there.
The closest equivalent will be K induction, where the engine will try from any state to reach the bad state.
Or it will prove that from no starting point, it will reach a bad ending point, where the assertions doesn't hold.
So equivalent for random test cases, maybe you want a coverage, yes, for your system.
You try hand only because generated by hand is not feasible.
You try to reach a corner case, but you cannot guarantee.
You cannot actually see every random, will not cover every from zero to infinity or two.
In the formal case, it does an exhaustive search of the inputs.
So it's like random.
If a random test will fail, it will find it.
Yes.
And the other difference is traditional tests can be procedure like you count, you do for loops, you call functions, maybe.
In formal, everything has to be synthesizable.
Everything needs to be logic.
There is no software in formal.
It's all hardware.
So if you want to verify something, you have to make a test harness to catch it around it.
In traditional simulation, you have a test vectors.
Maybe a sequence of vectors, which you want to see.
And then in formal verification, you assume.
So it's not completely random, completely free.
The engine has to follow your rules.
So like if you have a valid signal, it has to stay stable while there is no ready from the next stage.
Well, you have to tell it if it's, if valid is up, then ready, it will stay up while ready isn't false in the previous stage.
So you assume inputs and you assert outputs.
That's the rule.
In traditional simulation, you also do assertions for automated testing, right?
So the workflow in formal verification should be like this.
In your high level definition, like harder definition language, you put the assertions.
Then it can be a very long, a VHDL or any other language like Python-based language, harder languages.
Then you make a work plan in the SSBI tool, which drives the process.
What processes?
First, you'll see, you may be remembered for the free FPGA and ASIC tooling.
It will take your HDL to code that you can put into FPGA.
Well, you also synthesize instead of an FPGA, it synthesizes to logic functions.
Which logic functions?
Well, there is a state, which is a state of all your design registers, all your memory.
There is an initial predicate which says, this state is initial, like the registers are zero, the system is the reset state.
Then is the transition relation, and it takes a state to the next state, like a finite state machine, for instance.
And then you have your assertions.
All these are Boolean functions, like AND or NOT and NAND.
And then, these other two uses as MTBMC proves correctness or outputs a trace.
It does exactly a search for an initial path to the bad state, an exhaustive search.
If the path is not found, the design is correct.
And if found, it outputs an error trace.
This is an example of a bad trace.
So, you have an initial state where the predicate holds, and there is a transition from S0 to S1, where the conditions hold on S1.
All the way to the final, the case state, where there is a failure here in the assertions.
So, the engine takes all of this logic here and try all the inputs, so this one is true.
And then it tells you the trace, which hitches this.
So, the algorithm is, from zero steps, you prove the base case, which is no path from the initial state will reach a bad state in K steps.
Like mathematical proof. This is your base case.
Then, the induction step. No path ending into a bad state can be reached in K plus 1 states.
So, if the base case holds, and the induction steps holds, then you prove it for infinite time.
You can hope to simulate for infinite time, but here you can. Yes.
Like, this is why we call it unbounded inductive proof. No bounds.
With our finite proof, I can prove it for all time for any input.
Okay. Well, but maybe, inductive case, I cannot prove it in K. We try K plus 1, K plus 2, etc.
Well, not for infinite, it's guaranteed to end, because you have a finite states, a number of states.
Your number of registers is finite, is limited, so it can be extremely huge, the state space, but it's finite.
It's true to the power of the number of flip-flops you have, right? But it's guaranteed to terminate.
And there are very clever algorithms, so you don't have to try every single combination.
So, let's try starting simple, right? This is a register with feedback. No inputs, no output, just internal state.
What is the state diagram of this? If it's 0, it will be 0, it starts 0 here, and it will keep being 0 for all time.
It can never reach the one state if it starts from 0. So, we tell the engine, the formal proof engine, please prove that it will ever be 0.
What he will search for paths which end here at 1. But there is no path. I can tell you, try one step, K equals 1.
It will work because there is no path in one step which will reach actually in any number of steps, right?
So, the base case holds, and the inductive steps also holds.
Complicated a bit. Now we have a registered output. So, here my notation is, the first number here is R, which starts 0, and S will be a copy of R after 1 clock.
So, it's also 0. If R was 1, then it will move to a copy of it in the next state, okay? And stay there.
But you see there is no path to here. And if it starts 0 and 1 here, it will go to 0 and 0. It will copy, lose the 1 in the next step.
It will copy the R. So, you can simulate the base case holds here.
And the inductive case, well, just one, just K equals 1 is not enough here. Because from here to here, you can reach a bad state if you start from here.
Remember, the inductive, the inductive, only the base case will start from the initial state. The inductive state, the inductive algorithm, the inductive step will start from, from, actually will start from the bad states.
It will start from here, trying to reach a good state. So, it starts from here, finds it's here and says one step is not enough. So, we try two steps. With two steps, yeah, it cannot be done.
We have two good steps, two good states and one bad state. No way. So, we have proven this case with two steps. No.
So, well, let's complicate a bit. We have an enable now. The output can be 0, will not copy R, and then I enable it and it can be, it will be copied.
So, enable, I put it here. So, it can be here or here. You see, I not label the transitions and the input is actually inside the state. I treat it as a state also. Why?
Because the transition relation is between two states and maybe it's from the states and inputs, I get the next state. Well, I put the two together, the input and the state is the state.
Okay. Because the transition relation is a relation, it's not a function of the inputs. So, you see from, if enable is 0, it will keep 0, 0, 0. Likewise, if enable is 0, it will keep where it is.
If enable goes to 1, then, well, it goes to here. If enable goes to 1, yes, it will copy. The input will be copied on the output.
Yes, here. Here you have, for instance, R is 0 and S is 1. And enable now is 1. So, in the next state, that R, the S will copy R. But you see, I'm asserting only that S must be 0.
So, R, I don't care. I don't know, actually. It's inside the design. So, only these states are where S is 1 are bad. And all the states where S is 0 are good.
Independent of R. So, you see, the base case is good with two steps. It will never reach. The base case will never reach these bad states from here. Never, ever.
And it will never reach. And, but now, what about if I have a, I'm in a bad state here. Okay. So, I try one, two steps. Okay, I, let's, I'm not proving induction, I cannot prove induction in only two steps.
You see, there is a path here. What is the path? R is 1, R is 0. Not enabled. Then I enable. So, it is copied. Now, R, S is 1. It's a bad state. So, in two states, I can reach a bad state.
So, let's try three. What happens in three? Well, I just repeat this. One, two, then three. One, two, then three, and four. Yes. So, you see, this loop here. So, I can try K equals four, K equals five.
Induction will never prove it. Induction will never work. Why? Because I'm allowing this loop here. So, in induction, you, you can't have loops, actually. Yes. Some engines will remove the loop for you.
Loops actually don't matter because you're only repeating yourself. Right? If there is a bad trace and you put a loop to repeat it, something in the middle, it only makes the trace longer. So, trace loops doesn't matter. No matter.
So, two ways to solve this. I break the loop. I say, if enable is zero, then in the next step, enable must be one. I put a logic around this. This is the assumptions. Okay?
The other way to solve this is to look inside and say R should be equal always to S. It will not make the proof wrong, wrong, because you are only strengthening the, the, the assertions.
You're not allowing anything more that you already have. So, if you say R must be equal to S, you are not doing anything wrong. So, what will happen is these two will gain the X.
By the way, the X, I said, are the bad states, right? The X, you, you, you know it. So, now I put X here and X here. So, the induction only has this, this X is up there too.
To see about. And then in K steps, it works, because there is no arrow from here, from, from these bad states, you can go to here, but, but, but not from here. So, induction will work if these two are bad states.
Okay. So, this is the kind of thing you have to worry about in formal verification. Yes.
Well, this is a flip flop with input. So, R will equal D after one and eight, one step. So, it goes from zero. It can start from here to here. And in next step, S will be equal to, to D, R will be equal to that, to D.
So, it will be one on one. Or if it's zero, next D is zero, it will stay zero. So, but you actually cannot verify this. You cannot verify, like this, you cannot verify that D equals R.
Because D will, R will equal D in the next clock. So, with this, you cannot assert anything. So, what you do, you put a test harness around it. So, you capture D in S. Now, S is extra logic, which you need to prove that the flip flop works.
So, I have here D, R, and S. So, R, S is supposed to be equal to R, equal to zero. So, it's supposed to, or if D is one, then eventually both will get one. So, the good states are zero, zero in the end, R, and S, zero, zero, zero, zero, or one, one, one, one.
What are the bad states? Zero, one, one, zero. One, zero, zero, one. So, yes, the induction will work here, because this bad state can actually be reached. So, with zero, zero, or one, it will already work.
So, this is an instance then where you need extra logic, external logic to prove things. And this is, well, I will not talk about this one, I just put it to scare you. Okay? Too many arrows, too many states, okay? Okay.
Okay, so this is what will be, this will look in high level definition, much high language. This is very log. So, we like usual, the simple one which has the feedback. So, R equals R.
And then, you have this extra thing here which, if formal is definition, is defined, then you assert that R is false. Okay? Not R, or you could write here R equal equal zero. It's the same thing. Okay?
And this one won't be present if you target an FPGA, for instance, only on formal.
So, you write the symbiosis write file, you prove, you put into the mode prove, you can do also BMC, only the base case here, or induction, you can choose.
Here's the decay that I talked about. It is one or ten, what you need to put here. Then, the nice thing about UOSIS and formal verification, the engine which proves that statement, the long logic statement, this one, the engine is standardized.
This output is a standard, so you can put, you can choose the engine you want. You drive it from UOSIS, but what proves is actually EISIS or Z3 or anything else that assets the output logic description that UOSIS outputs.
Okay? So, this is instructions from for UOSIS here, and there's one missing here, which it is implicit, which is write SMT, write the logic here. But here you put the number of, name of the VADILOCK file and the top level of your design and the files here.
And then you run it and it says induction, trying step one, trying step zero, and trying base case, summary, pass, it pass, so, proof, successfully proven by K induction.
And it passes. And you put this into your test suite, GitHub, something, GitHub, or not GitHub, sorry, if you can. Continuous integration test suite, yes, CI.
This is an example with a Python-based language, so you put imports here. This is an engine, by the way. I put here two registers instead of one because it will optimize away if I put only one with feedback, so I put two with feedback.
Okay? And S will equal run and R2 in the next cycle. If the enable is true. This is one with enable. And then you assert that S is false, always, because in the initial state is false, is zero. So it will all be zero.
And that is what happens, forget this about a moment. It will fail induction. You remember, you can stay with enable false for infinity. That was a loop. So it outputs the failing case here.
It will start in the case where R is one and S is zero. And I don't only care about S being zero, but S will be one here. How?
So enable was false for a long time. Then in the last possible time, it raises enable to one and you are cooked. Yes, you failed. So you go back and do the things I said.
You assume that R either enable is true or in the past enable was true. So you don't have a choice if you're not enable now, you'll be enabled next. So this, only this one will solve your problem.
And the other one is this. You assert that the R, the internal state is zero, which is true. You are not making any more mistakes. You are only making stronger conditions. Now R must be false.
Then you can prove it in five steps. And now it will pass. Like either one of these. This one, that's why I said this one is equivalent to gray box, maybe your design is not a black box. You need to see inside.
There is an internal state which is not reached maybe. So this is how one way to put memories in the team. So test memories. So this is a memory. One way to test memories. You can have gigabyte of memory.
But what you do is you only test one address, but which address, any address. And then if the address is that what we tested, it will be captured here. And if you read from it, it will show the capture data and the data need to be equal.
So that's a way to test a memory. If it works for any one address, it will work for any address at all. So you can have gigabytes of memory or megabytes. That's the same for you. You won't simulate gigabytes of memory. It only simulates these registers and the memory location. One memory location.
And this one is if you have a pipeline with streams, you can count the number of transactions coming in, the number of transactions coming out. And then you say the counts need to be compatible.
You cannot have more coming in that coming out. That will mean you drop it, packets. Or if you have more out that coming in, then you are duplicating packets. So that's a way to test.
And that's one. I'll skip. Okay. So thank you.
Thank you.
Questions. You have questions. I haven't till when.
My talk ends in five minutes. So you can. Yes, please.
In the example you've shown, I saw that the depth was manually specified.
Wait. If you can wait a bit before leaving, I still have five minutes, please.
So in the Python code you showed, I saw that the depth was manually specified. If the proof changes over time or you adjust your circuit, you need to also adjust the depth.
Yes.
And if the depth is insufficient, will the proof fail?
Indeed. Well, the question was if you adjust the circuit, will the, will need more steps in the proof? Yes, definitely.
And more importantly, if I change the circuit and I forget to change the depth, will the proof still pass if it doesn't have sufficient depth?
If it has insufficient depth, surely we'll have a failure. Yes.
Next question, maybe. No questions. Well, if you think about a question, please.
I have five, some minutes left. Thank you.
Okay. One more.
How does this scan to big circuits? Like how much time does it take?
Okay. Good question. Good question.
So I thought, please come down, people. The question was if, how much time it takes, what the complexity is.
So one problem with a final verification, you can never be sure.
You can have a simple design which takes tens of minutes. You don't know why. You made a modification. It, one second.
You want, because, and the other thing is solvers. Like I said, you can change the solver. Okay.
If you change it, one will be fast. The other will be slow. If you change the circuit, vice versa. Okay.
So it's non-deterministic, really.
Yes. Good. Thank you.
Sorry. I, I was a bit nervous earlier. I am actually a dev room manager for this session.
So I, I'm partially giving instructions to people here. Okay.
Thank you. So the audience thinks I'm, it was good. Perfect.
Well, if there is no much.
Okay.
Excellent. Thank you very much.
Okay. I'll finish then. Thank you very much. You can.