Re: [isabelle] verilog.thy
As I recall, Daryl constructed an enormous HOL datatype capturing
part of the grammar of Verilog. It got collected into a regression suite
by John Harrison when he was building his datatype package. Presumably,
that regression suite was later used to test Isabelle's datatype package.
On Mon, Jul 16, 2012 at 7:54 AM, Makarius <makarius at sketis.net> wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and