The electronic design community has been slow to embrace a cloud computing strategy for its design projects, mostly due to concerns about IP security. An emerging approach could change that reluctance and allow more designers to leverage the cloud as a compute platform for verification. This approach has particular benefits for embedded designs making use of embedded processor subsystems and other IP from various sources.

Formal verification technologies, which are becoming the basis for more and more verification solutions, also hold the key to mitigate cloud security concerns. Design security can be assured by the technology’s ability to break a verification problem down into multiple, abstract mathematical problems, and transfer them to the cloud to be solved (Figure 1), with all design detail removed. The formal verification process accomplishes this by extracting specific states to be analyzed and comparing with required properties. The design detail is retained and reapplied locally to the results of the cloud operation. This process eliminates the need to transfer IP out of the office.

The resulting solution harnesses a collection of cloud-based servers to provide a broad range of verification capabilities, offering easy adoption and usage, on-demand performance trade-offs, and a pay-per-use business model. This is particularly relevant for IP-based embedded designs where the IP is utilized by a third party who may not have ownership of the formal technology.

Acquiring verification software through the cloud

Cloud computing verification software makes use of a “Client Tool” – that is, a component that operates on a local host computer and acts as a front end for the cloud engines, creating the mathematical proof problem sets from the design code for transmission to the cloud. The client tool includes a “linting” capability – a way to find design errors in Hardware Description Language (HDL) code – and manages communication with the cloud solution. It also allows any required debug of the results of the cloud processing to be performed back on the local host computer.

Traditionally, verification software is licensed to run on a local host computer and the entire operation from design input to results debug is accomplished using the single product. For the cloud scenario the client tool makes the user experience identical, as if the complete product was running locally, providing a transparent feel to the cloud use model.

Practical applications

The combination of a transformational, pay-per-use business model, access to a limitless number of compute engines, and on-demand verification applications provides some interesting new benefits.

For example, this software is ideal for new users who want to add powerful formal design checks to their existing simulation-based verification flow with a minimal learning curve and setup process.

In the most basic cloud verification process, the design Register Transfer Level (RTL) code is checked locally by the included lint capability. Then, assertion synthesis is used to automatically create powerful tests for many facets of the design. The automated tests include a range of fatal design error checks, potential mismatch issues between simulation and synthesis, register and signaling initialization and toggling problems, code and Finite State Machine (FSM) coverage, and many other fault scenarios. By providing this mechanism in the cloud, new users can take a “try and see” attitude without a time-consuming evaluation process, quickly testing their design with no painful learning curve, and getting a taste of formal technology, unlike the more traditional approach where a full tool licensing and installation process must be accomplished, usually by a vendor’s engineer visiting onsite, often coupled with a sales effort by the vendor.

Advanced users can also receive considerable benefit. Formal verification is inherently a concurrent process with the mathematical proof problems being run in parallel. The cloud solution provides a limitless number of compute servers and, as such, a verification run may be executed across the number of machines to provide optimal parallel execution. Even the cost remains static – 10 hours on a single server would cost the same as one hour on 10 servers. In the software licensing approach, enough licenses would have had to be purchased up-front to cover the full parallel usage, placing a usually small cap on the number of operations that may be run together. Parallel operation is often severally limited in most verification installations due to this.

The solution also enables on-demand usage for specific purposes, such IP integration or a means for verification service providers who need to have access to the tools while working in a foreign environment. In each case, the software can be leveraged without the need to purchase it up front by the end-customer, ideal when a third party is involved who does not leverage formal solutions.

Cloud advantages for embedded designs

Embedded designs have some specific issues that can be mitigated through cloud application-based verification. The nature of embedded designs is that IP will be leveraged from a variety of sources. This IP will have a range of verification metrics applied to it, and may use complex interfaces for interconnection purposes (Figure 2).

Formal verification can be used to great effect in this scenario, as discussed by a leading semiconductor company at the recent Design Automation Conference, to provide a rigorous integration test environment. Assertions are used to specify interfaces and the expected information to be passed between the IP and platform. This investment in assertions is considered worthwhile given the reusable nature of the IP and the importance of ensuring that it is interconnected correctly in a foreign environment. Of course, if this interconnect is through a standard bus protocol – the AHB standard from ARM, for example – then a standard set of protocol assertions may be used to ensure its validity. The use of assertions in this manner has been proven to increase quality and reduce integration time, as, given the reusable nature of the IP, more investment may be applied to ensuing is it fully tested, and the need to rewrite the assertions will have been eliminated.

What has this got to do with the cloud? The IP producer might utilize assertions in a formal environment to test IP interfaces, for example, to ensure that the communication protocol applied by the IP consumer is as specified. However, this does not mean that the IP consumer has access to formal technology. In this case, it is unlikely that the consumer will want to purchase tools and endure a lengthy evaluation process. The cloud allows IP integration analysis to be leveraged without the expense and overhead of unnecessary tool ownership by the IP consumer, saving as much as 95 percent of the cost, simply by accessing the cloud solution for those IP checks on a pay-per-use basis.

Of course, the same is true if other formal static checks suitable for embedded design are used. For example, protocol analysis, register checking, and other System-on-Chip (SoC) style analysis are available in the cloud and might require a small number of applications in the design process. This is ideal for the embedded design team who might want to quickly create a hardware platform to utilize either an emulator or virtual models, and check that it is correctly implemented without employing a complex verification process, so they can get on with software design.

Verification within budget

One of the most significant benefits of the cloud solution is the business model and its implications on tool budgeting and embedded designer control. Traditional Electronic Design Automation (EDA) tool licensing, for example, normally requires an upfront investment, either a time-based or perpetual license. This requires the purchaser to have a good understanding of tool resource requirements, particularly difficult to estimate with any verification solution as the use model will depend on coding quality, complexity, and other hard-to-predict factors. This is generally true regardless of application area, and becomes more complex with potential project size and team structure.

In most verification scenarios, there is a bulge of tool usage that gets larger as more code is completed and checked into the design database. As RTL coding nears completion, the demand on formal verification software will be extensive, sometimes by as much as four to five times average for complex designs such as communications and multimedia platforms, and drop off as the design is synthesized and silicon laid out. The extent of this verification bulge is partially dependent upon code quality, coverage achieved, and other metrics. As such, a certain predictable proportion of the licenses will be used throughout the entire design flow. A somewhat unpredictable number of licenses will be applied during the bulge period.

The cloud computing solution enables a combined business model where some licenses may be purchased up front and others applied on-demand using a pay-per-use scheme. The design team is in control of its resource requirements, leveraging exactly what it needs for the variable components of the verification process and eliminating redundant licenses. This model also allows for greater financial control, shifting some of the tool expense burden from capital budgets to more appropriate operational or project money sources.

Dr. Raik Brinkmann is President, Chief Executive Officer, and Co-founder of OneSpin Solutions. He brings to the CEO role more than 15 years of broad expertise in management, verification and industrial R&D, having served at companies in both Europe and the U.S. Dr. Brinkmann holds a Diplom Informatiker from the Clausthal Technical University, Germany and a Dr.-Ing. from the Department of Electrical Engineering at the University of Kaiserslautern, Germany.

OneSpin Solutions www.onespin-solutions.com

Follow: Twitter Facebook LinkedIn