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.

Konrad.

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.
>
>
>         Makarius
>





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