diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index 604d04c7..73173391 100644
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -297,7 +297,14 @@ As verification properties become more complex and check longer sequences, the
 additional effort of hand-coding without SVA properties becomes much more
 difficult.  Using a parser such as Verific supports these checks *without*
 having to write out potentially complicated state machines. Verific is included
-for use in the *Tabby CAD Suite*.  
+for use in the *Tabby CAD Suite*.
+
+.. note::
+
+   The Verific frontend for Yosys requires the commercial `Tabby CAD Suite`_.
+   This is not the same as simply having a Verific license when using Yosys.
+
+.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet
 
 Further information
 *******************
diff --git a/docs/source/verific.rst b/docs/source/verific.rst
index 504c8000..87beb357 100644
--- a/docs/source/verific.rst
+++ b/docs/source/verific.rst
@@ -2,6 +2,14 @@
 SystemVerilog, VHDL, SVA
 ========================
 
+.. note::
+
+   This document describes features only available with the commercial `Tabby
+   CAD Suite`_ and the included Verific frontend. This is not the same as simply
+   having a Verific license when using Yosys.
+
+.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet
+
 Run ``verific -sv <files>`` in the ``[script]`` section of you ``.sby`` file
 to read a SystemVerilog source file, and ``verific -vhdl <files>`` to read a
 VHDL source file.
diff --git a/docs/source/verilog.rst b/docs/source/verilog.rst
index 474514eb..13f36c44 100644
--- a/docs/source/verilog.rst
+++ b/docs/source/verilog.rst
@@ -20,10 +20,10 @@ within the core.
    `endif
    endmodule
 
-The ``bind()`` operator can also be used when using the Verific front end.
-This will provide an option to attach formal properties to a given piece
-of logic, without actually modifying the module in question to do so as
-we did in the example above.
+The ``bind()`` operator can also be used when using the Verific front end. This
+will provide an option to attach formal properties to a given piece of logic,
+without actually modifying the module in question to do so as we did in the
+example above. Refer to :doc:`verific` for more on the Verific front end.
 
 SystemVerilog Immediate Assertions
 ----------------------------------