write_smt2: bugs caused by the '>>' operator under certain circumstances

Version

Yosys 0.28+6 (git sha1 cee3cb31b, clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

Verilog file:

module top (res, offset);
  output [3:0] res; // 4-bit
  input signed [4:0] offset; // 5-bit
  assign res = 4'sb1000 >> offset;
 endmodule

Yosys script:

read_verilog -formal top.v; hierarchy -check -top top
proc; opt; memory -nordff -nomap; opt -fast
dffunmap; write_smt2 -wires"

Expected Behavior

As far as I know, 4'sb1000 shouldn't be sign-extended to 5'sb11000 in this situation. For example, when offset=2, res is expected to be 2(4'b0010).

First, according to this example from SystemVerilog standard (IEEE Std 1800-2017), the width of 4'sb1000 >> offset is expected to be 4.

Second, I tried this test case on ModelSim and Verilator. Both of them returned the value 2.

Actual Behavior

Output of Yosys:

; SMT-LIBv2 description generated by Yosys 0.28+6 (git sha1 cee3cb31b, clang 10.0.0-4ubuntu1 -fPIC -Os)
; yosys-smt2-module top
(declare-sort |top_s| 0)
(declare-fun |top_is| (|top_s|) Bool)
(declare-fun |top#0| (|top_s|) (_ BitVec 5)) ; \offset
; yosys-smt2-input offset 5
; yosys-smt2-wire offset 5
; yosys-smt2-witness {"offset": 0, "path": ["\\offset"], "smtname": "offset", "smtoffset": 0, "type": "input", "width": 5}
(define-fun |top_n offset| ((state |top_s|)) (_ BitVec 5) (|top#0| state))
(define-fun |top#1| ((state |top_s|)) (_ BitVec 4) ((_ extract 3 0) (bvlshr #b11000 (|top#0| state)))) ; \res
; yosys-smt2-output res 4
; yosys-smt2-wire res 4
(define-fun |top_n res| ((state |top_s|)) (_ BitVec 4) (|top#1| state))
(define-fun |top_a| ((state |top_s|)) Bool true)
(define-fun |top_u| ((state |top_s|)) Bool true)
(define-fun |top_i| ((state |top_s|)) Bool true)
(define-fun |top_h| ((state |top_s|)) Bool true)
(define-fun |top_t| ((state |top_s|) (next_state |top_s|)) Bool true) ; end of module top
; yosys-smt2-topmod top
; end of yosys output

Note the expression (_ extract 3 0) (bvlshr #b11000 (|top#0| state)) in line 10. This indicates that when offset=2, the output signal res is 6(4'b0110).

So I thought this might be a bug.

YosysHQ / yosys