From e043d3bd21e9a0ebd37b8ac2ca262ed630a5b192 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 25 Feb 2022 10:10:43 +0000 Subject: Add back pure documentation --- docs/README.org | 7 + docs/common.org | 13 ++ docs/documentation.org | 557 +++++++++++++++++++++++++++++++++++++++++++++++++ docs/fdl.org | 489 +++++++++++++++++++++++++++++++++++++++++++ docs/man.org | 36 ++++ 5 files changed, 1102 insertions(+) create mode 100644 docs/README.org create mode 100644 docs/common.org create mode 100644 docs/documentation.org create mode 100644 docs/fdl.org create mode 100644 docs/man.org (limited to 'docs') diff --git a/docs/README.org b/docs/README.org new file mode 100644 index 0000000..4113ed9 --- /dev/null +++ b/docs/README.org @@ -0,0 +1,7 @@ +#+title: Vericert Documentation + +The documentation for [[https://github.com/ymherklotz/vericert][Vericert]], which is written in the [[/documentation.org][documentation.org]] file. + +* How to develop on documentation + +The documentation uses =hugo= to generate the website, diff --git a/docs/common.org b/docs/common.org new file mode 100644 index 0000000..8c39be0 --- /dev/null +++ b/docs/common.org @@ -0,0 +1,13 @@ +#+author: Yann Herklotz +#+email: git@ymhg.org + +#+macro: version 1.2.2 +#+macro: modified 2022-02-24 + +#+macro: link src_emacs-lisp[:results raw]{(ymhg/link "$1" "$2")} + +#+macro: texinfo_head (eval (if (eq org-export-current-backend 'texinfo) "#+exclude_tags: noexport_texinfo" "#+exclude_tags: onlyexport_texinfo")) +#+macro: latex_head (eval (if (eq org-export-current-backend 'latex) "#+exclude_tags: noexport_latex" "#+exclude_tags: onlyexport_latex")) +#+macro: hugo_head (eval (if (eq org-export-current-backend 'hugo) "#+exclude_tags: noexport_hugo" "#+exclude_tags: onlyexport_hugo")) +{{{texinfo_head}}} +{{{latex_head}}} diff --git a/docs/documentation.org b/docs/documentation.org new file mode 100644 index 0000000..d4ef799 --- /dev/null +++ b/docs/documentation.org @@ -0,0 +1,557 @@ +#+title: Vericert Manual +#+subtitle: Release {{{version}}} +#+author: Yann Herklotz +#+email: git@ymhg.org +#+language: en + +* Docs +:PROPERTIES: +:EXPORT_FILE_NAME: _index +:EXPORT_HUGO_SECTION: docs +:CUSTOM_ID: docs +:END: + +Vericert translates C code into a hardware description language called Verilog, which can then be +synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or +application-specific integrated circuit (ASIC). + +#+attr_html: :width 600 +#+caption: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language. +#+name: fig:design +[[/images/toolflow.svg]] + +The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler +called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation. + +#+texinfo: @insertcopying + +* COPYING +:PROPERTIES: +:COPYING: t +:END: + +Copyright (C) 2019-2022 Yann Herklotz. + +#+begin_quote +Permission is granted to copy, distribute and/or modify this document +under the terms of the GNU Free Documentation License, Version 1.3 +or any later version published by the Free Software Foundation; +with no Invariant Sections, no Front-Cover Texts, and no Back-Cover +Texts. A copy of the license is included in the section entitled ``GNU +Free Documentation License''. +#+end_quote + +* Building Vericert +:PROPERTIES: +:EXPORT_FILE_NAME: building +:EXPORT_HUGO_SECTION: docs +:CUSTOM_ID: building +:END: + +#+transclude: [[file:~/projects/vericert/README.org::#building][file:~/projects/vericert/README.org::#building]] :only-contents :exclude-elements "headline property-drawer" +#+transclude: [[file:~/projects/vericert/README.org::#downloading-compcert][file:~/projects/vericert/README.org::#downloading-compcert]] +#+transclude: [[file:~/projects/vericert/README.org::#setting-up-nix][file:~/projects/vericert/README.org::#setting-up-nix]] +#+transclude: [[file:~/projects/vericert/README.org::#makefile-build][file:~/projects/vericert/README.org::#makefile-build]] + +** Testing + +To test out ~vericert~ you can try the following examples which are in the test folder using the +following: + +#+begin_src shell +./bin/vericert test/loop.c -o loop.v +./bin/vericert test/conditional.c -o conditional.v +./bin/vericert test/add.c -o add.v +#+end_src + +Or by running the test suite using the following command: + +#+begin_src shell +make test +#+end_src + +* Using Vericert +:PROPERTIES: +:CUSTOM_ID: using-vericert +:END: + +Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the +following C file (~main.c~): + +#+begin_src C +void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { + int sum = 0; + for (int c = 0; c < 2; c++) { + for (int d = 0; d < 2; d++) { + for (int k = 0; k < 2; k++) { + sum = sum + first[c][k]*second[k][d]; + } + multiply[c][d] = sum; + sum = 0; + } + } +} + +int main() { + int f[2][2] = {{1, 2}, {3, 4}}; + int s[2][2] = {{5, 6}, {7, 8}}; + int m[2][2] = {{0, 0}, {0, 0}}; + + matrix_multiply(f, s, m); + return m[1][1]; +} +#+end_src + +It can be compiled using the following command, assuming that vericert is somewhere on the path. + +#+begin_src shell +vericert main.c -o main.v +#+end_src + +The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to +simulate the hardware, which should give the same result as executing the C code. Using [[http://iverilog.icarus.com/][Icarus +Verilog]] as an example: + +#+begin_src shell +iverilog -o main_v main.v +#+end_src + +When executing, it should therefore print the following: + +#+begin_src shell +$ ./main_v +finished: 50 +#+end_src + +This gives the same result as executing the C in the following way: + +#+begin_src shell +$ gcc -o main_c main.c +$ ./main_c +$ echo $? +50 +#+end_src + +* Unreleased Features +:PROPERTIES: +:EXPORT_FILE_NAME: unreleased +:EXPORT_HUGO_SECTION: docs +:CUSTOM_ID: unreleased-features +:END: + +The following are unreleased features in Vericert that are currently being worked on and have not +been completely proven correct yet. Currently this includes features such as: + +- [[#scheduling][scheduling]], +- [[#operation-chaining][operation chaining]], +- [[#if-conversion][if-conversion]], and +- [[#functions][functions]]. + +This page gives some preliminary information on how the features are implemented and how the proofs +for the features are being done. Once these features are properly implemented, they will be added +to the proper documentation. + +** Scheduling +:PROPERTIES: +:CUSTOM_ID: scheduling +:END: + +Scheduling is an optimisation which is used to run various instructions in parallel that are +independent to each other. + +** Operation Chaining +:PROPERTIES: +:CUSTOM_ID: operation-chaining +:END: + +Operation chaining is an optimisation that can be added on to scheduling and allows for the +sequential execution of instructions in a clock cycle, while executing other instructions in +parallel in the same clock cycle. + +** If-conversion +:PROPERTIES: +:CUSTOM_ID: if-conversion +:END: + +If-conversion is an optimisation which can turn code with simple control flow into a single block +(called a hyper-block), using predicated instructions. + +** Functions +:PROPERTIES: +:CUSTOM_ID: functions +:END: + +Functions are currently only inlined in Vericert, however, we are working on a proper interface to +integrate function calls into the hardware. + +* Coq Style Guide + :PROPERTIES: + :CUSTOM_ID: coq-style-guide + :EXPORT_FILE_NAME: coq-style-guide + :EXPORT_HUGO_SECTION: docs + :END: + +This style guide was taken from [[https://github.com/project-oak/silveroak][Silveroak]], it outlines code style for Coq code in this +repository. There are certainly other valid strategies and opinions on Coq code style; this is laid +out purely in the name of consistency. For a visual example of the style, see the [[#example][example]] at the +bottom of this file. + +** Code organization + :PROPERTIES: + :CUSTOM_ID: code-organization + :END: +*** Legal banner + :PROPERTIES: + :CUSTOM_ID: legal-banner + :END: + +- Files should begin with a copyright/license banner, as shown in the example above. + +*** Import statements + :PROPERTIES: + :CUSTOM_ID: import-statements + :END: + +- =Require Import= statements should all go at the top of the file, followed by file-wide =Import= + statements. + + - =Import=s often contain notations or typeclass instances that might override notations or + instances from another library, so it's nice to highlight them separately. + +- One =Require Import= statement per line; it's easier to scan that way. +- =Require Import= statements should use "fully-qualified" names (e.g. =Require Import + Coq.ZArith.ZArith= instead of =Require Import ZArith=). + + - Use the =Locate= command to find the fully-qualified name! + +- =Require Import='s should go in the following order: + + 1. Standard library dependencies (start with =Coq.=) + 2. External dependencies (anything outside the current project) + 3. Same-project dependencies + +- =Require Import='s with the same root library (the name before the first =.=) should be grouped + together. Within each root-library group, they should be in alphabetical order (so =Coq.Lists.List= + before =Coq.ZArith.ZArith=). + +*** Notations and scopes + :PROPERTIES: + :CUSTOM_ID: notations-and-scopes + :END: + +- Any file-wide =Local Open Scope='s should come immediately after the =Import=s (see example). + + - Always use =Local Open Scope=; just =Open Scope= will sneakily open the scope for those who import + your file. + +- Put notations in their own separate modules or files, so that those who import your file can + choose whether or not they want the notations. + + - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this + flexibility! + +** Formatting + :PROPERTIES: + :CUSTOM_ID: formatting + :END: +*** Line length + :PROPERTIES: + :CUSTOM_ID: line-length + :END: + +- Maximum line length 80 characters. + + - Many Coq IDE setups divide the screen in half vertically and use only half to display source + code, so more than 80 characters can be genuinely hard to read on a laptop. + +*** Whitespace and indentation + :PROPERTIES: + :CUSTOM_ID: whitespace-and-indentation + :END: + +- No trailing whitespace. + +- Spaces, not tabs. + +- Files should end with a newline. + + - Many editors do this automatically on save. + +- Colons may be either "English-spaced", with no space before the colon and one space after (=x: nat=) + or "French-spaced", with one space before and after (=x : nat=). + +- Default indentation is 2 spaces. + + - Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE + defaults. + +- Use 2-space indents if inserting a line break immediately after: + + - =Proof.= + - =fun <...> =>= + - =forall <...>,= + - =exists <....>,= + +- The style for indenting arguments in function application depends on where you make a line + break. If you make the line break immediately after the function name, use a 2-space + indent. However, if you make it after one or more arguments, align the next line with the first + argument: + + #+begin_src coq + (Z.pow + 1 2) + (Z.pow 1 2 3 + 4 5 6) + #+end_src + +- =Inductive= cases should not be indented. Example: + + #+begin_src coq + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo + . + #+end_src + +- =match= or =lazymatch= cases should line up with the "m" in =match= or "l" in =lazymatch=, as in the + following examples: + + #+begin_src coq + match x with + | 3 => true + | _ => false + end. + + lazymatch x with + | 3 => idtac + | _ => fail "Not equal to 3:" x + end. + + repeat match goal with + | _ => progress subst + | _ => reflexivity + end. + + do 2 lazymatch goal with + | |- context [eq] => idtac + end. + #+end_src + +** Definitions and Fixpoints + :PROPERTIES: + :CUSTOM_ID: definitions-and-fixpoints + :END: + +- It's okay to leave the return type of =Definition='s and =Fixpoint='s implicit (e.g. ~Definition x := 5~ + instead of ~Definition x : nat := 5~) when the type is very simple or obvious (for instance, the + definition is in a file which deals exclusively with operations on =Z=). + +** Inductives + :PROPERTIES: + :CUSTOM_ID: inductives + :END: + +- The =.= ending an =Inductive= can be either on the same line as the last case or on its own line + immediately below. That is, both of the following are acceptable: + + #+begin_src coq + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo + . + Inductive Foo : Type := + | FooA : Foo + | FooB : Foo. + #+end_src + +** Lemma/Theorem statements + :PROPERTIES: + :CUSTOM_ID: lemmatheorem-statements + :END: + +- Generally, use =Theorem= for the most important, top-level facts you prove and =Lemma= for everything + else. +- Insert a line break after the colon in the lemma statement. +- Insert a line break after the comma for =forall= or =exist= quantifiers. +- Implication arrows (=->=) should share a line with the previous hypothesis, not the following one. +- There is no need to make a line break after every =->=; short preconditions may share a line. + +** Proofs and tactics + :PROPERTIES: + :CUSTOM_ID: proofs-and-tactics + :END: + +- Use the =Proof= command (lined up vertically with =Lemma= or =Theorem= it corresponds to) to open a + proof, and indent the first line after it 2 spaces. + +- Very small proofs (where =Proof. Qed.= is <= 80 characters) can go all in one line. + +- When ending a proof, align the ending statement (=Qed=, =Admitted=, etc.) with =Proof=. + +- Avoid referring to autogenerated names (e.g. =H0=, =n0=). It's okay to let Coq generate these names, + but you should not explicitly refer to them in your proof. So =intros; my_solver= is fine, but + =intros; apply H1; my_solver= is not fine. + + - You can force a non-autogenerated name by either putting the variable before the colon in the + lemma statement (=Lemma foo x : ...= instead of =Lemma foo : forall x, ...=), or by passing + arguments to =intros= (e.g. =intros ? x= to name the second argument =x=) + +- This way, the proof won't break when new hypotheses are added or autogenerated variable names + change. + +- Use curly braces ={}= for subgoals, instead of bullets. + +- /Never write tactics with more than one subgoal focused./ This can make the proof very confusing to + step through! If you have more than one subgoal, use curly braces. + +- Consider adding a comment after the opening curly brace that explains what case you're in (see + example). + + - This is not necessary for small subgoals but can help show the major lines of reasoning in large + proofs. + +- If invoking a tactic that is expected to return multiple subgoals, use =[ | ... | ]= before the =.= to + explicitly specify how many subgoals you expect. + + - Examples: =split; [ | ].= =induction z; [ | | ].= + - This helps make code more maintainable, because it fails immediately if your tactic no longer + solves as many subgoals as expected (or unexpectedly solves more). + +- If invoking a string of tactics (composed by =;=) that will break the goal into multiple subgoals + and then solve all but one, still use =[ ]= to enforce that all but one goal is solved. + + - Example: =split; try lia; [ ]=. + +- Tactics that consist only of =repeat=-ing a procedure (e.g. =repeat match=, =repeat first=) should + factor out a single step of that procedure a separate tactic called =_step=, because + the single-step version is much easier to debug. For instance: + + #+begin_src coq + Ltac crush_step := + match goal with + | _ => progress subst + | _ => reflexivity + end. + Ltac crush := repeat crush_step. + #+end_src + +** Naming + :PROPERTIES: + :CUSTOM_ID: naming + :END: + +- Helper proofs about standard library datatypes should go in a module that is named to match the + standard library module (see example). + + - This makes the helper proofs look like standard-library ones, which is helpful for categorizing + them if they're genuinely at the standard-library level of abstraction. + +- Names of modules should start with capital letters. +- Names of inductives and their constructors should start with capital letters. +- Names of other definitions/lemmas should be snake case. + +** Example + :PROPERTIES: + :CUSTOM_ID: example + :END: +A small standalone Coq file that exhibits many of the style points. + +#+begin_src coq +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 Name + * + * + *) + + Require Import Coq.Lists.List. + Require Import Coq.micromega.Lia. + Require Import Coq.ZArith.ZArith. + Import ListNotations. + Local Open Scope Z_scope. + + (* Helper proofs about standard library integers (Z) go within [Module Z] so + that they match standard-library Z lemmas when used. *) + Module Z. + Lemma pow_3_r x : x ^ 3 = x * x * x. + Proof. lia. Qed. (* very short proofs can go all on one line *) + + Lemma pow_4_r x : x ^ 4 = x * x * x * x. + Proof. + change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))). + repeat match goal with + | _ => rewrite Z.pow_1_r + | _ => rewrite Z.pow_succ_r by lia + | |- context [x * (?a * ?b)] => + replace (x * (a * b)) with (a * b * x) by lia + | _ => reflexivity + end. + Qed. + End Z. + (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they + were in the ZArith library! *) + + Definition bar (x y : Z) := x ^ (y + 1). + + (* example with a painfully manual proof to show case formatting *) + Lemma bar_upper_bound : + forall x y a, + 0 <= x <= a -> 0 <= y -> + 0 <= bar x y <= a ^ (y + 1). + Proof. + (* avoid referencing autogenerated names by explicitly naming variables *) + intros x y a Hx Hy. revert y Hy x a Hx. + (* explicitly indicate # subgoals with [ | ... | ] if > 1 *) + cbv [bar]; refine (natlike_ind _ _ _); [ | ]. + { (* y = 0 *) + intros; lia. } + { (* y = Z.succ _ *) + intros. + rewrite Z.add_succ_l, Z.pow_succ_r by lia. + split. + { (* 0 <= bar x y *) + apply Z.mul_nonneg_nonneg; [ lia | ]. + apply Z.pow_nonneg; lia. } + { (* bar x y < a ^ y *) + rewrite Z.pow_succ_r by lia. + apply Z.mul_le_mono_nonneg; try lia; + [ apply Z.pow_nonneg; lia | ]. + (* For more flexible proofs, use match statements to find hypotheses + rather than referring to them by autogenerated names like H0. In this + case, we'll take any hypothesis that applies to and then solves the + goal. *) + match goal with H : _ |- _ => apply H; solve [auto] end. } } + Qed. + + (* Put notations in a separate module or file so that importers can + decide whether or not to use them. *) + Module BarNotations. + Infix "#" := bar (at level 40) : Z_scope. + Notation "x '##'" := (bar x x) (at level 40) : Z_scope. + End BarNotations. +#+end_src + +* Index - Features +:PROPERTIES: +:CUSTOM_ID: cindex +:APPENDIX: t +:INDEX: cp +:DESCRIPTION: Key concepts & features +:END: + +* Export Setup :noexport: + +#+setupfile: common.org + +#+export_file_name: vericert.texi + +#+texinfo_dir_category: High-level synthesis tool +#+texinfo_dir_title: Vericert +#+texinfo_dir_desc: Formally verified high-level synthesis tool + +* GNU Free Documentation License +:PROPERTIES: +:appendix: t +:END: + +#+include: fdl.org diff --git a/docs/fdl.org b/docs/fdl.org new file mode 100644 index 0000000..81e2cd9 --- /dev/null +++ b/docs/fdl.org @@ -0,0 +1,489 @@ +# The GNU Free Documentation License. +#+begin_center +Version 1.3, 3 November 2008 +#+end_center + +# This file is intended to be included within another document. + +#+begin_verse +Copyright \copy{} 2000, 2001, 2002, 2007, 2008 Free Software Foundation, Inc. +https://fsf.org/ + +Everyone is permitted to copy and distribute verbatim copies +of this license document, but changing it is not allowed. +#+end_verse + +0. [@0] PREAMBLE + + The purpose of this License is to make a manual, textbook, or other + functional and useful document @@texinfo:@dfn{@@free@@texinfo:}@@ + in the sense of freedom: to assure everyone the effective freedom + to copy and redistribute it, with or without modifying it, either + commercially or noncommercially. Secondarily, this License + preserves for the author and publisher a way to get credit for + their work, while not being considered responsible for + modifications made by others. + + This License is a kind of "copyleft", which means that derivative + works of the document must themselves be free in the same sense. + It complements the GNU General Public License, which is a copyleft + license designed for free software. + + We have designed this License in order to use it for manuals for + free software, because free software needs free documentation: + a free program should come with manuals providing the same freedoms + that the software does. But this License is not limited to + software manuals; it can be used for any textual work, regardless + of subject matter or whether it is published as a printed book. We + recommend this License principally for works whose purpose is + instruction or reference. + +1. APPLICABILITY AND DEFINITIONS + + This License applies to any manual or other work, in any medium, + that contains a notice placed by the copyright holder saying it can + be distributed under the terms of this License. Such a notice + grants a world-wide, royalty-free license, unlimited in duration, + to use that work under the conditions stated herein. The + "Document", below, refers to any such manual or work. Any member + of the public is a licensee, and is addressed as "you". You accept + the license if you copy, modify or distribute the work in a way + requiring permission under copyright law. + + A "Modified Version" of the Document means any work containing the + Document or a portion of it, either copied verbatim, or with + modifications and/or translated into another language. + + A "Secondary Section" is a named appendix or a front-matter section + of the Document that deals exclusively with the relationship of the + publishers or authors of the Document to the Document's overall + subject (or to related matters) and contains nothing that could + fall directly within that overall subject. (Thus, if the Document + is in part a textbook of mathematics, a Secondary Section may not + explain any mathematics.) The relationship could be a matter of + historical connection with the subject or with related matters, or + of legal, commercial, philosophical, ethical or political position + regarding them. + + The "Invariant Sections" are certain Secondary Sections whose + titles are designated, as being those of Invariant Sections, in the + notice that says that the Document is released under this License. + If a section does not fit the above definition of Secondary then it + is not allowed to be designated as Invariant. The Document may + contain zero Invariant Sections. If the Document does not identify + any Invariant Sections then there are none. + + The "Cover Texts" are certain short passages of text that are + listed, as Front-Cover Texts or Back-Cover Texts, in the notice + that says that the Document is released under this License. + A Front-Cover Text may be at most 5 words, and a Back-Cover Text + may be at most 25 words. + + A "Transparent" copy of the Document means a machine-readable copy, + represented in a format whose specification is available to the + general public, that is suitable for revising the document + straightforwardly with generic text editors or (for images composed + of pixels) generic paint programs or (for drawings) some widely + available drawing editor, and that is suitable for input to text + formatters or for automatic translation to a variety of formats + suitable for input to text formatters. A copy made in an otherwise + Transparent file format whose markup, or absence of markup, has + been arranged to thwart or discourage subsequent modification by + readers is not Transparent. An image format is not Transparent if + used for any substantial amount of text. A copy that is not + "Transparent" is called "Opaque". + + Examples of suitable formats for Transparent copies include plain + ASCII without markup, Texinfo input format, LaTeX input format, + SGML or XML using a publicly available DTD, and standard-conforming + simple HTML, PostScript or PDF designed for human modification. + Examples of transparent image formats include PNG, XCF and JPG. + Opaque formats include proprietary formats that can be read and + edited only by proprietary word processors, SGML or XML for which + the DTD and/or processing tools are not generally available, and + the machine-generated HTML, PostScript or PDF produced by some word + processors for output purposes only. + + The "Title Page" means, for a printed book, the title page itself, + plus such following pages as are needed to hold, legibly, the + material this License requires to appear in the title page. For + works in formats which do not have any title page as such, "Title + Page" means the text near the most prominent appearance of the + work's title, preceding the beginning of the body of the text. + + The "publisher" means any person or entity that distributes copies + of the Document to the public. + + A section "Entitled XYZ" means a named subunit of the Document + whose title either is precisely XYZ or contains XYZ in parentheses + following text that translates XYZ in another language. (Here XYZ + stands for a specific section name mentioned below, such as + "Acknowledgements", "Dedications", "Endorsements", or "History".) + To "Preserve the Title" of such a section when you modify the + Document means that it remains a section "Entitled XYZ" according + to this definition. + + The Document may include Warranty Disclaimers next to the notice + which states that this License applies to the Document. These + Warranty Disclaimers are considered to be included by reference in + this License, but only as regards disclaiming warranties: any other + implication that these Warranty Disclaimers may have is void and + has no effect on the meaning of this License. + +2. VERBATIM COPYING + + You may copy and distribute the Document in any medium, either + commercially or noncommercially, provided that this License, the + copyright notices, and the license notice saying this License + applies to the Document are reproduced in all copies, and that you + add no other conditions whatsoever to those of this License. You + may not use technical measures to obstruct or control the reading + or further copying of the copies you make or distribute. However, + you may accept compensation in exchange for copies. If you + distribute a large enough number of copies you must also follow the + conditions in section 3. + + You may also lend copies, under the same conditions stated above, + and you may publicly display copies. + +3. COPYING IN QUANTITY + + If you publish printed copies (or copies in media that commonly + have printed covers) of the Document, numbering more than 100, and + the Document's license notice requires Cover Texts, you must + enclose the copies in covers that carry, clearly and legibly, all + these Cover Texts: Front-Cover Texts on the front cover, and + Back-Cover Texts on the back cover. Both covers must also clearly + and legibly identify you as the publisher of these copies. The + front cover must present the full title with all words of the title + equally prominent and visible. You may add other material on the + covers in addition. Copying with changes limited to the covers, as + long as they preserve the title of the Document and satisfy these + conditions, can be treated as verbatim copying in other respects. + + If the required texts for either cover are too voluminous to fit + legibly, you should put the first ones listed (as many as fit + reasonably) on the actual cover, and continue the rest onto + adjacent pages. + + If you publish or distribute Opaque copies of the Document + numbering more than 100, you must either include a machine-readable + Transparent copy along with each Opaque copy, or state in or with + each Opaque copy a computer-network location from which the general + network-using public has access to download using public-standard + network protocols a complete Transparent copy of the Document, free + of added material. If you use the latter option, you must take + reasonably prudent steps, when you begin distribution of Opaque + copies in quantity, to ensure that this Transparent copy will + remain thus accessible at the stated location until at least one + year after the last time you distribute an Opaque copy (directly or + through your agents or retailers) of that edition to the public. + + It is requested, but not required, that you contact the authors of + the Document well before redistributing any large number of copies, + to give them a chance to provide you with an updated version of the + Document. + +4. MODIFICATIONS + + You may copy and distribute a Modified Version of the Document + under the conditions of sections 2 and 3 above, provided that you + release the Modified Version under precisely this License, with the + Modified Version filling the role of the Document, thus licensing + distribution and modification of the Modified Version to whoever + possesses a copy of it. In addition, you must do these things in + the Modified Version: + + #+attr_texinfo: :enum A + 1. Use in the Title Page (and on the covers, if any) a title + distinct from that of the Document, and from those of previous + versions (which should, if there were any, be listed in the + History section of the Document). You may use the same title as + a previous version if the original publisher of that version + gives permission. + + 2. List on the Title Page, as authors, one or more persons or + entities responsible for authorship of the modifications in the + Modified Version, together with at least five of the principal + authors of the Document (all of its principal authors, if it has + fewer than five), unless they release you from this requirement. + + 3. State on the Title page the name of the publisher of the + Modified Version, as the publisher. + + 4. Preserve all the copyright notices of the Document. + + 5. Add an appropriate copyright notice for your modifications + adjacent to the other copyright notices. + + 6. Include, immediately after the copyright notices, a license + notice giving the public permission to use the Modified Version + under the terms of this License, in the form shown in the + Addendum below. + + 7. Preserve in that license notice the full lists of Invariant + Sections and required Cover Texts given in the Document's + license notice. + + 8. Include an unaltered copy of this License. + + 9. Preserve the section Entitled "History", Preserve its Title, and + add to it an item stating at least the title, year, new authors, + and publisher of the Modified Version as given on the Title + Page. If there is no section Entitled "History" in the Document, + create one stating the title, year, authors, and publisher of + the Document as given on its Title Page, then add an item + describing the Modified Version as stated in the previous + sentence. + + 10. Preserve the network location, if any, given in the Document + for public access to a Transparent copy of the Document, and + likewise the network locations given in the Document for + previous versions it was based on. These may be placed in the + "History" section. You may omit a network location for a work + that was published at least four years before the Document + itself, or if the original publisher of the version it refers + to gives permission. + + 11. For any section Entitled "Acknowledgements" or "Dedications", + Preserve the Title of the section, and preserve in the section + all the substance and tone of each of the contributor + acknowledgements and/or dedications given therein. + + 12. Preserve all the Invariant Sections of the Document, unaltered + in their text and in their titles. Section numbers or the + equivalent are not considered part of the section titles. + + 13. Delete any section Entitled "Endorsements". Such a section may + not be included in the Modified Version. + + 14. Do not retitle any existing section to be Entitled + "Endorsements" or to conflict in title with any Invariant + Section. + + 15. Preserve any Warranty Disclaimers. + + If the Modified Version includes new front-matter sections or + appendices that qualify as Secondary Sections and contain no material + copied from the Document, you may at your option designate some or all + of these sections as invariant. To do this, add their titles to the + list of Invariant Sections in the Modified Version's license notice. + These titles must be distinct from any other section titles. + + You may add a section Entitled "Endorsements", provided it contains + nothing but endorsements of your Modified Version by various + parties---for example, statements of peer review or that the text has + been approved by an organization as the authoritative definition of a + standard. + + You may add a passage of up to five words as a Front-Cover Text, and a + passage of up to 25 words as a Back-Cover Text, to the end of the list + of Cover Texts in the Modified Version. Only one passage of + Front-Cover Text and one of Back-Cover Text may be added by (or + through arrangements made by) any one entity. If the Document already + includes a cover text for the same cover, previously added by you or + by arrangement made by the same entity you are acting on behalf of, + you may not add another; but you may replace the old one, on explicit + permission from the previous publisher that added the old one. + + The author(s) and publisher(s) of the Document do not by this License + give permission to use their names for publicity for or to assert or + imply endorsement of any Modified Version. + +5. COMBINING DOCUMENTS + + You may combine the Document with other documents released under + this License, under the terms defined in section 4 above for + modified versions, provided that you include in the combination all + of the Invariant Sections of all of the original documents, + unmodified, and list them all as Invariant Sections of your + combined work in its license notice, and that you preserve all + their Warranty Disclaimers. + + The combined work need only contain one copy of this License, and + multiple identical Invariant Sections may be replaced with a single + copy. If there are multiple Invariant Sections with the same name + but different contents, make the title of each such section unique + by adding at the end of it, in parentheses, the name of the + original author or publisher of that section if known, or else + a unique number. Make the same adjustment to the section titles in + the list of Invariant Sections in the license notice of the + combined work. + + In the combination, you must combine any sections Entitled + "History" in the various original documents, forming one section + Entitled "History"; likewise combine any sections Entitled + "Acknowledgements", and any sections Entitled "Dedications". You + must delete all sections Entitled "Endorsements." + +6. COLLECTIONS OF DOCUMENTS + + You may make a collection consisting of the Document and other + documents released under this License, and replace the individual + copies of this License in the various documents with a single copy + that is included in the collection, provided that you follow the + rules of this License for verbatim copying of each of the documents + in all other respects. + + You may extract a single document from such a collection, and + distribute it individually under this License, provided you insert + a copy of this License into the extracted document, and follow this + License in all other respects regarding verbatim copying of that + document. + +7. AGGREGATION WITH INDEPENDENT WORKS + + A compilation of the Document or its derivatives with other + separate and independent documents or works, in or on a volume of + a storage or distribution medium, is called an "aggregate" if the + copyright resulting from the compilation is not used to limit the + legal rights of the compilation's users beyond what the individual + works permit. When the Document is included in an aggregate, this + License does not apply to the other works in the aggregate which + are not themselves derivative works of the Document. + + If the Cover Text requirement of section 3 is applicable to these + copies of the Document, then if the Document is less than one half + of the entire aggregate, the Document's Cover Texts may be placed + on covers that bracket the Document within the aggregate, or the + electronic equivalent of covers if the Document is in electronic + form. Otherwise they must appear on printed covers that bracket + the whole aggregate. + +8. TRANSLATION + + Translation is considered a kind of modification, so you may + distribute translations of the Document under the terms of + section 4. Replacing Invariant Sections with translations requires + special permission from their copyright holders, but you may + include translations of some or all Invariant Sections in addition + to the original versions of these Invariant Sections. You may + include a translation of this License, and all the license notices + in the Document, and any Warranty Disclaimers, provided that you + also include the original English version of this License and the + original versions of those notices and disclaimers. In case of + a disagreement between the translation and the original version of + this License or a notice or disclaimer, the original version will + prevail. + + If a section in the Document is Entitled "Acknowledgements", + "Dedications", or "History", the requirement (section 4) to + Preserve its Title (section 1) will typically require changing the + actual title. + +9. TERMINATION + + You may not copy, modify, sublicense, or distribute the Document + except as expressly provided under this License. Any attempt + otherwise to copy, modify, sublicense, or distribute it is void, + and will automatically terminate your rights under this License. + + However, if you cease all violation of this License, then your + license from a particular copyright holder is reinstated (a) + provisionally, unless and until the copyright holder explicitly and + finally terminates your license, and (b) permanently, if the + copyright holder fails to notify you of the violation by some + reasonable means prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is + reinstated permanently if the copyright holder notifies you of the + violation by some reasonable means, this is the first time you have + received notice of violation of this License (for any work) from + that copyright holder, and you cure the violation prior to 30 days + after your receipt of the notice. + + Termination of your rights under this section does not terminate + the licenses of parties who have received copies or rights from you + under this License. If your rights have been terminated and not + permanently reinstated, receipt of a copy of some or all of the + same material does not give you any rights to use it. + +10. FUTURE REVISIONS OF THIS LICENSE + + The Free Software Foundation may publish new, revised versions of + the GNU Free Documentation License from time to time. Such new + versions will be similar in spirit to the present version, but may + differ in detail to address new problems or concerns. See + https://www.gnu.org/copyleft/. + + Each version of the License is given a distinguishing version + number. If the Document specifies that a particular numbered + version of this License "or any later version" applies to it, you + have the option of following the terms and conditions either of + that specified version or of any later version that has been + published (not as a draft) by the Free Software Foundation. If + the Document does not specify a version number of this License, + you may choose any version ever published (not as a draft) by the + Free Software Foundation. If the Document specifies that a proxy + can decide which future versions of this License can be used, that + proxy's public statement of acceptance of a version permanently + authorizes you to choose that version for the Document. + +11. RELICENSING + + "Massive Multiauthor Collaboration Site" (or "MMC Site") means any + World Wide Web server that publishes copyrightable works and also + provides prominent facilities for anybody to edit those works. + A public wiki that anybody can edit is an example of such + a server. A "Massive Multiauthor Collaboration" (or "MMC") + contained in the site means any set of copyrightable works thus + published on the MMC site. + + "CC-BY-SA" means the Creative Commons Attribution-Share Alike 3.0 + license published by Creative Commons Corporation, + a not-for-profit corporation with a principal place of business in + San Francisco, California, as well as future copyleft versions of + that license published by that same organization. + + "Incorporate" means to publish or republish a Document, in whole + or in part, as part of another Document. + + An MMC is "eligible for relicensing" if it is licensed under this + License, and if all works that were first published under this + License somewhere other than this MMC, and subsequently + incorporated in whole or in part into the MMC, (1) had no cover + texts or invariant sections, and (2) were thus incorporated prior + to November 1, 2008. + + The operator of an MMC Site may republish an MMC contained in the + site under CC-BY-SA on the same site at any time before August 1, + 2009, provided the MMC is eligible for relicensing. + +#+texinfo: @page + +* ADDENDUM: How to use this License for your documents +:PROPERTIES: +:UNNUMBERED: notoc +:END: + +To use this License in a document you have written, include a copy of +the License in the document and put the following copyright and +license notices just after the title page: + +#+begin_example + Copyright (C) YEAR YOUR NAME. + Permission is granted to copy, distribute and/or modify this document + under the terms of the GNU Free Documentation License, Version 1.3 + or any later version published by the Free Software Foundation; + with no Invariant Sections, no Front-Cover Texts, and no Back-Cover + Texts. A copy of the license is included in the section entitled ``GNU + Free Documentation License''. +#+end_example + +If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts, +replace the "with...Texts."\nbsp{}line with this: + +#+begin_example + with the Invariant Sections being LIST THEIR TITLES, with + the Front-Cover Texts being LIST, and with the Back-Cover Texts + being LIST. +#+end_example + +If you have Invariant Sections without Cover Texts, or some other +combination of the three, merge those two alternatives to suit the +situation. + +If your document contains nontrivial examples of program code, we +recommend releasing these examples in parallel under your choice of +free software license, such as the GNU General Public License, to +permit their use in free software. diff --git a/docs/man.org b/docs/man.org new file mode 100644 index 0000000..279165c --- /dev/null +++ b/docs/man.org @@ -0,0 +1,36 @@ +#+title: vericert +#+man_class_options: :section-id "1" +#+export_file_name: vericert.1 + +* NAME + +vericert - A formally verified high-level synthesis tool. + +* SYNOPSYS + +*vericert* [ *OPTION* ]... [ *FILE* ]... + +* DESCRIPTION + +- -drtl :: Print intermediate RTL. + +* AUTHOR + +Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. + +* COPYRIGHT + +Copyright (C) 2019-2022 Yann Herklotz + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . -- cgit