mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Ignore L_pi nets in "yosys-smtbmc --cex"
This commit is contained in:
		
							parent
							
								
									9e980a2bb0
								
							
						
					
					
						commit
						281a977b39
					
				
					 1 changed files with 5 additions and 2 deletions
				
			
		| 
						 | 
					@ -319,12 +319,15 @@ assert topmod in smt.modinfo
 | 
				
			||||||
 | 
					
 | 
				
			||||||
if cexfile is not None:
 | 
					if cexfile is not None:
 | 
				
			||||||
    with open(cexfile, "r") as f:
 | 
					    with open(cexfile, "r") as f:
 | 
				
			||||||
        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?(@\d+)=([01])')
 | 
					        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
 | 
				
			||||||
        for entry in f.read().split():
 | 
					        for entry in f.read().split():
 | 
				
			||||||
            match = cex_regex.match(entry)
 | 
					            match = cex_regex.match(entry)
 | 
				
			||||||
            assert match
 | 
					            assert match
 | 
				
			||||||
 | 
					
 | 
				
			||||||
            name, bit, step, val = match.group(1), match.group(2), match.group(3), match.group(4)
 | 
					            name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					            if extra_name != "":
 | 
				
			||||||
 | 
					                continue
 | 
				
			||||||
 | 
					
 | 
				
			||||||
            if name not in smt.modinfo[topmod].inputs:
 | 
					            if name not in smt.modinfo[topmod].inputs:
 | 
				
			||||||
                continue
 | 
					                continue
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue