mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-12 16:28:17 +00:00
Update README.md
This commit is contained in:
parent
7f2c4189dc
commit
f7f5135508
|
@ -17,9 +17,12 @@ the following technique for proving and using inductive invariants.
|
||||||
Consider the following circuit (stripped-down [example.sv](example.sv)):
|
Consider the following circuit (stripped-down [example.sv](example.sv)):
|
||||||
|
|
||||||
```SystemVerilog
|
```SystemVerilog
|
||||||
module example(input logic clk, output reg [4:0] state);
|
module example(clk, state);
|
||||||
initial state = 27;
|
input logic clk;
|
||||||
|
output logic [4:0] state = 27;
|
||||||
|
|
||||||
always_ff @(posedge clk) state <= (5'd 2 * state - 5'd 1) ^ (state & 5'd 7);
|
always_ff @(posedge clk) state <= (5'd 2 * state - 5'd 1) ^ (state & 5'd 7);
|
||||||
|
|
||||||
always_comb assert (state != 0);
|
always_comb assert (state != 0);
|
||||||
endmodule
|
endmodule
|
||||||
```
|
```
|
||||||
|
|
Loading…
Reference in a new issue