Skip to content

arithmetic/sub: declare the missing cout port - #70

Open
kroening wants to merge 1 commit into
zeroasiccorp:mainfrom
kroening:fix-sub-undeclared-cout
Open

kroening wants to merge 1 commit into
zeroasiccorp:mainfrom
kroening:fix-sub-undeclared-cout

Conversation

@kroening

Copy link
Copy Markdown

Summary

arithmetic/sub/rtl/sub.v computes

assign {cout, out[DW-1:0]} = a[DW-1:0] - b[DW-1:0];

but cout is never declared: it isn't a port, and there's no
wire/reg declaration for it either. This is invalid Verilog (an
undeclared identifier used on an lvalue), caught by any tool that
checks for undeclared identifiers -- e.g. ebmc reports
unknown identifier cout while type-checking, and rejects the module.

Fix

Add cout as an output port, mirroring the sibling add module's
cin/cout convention: a - b is computed as a (DW+1)-bit
operation, with the extra bit carrying the borrow/carry-out.

How found

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

The module assigns {cout, out[DW-1:0]} = a - b, but cout was never
declared anywhere -- not as a port, and not as a wire/reg. Any
Verilog tool that checks for undeclared identifiers rejects this
(e.g. EBMC: "unknown identifier cout"). Add cout as an output port,
mirroring the sibling add module's cin/cout convention (a[DW-1:0] -
b[DW-1:0] is computed as a (DW+1)-bit operation, with the extra bit
carrying the borrow/carry-out).

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