mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-28 19:35:53 +00:00
Code Activity

smt2: emit smtlib2_comb_expr outputs after all inputs

Browse source
This commit is contained in:
Jannis Harder 2022-06-07 17:37:04 +02:00
parent 5f9a97d234
commit ac22f1764d
3 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

10
tests/various/smtlib2_module-expected.smt2
View file

@ -5,6 +5,9 @@
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output add 8
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
@ -12,9 +15,6 @@
)
(bvadd a b)
))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output eq 1
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state))
@ -64,10 +64,10 @@
(|uut_a 2| state)
(|smtlib2_a| (|uut_h s| state))
))
(define-fun |uut_u| ((state |uut_s|)) Bool
(define-fun |uut_u| ((state |uut_s|)) Bool
(|smtlib2_u| (|uut_h s| state))
)
(define-fun |uut_i| ((state |uut_s|)) Bool
(define-fun |uut_i| ((state |uut_s|)) Bool
(|smtlib2_i| (|uut_h s| state))
)
(define-fun |uut_h| ((state |uut_s|)) Bool (and