Posted by Iain Singleton on June 2, 2017
Ever since I started working in verification it’s always felt like a huge responsibility. It’s up to me to make sure that this design doesn’t have a bug that could sneak its way into silicon, then into millions of consumer products, bankrupting the company or worse. I always felt like missing that one issue in that one line of RTL could be the first beat of the butterfly wing that starts some kind of global meltdown! Perhaps my paranoid delusions make me a better engineer, likely not, but I’m stuck with them nonetheless!
The fact I’ve always been lucky enough to work with formal has been something of a comfort. I know that I’m exploring all possibilities, leaving no stone unturned, so my worries get somewhat minimized. When it comes to accuracy of constraints however, I’ve always had a tough time feeling confident in them.
Formal technology has evolved significantly in recent years and I now have access to a wider range of features that can help me rest a little easier. From built in coverage based overconstraint analysis, to waveform based design exploration I now have a much better idea of what my constraints are really doing. We’ll discuss these in more detail in subsequent blogs but if you’re interested in learning a little more check out this cool webinar on formal sign off flows
These new features have helped me a lot, but it’s not to say I haven’t, at times, still found myself sat with no spec, an un-cooperative designer sat 5000 miles away and an impossible timescale. I guess engineering wasn’t supposed to be easy! Thinking about this blog entry reminded me of an old fairy tale, Goldilocks and the Three Bears, which I have unashamedly used below to explain how life with constraints can sometimes feel. #thestruggleisreal my friends!
Once upon a time there was an engineer called Goldilocks, who was tasked with formally verifying a block for Bear Industries. Goldilocks studied the spec for the prdge-300 block and developed her test plan as accurately as possible, but the spec was confusing and missing micro-architectural information. Goldilocks set about trying to develop her constraints as best she could. As this was a packet based interface she reasoned “It must be the case that I can only change the input data on a valid and ready.” Goldilocks added her constraint and ran her formal tool. Her assertions failed! Goldilocks jumped for joy and called the designer as quickly as possible. “I’ve found a bug!” she exclaimed, her cry ringing out across the cubes of the office. The grumpy design engineer was very busy. His block had already been verified in simulation and he did not have time to be wasted. After reluctantly reviewing the waves he responded to Goldilocks “This trace is nonsense! You can’t have packet IDs changing during a packet!”
Goldilocks’ realized that her constraint was too underconstraining and she would need to review her environment.
Taking the design engineers comments on board Goldilocks went back to her emacs to try again. “Hmm IDs can’t change during a packet?” Goldilocks pondered, “that must mean I should make them stable!” Goldilocks added her new constraint and re-ran the properties. All full proofs! Goldilocks was pleased that she had been able to close some of the tough properties and gleefully passed her block off for review and sign-off. Later that day however, Goldilocks received a call from the review team to say that her constraints failed in the top level simulations. Packet IDs should be allowed to change, just not during the same packet transfer. Her second constraint had been too overconstraining. The management team and designer were starting to question the value of formal, they’d been taping out for years using simulation and didn’t know why they should be wasting any more money.
Goldilocks was nothing if not a determined engineer and would not let these setbacks stop her from completing her formal work. She chased up the designer for final clarification on the interfaces and sat up late that evening to complete the work. Running her properties one final time she saw a failure! Goldilocks sent the waves to the designer and her environment to the review team and went to bed.
Having stayed up so late the previous evening Goldilocks overslept and in the morning was awoken by a call from Bear Industries. Goldilocks was panicked and ready to rush to the office but on the phone was the director of verification. “Great work Goldilocks! Your constraints have passed review and the failure was a critical bug we missed in simulations!” The management team and grumpy design engineer all came around to the joys of formal, her third constraint was just right.
Our global team of experts share their insights about the latest technologies, trends, and solutions in formal verification.