Quote: prove microcode program via an APL-like symbolic simulation on bit arrays; symbolic theorems and tests matched to actual

Note

prove microcode by building symbolic simulation in an APL like language based on bit arrays, then proving theorems about symbolic simulation against the actual bit array describing the microcode. i.e. execute the specifications and execute the low level instructions and see if they match. some thing like that anyway

Related Topics

Group: program proving   (10 topics, 310 quotes)