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

Adjusting for use with OSS

Browse source 
i.e. doesn't use concurrent assertions
This commit is contained in:
KrystalDelusion 2022-05-02 12:20:27 +12:00
parent f33c2eda52
commit 48d846d529
1 changed files with 55 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

108
docs/examples/fifo/top.sv
View file

@ -54,7 +54,7 @@ module fifo (
end
assign full = data_count == MAX_DATA-1;
assign empty = data_count == 0;
assign empty = (data_count == 0) && rst_n;
assign count = data_count;
// write while full => overwrite oldest data, move read pointer
@ -65,72 +65,74 @@ module fifo (
`ifdef FORMAL
// observers
wire [4:0] addr_diff;
assign addr_diff = waddr >= raddr ? waddr - raddr : waddr + MAX_DATA - raddr;
// tests should not run through a reset
// not entirely sure what this actually does
default clocking @(posedge clk); endclocking
default disable iff (~rst_n);
assign addr_diff = waddr >= raddr
? waddr - raddr
: waddr + MAX_DATA - raddr;
// tests
always @(posedge clk or negedge rst_n) begin
// waddr and raddr are zero while reset is low
ap_reset: assert property (~rst_n |=> !waddr && !raddr);
wp_reset: cover property (rst_n);
always @(posedge clk) begin
if (rst_n) begin
// waddr and raddr can only be non zero if reset is high
w_nreset: cover (waddr || raddr);
// waddr and raddr can only be non zero if reset is high
ap_nreset: assert property (waddr || raddr |=> $past(rst_n));
wp_nreset: cover property (waddr || raddr);
// count never less than zero, or more than max
a_uflow: assert (count >= 0);
a_uflow2: assert (raddr >= 0);
a_oflow: assert (count < MAX_DATA);
a_oflow2: assert (waddr < MAX_DATA);
// count never less than zero, or more than max
ap_uflow: assert (count >= 0);
ap_uflow2: assert (raddr >= 0);
ap_oflow: assert (count < MAX_DATA);
ap_oflow2: assert (waddr < MAX_DATA);
// count should be equal to the difference between writer and reader address
a_count_diff: assert (count == addr_diff);
// count should be equal to the difference between writer and reader address
ap_count_diff: assert (count == addr_diff);
// count should only be able to increase or decrease by 1
a_counts: assert (count == 0
|| count == $past(count)
|| count == $past(count) + 1
|| count == $past(count) - 1);
// count should only be able to increase or decrease by 1
ap_counts: assert (count == 0
|| count == $past(count)
|| count == $past(count) + 1
|| count == $past(count) - 1);
// read/write addresses can only increase (or stay the same)
a_raddr: assert (raddr == 0
|| raddr == $past(raddr)
|| raddr == $past(raddr + 1));
a_waddr: assert (waddr == 0
|| waddr == $past(waddr)
|| waddr == $past(waddr + 1));
// read/write addresses can only increase (or stay the same)
ap_raddr: assert (raddr == 0
|| raddr == $past(raddr)
|| raddr == $past(raddr + 1));
ap_waddr: assert (waddr == 0
|| waddr == $past(waddr)
|| waddr == $past(waddr + 1));
// read/write enables enable
// ap_raddr2: assert property (ren |=> raddr != $past(raddr));
// ap_waddr2: assert property (wen |=> waddr != $past(waddr));
// read/write enables enable
ap_raddr2: assert property (ren |=> raddr != $past(raddr));
ap_waddr2: assert property (wen |=> waddr != $past(waddr));
// read/write needs enable UNLESS full/empty
// ap_raddr3: assert property (!ren && !full |=> raddr == $past(raddr));
// ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr));
// read/write needs enable UNLESS full/empty
ap_raddr3: assert property (!ren && !full |=> raddr == $past(raddr));
ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr));
// full and empty work as expected
a_full: assert (!full || full && count == MAX_DATA-1);
w_full: cover (wen && !ren && count == MAX_DATA-2);
a_empty: assert (!empty || empty && count == 0);
w_empty: cover property (ren && !wen && count == 1);
// can we corrupt our data?
// ap_overfill: assert property (wen && full |=> raddr != $past(raddr));
w_overfill: cover ($past(rskip) && raddr);
// ap_underfill: assert property (ren && empty |=> waddr != $past(waddr));
w_underfill: cover ($past(wskip) && waddr);
end else begin
// waddr and raddr are zero while reset is low
a_reset: assert (!waddr && !raddr);
w_reset: cover (~rst_n);
// full and empty work as expected
ap_full: assert property (wen && !ren && count == MAX_DATA-2 |=> full);
wp_full: cover property (wen && !ren && count == MAX_DATA-2);
ap_empty: assert property (ren && !wen && count == 1 |=> empty);
wp_empty: cover property (ren && !wen && count == 1);
// can we corrupt our data?
ap_overfill: assert property (wen && full |=> raddr != $past(raddr));
wp_overfill: cover property (wen && full);
ap_underfill: assert property (ren && empty |=> waddr != $past(waddr));
wp_underfill: cover property (ren && empty);
// outputs are zero while reset is low
a_zero_out: assert (!empty && !full && !count);
end
end
// assumptions
always @(posedge clk or negedge rst_n) begin
always @(posedge clk) begin
// 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 ((wen && wdata != $past(wdata)) || (!wen && wdata == $past(wdata)));
// assume property (wen |=> wdata != $past(wdata));
// assume property (!wen |=> wdata == $past(wdata));
end
`endif