About books/projects/arm/second/fsqrt4/fsqrt4.cpp proof using ACL2

[whitecloudsun]

After I read the book of Formal Verification of Floating Point Hardware Design, I haven't found any information about how to use proof scripts in the books/projects/arm/second/fsqrt4/ directory to complete prove process with ACL2。

After converting CModel into ACL2 script, are you sure that ACL2 can be used to complete the proof？Are there any operational guidelines that can be provided？

I hope to receive your reply as soon as possible. Thank you very much！

[russinoff]

The proof script in that directory may be certified in the same way in which all scripts in the books directory are certified, by following the instructions on the ACL2 Web site. See https://www.cs.utexas.edu/users/moore/acl2/v8-5/HTML/installation/using.html#Certifying

…

On Wed, Sep 13, 2023 at 1:38 AM whitecloudsun ***@***.***> wrote: After I read the book of Formal Verification of Floating Point Hardware Design, I haven't found any information about how to use proof scripts in the books/projects/arm/second/fsqrt4/ directory to complete prove process with ACL2。 After converting CModel into ACL2 script, are you sure that ACL2 can be used to complete the proof？Are there any operational guidelines that can be provided？ I hope to receive your reply as soon as possible. Thank you very much！ — Reply to this email directly, view it on GitHub <#1539>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADFJGSJB4LDJJB4BY36ZIYTX2FBGPANCNFSM6AAAAAA4V25UBE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[whitecloudsun]

Thank you for your friendly answer。I run the projects/arm/second/fsqrt4/fsqrt4.lisp in the same way as running the projects/rp-rewriter/lib/mult3/demo/demo-2.lisp，but for statement of IN-PACKAGE "RTL" in scripts, an error that is unrecognized package names RTL will be reported, what should I do to resolve this error?

I hope to receive your reply as soon as possible. Thank you very much！

[ericwhitmansmith]

Hi, Try standing in the directory books/projects/arm/second/fsqrt4/ and doing:
(ld "rtl/rel11/package.lsp" :dir :system)
(ld "fsqrt4.lisp")
If the directory is certified, the first of those 2 commands can be replaced by (ld "fsqrt4.port").

[whitecloudsun]

Hi，ericwhitmansmith，may I ask if adding --load package.lsp during the CCL lx86cl64 execution ? it did not seem to have any effect, unrecognized RTL package error still reported.

[ericwhitmansmith]

Hi, I don't know, but using --load doesn't sound like the kind of thing ACL2 users commonly do. To clarify my answer above, you should submit the two ld commands above to ACL2, not Common Lisp.

[whitecloudsun]

Can I ask how to submit two ld commands to acl2 and what are the specific steps？I have execute that make -j 2 rtl in the directory of books and generate corresponding .cert and .out file，otherwise，fsqrt4. port has been generated by executing cert.pl -acl2 $path/saved fsqrt4.lisp in the fsqrt4 directory_ Generated by acl2, then I execute that ccl/lx86cl64 fsqrt4.lisp with -I 、-K、 -e options，and reported unrecognized "RTL" package error.

May I ask if there are any issues with my execution method, or if there are any steps that I have missed? Could you please help me point them out?

I hope to receive your reply as soon as possible. Thank you very much！

[whitecloudsun]

Now, “RTL” package has been recognized, I did it according to the following steps，
1、write run_fsqrt4.lisp
(ld "path/to/rtl/package.lsp")
(ld "path/to/a.lisp")
2、saved_acl2 < run-fsqrt4.lisp

Thank you for your patient guidance！

[solswords]

I think ACL2 users typically are in one of two modes: - interactive development: run saved_acl2 without arguments and type/submit forms at the prompt - batch book certification, using cert.pl or makefiles based on it (e.g. bools/GNUmakefile). I think we aren't clear on which one you want. It looks like you've certified fsqrt4.lisp, so that means you've run all the events in that book and the proofs were completed successfully (you can look at fsqrt4.cert.out to see the output). If you want to run the events in the book interactively, that's where you might need to submit those two LD commands that Eric mentioned. But it might be that the package problems you were seeing before were because books weren't certified, and now that they are those problems might go away.

…

On Fri, Sep 15, 2023 at 4:29 AM whitecloudsun ***@***.***> wrote: Now, “RTL” package has been recognized, I did it according to the following steps， 1、write run_fsqrt4.lisp (ld "path/to/rtl/package.lsp") (ld "path/to/a.lisp") 2、saved_acl2 < run-fsqrt4.lisp Thank you for your patient guidance！ — Reply to this email directly, view it on GitHub <#1539 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABJLGKJ77DMPV42ZZII3GI3X2QNXLANCNFSM6AAAAAA4V25UBE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>