From: Clifford Wolf Date: Fri, 29 Jun 2018 17:32:03 +0000 (+0200) Subject: Update examples X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5e5f5dcbb99c0038f8f9f18a967705f10f62c61;p=SymbiYosys.git Update examples Signed-off-by: Clifford Wolf --- 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.sv b/docs/examples/demos/fib.sv new file mode 100644 index 0000000..f199447 --- /dev/null +++ b/docs/examples/demos/fib.sv @@ -0,0 +1,63 @@ +module fib ( + input clk, pause, start, + input [3:0] n, + output reg busy, done, + output reg [9:0] f +); + reg [3:0] count; + reg [9:0] q; + + initial begin + done = 0; + busy = 0; + end + + always @(posedge clk) begin + done <= 0; + if (!pause) begin + if (!busy) begin + if (start) + busy <= 1; + count <= 0; + q <= 1; + f <= 0; + end else begin + q <= f; + f <= f + q; + count <= count + 1; + if (count == n) begin + busy <= 0; + done <= 1; + end + end + end + end + +`ifdef FORMAL + always @(posedge clk) begin + if (busy) begin + assume (!start); + assume ($stable(n)); + end + + if (done) begin + case ($past(n)) + 0: assert (f == 1); + 1: assert (f == 1); + 2: assert (f == 2); + 3: assert (f == 3); + 4: assert (f == 5); + 5: assert (f == 8); + endcase + cover (f == 13); + cover (f == 144); + cover ($past(n) == 15); + end + + assume property (s_eventually !pause); + + if (start && !pause) + assert property (s_eventually done); + end +`endif +endmodule diff --git a/docs/examples/demos/fib.v b/docs/examples/demos/fib.v deleted file mode 100644 index 016e75f..0000000 --- a/docs/examples/demos/fib.v +++ /dev/null @@ -1,63 +0,0 @@ -module fib ( - input clk, pause, start, - input [3:0] n, - output reg busy, done, - output reg [9:0] f -); - reg [3:0] count; - reg [9:0] q; - - initial begin - done = 0; - busy = 0; - end - - always @(posedge clk) begin - done <= 0; - if (!pause) begin - if (!busy) begin - if (start) - busy <= 1; - count <= 0; - q <= 1; - f <= 0; - end else begin - q <= f; - f <= f + q; - count <= count + 1; - if (count == n) begin - busy <= 0; - done <= 1; - end - end - end - end - -`ifdef FORMAL - always @(posedge clk) begin - if (busy) begin - assume (!start); - assume ($stable(n)); - end - - if (done) begin - case ($past(n)) - 0: assert (f == 1); - 1: assert (f == 1); - 2: assert (f == 2); - 3: assert (f == 3); - 4: assert (f == 5); - 5: assert (f == 8); - endcase - cover (f == 13); - cover (f == 144); - cover ($past(n) == 15); - end - - assume (s_eventually !pause); - - if (start && !pause) - assert (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.sv b/docs/examples/puzzles/wolf_goat_cabbage.sv new file mode 100644 index 0000000..9c9fe7a --- /dev/null +++ b/docs/examples/puzzles/wolf_goat_cabbage.sv @@ -0,0 +1,38 @@ +// A man needs to cross a river with a wolf, a goat and a cabbage. His boat is only large +// enough to carry himself and one of his three possessions, so he must transport these +// items one at a time. However, if he leaves the wolf and the goat together unattended, +// then the wolf will eat the goat; similarly, if he leaves the goat and the cabbage together +// unattended, then the goat will eat the cabbage. How can the man get across safely with +// his three items? + +module wolf_goat_cabbage (input clk, input w, g, c); + // everyone starts at the 1st river bank + reg bank_w = 0; // wolf + reg bank_g = 0; // goat + reg bank_c = 0; // cabbage + reg bank_m = 0; // man + + always @(posedge clk) begin + // maximum one of the control signals must be high + assume (w+g+c <= 1); + + // we want wolf, goat, and cabbage on the 2nd river bank + 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); + end + + // don't leave goat and cabbage unattended + if (bank_g != bank_m) begin + assume (bank_g != bank_c); + end + + // man travels and takes the selected item with him + if (w && (bank_w == bank_m)) bank_w <= !bank_m; + if (g && (bank_g == bank_m)) bank_g <= !bank_m; + if (c && (bank_c == bank_m)) bank_c <= !bank_m; + bank_m <= !bank_m; + end +endmodule diff --git a/docs/examples/puzzles/wolf_goat_cabbage.v b/docs/examples/puzzles/wolf_goat_cabbage.v deleted file mode 100644 index b5e46eb..0000000 --- a/docs/examples/puzzles/wolf_goat_cabbage.v +++ /dev/null @@ -1,38 +0,0 @@ -// A man needs to cross a river with a wolf, a goat and a cabbage. His boat is only large -// enough to carry himself and one of his three possessions, so he must transport these -// items one at a time. However, if he leaves the wolf and the goat together unattended, -// then the wolf will eat the goat; similarly, if he leaves the goat and the cabbage together -// unattended, then the goat will eat the cabbage. How can the man get across safely with -// his three items? - -module wolf_goat_cabbage (input clk, input w, g, c); - // everyone starts at the 1st river bank - reg bank_w = 0; // wolf - reg bank_g = 0; // goat - reg bank_c = 0; // cabbage - reg bank_m = 0; // man - - always @(posedge clk) begin - // maximum one of the control signals must be high - assume(w+g+c <= 1); - - // we want wolf, goat, and cabbage on the 2nd river bank - 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); - end - - // don't leave goat and cabbage unattended - if (bank_g != bank_m) begin - assume(bank_g != bank_c); - end - - // man travels and takes the selected item with him - if (w && (bank_w == bank_m)) bank_w <= !bank_m; - if (g && (bank_g == bank_m)) bank_g <= !bank_m; - if (c && (bank_c == bank_m)) bank_c <= !bank_m; - bank_m <= !bank_m; - end -endmodule