blob: cb6143f853ce9fbeb86d3f0f2bceecec55986321 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
#+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/>.
|
