Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)
				
			 
			
		 
		
		
		
			You can not select more than 25 topics
			Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
		
		
		
		
		
			
	
	
		
			
				
				
					
						
						
							|  | include tests.mk | 
						
						
							|  | 
 | 
						
						
							|  | 
 | 
						
						
							|  | .PHONY: all clean | 
						
						
							|  | 
 | 
						
						
							|  | all: ${psl_tests} | 
						
						
							|  | 
 | 
						
						
							|  | 
 | 
						
						
							|  | %: %.vhd work/%.sby | 
						
						
							|  | 	ghdl --synth --std=08 $@.vhd -e issue > work/$@_synth.vhd | 
						
						
							|  | 	-sby --yosys "yosys -m ghdl" -f -d work/$@ work/$@.sby bmc | 
						
						
							|  | 
 | 
						
						
							|  | work/%.sby: template.sby | 
						
						
							|  | 	mkdir -p work | 
						
						
							|  | 	sed 's/__ISSUE__/$(basename $(notdir $@))/g' $< > $@ | 
						
						
							|  | 
 | 
						
						
							|  | 
 | 
						
						
							|  | clean: | 
						
						
							|  | 	rm -rf work
 |