The CRITTER System: Analyzing Digital Circuits by Propagating Behaviors and Specifications

Van E. Kelly, Louis I. Steinberg

CRITTER is a system that reasons about digital hardware designs, using a a declarative representation that can represent components and signals at arbitrary levels of abstraction. CRITTER can derive the behaviors of a component’s outputs given the behaviors of the inputs. It can derive the specifications a component’s inputs must meet in order for some given specifications on the outputs to be met, and it can verify that a given signal behavior satisfies a given specification. By combining these operations, it evaluates both the correctness and the robustness of the overall design.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.