BANGALORE, India Five Indian researchers from the have proposed a new approach to formal property verification.
The researchers from the Indian Institute of Technology (IIT), Kharagpur recently presented a formal and intuitive way of writing an unambiguous test plan amenable to formal analysis. The presentation also encompassed the notion of test plan coverage by properties and a formal method to identify which part of the test plan is being covered by the formal properties.
“We believe that our methodology will help to significantly reduce the simulation overhead through test plan reduction, thus shortening the design validation time which is till now the main bottleneck for reducing the time-to- market of a complex digital chip,” the researchers said.
The electronics research community is making a determined attempt to double the size of what is considered a single system every few years. This has spawned major challenges for the developers of tools for electronic system design, primarily in terms of verification.
Traditional approaches to formal verification attempt to validate a given RTL implementation against a formal specification using techniques such as model checking. But pure formal methods in verification are still not accepted in design flow.
Micro-architects write the test plan of the design, a structured way to check that a design satisfies the list of properties at different points of time and so conforms to the protocol when different input sequences are driven to it. There is no formal way to write the plan in an unambiguous manner and so it is difficult for designers to find out which part of the test plan is covered by the formal property verification (FPV) effort.
The IIT researchers propose test plan coverage by FPV. The researchers propose a syntactic structure for a test plan, calling it the Test Plan Description Language (TDPL). A key component of the language is the use of simply syntax, using notations that do not appear alien to a designer.
“In FPV, designers write formal properties for the correctness of the RTL design and model check those on the implementation," according to a paper authored by the researchers. "But due to lack of any adequate behavioral coverage metrics in FPV, designers are not sure whether all the scenario mentioned in the test plan have been covered in FPV. Hence, they again perform simulation over the test plan scenarios to increase the degree of confidence.”
The researchers said their paper presents preliminary ideas about structuring a test plan and showing how parts of it can be covered using FPV. The researchers suggest the syntax for writing the test plan can be improved by working with design architects so as to better suit their designer’s needs. A detailed case study on the ARM AMBA APB protocol has shown good results, they said.