Assume/Assert Cell Support

nmigen/__init__.py

@@ -1,4 +1,4 @@
-from .hdl.ast import Value, Const, C, Mux, Cat, Repl, Array, Signal, ClockSignal, ResetSignal
+from .hdl.ast import Value, Const, C, Mux, Cat, Repl, Array, Signal, ClockSignal, ResetSignal, Assert, Assume
 from .hdl.dsl import Module
 from .hdl.cd import ClockDomain
 from .hdl.ir import Fragment, Instance

nmigen/back/pysim.py

@@ -297,6 +297,12 @@ def run(state):
             lhs(state, normalize(rhs(state), shape))
         return run
 
+    def on_Assert(self, stmt):
+        raise NotImplementedError("Asserts not yet implemented for Simulator backend.") # :nocov:
+
+    def on_Assume(self, stmt):
+        pass # :nocov:
+
     def on_Switch(self, stmt):
         test  = self.rrhs_compiler(stmt.test)
         cases = []

nmigen/back/rtlil.py

@@ -565,6 +565,26 @@ def on_Assign(self, stmt):
                 stmt.rhs, lhs_bits, lhs_sign)
         self._case.assign(self.lhs_compiler(stmt.lhs), rhs_sigspec)
 
+    def on_Assert(self, stmt):
+        self(stmt._en.eq(1))
+        self(stmt._check.eq(stmt.test))
+        en_wire = self.rhs_compiler(stmt._en)
+        check_wire = self.rhs_compiler(stmt._check)
+        self.state.rtlil.cell("$assert", ports={
+            "\\A": check_wire,
+            "\\EN": en_wire,
+        }, params={ }, src=src(stmt.test.src_loc))
+
+    def on_Assume(self, stmt):
+        self(stmt._en.eq(1))
+        self(stmt._check.eq(stmt.test))
+        en_wire = self.rhs_compiler(stmt._en)
+        check_wire = self.rhs_compiler(stmt._check)
+        self.state.rtlil.cell("$assume", ports={
+            "\\A": check_wire,
+            "\\EN": en_wire,
+        }, params={ }, src=src(stmt.test.src_loc))
+
     def on_Switch(self, stmt):
         self._check_rhs(stmt.test)
 

nmigen/hdl/ast.py

@@ -12,8 +12,9 @@
     "Value", "Const", "C", "Operator", "Mux", "Part", "Slice", "Cat", "Repl",
     "Array", "ArrayProxy",
     "Signal", "ClockSignal", "ResetSignal",
-    "Statement", "Assign", "Switch", "Delay", "Tick", "Passive",
-    "ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict", "SignalSet",
+    "Statement", "Assign", "Assert", "Assume", "Switch", "Delay", "Tick",
+    "Passive", "ValueKey", "ValueDict", "ValueSet", "SignalKey", "SignalDict",
+    "SignalSet",
 ]
 
 
@@ -826,6 +827,65 @@ def __repr__(self):
         return "(eq {!r} {!r})".format(self.lhs, self.rhs)
 
 
+class Assert(Statement):
+    def __init__(self, test, _en=None, _check=None):
+        self.test = Value.wrap(test)
+        if _en is None:
+            self._en = Signal(1, reset_less=True,
+                              name="assert${}$en".format(src(self.test.src_loc)))
+            self._en.src_loc = self.test.src_loc
+        else:
+            self._en = _en
+
+        if _check is None:
+            self._check = Signal(1, reset_less=True,
+                                 name="assert${}$check".format(src(self.test.src_loc)))
+            self._check.src_loc = self.test.src_loc
+        else:
+            self._check = _check
+
+    def _lhs_signals(self):
+        return ValueSet((self._en, self._check))
+
+    def _rhs_signals(self):
+        return self.test._rhs_signals()
+
+    def __repr__(self):
+        return "(assert {!r})".format(self.test)
+
+
+def src(src_loc):
+    file, line = src_loc
+    return "{}:{}".format(file, line)
+
+
+class Assume(Statement):
+    def __init__(self, test, _en=None, _check=None):
+        self.test = Value.wrap(test)
+        if _en is None:
+            self._en = Signal(1, reset_less=True,
+                              name="assume${}$en".format(src(self.test.src_loc)))
+            self._en.src_loc = self.test.src_loc
+        else:
+            self._en = _en
+
+        if _check is None:
+            self._check = Signal(1, reset_less=True,
+                                 name="assume${}$check".format(src(self.test.src_loc)))
+        else:
+            self._check = _check
+            self._check.src_loc = self.test.src_loc
+
+    def _lhs_signals(self):
+        return ValueSet((self._en, self._check))
+
+    def _rhs_signals(self):
+        return self.test._rhs_signals()
+
+    def __repr__(self):
+        return "(assume {!r})".format(self.test)
+
+
 class Switch(Statement):
     def __init__(self, test, cases):
         self.test  = Value.wrap(test)

nmigen/hdl/dsl.py

@@ -336,9 +336,9 @@ def domain_name(domain):
             self._pop_ctrl()
 
         for assign in Statement.wrap(assigns):
-            if not compat_mode and not isinstance(assign, Assign):
+            if not compat_mode and not isinstance(assign, (Assign, Assert, Assume)):
                 raise SyntaxError(
-                    "Only assignments may be appended to d.{}"
+                    "Only assignments, asserts, and assumes may be appended to d.{}"
                     .format(domain_name(domain)))
 
             for signal in assign._lhs_signals():

nmigen/hdl/xfrm.py

@@ -141,6 +141,14 @@ class StatementVisitor(metaclass=ABCMeta):
     def on_Assign(self, stmt):
         pass # :nocov:
 
+    @abstractmethod
+    def on_Assert(self, stmt):
+        pass # :nocov:
+
+    @abstractmethod
+    def on_Assume(self, stmt):
+        pass # :nocov:
+
     @abstractmethod
     def on_Switch(self, stmt):
         pass # :nocov:
@@ -155,6 +163,10 @@ def on_unknown_statement(self, stmt):
     def on_statement(self, stmt):
         if type(stmt) is Assign:
             return self.on_Assign(stmt)
+        elif type(stmt) is Assert:
+            return self.on_Assert(stmt)
+        elif type(stmt) is Assume:
+            return self.on_Assume(stmt)
         elif isinstance(stmt, Switch):
             # Uses `isinstance()` and not `type() is` because nmigen.compat requires it.
             return self.on_Switch(stmt)
@@ -174,6 +186,12 @@ def on_value(self, value):
     def on_Assign(self, stmt):
         return Assign(self.on_value(stmt.lhs), self.on_value(stmt.rhs))
 
+    def on_Assert(self, stmt):
+        return Assert(self.on_value(stmt.test), _en=stmt._en, _check=stmt._check)
+
+    def on_Assume(self, stmt):
+        return Assume(self.on_value(stmt.test), _en=stmt._en, _check=stmt._check)
+
     def on_Switch(self, stmt):
         cases = OrderedDict((k, self.on_statement(s)) for k, s in stmt.cases.items())
         return Switch(self.on_value(stmt.test), cases)
@@ -294,6 +312,10 @@ class SwitchCleaner(StatementVisitor):
     def on_Assign(self, stmt):
         return stmt
 
+    on_Assert = on_Assign
+
+    on_Assume = on_Assign
+
     def on_Switch(self, stmt):
         cases = OrderedDict((k, self.on_statement(s)) for k, s in stmt.cases.items())
         if any(len(s) for s in cases.values()):
@@ -338,6 +360,10 @@ def groups(self):
     def on_Assign(self, stmt):
         self.unify(*stmt._lhs_signals())
 
+    on_Assert = on_Assign
+
+    on_Assume = on_Assign
+
     def on_Switch(self, stmt):
         for case_stmts in stmt.cases.values():
             self.on_statements(case_stmts)
@@ -362,6 +388,13 @@ def on_Assign(self, stmt):
         if any_lhs_signal in self.signals:
             return stmt
 
+    def on_Assert(self, stmt):
+        any_lhs_signal = next(iter(stmt._lhs_signals()))
+        if any_lhs_signal in self.signals:
+            return stmt
+
+    on_Assume = on_Assert
+
 
 class _ControlInserter(FragmentTransformer):
     def __init__(self, controls):

nmigen/test/test_hdl_dsl.py

@@ -74,7 +74,7 @@ def test_d_wrong(self):
     def test_d_asgn_wrong(self):
         m = Module()
         with self.assertRaises(SyntaxError,
-                msg="Only assignments may be appended to d.sync"):
+                msg="Only assignments, asserts, and assumes may be appended to d.sync"):
             m.d.sync += Switch(self.s1, {})
 
     def test_comb_wrong(self):