Page 34

EETE JAN 2016

degisn & prdoucts Circuit analyiss & bdeug tion engineer applies some assertions on the design outputs, which are essentially statements about functional behavior that should hold true. Then the formal engines busily try to find examples where the assertion does not hold true. For each case the tool finds, a short signal trace is created showing the combination of events that would disprove the property. This trace is called a counterexample (CEX). Each CEX the tool finds is a possible bug. The latest formal tools have engines that are dedicated to penetrating the design state space, widely and deeply, seeking out these CEXs, thus removing bugs from designs, without even the intention of completing the formal proof! Ultrasoc cores provide ‘bare-metal’ security Ultrasoc Technologies Ltd is moving into active functionality by providing support for “bare-metal” security. “Debug is a valuable thing but we realized you can do a lot of other things with the analytical cores we provide,” Rupert Baines, the company’s CEO, told EE Times Europe. “For example our on-chip debug support is dynamically aware of what cores are in use and what cores are not.” While the activities that Ultrasoc could support on-chip are diverse including dynamic voltage and frequency scaling (DVFS) to achieve power savings the first chosen activity is security. The Internet of Things and the connected car in automotive are expected to be the initial applications for the technology. The Ultrasoc support hardware is able to monitor accesses to different regions of memory and raise flags if a process enters a forbidden region, it can monitor software behavior patterns and code sequences. Most security is provided above the level of the operating system, said Baines, but this is complementary “bare-metal security” that is non-intrusive and remains robust even if conventional security measures are compromised, he added. This functionality is provided by the same set of gates that have established benefits for developing an SoC and includes that benefit of supporting multiprocessor In other cases, when all CEXs have been removed, it’s important to be able to answer the question, “Is the design fully verified?” If the requisite number of formal proofs have completed, the answer is “yes.” In order to reach this conclusion, the coverage achieved by the set of assertions needs to be analyzed. Again, leading formal tools have this capability. If sufficient assertions have completed, then the verification is absolute, but achieving this happy state on designs of today’s complexity can be highly challenging. To address this issue, some formal tools can analyze coverage attained from assertions whose proofs did not complete. These assertions may have been shown to hold true for a certain cycle depth. We call these bounded proofs, and with the right analysis, these can be of great value and effectively extend the value of formal’s absolute proof nature to a wider and larger class of designs. Summary The big advantage of formal apps is that they do not require deep formal verification expertise. Anyone who can run simulation can use apps to find problems in specific areas that would otherwise require a lot of vectors. Additionally, given just a simple set of assertions about the design’s functional behavior, it’s easy for any verification engineer to go bug hunting. Of course, expert users can take advantage of the full power of the engines, which have improved immeasurably over the last few years. Even when proofs don’t complete, we know definitively what has and has not been verified, using bounded proof analysis. But the big change is in usability. People who are not formal verification experts can accomplish a lot that is easy to do formally and hard to do with simulation. And once you have proved something formally, there is no need to ever prove it again with some other approach. Formal will continue to be mission critical in 2016. and heterogeneous systems. “It’s another use case for the same gates, although there will be an incremental license fee and royalty for using the bare-metal security features,” Baines added. Ultrasoc’s debug support comes as a tool box with up to about 30 different debug functions supported by a number of cores. The typical overhead in terms of gates as a proportion of the total varies between 1 or 2 percent and 7 percent. By adding the security use case it means the Ultrasoc debug support is functionally active after IC deployment as well as in the design phase pre- and post-silicon implementation. Although it functions below and outside of the operating system, the technology also provides a means of communicating with software on the device as part of a holistic security system, if this is necessary. Bare-Metal Security features also provide visibility of the whole system, making it extremely difficult to camouflage or hide an attack. Although originally developed for debug and silicon validation, UltraSoCs IP also enables a broad range of value-added functionality in-service, of which security is just one example. Other applications include in-field monitoring, performance optimization, reducing power utilization and SLA enforcement. UltraSoC’s announcement coincides with the inaugural conference of the IoT Security Foundation in London whose aims is to maximize the benefits of the IoT by promoting knowledge and best practice in excellent, appropriate security to those who specify, make and use IoT products and systems. Ultrasoc Technologies Ltd. www.ultrasoc.com 34 Electronic Engineering Times Europe January 2016 www.electronics-eetimes.com


EETE JAN 2016
To see the actual publication please follow the link above