#!/usr/bin/env python3
import argparse
import sys
import random
from contextlib import contextmanager
# set to 'True' to compare verific with yosys
test_verific = False
@contextmanager
def redirect_stdout(new_target):
old_target, sys.stdout = sys.stdout, new_target
try:
yield new_target
finally:
sys.stdout = old_target
def random_expr(variables):
c = random.choice(['bin', 'uni', 'var', 'const'])
if c == 'bin':
op = random.choice(['+', '-', '*', '<', '<=', '==', '!=', '>=', '>', '<<', '>>', '<<<', '>>>', '|', '&', '^', '~^', '||', '&&'])
return "(%s %s %s)" % (random_expr(variables), op, random_expr(variables))
if c == 'uni':
op = random.choice(['+', '-', '~', '|', '&', '^', '~^', '!', '$signed', '$unsigned'])
return "%s(%s)" % (op, random_expr(variables))
if c == 'var':
return random.choice(variables)
if c == 'const':
bits = random.randint(1, 32)
return "%d'd%s" % (bits, random.randint(0, 2**bits-1))
raise AssertionError
parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG')
parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate')
args = parser.parse_args()
if args.seed is not None:
print("PRNG seed: %d" % args.seed)
random.seed(args.seed)
for idx in range(args.count):
with open('temp/uut_%05d.v' % idx, 'w') as f:
with redirect_stdout(f):
rst2 = random.choice([False, True])
if rst2:
print('module uut_%05d(clk, rst1, rst2, rst, a, b, c, x, y, z);' % (idx))
print(' input clk, rst1, rst2;')
print(' output rst;')
print(' assign rst = rst1 || rst2;')
else:
print('module uut_%05d(clk, rst, a, b, c, x, y, z);' % (idx))
print(' input clk, rst;')
variables=['a', 'b', 'c', 'x', 'y', 'z']
print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 31)))
print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 31)))
print(' input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 31)))
print(' output reg%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 31)))
print(' output reg%s [%d:0] y;' % (random.choice(['', ' signed']), random.randint(0, 31)))
print(' output reg%s [%d:0] z;' % (random.choice(['', ' signed']), random.randint(0, 31)))
state_bits = random.randint(5, 16);
print(' %sreg [%d:0] state;' % (random.choice(['', '(* fsm_encoding = "one-hot" *)',
'(* fsm_encoding = "binary" *)']), state_bits-1))
states=[]
for i in range(random.randint(2, 10)):
n = random.randint(0, 2**state_bits-1)
if n not in states:
states.append(n)
print(' always @(posedge clk) begin')
print(' if (%s) begin' % ('rst1' if rst2 else 'rst'))
print(' x <= %d;' % random.randint(0, 2**31-1))
print(' y <= %d;' % random.randint(0, 2**31-1))
print(' z <= %d;' % random.randint(0, 2**31-1))
print(' state <= %d;' % random.choice(states))
print(' end else begin')
print(' case (state)')
for state in states:
print(' %d: begin' % state)
for var in ('x', 'y', 'z'):
print(' %s <= %s;' % (var, random_expr(variables)))
next_states = states[:]
for i in range(random.randint(0, len(states))):
next_state = random.choice(next_states)
next_states.remove(next_state)
print(' if ((%s) %s (%s)) state <= %s;' % (random_expr(variables),
random.choice(['<', '<=', '>=', '>']), random_expr(variables), next_state))
print(' end')
print(' endcase')
if rst2:
print(' if (rst2) begin')
print(' x <= a;')
print(' y <= b;')
print(' z <= c;')
print(' state <= %d;' % random.choice(states))
print(' end')
print(' end')
print(' end')
print('endmodule')
with open('temp/uut_%05d.ys' % idx, 'w') as f:
with redirect_stdout(f):
if test_verific:
print('read_verilog temp/uut_%05d.v' % idx)
print('proc;; rename uut_%05d gold' % idx)
print('verific -vlog2k temp/uut_%05d.v' % idx)
print('verific -import uut_%05d' % idx)
print('rename uut_%05d gate' % idx)
else:
print('read_verilog temp/uut_%05d.v' % idx)
print('proc;;')
print('copy uut_%05d gold' % idx)
print('rename uut_%05d gate' % idx)
print('cd gate')
print('opt; wreduce; share%s; opt; fsm;;' % random.choice(['', ' -aggressive']))
print('cd ..')
print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter')
print('sat -verify-no-timeout -timeout 20 -seq 5 -set-at 1 %s_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter' % ('gold' if rst2 else 'in'))
9
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
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
/*
ChibiOS - Copyright (C) 2006..2018 Giovanni Di Sirio
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*/
#ifndef MCUCONF_H
#define MCUCONF_H
/*
* STM32L1xx drivers configuration.
* The following settings override the default settings present in
* the various device driver implementation headers.
* Note that the settings for each driver only have effect if the whole
* driver is enabled in halconf.h.
*
* IRQ priorities:
* 15...0 Lowest...Highest.
*
* DMA priorities:
* 0...3 Lowest...Highest.
*/
#define STM32L4xx_MCUCONF
/*
* HAL driver system settings.
*/
#define STM32_NO_INIT FALSE
#define STM32_VOS STM32_VOS_RANGE1
#define STM32_PVD_ENABLE FALSE
#define STM32_PLS STM32_PLS_LEV0
#define STM32_HSI16_ENABLED FALSE
#define STM32_LSI_ENABLED TRUE
#define STM32_HSE_ENABLED FALSE
#define STM32_LSE_ENABLED TRUE
#define STM32_MSIPLL_ENABLED TRUE
#define STM32_ADC_CLOCK_ENABLED TRUE
#define STM32_USB_CLOCK_ENABLED TRUE
#define STM32_SAI1_CLOCK_ENABLED TRUE
#define STM32_SAI2_CLOCK_ENABLED TRUE
#define STM32_MSIRANGE STM32_MSIRANGE_4M
#define STM32_MSISRANGE STM32_MSISRANGE_4M
#define STM32_SW STM32_SW_PLL
#define STM32_PLLSRC STM32_PLLSRC_MSI
#define STM32_PLLM_VALUE 1
#define STM32_PLLN_VALUE 80
#define STM32_PLLP_VALUE 7
#define STM32_PLLQ_VALUE 6
#define STM32_PLLR_VALUE 4
#define STM32_HPRE STM32_HPRE_DIV1
#define STM32_PPRE1 STM32_PPRE1_DIV1
#define STM32_PPRE2 STM32_PPRE2_DIV1
#define STM32_STOPWUCK STM32_STOPWUCK_MSI
#define STM32_MCOSEL STM32_MCOSEL_NOCLOCK
#define STM32_MCOPRE STM32_MCOPRE_DIV1
#define STM32_LSCOSEL STM32_LSCOSEL_NOCLOCK
#define STM32_PLLSAI1N_VALUE 72
#define STM32_PLLSAI1P_VALUE 7
#define STM32_PLLSAI1Q_VALUE 6
#define STM32_PLLSAI1R_VALUE 6
#define STM32_PLLSAI2N_VALUE 72
#define STM32_PLLSAI2P_VALUE 7
#define STM32_PLLSAI2R_VALUE 6
#define STM32_USART1SEL STM32_USART1SEL_SYSCLK
#define STM32_USART2SEL STM32_USART2SEL_SYSCLK
#define STM32_USART3SEL STM32_USART3SEL_SYSCLK
#define STM32_UART4SEL STM32_UART4SEL_SYSCLK
#define STM32_UART5SEL STM32_UART5SEL_SYSCLK
#define STM32_LPUART1SEL STM32_LPUART1SEL_SYSCLK
#define STM32_I2C1SEL STM32_I2C1SEL_SYSCLK
#define STM32_I2C2SEL STM32_I2C2SEL_SYSCLK
#define STM32_I2C3SEL STM32_I2C3SEL_SYSCLK
#define STM32_LPTIM1SEL STM32_LPTIM1SEL_PCLK1
#define STM32_LPTIM2SEL STM32_LPTIM2SEL_PCLK1
#define STM32_SAI1SEL STM32_SAI1SEL_OFF
#define STM32_SAI2SEL STM32_SAI2SEL_OFF
#define STM32_CLK48SEL STM32_CLK48SEL_PLLSAI1
#define STM32_ADCSEL STM32_ADCSEL_SYSCLK
#define STM32_SWPMI1SEL STM32_SWPMI1SEL_PCLK1
#define STM32_DFSDMSEL STM32_DFSDMSEL_PCLK1
#define STM32_RTCSEL STM32_RTCSEL_LSI
/*
* IRQ system settings.
*/
#define STM32_IRQ_EXTI0_PRIORITY 6
#define STM32_IRQ_EXTI1_PRIORITY 6
#define STM32_IRQ_EXTI2_PRIORITY 6
#define STM32_IRQ_EXTI3_PRIORITY 6
#define STM32_IRQ_EXTI4_PRIORITY 6
#define STM32_IRQ_EXTI5_9_PRIORITY 6
#define STM32_IRQ_EXTI10_15_PRIORITY 6
#define STM32_IRQ_EXTI1635_38_PRIORITY 6
#define STM32_IRQ_EXTI18_PRIORITY 6
#define STM32_IRQ_EXTI19_PRIORITY 6
#define STM32_IRQ_EXTI20_PRIORITY 6
#define STM32_IRQ_EXTI21_22_PRIORITY 15
/*
* ADC driver system settings.
*/
#define STM32_ADC_DUAL_MODE FALSE
#define STM32_ADC_COMPACT_SAMPLES FALSE
#define STM32_ADC_USE_ADC1 TRUE
#define STM32_ADC_USE_ADC2 TRUE
#define STM32_ADC_USE_ADC3 TRUE
#define STM32_ADC_ADC1_DMA_STREAM STM32_DMA_STREAM_ID(1, 1)
#define STM32_ADC_ADC2_DMA_STREAM STM32_DMA_STREAM_ID(1, 2)
#define STM32_ADC_ADC3_DMA_STREAM STM32_DMA_STREAM_ID(1, 3)
#define STM32_ADC_ADC1_DMA_PRIORITY 2
#define STM32_ADC_ADC2_DMA_PRIORITY 2
#define STM32_ADC_ADC3_DMA_PRIORITY 2
#define STM32_ADC_ADC12_IRQ_PRIORITY 5
#define STM32_ADC_ADC3_IRQ_PRIORITY 5
#define STM32_ADC_ADC1_DMA_IRQ_PRIORITY 5
#define STM32_ADC_ADC2_DMA_IRQ_PRIORITY 5
#define STM32_ADC_ADC3_DMA_IRQ_PRIORITY 5
#define STM32_ADC_ADC123_CLOCK_MODE ADC_CCR_CKMODE_AHB_DIV1
/*
* CAN driver system settings.
*/
#define STM32_CAN_USE_CAN1 FALSE
#define STM32_CAN_CAN1_IRQ_PRIORITY 11
/*
* DAC driver system settings.
*/
#define STM32_DAC_DUAL_MODE FALSE
#define STM32_DAC_USE_DAC1_CH1 FALSE
#define STM32_DAC_USE_DAC1_CH2 FALSE
#define STM32_DAC_DAC1_CH1_IRQ_PRIORITY 10
#define STM32_DAC_DAC1_CH2_IRQ_PRIORITY 10
#define STM32_DAC_DAC1_CH1_DMA_PRIORITY 2
#define STM32_DAC_DAC1_CH2_DMA_PRIORITY 2
#define STM32_DAC_DAC1_CH1_DMA_STREAM STM32_DMA_STREAM_ID(2, 4)
#define STM32_DAC_DAC1_CH2_DMA_STREAM STM32_DMA_STREAM_ID(1, 4)
/*
* GPT driver system settings.
*/
#define STM32_GPT_USE_TIM1 FALSE
#define STM32_GPT_USE_TIM2 FALSE
#define STM32_GPT_USE_TIM3 FALSE
#define STM32_GPT_USE_TIM4 FALSE
#define STM32_GPT_USE_TIM5 FALSE
#define STM32_GPT_USE_TIM6 FALSE
#define STM32_GPT_USE_TIM7 FALSE
#define STM32_GPT_USE_TIM8 FALSE
#define STM32_GPT_USE_TIM15 FALSE
#define STM32_GPT_USE_TIM16 FALSE
#define STM32_GPT_USE_TIM17 FALSE
#define STM32_GPT_TIM1_IRQ_PRIORITY 7
#define STM32_GPT_TIM2_IRQ_PRIORITY 7
#define STM32_GPT_TIM3_IRQ_PRIORITY 7
#define STM32_GPT_TIM4_IRQ_PRIORITY 7
#define STM32_GPT_TIM5_IRQ_PRIORITY 7
#define STM32_GPT_TIM6_IRQ_PRIORITY 7
#define STM32_GPT_TIM7_IRQ_PRIORITY 7
#define STM32_GPT_TIM8_IRQ_PRIORITY 7
#define STM32_GPT_TIM15_IRQ_PRIORITY 7
#define STM32_GPT_TIM16_IRQ_PRIORITY 7
#define STM32_GPT_TIM17_IRQ_PRIORITY 7
/*
* I2C driver system settings.
*/
#define STM32_I2C_USE_I2C1 FALSE
#define STM32_I2C_USE_I2C2 FALSE
#define STM32_I2C_USE_I2C3 FALSE
#define STM32_I2C_BUSY_TIMEOUT 50
#define STM32_I2C_I2C1_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 7)
#define STM32_I2C_I2C1_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 6)
#define STM32_I2C_I2C2_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 5)
#define STM32_I2C_I2C2_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 4)
#define STM32_I2C_I2C3_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 3)
#define STM32_I2C_I2C3_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 2)
#define STM32_I2C_I2C1_IRQ_PRIORITY 5
#define STM32_I2C_I2C2_IRQ_PRIORITY 5
#define STM32_I2C_I2C3_IRQ_PRIORITY 5
#define STM32_I2C_I2C1_DMA_PRIORITY 3
#define STM32_I2C_I2C2_DMA_PRIORITY 3
#define STM32_I2C_I2C3_DMA_PRIORITY 3
#define STM32_I2C_DMA_ERROR_HOOK(i2cp) osalSysHalt("DMA failure")
/*
* ICU driver system settings.
*/
#define STM32_ICU_USE_TIM1 FALSE
#define STM32_ICU_USE_TIM2 FALSE
#define STM32_ICU_USE_TIM3 FALSE
#define STM32_ICU_USE_TIM4 FALSE
#define STM32_ICU_USE_TIM5 FALSE
#define STM32_ICU_USE_TIM8 FALSE
#define STM32_ICU_TIM1_IRQ_PRIORITY 7
#define STM32_ICU_TIM2_IRQ_PRIORITY 7
#define STM32_ICU_TIM3_IRQ_PRIORITY 7
#define STM32_ICU_TIM4_IRQ_PRIORITY 7
#define STM32_ICU_TIM5_IRQ_PRIORITY 7
#define STM32_ICU_TIM8_IRQ_PRIORITY 7
/*
* PWM driver system settings.
*/
#define STM32_PWM_USE_ADVANCED FALSE
#define STM32_PWM_USE_TIM1 FALSE
#define STM32_PWM_USE_TIM2 FALSE
#define STM32_PWM_USE_TIM3 FALSE
#define STM32_PWM_USE_TIM4 FALSE
#define STM32_PWM_USE_TIM5 FALSE
#define STM32_PWM_USE_TIM8 FALSE
#define STM32_PWM_TIM1_IRQ_PRIORITY 7
#define STM32_PWM_TIM2_IRQ_PRIORITY 7
#define STM32_PWM_TIM3_IRQ_PRIORITY 7
#define STM32_PWM_TIM4_IRQ_PRIORITY 7
#define STM32_PWM_TIM5_IRQ_PRIORITY 7
#define STM32_PWM_TIM8_IRQ_PRIORITY 7
/*
* QSPI driver system settings.
*/
#define STM32_QSPI_USE_QUADSPI1 FALSE
#define STM32_QSPI_QUADSPI1_DMA_STREAM STM32_DMA_STREAM_ID(2, 7)
/*
* SDC driver system settings.
*/
#define STM32_SDC_USE_SDMMC1 FALSE
#define STM32_SDC_SDMMC_UNALIGNED_SUPPORT TRUE
#define STM32_SDC_SDMMC_WRITE_TIMEOUT 1000
#define STM32_SDC_SDMMC_READ_TIMEOUT 1000
#define STM32_SDC_SDMMC_CLOCK_DELAY 10
#define STM32_SDC_SDMMC1_DMA_PRIORITY 3
#define STM32_SDC_SDMMC1_IRQ_PRIORITY 9
#define STM32_SDC_SDMMC1_DMA_STREAM STM32_DMA_STREAM_ID(2, 4)
/*
* SERIAL driver system settings.
*/
#define STM32_SERIAL_USE_USART1 FALSE
#define STM32_SERIAL_USE_USART2 TRUE
#define STM32_SERIAL_USE_USART3 FALSE
#define STM32_SERIAL_USE_LPUART1 FALSE
#define STM32_SERIAL_USART1_PRIORITY 12
#define STM32_SERIAL_USART2_PRIORITY 12
#define STM32_SERIAL_USART3_PRIORITY 12
#define STM32_SERIAL_LPUART1_PRIORITY 12
/*
* SPI driver system settings.
*/
#define STM32_SPI_USE_SPI1 FALSE
#define STM32_SPI_USE_SPI2 FALSE
#define STM32_SPI_USE_SPI3 FALSE
#define STM32_SPI_SPI1_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 3)
#define STM32_SPI_SPI1_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 4)
#define STM32_SPI_SPI2_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 4)
#define STM32_SPI_SPI2_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 5)
#define STM32_SPI_SPI3_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 1)
#define STM32_SPI_SPI3_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 2)
#define STM32_SPI_SPI1_DMA_PRIORITY 1
#define STM32_SPI_SPI2_DMA_PRIORITY 1
#define STM32_SPI_SPI3_DMA_PRIORITY 1
#define STM32_SPI_SPI1_IRQ_PRIORITY 10
#define STM32_SPI_SPI2_IRQ_PRIORITY 10
#define STM32_SPI_SPI3_IRQ_PRIORITY 10
#define STM32_SPI_DMA_ERROR_HOOK(spip) osalSysHalt("DMA failure")
/*
* ST driver system settings.
*/
#define STM32_ST_IRQ_PRIORITY 8
#define STM32_ST_USE_TIMER 2
/*
* UART driver system settings.
*/
#define STM32_UART_USE_USART1 FALSE
#define STM32_UART_USE_USART2 FALSE
#define STM32_UART_USE_USART3 FALSE
#define STM32_UART_USE_UART4 FALSE
#define STM32_UART_USE_UART5 FALSE
#define STM32_UART_USE_LPUART1 FALSE
#define STM32_UART_USART1_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 7)
#define STM32_UART_USART1_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 6)
#define STM32_UART_USART2_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 6)
#define STM32_UART_USART2_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 7)
#define STM32_UART_USART3_RX_DMA_STREAM STM32_DMA_STREAM_ID(1, 3)
#define STM32_UART_USART3_TX_DMA_STREAM STM32_DMA_STREAM_ID(1, 2)
#define STM32_UART_UART4_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 5)
#define STM32_UART_UART4_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 3)
#define STM32_UART_UART5_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 2)
#define STM32_UART_UART5_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 1)
#define STM32_UART_LPUART1_RX_DMA_STREAM STM32_DMA_STREAM_ID(2, 7)
#define STM32_UART_LPUART1_TX_DMA_STREAM STM32_DMA_STREAM_ID(2, 6)
#define STM32_UART_USART1_IRQ_PRIORITY 12
#define STM32_UART_USART2_IRQ_PRIORITY 12
#define STM32_UART_USART3_IRQ_PRIORITY 12
#define STM32_UART_UART4_IRQ_PRIORITY 12
#define STM32_UART_UART5_IRQ_PRIORITY 12
#define STM32_UART_USART1_DMA_PRIORITY 0
#define STM32_UART_USART2_DMA_PRIORITY 0
#define STM32_UART_USART3_DMA_PRIORITY 0
#define STM32_UART_UART4_DMA_PRIORITY 0
#define STM32_UART_UART5_DMA_PRIORITY 0
#define STM32_UART_LPUART1_DMA_PRIORITY 0
#define STM32_UART_DMA_ERROR_HOOK(uartp) osalSysHalt("DMA failure")
/*
* USB driver system settings.
*/
#define STM32_USB_USE_OTG1 FALSE
#define STM32_USB_OTG1_IRQ_PRIORITY 14
#define STM32_USB_OTG1_RX_FIFO_SIZE 512
#define STM32_USB_OTG_THREAD_PRIO LOWPRIO
#define STM32_USB_OTG_THREAD_STACK_SIZE 128
#define STM32_USB_OTGFIFO_FILL_BASEPRI 0
/*
* WDG driver system settings.
*/
#define STM32_WDG_USE_IWDG FALSE
#endif /* MCUCONF_H */
|