next up previous
Next: A Synthesis Session Up: MINIMALIST Tools Previous: Synthesis-for-Testability

Verifier

MINIMALIST features a simple tool to verify that a given logic implementation (produced by any method) realizes the specified burst-mode behaviour, independent of the particular state merges or encoding which have been performed. The verifier simulates the implementation's response to each specified input burst, and compares it to the specification; any mismatches of output or state at the end of the burst and any logic hazards are reported. Although each burst is considered only once, the analysis that is performed accounts for all possible interleavings of individual input changes. Since the verifier needs to traverse each edge in the specification's state graph only once, this tool is eminently practical even for very large specifications -- the time required is never more than a few seconds. Currently, verification of only two-level AND/OR implementations is provided. However, the framework allows for verification of multi-level implementations as well (using the 9-valued algebra developed by Kung [13]), which will be completely supported in the near future. Also, the current version of the verifier does not detect output changes made after partial input bursts. Finally, being a purely combinational verifier, it does not verify the one-sided timing constraints also needed to ensure correct operation [1]. Such a capability may be added in a future release.


next up previous
Next: A Synthesis Session Up: MINIMALIST Tools Previous: Synthesis-for-Testability
Steven Nowick
1999-07-28