mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-15 09:48:43 +00:00
Adjusting assumptions
This commit is contained in:
parent
ec02e25f5c
commit
e106d5c161
|
@ -128,9 +128,9 @@ module fifo (
|
||||||
|
|
||||||
// assumptions
|
// assumptions
|
||||||
always @(posedge clk or negedge rst_n) begin
|
always @(posedge clk or negedge rst_n) begin
|
||||||
// when writing the write data will change (so that we can line up reads with writes)
|
// data will change when writing (and only when writing) so we can line up reads with writes
|
||||||
assume property (wen |=> wdata != $past(wdata));
|
assume property (wen |=> wdata != $past(wdata));
|
||||||
assume (wdata);
|
assume property (!wen |=> wdata == $past(wdata));
|
||||||
end
|
end
|
||||||
`endif
|
`endif
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue