mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 03:32:29 +00:00 
			
		
		
		
	Add more tests
This commit is contained in:
		
							parent
							
								
									9cba05285b
								
							
						
					
					
						commit
						ca1fac7c47
					
				
					 1 changed files with 152 additions and 0 deletions
				
			
		|  | @ -356,3 +356,155 @@ design -import gate -as gate | |||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs gold gate miter | ||||
| sat -verify -prove-asserts -show-ports miter | ||||
| 
 | ||||
| ## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132 | ||||
| 
 | ||||
| design -reset | ||||
| read_verilog -formal <<EOT | ||||
| module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); | ||||
| always @* begin | ||||
|     o <= {{W{{1'bx}}}}; | ||||
|     if (s[0] == 1'b0) | ||||
|      if (s[1] == 1'b0) | ||||
|       if (s[2] == 1'b0) | ||||
|        o <= i[0*W+:W]; | ||||
|       else | ||||
|        o <= i[1*W+:W]; | ||||
|      else | ||||
|       if (s[2] == 1'b0) | ||||
|        o <= i[2*W+:W]; | ||||
|       else | ||||
|        o <= i[3*W+:W]; | ||||
|     else | ||||
|      if (s[1] == 1'b0) | ||||
|       if (s[2] == 1'b0) | ||||
|        o <= i[4*W+:W]; | ||||
| end | ||||
| endmodule | ||||
| EOT | ||||
| prep | ||||
| design -save gold | ||||
| 
 | ||||
| wreduce | ||||
| opt -full | ||||
| techmap | ||||
| muxcover -mux8=350 | ||||
| clean | ||||
| opt_expr -mux_bool | ||||
| select -assert-count 0 t:$_MUX_ | ||||
| select -assert-count 0 t:$_MUX4_ | ||||
| select -assert-count 1 t:$_MUX8_ | ||||
| select -assert-count 0 t:$_MUX16_ | ||||
| techmap -map +/simcells.v t:$_MUX8_ | ||||
| design -stash gate | ||||
| 
 | ||||
| design -import gold -as gold | ||||
| design -import gate -as gate | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter | ||||
| sat -verify -prove-asserts -show-ports miter | ||||
| 
 | ||||
| ## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 | ||||
| design -load gold | ||||
| 
 | ||||
| wreduce | ||||
| opt -full | ||||
| techmap | ||||
| muxcover -mux8=350 -nodecode | ||||
| clean | ||||
| opt_expr -mux_bool | ||||
| select -assert-count 0 t:$_MUX_ | ||||
| select -assert-count 0 t:$_MUX4_ | ||||
| select -assert-count 1 t:$_MUX8_ | ||||
| select -assert-count 0 t:$_MUX16_ | ||||
| techmap -map +/simcells.v t:$_MUX8_ | ||||
| design -stash gate | ||||
| 
 | ||||
| design -import gold -as gold | ||||
| design -import gate -as gate | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter | ||||
| sat -verify -prove-asserts -show-ports miter | ||||
| 
 | ||||
| ## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132 | ||||
| 
 | ||||
| design -reset | ||||
| read_verilog -formal <<EOT | ||||
| module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); | ||||
| always @* begin | ||||
|     o <= {{W{{1'bx}}}}; | ||||
|     if (s[3] == 1'b0) | ||||
|      if (s[2] == 1'b0) | ||||
|       if (s[1] == 1'b0) | ||||
|        if (s[0] == 1'b0) | ||||
|         o <= i[0*W+:W]; | ||||
|        else | ||||
|         o <= i[1*W+:W]; | ||||
|       else | ||||
|        if (s[0] == 1'b0) | ||||
|         o <= i[2*W+:W]; | ||||
|        else | ||||
|         o <= i[3*W+:W]; | ||||
|      else | ||||
|       if (s[1] == 1'b0) | ||||
|        if (s[0] == 1'b0) | ||||
|         o <= i[4*W+:W]; | ||||
|        else | ||||
|         o <= i[5*W+:W]; | ||||
|       else | ||||
|        if (s[0] == 1'b0) | ||||
|         o <= i[6*W+:W]; | ||||
|        else | ||||
|         o <= i[7*W+:W]; | ||||
|     else | ||||
|      if (s[2] == 1'b0) | ||||
|       if (s[1] == 1'b0) | ||||
|        if (s[0] == 1'b0) | ||||
|         o <= i[8*W+:W]; | ||||
| end | ||||
| endmodule | ||||
| EOT | ||||
| prep | ||||
| design -save gold | ||||
| 
 | ||||
| wreduce | ||||
| opt -full | ||||
| techmap | ||||
| muxcover -mux16=750 | ||||
| clean | ||||
| opt_expr -mux_bool | ||||
| select -assert-count 0 t:$_MUX_ | ||||
| select -assert-count 0 t:$_MUX4_ | ||||
| select -assert-count 0 t:$_MUX8_ | ||||
| select -assert-count 1 t:$_MUX16_ | ||||
| techmap -map +/simcells.v t:$_MUX16_ | ||||
| design -stash gate | ||||
| 
 | ||||
| design -import gold -as gold | ||||
| design -import gate -as gate | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter | ||||
| sat -verify -prove-asserts -show-ports miter | ||||
| 
 | ||||
| ## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 | ||||
| 
 | ||||
| design -load gold | ||||
| 
 | ||||
| wreduce | ||||
| opt -full | ||||
| techmap | ||||
| muxcover -mux16=750 -nodecode | ||||
| clean | ||||
| opt_expr -mux_bool | ||||
| select -assert-count 0 t:$_MUX_ | ||||
| select -assert-count 0 t:$_MUX4_ | ||||
| select -assert-count 0 t:$_MUX8_ | ||||
| select -assert-count 1 t:$_MUX16_ | ||||
| techmap -map +/simcells.v t:$_MUX16_ | ||||
| design -stash gate | ||||
| 
 | ||||
| design -import gold -as gold | ||||
| design -import gate -as gate | ||||
| 
 | ||||
| miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter | ||||
| sat -verify -prove-asserts -show-ports miter | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue