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

Application Systems

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 2

Computer Systems and Engineering

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.