-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathREADME.simgen
138 lines (100 loc) · 4.42 KB
/
README.simgen
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
SimSoC-Cert, a toolkit for generating certified processor simulators
See the COPYRIGHTS and LICENSE files
--------------------------------------------------------------------
This files describes the possible usages of the code generator simgen.
Files extensions used:
----------------------
.pc : ARMv6 pseudocode (text file)
.dec: OCaml value of type Codetype.maplist representing the binary
decoding tables of some instructions (binary file)
.syntax: OCaml value of type Syntaxtype.syntax representing the
assembly syntax of some instructions (binary file)
.dat: OCaml value of type Manual.manual representing the binary
encoding, assembly syntax and pseudocode semantics of some
instructions (binary file)
.bin: binary code without ELF header (binary file)
(use tools/bin2elf/bin2elf to generate the appropriate ELF header)
.wgt: space-separated list of non-negative integers (weights) of
length the number of instructions (text file)
(can be generated by SimSoC for ARMv6)
General options:
----------------
-h|-help|--help: Display the list of options
-d: debugging mode
-v: verbose mode
-seed <integer>: set the seed of the pseudo-random number generator
used in test generation
Options that can be used in conjonction with the -ipc option:
-------------------------------------------------------------
-norm: normalize the pseudocode
-check: internally reparse the pseudocode after parsing
(and after normalization with -norm option)
Usages:
Pretty-print and normalize pseudocode:
--------------------------------------
simgen/main -ipc file1.pc -opc > file2.pc
Generate a Coq decoder from a decoding file:
--------------------------------------------
simgen/main -idec file1.dec -ocoq-dec > file2.v
Convert pseudocode into Coq code:
---------------------------------
simgen/main -ipc file1.pc -ocoq-inst > file2.v
Remark: the pseudocode is automatically normalized.
Generate assembly instructions to test a decoder:
-------------------------------------------------
simgen/main -ipc file1.pc -idec file2.dec -isyntax file3.syntax -oasm-test file4.txt
Generate binary instructions to test a decoder:
-----------------------------------------------
simgen/main -ipc file1.pc -idec file2.dec -isyntax file3.syntax -obin-test > file4.arm
Generate a non-optimized C simulator:
-------------------------------------
simgen/main -ipc file1.pc -idec file2.dec -ocxx prefix
Generates:
prefix.h
prefix.c
Remark: the pseudocode is automatically normalized.
Generate an optimized C simulator:
----------------------------------
simgen/main -ipc file1.pc -idec file2.dec -isyntax file3.syntax -oc4dt prefix
Generates:
- prefix.h:
the instruction type and the instruction numeric identifiers
- prefix.c:
instruction names, and the "may_branch" function
- prefix_expanded.h:
declaration of the semantics function, with an expanded list of arguments
- prefix_expanded.hot.c, prefix_expanded.cold.c:
implementation of the previous header file
- prefix_grouped.h:
declaration of the semantics function, with the arguments stored
in a structure type
- prefix_grouped.hot.c, prefix_grouped.cold.c:
implementation of the previous header file
- prefix_arm_decode_exec.c:
decoder for ARM32 code, which directly call the semantics function
- prefix_thumb_decode_exec.c:
decoder for Thumb code, which directly call the semantics function
- prefix_arm_decode_store.c:
decoder for ARM32 code, which store the decoded instruction
using the type defined in prefix.h
- prefix_thumb_decode_store.c:
decoder for Thumb code, which store the decoded instruction
using the type defined in prefix.h
- prefix-llvm_generator.hpp:
part of an ARM to LLVM translator (this file cannot be compiled
outside SimSoC)
- prefix_printer.h, prefix_printer.c:
instruction printers using the ASM format (C code using fprintf)
- prefix_printer.hpp, prefix_printer.cpp:
instruction printers using the ASM format (C++ code using streams)
- print_sizes.c:
stand-alone program to control the size of the instruction type and subtypes
Remark:
- the pseudocode is automatically normalized
- the following files are not used by simlight2 (but are used by SimSoC):
prefix-llvm_generator.hpp, prefix_printer.hpp, and prefix_printer.cpp
- the following files are not used by SimSoC:
prefix_arm_decode_exec.c, prefix_thumb_decode_exec.c, prefix_printer.h,
and prefix_printer.c
Options:
-iwgt file4.wgt: instructions of non-zero weigth are not specialized