Hide keyboard shortcuts

Hot-keys on this page

r m x p   toggle line displays

j k   next/prev highlighted chunk

0   (zero) top of page

1   (one) first highlighted chunk

1# -------------------------------------------------------------------------------------------------- 

2# Copyright (c) Lukas Vik. All rights reserved. 

3# 

4# This file is part of the tsfpga project. 

5# https://tsfpga.com 

6# https://gitlab.com/tsfpga/tsfpga 

7# -------------------------------------------------------------------------------------------------- 

8 

9from fnmatch import fnmatch 

10from pathlib import Path 

11 

12from vunit import VUnitCLI, VUnit 

13from vunit.test.list import TestList 

14from vunit.test.runner import TestRunner 

15from vunit.test.report import TestReport 

16from vunit.color_printer import COLOR_PRINTER, NO_COLOR_PRINTER 

17 

18from tsfpga.yosys_project import YosysProject 

19from tsfpga.module import BaseModule 

20 

21 

22class FormalConfig: 

23 

24 # pylint: disable=too-many-arguments 

25 def __init__( 

26 self, top, generics=None, engine_command="smtbmc", solver_command="z3", mode="bmc", depth=20 

27 ): 

28 """ 

29 Arguments: 

30 top (str): Name of top level entity. 

31 generics (dict): Generics that will be applied to the top level. 

32 engine_command (str): Engine command, e.g. ``smtbmc --syn --nopresat`` 

33 solver_command (str): Solver command, e.g. 

34 ``z3 rewriter.cache_all=true opt.enable_sat=true`` 

35 mode (str): Typically ``bmc`` or ``prove``. 

36 depth (int): In ``bmc`` mode, this parameter is the depth of the bounded model 

37 check. In ``prove`` mode it is ignored for all engines except ``smtbmc`` 

38 where it is used as the depth for k-induction. 

39 """ 

40 self.top = top 

41 self.generics = None if generics is None else generics.copy() 

42 self.formal_settings = dict( 

43 engine_command=engine_command, solver_command=solver_command, mode=mode, depth=depth 

44 ) 

45 

46 @property 

47 def test_name(self): 

48 return BaseModule.test_case_name(self.top, self.generics) 

49 

50 

51class FormalProject: 

52 def __init__(self, project_path, modules): 

53 self._formal_config_list = [] 

54 self.project_path = project_path.resolve() 

55 self.modules = modules 

56 

57 def add_config(self, **kwargs): 

58 config = FormalConfig(**kwargs) 

59 self._formal_config_list.append(config) 

60 

61 def list_tests(self, test_filters="*"): 

62 test_list = self._create_test_list(test_filters) 

63 for test in test_list: 

64 print(test.name) 

65 print(f"Listed {test_list.num_tests} tests") 

66 

67 def run(self, num_threads=1, verbose=False, quiet=False, no_color=False, test_filters=None): 

68 # First, compile the source code and assign the compile result information to the 

69 # test objects. 

70 src_files, compiled_libraries = self._compile_source_code() 

71 test_list = self._create_test_list(test_filters) 

72 for test in test_list: 

73 # 'test' in this context is a TestCaseWrapper object. 

74 # Access the member to get the FormalTestCase object. 

75 # pylint: disable=protected-access 

76 test._test_case.set_src_files(src_files) 

77 # pylint: disable=protected-access 

78 test._test_case.set_compiled_libraries(compiled_libraries) 

79 

80 if verbose: 

81 verbosity = TestRunner.VERBOSITY_VERBOSE 

82 elif quiet: 

83 verbosity = TestRunner.VERBOSITY_QUIET 

84 else: 

85 verbosity = TestRunner.VERBOSITY_NORMAL 

86 

87 color_printer = NO_COLOR_PRINTER if no_color else COLOR_PRINTER 

88 report = TestReport(printer=color_printer) 

89 

90 # Run all the tests 

91 test_runner = TestRunner( 

92 report=report, 

93 output_path=self.project_path, 

94 verbosity=verbosity, 

95 num_threads=num_threads, 

96 no_color=no_color, 

97 ) 

98 test_runner.run(test_list) 

99 

100 return report.all_ok() 

101 

102 def _create_test_list(self, test_filters): 

103 test_list = TestList() 

104 for formal_config in self._formal_config_list: 

105 test_list.add_test(FormalTestCase(formal_config)) 

106 

107 def test_filter(name, attribute_names): # pylint: disable=unused-argument 

108 """ 

109 The ``attribute_names`` argument is used by VUnit in it's test filtering. 

110 We have no such concept, but the argument is needed so the function signature 

111 is correct. 

112 """ 

113 return any(fnmatch(name, test_name_filter) for test_name_filter in test_filters) 

114 

115 test_list.keep_matches(test_filter) 

116 

117 return test_list 

118 

119 def _compile_source_code(self, no_color=False): 

120 # Set up a VUnit project for compilation of sources 

121 args = VUnitCLI().parse_args(["--no-color", no_color]) 

122 args.output_path = self.project_path / "vunit_out" 

123 vunit_proj = VUnit.from_args(args=args) 

124 

125 src_files = [] 

126 compiled_libraries = [] 

127 

128 for module in self.modules: 

129 vunit_library = vunit_proj.add_library(module.library_name) 

130 compiled_libraries.append(args.output_path / "ghdl" / "libraries" / module.library_name) 

131 

132 for hdl_file in module.get_formal_files(): 

133 if hdl_file.is_vhdl: 

134 vunit_library.add_source_file(hdl_file.path) 

135 else: 

136 assert False, f"Can not handle this file: {hdl_file.path}" 

137 

138 src_files.append(hdl_file.path) 

139 

140 vunit_proj.set_compile_option("ghdl.a_flags", ["-fpsl", "-fsynopsys", "-frelaxed"]) 

141 vunit_proj._main_compile_only() # pylint: disable=protected-access 

142 

143 return src_files, compiled_libraries 

144 

145 

146class FormalTestCase: 

147 def __init__(self, formal_config): 

148 self._formal_config = formal_config 

149 self._src_files = None 

150 self._compiled_libraries = None 

151 

152 self._setup_unused_vunit_fields() 

153 

154 def _setup_unused_vunit_fields(self): 

155 """ 

156 Setup fields that are needed in a test case for VUnit test handling to work. 

157 These are unused by us. I think we are mimicking a IndependentSimTestCase object. 

158 """ 

159 self.attribute_names = set() 

160 

161 class TestConfiguration: 

162 

163 attributes = dict() 

164 

165 self.test_configuration = TestConfiguration() 

166 

167 @property 

168 def name(self): 

169 return self._formal_config.test_name 

170 

171 def set_src_files(self, src_files): 

172 self._src_files = src_files 

173 

174 def set_compiled_libraries(self, compiled_libraries): 

175 self._compiled_libraries = compiled_libraries 

176 

177 def run(self, output_path, read_output): # pylint: disable=unused-argument 

178 """ 

179 VUnit test runner sends another argument "read_output" which we don't use. 

180 It can be used to read back the STDOUTput from a test. Typically used in a post 

181 test hook. 

182 """ 

183 # If these have not been set there is something procedurally wrong 

184 if self._src_files is None: 

185 raise ValueError("FormalTestCase missing source files") 

186 if self._compiled_libraries is None: 

187 raise ValueError("FormalTestCase missing compiled libraries") 

188 

189 output_path = Path(output_path) 

190 

191 project = YosysProject( 

192 top=self._formal_config.top, 

193 generics=self._formal_config.generics, 

194 formal_settings=self._formal_config.formal_settings, 

195 ) 

196 

197 test_ok = project.run_formal( 

198 project_path=output_path, 

199 src_files=self._src_files, 

200 compiled_libraries=self._compiled_libraries, 

201 ) 

202 

203 if not test_ok: 

204 self._print_trace_help(output_path) 

205 

206 return test_ok 

207 

208 @staticmethod 

209 def _print_trace_help(output_path): 

210 """ 

211 Prints the location of trace files, if any available. 

212 """ 

213 message = "\n\nFormal test case failed. " 

214 vcd_files = list(output_path.glob("**/*.vcd")) 

215 if vcd_files: 

216 message += "You might want to inspect the trace file(s):" 

217 print(message) 

218 for vcd_file in vcd_files: 

219 print(f" gtkwave {vcd_file} &") 

220 else: 

221 message += ( 

222 "There does not seem to be any trace files available for inspection. " 

223 "Please see log output instead." 

224 ) 

225 print(message)