mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 06:44:06 +00:00
Code Activity

Remove redundancies in certain logic checks

Browse source 
A | A' === True, A | (A' & B) === A | B
This commit is contained in:
KrystalDelusion 2022-08-01 20:36:19 +12:00
parent 672a559b92
commit ed9b291d2b
2 changed files with 9 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
docs/examples/fifo/fifo.sv
View file

@ -96,7 +96,7 @@ module fifo
init <= 1; init <= 1;
// if init is low we don't care about the value of rst_n // if init is low we don't care about the value of rst_n
// if init is high (rst_n has ben high), then rst_n must remain high // if init is high (rst_n has ben high), then rst_n must remain high
assume (!init || init && rst_n); assume (!init || rst_n);
end end
// tests // tests
@ -128,9 +128,9 @@ module fifo
|| waddr == $past(waddr + 1)); || waddr == $past(waddr + 1));
// full and empty work as expected // full and empty work as expected
a_full: assert (!full || full && count == MAX_DATA); a_full: assert (!full || count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1); w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || empty && count == 0); a_empty: assert (!empty || count == 0);
w_empty: cover (ren && !wen && count == 1); w_empty: cover (ren && !wen && count == 1);
// can we corrupt our data? // can we corrupt our data?
@ -165,8 +165,9 @@ module fifo
// change data when writing (and only when writing) so we can line // change data when writing (and only when writing) so we can line
// up reads with writes // up reads with writes
assume property (wen |=> $changed(wdata)); //TODO: this but with a cover statement
assume property (!wen |=> $stable(wdata)); // assume property (wen |=> $changed(wdata));
// assume property (!wen |=> $stable(wdata));
end end
end end
`else // !VERIFIC `else // !VERIFIC

17
docs/examples/fifo/golden/fifo.sv
View file

@ -98,7 +98,7 @@ module fifo
init <= 1; init <= 1;
// if init is low we don't care about the value of rst_n // if init is low we don't care about the value of rst_n
// if init is high (rst_n has ben high), then rst_n must remain high // if init is high (rst_n has ben high), then rst_n must remain high
assume (!init || init && rst_n); assume (!init || rst_n);
end end
// tests // tests
@ -130,9 +130,9 @@ module fifo
|| waddr == $past(waddr + 1)); || waddr == $past(waddr + 1));
// full and empty work as expected // full and empty work as expected
a_full: assert (!full || full && count == MAX_DATA); a_full: assert (!full || count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1); w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || empty && count == 0); a_empty: assert (!empty || count == 0);
w_empty: cover (ren && !wen && count == 1); w_empty: cover (ren && !wen && count == 1);
// can we corrupt our data? // can we corrupt our data?
@ -163,19 +163,8 @@ module fifo
// can we corrupt our data? // can we corrupt our data?
ap_overfill: assert property (wen && full |=> $changed(raddr)); ap_overfill: assert property (wen && full |=> $changed(raddr));
ap_underfill: assert property (ren && empty |=> $changed(waddr)); ap_underfill: assert property (ren && empty |=> $changed(waddr));
// change data when writing (and only when writing) so we can line
// up reads with writes
assume property (wen |=> $changed(wdata));
assume property (!wen |=> $stable(wdata));
end end
end end
`else // !VERIFIC
// without verific we are more limited in describing the above assumption
always @(posedge clk) begin
assume ((wen && wdata != $past(wdata))
|| (!wen && wdata == $past(wdata)));
end
`endif // VERIFIC `endif // VERIFIC
`endif // FORMAL `endif // FORMAL