mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-06 14:24:08 +00:00
Update remaining quickstart examples
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
parent
45a11da8ea
commit
2fa29974dd
|
@ -5,8 +5,8 @@ mode cover
|
|||
smtbmc
|
||||
|
||||
[script]
|
||||
read_verilog -formal cover.v
|
||||
read -formal cover.sv
|
||||
prep -top top
|
||||
|
||||
[files]
|
||||
cover.v
|
||||
cover.sv
|
||||
|
|
|
@ -8,6 +8,10 @@ module top (
|
|||
state <= ((state << 5) + state) ^ din;
|
||||
end
|
||||
|
||||
cover property (state == 'd 12345678);
|
||||
cover property (state == 'h 12345678);
|
||||
`ifdef FORMAL
|
||||
always @(posedge clk) begin
|
||||
cover (state == 'd 12345678);
|
||||
cover (state == 'h 12345678);
|
||||
end
|
||||
`endif
|
||||
endmodule
|
|
@ -7,8 +7,8 @@ expect fail
|
|||
smtbmc boolector
|
||||
|
||||
[script]
|
||||
read_verilog -formal memory.v
|
||||
read -formal memory.sv
|
||||
prep -top testbench
|
||||
|
||||
[files]
|
||||
memory.v
|
||||
memory.sv
|
||||
|
|
|
@ -12,7 +12,7 @@ module testbench (
|
|||
.rdata(rdata)
|
||||
);
|
||||
|
||||
wire [9:0] test_addr = $anyconst;
|
||||
(* anyconst *) reg [9:0] test_addr;
|
||||
reg test_data_valid = 0;
|
||||
reg [7:0] test_data;
|
||||
|
|
@ -5,8 +5,8 @@ mode prove
|
|||
smtbmc
|
||||
|
||||
[script]
|
||||
read_verilog -formal prove.v
|
||||
read -formal prove.sv
|
||||
prep -top testbench
|
||||
|
||||
[files]
|
||||
prove.v
|
||||
prove.sv
|
||||
|
|
|
@ -8,11 +8,15 @@ module testbench (
|
|||
.clk (clk ),
|
||||
.reset(reset),
|
||||
.din (din ),
|
||||
.dout (dout ),
|
||||
.dout (dout )
|
||||
);
|
||||
|
||||
initial assume (reset);
|
||||
assert property (reset || !dout[1:0]);
|
||||
reg init = 1;
|
||||
always @(posedge clk) begin
|
||||
if (init) assume (reset);
|
||||
if (!reset) assert (!dout[1:0]);
|
||||
init <= 0;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module demo (
|
|
@ -190,7 +190,7 @@ also be a useful method for evaluating engines.)
|
|||
|
||||
Let's consider the following example:
|
||||
|
||||
.. literalinclude:: ../examples/quickstart/memory.v
|
||||
.. literalinclude:: ../examples/quickstart/memory.sv
|
||||
:language: systemverilog
|
||||
|
||||
This example is expected to fail verification (see the BUG comment).
|
||||
|
@ -224,7 +224,7 @@ Bounded model checks only prove that the safety properties hold for the first
|
|||
and we need to prove that the safety properties hold forever, not just the first
|
||||
*N* cycles. Let us consider the following example:
|
||||
|
||||
.. literalinclude:: ../examples/quickstart/prove.v
|
||||
.. literalinclude:: ../examples/quickstart/prove.sv
|
||||
:language: systemverilog
|
||||
|
||||
Proving this design in an unbounded manner can be achieved using the following
|
||||
|
|
Loading…
Reference in a new issue