From 93e7e1d1e2d44d5db81e5161692915ade7cfdc21 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 23 Jun 2018 18:25:52 +0200
Subject: [PATCH] Improve documentation of scripts and Verific bindings

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 docs/source/reference.rst | 22 ++++++++++++++++------
 docs/source/verific.rst   |  9 ++++++++-
 docs/source/verilog.rst   | 27 ++++++++++++++++++++++-----
 3 files changed, 46 insertions(+), 12 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 1a61917..9ef84c1 100644
--- a/docs/source/reference.rst
+++ b/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``.
diff --git a/docs/source/verific.rst b/docs/source/verific.rst
index aa79f22..504c800 100644
--- a/docs/source/verific.rst
+++ b/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
 -----------------------------
 
diff --git a/docs/source/verilog.rst b/docs/source/verilog.rst
index 317dca9..d83b299 100644
--- a/docs/source/verilog.rst
+++ b/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`.
+
-- 
2.30.2