Email Gateway (Aug 18 2022 at 20:29): Email Gateway (Aug 18 2022 at 20:29):From: Konrad Slind <konrad.slind@gmail.com>
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.
Email Gateway (Aug 18 2022 at 20:32):From: li yongjian <lyj238@gmail.com>
In ~/src/HOL/Datatype_Benchmark, there is a verilog.thy.
Who write it?
Is there any parser which transforms verilog code to such a datatype?
Email Gateway (Aug 19 2022 at 08:12):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 23 2024 at 12:29 UTC