I have completed my thesis on synchronous trace theory:
Synchronous trace theory provides a trace-theoretical (behavioral) model of combinational and sequential, synchronous circuitry which supports formal hierarchical verification and replacement. Some of the most interesting problems we encountered in developing this theory appear in modeling purely combinational hardware. A summary of the relevant problems and our solution appears in the second publication listed below. My thesis incorporates both the combinational and the sequential theories.
In 1991, I participated in a formal verification project at Hewlett-Packard. The results of that project are documented in the first publication below. A more detailed version of that publication, from which fewer proprietary hardware details were deleted, appeared in the Hewlett-Packard internal Design Technology Conference in 1992, where it won Best Paper award in the "Simulation and Modeling" session.
Abstract: We report on our investigation of a new verification tool, the Symbolic Model Verifier (SMV), created at Carnegie-Mellon University. We have successfully employed this tool to detect deadlock in an industrial design, namely, Hewlett-Packard's Summit bus converter chips. In addition to locating a known deadlock in the original chip design and checking its solution, we successfully detected other previously unknown defects in the design. In our experiments, we were able to verify properties on finite-state models of the circuit with 150 to 200 state variables in a matter of minutes.
Abstract: Hierarchical descriptions of combinational circuits often contain apparent loops. Since it may be difficult to distinguish apparent loops from actual loops, it is useful to construct models of combinational circuits that can handle cyclic dependencies. We show that Boolean relations are inadequate for this purpose, and define a ternary model that solves the problem. We use the model to characterize exact solutions to a broad class of substitution and rectification problems. The theory cleanly handles network transformations that might introduce cyclic dependencies.