Skip to content

Add CIRCT datapath synthesis benchmarks 2025 #17

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

Open
cowardsa wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add CIRCT datapath synthesis benchmarks 2025 #17

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
524 changes: 524 additions & 0 deletions non-incremental/QF_BV/20250812-Circt/add_three.12_bit.smt2
View file
Open in desktop

Large diffs are not rendered by default.

163 changes: 163 additions & 0 deletions non-incremental/QF_BV/20250812-Circt/add_three.4_bit.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,163 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
Generated by: Samuel Coward
Generated on: 2025-08-12
Generator: CIRCT
Application: Datapath synthesis of digital circuits
Target solver: Bitwuzla
Time limit: 300.0
Benchmarks generated by the CIRCT tool to check correctness of lowering
from word-level bitvector circuit to a gate-level netlist.
Using compressor tree circuits proves challenging for SMT.|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)

; solver scope 0
(declare-const tmp (_ BitVec 4))
(declare-const tmp_0 (_ BitVec 4))
(declare-const tmp_1 (_ BitVec 4))
(assert (let ((tmp_2 ((_ extract 0 0) tmp_1)))
(let ((tmp_3 ((_ extract 0 0) tmp_0)))
(let ((tmp_4 ((_ extract 0 0) tmp)))
(let ((tmp_5 (bvand tmp_4 tmp_3)))
(let ((tmp_6 (bvxor tmp_5 #b1)))
(let ((tmp_7 (bvxor tmp_3 #b1)))
(let ((tmp_8 (bvxor tmp_4 #b1)))
(let ((tmp_9 (bvand tmp_8 tmp_7)))
(let ((tmp_10 (bvxor tmp_9 #b1)))
(let ((tmp_11 (bvand tmp_10 tmp_6)))
(let ((tmp_12 (bvand tmp_11 tmp_2)))
(let ((tmp_13 (bvxor tmp_12 #b1)))
(let ((tmp_14 (bvxor tmp_2 #b1)))
(let ((tmp_15 (bvxor tmp_11 #b1)))
(let ((tmp_16 (bvand tmp_15 tmp_14)))
(let ((tmp_17 (bvxor tmp_16 #b1)))
(let ((tmp_18 (bvand tmp_17 tmp_13)))
(let ((tmp_19 (bvand tmp_6 tmp_13)))
(let ((tmp_20 (bvxor tmp_19 #b1)))
(let ((tmp_21 ((_ extract 1 1) tmp_1)))
(let ((tmp_22 ((_ extract 1 1) tmp_0)))
(let ((tmp_23 ((_ extract 1 1) tmp)))
(let ((tmp_24 (bvand tmp_23 tmp_22)))
(let ((tmp_25 (bvxor tmp_24 #b1)))
(let ((tmp_26 (bvxor tmp_22 #b1)))
(let ((tmp_27 (bvxor tmp_23 #b1)))
(let ((tmp_28 (bvand tmp_27 tmp_26)))
(let ((tmp_29 (bvxor tmp_28 #b1)))
(let ((tmp_30 (bvand tmp_29 tmp_25)))
(let ((tmp_31 (bvand tmp_30 tmp_21)))
(let ((tmp_32 (bvxor tmp_31 #b1)))
(let ((tmp_33 (bvxor tmp_21 #b1)))
(let ((tmp_34 (bvxor tmp_30 #b1)))
(let ((tmp_35 (bvand tmp_34 tmp_33)))
(let ((tmp_36 (bvxor tmp_35 #b1)))
(let ((tmp_37 (bvand tmp_36 tmp_32)))
(let ((tmp_38 (bvand tmp_37 tmp_20)))
(let ((tmp_39 (bvxor tmp_38 #b1)))
(let ((tmp_40 (bvxor tmp_37 #b1)))
(let ((tmp_41 (bvand tmp_40 tmp_19)))
(let ((tmp_42 (bvxor tmp_41 #b1)))
(let ((tmp_43 (bvand tmp_42 tmp_39)))
(let ((tmp_44 (bvand tmp_25 tmp_32)))
(let ((tmp_45 (bvxor tmp_44 #b1)))
(let ((tmp_46 (bvand tmp_45 tmp_38)))
(let ((tmp_47 (bvxor tmp_46 #b1)))
(let ((tmp_48 (bvand tmp_44 tmp_39)))
(let ((tmp_49 (bvxor tmp_48 #b1)))
(let ((tmp_50 (bvand tmp_49 tmp_47)))
(let ((tmp_51 ((_ extract 2 2) tmp_1)))
(let ((tmp_52 ((_ extract 2 2) tmp_0)))
(let ((tmp_53 ((_ extract 2 2) tmp)))
(let ((tmp_54 (bvand tmp_53 tmp_52)))
(let ((tmp_55 (bvxor tmp_54 #b1)))
(let ((tmp_56 (bvxor tmp_52 #b1)))
(let ((tmp_57 (bvxor tmp_53 #b1)))
(let ((tmp_58 (bvand tmp_57 tmp_56)))
(let ((tmp_59 (bvxor tmp_58 #b1)))
(let ((tmp_60 (bvand tmp_59 tmp_55)))
(let ((tmp_61 (bvand tmp_60 tmp_51)))
(let ((tmp_62 (bvxor tmp_61 #b1)))
(let ((tmp_63 (bvxor tmp_51 #b1)))
(let ((tmp_64 (bvxor tmp_60 #b1)))
(let ((tmp_65 (bvand tmp_64 tmp_63)))
(let ((tmp_66 (bvxor tmp_65 #b1)))
(let ((tmp_67 (bvand tmp_66 tmp_62)))
(let ((tmp_68 (bvand tmp_67 tmp_50)))
(let ((tmp_69 (bvxor tmp_68 #b1)))
(let ((tmp_70 (bvxor tmp_50 #b1)))
(let ((tmp_71 (bvxor tmp_67 #b1)))
(let ((tmp_72 (bvand tmp_71 tmp_70)))
(let ((tmp_73 (bvxor tmp_72 #b1)))
(let ((tmp_74 (bvand tmp_73 tmp_69)))
(let ((tmp_75 (bvand tmp_67 tmp_45)))
(let ((tmp_76 (bvxor tmp_75 #b1)))
(let ((tmp_77 (bvand tmp_71 tmp_44)))
(let ((tmp_78 (bvxor tmp_77 #b1)))
(let ((tmp_79 (bvand tmp_78 tmp_76)))
(let ((tmp_80 (bvand tmp_38 tmp_79)))
(let ((tmp_81 (bvxor tmp_80 #b1)))
(let ((tmp_82 (bvand tmp_81 tmp_76)))
(let ((tmp_83 (bvxor tmp_82 #b1)))
(let ((tmp_84 (bvand tmp_55 tmp_62)))
(let ((tmp_85 (bvxor tmp_84 #b1)))
(let ((tmp_86 (bvand tmp_85 tmp_83)))
(let ((tmp_87 (bvxor tmp_86 #b1)))
(let ((tmp_88 (bvand tmp_84 tmp_82)))
(let ((tmp_89 (bvxor tmp_88 #b1)))
(let ((tmp_90 (bvand tmp_89 tmp_87)))
(let ((tmp_91 ((_ extract 3 3) tmp_1)))
(let ((tmp_92 ((_ extract 3 3) tmp_0)))
(let ((tmp_93 ((_ extract 3 3) tmp)))
(let ((tmp_94 (bvand tmp_93 tmp_92)))
(let ((tmp_95 (bvxor tmp_94 #b1)))
(let ((tmp_96 (bvxor tmp_92 #b1)))
(let ((tmp_97 (bvxor tmp_93 #b1)))
(let ((tmp_98 (bvand tmp_97 tmp_96)))
(let ((tmp_99 (bvxor tmp_98 #b1)))
(let ((tmp_100 (bvand tmp_99 tmp_95)))
(let ((tmp_101 (bvand tmp_100 tmp_91)))
(let ((tmp_102 (bvxor tmp_101 #b1)))
(let ((tmp_103 (bvxor tmp_91 #b1)))
(let ((tmp_104 (bvxor tmp_100 #b1)))
(let ((tmp_105 (bvand tmp_104 tmp_103)))
(let ((tmp_106 (bvxor tmp_105 #b1)))
(let ((tmp_107 (bvand tmp_106 tmp_102)))
(let ((tmp_108 (bvand tmp_107 tmp_90)))
(let ((tmp_109 (bvxor tmp_108 #b1)))
(let ((tmp_110 (bvxor tmp_90 #b1)))
(let ((tmp_111 (bvxor tmp_107 #b1)))
(let ((tmp_112 (bvand tmp_111 tmp_110)))
(let ((tmp_113 (bvxor tmp_112 #b1)))
(let ((tmp_114 (bvand tmp_113 tmp_109)))
(let ((tmp_115 (bvand tmp_107 tmp_85)))
(let ((tmp_116 (bvxor tmp_115 #b1)))
(let ((tmp_117 (bvand tmp_111 tmp_84)))
(let ((tmp_118 (bvxor tmp_117 #b1)))
(let ((tmp_119 (bvand tmp_118 tmp_116)))
(let ((tmp_120 (bvand tmp_83 tmp_119)))
(let ((tmp_121 (bvxor tmp_120 #b1)))
(let ((tmp_122 (bvand tmp_121 tmp_116)))
(let ((tmp_123 (bvxor tmp_122 #b1)))
(let ((tmp_124 (bvand tmp_95 tmp_102)))
(let ((tmp_125 (bvxor tmp_124 #b1)))
(let ((tmp_126 (bvand tmp_125 tmp_123)))
(let ((tmp_127 (bvxor tmp_126 #b1)))
(let ((tmp_128 (bvand tmp_124 tmp_122)))
(let ((tmp_129 (bvxor tmp_128 #b1)))
(let ((tmp_130 (bvand tmp_129 tmp_127)))
(let ((tmp_131 (concat tmp_130 tmp_114)))
(let ((tmp_132 (concat tmp_131 tmp_74)))
(let ((tmp_133 (concat tmp_132 tmp_43)))
(let ((tmp_134 (concat tmp_133 tmp_18)))
(let ((tmp_135 (concat #b0 tmp_1)))
(let ((tmp_136 (concat #b0 tmp_0)))
(let ((tmp_137 (concat #b0 tmp)))
(let ((tmp_138 (bvadd tmp_137 tmp_136)))
(let ((tmp_139 (bvadd tmp_138 tmp_135)))
(let ((tmp_140 (distinct tmp_139 tmp_134)))
tmp_140))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

(exit)
Loading