Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/705 Thanks!
I have the tremendous pleasure
and the big honor here to see you,
Clifford, for the most of the guys who
know him and the other guys who don't
know him.
Be warned, because
this man is like a bullet
train.
So the moment we press that button,
start the start
the race and you be
careful.
So fasten seatbelts.
Ladies and gentlemen.
Here is the man.
Thank you. Yes.
If you put it in play.
So, OK, this is my talk about
form verification with yours as SMTP.
See it.
And it's the.
This is my talk about format verification
with your SMTP, BMC, and
it's a shorter version
of my talk, but I still need to
speak very fast.
So if you're interested in the
full flight set, go to this
link.
The link will be also on the last slide
of this presentation. So you don't need
to like, write it down right now.
And you can also download all the
profiles files. For example, as I showed
you during my talk from from this
page. And my
my goal is really to just
give you a
rough idea of what you can do
with the refusers sometimes here
and then you can download the sample
files, reproduce the stuff that I can.
I will be talking here and then modify
this examples to fit your
verification needs, whatever, whatever
you need to do.
OK, but really
quickly, if just a little bit about the
users as a whole, because
there are a lot of things you can do with
users besides formal verification.
So there are a lot of syntheses, flaws
that are available in users.
So most prominently we can do synthesis
for for the future is I had
the talk last year at CES
about that and I had to reverse engineer
this for the bitstream format in order to
enable this flow.
But there is also a synthesis Flarf
exciting seven series features
here. You need to use sailing's we've of
a place and throughout, but the synthesis
part can be done by users.
There are also a couple of async flows
that are enabled by users.
You can also do your custom synthesis
flows, which is something that some
people do on the formal verification
site.
We have users S.A.
BMC, which is the thing that I will be
talking about today.
But there are also some other
verification flows available in
the also's.
For example, there are a couple of built
in comments in users directive that can
be used for certain verification
tasks. There's a built in sub
so that you can use for some things.
There is an equivalence checking
framework or you can use
your source just as a front end to
convert your design into something
that can be understood by other tools.
For example, you could use users
as a front end and combine it with ABC
and to verification in the ABC.
But the thing I'll be talking about is
the first one uses some key here,
a framework for bounded model check
or induction enabled by users.
It can be combined with any existing
SMPTE to solving
so that there is not a lock in here to
one specific Soulsville.
You can combine it with anyone because
I'm using the Asanti Liberta language to
communicate with that soever.
Um, and there are a couple of servers
that will test tested.
So usually when you read here, support
that Tolliver's, it means well tested
saurus because in principle with
any source that supports this file format
and those will test it, all of us are,
for example, said freakier
for ICS and so on.
Good, but before we
dove into a formal verification of
this slide and this is my
way, you should be excited about this
slide.
So I have
some thoughts here about the availability
of other tools for students,
for hobbyists, for enthusiasts
who just would like to experiment with
the technology or that kind
of stuff. And on the FPGA synthesis
site, there are a couple of free to use
tools. So if you're interested in playing
with this kind of technologies, you can
just download the free stuff from filings
or other
vendor and install it.
And maybe within an hour or two,
if the installation
goes goes without any major difficulties,
you you can play around with it
and you can start making
your experiences with this kind of
technology and with FPGA
synthesis, even some
free and open source options.
So there is the orses
floor with Project Isong on 540, for
example.
But this is not the only one.
There is also Vitara within two or
three frameworks.
So there are a couple of options.
The same thing for HGL simulation.
If you would like to simulate a circuit,
I would like to to make
your own experiences with FPGA.
By HGL simulation, you can
download some free to use tools like
Xilinx, XM and
even some open source tools that you can
download and start learning about
this kind of stuff just within
minutes. However, take how
long it takes to install.
We are not using up get something like
this.
However, on the formal verification
side, we have a completely different
picture. There's practically no
free to use tool that is.
Besides the things I showed you today
know are free and open
source told that you could use to do
and format verification.
And interestingly, at the same time,
people in the industry are complaining
they can't hire anyone who has
experienced performer verification.
And I really wonder why why this is
so why there are no people with formal
verification even though the industry
demands them.
So I think this should be
the the focus of that.
I can't really tell you stuff like how
fast is my floor compared with the
commercial floors because I don't have
access to those commercial floors.
I have.
I had no way so far to compare
my stuff with the commercially available
stuff, because even so,
I,
I do some research at the University
Institute and I have some commercial
software that I have nothing that's
comparable on the farmer verification
front.
So I think it doesn't really matter that
much if my tool is
faster than the commercial
tool, if it supports exactly the same
features, that the really important thing
is that this is something that enables
you to to make experiences
with this kind of technology.
And hopefully one day
I will be able to compare my work
with the commercial tools and then I
will know if I'm better
or if they are better or if they're
about equal.
OK, so when we're talking about farmer
verification, what are we actually
talking about? And in almost
all representations about this kind of
stuff, you will find a slide that looks
more like like this one
that have a couple of
of of states Yazaki it can be
in.
And the couple of simulation traces of
the simulation traces are there.
I don't know what what color
this is, but this here is
a simulation race.
Oh you don't see it.
This here is one of those simulation
traces,
and you see we have three simulation
cases here and they cover a
subset of all the states,
interestingly, that don't cover this red
state. And the red state is a red state
that violates an association.
So when we would like to verify it this
second, we would like to be sure
that we have caught this red state that
we have shown that this state is actually
reachable.
One one way to improve
the coverage here would be just
to run more and more random simulations.
However, if you look at this example
really carefully, you will see
that there is only one possible path
that goes to this one, one red state.
And one of those traces almost got
there. But the last minute
decided to go a different route within
the states diagram.
And if you just multiply it, the choices
you have at each node on this path,
you will realize that you could run
a thousand simulation traces on this
really, really small example.
And you still only have about 50
percent chance to to
to get to this one red state
that violates your assumptions.
So random simulation is not really
a solution if you would like to make sure
if an invalid state is reachable
or not, you have to use former methods
and the former methods actually
like look at the whole state
diagram as as
a whole. So it's not simulating many,
many individual places.
Instead, it will give you a definite
answer if this state, this red
state is rich or not
in this situation.
And then you simulate that a
lot, you can be
fairly certain.
You can be more certain if assimilate for
many, many hours, but only
with formal verification.
You can absolutely be sure that no
assertion can be violated in your
design. So that's that's what they're
talking about. And we're talking about
far more verification.
So why would we do this?
Why would we want formal verification?
And in almost all
cases where people use formal
verification, they have to first
use case. They would like to prove
that at the sign is correct.
And in many cases, this this is
a really good reason to do formal
verification. I just told you, when
you have to be sure this is the only way
you can can achieve them.
However, proving that the
design is correct, even if you have a
formal verification tool, is a pretty
hard thing.
So first of all,
you need a formal specification of the
correct behavior if you don't have a
formal verification of the correct
behavior. How can the tool know which
is the right behavior and which just the
wrong behavior and
usually just this one step,
creating a formal specification
of the right behavior can already be a
showstopper.
This could be a project so that
you you wouldn't think it's worth
your your wine in
many applications.
So maybe if you are in
some space applications,
you can get around it.
But in many other cases, people
might say, well, if there is a problem
in the field, I'll just create a new FPGA
image and we will figure out how to how
to update the devices in the field.
However, there are two other big, big
application domains for formal
verification.
There is back hunting and there is
optimization.
And I think usually we don't
talk about this to that much.
And I think the reason is that the
pricing on the commercial tours is
prohibitive.
So you only buy
those commercial tools if you really,
really have to.
And the only case where you really have
to is if you have the first case, if
you need proof that the design is correct
and many projects might benefit
from having formal verification around
for background hunting optimization,
but they don't do it because it's not on
the radar.
So what is the difference between
counting and proving that the design is
correct? So first of all, for accounting,
you only need a partial specification.
If you just have specified some part
of the circuit, you can use the former
tools to figure out if the socket
at least conforms to this partial
specification.
Maybe there is other stuff that is not
specified with this partial
specification, but if there is a back
that is somewhere within the specified
domain, then then you can use this.
The other thing is
when you do back hunting, you can do
many different checks
with different overlapping
partial specifications.
And you only need to have a
really good feeling about that.
All this overlapping specifications
really cover the entire.
Havey off the sacket, that's when
you want like to prove that the design is
correct and you would like to fracture
into individual small checks,
that you have to have a second proof
that proof that you haven't left and the
gaps with this partial
specifications.
And there are cases where people do
that and they claim that the first thing.
But actually they don't because this
this are questions that are left open
if you do that. So this is just one
thing, but it can be really beneficial
to have those tools for back hunting.
Usually they will find
Besar a box really, really obscure
box packs that you would never find
using handwritten test
benches because nobody comes up with
the crazy things they do with
your design in order to trigger
an assertion.
So not only will it find
bugs, it will find those sparks
that are really, really, really hard to
find in the field.
That box there you have a processor
and that works really fine.
And after a year that is in the field,
someone comes to you and says, well,
there is this one plug in.
And if you use this binary for the Skemp
plugin and you run it an entire day,
then it will somehow crash the
process. So at one point
and this is like the thing you get as
a back report and then you have to figure
out how to go from there to
the one obscure thing in your
instruction cache that went wrong.
And that was triggered by this one
scenario.
Um, so the R
but if you find the same back here,
the will give you a counterexample.
It will tell you. Well if I,
if I, if I use the inputs of your socket
in this way, then the socket will go into
the estate. And here you have said the
state is an invalid state that should
not read it. So you're in a much, much
better position to have to
figure out what's actually going wrong.
Even if you could already reproduce the
bug in hardware,
you would be on the very different
standing here.
So so be the hunter.
Don't be the hunted.
When it comes to the box
with optimization,
we essentially do
the same thing as we would do when the
proof of design is correct.
But we just use the an optimized design
like a spec.
So we have already a design that works
and we know this is that this behavior we
want and that we would like to optimize
the kind usually of any optimized call
your make it a little bit more complex.
So if you would like to optimize
for power, for example, you would add
are allocating in certain cases
and then you have to put
additional thought into which
flipflop stage can be
located in a cycle.
And if this if there
is a problem somewhere, then you would
find this by formally verifying you
optimized design using the, um, optimized
design specification.
In this case, this would be very, very
similar to farmers formal equivalents.
Checking, however, there are cases
where your optimization reduces the
number of cycles needed to produce
the same result.
And then we are already beyond what
formula equivalents checking would do,
because now we have two circuits
that are formally not
equivalent, because once this
circuit is producing the result one cycle
earlier than the other one, but we could
still construct a farmer proof using
property checking to make sure that the
result both circuits produce
the same.
OK, I'm not really going to talk
about the things on the slide here.
This is just to
to show you it's really easy to install
this on an open to
anything beyond those of other
distributions, of course.
So you really have no excuse
for not trying this out.
If you do anything about formal
verification, could be could
be useful. It's not like you have to
spend an afternoon compiling for tangoed
from the 70s in
in instead you just
get some prerequisites and then you build
your source and then you build a set
and something solid.
And after 20 minutes of
however fast
your computer can be large C++
projects, you have everything in start
and you can playing around with
the examples in this presentation.
So the first
link is the same link you had on the
first slide.
This is where I can download the slides
and also some examplar files,
some example files that can
also be interesting are the examples
in example, slash SMTP E.M.S.
within the order source code.
And if you know my pick of
the two project, that's a
five implementation.
There's is a couple of former staff there
as well.
And it could also look
look, they are far more examples and
crazy things you can do with this form
verification.
OK, let's let's get right into it.
Some code.
This is simple HelloWallet example.
So if you have accountably initialized
the counter to to zero in this case
and then we have a clock block and we say
whenever we get a rising clock, that's
when the reset is higher than
countervail to zero.
And then reset is not high.
Then we will increment the content.
And then we have some farmer statements
at the at the end of this input.
So we assume that the counter
will never reach the value of ten
and then the Assad, that the counter
will never reach the value of 15.
And since we are incrementing and
steps of one, we never can go
to 15 without going over 10.
So indeed, this should
hold to verify
this. We call this three
commands on the lower right.
The first command is.
So if you use your for a synthesis
of this circuit, but they don't
synthesizers for an FHA
or an async architecture, instead they
synthesize it into an essential to
description of this circuit.
And then we use users, SMTP,
E.M.S. to check if
the assumptions are right.
And we have two calls here.
The first one does a bounded model check.
So we check if the
socket
if all the assumptions hold within
the first and cycles, the default
value is 20 at the second call
tries to perform an induction step
to prove that. In fact, that doesn't only
hold for the first end cycles.
It holds for infinitely many cycles.
It holds forever.
This is what we would like to do.
In most cases. We would like to do that.
Something holds forever.
However, in some cases with very
complex designs, this can be hard
to achieve.
Then you are in trouble if you would like
to prove that your design is correct
under all circumstances.
But if you are, for example, back
hunting, you could still save Allahpundit
model check for 100 cycles.
Gives me enough competence, confidence
that that actually this
design is correct and works as expected
because of my understanding of
my design. I know within hundred
cycles that should reach all the richer
states anyways.
So when you run it, you you get
this output and
the first one is for the bounded model
checks of it, just check
the assertions, hold assertions
in timestep zero, then after
one state transition, do they
hold in state one and so on until
we reached state 19.
And the other one is the induction
step at the induction step count
backwards from 120.
And if it's very easy to prove something
by induction, we will talk a little bit
more about this later in the
presentation.
Then this will maybe try to
improve induction and step 20 and
then step 19 and say, well,
it's passed, everything is OK in this
case is a little bit harder
and we need to go down all the way
to step 15 before the
induction vox.
And then we'll see a little bit later of
why this is.
OK,
so who here knows
a little bit of relock?
Oh, that's good. It's at least at least
maybe maybe maybe 30 percent, maybe maybe
half of that. That's correct.
So for formal verification, you need to
have some additional statements
in the language.
Namely, you need to have a way
to create assertions and you need a
way to create assumptions.
And we've seen those assert and assume
statements already in the world.
Example I just showed you before.
So when you have a stop, some expression,
it just says we say
this expression must always be true.
And if there is a way to make
this and this expression of forest, then
this is a back. And the tool should tell
us how to get into the state to
demonstrate the readability of
this back to us
and assume we also say
this expression is always true, but we
don't say it's an inherent property of
the design. We say this is something
we
we restrict our proof to.
So in some cases, you might say
we assume that this input
signal is only always low or
we assume that those two inputs
are never high at the same time, maybe
because this is some kind of a protocol
and we assume that the the other side
of the the product might appear to talk.
This protocol to this
is using the protocol correctly.
And maybe in this protocol, those two
signals can't be asserted at the same
time, restrict
for verification, essentially does
the same thing with, say, we don't want
to consider traces that
this expression is false.
We only want to conceal the traces.
What this expression is true.
However, there is a little
difference in the circumstances
when you use assume and then you use
restrict and
assume you use, then your
assertions depend on it.
When you say, well, if this assumption
doesn't hold and they really don't care
about this, because I know if,
for example, it is two lines
that both at the same time,
then my car will go into some crazy
state because I
brought my car under the assumption that
the I'm talking this protocol to Will
Will actually the product specification
with restriction V,
v, v essentially say
this makes the proof easier
if you assume this expression, but
it's not really necessary for our
assertions to hold.
And because of that, then an assumption
is violated.
Simulation will also produce an error,
but even a restriction is violated
in simulation. Then they don't care
because we've set assassins' don't
really depend on it.
It's just an additional thing for formal
verification
that makes the proof a little bit easier.
There are immediate assertions
and concurrent assertions in the Haluk,
so immediate assertions
are within the behavioral block like
initial always and
the we can use, assume and sound
like like a normal statement.
Concurrent assertions are used
in your context
and essentially assume or assert
that something will hold forever
in our state.
That is in the behavior of our part.
We could use an if statement to
try to add an additional a condition
to discussion or an assumption.
And then this assumption assumption would
only need to be true.
Then the if statement Audiovox
usually the concurrent assertions and
they are used with system
of properties that
can be temporal properties.
But right now your source doesn't support
any of that.
So and because of that,
we could say
when we're using users, when they're
using this flow, then usually we
will use immediate assassins', but
between within and behave a block like
initial olelbis.
OK.
Former test benchers,
so in simulation, we usually have a test
bench that creates input
signal as far as I could and stuff like
that.
With formal verification,
you also sometimes use test benches,
however, those test benches don't
play through one possible
path with our circus like a
normal simulation test against us.
Instead, we
would just add some external restrictions
or assumptions for stuff
like well researched below
and the far sighted things like that.
But other than that, we believe a lot
of our free room for the verification
tour to actually explore
different different parts and
and and see if
using the thing in the former
test bench it can can reach
an invalid state.
So this is a variation
of of the science
we had before the HelloWallet design.
But now we're using your former test
bench. You see, I've removed
the initialization for the counter.
So now we only have there's always blocks
traversable.
If reset is higher than the set, count
to zero. Otherwise we increment count.
And then our former test bench on the
right, we assume that the reset
signal will be higher initially
and the first cycler.
So because of that, we we
we've reset the design from outside,
from the test bench in the first cycle.
And then you have the same assumption and
the same combination you had before,
but now with a condition around it
that we don't check it in in the initial
state.
So in the initial state, they don't care
what the count is because it can be
anything.
They just paid for the reset to complete.
And after the reset has completed,
then we are not in the initial state
anymore. Then we actually apply
our assumption in the.
OK.
This is a slide I thought I removed.
Oh,
yeah,
so bounded and unbounded methods.
This is this is terminology you will hear
a lot when when when I'm
reading.
I'm talking about a former method,
a bounded method, essentially says
we check that the property holds within
the first End-Time steps.
And we had this before here and I just
call yours SMTP mce without
a parameter then given the bounded
model check for 20
cycles and then inbounded method
is we would like to prove that the
property holds forever and not only
for a limited number of
cycles after the initial state.
So PMC, which is part
of the user Stasch assumptive
BMC name is bounded
model check. That's a bounded method
and temporal induction is a mechanism
that that builds in a
way on a bounded model check
and extends the
validity of the of the check
for Fiverr.
Let's have a look how we can do that.
That's the bounded model check.
So we create
a former circuit within our tool that
more or less looks like the example
at the top here.
If you have an initial state in yellow
and then three
states that follow the initial state
does that the green states here.
And for each of those four states,
we check if all the assumptions
hold. So this is the
way of creating a bounded model check.
Remember this now
I like former states like very obvious.
They're like placeholders for all the
states that are possible.
The only thing that they constrain as the
first one should be a yellow one.
It should be an initial state.
And the others don't need to be initial
states. Their only constraint that there
must be a valid state that can
follow after
the initial state in case of the second
and so on.
And this works.
So this is a correct way of making
inbounded model check for four and equals
the three time steps.
But it's not very efficient.
And in practice, it turns out it's
much more efficient to use the scheme
on the bottom half of the slide.
The first just create a symbolic
initial state. So as symbolic state that
can represent any initial state
and the check is there and the initial
state that violates one
of my assertions.
And if there is such an additional state,
then we are done. I just output the state
and say, well, obviously this initial
state violates our sanctions.
So this is your counter example.
If this
does not succeed in
the way for the tool we've got, the tool
would like to find the back so it doesn't
find it back here.
We figure out that already
initial states actually conform
to the assertions.
Then we create a former
model for two states.
And now we can we can assume
that all the assertions in the first
state will hold because that's what we
just proved in the first state.
Uh.
Yeah, and so on, so if I find something
here, but a counterexample that's too
steep, if it doesn't count.
Well, we move on to the to the next
state, our next step and make
it prove that the three
cycliste and so forth.
And in practice, this turns out to be
much, much more efficient than the
naive approach.
I would like to prove like everything
at once, especially if you would like
to do a deep founded model check like 100
cycliste or something like that.
So tentpole induction now
takes one of those bounded model checks
of now we have one of those founded model
checks above.
It's then the implementation that really
doesn't matter.
And then they create the proof that you
see in the middle of the slide here.
So initially we say there
is an initial state followed
by three other states and none
of them violates any assertions and they
have proven that.
And now we would like to prove that.
Then there are three states.
Consecutive that don't violate
assassin, then there is no way
for a first date to violate
the session.
And if this if this works, if
we can prove this, we have obviously
proven that this option will hold forever
because.
This here kind of fits together, so
they can just say, well, we have proven
one, two, three noninsured states,
so this exists and if this
proof holds, we know every
state that follows the failed state here
must also
conform with our assumptions.
And then I just take this
proof that I have made and I don't need
to change this proof.
I don't need to rerun this proof.
Just think of moving this one
step to the right and I can apply the
same argument again and again and again.
And therefore I have proven that my
properties will hold forever.
So this is great.
However, it doesn't always work.
So if if this kind of thing
works and tells us, well, the
science seems to be fine,
then
then everything is good.
But this might tell us I can't
I can't do this.
I can't do this proof.
I find a counterexample.
And now this counterexample can
mean, well, maybe my assertions
are violated somewhere deeper in
the state space or it can mean
well, maybe,
maybe everything is correct.
But I just need a deeper induction
proof. Maybe it doesn't work with three
time steps. Maybe it only works with 20
or 100, or maybe it doesn't work
at all.
And that's what we see in this picture.
So.
Here again, we have the states
that violate assertions and that
then we have all the states in
this area. So if you look
at the direction of the arrows, you see
there is no arrow going out from this
either barber to the barber.
So there's actually are the regional
states and the systems.
However, usually we don't have an
explicit representation of an explicit
picture like this of all the states.
And then we have this this
intermediate zone here
where there are states
that are OK with our sessions,
but nevertheless unreachable.
And when we look at this proof
that we are trying to do this here,
we don't we don't know if these states
are very chipper or not.
So we could, for example,
find here one, two, three
states that are OK with our assertions,
followed by a state that's not OK with
our assumptions.
So if you find something like that are
the easiest thing we can do, we can
increment the index length.
So here we need at least five
consecutive states because they are.
But if you say we have proven for five
consecutive states that are OK with our
sessions, then
then we won't get a counterexample
here. However, we might get
a counter example here.
Why?
Because there is a loop and
in this loop I can fit and arbitrarily
long sequence of states that are
OK with my assertions.
And then in the end I break out and
reach this state here.
So here I can't just make the induction
longer, have to use something
else. For example, I have to add
an additional assertion to my design
that invalidates one of those four
states that built the loop.
And if I do this,
then I can can prove this example
by induction, because I don't have this
this this loop there anymore.
I'm.
So when
you would like to do this one, you would
like to make such a proof of
this is the entire floor, you'd be
using you you'd use you take
your lock designed your assertions, you
put them through your source.
You also generate some key tulip model.
Then we put this into yours as SMTP,
BMC, together with an external
constraints. Fine,
pass it to the server and
then I get a pass fail information.
And if it fails, I get a counterexample
with if you file or a
test bench that reproduces the
counterexample, why are constraints filed
that I could put back in on
the left side?
For example, if I would like to just
easily reproduce
a thing that I found before.
So the typical backflow would be
the fast run abounded model check.
That's the easy part, we say
for 10 steps, for 20 steps.
See if you can find a violation of my
assertions within 10 or 20 steps.
And if this is
if this fails, then we know we have it
back.
We know we either have it back or one of
our suggestions is bogus.
This is, of course, also an
option.
So the solution is either fix the back
or add additional assumptions
or loosen the sanctions
so that everything is fine.
If this passes, then we move on to
step two.
And step two is this this temple
induction step.
And if that fails,
then we have to investigate the
counterexample we get and make a
decision. Is this remember what
the soldier is showing us or is this not
reachable?
This is our judgment call, essentially.
And if it's Cheverton the same
thing as before, we have to fix the
design. We have to add assumption
all. We have to do some assertions.
However, if it's unreachable,
then you have to add additional
assertions usually to tell
the story about that. This is actually an
unreachable state.
And that's that's the kind of dialog
you have with this tour.
While formally verifying something,
the soldier is giving you a
counterexample and you have to explain to
the soldier, well, that's actually not
reachable because this condition
will never become true and then the
sort of give you another counterexample
and so forth.
The nice thing about this is
when it passes,
we know everything is right, but
we still have two options.
We can say we'd be
fine with the thing we have have we have
proven that our design process
verification get done.
But we could also say I would like to
have more assassins in my
design and then I just reduce
the length and I will get another
counterexample now for induction
with with a small
inducts length.
But now I will know that
every counterexample I get is unreachable
and it's much, much easier to
track with this.
And if I make a mistake
and then add an assertion
while of telling
the whole that something is unreachable,
well, the soldier will then tell us
he isn't the sergeant that can be
violated using this at this path.
So there is really nothing you can
inherently to do wrong.
Um, yeah, the
idea would be to talk about this floor
again with this graphics, but I will skip
it.
So we
have a variation of the design
we had before. We have to count again.
But this this time we
have a most important remote input,
tells us if it should count up or if it
should count down.
And we
assume that initially count is five
and viasat that it can never be 200.
And if you stare at us for a little
while, we see this is true because
when it's the count is ninety nine,
we will not increment it any further.
So there is no way to go from
four and five to 200
or so. There is no way to do it with
another floor on the floor because it
count to zero.
We also don't incremented anymore.
And if we run this, uh,
the bounded model check
will work.
However, temple induction will not work.
It will give us a counterexample like
this that starts with one
hundred ninety four and
then increment and increment an
incremental decremental that will
do some things here really, really close
to two hundred. And at the end of the
count example and then I can increment
from one hundred ninety nine to two
hundred.
Of course the thing is,
the reason why we get the counterexample
like this is because we haven't really
told the server that count
equals one hundred and ninety
four is not reachable either.
So if we modify our design like this
and we add an additional insertion of a
say count is always smaller
than 100, then
the proof will work and we will
have proven that all this assassins'
actually put.
And because in the example I had first
I was only incrementing
and I was saying, we can't reach step
10 but the Assad
so we assume we don't reach Lieutenant
ViaSat, they never reach 15
because of that. I had to have 15
steps in my temper and five
steps in my temple and proof
from 15
to 20 in order to prove that now
that we have correctly described
the entirety of our state of our design,
we can actually complete temporal
induction with just within just one
second.
OK, I have some some some other examples
that I just would like to mention
quickly. Now,
there is a special command
called SRP Mook's
that adds additional assassins
to your design whenever there is
a parallel case statement.
And then this this example, we have
a parallel statement in the analog.
So we as a designer tell the tour
that those two cases and the parallel
case statement are exclusive and
that we might use this information
to do any optimizations.
And if if we are wrong about this,
this thing that we say well, is the case
statement is parallel, then we
might run into.
Even more problems
because we might, for example, test
our design and FPGA for many,
many hours and everything, that's fine.
And it turns out the reason is because
maybe this FPGA tool in this instance
has ignored the parallel case.
But then we go to an for example,
and we synthesize the same thing with the
AC tool and maybe the AC
will actually use this parallel case to
do an optimization.
And then all these hours of testing we've
done on FPGA is completely worthless.
But with a formal verification tool, we
can, of course, prove stuff like that.
Um, that's another
example. I have a memory design
here and I have another memory design
that's kind of convoluted, but sometimes
called looks like this.
And it would like to force synthesized
water into a
special form of of the resource.
It would like to prove that these two
memories are equal.
And if we if we do that, we
create this kind of formal test
bench that just instantiates both
memories in parallel.
And then we add this additional
constraint file on the upper right
that we assume that in the initial
state, the the memories in
those two instances are actually the
same.
And then for all the other states,
we assert that they are still the same.
And we also assert that the output, the
same value for the same
input and the input will be the same
because the input parts are connected to
the same top level input.
This is an example for using
multiple domains with yours.
SMP BMC is just to
show you that this is something that's
also possible.
So here we have a
counter, but we implement this
counter just by using the
the lower bid we've just created as
a clock input, another Pockley flipflop
and then we go on.
So if you're building
acounter from like Title
IX, then this would be a possible
way to build account counter.
Usually don't do this on a chip
because now we have one, two,
three, four different Tuckerman's here.
So the first Orvis block is like the
regular counter and then the other
four Orvis blocks are
the bits for our other counter.
And then we assert this two counters.
They must always have the same value.
And indeed I can,
I can prove this.
I need the special command clock to f
logic to enable this,
but then this can be done
similarly. This is another design
that I have a set reset flipflop.
Never use something like that in the real
design. It's horrible.
But if, if you have
to use it for some reason, we
can we can actually check
in.
And of course, and
this is actually what exciting stories do
for us, we said flip flop because they
don't have the resources to create
this weird thing with two flip flops on
the latch and them.
And we can actually prove that this is
the right thing to do, that this is a
flip flop like this can also
cost them things.
I'm not going to talk about them.
There is a larger project going on right
now trying to do end to end farmer
verification of his
five processors.
It's called Risk five former US.
I'm working on that right now.
And this is also, of course, using
a lot of this infrastructure
to do this kind of verifications.
If I would like to look into a more
complex thing that can be done
with farmer verification and with this
farmer verification floor, that this
would probably be worth a look
at future work.
Well, I would like to add more
system lock assertion,
property support.
This is just something that you will find
a lot of existing code for farmer
verification tools.
And it would be interesting to be
able to use some of that with this flow
as well.
Then there is improved support for the
propagation.
So in some of my other farmer
verification flows, I can actually
model the propagation
exactly the way the way
I like LRM is specifying.
It would be interesting to also
be able to do that with this flow.
I have on my to do list
C backend for users so
you can take a circuit and
convert it to a flavor of C
that is is good for farmer
verification with see farmer verification
tools like, like C bruv.
Yes. BMC, stuff like that.
And also there is a project going on
called Symbiosis, which is like
a big front to, to
use all is userspace
farmer verification flows
without having to land.
And you think whenever you switch
from one floor to another,
that's it.
So what did we learn today, Clifford?
What did we learn today?
What did I learn today that I can speak
very fast? No, no, you were really
something you do in the normally in half
day. You did in the hours.
Yeah, yeah, yeah.
We have some questions at the audience.
I know there's one on the web.
I will take this right now.
No.
That's disappointing, but we have some
others. This man, please.
I did not yet understand what
is the difference between Yosses and just
using, like, any
kind of very simulator?
I mean, the simulators also
react on assaults and whatnot.
Yeah, but you have to write a test
bench that triggers discussion
and with formal verification, you don't
have to do that. You can't just say this
is the set of valid inputs
and are.
There is a better way to do that.
So
when I go to that simulation,
you just have individual places that may
or may not trigger your assertion, but
this form of verification.
Can I have a tool kit for you?
Looks at the big picture because it can't
paint the big picture. I mean, this is a
comic, but the state
graph for real, VITAC it would probably
have more states than the photons in the
universe.
The country.
Yeah.
Someone else this
I'm wondering if in your experiments
you have actually run into problems with
Vorkuta
that your solutions hold because you have
restricted, artificially restricted
the state space too far.
Yeah, I mean, this is possible whenever
you use restrict, I assume
you have this risk that
you restricted it in a way
so it doesn't really work anymore.
So in the usual backflow, you
often have some vehicle
of defiance or whatever in your design
that you can use to to artificially
add bugs.
And then you always check that at least
you still can find those parts, of
course. This is not a guarantee, but
at least that improves the situation a
little bit.
OK, a question there from outer space,
yes. So what kind of expressions
does he also support in these assertions?
Because essentially I only
support immediate assertions you
can use like any violent expression,
but it's not the system of property
syntax that you could use
to to express temporal
properties, insisting that all of those
are not supported right now.
One last question, yes, sir,
can you give me a rough idea of
how long the of verification
needs?
It really, really depends on the kind
of problem on the soldier you have
on many other parameters.
So here I have a couple of soldiers,
three different benchmarks.
And you see there is quite, quite
a span and always
maybe this is not the can can be seen
here. But but often you
have an example of really,
really well with one soldier.
But it takes a long time with another
soldier, but with a different problem,
just vice versa.
And because of that, it's really good
that we can use the that some people see
with almost every assembly to deliver.
Thank you.
OK, thank you, Clifford.
It's really fantastic to have you here.
And really the will that you're sharing,
your knowledge, your explorations
with all these people that
give him another applause, please.
Thank you.