Skip to content

Instantly share code, notes, and snippets.

@mattyoung101

mattyoung101/README.md

Last active November 28, 2024 13:21
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mattyoung101/801a8d2766e8a152cbbcedb1849a4b74 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mattyoung101/801a8d2766e8a152cbbcedb1849a4b74 to your computer and use it in GitHub Desktop.
Download ZIP
Yosys eqy reproducer
Raw
README.md
  1. Download gist
  2. Run eqy -f reproduce_sat.eqy - this should pass
  3. Run eqy -f reproduce_sby.eqy - this will not pass
Raw
gate.il
# Generated by Yosys 0.46+11 (git sha1 0200a7680, ccache clang++ 18.1.8 -Og -fPIC -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize=address)
autoidx 39
attribute \tamara_triplicate 1
attribute \top 1
attribute \src "../tests/verilog/not_dff_tmr.sv:5.1-25.10"
module \not_dff_tmr
attribute \src "../tests/verilog/not_dff_tmr.sv:13.7-13.9"
attribute \tamara_cone "1"
wire $auto$logic_graph.cpp:303:replicate$\ff__replica1_cone1__$6
attribute \src "../tests/verilog/not_dff_tmr.sv:13.7-13.9"
attribute \tamara_cone "1"
wire $auto$logic_graph.cpp:304:replicate$\ff__replica2_cone1__$7
wire $auto$voter_builder.cpp:38:build$A$10
wire $auto$voter_builder.cpp:39:build$B$11
wire $auto$voter_builder.cpp:40:build$C$12
wire $auto$voter_builder.cpp:43:build$OUT$13
wire $auto$voter_builder.cpp:44:build$ERR$14
wire $auto$voter_builder.cpp:50:build$not0_and2_wire$15
wire $auto$voter_builder.cpp:54:build$not1_and3_wire$17
wire $auto$voter_builder.cpp:58:build$not2_and5_wire$19
wire $auto$voter_builder.cpp:63:build$and0_or0_wire$21
wire $auto$voter_builder.cpp:67:build$and1_or0_wire$23
wire $auto$voter_builder.cpp:71:build$and2_or1_wire$25
wire $auto$voter_builder.cpp:75:build$and3_or1_wire$27
wire $auto$voter_builder.cpp:79:build$and4_or2_wire$29
wire $auto$voter_builder.cpp:83:build$and5_or3_wire$31
wire $auto$voter_builder.cpp:88:build$or0_or2_wire$33
wire $auto$voter_builder.cpp:92:build$or1_or3_wire$35
attribute \src "../tests/verilog/not_dff_tmr.sv:6.17-6.18"
wire input 1 \a
attribute \src "../tests/verilog/not_dff_tmr.sv:7.17-7.20"
wire input 2 \clk
attribute \src "../tests/verilog/not_dff_tmr.sv:10.18-10.21"
attribute \tamara_error_sink 1
wire output 4 \err
attribute \src "../tests/verilog/not_dff_tmr.sv:13.7-13.9"
attribute \tamara_cone "1"
attribute \tamara_original 1
wire \ff
attribute \src "../tests/verilog/not_dff_tmr.sv:8.18-8.19"
wire output 3 \o
attribute \src "../tests/verilog/not_dff_tmr.sv:19.12-19.15"
attribute \tamara_cone "1"
cell $logic_not $auto$logic_graph.cpp:276:replicate$$logic_not$../tests/verilog/not_dff_tmr.sv:19$2__replica1_cone1__$4
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$logic_graph.cpp:303:replicate$\ff__replica1_cone1__$6
connect \Y $auto$voter_builder.cpp:38:build$A$10
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_tmr.sv:15.1-17.4"
attribute \tamara_cone "1"
cell $dff $auto$logic_graph.cpp:276:replicate$$procdff$3__replica1_cone1__$8
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q $auto$logic_graph.cpp:303:replicate$\ff__replica1_cone1__$6
end
attribute \src "../tests/verilog/not_dff_tmr.sv:19.12-19.15"
attribute \tamara_cone "1"
cell $logic_not $auto$logic_graph.cpp:277:replicate$$logic_not$../tests/verilog/not_dff_tmr.sv:19$2__replica2_cone1__$5
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$logic_graph.cpp:304:replicate$\ff__replica2_cone1__$7
connect \Y $auto$voter_builder.cpp:39:build$B$11
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_tmr.sv:15.1-17.4"
attribute \tamara_cone "1"
cell $dff $auto$logic_graph.cpp:277:replicate$$procdff$3__replica2_cone1__$9
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q $auto$logic_graph.cpp:304:replicate$\ff__replica2_cone1__$7
end
attribute \tamara_voter 1
cell $logic_not $auto$voter_builder.cpp:51:build$not0$16
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:38:build$A$10
connect \Y $auto$voter_builder.cpp:50:build$not0_and2_wire$15
end
attribute \tamara_voter 1
cell $logic_not $auto$voter_builder.cpp:55:build$not1$18
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:39:build$B$11
connect \Y $auto$voter_builder.cpp:54:build$not1_and3_wire$17
end
attribute \tamara_voter 1
cell $logic_not $auto$voter_builder.cpp:59:build$not2$20
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:40:build$C$12
connect \Y $auto$voter_builder.cpp:58:build$not2_and5_wire$19
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:64:build$and0$22
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:39:build$B$11
connect \B $auto$voter_builder.cpp:40:build$C$12
connect \Y $auto$voter_builder.cpp:63:build$and0_or0_wire$21
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:68:build$and1$24
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:38:build$A$10
connect \B $auto$voter_builder.cpp:40:build$C$12
connect \Y $auto$voter_builder.cpp:67:build$and1_or0_wire$23
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:72:build$and2$26
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:50:build$not0_and2_wire$15
connect \B $auto$voter_builder.cpp:40:build$C$12
connect \Y $auto$voter_builder.cpp:71:build$and2_or1_wire$25
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:76:build$and3$28
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:54:build$not1_and3_wire$17
connect \B $auto$voter_builder.cpp:38:build$A$10
connect \Y $auto$voter_builder.cpp:75:build$and3_or1_wire$27
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:80:build$and4$30
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:38:build$A$10
connect \B $auto$voter_builder.cpp:39:build$B$11
connect \Y $auto$voter_builder.cpp:79:build$and4_or2_wire$29
end
attribute \tamara_voter 1
cell $logic_and $auto$voter_builder.cpp:84:build$and5$32
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:58:build$not2_and5_wire$19
connect \B $auto$voter_builder.cpp:39:build$B$11
connect \Y $auto$voter_builder.cpp:83:build$and5_or3_wire$31
end
attribute \tamara_voter 1
cell $logic_or $auto$voter_builder.cpp:89:build$or0$34
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:63:build$and0_or0_wire$21
connect \B $auto$voter_builder.cpp:67:build$and1_or0_wire$23
connect \Y $auto$voter_builder.cpp:88:build$or0_or2_wire$33
end
attribute \tamara_voter 1
cell $logic_or $auto$voter_builder.cpp:93:build$or1$36
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:71:build$and2_or1_wire$25
connect \B $auto$voter_builder.cpp:75:build$and3_or1_wire$27
connect \Y $auto$voter_builder.cpp:92:build$or1_or3_wire$35
end
attribute \tamara_voter 1
cell $logic_or $auto$voter_builder.cpp:96:build$or2$37
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:88:build$or0_or2_wire$33
connect \B $auto$voter_builder.cpp:79:build$and4_or2_wire$29
connect \Y $auto$voter_builder.cpp:43:build$OUT$13
end
attribute \tamara_voter 1
cell $logic_or $auto$voter_builder.cpp:99:build$or3$38
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $auto$voter_builder.cpp:92:build$or1_or3_wire$35
connect \B $auto$voter_builder.cpp:83:build$and5_or3_wire$31
connect \Y $auto$voter_builder.cpp:44:build$ERR$14
end
attribute \src "../tests/verilog/not_dff_tmr.sv:19.12-19.15"
attribute \tamara_cone "1"
attribute \tamara_original 1
cell $logic_not $logic_not$../tests/verilog/not_dff_tmr.sv:19$2
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A \ff
connect \Y $auto$voter_builder.cpp:40:build$C$12
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_tmr.sv:15.1-17.4"
attribute \tamara_cone "1"
attribute \tamara_original 1
cell $dff $procdff$3
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q \ff
end
connect \o $auto$voter_builder.cpp:43:build$OUT$13
connect \err $auto$voter_builder.cpp:44:build$ERR$14
end
Raw
gold.il
# Generated by Yosys 0.46+11 (git sha1 0200a7680, ccache clang++ 18.1.8 -Og -fPIC -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize=address)
autoidx 19
attribute \top 1
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:3.1-26.10"
module \not_dff_tmr
attribute \src "../tests/verilog/voter.sv:10.45-10.52"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$12_Y
attribute \src "../tests/verilog/voter.sv:10.19-10.26"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$7_Y
attribute \src "../tests/verilog/voter.sv:10.32-10.39"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$9_Y
attribute \src "../tests/verilog/voter.sv:9.19-9.25"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$1_Y
attribute \src "../tests/verilog/voter.sv:9.31-9.37"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$2_Y
attribute \src "../tests/verilog/voter.sv:9.43-9.49"
wire $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$4_Y
attribute \src "../tests/verilog/voter.sv:10.50-10.52"
wire $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$11_Y
attribute \src "../tests/verilog/voter.sv:10.19-10.21"
wire $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$6_Y
attribute \src "../tests/verilog/voter.sv:10.37-10.39"
wire $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$8_Y
attribute \src "../tests/verilog/voter.sv:10.18-10.40"
wire $flatten\voter.$logic_or$../tests/verilog/voter.sv:10$10_Y
attribute \src "../tests/verilog/voter.sv:9.18-9.38"
wire $flatten\voter.$logic_or$../tests/verilog/voter.sv:9$3_Y
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:4.17-4.18"
wire input 1 \a
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:5.17-5.20"
wire input 2 \clk
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:7.18-7.21"
wire output 4 \err
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:10.7-10.10"
wire \ff1
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:11.7-11.10"
wire \ff2
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:12.7-12.10"
wire \ff3
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:6.18-6.19"
wire output 3 \o
attribute \hdlname "voter a"
attribute \src "../tests/verilog/voter.sv:3.17-3.18"
wire \voter.a
attribute \hdlname "voter b"
attribute \src "../tests/verilog/voter.sv:4.17-4.18"
wire \voter.b
attribute \hdlname "voter c"
attribute \src "../tests/verilog/voter.sv:5.17-5.18"
wire \voter.c
attribute \hdlname "voter err"
attribute \src "../tests/verilog/voter.sv:7.18-7.21"
wire \voter.err
attribute \hdlname "voter out"
attribute \src "../tests/verilog/voter.sv:6.18-6.21"
wire \voter.out
attribute \src "../tests/verilog/voter.sv:10.45-10.52"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$12
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.b
connect \B $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$11_Y
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$12_Y
end
attribute \src "../tests/verilog/voter.sv:10.19-10.26"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$7
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$6_Y
connect \B \voter.c
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$7_Y
end
attribute \src "../tests/verilog/voter.sv:10.32-10.39"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$9
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.a
connect \B $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$8_Y
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$9_Y
end
attribute \src "../tests/verilog/voter.sv:9.19-9.25"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$1
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.a
connect \B \voter.b
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$1_Y
end
attribute \src "../tests/verilog/voter.sv:9.31-9.37"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$2
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.b
connect \B \voter.c
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$2_Y
end
attribute \src "../tests/verilog/voter.sv:9.43-9.49"
cell $logic_and $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$4
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.a
connect \B \voter.c
connect \Y $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$4_Y
end
attribute \src "../tests/verilog/voter.sv:10.50-10.52"
cell $logic_not $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$11
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.c
connect \Y $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$11_Y
end
attribute \src "../tests/verilog/voter.sv:10.19-10.21"
cell $logic_not $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$6
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.a
connect \Y $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$6_Y
end
attribute \src "../tests/verilog/voter.sv:10.37-10.39"
cell $logic_not $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$8
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \Y_WIDTH 1
connect \A \voter.b
connect \Y $flatten\voter.$logic_not$../tests/verilog/voter.sv:10$8_Y
end
attribute \src "../tests/verilog/voter.sv:10.18-10.40"
cell $logic_or $flatten\voter.$logic_or$../tests/verilog/voter.sv:10$10
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$7_Y
connect \B $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$9_Y
connect \Y $flatten\voter.$logic_or$../tests/verilog/voter.sv:10$10_Y
end
attribute \src "../tests/verilog/voter.sv:10.18-10.53"
cell $logic_or $flatten\voter.$logic_or$../tests/verilog/voter.sv:10$13
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $flatten\voter.$logic_or$../tests/verilog/voter.sv:10$10_Y
connect \B $flatten\voter.$logic_and$../tests/verilog/voter.sv:10$12_Y
connect \Y \voter.err
end
attribute \src "../tests/verilog/voter.sv:9.18-9.38"
cell $logic_or $flatten\voter.$logic_or$../tests/verilog/voter.sv:9$3
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$1_Y
connect \B $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$2_Y
connect \Y $flatten\voter.$logic_or$../tests/verilog/voter.sv:9$3_Y
end
attribute \src "../tests/verilog/voter.sv:9.18-9.50"
cell $logic_or $flatten\voter.$logic_or$../tests/verilog/voter.sv:9$5
parameter \A_SIGNED 0
parameter \A_WIDTH 1
parameter \B_SIGNED 0
parameter \B_WIDTH 1
parameter \Y_WIDTH 1
connect \A $flatten\voter.$logic_or$../tests/verilog/voter.sv:9$3_Y
connect \B $flatten\voter.$logic_and$../tests/verilog/voter.sv:9$4_Y
connect \Y \voter.out
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:14.1-16.4"
cell $dff $procdff$15
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q \ff1
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:14.1-16.4"
cell $dff $procdff$16
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q \ff2
end
attribute \always_ff 1
attribute \src "../tests/verilog/not_dff_manual_tmr.sv:14.1-16.4"
cell $dff $procdff$17
parameter \CLK_POLARITY 1'1
parameter \WIDTH 1
connect \CLK \clk
connect \D \a
connect \Q \ff3
end
attribute \cell_module_not_derived 1
attribute \cell_src "../tests/verilog/not_dff_manual_tmr.sv:18.7-24.2"
attribute \module "voter"
attribute \module_src "../tests/verilog/voter.sv:2.1-11.10"
cell $scopeinfo \voter
parameter \TYPE "module"
end
connect \voter.a \ff1
connect \voter.b \ff2
connect \voter.c \ff3
connect \err \voter.err
connect \o \voter.out
end
Raw
original.eqy
# Test that checks that a manual implementation of the not_dff_tmr circuit is equivalent to the TaMaRa auto
# generated one
[gold]
read_verilog -sv ../tests/verilog/voter.sv
read_verilog -sv ../tests/verilog/not_dff_manual_tmr.sv
prep -top not_dff_tmr
flatten
[gate]
plugin -i libtamara.so
read_verilog -DTAMARA -sv ../tests/verilog/not_dff_tmr.sv
hierarchy -top not_dff_tmr
prep
tamara_tmr
# [strategy sby]
# use sby
# depth 2
# engine smtbmc yices
[strategy sat]
use sat
depth 25
Raw
reproduce_sat.eqy
# Test that checks that a manual implementation of the not_dff_tmr circuit is equivalent to the TaMaRa auto
# generated one
[gold]
read_rtlil gate.il
[gate]
read_rtlil gold.il
[strategy sat]
use sat
depth 25
Raw
reproduce_sby.eqy
# Test that checks that a manual implementation of the not_dff_tmr circuit is equivalent to the TaMaRa auto
# generated one
[gold]
read_rtlil gate.il
[gate]
read_rtlil gold.il
[strategy sby]
use sby
depth 2
engine smtbmc yices
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment