A Fractal Design Approach to Ease Verification
A graduate student working with Daniel Sorin is taking a novel design approach to ease the verification process
In 1994, a small glitch was uncovered in a floating point unit in the Pentium P5 microprocessor. Unfortunately, it wasn’t detected until after it had been installed in countless computers, which forced the company to take a $475 million charge to replace the faulty components.
Somehow, the defect slipped past the company’s rigorous testing procedures. These instances, though extremely rare in the industry, demonstrate how important in can be for manufacturers to ensure that computer components perform up to design expectations.
The process of ensuring that a computer component or a piece of software operates as expected is known as verification. A graduate student working with Daniel Sorin, associate professor of electrical and computer engineering at the Pratt School of Engineering, is taking a novel design approach to ease the verification process.
“Traditionally, two distinct groups are involved in the creation of a new product, such as a central processing unit (CPU) for a computer,” said Meng Zhang, a third-year graduate student in electrical and computer engineering. “Typically, the designers create a component for a specific need, and then pass the finished product on to the verification specialists, whose tests ensure that it functions properly.”
The verification is usually an isolated step performed on the more or less finalized design, she explained, adding that it is highly likely that later a design is discovered to be very difficult to verify specifically because its verifiability was not considered in the design stage.
Zhang is working on an approach that helps breaks down the barriers that often separate the designers from the “verifiers.”
“We are investigating strategies that encourage the designers to consider verifiability early in the design stage and design the system in a way that is amenable to verification,” she said. “That could streamline the process and make it more reliable.”
The Intel case of 1994 illustrates how important the verification process can be, especially as computer components become increasingly complex and are integrated into myriads of devices.
One form of verification, known as “formal,” involves exploring all the states a system can have to uncover bugs, a useful way to prove the correctness of system and very important in life-critical areas – such as medical devices -- but also a process that is very time-consuming and expensive.
To achieve the completeness of such a formal verification process, Zhang and Sorin believe that components could be designed with fractal theories in mind. That means that the architecture of a component is made up of smaller, and identical, building blocks. Each building block is a reduced size copy of the whole. Their goal is to explore how to design processors and their memory systems to make them more amenable to verification.
“Using this fractal-based approach to architecture design, if we can verify the correctness of the smallest building block, we can prove the correctness of the whole system by induction,” Zhang said. “Since each part looks and acts like the whole, we can be confident that there are not any errors in the whole system.”
Specifically, she is applying this fractal-based approach in cache coherence, which refers to the consistency of shared data, such as that stored on multiple CPUs within a laptop computer.
“You need to verify that the different CPUs are reading the latest data in a coordinated way,” she explained. “We don’t want any of them working off stale data.”
Zhang was drawn to this field of research because it straddles two disciplines that have not always been known to work closely together – designers of computer architecture and those responsible for proving the component works. She experienced a steep learning curve, since before coming to Duke, she primarily had been studying systems-level computer architecture.
She expects to complete her PhD in 2013, and hopes to be able combine her interests in architecture and verification. She came to Pratt in 2008 after obtaining her M.S. and B.S. degrees from Beihang University in China.