Dear Dwi,
This is classic HOL stuff - see this old
paper<https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf> or my
thesis<http://dx.doi.org/10.1017/CBO9780511569845>.
I suspect that floating-point verification directly in HOL, at least for
circuits of any size, will be quite challenging. However, David
Russinoff<http://dblp.org/pid/53/70> does this kind of thing quite regularly in
ACL2, so it’s certainly possible.
All best regards,
Tom
On 23/07/2016, 05:01, "dwi.teguh51"
<dwi.tegu...@ui.ac.id<mailto:dwi.tegu...@ui.ac.id>> wrote:
Dear all,
Hi, I'm Dwi, a newbie in HOL
Now I'm still learning and exploring hardware verification especially
about floating point for my master thesis.
I want to try the verification at the gate level. Is anyone ever tried
to specify or modeling the basic logic gates (AND, OR, NOT, etc.) in HOL
or HOL Light? Is there any related library I can explore?
Thank you.
Best Regards,
Dwi
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
