Unable to access symbols defined within Verilog modules

When I run CoSA --problems examples/counters/problem_verilog.txt from within my unmodified CosA repo copy, it complains that it cannot access the symbol counter_2.out when trying the task [counter_2_reaches_1]:

❯ CoSA master* ⇣ CoSA --problems examples/counters/problem_verilog.txt            
/usr/local/lib/python3.8/site-packages/pysmt/walkers/generic.py:43: DeprecationWarning: Using or importing the ABCs from 'collections' instead of from 'collections.abc' is deprecated since Python 3.3, and in 3.9 it will stop working
  if len(nodetypes) == 1 and isinstance(nodetypes[0], collections.Iterable):
Parsing file "examples/counters/counters.v"... DONE
Parsing file "examples/counters/toggle-clk1.ssts"... DONE
Solving "counter_out_0" .. TRUE
Solving "counter_2_reaches_1_0" Traceback (most recent call last):
  File "/Users/mdko/CoSA/cosa/analyzers/dispatcher.py", line 651, in convert_formula
    with pdef_file.open() as f:
  File "/usr/local/Cellar/python@3.8/3.8.5/Frameworks/Python.framework/Versions/3.8/lib/python3.8/pathlib.py", line 1218, in open
    return io.open(self, mode, buffering, encoding, errors, newline,
  File "/usr/local/Cellar/python@3.8/3.8.5/Frameworks/Python.framework/Versions/3.8/lib/python3.8/pathlib.py", line 1074, in _opener
    return self._accessor.open(self, flags, mode)
FileNotFoundError: [Errno 2] No such file or directory: 'examples/counters/F(counter_2.out = 1_8)'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/lib/python3.8/site-packages/pysmt/formula.py", line 119, in get_symbol
    return self.symbols[name]
KeyError: 'counter_2.out'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/bin/CoSA", line 11, in <module>
    load_entry_point('CoSA', 'console_scripts', 'CoSA')()
  File "/Users/mdko/CoSA/cosa/shell.py", line 210, in main
    sys.exit(run_problems(problems_config))
  File "/Users/mdko/CoSA/cosa/shell.py", line 166, in run_problems
    psol.solve_problems(problems_config)
  File "/Users/mdko/CoSA/cosa/analyzers/dispatcher.py", line 516, in solve_problems
    prop = self.convert_formula(problem.properties,
  File "/Users/mdko/CoSA/cosa/analyzers/dispatcher.py", line 657, in convert_formula
    converted_tuples = parser.parse_formulae([p.strip() for p in formula.split(MODEL_SP)])
  File "/Users/mdko/CoSA/cosa/encoders/ltl.py", line 304, in parse_formulae
    formula = self.parse_formula(strform)
  File "/Users/mdko/CoSA/cosa/encoders/ltl.py", line 294, in parse_formula
    return self.parse_string(quote_names(strformula))
  File "/Users/mdko/CoSA/cosa/encoders/ltl.py", line 286, in parse_string
    return PrattParser(ExtLexer).parse(string)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 486, in parse
    result = self.expression()
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 469, in expression
    left = t.nud(self)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 529, in nud
    right = parser.expression(self.lbp)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 468, in expression
    self.token = next(self.tokenizer)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 74, in tokenize
    yield symbol(capture)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 222, in identifier
    return Identifier(read, env=self.env)
  File "/usr/local/lib/python3.8/site-packages/pysmt/parsing.py", line 326, in __init__
    self.value = env.formula_manager.get_symbol(name)
  File "/usr/local/lib/python3.8/site-packages/pysmt/formula.py", line 121, in get_symbol
    raise UndefinedSymbolError(name)
pysmt.exceptions.UndefinedSymbolError: 'counter_2.out' is not defined!

Do I need to add an output to the top-level Verilog module for each signal I wish to check, or is accessing the internal wires of Verilog modules supported like in CoreIR .json files?

Thanks!

cristian-mattarei / CoSA

Unable to access symbols defined within Verilog modules #128