From 334869ab28f980b01148fd5fe004b60e20e0a86b Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Wed, 19 Aug 2020 11:49:55 +0800 Subject: [PATCH] Add option to specify solver in nmigen.test.utils --- nmigen/test/utils.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/nmigen/test/utils.py b/nmigen/test/utils.py index c3907ce8..41241275 100644 --- a/nmigen/test/utils.py +++ b/nmigen/test/utils.py @@ -53,7 +53,7 @@ def assertWarns(self, category, msg=None): if msg is not None: self.assertEqual(str(warns[0].message), msg) - def assertFormal(self, spec, mode="bmc", depth=1): + def assertFormal(self, spec, mode="bmc", depth=1, engine="smtbmc"): caller, *_ = traceback.extract_stack(limit=2) spec_root, _ = os.path.splitext(caller.filename) spec_dir = os.path.dirname(spec_root) @@ -80,7 +80,7 @@ def assertFormal(self, spec, mode="bmc", depth=1): wait on [engines] - smtbmc + {engine} [script] read_ilang top.il @@ -92,6 +92,7 @@ def assertFormal(self, spec, mode="bmc", depth=1): """).format( mode=mode, depth=depth, + engine=engine, script=script, rtlil=rtlil.convert(Fragment.get(spec, platform="formal")) )