Add note on docs to clarify verific support

Having a verific license does not provide access to the verific frontend. This helps to make that clearer.

docs/source/quickstart.rst

@@ -299,6 +299,13 @@ 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*.
 
+.. 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
 *******************
 For more information on the uses of assertions and the difference between

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.

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.
+The ``bind()`` operator can also be used when using the Verific front end. This
-This will provide an option to attach formal properties to a given piece
+will provide an option to attach formal properties to a given piece of logic,
-of logic, without actually modifying the module in question to do so as
+without actually modifying the module in question to do so as we did in the
-we did in the example above.
+example above. Refer to :doc:`verific` for more on the Verific front end.
 
 SystemVerilog Immediate Assertions
 ----------------------------------