From c5e5f5dcbb99c0038f8f9f18a967705f10f62c61 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 29 Jun 2018 19:32:03 +0200 Subject: [PATCH] Update examples Signed-off-by: Clifford Wolf --- docs/examples/demos/fib.sby | 4 +-- docs/examples/demos/{fib.v => fib.sv} | 4 +-- docs/examples/multiclk/dpmem.sby | 4 +-- docs/examples/multiclk/dpmem.sv | 15 +++++++---- docs/examples/puzzles/primegen.sby | 4 +-- docs/examples/puzzles/primegen.sv | 27 +++++++++++++++++++ docs/examples/puzzles/primegen.v | 27 ------------------- docs/examples/puzzles/wolf_goat_cabbage.sby | 4 +-- ...lf_goat_cabbage.v => wolf_goat_cabbage.sv} | 8 +++--- 9 files changed, 51 insertions(+), 46 deletions(-) rename docs/examples/demos/{fib.v => fib.sv} (91%) create mode 100644 docs/examples/puzzles/primegen.sv delete mode 100644 docs/examples/puzzles/primegen.v rename docs/examples/puzzles/{wolf_goat_cabbage.v => wolf_goat_cabbage.sv} (90%) diff --git a/docs/examples/demos/fib.sby b/docs/examples/demos/fib.sby index 4622009..293a7fe 100644 --- a/docs/examples/demos/fib.sby +++ b/docs/examples/demos/fib.sby @@ -21,8 +21,8 @@ aiger suprove -- [script] -read_verilog -formal fib.v +read -formal fib.sv prep -top fib [files] -fib.v +fib.sv diff --git a/docs/examples/demos/fib.v b/docs/examples/demos/fib.sv similarity index 91% rename from docs/examples/demos/fib.v rename to docs/examples/demos/fib.sv index 016e75f..f199447 100644 --- a/docs/examples/demos/fib.v +++ b/docs/examples/demos/fib.sv @@ -54,10 +54,10 @@ module fib ( cover ($past(n) == 15); end - assume (s_eventually !pause); + assume property (s_eventually !pause); if (start && !pause) - assert (s_eventually done); + assert property (s_eventually done); end `endif endmodule diff --git a/docs/examples/multiclk/dpmem.sby b/docs/examples/multiclk/dpmem.sby index bd63e04..66ad19a 100644 --- a/docs/examples/multiclk/dpmem.sby +++ b/docs/examples/multiclk/dpmem.sby @@ -7,8 +7,8 @@ multiclock on smtbmc [script] -read_verilog -sv -formal dpmem.sv -prep -nordff -top top +read -formal dpmem.sv +prep -top top chformal -early -assume [files] diff --git a/docs/examples/multiclk/dpmem.sv b/docs/examples/multiclk/dpmem.sv index 46d9872..87e4f61 100644 --- a/docs/examples/multiclk/dpmem.sv +++ b/docs/examples/multiclk/dpmem.sv @@ -41,14 +41,17 @@ module top ( reg shadow_valid = 0; reg [3:0] shadow_data; - const rand reg [3:0] shadow_addr; + (* anyconst *) reg [3:0] shadow_addr; - always @($global_clock) begin - assume($stable(rc) || $stable(wc)); + reg init = 1; + (* gclk *) reg gclk; - if (!$initstate) begin + always @(posedge gclk) begin + assume ($stable(rc) || $stable(wc)); + + if (!init) begin if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin - assert(shadow_data == rd); + assert (shadow_data == rd); end if ($rose(wc) && $past(we) && shadow_addr == $past(wa)) begin @@ -56,5 +59,7 @@ module top ( shadow_valid <= 1; end end + + init <= 0; end endmodule diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby index 53b005e..9e6da21 100644 --- a/docs/examples/puzzles/primegen.sby +++ b/docs/examples/puzzles/primegen.sby @@ -12,10 +12,10 @@ primes_fail: expect fail smtbmc --dumpsmt2 --progress --stbv z3 [script] -read_verilog -formal primegen.v +read -formal primegen.sv primes_fail: chparam -set offset 7 primes primegen: prep -top primegen ~primegen: prep -top primes [files] -primegen.v +primegen.sv diff --git a/docs/examples/puzzles/primegen.sv b/docs/examples/puzzles/primegen.sv new file mode 100644 index 0000000..7bd4788 --- /dev/null +++ b/docs/examples/puzzles/primegen.sv @@ -0,0 +1,27 @@ +module primegen; + (* anyconst *) reg [31:0] prime; + (* allconst *) reg [15:0] factor; + + always @* begin + if (1 < factor && factor < prime) + assume ((prime % factor) != 0); + assume (prime > 1000000000); + cover (1); + end +endmodule + +module primes; + parameter [8:0] offset = 500; + (* anyconst *) reg [8:0] prime1; + wire [9:0] prime2 = prime1 + offset; + (* allconst *) reg [4:0] factor; + + always @* begin + if (1 < factor && factor < prime1) + assume ((prime1 % factor) != 0); + if (1 < factor && factor < prime2) + assume ((prime2 % factor) != 0); + assume (1 < prime1); + cover (1); + end +endmodule diff --git a/docs/examples/puzzles/primegen.v b/docs/examples/puzzles/primegen.v deleted file mode 100644 index 95d6ddc..0000000 --- a/docs/examples/puzzles/primegen.v +++ /dev/null @@ -1,27 +0,0 @@ -module primegen; - wire [31:0] prime = $anyconst; - wire [15:0] factor = $allconst; - - always @* begin - if (1 < factor && factor < prime) - assume((prime % factor) != 0); - assume(prime > 1000000000); - cover(1); - end -endmodule - -module primes; - parameter [8:0] offset = 500; - wire [8:0] prime1 = $anyconst; - wire [9:0] prime2 = prime1 + offset; - wire [4:0] factor = $allconst; - - always @* begin - if (1 < factor && factor < prime1) - assume((prime1 % factor) != 0); - if (1 < factor && factor < prime2) - assume((prime2 % factor) != 0); - assume(1 < prime1); - cover(1); - end -endmodule diff --git a/docs/examples/puzzles/wolf_goat_cabbage.sby b/docs/examples/puzzles/wolf_goat_cabbage.sby index a980a3f..a788488 100644 --- a/docs/examples/puzzles/wolf_goat_cabbage.sby +++ b/docs/examples/puzzles/wolf_goat_cabbage.sby @@ -6,8 +6,8 @@ depth 100 smtbmc [script] -read_verilog -formal wolf_goat_cabbage.v +read -formal wolf_goat_cabbage.sv prep -top wolf_goat_cabbage [files] -wolf_goat_cabbage.v +wolf_goat_cabbage.sv diff --git a/docs/examples/puzzles/wolf_goat_cabbage.v b/docs/examples/puzzles/wolf_goat_cabbage.sv similarity index 90% rename from docs/examples/puzzles/wolf_goat_cabbage.v rename to docs/examples/puzzles/wolf_goat_cabbage.sv index b5e46eb..9c9fe7a 100644 --- a/docs/examples/puzzles/wolf_goat_cabbage.v +++ b/docs/examples/puzzles/wolf_goat_cabbage.sv @@ -14,19 +14,19 @@ module wolf_goat_cabbage (input clk, input w, g, c); always @(posedge clk) begin // maximum one of the control signals must be high - assume(w+g+c <= 1); + assume (w+g+c <= 1); // we want wolf, goat, and cabbage on the 2nd river bank - cover(bank_w && bank_g && bank_c); + cover (bank_w && bank_g && bank_c); // don't leave wolf and goat unattended if (bank_w != bank_m) begin - assume(bank_w != bank_g); + assume (bank_w != bank_g); end // don't leave goat and cabbage unattended if (bank_g != bank_m) begin - assume(bank_g != bank_c); + assume (bank_g != bank_c); end // man travels and takes the selected item with him -- 2.30.2