Hardware/Software Verification enters the "atomic age": Part 2

George Harper, Bluespec

April 2, 2008

George Harper, Bluespec

Today's system designs are increasingly complex, especially in the dimension of concurrency, on both the hardware and software sides. As pointed out in Part 1, the industry is just now seriously grappling with how to write parallel software on new multi-threaded and multicore hardware architectures that keep growing in size and complexity.

Atomic transactions are emerging as a powerful new tool with all of these efforts and enabling a new atomic age for hardware and software design. Rishiyur Nikhil and Arvind have discussed the implications of atomicity in software design in an earlier series on Embedded.com. . Here I will confine the topic to the impact on hardware verification methodology.

When verification teams are the downstream beneficiaries of designs built using atomic transactions instead of traditional, lower-level concurrency mechanisms, there are implications both to the methodologies that they might use and to the benefits that they might experience.

As an example, let's look at the verification of hardware designed with BSV (Bluespec SystemVerilog). Enabled through atomic transactions, BSV has module interface semantics and guards that ensure that other modules will properly interface with them. Once the interface is verified at the module unit level, it cannot be improperly interfaced with when integrated within a larger design.

BSV is explicitly parallel and based on atomic transactions, the highest level of abstraction for specifying concurrent behavior, so prevalent in System-on-Chips. Its atomic transactions encompass communication protocols across module boundaries, enabling robust scaling to large systems and robust IP reuse. For this reason, BSV's atomic transactions are composable " easily scaling to larger, more complex designs without a corresponding increase in complexity.

Figure 1: BSV compilation stages

Starting at a high-level model, implementation, transactor or testbench designed with these atomic transactions, the BSV compiler (Figure 1, above) can synthesize efficient Verilog RTL for use in an emulator, FPGA or ASIC. Or, it can generate a fast SystemC simulation object. Composable atomic transactions for hardware enable:

* Design by refinement from executable specification to final implementation
* Architectural exploration with early architectural feedback
* Early fast executable models for software development
* Synthesizable models and verification

What are the implications to verification methodology? As an example, let's look at the verification of hardware designed with BSV. Even when not using BSV directly, for synthesizable test benches and reference models, verification derives many benefits when the design under test (DUT) has been designed with BSV. These benefits include the following:

1) With much simpler, more powerful concurrency management, atomic transaction-based designs have many fewer bugs. This translates into much less time spent diagnosing and debugging bugs and more time spent waiting for re-work, performing re-verification, and developing additional tests. And, since designs are stable much earlier, FPGAs and emulators can be leveraged much earlier in the design cycle.

2) Written at a significantly higher level, these designs result in earlier code availability and code that is easier to interconnect and that is more mature. This translates into earlier design and verification integration, faster resolution of integration issues, and a much earlier start to real verification.

3) Atomic transactions enable more IP reuse, which eliminates verification by leveraging previous verification efforts.

4) As these designs are written operation-centrically as opposed to state-centric, they are simpler to understand and read like specifications. This makes it much easier to write tests targeted at the hardware. As tests and executable specifications deal with the same concepts, it makes it much easier to get the tests correct and complete, including corner cases.

5) With formal interface semantics that ensure proper module instantiation, there is less to verify at the system level and better leverage of unit level verification. This enables a strategy where you can verify module interface behavior once, not at every instantiation.

Let's specifically look at the final point in detail and explore how this changes how verification may approach this aspect of a design.

Figure 2: BSV compilation with the Verilog back end

As mentioned earlier, BSV has module interface semantics and guards that ensure that other modules will properly interface with them. This capability enables a completely different attack plan by a verification team, which usually focuses on system level verification, and less so on blocks or sub-IP.

Atomic-transaction-based interface semantics and guards allow a strategy of attacking the design inside out " and focusing on units and re-usable library elements first, and then focusing on the system.

This will be possible because unit level interface testing is 100% leverageable at higher levels of design hierarchy. Instead of verification growing exponentially with size/complexity, it might grow more linearly.