Ambiguous reset condition - nonce_offset_i

[norman-stewart]

"./pcrvault/rtl/pv_gen_hash.sv"

Register nonce_offset_i is in "else" condition but not in reset condition of synchronous always block.
This asymmetry can lead to complications with LINT, netlist synthesis, and formal verification closure.

Current:
always_ff @(posedge clk or negedge rst_b) begin : api_regs
if (~rst_b) begin
gen_hash_fsm_ps <= GEN_HASH_IDLE;
block_offset_i <= '0;
read_entry <= '0;
read_offset <= '0;
end
else begin
gen_hash_fsm_ps <= gen_hash_fsm_ns;
block_offset_i <= block_offset_nxt;
nonce_offset_i <= nonce_offset_nxt;
read_entry <= read_entry_nxt;
read_offset <= read_offset_nxt;
end
end

Recommend:
always_ff @(posedge clk or negedge rst_b) begin : api_regs
if (~rst_b) begin
gen_hash_fsm_ps <= GEN_HASH_IDLE;
block_offset_i <= '0;
read_entry <= '0;
read_offset <= '0;
end
else begin
gen_hash_fsm_ps <= gen_hash_fsm_ns;
block_offset_i <= block_offset_nxt;
//nonce_offset_i <= nonce_offset_nxt;
read_entry <= read_entry_nxt;
read_offset <= read_offset_nxt;
end
end
always_ff @(posedge clk) begin : api_regs_noreset
nonce_offset_i <= nonce_offset_nxt;
end

or Recommend:
always_ff @(posedge clk or negedge rst_b) begin : api_regs
if (~rst_b) begin
gen_hash_fsm_ps <= GEN_HASH_IDLE;
block_offset_i <= '0;
nonce_offset_i <= '0;
read_entry <= '0;
read_offset <= '0;
end
else begin
gen_hash_fsm_ps <= gen_hash_fsm_ns;
block_offset_i <= block_offset_nxt;
nonce_offset_i <= nonce_offset_nxt;
read_entry <= read_entry_nxt;
read_offset <= read_offset_nxt;
end
end

[norman-stewart]

Duplicates: #339

[Nitsirks]

Can we include this in the lint PR?

[norman-stewart]

Formality will not match #2.
Formality is unhappy so far with #1, but I don't yet see why. There's some modelling funny business on the implied yet missing reset condition. I think it results in a "dont_care" X in the "if" from a formal perspective.

We can include fix #2 in the PR, though it will break our RTL=RTL formal verification that is otherwise passing for all other proposed fixes.

[Nitsirks]

We can sequence it as separate PRs, but I think this fix is a quality of life fix for integrators that should be pulled into 1.1. I'll let other weigh in on it if they have any objections.

I think fix 2 is my preference. Properly reset the signal.

[norman-stewart]

Sure... let me send out summary and let's do PR with formality passing. There's some low hanging fruit in the remainder that we can swarm on quickly as an incremental.

[bharatpillilli]

@Nitsirks and @nstewart-amd - Could we please close this and other lint issues once the 1.1 Lint PR is completed?

[calebofearth]

(Same as #339) - This is addressed by commit 020cdc6 from #483