Implement RFC 50: Print and string formatting.

Co-authored-by: Catherine <whitequark@whitequark.org>

docs/changes.rst

@@ -35,6 +35,8 @@ Apply the following changes to code written against Amaranth 0.4 to migrate it t
 * Convert uses of ``Simulator.add_sync_process`` used as testbenches to ``Simulator.add_testbench``
 * Convert other uses of ``Simulator.add_sync_process`` to ``Simulator.add_process``
 * Replace uses of ``amaranth.hdl.Memory`` with ``amaranth.lib.memory.Memory``
+* Replace imports of ``amaranth.asserts.{Assert, Assume, Cover}`` with imports from ``amaranth.hdl``
+* Remove any usage of ``name=`` with assertions, possibly replacing them with custom messages
 
 
 Implemented RFCs
@@ -46,6 +48,7 @@ Implemented RFCs
 .. _RFC 43: https://amaranth-lang.org/rfcs/0043-rename-reset-to-init.html
 .. _RFC 45: https://amaranth-lang.org/rfcs/0045-lib-memory.html
 .. _RFC 46: https://amaranth-lang.org/rfcs/0046-shape-range-1.html
+.. _RFC 50: https://amaranth-lang.org/rfcs/0050-print.html
 
 * `RFC 17`_: Remove ``log2_int``
 * `RFC 27`_: Testbench processes for the simulator
@@ -53,6 +56,7 @@ Implemented RFCs
 * `RFC 43`_: Rename ``reset=`` to ``init=``
 * `RFC 45`_: Move ``hdl.Memory`` to ``lib.Memory``
 * `RFC 46`_: Change ``Shape.cast(range(1))`` to ``unsigned(0)``
+* `RFC 50`_: ``Print`` statement and string formatting
 
 
 Language changes
@@ -62,6 +66,7 @@ Language changes
 
 * Added: :class:`ast.Slice` objects have been made const-castable.
 * Added: :func:`amaranth.utils.ceil_log2`, :func:`amaranth.utils.exact_log2`. (`RFC 17`_)
+* Added: :class:`Format` objects, :class:`Print` statements, messages in :class:`Assert`, :class:`Assume` and :class:`Cover`. (`RFC 50`_)
 * Changed: ``m.Case()`` with no patterns is never active instead of always active. (`RFC 39`_)
 * Changed: ``Value.matches()`` with no patterns is ``Const(0)`` instead of ``Const(1)``. (`RFC 39`_)
 * Changed: ``Signal(range(stop), init=stop)`` warning has been changed into a hard error and made to trigger on any out-of range value.
@@ -69,11 +74,13 @@ Language changes
 * Changed: ``Shape.cast(range(1))`` is now ``unsigned(0)``. (`RFC 46`_)
 * Changed: the ``reset=`` argument of :class:`Signal`, :meth:`Signal.like`, :class:`amaranth.lib.wiring.Member`, :class:`amaranth.lib.cdc.FFSynchronizer`, and ``m.FSM()`` has been renamed to ``init=``. (`RFC 43`_)
 * Changed: :class:`Shape` has been made immutable and hashable.
+* Changed: :class:`Assert`, :class:`Assume`, :class:`Cover` have been moved to :mod:`amaranth.hdl` from :mod:`amaranth.asserts`. (`RFC 50`_)
 * Deprecated: :func:`amaranth.utils.log2_int`. (`RFC 17`_)
 * Deprecated: :class:`amaranth.hdl.Memory`. (`RFC 45`_)
 * Removed: (deprecated in 0.4) :meth:`Const.normalize`. (`RFC 5`_)
 * Removed: (deprecated in 0.4) :class:`Repl`. (`RFC 10`_)
 * Removed: (deprecated in 0.4) :class:`ast.Sample`, :class:`ast.Past`, :class:`ast.Stable`, :class:`ast.Rose`, :class:`ast.Fell`.
+* Removed: assertion names in :class:`Assert`, :class:`Assume` and :class:`Cover`. (`RFC 50`_)
 
 
 Standard library changes
@@ -91,6 +98,7 @@ Toolchain changes
 -----------------
 
 * Added: ``Simulator.add_testbench``. (`RFC 27`_)
+* Added: support for :class:`amaranth.hdl.Assert` in simulation. (`RFC 50`_)
 * Deprecated: ``Settle`` simulation command. (`RFC 27`_)
 * Deprecated: ``Simulator.add_sync_process``. (`RFC 27`_)
 * Removed: (deprecated in 0.4) use of mixed-case toolchain environment variable names, such as ``NMIGEN_ENV_Diamond`` or ``AMARANTH_ENV_Diamond``; use upper-case environment variable names, such as ``AMARANTH_ENV_DIAMOND``.

docs/guide.rst

@@ -938,6 +938,8 @@ Every signal included in the target of an assignment becomes a part of the domai
 
    The answer is no. While this kind of code is occasionally useful, rejecting it greatly simplifies backends, simulators, and analyzers.
 
+In addition to assignments, :ref:`assertions, assumptions <lang-asserts>`, and :ref:`debug prints <lang-print>` can be added using the same syntax.
+
 
 .. _lang-assignorder:
 
@@ -1287,6 +1289,89 @@ Consider the following code:
 Whenever there is a transition on the clock of the ``sync`` domain, the :py:`timer` signal is incremented by one if :py:`up` is true, decremented by one if :py:`down` is true, and retains its value otherwise.
 
 
+.. _lang-assert:
+
+Assertions
+==========
+
+Some properties are so important that if they are violated, the computations described by the design become meaningless. These properties should be guarded with an :class:`Assert` statement that immediately terminates the simulation if its condition is false. Assertions should generally be added to a :ref:`synchronous domain <lang-sync>`, and may have an optional message printed when it is violated:
+
+.. testcode::
+
+    ip = Signal(16)
+    m.d.sync += Assert(ip < 128, "instruction pointer past the end of program code!")
+
+Assertions may be nested within a :ref:`control block <lang-control>`:
+
+.. testcode::
+    :hide:
+
+    booting = Signal()
+
+.. testcode::
+
+    with m.If(~booting):
+        m.d.sync += Assert(ip < 128)
+
+.. warning::
+
+    While is is also possible to add assertions to the :ref:`combinatorial domain <lang-comb>`, simulations of combinatorial circuits may have *glitches*: instantaneous, transient changes in the values of expressions that are being computed which do not affect the result of the computation (and are not visible in most waveform viewers for that reason). Depending on the tools used for simulation, a glitch in the condition of an assertion or of a :ref:`control block <lang-control>` that contains it may cause the simulation to be terminated, even if the glitch would have been instantaneously resolved afterwards.
+
+    If the condition of an assertion is assigned in a synchronous domain, then it is safe to add that assertion in the combinatorial domain. For example, neither of the assertions in the example below will be violated due to glitches, regardless of which domain the :py:`ip` and :py:`booting` signals are driven by:
+
+    .. testcode::
+
+        ip_sync = Signal.like(ip)
+        m.d.sync += ip_sync.eq(ip)
+
+        m.d.comb += Assert(ip_sync < 128)
+        with m.If(booting):
+            m.d.comb += Assert(ip_sync < 128)
+
+    Assertions should be added in a :ref:`synchronous domain <lang-sync>` when possible. In cases where it is not, such as if the condition is a signal that is assigned in a synchronous domain elsewhere, care should be taken while adding the assertion to the combinatorial domain.
+
+
+.. _lang-print:
+
+Debug printing
+==============
+
+The value of any expression, or of several of them, can be printed to the terminal during simulation using the :class:`Print` statement. When added to the :ref:`combinatorial domain <lang-comb>`, the value of an expression is printed whenever it changes:
+
+.. testcode::
+
+    state = Signal()
+    m.d.comb += Print(state)
+
+When added to a :ref:`synchronous domain <lang-sync>`, the value of an expression is printed whenever the active edge occurs on the clock of that domain:
+
+.. testcode::
+
+    m.d.sync += Print("on tick: ", state)
+
+The :class:`Print` statement, regardless of the domain, may be nested within a :ref:`control block <lang-control>`:
+
+.. testcode::
+
+    old_state = Signal.like(state)
+    m.d.sync += old_state.eq(state)
+    with m.If(state != old_state):
+        m.d.sync += Print("was: ", old_state, "now: ", state)
+
+The arguments to the :class:`Print` statement have the same meaning as the arguments to the Python :func:`print` function, with the exception that only :py:`sep` and :py:`end` keyword arguments are supported. In addition, the :class:`Format` helper can be used to apply formatting to the values, similar to the Python :meth:`str.format` method:
+
+.. testcode::
+
+    addr = Signal(32)
+    m.d.sync += Print(Format("address: {:08x}", addr))
+
+In both :class:`Print` and :class:`Format`, arguments that are not Amaranth :ref:`values <lang-values>` are formatted using the usual Python rules. The optional second :py:`message` argument to :class:`Assert` (described :ref:`above <lang-assert>`) also accepts a string or the :class:`Format` helper:
+
+.. testcode::
+
+    m.d.sync += Assert((addr & 0b111) == 0, message=Format("unaligned address {:08x}!", addr))
+
+
 .. _lang-clockdomains:
 
 Clock domains

docs/reference.rst

@@ -63,6 +63,9 @@ The prelude exports exactly the following names:
 * :class:`Signal`
 * :class:`ClockSignal`
 * :class:`ResetSignal`
+* :class:`Format`
+* :class:`Print`
+* :func:`Assert`
 * :class:`Module`
 * :class:`ClockDomain`
 * :class:`Elaboratable`