Introducing sequential equivalence checking
In combinatorial equivalence checking, the key was finding the corresponding state storage devices in each design, though the encoding of those states may vary across designs or be difficult to find. In sequential equivalence checking8, the designs can be retimed in relation to each other, meaning that some states may at times be modeled exclusively.
In Figure 2, the design on the right deposits an intermediate value in the register. The other design does not correspond, except for the ephemeral signal value on first adder output.
A sequential equivalence checker needs to recognize corresponding values in the two designs and then ascertain that the function is present in both between the identified time points. This is called a “synchronization point."9 Similarities are expected between the two designs, simplifying identification of the compare points.
Looking into the crystal ball
The key to successful future projection is using the right data points and trends that maintain validity. When implementation changes were made in a gate level design, testing occurred before it was checked to avoid disturbing the rest of the system.
The answer was not running the complete test suite. Combinatorial equivalence checking solved this and enabled verification to migrate to a higher level of abstraction. Longer, more robust tests were created when functional verification concentrated on the RTL level.
Similarly, sequential equivalence checking could eliminate the necessity for most functional verification at the RTL level. Temporal assertions are advancing with the standardization and adoption of PSL and SystemVerilog, meaning that a solution for ensuring that the timing of the implementation model conforms to the specification is emerging. The high-level simulators much faster than the existing emulators running at the RTL level have already demonstrated the enormous amounts of functional verification they can provide.
All three pieces of technology that are necessary to enable the transition to higher levels of abstraction are in place and maturing. In coming years, we expect to see significant changes in approaches to the verification problem, which will enable larger, more complex designs to be tackled, as well as affect the design flow.
Many designers are reluctant to build and use behavioral models because they cannot check for functional equivalence between them and RTL designs. Sequential equivalence checking will increase confidence, regardless of the decision to adopt behavioral synthesis tools. Hopefully, these performance and quality improvements will continue until the next major roadblock in the flow is encountered, which will involve managing the necessary levels of concurrency in the design.
1. Bailey - executive editor: The Functional Verification of Electronic Systems. International Engineering Consortium 2005
2. Bailey, Martin & Anderson: Taxonomies for the Development and Verification of Digital Systems. Springer 2005
3. Open SystemC Initiative: http://www.systemc.org/
4. ARM PrimeXsys Platforms overview: http://www.arm.com/products/solutions/PrimeXsysPlatforms.html
5. Keenan: "TI builds wireless VoIP solution using OMAP architecture," CommsDesign, Sept. 2004
6. "The System Engineering Inflection Point," Vast Systems whitepaper, Jan. 2004
7. Stoye, Greaves. "Using VTOC for large SoC concurrent engineering: A real world case study." DesignCon 2003
8. Van Eijk: Sequential Equivalence Checking Based on Structural Similarities. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, Vol. 19, No. 7, July 2000
9. Sequential Equivalence Checking: A New Approach to Functional Verification of Datapath and Control Logic Changes. Calypto web site, 2005, http://www.calypto.com.
Brian Bailey is an independent functional verification consultant helping system designers improve their verification efficiency, and providing guidance and technology services to small start-up companies and venture capital companies. He has spent over 20 years creating verification solutions in a number of EDA companies and is active in the standards community. He can be reached at firstname.lastname@example.org.