On Thursday 17 September 2009 01:56:41 Behzad Akbarpour wrote: >I have a huge definition of an RTL design function (more that 6000 lines of >HOL code), and I'm trying to load and compile it in HOL, but I couldn't >succeed. ... > Do you have any idea how to solve this problem?
Back in 1988 we verified a hardware device using HOL by importing the netlist generated from the tool used to design the hardware. What we found to be the most significant problem at our first attempt was the types of the resulting terms. We used a functional representation for hardware blocks and the domain of the function was the product of the types of the signals going into the block. The resulting types were so complex that the HOL type checker took forever. We fixed this problem by using lists instead of products. Presumably all the performace characteristics are completely different these days. but the possibility remains that your problem might be connected with the types which are covertly generated by your spec. Roger Jones ------------------------------------------------------------------------------ Come build with us! The BlackBerry® Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9-12, 2009. Register now! http://p.sf.net/sfu/devconf _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
