Verification Unification

Semiconductor Engineering brought together industry luminaries to initiate the discussion about the role that formal technologies will play with the recently released early adopter’s draft of Portable Stimulus and how it may help to bring the two execution technologies closer together. Participating in this roundtable are Joe Hupcey, verification product technologist for Mentor, a Siemens Business; Tom Fitzpatrick, verification evangelist for Mentor and vice chair of the Portable Stimulus Working Group (PSWG); , chief executive officer of Breker; Roger Sabbagh, vice president of applications engineering at Oski Technology; Sean Safarpour , director of CAE for VC formal at Synopsys; Tom Anderson, who was product manager at Cadence at the time and secretary of the Portable Stimulus working group; and Ashish Darbari, director of product management for OneSpin Solutions. Part one can be found here, and part two here. What follows are excerpts from that conversation.

SE: The conversation so far has been about functionality. There are additional things to worry about these days. What about power ?

Fitzpatrick: There are two aspects to power. One is the power controller and we have shown part of how you deal with that in the DVCon tutorial. It just becomes another set of actions that are specified in the design. It is just another aspect of stimulus to get the design into a certain power state. There is also the question of modeling the power control in the first place using UPF. That becomes more of how does the simulator model that. There is some additional mapping that has to happen between putting the design in this power state and how that is actually accomplished.

Darbari: You haven’t factored the power side into PS?

Fitzpatrick: Right, we haven’t factored it as something separate. We claim it is just another aspect of stimulus.

Darbari: How would a UPF spec fit into this? How do we know the two are aligned?

Fitzpatrick: UPF allows you to define the different power islands. I would not call it an intent specification, but a design specification. It becomes part of the design from the test intent side of things and we need to make sure that I can turn the power on and off and that if I try and do this action, then this power island had better be on otherwise I can’t do it. I don’t see that PS needs to know about anything specific in the UPF other than the power controller algorithms that have to be exercised.

Darbari: So could we do without UPF? If I am trying to check that it all works at the system level using portable stimulus, then can I use it without the UPF?

Sabbagh: You want to use it in the context of the UPF because you want the notion of the power structures in the model.

Hupcey: It is alternative information.

Sabbagh: You are going to model that this thing in turned off, and these isolation cells are in there, and this block cannot talk to this one.

Darbari: Should it be done independent of PS or tied into it?

Anderson: There is a lot of stuff that you can do with formal verification in terms of analyzing low-power structures and the control, but the notion is that you want to take the set of tests from PS and overlay what happens when you start messing with the power domains. If you turn things on and off, do things stop working? We tend to find that the people who care about this are the architects and they have a very high-level view of it rather than what is in UPF.

SE: What about safety and security?

Safarpour: Security is one area that is very applicable. Customers are interested in formal for security because of the completeness of formal. They want to check their security architectural level protocols. We are not in RTL at this point. The best formal tool cannot handle this at RTL, so we are validating the architectural-level security protocols on some high-level model. The architect can define that using PS in terms of what is it that he intends the right model to do, what are the trusted members, how are they allowed to access the secure part of the memory, what is not allowed etc. Formal can validate that model. We are using a proprietary input format to do this today, but it is the same thing.

Darbari: Does this require a synthesizable design?

Safarpour: We do some modeling.

Fitzpatrick: Some kind of high-level RTL model.

Sabbagh: You abstract away anything that does not have to do with this feature, so you build in this contract with each of the architectural elements, blocks or components and you say I will assume that this block will do this and you model that with RTL code and assumes and assumptions.

Hupcey: When you do an analysis of a secure store or path analysis, this sounds like another case where formal does the analysis and feeds back to PS. So is this only way to engage the thrust reverser, the only path or the interlock to the brakes or a storage element that has only one or two ways to read it? That is all formal, and a case where it is characterized and can export some or stimulus to include in a bigger picture, that would be driven by PS. As much as one technology can conclusively verify something, customers do like some overlap and redundancy —especially at the system level. So it is formally proven at the RT level, but we would like to re-use that learning at the system level, where we can do bigger transactions.

Safarpour: That is probably even more important because formal is only applying to the model, not the RTL, so when it goes to the emulator, now you can really use the stimulus to drive it.

Sabbagh: We can close the loop with formal on the RTL as well because those contracts between the blocks that you assume about the blocks can be turned into asserts and then when you get the RTL you can prove that the RTL conforms to that contract. So all of my blocks match the architectural models and I proved the system-level property on the architectural models, so hopefully you get fairly high level of confidence.

Hamid: Now we just need to generate those security properties from PS on top of the abstract RTL model so we can…

Hupcey: We are traversing the entire V diagram.

SE: Do we need to define the paths in the graph that are illegal? Then formal could try and find counter examples.

Darbari: Safety is the classic example. Fault simulation is done extensively on hardware designs, and then formal comes along and provides assessment of propagation analysis. So you could do injection and safety analysis, but today it is done at a hardware level rather than a system level. I am sure people working in software would be doing the same, but there is no system view of safety yet. Now is perhaps a good time to capture those kinds of issues. It is all about requirements and we need to be able to capture them in an abstract form so that we can derive the interesting testcases for hardware and software. Not everyone will go and do system level. The hardware team would like to do the analysis on the hardware, and ISO 26262 has a specific mandate for this. People do have to prove they are compliant. So there is work needed here. How does one capture this at the PS layer? It is an interesting question.

Hupcey: Formal has the benefit of having both illegal and legal together, and two sides of the coin are proven. I am curious what best practice may be in the PS world? Do you create graphs for the known illegal cases to make sure the design rejects them like it should?

Hamid: Absolutely. You have your good cases, you have the error cases and you have the don’t do this cases.

Anderson: There are aspects of safety and security that people do model today. Which processors can access which memory regions or which IOs are accessible from which processors. There are certain things that are in the PS models today. We need to understand that to generate tests. That may be under the control of a programmable register somewhere. I would not claim that we have tackled the whole problem yet.

SE: What other connections point exist between formal and PS?

Hupcey: is the big one and customers are using that every day.

Fitzpatrick: I have covered this because I have proven it.

Hupcey: Right, and I haven’t covered this and why not – because of the configuration. This is what people adopting the technology will go for first.

Darbari: Completeness is a very interesting aspect of PS. If you can pre-validate all of the noisy inconsistencies in the specification, it makes a lot of sense. That is the hardest part of any verification and validation activity. No matter if you use UVM or formal, nobody knows how complete you are. Then you may have an inconsistent set of checkers or constraints, never mind the actual modeling and if in PS you have a way to capture the requirements which can be analyzed for inconsistencies, then that is a great feature which doesn’t exist anywhere else.

Fitzpatrick: The way we envision it is that there are requirements for any given operation, such as resources. You have this whole pile of things and the graph says I want to do this and then that. The tool figures out all of the other stuff that is required to go from A to B. It could be that there are thousands of ways to do that. You can generate a test for each of them and run them all or if you could do some analysis on the graph, or based on some external analysis…

Darbari: Or find inconsistencies in the spec. That is the biggest attraction.

Sabbagh: Kind of like formal lint of the spec. So if you have your constraints and your coverage is unreachable based on those constraints, formal can find the inconsistencies or given the graph, you may have some deadlock conditions.

Fitzpatrick: We have defined the semantics well enough that you can figure out if you want to do A followed by B, then what other stuff has to exist in the middle to make that happen. In doing that, there are other things that may be constrained such that it prevents it from being one of those paths – that may be a good thing or not. If you write an explicit scenario, we can say no – that is not possible because these two things cannot talk to each other for this reason.

Darbari: If you have concurrent threads running and there is a sequential dependency that could produce a cycle…

Fitzpatrick: Yes, it becomes more complicated, but the other thing about PS is the ability to say I have this pile of stuff that you can pick from. Formal can analyze that pile of stuff to figure out which ones actually exist….

Darbari: So you are talking about consistency and completeness. If you don’t have consistency then you have to be worried.

Fitzpatrick: Today, the tool could identify the one that would never be used because it has been written wrong – that is fairly easy to find.

Darbari: Livelock would be another interesting thing to check for.

Fitzpatrick: So the question becomes, how much of the kinds of things that we currently do on an RTL model can we do on a PS model and in what form.

Anderson: It is funny – we started off on the path of what can PS do for formal. If you have a PS model, how can formal leverage that? We have shifted to looking at it the other way around which is how can PS leverage things that formal can provide.

SE: Is nirvana being able to do equivalence checking between the design and the requirements as captured in a PS model?

Darbari: You will not always have full equivalence because one could be a refinement of the other.

Hamid: You want to prove that the design is an implementation of the requirements as defined by PS.

Fitzpatrick: I am not going to hold by breath waiting for someone to come out with that.

SE: So, as a result of this discussion, will nay formal people start being involved with PS?

Anderson: While many extension areas have been talked about for PS, formal has never been brought up before and it should be.

Fitzpatrick: Agreed. We have our Enterprise verification platform slide that shows four engines: simulation, emulation and formal, and I know Cadence has the same picture. So it would be nice if we could say that PS is the layer that goes to all of them.

Safarpour: This discussion is really good but after we are done with this, we go back to the day to day and the customer has a block and they are working with these constraints and they are asking how to get their proofs, so we need baby steps – what is it in the short term that would provide enough benefit if we liked formal and PS?

SE: Now is the time to do that. A small change to accommodate formal could have a significant impact and enable a lot of other things down the road.

Fitzpatrick: The first step may be to take a PS, perhaps from the tutorial and turn it into a set of assertions and see if that makes sense. The question of applying formal to the PS model is more of a tool issue. Each vendor will have their own way of doing it. That is not part of the standard.