Re: [isabelle] verilog.thy



On Tue, 3 Jul 2012, li yongjian wrote:

In ~/src/HOL/Datatype_Benchmark, there is a verilog.thy.
Who write it?

The source file mentions "Daryl", which probably means Daryl Stewart, and points back to some Verilog/HOL project at Cambridge in the mid 1990-ies. These files have been converted to Isabelle/HOL from HOL files by Konrad Slind and/or John Harrison from many years ago.


Is there any parser which transforms verilog code to such a datatype?

You can try yourself to google for Verilog parsers, and then make a little converter into Isabelle/ML term structure, for example.


The datatype benchmark above is really just a benchmark. These Verilog datatype definitions are far too concrete and redundant to be of any use in Isabelle/HOL. Every function you define over it and every induction proof you do would have to mention these all these constructors and arguments.

A more realistic formalization would somehow group and nest language elements, to avoid excessive breadth of the type definition.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.