Improve documentation of scripts and Verific bindings

Signed-off-by: Clifford Wolf <clifford@clifford.at>

docs/source/reference.rst

@@ -95,10 +95,10 @@ combinations of some host implementations A and B and device implementations X a
    live: aiger suprove
 
    [script]
-   hostA: read_verilog hostA.v
-   hostB: read_verilog hostB.v
-   deviceX: read_verilog deviceX.v
-   deviceY: read_verilog deviceY.v
+   hostA: read -sv hostA.v
+   hostB: read -sv hostB.v
+   deviceX: read -sv deviceX.v
+   deviceY: read -sv deviceY.v
    ...
 
 The ``[tasks]`` section must appear in the ``.sby`` file before the first
@@ -286,10 +286,11 @@ design file ``mytest.sv`` with the top-module ``mytest``:
 .. code-block:: text
 
    [script]
-   read_verilog -sv mytest.sv
+   read -sv mytest.sv
    prep -top mytest
 
-Or using the Verific SystemVerilog parser:
+Or explicitly using the Verific SystemVerilog parser (default for ``read -sv``
+when Yosys is built with Verific support):
 
 .. code-block:: text
 
@@ -298,6 +299,15 @@ Or using the Verific SystemVerilog parser:
    verific -import mytest
    prep -top mytest
 
+Or explicitly using the native Yosys Verilog parser (default for ``read -sv``
+when Yosys is not built with Verific support):
+
+.. code-block:: text
+
+   [script]
+   read_verilog -sv mytest.sv
+   prep -top mytest
+
 Run ``yosys`` in a terminal window and enter ``help`` on the Yosys prompt
 for a command list. Run ``help <command>`` for a detailed description of the
 command, for example ``help prep``.

docs/source/verific.rst

@@ -7,11 +7,18 @@ to read a SystemVerilog source file, and ``verific -vhdl <files>`` to read a
 VHDL source file.
 
 After all source files have been read, run ``verific -import <topmodule>``
-to import the design elaborated at the specified top module.
+to import the design elaborated at the specified top module. This step is
+optional (will be performed automatically) if the top-level module of
+your design has been read using Verific.
+
+Use ``read -sv`` to automatically use Verific to read a source file if Yosys
+has been built with Verific.
 
 Run ``yosys -h verific`` in a terminal window and enter for more information
 on the ``verific`` script command.
 
+.. _sva:
+
 Supported SVA Property Syntax
 -----------------------------
 

docs/source/verilog.rst

@@ -4,7 +4,9 @@ Formal extensions to Verilog
 
 TBD
 
-``read_verilog -formal``
+``read -sv``
+
+``read_verilog -sv``
 
 SystemVerilog Immediate Assertions
 ----------------------------------
@@ -33,17 +35,32 @@ Liveness and Fairness
 
 TBD
 
-``assert(eventually <expr>);``
+``assert property (eventually <expr>);``
 
-``assume(eventually <expr>);``
+``assume property (eventually <expr>);``
 
 Unconstrained Variables
 -----------------------
 
 TBD
 
-Nonstandard Extensions in Yosys
--------------------------------
+``(* anyconst *)``
+
+``(* anyseq *)``
+
+``(* allconst *)``
+
+``(* allseq *)``
+
+Global Clock
+------------
 
 TBD
 
+``(* gclk *)``
+
+SystemVerilog Concurrent Assertions
+-----------------------------------
+
+TBD, see :ref:`sva`.
+