--
[script]
-read_verilog -formal fib.v
+read -formal fib.sv
prep -top fib
[files]
-fib.v
+fib.sv
--- /dev/null
+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
+++ /dev/null
-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
smtbmc
[script]
-read_verilog -sv -formal dpmem.sv
-prep -nordff -top top
+read -formal dpmem.sv
+prep -top top
chformal -early -assume
[files]
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
shadow_valid <= 1;
end
end
+
+ init <= 0;
end
endmodule
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
--- /dev/null
+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
+++ /dev/null
-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
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
--- /dev/null
+// 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
+++ /dev/null
-// 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
projects / SymbiYosys.git / commitdiff