Many thanks. Actually, I have changed the definition from predicate format to a function format to avoid existentials on wires and registers and conjunctions and also to make it testable using EVAL. Instead, I have used "let in" structure and the whole design which is a tranlation from Verilog to HOL looks like the following:
val Design = Define `Design input t = let wire = \t. f1 (input (t)) in let register = \t. f2 (input (t),wire (t)) in let output = \t. f3 (input (t),wire (t), register (t)) in output (t)`; there are many "let in" lines like above collected from different relating files and this makes the final flat design very huge. I have used Anthony's new words theory in HOL to represent the signals in RTL level. So, most of the expressions and signals have the type :'a word. One option is to focus on smaller sub-blocks and modules instead of defining the whole design at once. Is there any other way to simplify this structure using term constructors? Thanks, Behzad On Sep 17 2009, Konrad Slind wrote: >Hi Behzad, > > A 6000 line term is probably making the parser and/or >type inferencer work very hard. It might be better to >build the term using term constructors such as >mk_neg, mk_conj, mk_disj, mk_exists, etc. > >Cheers, >Konrad. > >On Sep 16, 2009, at 6:56 PM, Behzad Akbarpour wrote: > >> Hi everyone; >> >> 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. I first tried to copy and paste from emacs but it didn't >> work. >> Then, I made a script file out of the definition together with the >> related >> theories but Holmake didn't generate the theory file at the end after >> taking lots of time. I even tried Magnus and Michael's script for >> interaction with HOL via emacs/xemacs using C-space and M-h M-r >> keys, but >> it didn't work either. Do you have any idea how to solve this problem? >> >> Thanks, >> >> Behzad >> >> >> ---------------------------------------------------------------------- >> -------- >> 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 > > ------------------------------------------------------------------------------ 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
