About the series
Hundred million-gate ASICs are possible by the end of the decade. However, numerous problems related to process technology and design need to be solved before such large chips will become commonplace. Computer scientists are much better equipped to solve problems related to the design-in-the-large. Bluespec is a language/methodology that promotes correctness-by-construction. Its underlying execution model is based on atomic actions on state elements (such as flip-flops, registers, ...), i.e., any legal behavior is explainable in a terms of a sequence of atomic actions on the state. Expressiveness of Bluespec is achieved by keeping its static semantics orthogonal to its hardware execution semantics -- the source program is turned into a flat interconnection of modules by "static elaboration" during the compile phase. This talk will present Bluespec via examples and show some of the designs done so far.