Formal, simulation, and AMBA verification IP combine to verify configurable powerline networking SoC
21 November 2013
HomePlug SoC functional block diagram
While wireless networking is a convenience, it is only valuable when it works. The HomePlug Broadband power line networking SoC is designed to enable networks over common power lines, extending the Internet to places where wireless networks cannot reach.
Such a product is subject to high schedule and cost pressures; we must constantly work to balance the development of cutting edge, differentiated capabilities with leveraging off-the-shelf, standard IP and interfaces and a myriad of peripherals.
By broadening our horizons and intermixing a formal analysis “app”, simulation, and assertion-based verification IP, my team and I obtained more complete results, faster and more efficiently than ever before. Some verification tasks naturally align with a given technology – for example, constrained random simulation is great for driving packet traffic and validating robustness to input noise, while formal is perfect for exhaustive analysis of complex logic and IP connectivity.
The device under test
The HomePlug powerline networking SoC (system on a chip) combines a high performing programmable powerline modem implementing HomePlug AV, 1.0 and GP PHY and MAC layers and an ARM9 CPU with an integrated analogue front end and on-chip peripherals. The variety of capabilities means that customers can employ 39 different peripherals of varying degrees of sophistication, in 1000s of operational use cases. Figure 1 is from the part’s datasheet.
Verifying IP connectivity
The first task is validating the basic connectivity between the IPs and peripherals of a given part configuration. This does not sound like much of a challenge until you realise that there are several low power, BIST (built-in self test), and other configuration modes that affect and/or multiplex the control signal and data paths even before any customer-requested customisations are included. This adds up to 10,000s of connections to be verified to 100% accuracy.
Initially we relied on detailed manual inspection plus C-based simulation testbenches and waveform analysis to indirectly provide this connectivity verification. However, it soon became clear that this next generation design, with the large number of peripherals, required an exhaustive approach.
Block diagram of AHB master interface
We looked to formal verification and found a solution in the SoC Connectivity App that runs on our formal tool (Cadence Incisive Formal Verifier). This app uses a clear text Excel spreadsheet to capture the connectivity spec. It automatically creates the corresponding assertions, runs the formal tool, and thus the counter examples from any assertion failures, pinpointing any errors. New configurations of IP can be verified within a matter of hours rather than several weeks, the time taken with the prior simulation based process.
During the verification a wrong connection on TX and RX line for the UART block was found. The ports were wrongly connected to the same GPIO instead of one for TX and another one for RX. This bug was not found with functional simulation where the UART was connected in loopback.
AMBA protocol verification
The ARM AMBA bus is a central artery for the SoC, and as the number of peripherals increased, the complexity of the AMBA implementation grew. Some of the IPs connecting to the internal bus were very complex themselves, featuring many operating and low power modes. From a project management point of view, the less time spent on standard, undifferentiated buses and components meant more time spent developing our high value differentiated IPs.
Consequently, it was decided to use assertion-based verification IP (ABVIP) for the AMBA protocol. This is a library of SVA/PSL assertions that capture the AMBA protocol rules such that formal or dynamic simulation tools can verify any errors in the front side of the IPs on the AMBA bus. Formal was also used to verify the AHB master interface since master port verification is a well known, clear strength of formal analysis.
Several peripherals of the device have AMBA master interfaces, beside the common slave interfaces. Adding to the verification challenge, these masters can have also more than two embedded DMA controllers. Error! Reference source not found. shows a simplified block diagram of the verified AHB master interface. It is formed of three FSMs that can generate AHB transactions that can be configured by registers accessible via AHB slave interfaces. This block has been extracted from the whole IP and some configuration has been constrained through assumed constructs.
Numerous slave peripherals hang off the bus for any given product derivative. When the formal analysis with the ABVIP was run, several bugs were discovered in the most mature peripherals; IP that had been simulated before and used in other designs. Over the duration of one project, seven violations of the AMBA protocol were found. Several bugs proved to be minor as the robustness of the AMBA protocol minimised their affects. Others were “must fix” bugs that would have meant trouble for the finished product(s).
Compared to earlier simulation based techniques, utilising formal technology within the familiar “app” and verification IP frameworks has enabled exhaustive verification of a complex DUT in a shorter amount of time, with higher quality of results, reports the team.
Since the success of the first project using this methodology, the team has taped-out multiple products with this flow, and the silicon validation results have been perfect. The flow has been deemed a “valuable contribution” to the overall team’s throughput, and a major cost and risk reduction for products.
Figure 1: HomePlug SoC functional block diagram.
Figure 2: Block diagram of AHB master interface.
Contact Details and Archive...