Fix regressions in tests

architecture/synth_ice40/synth_ice40_nobram.ys

@@ -33,5 +33,5 @@ cd top
 
 select -assert-count 6 t:SB_DFF
 select -assert-count 384 t:SB_DFFE
-select -assert-count 368 t:SB_LUT4
+select -assert-count 377 t:SB_LUT4
 select -assert-none t:SB_DFF t:SB_DFFE t:SB_LUT4 %% t:* %D

architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_asym_ram_tdp_write_first.ys

@@ -17,13 +17,13 @@ stat
 #Vivado synthesizes 1 RAMB18E1.
 select -assert-count 2 t:BUFG
 select -assert-count 200 t:FDRE
-select -assert-count 10 t:LUT2
-select -assert-count 44 t:LUT3
-select -assert-count 81 t:LUT4
-select -assert-count 104 t:LUT5
-select -assert-count 560 t:LUT6
-select -assert-count 261 t:MUXF7
-select -assert-count 127 t:MUXF8
+select -assert-count 15 t:LUT2
+select -assert-count 64 t:LUT3
+select -assert-count 4 t:LUT4
+select -assert-count 91 t:LUT5
+select -assert-count 719 t:LUT6
+select -assert-count 328 t:MUXF7
+select -assert-count 148 t:MUXF8
 
 
 select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D

architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_fsm_1.ys

@@ -2,15 +2,20 @@ read_verilog ../fsm_1.v
 hierarchy -top fsm_1
 proc
 flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd fsm_1 # Constrain all select calls below inside the top module
 #Vivado synthesizes 2 LUT5, 2 LUT4, 1 LUT3, 4 FDRE.
 stat
 select -assert-count 1 t:BUFG
-select -assert-count 4 t:FDRE
-select -assert-count 2 t:LUT4
-select -assert-count 2 t:LUT5
-select -assert-count 1 t:LUT6
+select -assert-count 6 t:FDRE
+select -assert-count 2 t:LUT2
+select -assert-count 3 t:LUT3
+select -assert-count 4 t:LUT6
+select -assert-count 2 t:MUXF7
+select -assert-count 1 t:MUXF8
 
-select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D
+select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D

regression/issue_00705/issue_00705.pat

-.MASK({ _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_, _18_ }),
+.MASK({ _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_, _2_ }),