Compiling Verilog into Timed Finite State Machines

	Szu-Tsung Cheng, Robert Brayton, Gary York, 
	 Katherine Yelick, and Alexander Saldanha

The lack of formal semantics for HDLs has made it hard to make a
formal bridge between simulation tools based on HDLs and
synthesis/verification tools based on finite state machines.  In this
paper we address the problem of finding a larger subset of Verilog HDL
(which includes timing constructs) and a systematic way of extracting
FSMs from programs built using the subset.  Using timed FSMs as the
target language for HDL compilation gives us two potntial advantages.
First, FSMs can be used to model systems that do not have a hardware
implementation.  Second, FSMs can be used to model systems that are
implementable but not automatically synthesizable.