FV2017 – Coverage Reloaded: Signing Off Designs with Confidence

FV2017 – Coverage Reloaded: Signing Off Designs with Confidence


I the difficult task of keeping you all
awake I hope you had a good lunch I’ll try and do that and you can tell me if I
did it well so why is this coverage reloaded because in a recent
verification future talk I talked about a coverage solution that OneSpin has I
didn’t think I had enough time to do justice to the technical side of the
story and I said to Mike if you give me half an hour in this conference I can
try and do that so everybody who’s here who’s ever done verification would
probably relate to this loop which is starting from requirements you go
through a plan you build your test bench then you run the test bench you find
failures so when debug them and then the internal question as Vince also pointed
out in the morning coverage sign-off or just the date in hand and disabled ship
it off anyways so this talk is about using a tool in an assisted way to guide
you in your sign-off process so I’m going to talk about this if you don’t
measure you don’t know I think Harry Foster said this I think some time ago
and I think everybody would would you know this is not rocket science you’ll
all agree some sort of measurement is required some of the challenges that
actually face all the verification engineers is when am I done?
And when am I done is a question that actually can be answered if you answer
some of the other ones. For example, have I written enough stimuli to cover all
requirements? What part of the design has been exercised by my assertions and
covers? So, I’m assuming in this context you’re using formal verification but
some of these or all of these actually are relevant to other forms of
verification – have I written good quality checks? What does quality mean?
Which parts for the design has been checked by my checkers? And, are all
specified functions implemented? Or have I forgot to implement certain features
or functions and are all specified functions verified? So, the top four
questions are addressed by a tool that we have is called Quantify and it is
meant to Quantify the effect of having had a verification test bench.
The last two questions are addressed by our completeness solution which is sold
as gap free and it is about finding gaps in your specification. So, whereas gap
free is more on the lines of validation you can think of Quantify as more as
problem of solving verification at some sort of abstraction level that’s the
difference between today’s talk I will talk more about how you use Quantify to
attain the information for sign-off. So, coverage and bugs I have been in EDA for
about eight months so I’ve been a user of formal verification tools so many
years and we talked about these things in this room in this conference and
others and we always questioned why bug hunting and collection of bugs which is
an anecdotal exercise should be seen in a different from the coverage exercise
where coverage could be an analytical way of conducting data and bugs are
usually anecdotal both are actually equally important then the way we see
this in OneSpin is there’s two sides the same coin I like to think of it as a
marriage made in heaven for some reason had been in divorce for many years so
we’re trying to bring the two back. So, 100 percent coverage with bugs in design
is unacceptable. I think we’ve all been there where we have 100% code coverage
functional coverage and for many different reasons we could still have
bugs. The thing to note here is ok be in court to collect some metrics we’ve got
tie them to the bugs that we are finding need to assess the quality of the test
bench and answer the questions but what is the overhead of doing all of this is
it the same as your actual verification task is it more is it a small delta so
we believe that extracting coverage should be quick the process itself
should not be a long winded process it should be easy to get the data out and
the report should be meaningful so I’ll try and persuade you to think in the
direction that Quantify offers you that solution. So, where quantity and quality
meet is in a metric driven sense when you actually have a single metric which
gives you an indicator of the quality of your verification so what happens
so if you were using Quantify is you take it as an input a hardware design
and a formal test bench you run your proofs you have some bounded proofs you
have some failed proofs you have some exhausted proofs you have your
constraints and you run a single command and it produces a metric driven report
linked to your design browser as an output and it provides two types of
information one is on the structural coverage and the other is on functional
coverage. The structural coverage is a way to figure out whether your design
was well-formed and whether you were able to exercise all the areas of the
design by your checkers. Even if you don’t have any checkers in this case
assertions you could still find out artifacts about your design. Functional
coverage comes to you because you have requirements specified as
assertions and we are then able to take the functional coverage information and
the structural coverage information and then we’ll a coverage model and we
produce a single report and a single metric to give you the overall progress
indicator so I’ll show you in an example I also believe that coverage and this
verification loop I showed you is an iterative loop an actually collection of
coverage and signing off using coverage should start from the first hour of
writing the design and I’m hoping that in the example I’m going to show you
you’ll find it that it’s possible to do it that way so we believe that the
designer bring of phase of the activity when you’re writing up your design you
have or may not have any complete set of requirements you could still run
Quantify and you can start collecting information on reach ability on read
code didn’t in court so if you are a low-power company who wants to make sure
you haven’t got wasted area in your design no need to wait until your
synthesis part we could find you redundant code on day one. And where
quality and quantity both matter is when you are really assessing the quality of
your verification and to keep it simple I think of them as three different
things missing checks over constraints and missed bugs or when you find them. So,
if you can do all these three things in a single view single frame of window and
that would be quite great. So, what we do is we actually so what
the way to solve this problem properly you need to be able to distinguish how
to assess the results because they’re all kind of different in some ways so we
have about nine different categories in which we split the results to keep it
simple I’ve six categories here and I’ll show you the other three in the next
slides what we are really saying here is give me the controllability information
meaning am I able to make an assessment that my design code is reachable is it
over constrained or is it just dead regardless of the constraints. I can get
this information however in the case of Quantify the way we do this is we rely
on your assertions so when I say reached by an assertion it means if you don’t
have an assertion you don’t get a reachable information however we do have
in the tool a feature which gives you reachability analysis without having to
have an assertion but in the context of the Quantify solution in the metric
driven verification view you do need checkers otherwise you don’t get the
coverage. If you do accidentally write some over constraints then you can find
this by actually looking at your dashboard view and it will tell you that
this bit of the design is unreachable and is unobservable and you can have
dead code regardless of your constraints so we are able to split it out and say
this is truly dead regardless of the constraints. In the observability model
we want to make an assessment on what happened when these lines of code are
actually activated in the controllability phase did they actually
do anything sensible okay it was possible to reach them but do they
produce the desired effect on executing them and it is this runtime behavior if
you like is actually obtained by running an observer ability analysis. So, if you
can actually observe each and every line of the or design with respect to
assertions then you say the whole design is covered if a specific line is not
reached and not observed then we say it’s uncovered but it’s possible that
you may be wiggling a line it may be activating getting activated but it
actually does not do sensible stuff meaning it doesn’t
actually do anything meaningful with respect to the assertions so you could
still be lacking the observability effect so that if that happens then we
say it’s unobserved so you have to be alarmed if you actually get anything
other than light-green so if you are over to constrain or you’re dead or
you’re uncovered or you’re unobserved if you’re in the green area you’re good.
What happens is we run Quantify and it produces produces a dashboard view it
has four different components I’ve only shown three here then how much is space
I’ll show you in the next few slides what’s happening in the top part of
the dashboard is this a single metric at the very top it actually is shown as 80%
of the design is covered and it shows that the assertions were exercised here
in the bottom half and in the middle it tells you if you wanted to exclude
certain code because it was verification code of or if it will just redundant
code or you could manually control the wave waiver part of it. It also tells you
whether you had a witness past what was the radius tells you which branches were
covered. Now, if you are interested in finding out what happens why am I only
getting 80% coverage then you can actually just open up the design browser
and what happens then is you start getting this information in a
color-coded format that makes it really easy to figure out what’s going on. The top part which is the green pin is covered this bit is over constrained
this is dead and this bit is uncovered so now you can look at a certain code in
the design and can make sense out of it as to why it is uncovered or an observed
or dead Let me show you this on my favorite
example and quite a few people in the room who know me from FIFO seem to
have the same repetition in OneSpin now. What I’ll show you in this example is
a test design so we have this design which is a circular buffer so we set and
clock pins it has a write in a read on a handshake takes data in reach data out
we’d write pointers and internal data array and empty and full flags so what
we really wanted for this device is to keep the
data categorically ordered not drop it and country order it and unduplicated. So a
very high-level if I was building a serialized device I would expect a
device to have this behavior here it’s those happens that this is a FIFO
here now I’m not saying you have a proper
verification planner it would be good if you had one and you can write this as
systematically in a planner of your choice and you can still start the
verification. But even if you didn’t have any of that and you were using good old
directed test bench to actually start testing the device you could use formal
instead and you can get better coverage because it’s exhaustive but equally now
you want the true sign-off information so what we’ll do is even before we write
any test bench this is the fourth part of the dashboard we’ll just run the
coverage tool okay and it confirms that actually the whole design is uncovered. It actually could have had dead code in this example it didn’t have that code if
it did have that code it will mark it as black. Because we haven’t written
anything there’s nothing to cover against and it shows you the design
browser view everything is red in the morning you’re a verification manager
walked through your engineers desks have a quick glance and depending on the
color you know you can figure out what is done and what is not done you need to
go and read through the logs by through data and all the rest of it. A test bench that is based on abstraction and this uses four registers
for sampling in and sampling out and builds an end-to-end check for authoring
and data loss and all the rest of it that I’ve talked about. The way we do
this is, we write an end-to-end check using two sampling in registers which
sample in non-deterministic values D1 in D2 and all we are saying is if D1
has gone before D2 that D1 must come out before D2 – so this is an
abstraction model that I’ve spoken about in previous talks. I’m going to use
this assertion base check and let’s see what happens then. Okay, I run this and
I get an exhaustive proof and as soon as I get the exhaustive proof
I also figure out this is the only check I have but I’ve got 63% of the
design covered with this one check and a third of it is unobserved and it’s
pretty bad but I’ve got about 5% uncovered. So, how do we deal with this
and what do we do next? What we’re going to do is we’ll click this file
here because this is being tagged as the design file and now I’m able to see that
actually there is a problem in these two lines of the design which
is really bad it seems to think that a lot of logic up
here and here is also unobserved. I can’t seem to observe anything about empty or
full I can’t seem to observe anything around write acknowledge signal. Here
I have an exhaustive proof of a design not a bounded proof and the tool is
telling me that is a problem. So, let’s debug this let’s take a look at
this closely. One thing that we actually encourage people to think of is if you
don’t have the appropriate set of checks it is possible that you’re not observing
your design signals so notice that in my authoring check I haven’t got anything
about empty and full so it’s quite obvious to think actually I could go and
add more checks. One way of doing this is just go add checks like these so
those of you are familiar with assertions could say from empty and if I
do a sequence of multiple pushes and no pops as many times as the depth and I go
full and I can write the dual for empty and I need one more check to say what
happens to the empty signal coming out of reset so I’m not saying this is the
only way to write it you can write other assertions that are observing the state
of empty and full so once you do this the coverage number increases so now
I’ve got 72% of the design covered but interestingly one of my
checks have failed so I can’t actually get full and two empty to pass so looks
like there was a bug in the design which I could not have foreseen before the tool
told me that there was missing coverage I wrote some extra checks and now I find
a rack was failure. Let’s debug this okay so click this hyperlink here and it
will show you this view Now, the two lines that were actually not
reachable before they were marked in red are now showing as unobserved and these
two lines here and empty is still unobserved so let’s take a look little
bit deeper and I notice that actually in the read acknowledge signal I’ve made an
error in writing the logic for this and it says coming out of free set I’m able
to not read the FIFO so I lower down the read acknowledge and at all other
occasions other than when I am full I have the read ability to read it out so
it’s actually this corner case scenario when I’m actually full I made a mistake
and ended up writing this line of RTL. This is preventing the ability to read
out of a full FIFO because you can’t do a read when it is full so we can fix it
okay and the fix is a natural one so I will fix it and I’ll read on this and
I’ll show you what the fix is in a second now the coverage number has
jumped up by four more percent but now I have no wack was failures no other
failures still the observation coverage is missing it’s now a fifth incomplete
so let’s take a look and what we did as a fix was to actually say if I’m empty
then don’t do a read at all of the times just to the read acknowledge is high and
in a lot of handshaking protocols this is quite normal. I did this however still
there is a problem and I still can’t actually get the hundred percent
coverage. What I do now is at this point I’m thinking the tool thinks
actually that there is a problem with the write acknowledge so it’s kind of
funny because I do have an end to an authoring check which does do writes
and reads but the tool seems to think that even though you might be doing
writes and read still the write is unobservable. What I will do now is
I’m going to go and write checks so on write acknowledge and read acknowledge
and they’re really good checks to write because they can detect deadlocks in
your device so I go and write these checks and I put some fairness
constraints to get them to go through and once I write this the coverage now is in the region of 90%
okay so not only do I get them to pass I am not only 9% unobserved and I’m doing
really well because I’m still hitting my exhaustive proofs. But what about the
remaining nine to ten percent. Why is it important? At this point if I don’t
have a tool that gives me this information in the form that I have and
if I haven’t exercised these buttons then I’m very tempted to sign off
because there is almost nothing that can tell me if anything is broken. The
problem is that there is still a bug in this design and actually this last 9% or so is actually telling you just that. Let’s take a look at this
chappy bit more closely the very top. I have got explicit checks on the
handshake signals so why does the tool think I’m not observing the right
acknowledge so let’s zoom in a bit more and let’s take a look at this what it is
saying is coming out of reset right acknowledge is one which is to be
expected the device is ready to read the data in it should be able to write the
data in, sorry. If I am not full absolutely fine to write stuff in but
when I do go full the write acknowledge goes low in the following clock cycle so
as you can see there is a potential here that I might be overwriting the data
when the FIFO is full. But then why did I not cache this bug? Was my ordering
check not good enough? Or my other checks it’s not good enough? Actually, as
it turns out we might be having a bug but we might be having a bug because and
we may not be able to see this because some constraints might be preventing you
from visualizing this. Actually, it does turn out at this point that I have
a hunch that there is a bug I don’t yet know this okay I I almost believe there
is a bug so the way to fix this is actually just look at the other places
where you might have reasoned about write acknowledge and actually given
this was a circularbuffer it was reasonable to have a side constraint and
the engineer was given a requirement saying if the FIFO was full then you
either don’t do a write or if you do in the very same clock cycle you must do a
read. So, the problem is when the fight
was full and you’re trying to do this extra write this constraint takes over
and allows the read to happen in the same clock cycle and when it does it
you’re not able to see the effect of this bug which we suspect wight now is
the bug we still don’t know. What we should do at this point is to take this
constraint away relax this and see what happens and the moment you take this
away the ordering check fails so you actually had a problem so it looks like
so our hunch in the right area one other check has failed so let’s debug
the ordering check. Pull up the wave and what happens here is that you have a
sequence of writes and the FIFO who goes full in this clock cycle you don’t
happen to have had any read up until this point the right pointer has wrapped
around and actually the new value that appeared in this clock cycle which is
one overwrites the value at index location zero and in this abstract model
of verifying this through the assertion I showed you the it uses non
deterministic values D1 and D2. It is quite obvious that actually this D1
was chosen to be 3 and D2 was chosen to be 1 and actually it was expecting to
read 3 but it ended up picking up 1 here. There is a problem let’s fix it ok so
at this point it is just useful to dance on your dashboard and notice the
coverage is dipped from 90% to 63% with 2 properties being shown to not have a
proof and close to 40% actually unobserved. Let’s go fix this and when
we do fix it we do get a dashboard like this which is something I was hoping to
see just after I had written my very first check because I thought I’d
written a great check. Let’s figure out what I did so I mirrored the logic for
write and read in exactly the same way sort of dual each other so coming out
of reset you know though if you’re not full you continue to write if you’re
full don’t fight it. This design now happens to
be checked any new data when it is full okay so now I’ve actually built the
capabilities in the design itself to reject the data when it’s full that may
or may not be the case you can actually check with your requirements with your
plan whether you wanted the device to actually have that behavior in this case
I believe the requirement is acceptable and the designer is happy for you to
have that. At this point, I realized that the constraint that I was carrying with
me was actually no longer required in fact that’s now property of the
design and actually I should have it on the interface that when I’m full I can’t
write it and when I’m empty I can’t read it. So, now what I’ve done is I’m actually gone in and added two more checks on
empty and full and I made sure that the device has that behavior then I go back
confirm it with the requirements and just make sure that this is what it was
required. Actually, these chappies here are no longer assumptions on the
interface and in fact the actual assumption I had written is no longer
even a requirement and in fact that fails for this design and the reason it
fails is because of the way the right acknowledge signal has been fixed in the
design of course if I design it differently to allow the write to happen
in the same clock cycle then the original constraint that could be now in
a circuit pass but at this point this is what the requirements are meant to be.
Actually, let’s take a step back and see what we’ve done so we started off by
having no test bench and everything was uncovered is then have one single
check we got about 60% of the design covered we then spotted missing checks
on empty and full because the coverage browsers told you so. We add checks run
the proofs they find a bug in the design we fix the design we run the proofs
again one Quantify we find more designs are still unobserved so we go
write more checks on the write and the read handshakes and at this point we
expect a design to be reasonably well quantified but it turns out it was still
in the region of 90%. Then we detected that there could be a problem with one
of the over constraints and if it then it was indeed
case and when we relaxed if we found a bug in the design. What happened here
is that all proofs are marked as proven there were several stages during your
development and verification cycle when you’ve had exhaustive proofs it was
not the case that you were had bounded proofs, you know. Properties were not
marked and reachable you had passing witnesses
you had checks on all design statements because I went and wrote these checks I
showed you and yet the coverage was not 100%. What happened is the
tool guided you, the tool is not an oracle it doesn’t tell you what check to write it guides you into an area of the design and forces you to think there is
a human element involved in this. It would be nice for deep learning to go to
a point that we can actually even unearth what would be useful to write
but at this point we can view hints and once you do this you’re able to unearth
the bugs and the over constraints. I just wanted to take this opportunity to
point out that this stuff works for other designs which are possibly more
complex than a FIFO and one of lead customers Infineon they have
an engineer Holger Busch who actually published a paper on using Quantify and
here is some of the data for that. But if you have actually worried about
safety given a lot of the safety work needs to go through compliance
and and requirements based verification the stuff has also been used by Holger
at Infineon and he’s kindly published his data where he shows actually how
coverage with Quantify would be used for safety. Let me actually just
briefly mention this before I wrap up. There are lots of different coverage
solutions in the market and I can see some people smiling and to be honest
they are all serving some purpose. The question is whether they are serving the
right purpose so the cone of influence coverage is a great technique to find
big gaps quickly but can lead to false optimism we have made other
presentations that we have short complete examples on this. We have the
proof core where the result depends on selected proof engine and if the more
abstraction you do the better the coverage model or sorry the worse the
coverage model is is more pessimistic this car engine is hard
not letting designers or verification engineers write assertions and when you
go to them and say for proof course you know I’ve got this bound and ran engine
this and engine that and this is cone of influence the managers don’t get it
right they don’t need more and more complex formal terminologies to get a
sense around sign-off then there is mutation so you know there are solutions
based on mutation which is a great technique the only problem is that some
of these solutions are implemented around mutating the RTL which forces
people to have too many iterative compile and runs and some of these
mutations can cause bad equity overall high runtime. Where we believe
Quantify brings here is the right level of abstraction where we merge the
structural and the functional coverage in one observation coverage model and
produced to you a report that is directly linked to the design browser
you show it the to a four year old and even he would make sense out of colors
never mind the experience managers who have to understand the complexity so if
we believe it addresses the problem of coverage in a decent way and I would
strongly encourage the verification engineers to consider doing coverage as
part of the design kind of flow going all the way to full-on verification.
That’s what I can wrap up. um and it’s still possible even with the
solution though isn’t it to have a hundred percent coverage and bugs in the
design it is still possible that yeah you could still have under person design
space coverage but the technique is actually offering you a way to make
sense out of your test bench and the coverage of the whole design but if you
haven’t implemented certain features of your requirements in the design in the
first place then there’s nothing to cover for this is where we said the
gap-free comes in because if there are if you have implemented everything in
those requirements of space into the design and you didn’t have checks then
this method will find it out for you and it will check which bits of it are
observed or data whatever but if you actually did not implement features
or from requirements point of view in the design in the first place there’s
nothing this method can do for that you need to use a gap free where we actually
just take the specifications themselves and run the whole analysis for
completeness that’s a separate talk I can talk to you about this if you like
okay you could you could cases a mr. Atif process that you shared on your
design with brief call for example yeah and to achieve the same result so I’m
struggling to see the possibly lighted so so not too long ago I was able to use
some of the tools because of my association the verification well I
didn’t see that but I guess the people who are building these solutions good I
mean I particularly I’ve looked at examples like this and run those tools
and I haven’t seen those problems up here and it is possible that the proof
score or the mutation or the cone of influence or all of them can find this
true but can they express it in the form that makes it easier for you to look at
and communicate with your managers and that’s the main aspect I mean it’s not
like the other solutions are bad right it’s just as I said whether they’re
quick and easy and whether they allow you to have it in meaningful format and
yes as I said you know this is not a validation it is not addressing a
validation problem it’s still a verification problem but it is true yeah
the proof core could potentially find it actually we do have an example where if
we do a proof core based analysis especially a cone of influence in
particular is very dodgy because if you end up writing an assertion which
actually says I can see the data being written in its read out but additionally
the fifo could be full or empty then the cone of influence because the full and
empty flags will cover the whole of the design the cone of influence would
actually say I you’ve got 95% coverage and your national property would be
saying I’ve just written one piece of data and just write this one out so
there are technical reasons why cone of insurance is not the best technique but
I could point you to a presentation where we have explained this in more
detail okay interesting Thanks questions online she should probably
worth asking please the examples are all from bounded for clues
what about bounded tools can we extract useful Kenyan influence and coverage
information from bounded position apply and the answer is yes there’s a switch
for use bounded reserves and you run this example with use bounded results
and you will get exactly the same story and second question is what about
merging the Quantify metrics with simulation coverage it’s been working on
that there’s axilla you see is discussing it yeah so that’s a good
question so we have been looking to merge the runs of one spring formal with
simulator results and we have been successful integration with mentors
questa and synopsis is VCS we have not looked at integrating
Quantify yet but it all depends on where is the need so right now we have one or
two customers who are actually using simulators and they’re using our formal
runs and they’re able to take the results of a session run so integrate
this back into their verification planners so the solution that we have
prepared is more on verification planning in tracking because we warned
the end customer to have the same view of simulation and formal in the same
verification plan that they have not having to have separate views and so on
and so forth so so we’ve just done this recently and we’re working with some
late customers to deploy this we’ve already done one deployment so far and
one final request to share the point is to visit presentations with CEO is not
the best solution so okay you have so we can do that so I think those
presentations have been done in the past we could provide yeah let’s do this the
other way let person get in touch with us and go

Leave a Reply

Your email address will not be published. Required fields are marked *