- Processor Verification
- ARM-Based SoC Verification
- Configurable IP Verification
- DSP Verification
Regardless of application, the logic of a design block falls into one of the three categories:
- Control Logic – controls how things should operate, such as arbiters, interrupt controller, power management unit, tag generators, and schedulers.
- Data Transport Logic – moves data from one end of the design to another, such as bus bridges, memory controller, PCI Express and USB controllers, DMA controllers, and switching blocks.
- Data Transform Logic – transforms data using some algorithms or mathematical functionality, such as MPEG decoders, image processors, security processors, and classification search blocks.
Different types of designs are suitable for different verification strategies. For example control intensive logic and data transport logic are good candidates for model checking (MC), whereas data transform logic is a good candidate for sequential equivalence checking (SEC). It is important to spend time on formal test planning so that the correct technology is deployed to verify the right block, so as to reduce overall verification cost and effort.
Oski has used formal technologies to verify all kinds of designs, as demonstrated by the diversity of our customer list. Contact us to find out what further can be done to verify your design.
Many blocks in a CPU design are good candidates for formal verification. Below is a block diagram of ARM Cortex-A15 processor, used only as an illustration. The blocks highlighted in yellow are suitable blocks for formal verification.
Some example properties that can be verified using formal verification include:
- “If a read arrives after a write, read data must match the last write’s data” for the Load-Store block.
- “If a write arrives for a pre-fetched address, followed by a read, read must not be serviced locally by pre-fetched data” for the Prefetcher block.
- “Instruction must not be dispatched unless all input operands required by the instruction are ready” for the Scheduler/Dispatch block.
- “Return stack never gets corrupted, even with spills and fills” for the Branching block.
- “A line can’t be made dirty unless it has unique permissions or unique permissions requested” for the Cache Controller block.
These properties are hard to verify with simulation, but formal technology that uses symbolic representation and Oski Abstraction Models can catch many corner case bugs. Some example bugs that are discovered include:
- A store queue is drained while data is yet to be written at the destination, a load uop with matching address arrives
- Dirty data in L1 cache was overwritten by stale L2 data, due to a false L2 request initiated by prefetch
- Exactly two threads were executing, one each in identical position in the two halves ( and ), both threads saw an illegal instrunction causing thread termination, but the Branching unit did not load new work from Return Stack causing an infinite loop with no active threads
- A Read Unique snoop request caused cache line state transition UD à I. In a corner case cycle a pipe uop still hits, and hence instruction successfully completes, causing cache inconsistency
Modern processor designs include many CPU cores, so it is even more important to use formal technology to exhaustively verify these CPU sub-blocks to minimize the verification effort at the top level, thereby reducing verification cost and shortening time to market. Oski can assist you with the complex tasks of processor verification using formal technology and Oski Abstraction Models.
ARM-Based SoC Verification
Most SoC designs today consist of ARM processors, internal and/or 3rd party IPs and are based on standard or custom bus interfaces. Many blocks in such SoC are good candidates for formal verification to replace simulation when doing functional verification.
The following diagram shows a conceptual SoC: the blocks in yellow and orange can be verified using model checking (MC) or sequential equivalence checking (SEC). For example, in a wireless subsystem consisting of MAC (Media Access Control), BB (Base Band) and radio (RF) blocks, the MAC can be verified using model checking, the BB can be verified using sequential equivalence checking by comparing RTL with the C reference model, and the RF should use the traditional simulation for verification. The whole wireless subsystem should still be verified using simulation, however with the verification effort spent in formally verifying MAC and BB, the effort and time it takes to simulate the whole wireless subsystem would be significantly reduced.
Oski has performed many projects on SoC verification and can assist you in identifying the best blocks for formal technology so you get the best verification ROI, taking advantage of the strength of both formal and simulation in your verification flow.
Configurable IP Verification
IPs are major building blocks of today’s SoCs. Most IPs today are highly configurable to satisfy the different needs and requirements of IP consumers. For example, a DDR memory controller can have the following configurations:
- Memory space: 16MB to 32GB
- Memory channel widths: x8/x16/x32/x64
- Number of ranks: 1 to 4
- Page management policy: Closed/Open Page
- Address mapping schemes
- Number of ports: 1 to 16
- Data Width: 32b, 64b or 128b
- DDR Timing parameters
Taken together, a DDR memory controller could offer more than 1 million different configurations, impossible for IP providers to verify all the configurations using simulation. By the same token, IP consumers can never be sure the configuration they have in use are thoroughly verified by the IP provider.
The solution to the problem consists of two parts:
- Deploy formal technology to thoroughly verify each IP. The symbolic nature of formal verification ensures that all configurations are verified, leaving no chance for bugs to slip through.
- Provide reusable and configurable IP kit which doesn’t just include configurable design IP, but also configurable Formal Testbench IP as shown in the diagram below. With the provided Formal Testbench, IP consumers can verify the specific configuration in use and confident that any modification made by the IP consumers will not cause design errors.
Oski can assist IP providers (external 3rd party or company internal group) to formally verify highly configurable IPs. “Oski Certified” IP means quality IP, a competitive advantage for IP providers.
Most DSP designs are “data transform” designs that change the value of the data based on certain functionality, such as convolution, FFT, and inverse quantization. Often DSP designs start with a C reference model and the RTL model can be manually written based on the high level spec or automatically generated using high level synthesis tools. For these types of designs, sequential equivalence checking that compares the RTL with the golden C reference model can offer the formal confidence that the RTL design is correct to the spec. Unlike combined equivalence checking tools that are easier to use and debug, sequential equivalence checking often requires constraints and Abstraction Models in order to converge.Oski can assist you in applying the SEC tools effectively for your DSP designs.