diff options
Diffstat (limited to 'docs/man.org')
| -rw-r--r-- | docs/man.org | 89 |
1 files changed, 0 insertions, 89 deletions
diff --git a/docs/man.org b/docs/man.org deleted file mode 100644 index cb6143f..0000000 --- a/docs/man.org +++ /dev/null @@ -1,89 +0,0 @@ -#+title: vericert -#+man_class_options: :section-id "1" -#+options: toc:nil num:nil -#+html_head_extra: <style>body{font-family:monospace;max-width:60em}h1{text-align:center}dt{font-weight:700}dd{margin-bottom:1em}</style> - -* NAME - -vericert - A formally verified high-level synthesis tool. - -* SYNOPSYS - -*vericert* [ *OPTION* ]... [ *FILE* ]... - -* DESCRIPTION - -** HLS Options: - -- --no-hls :: Do not use HLS and generate standard flow -- --simulate :: Simulate the result with the Verilog semantics -- --debug-hls :: Add debug logic to the Verilog -- --initialise-stack :: initialise the stack to all 0s - -** HLS Optimisations: - -- -fschedule :: Schedule the resulting hardware [off] -- -fif-conversion :: If-conversion optimisation [off] - -** General options: - -- -stdlib <dir> :: Set the path of the Compcert run-time library -- -v :: Print external commands before invoking them -- -timings :: Show the time spent in various compiler passes -- -version :: Print the version string and exit -- -target <value> :: Generate code for the given target -- -conf <file> :: Read configuration from file -- @<file> :: Read command line options from <file> - -** Tracing Options: - -- -dprepro :: Save C file after preprocessing in <file>.i -- -dparse :: Save C file after parsing and elaboration in <file>.parsed.c -- -dc :: Save generated C in <file>.compcert.c -- -dclight :: Save generated Clight in <file>.light.c -- -dcminor :: Save generated Cminor in <file>.cm -- -drtl :: Save RTL at various optimization points in <file>.rtl.<n> -- -drtlblock :: Save RTLBlock <file>.rtlblock -- -dhtl :: Save HTL before Verilog generation <file>.htl -- -dltl :: Save LTL after register allocation in <file>.ltl -- -dmach :: Save generated Mach code in <file>.mach -- -dasm :: Save generated assembly in <file>.s -- -dall :: Save all generated intermediate files in <file>.<ext> -- -sdump :: Save info for post-linking validation in <file>.json -- -o <file> :: Generate output in <file> - -** Diagnostic options: - -- -Wall :: Enable all warnings -- -W<warning> :: Enable the specific <warning> -- -Wno-<warning> :: Disable the specific <warning> -- -Werror :: Make all warnings into errors -- -Werror=<warning> :: Turn <warning> into an error -- -Wno-error=<warning> :: Turn <warning> into a warning even if -Werror is specified -- -Wfatal-errors :: Turn all errors into fatal errors aborting the compilation -- -fdiagnostics-color :: Turn on colored diagnostics -- -fno-diagnostics-color :: Turn of colored diagnostics -- -fmax-errors=<n> :: Maximum number of errors to report -- -fdiagnostics-show-option :: Print the option name with mappable diagnostics -- -fno-diagnostics-show-option :: Turn of printing of options with mappable diagnostics - -* AUTHOR - -Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. - -* COPYRIGHT - -Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com> - -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 <https://www.gnu.org/licenses/>. |