mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Adding USE_VERIFIC flag

Browse source 
Adding variations in .sby file where tabby uses verific and oss doesn't.
This commit is contained in:
KrystalDelusion 2022-06-07 11:49:25 +12:00
parent aed5a33bef
commit fef6d3a8a6
2 changed files with 35 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
docs/examples/fifo/fifo.sby
View file

@ -1,6 +1,9 @@
[tasks] [tasks]
cover prove_oss prove oss
prove prove_tabby prove tabby
cover_oss cover oss
cover_tabby cover tabby
prove_oss cover_oss : default
[options] [options]
cover: cover:
@ -16,6 +19,7 @@ prove: abc pdr
[script] [script]
read -sv fifo.sv read -sv fifo.sv
tabby: read -define USE_VERIFIC=1
read -formal top.sv read -formal top.sv
prep -top fifo prep -top fifo

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

@ -108,14 +108,6 @@ module fifo (
|| waddr == $past(waddr) || waddr == $past(waddr)
|| waddr == $past(waddr + 1)); || 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 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 // full and empty work as expected
a_full: assert (!full || full && count == MAX_DATA); a_full: assert (!full || full && count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1); w_full: cover (wen && !ren && count == MAX_DATA-1);
@ -123,9 +115,7 @@ module fifo (
w_empty: cover (ren && !wen && count == 1); w_empty: cover (ren && !wen && count == 1);
// can we corrupt our data? // can we corrupt our data?
// ap_overfill: assert property (wen && full |=> raddr != $past(raddr));
w_overfill: cover ($past(rskip) && raddr); w_overfill: cover ($past(rskip) && raddr);
// ap_underfill: assert property (ren && empty |=> waddr != $past(waddr));
w_underfill: cover ($past(wskip) && waddr); w_underfill: cover ($past(wskip) && waddr);
end else begin end else begin
// waddr and raddr are zero while reset is low // waddr and raddr are zero while reset is low
@ -137,13 +127,36 @@ module fifo (
end end
end end
// assumptions `ifdef USE_VERIFIC
// if we have verific we can also do the following additional tests
always @(posedge clk) begin always @(posedge clk) begin
// data will change when writing (and only when writing) so we can line up reads with writes if (rst_n) begin
assume ((wen && wdata != $past(wdata)) || (!wen && wdata == $past(wdata))); // read/write enables enable
// assume property (wen |=> wdata != $past(wdata)); ap_raddr2: assert property (ren |=> $changed(raddr));
// assume property (!wen |=> wdata == $past(wdata)); ap_waddr2: assert property (wen |=> $changed(waddr));
// read/write needs enable UNLESS full/empty
ap_raddr3: assert property (!ren && !full |=> $stable(raddr));
ap_waddr3: assert property (!wen && !empty |=> $stable(waddr));
// can we corrupt our data?
ap_overfill: assert property (wen && full |=> $changed(raddr));
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
`endif `else // !USE_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 // USE_VERIFIC
`endif // FORMAL
endmodule endmodule