We propose a model for modular synchronous systems
with combinational dependencies and define consistency using this
model. We then show how to derive this model from a modular
specification where individual modules are specified as Kripke
Structures and give an algorithm to check the system for
consistency. We have implemented this algorithm symbolically using
BDDs in a tool, SpecCheck. We have used this tool to check an example bus protocol
derived from an industrial specification. The counterexamples obtained
for this protocol highlight the need for consistency checking.
