Skip to content

Instantly share code, notes, and snippets.

@Zottel

Zottel/buffer_output.sv Secret

Created October 21, 2020 10:08
Show Gist options
  • Save Zottel/72d281b9ddc8cf614f16dc74327c65c1 to your computer and use it in GitHub Desktop.
Save Zottel/72d281b9ddc8cf614f16dc74327c65c1 to your computer and use it in GitHub Desktop.
Download ZIP
Failing assertions, may I read like this?
Raw
buffer_output.sv
module buffer_output #(ADDR_WIDTH=8, DATA_WIDTH=32, DEPTH=5) (
input wire clock,
message_interface.producer dtn,
instruction_output_interface.consumer cu,
data_interface data);
wire data_valid;
wire addr_valid;
assign dtn.valid = data_valid && addr_valid;
wire shared_ack;
assign shared_ack = data_valid && addr_valid && dtn.ack;
fifo_pointers
#(.WIDTH(DATA_WIDTH), .DEPTH(DEPTH))
data_fifo (
.clock(clock),
.in(data.data),
.in_valid(data.valid),
.in_ack(data.ack),
.out(dtn.data),
.out_valid(data_valid),
.out_ack(shared_ack));
fifo_pointers
#(.WIDTH(ADDR_WIDTH), .DEPTH(DEPTH))
addr_fifo (
.clock(clock),
.in(cu.move_to),
.in_valid(cu.move_valid),
.in_ack(cu.move_ack),
.out(dtn.to),
.out_valid(addr_valid),
.out_ack(shared_ack));
`ifdef FORMAL
always @ (posedge clock) begin
only_together_valid:
assert (!dtn.valid || (data_fifo.out_valid && addr_fifo.out_valid));
data_ack_only_when_both_valid:
assert (!data_fifo.out_ack
|| (data_fifo.out_valid && addr_fifo.out_valid));
addr_ack_only_when_both_valid:
assert (!addr_fifo.out_ack
|| (data_fifo.out_valid && addr_fifo.out_valid));
ack_only_together:
assert (data_fifo.out_ack == addr_fifo.out_ack);
end
`endif
endmodule
@Zottel
Copy link
Author

Zottel commented Oct 21, 2020 

root@...:/workdir/output# rm -Rf buffer_output; sby buffer_output.sby 
SBY 10:09:09 [buffer_output] Copy '../interfaces/data_interface.sv' to 'buffer_output/src/data_interface.sv'.
SBY 10:09:09 [buffer_output] Copy '../interfaces/instruction_output_interface.sv' to 'buffer_output/src/instruction_output_interface.sv'.
SBY 10:09:09 [buffer_output] Copy '../interfaces/message_interface.sv' to 'buffer_output/src/message_interface.sv'.
SBY 10:09:09 [buffer_output] Copy 'buffer_output.sv' to 'buffer_output/src/buffer_output.sv'.
SBY 10:09:09 [buffer_output] Copy '../generic/fifo_pointers.sv' to 'buffer_output/src/fifo_pointers.sv'.
SBY 10:09:09 [buffer_output] engine_0: smtbmc z3
SBY 10:09:09 [buffer_output] engine_1: smtbmc yices
SBY 10:09:09 [buffer_output] base: starting process "cd buffer_output/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 10:09:09 [buffer_output] base: buffer_output.sv:10: Warning: Identifier `\dtn.valid' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:13: Warning: Identifier `\dtn.ack' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:20: Warning: Identifier `\data.data' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:21: Warning: Identifier `\data.valid' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:22: Warning: Identifier `\data.ack' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:23: Warning: Identifier `\dtn.data' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:31: Warning: Identifier `\cu.move_to' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:32: Warning: Identifier `\cu.move_valid' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:33: Warning: Identifier `\cu.move_ack' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:34: Warning: Identifier `\dtn.to' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:41: Warning: Identifier `\data_fifo.out_valid' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:41: Warning: Identifier `\addr_fifo.out_valid' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:43: Warning: Identifier `\data_fifo.out_ack' is implicitly declared.
SBY 10:09:09 [buffer_output] base: buffer_output.sv:46: Warning: Identifier `\addr_fifo.out_ack' is implicitly declared.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [7] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [6] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [5] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [4] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [3] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [2] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [1] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\dtn.from [0] is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\addr_fifo.out_valid is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\data_fifo.out_valid is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\addr_fifo.out_ack is used but has no driver.
SBY 10:09:09 [buffer_output] base: Warning: Wire buffer_output.\data_fifo.out_ack is used but has no driver.
SBY 10:09:09 [buffer_output] base: finished (returncode=0)
SBY 10:09:09 [buffer_output] smt2: starting process "cd buffer_output/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 10:09:09 [buffer_output] smt2: finished (returncode=0)
SBY 10:09:09 [buffer_output] engine_0: starting process "cd buffer_output; yosys-smtbmc -s z3 --presat --noprogress -t 2  --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 10:09:09 [buffer_output] engine_1: starting process "cd buffer_output; yosys-smtbmc -s yices --presat --unroll --noprogress -t 2  --append 0 --dump-vcd engine_1/trace.vcd --dump-vlogtb engine_1/trace_tb.v --dump-smtc engine_1/trace.smtc model/design_smt2.smt2"
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Solver: z3
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Solver: yices
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Checking assertions in step 1..
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Checking assumptions in step 0..
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Checking assertions in step 0..
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  BMC failed!
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Assert failed in buffer_output: data_ack_only_when_both_valid
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Assert failed in buffer_output: ack_only_together
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Checking assumptions in step 1..
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Checking assertions in step 1..
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  BMC failed!
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Assert failed in buffer_output: addr_ack_only_when_both_valid
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Assert failed in buffer_output: ack_only_together
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Writing trace to VCD file: engine_1/trace.vcd
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Writing trace to Verilog testbench: engine_1/trace_tb.v
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Writing trace to constraints file: engine_1/trace.smtc
SBY 10:09:09 [buffer_output] engine_1: ##   0:00:00  Status: failed
SBY 10:09:09 [buffer_output] engine_0: ##   0:00:00  Status: failed
SBY 10:09:09 [buffer_output] engine_0: finished (returncode=1)
SBY 10:09:09 [buffer_output] engine_0: Status returned by engine: FAIL
SBY 10:09:09 [buffer_output] engine_1: terminating process
SBY 10:09:09 [buffer_output] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 10:09:09 [buffer_output] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 10:09:09 [buffer_output] summary: engine_0 (smtbmc z3) returned FAIL
SBY 10:09:09 [buffer_output] summary: counterexample trace: buffer_output/engine_0/trace.vcd
SBY 10:09:09 [buffer_output] DONE (FAIL, rc=2)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment