Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

write_smt2: redundant uninterpreted function #3769

Open
YikeZhou opened this issue May 18, 2023 · 1 comment · May be fixed by #3953
Open

write_smt2: redundant uninterpreted function #3769

YikeZhou opened this issue May 18, 2023 · 1 comment · May be fixed by #3953
Labels
pending-verification This issue is pending verification and/or reproduction

Comments

@YikeZhou
Copy link

Version

Yosys 0.29+21 (git sha1 147cceb, clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

Verilog file top.v:

module top(
  input clk,
  input [2:0] i,
  output reg [2:0] o
);
  always @(posedge clk) begin
    o <= ((3'h6) & (^i)) ? 3'h0 : i;
  end
endmodule

SMT-LIBv2 template test.tpl:

(set-logic QF_UFBV)

%%

(declare-fun s1
    () top_s)
(declare-fun s2
    () top_s)
(assert
    (top_t s1 s2))

(assert
    (distinct
        (|top_n i| s1)
        (|top_n o| s2)))

(check-sat)
(get-model)

Yosys script write_smt2.ys:

read_verilog top.v
hierarchy -check; proc; opt; dffunmap
write_smt2 -tpl test.tpl top.smt2

Commands:

$ yosys write_smt2.ys
$ z3 top.smt2

Expected Behavior

  • (3'h6) & (^i) is expected to be 0.
  • Therefore, the procedural assignment can be considered as o <= i.
  • (check-sat) is expected to yield UNSAT.

Actual Behavior

The output of z3 shows that it did find a model for us.

sat
(
  (define-fun s2 () top_s
    top_s!val!0)
  (define-fun s1 () top_s
    top_s!val!0)
  (define-fun |top#0| ((x!0 top_s)) Bool
    false)
  (define-fun |top#1| ((x!0 top_s)) (_ BitVec 3)
    #b011)
  (define-fun |top#4| ((x!0 top_s)) Bool
    true)
  (define-fun |top#2| ((x!0 top_s)) (_ BitVec 3)
    #b000)
  (define-fun top_is ((x!0 top_s)) Bool
    false)
)
@YikeZhou YikeZhou added the pending-verification This issue is pending verification and/or reproduction label May 18, 2023
@YikeZhou
Copy link
Author

This is the output of yosys:

; SMT-LIBv2 description generated by Yosys 0.29+21 (git sha1 147cceb51, 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|) Bool) ; \clk
; yosys-smt2-input clk 1
; yosys-smt2-clock clk posedge
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "posedge", "width": 1}
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |top_n clk| ((state |top_s|)) Bool (|top#0| state))
(declare-fun |top#1| (|top_s|) (_ BitVec 3)) ; \i
; yosys-smt2-input i 3
; yosys-smt2-witness {"offset": 0, "path": ["\\i"], "smtname": "i", "smtoffset": 0, "type": "input", "width": 3}
(define-fun |top_n i| ((state |top_s|)) (_ BitVec 3) (|top#1| state))
; yosys-smt2-witness {"offset": 0, "path": ["\\o"], "smtname": 2, "smtoffset": 0, "type": "reg", "width": 3}
(declare-fun |top#2| (|top_s|) (_ BitVec 3)) ; \o
; yosys-smt2-output o 3
; yosys-smt2-register o 3
(define-fun |top_n o| ((state |top_s|)) (_ BitVec 3) (|top#2| state))
(define-fun |top#3| ((state |top_s|)) Bool (xor  (= ((_ extract 0 0) (|top#1| state)) #b1) (= ((_ extract 1 1) (|top#1| state)) #b1) (= ((_ extract 2 2) (|top#1| state)) #b1))) ; { $and$top.v:7$3_Y [2:1] $reduce_xor$top.v:7$2_Y [0] }
(declare-fun |top#4| (|top_s|) Bool) ; 1'0
(define-fun |top#5| ((state |top_s|)) Bool (or  false (|top#4| state) false)) ; $reduce_bool$top.v:7$4_Y
(define-fun |top#6| ((state |top_s|)) (_ BitVec 3) (ite (|top#5| state) #b000 (|top#1| state))) ; $auto$rtlil.cc:2496:Mux$9
(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 
  (= (|top#6| state) (|top#2| next_state)) ; $auto$ff.cc:266:slice$7 \o
) ; end of module top
; yosys-smt2-topmod top
; end of yosys output

The uninterpreted function

(declare-fun |top#4| (|top_s|) Bool) ; 1'0

looks a little strange. I'm not sure if I understand this very well. But shouldn't it be a constant zero?

@YikeZhou YikeZhou changed the title write_smt2: uninterpreted function write_smt2: redundant uninterpreted function May 18, 2023
georgerennie added a commit to georgerennie/yosys that referenced this issue Sep 24, 2023
@georgerennie
smt2: Check for constant bool after fully resolving signal
f6f85f4 
* This fixes YosysHQ#3769
@georgerennie georgerennie linked a pull request Sep 24, 2023 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending-verification This issue is pending verification and/or reproduction
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

smt2: Check for constant bool after fully resolving signal georgerennie/yosys
1 participant
@YikeZhou