aboutsummaryrefslogtreecommitdiffstats
path: root/techlibs/xilinx/lutrams_map.v
blob: 3ac1143bbd6a8284d9690a88c411aec3a47d47da (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
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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279

module \$__XILINX_RAM16X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [15:0] INIT = 16'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [3:0] A1ADDR;
	output A1DATA;

	input [3:0] B1ADDR;
	input B1DATA;
	input B1EN;

	RAM16X1D #(
		.INIT(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.DPRA0(A1ADDR[0]),
		.DPRA1(A1ADDR[1]),
		.DPRA2(A1ADDR[2]),
		.DPRA3(A1ADDR[3]),
		.DPO(A1DATA),

		.A0(B1ADDR[0]),
		.A1(B1ADDR[1]),
		.A2(B1ADDR[2]),
		.A3(B1ADDR[3]),
		.D(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM32X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [31:0] INIT = 32'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [4:0] A1ADDR;
	output A1DATA;

	input [4:0] B1ADDR;
	input B1DATA;
	input B1EN;

	RAM32X1D #(
		.INIT(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.DPRA0(A1ADDR[0]),
		.DPRA1(A1ADDR[1]),
		.DPRA2(A1ADDR[2]),
		.DPRA3(A1ADDR[3]),
		.DPRA4(A1ADDR[4]),
		.DPO(A1DATA),

		.A0(B1ADDR[0]),
		.A1(B1ADDR[1]),
		.A2(B1ADDR[2]),
		.A3(B1ADDR[3]),
		.A4(B1ADDR[4]),
		.D(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM64X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [63:0] INIT = 64'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [5:0] A1ADDR;
	output A1DATA;

	input [5:0] B1ADDR;
	input B1DATA;
	input B1EN;

	RAM64X1D #(
		.INIT(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.DPRA0(A1ADDR[0]),
		.DPRA1(A1ADDR[1]),
		.DPRA2(A1ADDR[2]),
		.DPRA3(A1ADDR[3]),
		.DPRA4(A1ADDR[4]),
		.DPRA5(A1ADDR[5]),
		.DPO(A1DATA),

		.A0(B1ADDR[0]),
		.A1(B1ADDR[1]),
		.A2(B1ADDR[2]),
		.A3(B1ADDR[3]),
		.A4(B1ADDR[4]),
		.A5(B1ADDR[5]),
		.D(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM128X1D (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [127:0] INIT = 128'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [6:0] A1ADDR;
	output A1DATA;

	input [6:0] B1ADDR;
	input B1DATA;
	input B1EN;

	RAM128X1D #(
		.INIT(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.DPRA(A1ADDR),
		.DPO(A1DATA),

		.A(B1ADDR),
		.D(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule


module \$__XILINX_RAM32X6SDP (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [32*6-1:0] INIT = {32*6{1'bx}};
	parameter CLKPOL2 = 1;
	input CLK1;

	input [4:0] A1ADDR;
	output [5:0] A1DATA;

	input [4:0] B1ADDR;
	input [5:0] B1DATA;
	input B1EN;

	wire [1:0] DOD_unused;

	RAM32M #(
		.INIT_A({INIT[187:186], INIT[181:180], INIT[175:174], INIT[169:168], INIT[163:162], INIT[157:156], INIT[151:150], INIT[145:144], INIT[139:138], INIT[133:132], INIT[127:126], INIT[121:120], INIT[115:114], INIT[109:108], INIT[103:102], INIT[ 97: 96], INIT[ 91: 90], INIT[ 85: 84], INIT[ 79: 78], INIT[ 73: 72], INIT[ 67: 66], INIT[ 61: 60], INIT[ 55: 54], INIT[ 49: 48], INIT[ 43: 42], INIT[ 37: 36], INIT[ 31: 30], INIT[ 25: 24], INIT[ 19: 18], INIT[ 13: 12], INIT[  7:  6], INIT[  1:  0]}),
		.INIT_B({INIT[189:188], INIT[183:182], INIT[177:176], INIT[171:170], INIT[165:164], INIT[159:158], INIT[153:152], INIT[147:146], INIT[141:140], INIT[135:134], INIT[129:128], INIT[123:122], INIT[117:116], INIT[111:110], INIT[105:104], INIT[ 99: 98], INIT[ 93: 92], INIT[ 87: 86], INIT[ 81: 80], INIT[ 75: 74], INIT[ 69: 68], INIT[ 63: 62], INIT[ 57: 56], INIT[ 51: 50], INIT[ 45: 44], INIT[ 39: 38], INIT[ 33: 32], INIT[ 27: 26], INIT[ 21: 20], INIT[ 15: 14], INIT[  9:  8], INIT[  3:  2]}),
		.INIT_C({INIT[191:190], INIT[185:184], INIT[179:178], INIT[173:172], INIT[167:166], INIT[161:160], INIT[155:154], INIT[149:148], INIT[143:142], INIT[137:136], INIT[131:130], INIT[125:124], INIT[119:118], INIT[113:112], INIT[107:106], INIT[101:100], INIT[ 95: 94], INIT[ 89: 88], INIT[ 83: 82], INIT[ 77: 76], INIT[ 71: 70], INIT[ 65: 64], INIT[ 59: 58], INIT[ 53: 52], INIT[ 47: 46], INIT[ 41: 40], INIT[ 35: 34], INIT[ 29: 28], INIT[ 23: 22], INIT[ 17: 16], INIT[ 11: 10], INIT[  5:  4]}),
		.INIT_D(64'bx),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.ADDRA(A1ADDR),
		.ADDRB(A1ADDR),
		.ADDRC(A1ADDR),
		.DOA(A1DATA[1:0]),
		.DOB(A1DATA[3:2]),
		.DOC(A1DATA[5:4]),
		.DOD(DOD_unused),

		.ADDRD(B1ADDR),
		.DIA(B1DATA[1:0]),
		.DIB(B1DATA[3:2]),
		.DIC(B1DATA[5:4]),
		.DID(2'b00),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM64X3SDP (CLK1, A1ADDR, A1DATA, B1ADDR, B1DATA, B1EN);
	parameter [64*3-1:0] INIT = {64*3{1'bx}};
	parameter CLKPOL2 = 1;
	input CLK1;

	input [5:0] A1ADDR;
	output [2:0] A1DATA;

	input [5:0] B1ADDR;
	input [2:0] B1DATA;
	input B1EN;

	wire DOD_unused;

	RAM64M #(
		.INIT_A({INIT[189], INIT[186], INIT[183], INIT[180], INIT[177], INIT[174], INIT[171], INIT[168], INIT[165], INIT[162], INIT[159], INIT[156], INIT[153], INIT[150], INIT[147], INIT[144], INIT[141], INIT[138], INIT[135], INIT[132], INIT[129], INIT[126], INIT[123], INIT[120], INIT[117], INIT[114], INIT[111], INIT[108], INIT[105], INIT[102], INIT[ 99], INIT[ 96], INIT[ 93], INIT[ 90], INIT[ 87], INIT[ 84], INIT[ 81], INIT[ 78], INIT[ 75], INIT[ 72], INIT[ 69], INIT[ 66], INIT[ 63], INIT[ 60], INIT[ 57], INIT[ 54], INIT[ 51], INIT[ 48], INIT[ 45], INIT[ 42], INIT[ 39], INIT[ 36], INIT[ 33], INIT[ 30], INIT[ 27], INIT[ 24], INIT[ 21], INIT[ 18], INIT[ 15], INIT[ 12], INIT[  9], INIT[  6], INIT[  3], INIT[  0]}),
		.INIT_B({INIT[190], INIT[187], INIT[184], INIT[181], INIT[178], INIT[175], INIT[172], INIT[169], INIT[166], INIT[163], INIT[160], INIT[157], INIT[154], INIT[151], INIT[148], INIT[145], INIT[142], INIT[139], INIT[136], INIT[133], INIT[130], INIT[127], INIT[124], INIT[121], INIT[118], INIT[115], INIT[112], INIT[109], INIT[106], INIT[103], INIT[100], INIT[ 97], INIT[ 94], INIT[ 91], INIT[ 88], INIT[ 85], INIT[ 82], INIT[ 79], INIT[ 76], INIT[ 73], INIT[ 70], INIT[ 67], INIT[ 64], INIT[ 61], INIT[ 58], INIT[ 55], INIT[ 52], INIT[ 49], INIT[ 46], INIT[ 43], INIT[ 40], INIT[ 37], INIT[ 34], INIT[ 31], INIT[ 28], INIT[ 25], INIT[ 22], INIT[ 19], INIT[ 16], INIT[ 13], INIT[ 10], INIT[  7], INIT[  4], INIT[  1]}),
		.INIT_C({INIT[191], INIT[188], INIT[185], INIT[182], INIT[179], INIT[176], INIT[173], INIT[170], INIT[167], INIT[164], INIT[161], INIT[158], INIT[155], INIT[152], INIT[149], INIT[146], INIT[143], INIT[140], INIT[137], INIT[134], INIT[131], INIT[128], INIT[125], INIT[122], INIT[119], INIT[116], INIT[113], INIT[110], INIT[107], INIT[104], INIT[101], INIT[ 98], INIT[ 95], INIT[ 92], INIT[ 89], INIT[ 86], INIT[ 83], INIT[ 80], INIT[ 77], INIT[ 74], INIT[ 71], INIT[ 68], INIT[ 65], INIT[ 62], INIT[ 59], INIT[ 56], INIT[ 53], INIT[ 50], INIT[ 47], INIT[ 44], INIT[ 41], INIT[ 38], INIT[ 35], INIT[ 32], INIT[ 29], INIT[ 26], INIT[ 23], INIT[ 20], INIT[ 17], INIT[ 14], INIT[ 11], INIT[  8], INIT[  5], INIT[  2]}),
		.INIT_D(64'bx),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.ADDRA(A1ADDR),
		.ADDRB(A1ADDR),
		.ADDRC(A1ADDR),
		.DOA(A1DATA[0]),
		.DOB(A1DATA[1]),
		.DOC(A1DATA[2]),
		.DOD(DOD_unused),

		.ADDRD(B1ADDR),
		.DIA(B1DATA[0]),
		.DIB(B1DATA[1]),
		.DIC(B1DATA[2]),
		.DID(1'b0),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM32X2Q (CLK1, A1ADDR, A1DATA, A2ADDR, A2DATA, A3ADDR, A3DATA, B1ADDR, B1DATA, B1EN);
	parameter [63:0] INIT = 64'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [4:0] A1ADDR, A2ADDR, A3ADDR;
	output [1:0] A1DATA, A2DATA, A3DATA;

	input [4:0] B1ADDR;
	input [1:0] B1DATA;
	input B1EN;

	RAM32M #(
		.INIT_A(INIT),
		.INIT_B(INIT),
		.INIT_C(INIT),
		.INIT_D(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.ADDRA(A1ADDR),
		.ADDRB(A2ADDR),
		.ADDRC(A3ADDR),
		.DOA(A1DATA),
		.DOB(A2DATA),
		.DOC(A3DATA),

		.ADDRD(B1ADDR),
		.DIA(B1DATA),
		.DIB(B1DATA),
		.DIC(B1DATA),
		.DID(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule

module \$__XILINX_RAM64X1Q (CLK1, A1ADDR, A1DATA, A2ADDR, A2DATA, A3ADDR, A3DATA, B1ADDR, B1DATA, B1EN);
	parameter [63:0] INIT = 64'bx;
	parameter CLKPOL2 = 1;
	input CLK1;

	input [5:0] A1ADDR, A2ADDR, A3ADDR;
	output A1DATA, A2DATA, A3DATA;

	input [5:0] B1ADDR;
	input B1DATA;
	input B1EN;

	RAM64M #(
		.INIT_A(INIT),
		.INIT_B(INIT),
		.INIT_C(INIT),
		.INIT_D(INIT),
		.IS_WCLK_INVERTED(!CLKPOL2)
	) _TECHMAP_REPLACE_ (
		.ADDRA(A1ADDR),
		.ADDRB(A2ADDR),
		.ADDRC(A3ADDR),
		.DOA(A1DATA),
		.DOB(A2DATA),
		.DOC(A3DATA),

		.ADDRD(B1ADDR),
		.DIA(B1DATA),
		.DIB(B1DATA),
		.DIC(B1DATA),
		.DID(B1DATA),
		.WCLK(CLK1),
		.WE(B1EN)
	);
endmodule
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-31 12:02:07 +0000
them, and pushes the result back on the stack. So the following command will select all {\$add} cells that have the {\tt foo} attribute set: \begin{verbatim} select t:$add a:foo %i \end{verbatim} The listing in Fig.~\ref{sumprod} uses the Yosys non-standard {\tt \{* ... *\}} syntax to set the attribute {\tt sumstuff} on all cells generated by the first assign statement. (This works on arbitrary large blocks of Verilog code an can be used to mark portions of code for analysis.) Selecting {\tt a:sumstuff} in this module will yield the circuit diagram shown in Fig.~\ref{sumprod_00}. As only the cells themselves are selected, but not the temporary wire {\tt \$1\_Y}, the two adders are shown as two disjunct parts. This can be very useful for global signals like clock and reset signals: just unselect them using a command such as {\tt select -del clk rst} and each cell using them will get its own net label. In this case however we would like to see the cells connected properly. This can be achieved using the {\tt \%x} action, that broadens the selection, i.e. for each selected wire it selects all cells connected to the wire and vice versa. So {\tt show a:sumstuff \%x} yields the diagram schon in Fig.~\ref{sumprod_01}. \begin{figure}[t] \includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/sumprod_01.pdf} \caption{Output of {\tt show a:sumstuff \%x} on Fig.~\ref{sumprod}} \label{sumprod_01} \end{figure} \subsection{Selecting logic cones} Fig.~\ref{sumprod_01} shows what is called the {\it input cone\/} of {\tt sum}, i.e. all cells and signals that are used to generate the signal {\tt sum}. The {\tt \%ci} action can be used to select the input cones of all object in the top selection in the stack maintained by the {\tt select} command. As the {\tt \%x} action, this commands broadens the selection by one ``step''. But this time the operation only works against the direction of data flow. That means, wires only select cells via output ports and cells only select wires via input ports. Fig.~\ref{select_prod} show the sequence of diagrams generated by the following commands: \begin{verbatim} show prod show prod %ci show prod %ci %ci show prod %ci %ci %ci \end{verbatim} When selecting many levels of logic, repeating {\tt \%ci} over and over again can be a bit dull. So there is a shortcut for that: the number of iterations can be appended to the action. So for example the action {\tt \%ci3} is identical to performing the {\tt \%ci} action three times. The action {\tt \%ci*} performs the {\tt \%ci} action over and over again until it has no effect anymore. \begin{figure}[t] \hfill \includegraphics[width=4cm,trim=0 1cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_02.pdf} \\ \includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_03.pdf} \\ \includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_04.pdf} \\ \includegraphics[width=\linewidth,trim=0 2cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_05.pdf} \\ \caption{Objects selected by {\tt select prod \%ci...}} \label{select_prod} \end{figure} \medskip In most cases there are certain cell types and/or ports that should not be considered for the {\tt \%ci} action, or we only want to follow certain cell types and/or ports. This can be achieved using additional patterns that can be appended to the {\tt \%ci} action. Lets consider the design from Fig.~\ref{memdemo_src}. It serves no purpose other than being a non-trivial circuit for demonstrating some of the advanced Yosys features. We synthesize the circuit using {\tt proc; opt; memory; opt} and change to the {\tt memdemo} module with {\tt cd memdemo}. If we type {\tt show} now we see the diagram shown in Fig.~\ref{memdemo_00}. \begin{figure}[b!] \lstinputlisting{APPNOTE_011_Design_Investigation/memdemo.v} \caption{Demo circuit for demonstrating some advanced Yosys features} \label{memdemo_src} \end{figure} \begin{figure*}[t] \includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_00.pdf} \\ \caption{Complete circuit diagram for the design shown in Fig.~\ref{memdemo_src}} \label{memdemo_00} \end{figure*} But maybe we are only interested in the tree of multiplexers that select the output value. In order to get there, we would start by just showing the output signal and its immediate predecessors: \begin{verbatim} show y %ci2 \end{verbatim} From this we would learn that {\tt y} is driven by a {\tt \$dff cell}, that {\tt y} is connected to the output port {\tt Q}, that the {\tt clk} signal goes into the {\tt CLK} input port of the cell, and that the data comes from a auto-generated wire into the input {\tt D} of the flip-flop cell. As we are not interested in the clock signal we add an additional pattern to the {\tt \%ci} action, that tells it to only follow ports {\tt Q} and {\tt D} of {\tt \$dff} cells: \begin{verbatim} show y %ci2:+$dff[Q,D] \end{verbatim} To add a pattern we add a colon followed by the pattern to the {\tt \%ci} action. The pattern it self starts with {\tt -} or {\tt +}, indicating if it is an include or exclude pattern, followed by an optional comma separated list of cell types, followed by an optional comma separated list of port names in square brackets. Since we know that the only cell considered in this case is a {\tt \$dff} cell, we could as well only specify the port names: \begin{verbatim} show y %ci2:+[Q,D] \end{verbatim} Or we could decide to tell the {\tt \%ci} action to not follow the {\tt CLK} input: \begin{verbatim} show y %ci2:-[CLK] \end{verbatim} \begin{figure}[b] \includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_01.pdf} \\ \caption{Output of {\tt show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff}} \label{memdemo_01} \end{figure} Next we would investigate the next logic level by adding another {\tt \%ci2} to the command: \begin{verbatim} show y %ci2:-[CLK] %ci2 \end{verbatim} From this we would learn that the next cell is a {\tt \$mux} cell and we would add additional pattern to narrow the selection on the path we are interested. In the end we would end up with a command such as \begin{verbatim} show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff \end{verbatim} in which the first {\tt \%ci} jumps over the initial d-type flip-flop and the 2nd action selects the entire input cone without going over multiplexer select inputs and flip-flop cells. The diagram produces by this command is shown in Fig.~\ref{memdemo_01}. \medskip Similar to {\tt \%ci} exists an action {\tt \%co} to select output cones that accepts the same syntax for pattern and repetition. The {\tt \%x} action mentioned previously also accepts this advanced syntax. This actions for traversing the circuit graph, combined with the actions for boolean operations such as intersection ({\tt \%i}) and difference ({\tt \%d}) are powerful tools for extracting the relevant portions of the circuit under investigation. See {\tt help select} for a complete list of actions available in selections. \subsection{Storing and recalling selections} The current selection can be stored in memory with the command {\tt select -set <name>}. It can later be recalled using {\tt select @<name>}. In fact, the {\tt @<name>} expression pushes the stored selection on the stack maintained by the {\tt select} command. So for example \begin{verbatim} select @foo @bar %i \end{verbatim} will select the intersection between the stored selections {\tt foo} and {\tt bar}. \medskip In larger investigation efforts it is highly recommended to maintain a script that sets up relevant selections, so they can easily be recalled, for example when Yosys needs to be re-run after a design or source code change. The {\tt history} command can be used to list all recent interactive commands. This feature can be useful for creating such a script from the commands used in an interactive session. \section{Advanced investigation techniques} \label{poke} When working with very large modules, it is often not enough to just select the interesting part of the module. Instead it can be useful to extract the interesting part of the circuit into a separate module. This can for example be useful if one wants to run a series of synthesis commands on the critical part of the module and wants to carefully read all the debug output created by the commands in order to spot a problem. This kind of troubleshooting is much easier if the circuit under investigation is encapsulated in a separate module. Fig.~\ref{submod} shows how the {\tt submod} command can be used to split the circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} into its components. The {\tt -name} option is used to specify the name of the new module and also the name of the new cell in the current module. \begin{figure}[t] \includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_00.pdf} \\ \centerline{\tt memdemo} \vskip1em\par \includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_01.pdf} \\ \centerline{\tt scramble} \vskip1em\par \includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_02.pdf} \\ \centerline{\tt outstage} \vskip1em\par \includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_03.pdf} \\ \centerline{\tt selstage} \vskip1em\par \begin{lstlisting}[basicstyle=\ttfamily\scriptsize] select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d submod -name scramble @scramble submod -name outstage @outstage submod -name selstage @selstage \end{lstlisting} \caption{The circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} broken up using {\tt submod}} \label{submod} \end{figure} \subsection{Evaluation of combinatorial circuits} The {\tt eval} command can be used to evaluate combinatorial circuits. For example (see Fig.~\ref{submod} for the circuit diagram of {\tt selstage}): {\scriptsize \begin{verbatim} yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1 9. Executing EVAL pass (evaluate the circuit given an input). Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1 Eval result: \n2 = 2'10. Eval result: \n1 = 2'10. \end{verbatim} \par} So the {\tt -set} option is used to set input values and the {\tt -show} option is used to specify the nets to evaluate. If no {\tt -show} option is specified, all selected output ports are used per default. If a necessary input value is not given, an error is produced. The option {\tt -set-undef} can be used to instead set all unspecified input nets to undef ({\tt x}). The {\tt -table} option can be used to create a truth table. For example: {\scriptsize \begin{verbatim} yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0] 10. Executing EVAL pass (evaluate the circuit given an input). Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0] \s1 \d [0] | \n1 \n2 ---- ------ | ---- ---- 2'00 1'0 | 2'00 2'00 2'00 1'1 | 2'xx 2'00 2'01 1'0 | 2'00 2'00 2'01 1'1 | 2'xx 2'01 2'10 1'0 | 2'00 2'00 2'10 1'1 | 2'xx 2'10 2'11 1'0 | 2'00 2'00 2'11 1'1 | 2'xx 2'11 Assumend undef (x) value for the following singals: \s2 \end{verbatim} } Note that the {\tt eval} command (as well as the {\tt sat} command discussed in the next sections) does only operate on flattened modules. It can not analyze signals that are passed through design hierarchy levels. So the {\tt flatten} command must be used on modules that instantiate other modules before this commands can be applied. \subsection{Solving combinatorial SAT problems} \begin{figure}[b] \lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v} \caption{A simple miter circuit for testing if a number is prime. But it has a problem (see main text and Fig.~\ref{primesat}).} \label{primetest} \end{figure} \begin{figure*}[!t] \begin{lstlisting}[basicstyle=\ttfamily\small] yosys [primetest]> sat -prove ok 1 -set p 31 8. Executing SAT pass (solving SAT problems in the circuit). Full command line: sat -prove ok 1 -set p 31 Setting up SAT problem: Import set-constraint: \p = 16'0000000000011111 Final constraint equation: \p = 16'0000000000011111 Imported 6 cells to SAT database. Import proof-constraint: \ok = 1'1 Final proof equation: \ok = 1'1 Solving problem with 2790 variables and 8241 clauses.. SAT proof finished - model found: FAIL! ______ ___ ___ _ _ _ _ (_____ \ / __) / __) (_) | | | | _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | | | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_| | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ |_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_| Signal Name Dec Hex Bin -------------------- ---------- ---------- --------------------- \a 15029 3ab5 0011101010110101 \b 4099 1003 0001000000000011 \ok 0 0 0 \p 31 1f 0000000000011111 yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0 9. Executing SAT pass (solving SAT problems in the circuit). Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0 Setting up SAT problem: Import set-constraint: \p = 16'0000000000011111 Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000 Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 } Imported 6 cells to SAT database. Import proof-constraint: \ok = 1'1 Final proof equation: \ok = 1'1 Solving problem with 2790 variables and 8257 clauses.. SAT proof finished - no model found: SUCCESS! /$$$$$$ /$$$$$$$$ /$$$$$$$ /$$__ $$ | $$_____/ | $$__ $$ | $$ \ $$ | $$ | $$ \ $$ | $$ | $$ | $$$$$ | $$ | $$ | $$ | $$ | $$__/ | $$ | $$ | $$/$$ $$ | $$ | $$ | $$ | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$ \____ $$$|__/|________/|__/|_______/|__/ \__/ \end{lstlisting} \caption{Experiments with the miter circuit from Fig.~\ref{primetest}. The first attempt of proving that 31 is prime failed because the SAT solver found a creative way of factorizing 31 using integer overflow.} \label{primesat} \end{figure*} Often the opposite of the {\tt eval} command is needed, i.e. the circuits output is given and we want to find the matching input signals. For small circuits with only a few input bits this can be accomplished by trying all possible input combinations, as it is done by the {\tt eval -table} command. For larger circuits however, Yosys provides the {\tt sat} command that uses a SAT \cite{CircuitSAT} solver \cite{MiniSAT} to solve this kind of problems. The {\tt sat} command works very similar to the {\tt eval} command. The main difference is that it is now also possible to set output values and find the corresponding input values. For Example: {\scriptsize \begin{verbatim} yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001 11. Executing SAT pass (solving SAT problems in the circuit). Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001 Setting up SAT problem: Import set-constraint: \s1 = \s2 Import set-constraint: { \n2 \n1 } = 4'1001 Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 } Imported 3 cells to SAT database. Import show expression: { \s1 \s2 \d } Solving problem with 81 variables and 207 clauses.. SAT solving finished - model found: Signal Name Dec Hex Bin -------------------- ---------- ---------- --------------- \d 9 9 1001 \s1 0 0 00 \s2 0 0 00 \end{verbatim} } Note that the {\tt sat} command supports signal names in both arguments to the {\tt -set} option. In the above example we used {\tt -set s1 s2} to constraint {\tt s1} and {\tt s2} to be equal. When more complex constraints are needed, a wrapper circuit must be constructed that checks the constraints and signals if the constraint was met using an extra output port, which then can be forced to a value using the {\tt -set} option. (Such a circuit that contains the circuit under test plus additional constraint checking circuitry is called a {\it miter\/} circuit.) Fig.~\ref{primetest} shows a miter circuit that is supposed to be used as a prime number test. If {\tt ok} is 1 for all input values {\tt a} and {\tt b} for a given {\tt p}, then {\tt p} is prime, or at least that is the idea. The Yosys shell session shown in Fig.~\ref{primesat} demonstrates that SAT solvers can even find the unexpected solutions to a problem: Using integer overflow there actually is a way of ``factorizing'' 31. The clean solution would of course be to perform the test in 32 bits, for example by replacing {\tt p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}, or by using a temporary variable for the 32 bit product {\tt a*b}. But as 31 fits well into 8 bits (and as the purpose of this document is to show off Yosys features) we can also simply force the upper 8 bits of {\tt a} and {\tt b} to zero for the {\tt sat} call, as is done in the second command in Fig.~\ref{primesat} (line 31). The {\tt -prove} option used in this example works similar to {\tt -set}, but tries to find a case in which the two arguments are not equal. If such a case is not found, the property is proven to hold for all inputs that satisfy the other constraints. It might be worth noting, that SAT solvers are not particularly efficient at factorizing large numbers. But if a small factorization problem occurs as part of a larger circuit problem, the Yosys SAT solver is perfectly capable of solving it. \subsection{Solving sequential SAT problems} \begin{figure}[t!] \begin{lstlisting}[basicstyle=\ttfamily\scriptsize] yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \ -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 6. Executing SAT pass (solving SAT problems in the circuit). Full command line: sat -seq 6 -show y -show d -set-init-undef -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 Setting up time step 1: Final constraint equation: { } = { } Imported 29 cells to SAT database. Setting up time step 2: Final constraint equation: { } = { } Imported 29 cells to SAT database. Setting up time step 3: Final constraint equation: { } = { } Imported 29 cells to SAT database. Setting up time step 4: Import set-constraint for timestep: \y = 4'0001 Final constraint equation: \y = 4'0001 Imported 29 cells to SAT database. Setting up time step 5: Import set-constraint for timestep: \y = 4'0010 Final constraint equation: \y = 4'0010 Imported 29 cells to SAT database. Setting up time step 6: Import set-constraint for timestep: \y = 4'0011 Final constraint equation: \y = 4'0011 Imported 29 cells to SAT database. Setting up initial state: Final constraint equation: { \y \s2 \s1 \mem[3] \mem[2] \mem[1] \mem[0] } = 24'xxxxxxxxxxxxxxxxxxxxxxxx Import show expression: \y Import show expression: \d Solving problem with 10322 variables and 27881 clauses.. SAT model found. maximizing number of undefs. SAT solving finished - model found: Time Signal Name Dec Hex Bin ---- -------------------- ---------- ---------- --------------- init \mem[0] -- -- xxxx init \mem[1] -- -- xxxx init \mem[2] -- -- xxxx init \mem[3] -- -- xxxx init \s1 -- -- xx init \s2 -- -- xx init \y -- -- xxxx ---- -------------------- ---------- ---------- --------------- 1 \d 0 0 0000 1 \y -- -- xxxx ---- -------------------- ---------- ---------- --------------- 2 \d 1 1 0001 2 \y -- -- xxxx ---- -------------------- ---------- ---------- --------------- 3 \d 2 2 0010 3 \y 0 0 0000 ---- -------------------- ---------- ---------- --------------- 4 \d 3 3 0011 4 \y 1 1 0001 ---- -------------------- ---------- ---------- --------------- 5 \d -- -- 001x 5 \y 2 2 0010 ---- -------------------- ---------- ---------- --------------- 6 \d -- -- xxxx 6 \y 3 3 0011 \end{lstlisting} \caption{Solving a sequential SAT problem in the {\tt memdemo} module from Fig.~\ref{memdemo_src}.} \label{memdemo_sat} \end{figure} The SAT solver functionality in Yosys can not only be used to solve combinatorial problems, but can also solve sequential problems. Let's consider the entire {\tt memdemo} module from Fig.~\ref{memdemo_src} and suppose we want to know which sequence of input values for {\tt d} will cause the output {\tt y} to produce the sequence 1, 2, 3 from any initial state. Fig.~\ref{memdemo_sat} show the solution to this question, as produced by the following command: \begin{verbatim} sat -seq 6 -show y -show d -set-init-undef \ -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 \end{verbatim} The {\tt -seq 6} option instructs the {\tt sat} command to solve a sequential problem in 6 time steps. (Experiments with lower number of steps have show that at least 3 cycles are necessary to bring the circuit in a state from which the sequence 1, 2, 3 can be produced.) The {\tt -set-init-undef} option tells the {\tt sat} command to initialize all registers to the undef ({\tt x}) state. The way the {\tt x} state is treated in Verilog will ensure that the solution will work for any initial state. The {\tt -max\_undef} option instructs the {\tt sat} command to find a solution with a maximum number of undefs. This way we can see clearly which inputs bits are relevant to the solution. Finally the three {\tt -set-at} options add constraints for the {\tt y} signal to play the 1, 2, 3 sequence, starting with time step 4. It is not surprising that the solution sets {\tt d = 0} in the first step, as this is the only way of setting the {\tt s1} and {\tt s2} registers to a known value. The input values for the other steps are a bit harder to work out manually, but the SAT solver finds the correct solution in an instant. \medskip There is much more to write about the {\tt sat} command. For example, there is a set of options that can be used to performs sequential proofs using temporal induction \cite{tip}. The command {\tt help sat} can be used to print a list of all options with short descriptions of their functions. \section{Conclusion} \label{conclusion} Yosys provides a wide range of functions to analyze and investigate designs. For many cases it is sufficient to simply display circuit diagrams, maybe use some additional commands to narrow the scope of the circuit diagrams to the interesting parts of the circuit. But some cases require more than that. For this applications Yosys provides commands that can be used to further inspect the behavior of the circuit, either by evaluating which output values are generated from certain input values ({\tt eval}) or by evaluation which input values and initial conditions can result in a certain behavior at the outputs ({\tt sat}). The SAT command can even be used to prove (or disprove) theorems regarding the circuit, in more advanced cases with the additional help of a miter circuit. This features can be powerful tools for the circuit designer using Yosys as a utility for building circuits and the software developer using Yosys as a framework for new algorithms alike. \begin{thebibliography}{9} \bibitem{yosys} Clifford Wolf. The Yosys Open SYnthesis Suite. \url{http://www.clifford.at/yosys/} \bibitem{graphviz} Graphviz - Graph Visualization Software. \url{http://www.graphviz.org/} \bibitem{xdot} xdot.py - an interactive viewer for graphs written in Graphviz's dot language. \url{https://github.com/jrfonseca/xdot.py} \bibitem{CircuitSAT} {\it Circuit satisfiability problem} on Wikipedia \url{http://en.wikipedia.org/wiki/Circuit_satisfiability} \bibitem{MiniSAT} MiniSat: a minimalistic open-source SAT solver. \url{http://minisat.se/} \bibitem{tip} Niklas Een and Niklas Sörensson (2003). Temporal Induction by Incremental SAT Solving. \url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161} \end{thebibliography} \end{document}
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-31 12:02:07 +0000