mirror of
https://github.com/YosysHQ/yosys
synced 2026-07-19 21:55:48 +00:00
WIP
This commit is contained in:
parent
dab9a386cc
commit
c3457e2e5c
35 changed files with 204 additions and 63 deletions
|
|
@ -8,11 +8,11 @@ copy gold fine
|
|||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter
|
||||
sat -verify -prove-asserts -show-ports miter
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ proc
|
|||
equiv_opt -assert opt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$dffe r:WIDTH=2 %i
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
####################
|
||||
|
||||
|
|
@ -25,7 +25,7 @@ equiv_opt -assert opt
|
|||
design -load postopt
|
||||
wreduce
|
||||
select -assert-count 1 t:$dffe r:WIDTH=2 %i
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
###################
|
||||
|
||||
|
|
@ -40,7 +40,7 @@ proc
|
|||
equiv_opt -assert opt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$dffe r:WIDTH=2 %i
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
###################
|
||||
|
||||
|
|
@ -56,7 +56,7 @@ equiv_opt -assert opt
|
|||
design -load postopt
|
||||
dump
|
||||
select -assert-count 1 t:$dffe r:WIDTH=4 %i
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$dffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
####################
|
||||
|
||||
|
|
@ -72,7 +72,7 @@ equiv_opt -assert opt
|
|||
design -load postopt
|
||||
wreduce
|
||||
select -assert-count 1 t:$sdffe r:WIDTH=2 %i
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
####################
|
||||
|
||||
|
|
@ -91,7 +91,7 @@ equiv_opt -assert opt
|
|||
design -load postopt
|
||||
wreduce
|
||||
select -assert-count 1 t:$sdffe r:WIDTH=2 %i
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
####################
|
||||
|
||||
|
|
@ -127,4 +127,4 @@ sat -tempinduct -verify -prove-asserts -show-ports miter
|
|||
|
||||
design -load gate
|
||||
select -assert-count 1 t:$sdffe r:WIDTH=3 %i
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$input_port %d
|
||||
select -assert-count 0 t:$sdffe %% t:* %D t:$*_port %d t:$public %d
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ alumacc
|
|||
equiv_opt -assert opt_expr -fine
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$pos
|
||||
select -assert-none t:$pos t:* %D t:$input_port %d
|
||||
select -assert-none t:$pos t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -20,7 +20,7 @@ EOT
|
|||
|
||||
alumacc
|
||||
select -assert-count 1 t:$alu
|
||||
select -assert-none t:$alu t:* %D t:$input_port %d
|
||||
select -assert-none t:$alu t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -33,7 +33,7 @@ EOT
|
|||
equiv_opt -assert opt_expr -fine
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$pos
|
||||
select -assert-none t:$pos t:* %D t:$input_port %d
|
||||
select -assert-none t:$pos t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -46,7 +46,7 @@ EOT
|
|||
equiv_opt -assert opt_expr -fine
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$pos
|
||||
select -assert-none t:$pos t:* %D t:$input_port %d
|
||||
select -assert-none t:$pos t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -60,7 +60,7 @@ alumacc
|
|||
equiv_opt -assert opt_expr -fine
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$not %% t:* %D t:$input_port %d
|
||||
select -assert-none t:$not %% t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -76,7 +76,7 @@ design -load postopt
|
|||
select -assert-count 1 t:$alu
|
||||
select -assert-count 1 t:$alu r:Y_WIDTH=3 %i
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$alu t:$not t:* %D %D t:$input_port %d
|
||||
select -assert-none t:$alu t:$not t:* %D %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -93,7 +93,7 @@ dump
|
|||
select -assert-count 2 t:$alu
|
||||
select -assert-count 1 t:$alu r:Y_WIDTH=2 %i
|
||||
select -assert-count 1 t:$alu r:Y_WIDTH=3 %i
|
||||
select -assert-none t:$alu t:* %D t:$input_port %d
|
||||
select -assert-none t:$alu t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -108,7 +108,7 @@ equiv_opt -assert opt -fine
|
|||
design -load postopt
|
||||
select -assert-count 2 t:$alu
|
||||
select -assert-count 2 t:$alu r:Y_WIDTH=3 %i
|
||||
select -assert-none t:$alu t:* %D t:$input_port %d
|
||||
select -assert-none t:$alu t:* %D t:$*_port %d t:$public %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ copy gold fine_keepdc
|
|||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
|
|
@ -27,12 +27,12 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
|
|
@ -56,12 +56,12 @@ copy gold fine_keepdc
|
|||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
|
|
@ -71,12 +71,12 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -fine -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 2 c:* t:$input_port %d
|
||||
select -assert-count 2 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ opt_expr -fine
|
|||
# The division by zero should be removed
|
||||
select -assert-count 0 t:$div
|
||||
# No cells should be left as it's replaced with constant undef
|
||||
select -assert-none t:* t:$input_port %d
|
||||
select -assert-none t:* t:$*_port %d t:$public %d
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
|
|
@ -64,7 +64,7 @@ design -load postopt
|
|||
# The mux should be removed completely
|
||||
select -assert-count 0 t:$mux
|
||||
# No additional cells needed - direct connection
|
||||
select -assert-none t:* t:$input_port %d
|
||||
select -assert-none t:* t:$*_port %d t:$public %d
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
|
|
@ -110,7 +110,7 @@ design -load postopt
|
|||
# The comparison of different constants should be replaced with constant 0
|
||||
select -assert-count 0 t:$eq
|
||||
# No other cells should be present (just the constant driver)
|
||||
select -assert-none t:* t:$input_port %d
|
||||
select -assert-none t:* t:$*_port %d t:$public %d
|
||||
|
||||
# opt.opt_expr.invert.double
|
||||
|
||||
|
|
@ -131,7 +131,7 @@ design -load postopt
|
|||
opt_clean -purge
|
||||
select -assert-count 0 t:$not
|
||||
# No other cells should be present
|
||||
select -assert-none t:* t:$input_port %d
|
||||
select -assert-none t:* t:$*_port %d t:$public %d
|
||||
|
||||
# opt.opt_expr.reduce_xnor_not
|
||||
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ copy gold fine_keepdc
|
|||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
|
|
@ -27,12 +27,12 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
|
|
@ -56,12 +56,12 @@ copy gold fine_keepdc
|
|||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
|
|
@ -71,12 +71,12 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -fine -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 2 c:* t:$input_port %d
|
||||
select -assert-count 2 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
|
|
|
|||
|
|
@ -66,12 +66,12 @@ copy gold fine_keepdc
|
|||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:* t:$input_port %d
|
||||
select -assert-none c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
|
|
@ -81,12 +81,12 @@ sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:* t:$input_port %d
|
||||
select -assert-count 1 c:* t:$*_port %d t:$public %d
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
|
|
|
|||
|
|
@ -196,7 +196,7 @@ select -module dffe_10 -assert-count 1 t:\$_NOT_
|
|||
select -module dffe_11 -assert-count 0 t:\$_NOT_
|
||||
|
||||
# $sdffe is not gated
|
||||
select -module sdffe -assert-count 0 sdffe t:* t:\$sdffe %d t:\$input_port %d
|
||||
select -module sdffe -assert-count 0 sdffe t:* t:\$sdffe %d t:\$*_port %d t:\$public %d
|
||||
|
||||
#------------------------------------------------------------------------------
|
||||
|
||||
|
|
|
|||
|
|
@ -28,4 +28,4 @@ hierarchy -top top
|
|||
rename -seed 2 -scramble-name c:bar
|
||||
select -assert-none c:bar
|
||||
select -assert-count 1 c:$_*_
|
||||
select -assert-none c:$_*_ w:* foo/c:$add$<<EOF:2$1 %% %n
|
||||
select -assert-none c:$_*_ w:* foo/t:$add %% %n
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue