Automatic generation of Chu space model expressions for verification

We present an algorithm for automatic generation of behavioral models of non-iterated systems from a structural Verilog specification. The models are represented as Chu spaces over the set of system events, and are used for verifying system behavior. The correctness and time complexity of the presented algorithm are briefly discussed along with a small example.