mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	add assertions for synth_microchip tests
This commit is contained in:
		
							parent
							
								
									e3c4791e5b
								
							
						
					
					
						commit
						8e7ec2d660
					
				
					 45 changed files with 67 additions and 49 deletions
				
			
		| 
						 | 
					@ -31,9 +31,9 @@ endmodule
 | 
				
			||||||
 | 
					
 | 
				
			||||||
(* techmap_celltype = "$reduce_xor" *)
 | 
					(* techmap_celltype = "$reduce_xor" *)
 | 
				
			||||||
module \$__microchip_XOR8_ (A, Y);
 | 
					module \$__microchip_XOR8_ (A, Y);
 | 
				
			||||||
	parameter A_SIGNED = 0;
 | 
						parameter A_SIGNED = 1;
 | 
				
			||||||
	parameter A_WIDTH = 0;
 | 
						parameter A_WIDTH = 8;
 | 
				
			||||||
	parameter Y_WIDTH = 0;
 | 
						parameter Y_WIDTH = 1;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
	input [A_WIDTH-1:0] A;
 | 
						input [A_WIDTH-1:0] A;
 | 
				
			||||||
	output [Y_WIDTH-1:0] Y;
 | 
						output [Y_WIDTH-1:0] Y;
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
							
								
								
									
										4
									
								
								tests/arch/microchip/.gitignore
									
										
									
									
										vendored
									
									
										Normal file
									
								
							
							
						
						
									
										4
									
								
								tests/arch/microchip/.gitignore
									
										
									
									
										vendored
									
									
										Normal file
									
								
							| 
						 | 
					@ -0,0 +1,4 @@
 | 
				
			||||||
 | 
					*.log
 | 
				
			||||||
 | 
					/run-test.mk
 | 
				
			||||||
 | 
					*.vm
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -21,7 +21,7 @@ module Registers(
 | 
				
			||||||
	input en,
 | 
						input en,
 | 
				
			||||||
	input rst,
 | 
						input rst,
 | 
				
			||||||
	input D,
 | 
						input D,
 | 
				
			||||||
	output Q
 | 
						output reg Q
 | 
				
			||||||
);
 | 
					);
 | 
				
			||||||
parameter LOAD_DATA = 1;
 | 
					parameter LOAD_DATA = 1;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -19,5 +19,6 @@ read_verilog Registers.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top Registers -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top Registers -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
# write final outputfile
 | 
					select -assert-count 1 t:SLE
 | 
				
			||||||
write_verilog -noexpr Registers.vm
 | 
					select -assert-count 1 t:CLKBUF
 | 
				
			||||||
 | 
					select -assert-none t:SLE t:CLKBUF %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog carryout.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top carryout -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top carryout -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr carryout.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog cascade.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top cascade -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top cascade -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr cascade.vm
 | 
					select -assert-count 2 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -13,9 +13,12 @@
 | 
				
			||||||
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 | 
					# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 | 
				
			||||||
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 | 
					# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 | 
				
			||||||
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 | 
					# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 | 
				
			||||||
 | 
					
 | 
				
			||||||
read_verilog dff_opt.v 
 | 
					read_verilog dff_opt.v 
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top dff_opt -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top dff_opt -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
# write final outputfile
 | 
					select -assert-count 1 t:SLE
 | 
				
			||||||
write_verilog -noexpr dff_opt.vm
 | 
					select -assert-count 1 t:CFG4
 | 
				
			||||||
 | 
					select -assert-count 1 t:CLKBUF
 | 
				
			||||||
 | 
					select -assert-none t:SLE t:CFG4 t:CLKBUF %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog full_dsp.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top full_dsp -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top full_dsp -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr full_dsp.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,6 @@ read_verilog large_mult.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top large_mult -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top large_mult -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr large_mult.vm
 | 
					select -assert-count 2 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -20,5 +20,5 @@ read_verilog mac.v
 | 
				
			||||||
# run the synth flow, specifies top module and additional parameters
 | 
					# run the synth flow, specifies top module and additional parameters
 | 
				
			||||||
synth_microchip -top mac -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top mac -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
# write final outputfile
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
write_verilog -noexpr mac.vm
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog postAdd_mult.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top postAdd_mult -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top postAdd_mult -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr postAdd_mult.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -16,6 +16,8 @@
 | 
				
			||||||
 | 
					
 | 
				
			||||||
read_verilog post_adder.v
 | 
					read_verilog post_adder.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top post_adder -abc9 -family polarfire
 | 
					synth_microchip -top post_adder -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr post_adder.vm
 | 
					 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog pre_adder_dsp.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top pre_adder_dsp -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top pre_adder_dsp -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr pre_adder_dsp.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,7 @@ read_verilog ram_SDP.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top ram_SDP -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top ram_SDP -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr ram_SDP.vm
 | 
					select -assert-count 1 t:RAM1K20
 | 
				
			||||||
 | 
					select -assert-count 1 t:CFG1
 | 
				
			||||||
 | 
					select -assert-none t:RAM1K20 t:CFG1 %% t:* %D
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog ram_TDP.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top ram_TDP -abc9 -family polarfire -noiopad -debug_memory
 | 
					synth_microchip -top ram_TDP -abc9 -family polarfire -noiopad -debug_memory
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr ram_TDP.vm
 | 
					select -assert-count 1 t:RAM1K20
 | 
				
			||||||
 | 
					select -assert-none t:RAM1K20 %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,6 @@ read_verilog reduce.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top reduce -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top reduce -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr reduce.vm
 | 
					select -assert-count 1 t:XOR8
 | 
				
			||||||
 | 
					select -assert-none t:XOR8 %% t:* %D
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog reg_c.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top reg_c -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top reg_c -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr reg_c.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog reg_test.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top reg_test -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top reg_test -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr reg_test.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
							
								
								
									
										4
									
								
								tests/arch/microchip/run-test.sh
									
										
									
									
									
										Executable file
									
								
							
							
						
						
									
										4
									
								
								tests/arch/microchip/run-test.sh
									
										
									
									
									
										Executable file
									
								
							| 
						 | 
					@ -0,0 +1,4 @@
 | 
				
			||||||
 | 
					#!/usr/bin/env bash
 | 
				
			||||||
 | 
					set -eu
 | 
				
			||||||
 | 
					source ../../gen-tests-makefile.sh
 | 
				
			||||||
 | 
					run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog signed_mult.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top signed_mult -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top signed_mult -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr signed_mult.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog simple_ram.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top simple_ram -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top simple_ram -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr simple_ram.vm
 | 
					select -assert-count 1 t:RAM1K20
 | 
				
			||||||
 | 
					select -assert-none t:RAM1K20 %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog unsigned_mult.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top unsigned_mult -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top unsigned_mult -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr unsigned_mult.vm
 | 
					select -assert-count 1 t:MACC_PA
 | 
				
			||||||
 | 
					select -assert-none t:MACC_PA %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -17,9 +17,9 @@ OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 | 
				
			||||||
*/
 | 
					*/
 | 
				
			||||||
 | 
					
 | 
				
			||||||
module uram_ar(data,waddr,we,clk,q);
 | 
					module uram_ar(data,waddr,we,clk,q);
 | 
				
			||||||
parameter d_width = 27;
 | 
					parameter d_width = 12;
 | 
				
			||||||
parameter addr_width = 2;
 | 
					parameter addr_width = 2;
 | 
				
			||||||
parameter mem_depth = 4;
 | 
					parameter mem_depth = 12;
 | 
				
			||||||
input [d_width-1:0] data;
 | 
					input [d_width-1:0] data;
 | 
				
			||||||
input [addr_width-1:0] waddr;
 | 
					input [addr_width-1:0] waddr;
 | 
				
			||||||
input we, clk;
 | 
					input we, clk;
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog uram_ar.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top uram_ar -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top uram_ar -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr uram_ar.vm
 | 
					select -assert-count 1 t:RAM64x12
 | 
				
			||||||
 | 
					select -assert-none t:RAM64x12 %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog uram_sr.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top uram_sr -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top uram_sr -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr uram_sr.vm
 | 
					select -assert-count 1 t:RAM64x12
 | 
				
			||||||
 | 
					select -assert-none t:RAM64x12 %% t:* %D
 | 
				
			||||||
| 
						 | 
					@ -23,25 +23,8 @@ module widemux(
 | 
				
			||||||
	output Y
 | 
						output Y
 | 
				
			||||||
 | 
					
 | 
				
			||||||
);
 | 
					);
 | 
				
			||||||
 | 
					assign Y = S1 ? (S0 ? data[3] : data[1]) : (S0 ? data[2] : data[0]);
 | 
				
			||||||
 | 
					
 | 
				
			||||||
wire A, B;
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
always @ (*) begin 
 | 
					 | 
				
			||||||
		if (S0)begin
 | 
					 | 
				
			||||||
		A = data[1];
 | 
					 | 
				
			||||||
		B = data[3];
 | 
					 | 
				
			||||||
		end else begin 
 | 
					 | 
				
			||||||
		A = data[0];
 | 
					 | 
				
			||||||
		B = data[2];
 | 
					 | 
				
			||||||
	end
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
	if (S1)begin
 | 
					 | 
				
			||||||
		Y = A;
 | 
					 | 
				
			||||||
	end else begin
 | 
					 | 
				
			||||||
		Y = B;
 | 
					 | 
				
			||||||
	end
 | 
					 | 
				
			||||||
 | 
					 | 
				
			||||||
end
 | 
					 | 
				
			||||||
endmodule
 | 
					endmodule
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -18,4 +18,5 @@ read_verilog widemux.v
 | 
				
			||||||
 | 
					
 | 
				
			||||||
synth_microchip -top widemux -abc9 -family polarfire -noiopad
 | 
					synth_microchip -top widemux -abc9 -family polarfire -noiopad
 | 
				
			||||||
 | 
					
 | 
				
			||||||
write_verilog -noexpr widemux.vm
 | 
					select -assert-count 1 t:MX4
 | 
				
			||||||
 | 
					select -assert-none t:MX4 %% t:* %D
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue