French design automation startup Valiosys has moved into beta testing on a tool that is intended to make the model-checking form of formal verification more accessible to chip designers.
Giang Nguyen, vice president of sales and marketing for Valiosys, acknowledged the company is moving into a difficult part of the design market, which has seen a high proportion of business failures but said Valiosys is trying to turn model checking into a complementary form of verification to simulation.
Model checking is a static form of verification that uses mathematical proofs to determine whether an input design matches a formal specification. The difficulty of training engineers to understand and generate the formal specification has made it difficult for model checkers to achieve wide adoption.
Valiosys has chosen to concentrate on simplifying the specification to a set of properties that a design needs to satisfy to pass.
She said the tool, which is based on the linear programming validation (LPV) technology developed at the University of Caen, Normandy by Valiosys founder Dr Jean-Luc Lambert, does not suffer from the capacity problems experienced by existing model checking tools.
"The only model checker out there is the one from Cadence. It is based on binary decision diagrams. The problem with that is that as soon as the model gets complex, the state space gets very crowded.
"Our technology doesn't look at the state space. It is a constraint solver."
The core LPV algorithm uses the idea of a logic cone to determine which inputs are needed to generate a specified output condition. The tool builds up a set of logic equations that represent the result of tracing back through the logic tree. By attempting to solve those equations the tool determines whether a condition is possible or not.
"Questions can be asked in a positive or negative way," said Nguyen.
She said this attribute of the tool could be used to work with simulation by making it easier to home in on the causes of an error caught during simulation.
"If you see an error in simulation, it is tough to go back and trace the root cause. Using a tool such as Improve, you can define the erroneous outputs as properties. You get what is guaranteed to be the shortest sequence leading to the root cause of the situation," said Nguyen.
She said the tool could also be used as a more robust form of equivalence checking, a formal verification technique that has achieved greater levels of acceptance. By using model checking techniques, she said the tool is better able to deal with retimed designs, something that equivalence checkers find difficult because the extra latches confuse them.
The properties that are used to check designs are entered using a set of assertions that may reflect constraints, output vectors or as properties that must always be true.
"We've realised the barrier to getting the tool accepted is that [model checking] is an unfamiliar area to most people," said Nguyen.
"The properties that Improve uses can take up three pages in Verilog. We think it is a good compromise."
So far, the company has focused on control-oriented blocks such as bus controllers rather than datapath designs.
"We're not any better than the competition in that area. But we are looking at a benchmark for a graphics processor," said Nguyen.
"The pixel data space can span many millions of cycles. We don't have an answer for that. If we have a way out, it will be a methodology way out."
She said the most favourable approach would be to prove the operation of component parts of the design and then prove those parts together.
"We really like the recursive approach," she said.