5 ms·

"Are you joking? Intel uses (even invented) so much verification tech it's crazy." That's kinda why I am sniggering. Intel has a rep for letting bugs go to sil

"Are you joking? Intel uses (even invented) so much verification tech it's crazy." That's kinda why I am sniggering. Intel has a rep for letting bugs go to silicon despite all that stuff. In terms of verification, they dropped the ball probably (unless they found these bugs in verification and decided to tape out anyway). One area where they fell on their face seems to be AVX. From TFA, "Certain Combinations of AVX Instructions May Cause Unpredictable System Behavior". That's a huge bug. Remember how we discussed the torture testing of floating point on the RISC-V ? Kinda similar issue. A customer wouldn't be happy with a huge bug there. The big 3 of EDA tools (Cadence, Synopsis, Mentor Graphics) provide their own tools for verifying this stuff called UVM. Like anything, it still relies on the person using the tool. It takes a lot of effort and planning to use this stuff. Whenever the verification engineer has to create Verification IP to test the IP, there's a chance they create bugs of their own. It's like a golden rule. That's why I am not a fan of formal methods. Nothing is proven until you have it working in silicon.

nickpsecurity 11y ago
"That's why I am not a fan of formal methods. Nothing is proven until you have it working in silicon." The one's that did use formal methods all the way did what they were supposed to and usually first pass. They were a mix of academic and defense-related stuff most people can't buy. What I normally see when I look up formal verification in industry is equivalence checking with custom shops also doing protocol verification and certain correctness angles. We've seen lots of what Intel does in their docs. So, that narrows the question down to "Why are these errata in there anyway?" "The big 3 of EDA tools (Cadence, Synopsis, Mentor Graphics) provide their own tools for verifying this stuff called UVM. Like anything, it still relies on the person using the tool. It takes a lot of effort and planning to use this stuff." Didn't know about that one. Thanks. The briefs I just Googled sound weaker than Intel's stuff and especially IBM's where presentations cover an incredible amount of specific verifications. Like you said, what one puts in determines what one gets out of it. So, are Intel just being lax on verification or is their stuff just too complex + optimized to catch all the corner cases? "Intel has a rep for letting bugs go to silicon despite all that stuff. " If it's intentional and avoidable, then I think it might be wise in another light. (Or not, but worth considering.) The other light is the Lipner essay on why shipping is more important than highest quality: https://blogs.microsoft.com/cybertrust/2007/08/23/the-ethics-of-perfection/ https://blogs.microsoft.com/cybertrust/2007/08/23/the-ethics... That comes from a background where he and Karger did high assurance systems that aimed for perfection and got as close as they could in that period. Kept slipping behind competition in terms of features/speed/price and that would effect market share. So, his prior employer canceled that product with his next one following his recommendation to hit acceptable quality levels, ship, and continuosly improve the product. Wonder if Intel is doing that to keep market dominance? "Nothing is proven until you have it working in silicon." This we agree on. The formally verified stuff usually works first try but that's thanks to billions in R&D in tooling & fabs they used. I like knowing a batch of chips performed exactly according to spec when probed during operation. Funny I can't remember what you HW people call that activity. Anyway, I'd love to email or chat with you sometime to see an insider's view on this topic and fill in some blanks. Reason being experienced ASIC people talk very little vs software people. I'm collecting what tidbits of reality I can for a variety of reasons. Two important ones are giving a head start to people aiming for HW design and boosting high assurance design by determining where the weak points are currently. Really busy right now but maybe later on, eh?
- gluggymug 11y ago
  "So, are Intel just being lax on verification or is their stuff just too complex + optimized to catch all the corner cases?" Lax! Of course it's complicated but verification is about finding the corner cases. Intel is driving all these extensions to the ISA. They have a pretty captive CPU market so they are slack. Qualcomm was the same with Wifi SoCs when I was there. Freescale was better but that may be because of the particular projects. "I like knowing a batch of chips performed exactly according to spec when probed during operation. Funny I can't remember what you HW people call that activity." ATE (automatic test equipment)? The thing is that Intel does have the toughest job. They are 28nm with a complicated design, lots of RAM, power is a big issue so clock gating probably everywhere etc. You can't really compare that with a military or an academic chip. The design constraints are much tougher for Intel. Still, Intel supposedly has all the geniuses and the money. They should have no excuses. On the formal stuff, I have yet to be convinced. I never just trust the tools, remember? My email is now in my user profile if you want to discuss further.
  - nickpsecurity 11y ago
    "ATE (automatic test equipment)?" Yeah. It's one of the only processes I have little data on. Must be straight-forward if I haven't stumbled on many academic papers on the subject. If not, there's a siloing effect happening on publishing side & the term will be helpful. "The thing is that Intel does have the toughest job. They are 28nm with a complicated design, lots of RAM, power is a big issue so clock gating probably everywhere etc. You can't really compare that with a military or an academic chip. The design constraints are much tougher for Intel." That's part of my point. Hitting perfection took making the problem a lot simpler than what Intel faced. Same happened in high assurance security where everything TCB was verified down to every trace and state. Took lots of geniuses... "Still, Intel supposedly has all the geniuses and the money. They should have no excuses." ...but still couldn't solve all the problems, keep up in feature parity, meet profit requirements, etc. So, I'm not so harsh on Intel for now given the complexity & business model. I might change my mind later. For now, we'll just disagree. :) "On the formal stuff, I have yet to be convinced. I never just trust the tools, remember?" Now, that I don't get. I've seen, in synthesis/verification work, one 9-transistor analog circuit take (IIRC) 55,000+ equations to represent all its behaviors. Digital ones easier but with tons of multi-layer cells wired up. For custom, they often behave differently. DRC's on modern nodes I read are in 1,000-2,500 range. I'm ignoring OPC because you're handicapped enough at this point. If you don't trust the tools, how are you getting anything done in ASIC land? You must write really fast plus have a discount card at Office Depot to do it all on pencil and paper. :P I think you trust tools more than you're letting on. You probably just cross-check tools with tools in various ways like I did with high assurance SW to catch tool-specific issues. That implies a lot of, but not total, trust in the tools. If I'm wrong, I'll be surprised and probably learn something in the process. There's another method HW people might already use that comes from theorem provers. They know the proving process is complex. It also breaks down into a series of primitive actions in logic. So, they split the activity between a complex, untrusted prover and a simple, easy-to-verify checker. I know state-machine equivalence & even many physical phenomenon can be modeled well in software. I've seen as much with FEC systems. Trick for HW might be turning all the tool outputs into a series of steps like in an audit log that such tools can verify. That might take a hell of a long time, though, but also should be easy to parallelize onto clusters, GPU's, FPGA's, etc. Do it on a macro-cell at a time composing the results like in proof abstraction or abstract interpretation for software. What you think?

nickpsecurity 11y ago

"That's why I am not a fan of formal methods. Nothing is proven until you have it working in silicon." The one's that did use formal methods all the way did what they were supposed to and usually first pass. They were a mix of academic and defense-related stuff most people can't buy. What I normally see when I look up formal verification in industry is equivalence checking with custom shops also doing protocol verification and certain correctness angles. We've seen lots of what Intel does in their docs. So, that narrows the question down to "Why are these errata in there anyway?" "The big 3 of EDA tools (Cadence, Synopsis, Mentor Graphics) provide their own tools for verifying this stuff called UVM. Like anything, it still relies on the person using the tool. It takes a lot of effort and planning to use this stuff." Didn't know about that one. Thanks. The briefs I just Googled sound weaker than Intel's stuff and especially IBM's where presentations cover an incredible amount of specific verifications. Like you said, what one puts in determines what one gets out of it. So, are Intel just being lax on verification or is their stuff just too complex + optimized to catch all the corner cases? "Intel has a rep for letting bugs go to silicon despite all that stuff. " If it's intentional and avoidable, then I think it might be wise in another light. (Or not, but worth considering.) The other light is the Lipner essay on why shipping is more important than highest quality: https://blogs.microsoft.com/cybertrust/2007/08/23/the-ethics-of-perfection/ https://blogs.microsoft.com/cybertrust/2007/08/23/the-ethics... That comes from a background where he and Karger did high assurance systems that aimed for perfection and got as close as they could in that period. Kept slipping behind competition in terms of features/speed/price and that would effect market share. So, his prior employer canceled that product with his next one following his recommendation to hit acceptable quality levels, ship, and continuosly improve the product. Wonder if Intel is doing that to keep market dominance? "Nothing is proven until you have it working in silicon." This we agree on. The formally verified stuff usually works first try but that's thanks to billions in R&D in tooling & fabs they used. I like knowing a batch of chips performed exactly according to spec when probed during operation. Funny I can't remember what you HW people call that activity. Anyway, I'd love to email or chat with you sometime to see an insider's view on this topic and fill in some blanks. Reason being experienced ASIC people talk very little vs software people. I'm collecting what tidbits of reality I can for a variety of reasons. Two important ones are giving a head start to people aiming for HW design and boosting high assurance design by determining where the weak points are currently. Really busy right now but maybe later on, eh?

gluggymug 11y ago
"So, are Intel just being lax on verification or is their stuff just too complex + optimized to catch all the corner cases?" Lax! Of course it's complicated but verification is about finding the corner cases. Intel is driving all these extensions to the ISA. They have a pretty captive CPU market so they are slack. Qualcomm was the same with Wifi SoCs when I was there. Freescale was better but that may be because of the particular projects. "I like knowing a batch of chips performed exactly according to spec when probed during operation. Funny I can't remember what you HW people call that activity." ATE (automatic test equipment)? The thing is that Intel does have the toughest job. They are 28nm with a complicated design, lots of RAM, power is a big issue so clock gating probably everywhere etc. You can't really compare that with a military or an academic chip. The design constraints are much tougher for Intel. Still, Intel supposedly has all the geniuses and the money. They should have no excuses. On the formal stuff, I have yet to be convinced. I never just trust the tools, remember? My email is now in my user profile if you want to discuss further.
- nickpsecurity 11y ago
  "ATE (automatic test equipment)?" Yeah. It's one of the only processes I have little data on. Must be straight-forward if I haven't stumbled on many academic papers on the subject. If not, there's a siloing effect happening on publishing side & the term will be helpful. "The thing is that Intel does have the toughest job. They are 28nm with a complicated design, lots of RAM, power is a big issue so clock gating probably everywhere etc. You can't really compare that with a military or an academic chip. The design constraints are much tougher for Intel." That's part of my point. Hitting perfection took making the problem a lot simpler than what Intel faced. Same happened in high assurance security where everything TCB was verified down to every trace and state. Took lots of geniuses... "Still, Intel supposedly has all the geniuses and the money. They should have no excuses." ...but still couldn't solve all the problems, keep up in feature parity, meet profit requirements, etc. So, I'm not so harsh on Intel for now given the complexity & business model. I might change my mind later. For now, we'll just disagree. :) "On the formal stuff, I have yet to be convinced. I never just trust the tools, remember?" Now, that I don't get. I've seen, in synthesis/verification work, one 9-transistor analog circuit take (IIRC) 55,000+ equations to represent all its behaviors. Digital ones easier but with tons of multi-layer cells wired up. For custom, they often behave differently. DRC's on modern nodes I read are in 1,000-2,500 range. I'm ignoring OPC because you're handicapped enough at this point. If you don't trust the tools, how are you getting anything done in ASIC land? You must write really fast plus have a discount card at Office Depot to do it all on pencil and paper. :P I think you trust tools more than you're letting on. You probably just cross-check tools with tools in various ways like I did with high assurance SW to catch tool-specific issues. That implies a lot of, but not total, trust in the tools. If I'm wrong, I'll be surprised and probably learn something in the process. There's another method HW people might already use that comes from theorem provers. They know the proving process is complex. It also breaks down into a series of primitive actions in logic. So, they split the activity between a complex, untrusted prover and a simple, easy-to-verify checker. I know state-machine equivalence & even many physical phenomenon can be modeled well in software. I've seen as much with FEC systems. Trick for HW might be turning all the tool outputs into a series of steps like in an audit log that such tools can verify. That might take a hell of a long time, though, but also should be easy to parallelize onto clusters, GPU's, FPGA's, etc. Do it on a macro-cell at a time composing the results like in proof abstraction or abstract interpretation for software. What you think?