3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00

Update examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-06-29 19:32:03 +02:00
parent 2fa29974dd
commit c5e5f5dcbb
9 changed files with 51 additions and 46 deletions

View file

@ -21,8 +21,8 @@ aiger suprove
--
[script]
read_verilog -formal fib.v
read -formal fib.sv
prep -top fib
[files]
fib.v
fib.sv

View file

@ -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

View file

@ -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]

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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