2 files changed, 141 insertions, 6 deletions
diff --git a/examples/config.toml b/examples/config.toml
index 497afe2..7f030d7 100644
--- a/examples/config.toml
+++ b/examples/config.toml
@@ -1,11 +1,43 @@
 
+[info]
+  commit = "d32f4cc45bc8c0670fb788b1fcd4c2f2b15fa094"
+  version = "0.3.0.0"
+
 [probability]
-  moditem.always = 1
-  moditem.assign = 10
-  statement.blocking = 5
+  expr.binary = 5
+  expr.concatenation = 3
+  expr.number = 1
+  expr.rangeselect = 5
+  expr.signed = 5
+  expr.string = 0
+  expr.ternary = 5
+  expr.unary = 5
+  expr.unsigned = 5
+  expr.variable = 5
+  moditem.assign = 5
+  moditem.combinational = 1
+  moditem.instantiation = 1
+  moditem.sequential = 1
+  statement.blocking = 0
   statement.conditional = 1
-  statement.nonblocking = 1
+  statement.forloop = 0
+  statement.nonblocking = 3
 
 [property]
-  depth = 3
-  size = 50
+  module.depth = 2
+  module.max = 5
+  output.combine = false
+  sample.method = "random"
+  sample.size = 10
+  size = 20
+  statement.depth = 3
+
+[[synthesiser]]
+  description = "yosys"
+  name = "yosys"
+  output = "syn_yosys.v"
+
+[[synthesiser]]
+  description = "vivado"
+  name = "vivado"
+  output = "syn_vivado.v"
diff --git a/examples/shift.v b/examples/shift.v
new file mode 100644
index 0000000..ad1c1fd
--- /dev/null
+++ b/examples/shift.v
@@ -0,0 +1,103 @@
+module shift1(input clk, in, output [3:0] q);
+   reg q0 = 0, q1 = 0, q2 = 0, q3 = 0;
+
+   always @(posedge clk) begin
+      q0 = in;
+   end
+   always @(posedge clk) begin
+      q1 = q0;
+   end
+   always @(posedge clk) begin
+      q2 = q1;
+   end
+   always @(posedge clk) begin
+      q3 = q2;
+   end
+
+   assign q = {q0, q1, q2, q3};
+endmodule // shift1
+
+module shift2(input clk, in, output [3:0] q);
+   reg q0 = 0, q1 = 0, q2 = 0, q3 = 0;
+
+   always @(*) begin
+      q2 = q1;
+      q3 = q2;
+      q1 = q0;
+      q0 = in;
+   end
+
+   assign q = {q0, q1, q2, q3};
+endmodule // shift2
+
+module shift3(input clk, in, output [3:0] q);
+   reg q0 = 0, q1 = 0, q2 = 0, q3 = 0;
+
+   always @(posedge clk) begin
+      q3 <= q2;
+      q2 <= q1;
+      q1 <= q0;
+      q0 <= in;
+   end
+
+   assign q = {q0, q1, q2, q3};
+endmodule // shift3
+
+module shift4(input clk, in, output [3:0] q);
+   reg q0 = 0, q1 = 0, q2 = 0, q3 = 0;
+
+   always @(posedge clk) begin
+      q0 <= in;
+   end
+   always @(posedge clk) begin
+      q1 <= q0;
+   end
+   always @(posedge clk) begin
+      q2 <= q1;
+   end
+   always @(posedge clk) begin
+      q3 <= q2;
+   end
+
+   assign q = {q0, q1, q2, q3};
+endmodule // shift4
+
+`ifdef FORMAL
+module top(input clk, in);
+   wire [3:0] q1, q2, q3, q4;
+
+   shift1 shift1(.clk(clk), .in(in), .q(q1));
+   shift2 shift2(.clk(clk), .in(in), .q(q2));
+   shift3 shift3(.clk(clk), .in(in), .q(q3));
+   shift4 shift4(.clk(clk), .in(in), .q(q4));
+
+   always @(posedge clk) begin
+      assert(q1 == q2);
+      assert(q2 == q3);
+      assert(q3 == q4);
+   end
+endmodule // top
+`endif
+
+`ifndef SYNTHESIS
+module main;
+   reg clk = 0, qin = 0;
+   wire [256:0] val = 256'h73a27383942819780a5765c741b2949712384778493895283249178574;
+   reg [5:0]   count = 0;
+   wire [3:0] q1out, q2out, q3out, q4out;
+
+   shift1 shift1(.clk(clk), .in(qin), .q(q1out));
+   shift2 shift2(.clk(clk), .in(qin), .q(q2out));
+   shift3 shift3(.clk(clk), .in(qin), .q(q3out));
+   shift4 shift4(.clk(clk), .in(qin), .q(q4out));
+
+   always #10 clk = ~clk;
+
+   always @(posedge clk) begin
+      count <= count + 1;
+      qin <= val >> count;
+      if(q1out !== q2out || q2out !== q3out || q3out !== q4out)
+        $strobe("q: %b\n q1: %b\n q2: %b\n q3: %b\n q4: %b\n\n", qin, q1out, q2out, q3out, q4out);
+   end
+endmodule // main
+`endif