Operational Semantics Based Formal Symbolic Simulation

This paper describes the development of progressively more powerful and abstract hardware simulators. A small computer hardware design and description language pico- ella is then introduced, followed by its formal semantics. Using a number of small examples, we will then show the how this formal semantics may be used within a proof system as a sophisticated simulation tool. Examples include some full adders, a general N bit adder, and two parity checkers