add some example code for loading various constructs

examples/defines/defines.svh

@@ -0,0 +1 @@
+parameter N = 4;

examples/defines/includes/include.svh

@@ -0,0 +1 @@
+`define IDX0 2

examples/defines/readme

@@ -0,0 +1,9 @@
+This example demonstrates three common ways of defining values.
+
+1. include.svh: Definitions that are in a file that is included using an `include directive. It will look for these in the directory where yosys is run, which for sby is the src/ directory, so listing in [files] should be enough. If you give destination names to place the files within subdirectories inside src/ (like for the `foo/bar.sv /data/prj42/modules/foobar.sv` example in the documentation) you may need to add a command `verific -vlog-incdir foo` at the beginning of the script to tell it to also look for include files in the src/foo/ subdirectory.
+
+2. defines.svh: Definitions that are just in a separate file that is not included using `include. These are only visible within the same compilation unit, so you need to list this file and any file that needs the definitions in the same line: `verific -sv defines.svh top.sv`.
+
+3. Macro definitions that are set directly from the script: these are set using the command `verific -vlog-define MACRO=value`
+
+Also, a small side note, you can choose between two commands to load files, `read` and `verific`. `read` has a simplified interface for basic loading, `verific` has more advanced configuration options. We recommend to never mix the two within the same script, either use only `read` or only `verific`. If you want to use `read`, the corresponding commands for the above would be `read -incdir foo` and `read -define MACRO=value`.

examples/defines/script.ys

@@ -0,0 +1,6 @@
+verific -vlog-incdir includes
+verific -vlog-define IDX1=1
+verific -sv defines.svh top.sv
+hierarchy -top top
+clean
+show

examples/defines/top.sv

@@ -0,0 +1,7 @@
+`include "include.svh"
+
+module top(input [N-1:0] i, output o);
+
+assign o = i[ `IDX0 ] & i[ `IDX1 ];
+
+endmodule

examples/sby_blackboxing/readme

@@ -0,0 +1,18 @@
+Our tools handle this a bit differently than you may be used to. At the end of the [script] section, SBY will perform a check to make sure there are no blackboxes in the design, and error out if it finds any. But it is still possible to achieve the same goal, the process is as follows:
+
+- First, if you do not want to load the files for the modules B, C and D at all (e.g. if you don't have the files, or it takes a long time to load), you still need to substitute a blackbox declaration so that the tool knows which ports are input and which ports are output. In VHDL, having a component declaration in the preamble of the instantiating entity is sufficient for this, but in SystemVerilog you need to add a different file that has some declarations like this:
+
+(* blackbox *)
+module B (input foo, output bar);
+endmodule
+
+If you are ok with loading the files but just want to exclude the contents of the modules for the compilation process, you can skip this step and just do the next part.
+
+- Now, once you have loaded the design, you need to tell the tool that you want to actually remove all instances of these modules from the design and leave their outputs unconstrained. To do this you can use the `cutpoint` followed by the `delete` command for each blackbox module:
+
+cutpoint t:B t:C t:D
+delete t:B t:C t:D
+
+Note that these commands need to be after the design is loaded (either with `hierarchy -top` or `verific -import`), but they can be before `prep`.
+
+In the case where a non-blackbox module is instantiated with non-default parameters, the full name with the parameter values as it is printed during import is needed, but you can use * wildcard to pattern match on the module name, e.g. t:B*. (For full documentation on all the ways you can select design elements in yosys, you can consult this documentation section: https://yosyshq.readthedocs.io/projects/yosys/en/manual-rewrite/using_yosys/more_scripting/selections.html For example, you can target only specific instances of a module using c:inst_name syntax.)

examples/sby_blackboxing/top.sby

@@ -0,0 +1,21 @@
+[tasks]
+cover
+prove
+
+[options]
+cover: mode cover
+prove: mode prove
+depth 10
+
+[engines]
+smtbmc yices
+
+[script]
+verific -sv top.v
+hierarchy -top top
+cutpoint t:Delay* t:Unknown
+delete t:Delay* t:Unknown
+prep
+
+[files]
+top.v

examples/sby_blackboxing/top.v

@@ -0,0 +1,45 @@
+module top(input clk, input en, output [3:0] count);
+
+wire dut_en, d1, d2;
+
+DUT dut_i (.clk(clk), .en(dut_en), .count(count));
+
+Delay delay_i (.i(en), .o(d1));
+Delay #(.PARAM(42)) delay42_i (.i(d1), .o(d2));
+Unknown bb_i (.i(d2), .o(dut_en));
+
+always @(posedge clk ) begin
+    assert (count < 4'd6);
+    cover (count == 4'd5);
+end
+
+endmodule
+
+module DUT (input clk, input en, output [3:0] count);
+
+    reg [3:0] c = 4'd0;
+
+    always @(posedge clk) begin
+        if (en)
+            if (c == 5)
+                c <= 4'd0;
+            else
+                c <= c + 4'd1;
+    end
+
+    assign count = c;
+
+endmodule
+
+module Delay #(parameter PARAM = 0) (input clk, input i, output o);
+    reg [PARAM:0] r;
+    assign o = r[PARAM];
+
+    always @(posedge clk) begin
+        r <= {r[PARAM-1:0], i};
+    end
+endmodule
+
+(* blackbox *)
+module Unknown (input i, output o);
+endmodule