close
By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.
The value of multiple verification engines, and what’s driving demand for verification in the cloud.
[...]
Kelf: "You can process large amounts of data in a formal engine more easily than you can move the design. Then you can analyze cache coherency with a specific capability that allows you to state the properties or specifics with regard to the Portable Stimulus tool. So it becomes much more straightforward. It’s analyzing that data, and having a platform to do that, which is the next frontier in verification. It’s not the performance of the engines. That’s not an issue. You have to have performance, of course. But it’s how you handle the data in the cloud or locally."
Part One: How close were the predictions for 2017? Most were fairly close but some big outliers and some things that were missed.
[...]
One area that had been suffering was automotive, which had seen some high profile security lapses. That suggested to David Kelf, vice president of marketing for OneSpin Solutions, that automotive designs would need to be built to be as secure as possible and that tools to help predict vulnerabilities would become more important. “While I haven’t observed any big stories this year on vehicles being sent off the road due to malicious action, it is clear the concern is still there,” says Kelf. “At various workshops and other events, the subject of automotive security and security in other applications comes up often. The ISO 26262 committee continues to discuss how this should be included in the regulations, and for sure we will see new directives on this. Security is also an area of interest in the design and verification solutions space. Other security initiatives will become apparent in 2018 also in various applications.”
OneSpin returns with another holiday puzzle, this year challenging people to use formal tools to solve what may be the world's hardest Sudoku grid. The deadline is Jan. 7th.
It’s no secret that the OneSpin team loves contests. Last year around this time, we set a challenge to engineers everywhere: solve the famous Einstein’s Riddle using a formal tool.
After an enthusiastic response, we decided to make the holiday puzzle an annual event, with a different subject area each year. Our engineering team was challenged to come up with a new topic, and my idea, which centers on what has been called the “World’s Hardest Sudoku,” was chosen for this year’s puzzle. You can learn more about the contest here. Read on to find out how I came up with the challenge.
Making sure a device can interface with a variety of protocols is becoming a major headache.
[...]
Considering this from the perspective of the SoC interconnect fabric, having multiple interface protocols, as it is often the case, creates asymmetries that complicate the verification significantly, observed Sergio Marchese, technical marketing manager at OneSpin Solutions. “Even ultra-rigorous verification of protocol checks is easy, at least for standard interfaces like AMBA, where one can leverage assertion-based VIP optimized for formal tools. Ensuring that the right data gets to the right place at the right time is generally difficult.”
With multiple protocols at play, the number of corner-case scenarios increases exponentially. Even for a supposedly simple AXI-to-AXI bridge, where the two sides operate on different data widths and transactions are split or aggregated, there are a lot of scenarios to consider. Add to that different clock domains, and it’s likely that simulation will miss some bugs, he said.
“Another crucial verification goal is to ensure that each interface always will make forward progress. This is an area where only formal verification, with appropriate methodology, can deliver 100% coverage and prove that the systems will not deadlock,” Marchese said.
At the next level of chip I/O interfaces, another type of verification challenge may come from architectures that support multiple standards and are optimized by sharing circuitry at the physical level and above, he explained. “The shared logic and additional hardware functions that accommodate the differences between different protocols create many more corner cases that have dedicated circuitry for each protocol. In this case, exhaustive formal analysis can reveal bugs in scenarios that one would not think of just by looking at the high-level specifications.”
It’s becoming harder for tools and methodologies to keep up with increasing design complexity. How to prevent your design from being compromised.
[...]
Raik Brinkmann, president and CEO of OneSpin Solutions is in full agreement. “Formal already provides a major contribution to the shift left paradigm. Here, the verification intent ranges from implementation issues (implied intent) to thorough block-level functional coverage (specification intent). Portable Stimulus will also address the coverage issue from a systems perspective where it becomes increasingly harder to capture design and verification intent in a machine-readable and humanly comprehensible way. It remains to be seen how the intent gap between formal at the block level and portable stimulus at the system level will be covered.”
People are looking at other areas in which machine learning may provide value. “Electronic system design, verification and project management data could be leveraged to improve the overall workflow efficiency or manage project risks,” points out Raik Brinkmann, president and CEO of OneSpin Solutions. “This would require the collection and consolidation of data along the design process across multiple tools. On a smaller scale, the effectiveness of individual methods could be further improved by combining advanced data analytics with new verification workflows, such as formal verification methods. In particular, gathering performance data during runtime over several episodes allows building predictive models for fine-tuning heuristics or projecting tool runtimes and verification results. Although the underlying predictive models will be specific to the task at hand, they share the requirement for good training data during their construction.”
I know this is good for verification. Every one of those trial-and-error runs means you have to verify it. When we talk about a move to abstraction, this is a huge move and makes verification more efficient and effective. You can break the verification problem into a high-level functional job and equivalency checking. Equivalence checking means checking consistency between the high-level model and RTL, which is hard.
