Relational STE and theorem proving for formal verification of industrial circuit designs

Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic tra...

Full description

Bibliographic Details
Main Authors: O'Leary, J, Kaivola, R, Melham, T
Format: Conference item
Published: 2013