From 0a6b3a9ebb3de6dcb6d28182e4a7ca8be2049122 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Fri, 15 Mar 2024 11:59:07 +0100
Subject: [PATCH 1/2] add example for blackboxing submodules

---
 examples/sby_blackboxing/readme  | 18 +++++++++++++
 examples/sby_blackboxing/top.sby | 21 +++++++++++++++
 examples/sby_blackboxing/top.v   | 45 ++++++++++++++++++++++++++++++++
 3 files changed, 84 insertions(+)
 create mode 100644 examples/sby_blackboxing/readme
 create mode 100644 examples/sby_blackboxing/top.sby
 create mode 100644 examples/sby_blackboxing/top.v

diff --git a/examples/sby_blackboxing/readme b/examples/sby_blackboxing/readme
new file mode 100644
index 0000000..75a0ce0
--- /dev/null
+++ b/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.)
diff --git a/examples/sby_blackboxing/top.sby b/examples/sby_blackboxing/top.sby
new file mode 100644
index 0000000..37b1eec
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/examples/sby_blackboxing/top.v b/examples/sby_blackboxing/top.v
new file mode 100644
index 0000000..102d814
--- /dev/null
+++ b/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
\ No newline at end of file

From bec7fe92945d476db9d6c2b2280c535263879b8e Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Fri, 15 Mar 2024 12:00:56 +0100
Subject: [PATCH 2/2] add example for various ways of importing defines

---
 examples/defines/defines.svh          | 1 +
 examples/defines/includes/include.svh | 1 +
 examples/defines/readme               | 9 +++++++++
 examples/defines/script.ys            | 6 ++++++
 examples/defines/top.sv               | 7 +++++++
 5 files changed, 24 insertions(+)
 create mode 100644 examples/defines/defines.svh
 create mode 100644 examples/defines/includes/include.svh
 create mode 100644 examples/defines/readme
 create mode 100644 examples/defines/script.ys
 create mode 100644 examples/defines/top.sv

diff --git a/examples/defines/defines.svh b/examples/defines/defines.svh
new file mode 100644
index 0000000..44b1f65
--- /dev/null
+++ b/examples/defines/defines.svh
@@ -0,0 +1 @@
+parameter N = 4;
\ No newline at end of file
diff --git a/examples/defines/includes/include.svh b/examples/defines/includes/include.svh
new file mode 100644
index 0000000..e39b477
--- /dev/null
+++ b/examples/defines/includes/include.svh
@@ -0,0 +1 @@
+`define IDX0 2
\ No newline at end of file
diff --git a/examples/defines/readme b/examples/defines/readme
new file mode 100644
index 0000000..281c2cc
--- /dev/null
+++ b/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`.
\ No newline at end of file
diff --git a/examples/defines/script.ys b/examples/defines/script.ys
new file mode 100644
index 0000000..cd67681
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/examples/defines/top.sv b/examples/defines/top.sv
new file mode 100644
index 0000000..d9c8283
--- /dev/null
+++ b/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
\ No newline at end of file