Skip to content

Instantly share code, notes, and snippets.

@thotypous

thotypous/top.sby

Last active February 18, 2025 11:57
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save thotypous/30b6a5092a659856061cf1070fa328eb to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save thotypous/30b6a5092a659856061cf1070fa328eb to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. thotypous revised this gist Feb 18, 2025. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion top.sby
    View file
    Original file line number Diff line number Diff line change
    @@ -3,7 +3,7 @@ mode cover
    depth 20

    [engines]
    smtbmc z3
    smtbmc yices

    [script]
    read -formal top.v
  2. thotypous revised this gist Feb 17, 2025. No changes.
  3. thotypous created this gist Feb 17, 2025.
    13 changes: 13 additions & 0 deletions top.sby
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,13 @@
    [options]
    mode cover
    depth 20

    [engines]
    smtbmc z3

    [script]
    read -formal top.v
    prep -top top

    [files]
    top.v
    17 changes: 17 additions & 0 deletions top.v
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,17 @@
    module top(input clk);

    reg [31:0] i;
    reg [31:0] j;

    initial begin
    i = 0;
    // if we do not set an initial value for j, the tool will find a value such that the cover statement below is SAT
    end

    always @(posedge clk) begin
    i <= i + 1;
    j <= j + j;
    cover (i == 3 && j == 32);
    end

    endmodule