Ready-to-run snippets

Code Examples

Ready-to-run Verilog, SystemVerilog, and UVM examples. Click any to open it live in the IDE.

← All examples

FV Assume-Guarantee: source and sink

SystemVerilog Formal Verification

The source proves its guarantees; the sink assumes them and proves the sum. Set the top module to src, then to sink.

Open in IDE
Related tutorial:
src.sv
// Check 1: set Top Module to src.
module src (input clk, input rst, input ready, output reg valid, output reg [7:0] data);
  // sends 1, 2, 3, ... on a valid/ready interface
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0; data <= 8'd1;
    end else begin
      valid <= 1'b1;
      if (valid && ready) data <= data + 8'd1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // GUARANTEES of the source, proven here
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (valid && data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && $past(valid && ready)) assert (data == $past(data) + 8'd1);
  always @(posedge clk) if (!init && !$past(rst) && !$past(valid && ready)) assert (data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && valid && !$past(valid)) assert (data == 8'd1);
`endif
endmodule
sink.sv
// Check 2: set Top Module to sink.
module sink (input clk, input rst, input stall, input valid, input [7:0] data,
             output ready, output reg [7:0] n, output reg [15:0] sum);
  // adds up every word it receives
  assign ready = !stall;
  always @(posedge clk)
    if (rst) begin
      n <= 8'd0; sum <= 16'd0;
    end else if (valid && ready) begin
      n <= n + 8'd1; sum <= sum + data;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // ASSUMPTIONS: what the source guarantees
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assume (valid && data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && $past(valid && ready)) assume (data == $past(data) + 8'd1);
  always @(posedge clk) if (!init && !$past(rst) && !$past(valid && ready)) assume (data == $past(data));
  always @(*) if (!init && n == 8'd0 && valid) assume (data == 8'd1);
  // the sink's own property
  always @(posedge clk) if (!init) assert (sum == ({8'd0, n} * ({8'd0, n} + 16'd1)) / 16'd2);
`endif
endmodule
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.