4 ms·

"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 bu

"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?
- gluggymug 11y ago
  "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." While it is true that we use tools to cross check each other, what I mean is that we regularly are manually looking through waveforms. At every stage of the flow, we are checking that our verification infrastructure is actually doing what it should to find bugs. Because a lot of the time, either we've stuffed up using the tool or the tool itself is stuffed. So much tooling is provided for you. Bus functional models, protocol checkers, etc. You are just cramming it all together and writing your own stuff over the top. There is always a mistake in there somewhere. "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." This is what happens with the UVM. A checker is written with a SystemVerilog interface by a third party or ourselves. It uses the UVM standard so you can integrate it with other UVM stuff to make even more abstract checkers. If I am writing the prover, I know I probably threw a few bugs in there! If only it were all parallelised because it is slow as hell.
  - nickpsecurity 11y ago
    "what I mean is that we regularly are manually looking through waveforms. At every stage of the flow, we are checking that our verification infrastructure is actually doing what it should to find bugs. Because a lot of the time, either we've stuffed up using the tool or the tool itself is stuffed." Waveform-based verification is something I know nothing about. I haven't seen it in any paper I've looked at. Is that what people do in logic analyzers and such? Do you have a link to a free reference discussing what people do with that stuff and how it's used to verify digital designs? I really should have this info in mind and on hand if you all rely on it more than verification tools. "This is what happens with the UVM. A checker is written with a SystemVerilog interface by a third party or ourselves. " That makes sense. "If I am writing the prover, I know I probably threw a few bugs in there!" I like that you're realistic. It's how I used to look at code on a complex project. Even with Correct-by-Construction, I didn't get to feel safe with my code: only wonder how obscure or unnecessarily simple a problem was left in it. I need to make a Philosoraptor meme along the lines of: "Do we create coding schemes or does the code scheme against us?" Haha. "If only it were all parallelised because it is slow as hell." There's the opportunity. Whether it can be acted on who knows. I do know so far that hardware is many blocks strung together with all kinds of tests that should be parallelizable. Now you've reinforced this potential in my mind. I have a trick for this but I'm holding off publishing it for now. Let's just say it's easier to parallelize stuff if one doesn't force their implementation to be inherently sequential or even tied to CPU's. And there's a little-known, albeit alpha-quality, way of doing both at once. :)

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?

gluggymug 11y ago
"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." While it is true that we use tools to cross check each other, what I mean is that we regularly are manually looking through waveforms. At every stage of the flow, we are checking that our verification infrastructure is actually doing what it should to find bugs. Because a lot of the time, either we've stuffed up using the tool or the tool itself is stuffed. So much tooling is provided for you. Bus functional models, protocol checkers, etc. You are just cramming it all together and writing your own stuff over the top. There is always a mistake in there somewhere. "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." This is what happens with the UVM. A checker is written with a SystemVerilog interface by a third party or ourselves. It uses the UVM standard so you can integrate it with other UVM stuff to make even more abstract checkers. If I am writing the prover, I know I probably threw a few bugs in there! If only it were all parallelised because it is slow as hell.
- nickpsecurity 11y ago
  "what I mean is that we regularly are manually looking through waveforms. At every stage of the flow, we are checking that our verification infrastructure is actually doing what it should to find bugs. Because a lot of the time, either we've stuffed up using the tool or the tool itself is stuffed." Waveform-based verification is something I know nothing about. I haven't seen it in any paper I've looked at. Is that what people do in logic analyzers and such? Do you have a link to a free reference discussing what people do with that stuff and how it's used to verify digital designs? I really should have this info in mind and on hand if you all rely on it more than verification tools. "This is what happens with the UVM. A checker is written with a SystemVerilog interface by a third party or ourselves. " That makes sense. "If I am writing the prover, I know I probably threw a few bugs in there!" I like that you're realistic. It's how I used to look at code on a complex project. Even with Correct-by-Construction, I didn't get to feel safe with my code: only wonder how obscure or unnecessarily simple a problem was left in it. I need to make a Philosoraptor meme along the lines of: "Do we create coding schemes or does the code scheme against us?" Haha. "If only it were all parallelised because it is slow as hell." There's the opportunity. Whether it can be acted on who knows. I do know so far that hardware is many blocks strung together with all kinds of tests that should be parallelizable. Now you've reinforced this potential in my mind. I have a trick for this but I'm holding off publishing it for now. Let's just say it's easier to parallelize stuff if one doesn't force their implementation to be inherently sequential or even tied to CPU's. And there's a little-known, albeit alpha-quality, way of doing both at once. :)