mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-24 20:16:01 +00:00
Code Activity

glift: Add examples, including a number of benchmarks used in some academic works.

Browse source
This commit is contained in:
Alberto Gonzalez 2020-04-24 08:23:08 +00:00
parent 72cebef279
commit ca3844d44e
No known key found for this signature in database
GPG key ID: 8395A8BA109708B2
18 changed files with 7279 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

39
examples/smtbmc/glift/mux2.ys Normal file
View file

@ -0,0 +1,39 @@
logger -expect log "SAT proof finished - no model found: SUCCESS!" 1
logger -expect log "Number of cells:.*[\t ]12" 1
logger -expect log "Number of cells:.*[\t ]20" 1
logger -expect log "Problem is satisfiable with \\gate.__glift_weight = 11." 1
logger -expect log "Problem is NOT satisfiable with \\gate.__glift_weight <= 10." 1
logger -expect log "Wire \\gate.__glift_weight is minimized at 11." 1
logger -expect log "Specializing .* from file with .* = 1." 2
logger -expect log "Specializing .* from file with .* = 0." 4
read_verilog <<EOT
module mux2(a, b, s, y);
input a, b, s;
output y;
wire s_n = ~s;
wire t0 = s & a;
wire t1 = s_n & b;
assign y = t0 | t1;
endmodule
EOT
techmap
copy mux2 uut
copy mux2 spec
delete mux2
glift -optimize-precise uut
glift -create-precise spec
design -push-copy
miter -equiv spec uut qbfmiter
flatten
delete spec uut
qbfsat -assume-outputs -assume-negative-polarity -write-solution mux2.soln qbfmiter
design -pop
copy uut solved
qbfsat -specialize-from-file mux2.soln solved
opt
miter -equiv spec solved proofmiter
flatten proofmiter
sat -prove trigger 0 proofmiter
delete proofmiter
stat solved spec