3 ms·

Hmm. I don't use Alloy nor do I know hardware yet. I'll still try to dig up something. (comes back) It looks like a lot of CompSci folks built test generation i

Hmm. I don't use Alloy nor do I know hardware yet. I'll still try to dig up something. (comes back) It looks like a lot of CompSci folks built test generation in Alloy for languages such as Java. Might have not released any general tools for Alloy, though. Good news is they describe the benefits and some specifics where hardware people might get ideas for homebrew tools. https://repositorio-aberto.up.pt/bitstream/10216/59949/1/000145607.pdf https://repositorio-aberto.up.pt/bitstream/10216/59949/1/000... http://www.dcc.fc.up.pt/~rvr/resources/MAP-i/2014s7c-mapi.pdf http://www.dcc.fc.up.pt/~rvr/resources/MAP-i/2014s7c-mapi.pd... One application to hardware with Alloy: http://www.samkirk.com/atpg-in-alloy4/ATPG_in_Alloy.pdf http://www.samkirk.com/atpg-in-alloy4/ATPG_in_Alloy.pdf Honestly, I'd have thought TLA+ would be better of the two for hardware given it deals with concurrent things. Also, it can do stuff similar to SPIN model-checker that was used extensively for hardware verification in the past. For hardware, I'd have experimented with SPIN for lightweight method with ACL2 for heavyweight esp thanks to Jared Davis at Centaur contributing ACL2 components he used. http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html https://www.cs.utexas.edu/~jared/publications/2011-memocode-centaur.pdf https://www.cs.utexas.edu/~jared/publications/2011-memocode-... Just for kicks, I did some quick Googling on test generation for sequential circuits to see if I could find anything interesting for you. Me, too, as I enjoy seeing what people do in your field. Most were paywalled but this one wasn't: http://www.smc2017.org/SMC2017_Papers/media/files/0080.pdf http://www.smc2017.org/SMC2017_Papers/media/files/0080.pdf

dbcurtis 9y ago
Thanks for the links. My current application is not test generation for hardware, though. I'm working with autonomous robots that need to interact with real world obstacles that can't be easily predicted (laundary carts, golden retrievers, bride's maids....), need to navigate spaces where WiFi comes and goes, and need to interact with other automated systems running their own state machine that I don't control. Something that could identify "Recovery scenario needed here" has good value.
- nickpsecurity 9y ago
  Apparently, I totally misread what you needed. Sorry. Your domain is very interesting. I briefly studied it a long time ago. They were using fusion of data coming from different components with quite non-deterministic algorithms such as fuzzy logic or neural networks. There wasn't any way to verify them at the time. I've seen a few attempts at such things but would need to know what kind of algorithm you use for sense, learn, and act (or whatever they call it). No guarantees here.

dbcurtis 9y ago

Thanks for the links. My current application is not test generation for hardware, though. I'm working with autonomous robots that need to interact with real world obstacles that can't be easily predicted (laundary carts, golden retrievers, bride's maids....), need to navigate spaces where WiFi comes and goes, and need to interact with other automated systems running their own state machine that I don't control. Something that could identify "Recovery scenario needed here" has good value.

nickpsecurity 9y ago
Apparently, I totally misread what you needed. Sorry. Your domain is very interesting. I briefly studied it a long time ago. They were using fusion of data coming from different components with quite non-deterministic algorithms such as fuzzy logic or neural networks. There wasn't any way to verify them at the time. I've seen a few attempts at such things but would need to know what kind of algorithm you use for sense, learn, and act (or whatever they call it). No guarantees here.