Skip to content

blocks/reedsolomon: fix s_nz multi-driver in rs_syndrome - #71

Open
kroening wants to merge 1 commit into
zeroasiccorp:mainfrom
kroening:fix-reedsolomon-s_nz-multi-driver
Open

kroening wants to merge 1 commit into
zeroasiccorp:mainfrom
kroening:fix-reedsolomon-s_nz-multi-driver

Conversation

@kroening

Copy link
Copy Markdown

Summary

rs_syndrome.s_nz is assigned in two separate always @(posedge clk)
blocks: the main accumulator block resets it to 0 alongside
s_valid/acc, and a second, dedicated block both resets it to 0 and
drives its real value (the OR-reduce of the final syndromes) on
in_valid && in_last. A variable driven by more than one procedural
block is invalid Verilog, caught by any tool that checks for this --
e.g. ebmc reports `s_nz' has multiple drivers and rejects the
module.

Fix

Remove the redundant reset assignment to s_nz from the first block;
the second block already resets it on rst and is its sole driver.
No behavioral change (both blocks reset it to the same value 0; only
the second block ever drives it to anything else).

Note

reedsolomon still won't fully elaborate with ebmc after this fix --
rs_dec.v shares an integer loop counter (k) across two clocked
always blocks, which is a separate, real bug in ebmc itself (not
this RTL), already reported at
diffblue/hw-cbmc#2184.

How found

Found via ebmc's parse/elaborate pass over the benchmark suite,
reported at https://diffblue.github.io/hw-cbmc/logikbench/.

s_nz was assigned in two separate always @(posedge clk) blocks: the
main accumulator block reset it to 0 alongside s_valid/acc, and a
second, dedicated block both reset it to 0 and drove its real value
(the OR-reduce of the final syndromes) on in_valid && in_last. A
variable driven by more than one procedural block is invalid Verilog,
caught by any tool that checks for this (e.g. EBMC:
"s_nz has multiple drivers").

Remove the redundant reset assignment from the first block; the
second block already resets s_nz on rst and is its sole driver.

Found via ebmc's parse/elaborate pass over the benchmark suite
(https://diffblue.github.io/hw-cbmc/logikbench/).

This branch has not been deployed

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant