#!/usr/bin/env python3
import argparse
import sys
import random
from contextlib import contextmanager
@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_plus_x():
return "%s x" % random.choice(['+', '+', '+', '-', '-', '|', '&', '^'])
def maybe_plus_x(expr):
if random.randint(0, 4) == 0:
return "(%s %s)" % (expr, random_plus_x())
else:
return expr
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 = 100, 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):
if random.choice(['bin', 'uni']) == 'bin':
print('module uut_%05d(a, b, c, d, x, s, y);' % (idx))
op = random.choice([
random.choice(['+', '-', '*', '/', '%']),
random.choice(['<', '<=', '==', '!=', '===', '!==', '>=', '>' ]),
random.choice(['<<', '>>', '<<<', '>>>']),
random.choice(['|', '&', '^', '~^', '||', '&&']),
])
print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] d;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input s;')
print(' output [%d:0] y;' % random.randint(0, 8))
print(' assign y = (s ? %s(%s %s %s) : %s(%s %s %s))%s;' %
(random.choice(['', '$signed', '$unsigned']), maybe_plus_x('a'), op, maybe_plus_x('b'),
random.choice(['', '$signed', '$unsigned']), maybe_plus_x('c'), op, maybe_plus_x('d'),
random_plus_x() if random.randint(0, 4) == 0 else ''))
print('endmodule')
else:
print('module uut_%05d(a, b, x, s, y);' % (idx))
op = random.choice(['~', '-', '!'])
print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8)))
print(' input s;')
print(' output [%d:0] y;' % random.randint(0, 8))
print(' assign y = (s ? %s(%s%s) : %s(%s%s))%s;' %
(random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('a'),
random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('b'),
random_plus_x() if random.randint(0, 4) == 0 else ''))
print('endmodule')
with open('temp/uut_%05d.ys' % idx, 'w') as f:
with redirect_stdout(f):
print('read_verilog temp/uut_%05d.v' % idx)
print('proc;;')
print('copy uut_%05d gold' % idx)
print('rename uut_%05d gate' % idx)
print('tee -a temp/all_share_log.txt log')
print('tee -a temp/all_share_log.txt log #job# uut_%05d' % idx)
print('tee -a temp/all_share_log.txt wreduce')
print('tee -a temp/all_share_log.txt share -aggressive gate')
print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter')
print('sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter')
6' href='#n6'>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
/*-----------------------------------------------------------------------*/
/* Low level disk I/O module skeleton for FatFs (C)ChaN, 2007 */
/*-----------------------------------------------------------------------*/
/* This is a stub disk I/O module that acts as front end of the existing */
/* disk I/O modules and attach it to FatFs module with common interface. */
/*-----------------------------------------------------------------------*/
#include "diskio.h"
/*-----------------------------------------------------------------------*/
/* Initialize a Drive */
DSTATUS disk_initialize (
BYTE drv /* Physical drive number (0..) */
)
{
return FR_OK;
}
/*-----------------------------------------------------------------------*/
/* Return Disk Status */
DSTATUS disk_status (
BYTE drv /* Physical drive number (0..) */
)
{
return FR_OK;
}
/*-----------------------------------------------------------------------*/
/* Read Sector(s) */
DRESULT disk_read (
BYTE drv, /* Physical drive number (0..) */
BYTE *buff, /* Data buffer to store read data */
DWORD sector, /* Sector address (LBA) */
BYTE count /* Number of sectors to read (1..128) */
)
{
DataflashManager_ReadBlocks_RAM(sector, count, buff);
return RES_OK;
}
/*-----------------------------------------------------------------------*/
/* Write Sector(s) */
#if _READONLY == 0
DRESULT disk_write (
BYTE drv, /* Physical drive number (0..) */
const BYTE *buff, /* Data to be written */
DWORD sector, /* Sector address (LBA) */
BYTE count /* Number of sectors to write (1..128) */
)
{
DataflashManager_WriteBlocks_RAM(sector, count, buff);
return RES_OK;
}
#endif /* _READONLY */
/*-----------------------------------------------------------------------*/
/* Miscellaneous Functions */
DRESULT disk_ioctl (
BYTE drv, /* Physical drive number (0..) */
BYTE ctrl, /* Control code */
void *buff /* Buffer to send/receive control data */
)
{
if (ctrl == CTRL_SYNC)
return RES_OK;
else
return RES_PARERR;
}
DWORD get_fattime (void)
{
TimeDate_t CurrTimeDate;
RTC_GetTimeDate(&CurrTimeDate);
return ((DWORD)(20 + CurrTimeDate.Year) << 25) |
((DWORD)CurrTimeDate.Month << 21) |
((DWORD)CurrTimeDate.Day << 16) |
((DWORD)CurrTimeDate.Hour << 11) |
((DWORD)CurrTimeDate.Minute << 5) |
(((DWORD)CurrTimeDate.Second >> 1) << 0);
}
|