Formal verification enables Agile RTL development

By Sergio Marchese |  No Comments  |  Posted: January 13, 2014
Topics/Categories: EDA - Verification  |  Tags: , ,  | Organizations:

Agile development started in the software domain but the methodology shows promise for SoC verification. Formal verification techniques can help implement an Agile flow.

The software and hardware engineering communities have traditionally used linear development processes such as “waterfall” or the “V-model”. These processes are best suited for projects with stable and clear requirements and a compartmentalized team structure, but are inappropriate for changes in schedule, requirements or resources.

In our fast-paced and highly competitive world, though, it is not uncommon to start coding before detailed and complete documentation is in place. Requirements change, even close to project deadlines, and resources are reshuffled. In some cases, it’s due to issues discovered in previously delivered products that required immediate attention.

Since the inception of the Agile manifesto in 2001, the software community has adopted Agile development practices and processes to overcome the limitations of linear development methodologies. The goal is to deliver better products more efficiently while fostering a more enjoyable working environment.

In recent years, the hardware community has shown interest in Agile and some successes have been reported. The consensus is that while Agile methodologies can bring improvements to hardware development, they need to be adapted to accommodate the key differences between hardware and software projects. For example, hardware development has to account for physical implementation, an aspect missing altogether in software projects, one in which there is a hard shipping deadline beyond which changes are difficult if not impossible. A good starting point to become familiar with Agile, especially for hardware development, is the website AgileSoC.

Agile experience

The aim of this article is to share two experiences where a novel approach was used to develop register transfer level (RTL) modules. System Verilog Assertions (SVAs) were developed in parallel with RTL code using OneSpin Solutions360-DV (Design Verification).

A team of seven design engineers developed the Verilog RTL model largely from scratch. A team of ten engineers, mainly developing directed tests, constrained-random tests, functional coverage and supporting the testbench and scripting infrastructure, carried out the verification task. The verification team reused a sophisticated and mature verification environment. A team of two engineers adapted and maintained a C-model of the IP used as golden reference. Some engineers were not fully allocated to this task, especially in the verification team. The duration of the project was about one year.

Each of the seven designers was responsible for RTL code development of one or more IP sub-modules. Requirements included correct functionality for the overall IP, as well as achieving power, area, frequency and cycle-based performance targets.

RTL development was carried out in stages roughly tied to features. For example, error detection and correction capabilities were introduced in later development stages. Verification had to synchronize with the RTL development plan, as it would have been pointless to run and debug thousands of tests checking functionality not yet fully implemented. Conversely, it was important to stress functionality already implemented.

Agile flow for verification (Source: OneSpin)

Image Agile flow for verification (Source: OneSpin)

My task was to carry out formal verification of two IP sub-modules, which were coded by two different designers. The primary goal of this task was to detect all functional bugs, ideally as soon as they were introduced in the RTL code. The secondary goal was to suggest RTL modifications that could help in achieving physical and cycle-based performance targets.
SVAs were used to verify expected RTL behavior and Property Specification Language (PSL) assertions to model boundary constraints were checked during RTL simulation. Assertions were developed using OneSpin’s 360-DV.

The formal verification process included these steps:

  • Initial familiarization with IP sub-module functionality using existing documents and meeting with the designer
  • Establish compilation, formal linting and autochecks flow using OneSpin Solutions’ 360-DV Inspect
  • Develop properties to verify features in implementation phase
  • Run quick Formal Regression (qFR), which incorporated the linting and other autochecks, as soon as new RTL code was available
  • Debug issues, fix assertions or RTL code and run qFR again until no check fails
  • Run full formal regression
  • Verify next feature
  • When necessary, restructure existing assertions to accommodate changes in features, or match improvements in the RTL implementation.

The designer created a code development branch dedicated to formal verification often updated once a day if not more. The qFR ran on each update and served as a gating point before merging RTL code into the main IP development branch. A large simulation regression, including thousands of directed and constrained-random tests, ran overnight to verify the IP.

Frequent regressions

Typically, the designer ran a simulation mini-regression of about 200 tests before making his code available in the formal verification branch. These tests were selected from the overnight regression and took about 15 minutes when run in parallel on a number of machines. Tests were run on the whole IP and served as a sanity check for the sub-module RTL and its correct integration in the overall IP.

All SVAs were available for the sub-module IP and run on a single machine. The formal engine and interface were flexible enough to allow users to customize the time spent on each check. In most cases, the qFR was set to last about 30 minutes and adjusted by passing a parameter to the TCL regression script. Within this timeframe, 360-DV could typically complete all linting and selected automatic checks, fully proving a few assertions and partially proving the remaining ones.

The formal regression could be set to run several hours to achieve confidence that the RTL functionality matched assertions. It would run all automatic checks, including dead code, finite state machine (FSM) and signal toggle. Typically, this would be done overnight and during weekends.

In most cases, when an assertion was due to fail, the formal engines would be able to find a counter-example quickly, often within seconds. This meant that when the RTL code passed the qFR, it was likely that no fails would be found during the overnight formal regression. Once more, unlike simulation mini-regression, the qFR included all functional checks and assertions, a key difference between the qFR and the simulation mini-regression.

The qFR detected deep RTL corner-case bugs in less than five minutes. On one occasion, I and the designer worked at the same desk, late in the day, rushing an RTL code fix and validating it with the qFR. It took four iterations to get it right, but it was possible to confidently merge the RTL code in the main IP development branch.

Enabling fast fixes

Designers are not keen to rush in a fix by changing the RTL code several times to get it right just before integrating their code in an overall project because they risk messing up others work. In this case, the qFR enabled this efficient flow, based on high confidence and fast iterations.

Results of this development methodology, based on a close collaboration between the RTL designer and formal verification engineer, included:

  • High-quality RTL code delivered ahead of schedule
  • During development, no RTL bugs were found by the overnight simulation regression
  • The designer and verification engineer could focus on their next task, without being pulled back by functional bugs found days or weeks after final check-in, as it is often the case when running extensive constrained-random testing
  • The RTL code underwent months of random testing and is on silicon. No functional bugs have been found so far.

The second point above deserves particular attention. During the IP development, many bugs were detected in other IP sub-modules. Typically, a bug would cause multiple directed or random tests to fail. Verification engineers analyzed failing tests in an attempt to rule out testbench issues. A designer would then do a first-level debug to identify the sub-module problem and pass the test to the sub-module owner. The designer responsible for the sub-module would do further debugging and implement an RTL code fix.

Was that Agile?

The RTL development flow implemented some Agile practices, including a focus on developing high-quality code rather than complete documentation or a detailed plan. The development was feature-driven and the code integrated as often as possible into the main development branch. The designer and verification engineer effectively constituted a self-organized team and worked closely together going beyond their official responsibilities of RTL and SVA coding, respectively. Changes in the RTL implementation to accommodate new features to make the code more robust and improve physical aspects were embraced and dealt with efficiently.

To further harness the benefits of Agile practices within an RTL development project, I would suggest even closer collaboration between the designer and verification engineer with less role boundaries and more code sharing.

Applying this methodology, the formal verification engineer acquired detailed knowledge on the RTL implementation that could be leveraged in other verification tasks. These include writing functional coverage, analyzing structural and functional coverage results, writing constraints to direct random testing and stress sub-module functionality.

Possible objections

The flow described in this paper could give rise to a number of concerns. In the past 15 years, hardware development has embraced the strategy to separate design and verification teams, perhaps excessively. Some popular opinions are:

  • Design and verification engineers should not work too closely as there is a risk that they will interpret specifications in the same way and make the same mistakes
  • White-box verification does not suit an RTL module under development, as continuous implementation changes generate unnecessary re-verification efforts
  • Design and verification require different sets of skills. Therefore, responsibilities should be clearly separated.

The flow presented here is not aligned with these opinions, although they are valid and should be considered carefully. An in-depth analysis goes beyond the scope of this article but the concerns are based on verification experiences with advanced testbench development rather than formal verification.

A pragmatic and gradual approach

Porting Agile practices and processes from software into hardware development requires some level of adaptation and risk mitigation. A gradual approach, based on identifying aspects that come with low risk and provide measurable benefits, is advisable. Successful experiences in using Agile to develop testbench and verification IP have been reported and, not surprising, these tasks, with their required technology and skills, are increasingly software-like in nature.

Although the experience presented here is far from developing an entire SoC using an Agile methodology, it could be a starting point. The experience demonstrates that Agile practices, combined with appropriate supporting technology, can bring benefits beyond testbench development to the hardware community.

An RTL module designed from scratch with mostly control logic, along with high-quality requirements for performance, timing and correct functionality, could be an ideal scenario to apply this approach. Two engineers with appropriate skills, positive attitudes about sharing code, balanced time allocation and experience, could make this work.

Conclusion

The hardware community has an increasing interest in Agile methodologies, fueled by Agile’s success in software projects. However, it is clear that Agile methodologies cannot be applied to hardware projects without some adaptation. Furthermore, companies aiming to fully embrace Agile need to change their engineering culture, a gradual and complex process.
We had a positive experience in adopting formal verification within a RTL development process that implemented Agile-recommended practices in a localized, low-risk fashion. This approach appears to be an effective and pragmatic way to improve the RTL development process by harnessing some of the benefits of Agile.

About the author

Sergio Marchese is a verification consultant at TeraStatic, based in Catania, Italy.

Comments are closed.

PLATINUM SPONSORS

Synopsys Cadence Design Systems Siemens EDA
View All Sponsors