Formal Confusion

Formal verification has come a long way in the past five years. Tool developers changed direction and started to create self-contained apps which have led to a rapid proliferation of the technology. But formal is a diverse set of tools that can solve a variety of problems in the verification space and this has created a different kind of confusion within the industry. To find out how the industry is coping with the rapid proliferation of these technologies, it can be more interesting to listen to the users themselves rather than the tool vendors.

Semiconductor Engineering sat down to discuss the right and wrong ways to apply formal verification technology with Normando Montecillo, associate technical director at Broadcom; Ashish Darbari, principal engineer at Imagination Technologies; Roger Sabbagh, principal engineer at Huawei; and Stuart Hoad, lead engineer at PMC Sierra/Microsemi. What follows are excerpts of a conversation that took place during Decoding Formal, an event organized by Oski Technology and sponsored by Synopsys.

SE: What are the best kinds of blocks or kinds of designs for the application of technologies?

Montecillo: The control blocks are really good—blocks that would not be described as transport. But beyond those, we are seeing blocks that have intertwined control and transformation, and we are starting to push the boundaries of formal into some of these areas and seeing success. It is a question about time, and given enough time I believe that transformation blocks could also be achieved.

Hoad: We are working hard to include blocks that contain bugs that may be difficult to find using traditional simulation techniques in our formal plan.

Sabbagh: I don’t see it as black and white, where some blocks are totally unsuitable for formal. There is a spectrum. You may have a block that has some gnarly mathematical thing and define it to be unsuitable for formal. But on the interface you may have complex flow control, and that is good place to start with formal. If you look at the block and list its functions, some of them may be difficult for traditional verification methods and a good fit for formal. So you have to look at this on a case-by-case basis.

Darbari: Designs that have a lot of sequential history and arbitration types of problems tend to have the most nightmare bugs in them but can also be quite easy to verify if you get it right. We should also address another issue: what do you mean by formal? The implication is that it means model checking, but that is only a part of the story. Formal also includes sequential equivalence checking and theorem proving as well. So while mathematical blocks may be difficult, some companies have been successful with data dominated arithmetic circuits and we do have tools that can cope with these. So rather than say what I would verify, I would put it as what blocks wouldn’t you verify with formal.

SE: Is this a verification planning issue?

Darbari: Before we even get to the plan, I would ask what is or is not possible. Then we can try a combination of strategies. Formal alone will not solve all of the problems but can complement simulation and . Verification is made to look very hard and formal in particular, but verification is problem solving. It is a mindset and a cultural issue.

Hoad: Planning is key. We could say that formal is going to be applied to everything, but we try and figure out where we will get the most value. Formal is a limited resource and we don’t have unlimited tools and we don’t have unlimited people who can run them. So we plan where we will get the most value. It may be low-end issues that are easy and quick or areas that we know are going to be difficult to simulate.

Normando: Schedule is important. Resources are limited, and in order to meet the schedule we need to put the best methodologies in place. We have found that formal fits in the front end where we can do initial bug hunting and get the design very clean. It is not about replacing what simulation does. It is about complementing it.

SE: That is a change. Formal used to be performed when simulation had been exhausted.

Darbari: People have been asking, ‘Where do we start?’ Start by removing the issue of complexity and look to see if it is a new design or if it has lots of new features. Do we have existing testbenches? Is this a legacy design that has had problems in the past? This is one way to choose the methodologies to use.

Hoad: There are a lot of factors, such as the maturity of the design team and the design, the verification team and the process. As the formal guy, I do not have the luxury of selecting the blocks. It normally starts with the previous design where there were problems closing coverage or we found some really nasty bugs. Then we can evaluate that block and decide which features are amenable to formal and where can we add value.

Montecillo: If I can find a bug on the front-end, why would you want to defer that to the back-end? Finding bugs as early as you can reduces the cost of the bug. If I could find them as soon as the RTL is finished, that would provide a cost saving. Because of this, I would also put formal in the front, even if it is finding very simple bugs.

Sabbagh: We can put it sooner than that. We can start using it to help the design.

Montecillo: Seeing the interaction between the designers and the verification guys can enlighten them.

Sabbagh: What if I don’t know what resources I am going to need. Is it design-feasible? We can prove architectural concepts as well.

SE: Who should do the formal work? The designers, the verification team, or should they be a separate specialist team? And where do you find those people?

Sabbagh: For automated things such as connectivity checking or structural coverage closure, these can be widely used by anyone in the design team. The simulation guys can do this. White box verification can be done by the designers by adding their own assertions, and maybe verification engineers adding assertions at the interfaces. But if you want to prove that it cannot deadlock or that there are no hazards in a pipeline, then you need someone who is a formal specialist — someone who works with formal on a day-to-day basis and has built up the expertise so they know how to decompose a problem to make it digestible by formal. How can I use abstractions? How can I use non-determinism? You have to have experience to use these, and that requires an investment in a formal team.

Hoad: You don’t necessarily want to isolate the design and verification team entirely from the formal work so that they can understand where best to apply it.

Sabbagh: Both teams need to be involved in the planning stage, but it requires someone coming at it from an orthogonal view. If you are not doing formal full time, it’s hard to build up the expertise.

Montecillo: I have been trying to push the designer to do more formal, and by formal I mean model checking as soon as they finish their design. I failed miserably. A lot of them refuse to do it because they don’t have the time to learn a new technology. Designers are over-burdened. The guys who have tried it have not done very well. There are times when they have exceeded my expectations, but those cases are rare. We have found that it is best to have a dedicated formal team that can set up the environment, write the , work and iterate the assertions and checkers with the designers. This model seems to be the most efficient way to get the schedule compressed. The designer is not the best for doing the formal verification.

Darbari: Designers should produce more standardized code starting with Lint, but I would rather have the independence of the verification engineer who can review the specification. We sometimes also try to have a third person do the review who has no prior knowledge of the design or the verification, and that has often highlighted some key issues. I would not just stop at the designers and verification team, but also add that architects could benefit from using it for modeling, such as performance modeling. On the questions of resources, people are not going to come from Mars. We have to train people and create the resource pipeline.

SE: What is the ideal background for someone coming into the field?

Darbari: I just look for a very clear head—problem solving skills.

Sabbagh: I don’t think we can realistically say that everyone can do it. You have to look at the way that they think and the ways they attempt to solve problems. Some people just don’t think in the right way.

Darbari: Experience and domain knowledge are equally important.

Sabbagh: Someone who is a pure verification person and has no design experience can be a problem. Knowing how RTL design works can help. Being able to code RTL efficiently or hardware design to minimize timing and area is the same kind of skill you need to code a formal testbench. You have to make it as simple as you can. This is often the same type of skills. Also the formal verifier sometimes has to do some white box testing and be able to look into the design and understand what is happening when there are internal structures that you are trying to verify. It is good if you have the design experience to know what you are looking at and the types of corner cases that you should be checking for.

In part two, the panelists tackle issues associated with completion, coverage and education.

Related Stories
Verification Facing Unique Inflection Point
Joining the dots between DVCon’s keynote by Wally Rhines, a conversation with Accellera’s Shishpal Rawat and a Cadence lunch panel.
A Formal Transformation
Exclusive: What happens when you put formal leaders from all over the world in the same room and give them an hour to discuss deployment?
System Level Verification Tackles New Role
Experts at the table, part one: The role of system-level verification is not the same as block-level verification and requires different ways to think about the problem.
Do Single-Vendor Flows Make Sense Yet?
Design tool providers may want to lock customers into a complete tool flow, but is that best for users or the industry?