cristian-mattarei/cosa

CoreIR Symbolic Analyzer

cosa's Issues

Brainstorm architecture for keeping CoreIR representation internally

Parsing errors don’t give line numbers

Just a reminder for me to address this when there’s time. It would be nice if parsing errors gave a line number. Especially for STS/ETS files. This might be harder for problem/property/assumption files.

Getting next value of array then accessing is wrong

next(arr)[addr] should be equivalent to (next(arr))[addr] but it’s not

AttributeError: '_BVType' object has no attribute 'get_type'

Hi

I encountered an error when using the latest CoSA (both the master branch on github and the latest from pip3 seems to produce the same error message).

Here is the error message (on the AXI example):

~/case-studies/axi$ CoSA --problems problem.txt
Parsing file "axi.vlist"... Reading source files from "axi.vlist"... Traceback (most recent call last):
  File "/home/hongce/cosaEnv/bin/CoSA", line 11, in <module>
    sys.exit(main())
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/shell.py", line 209, in main
    sys.exit(run_problems(problems_config))
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/shell.py", line 165, in run_problems
    psol.solve_problems(problems_config)
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/analyzers/dispatcher.py", line 364, in solve_problems
    modifier)
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/analyzers/dispatcher.py", line 315, in parse_model
    (hts_a, inv_a, ltl_a) = parser.parse_file(filepath, general_config, flags)
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/encoders/verilog_yosys.py", line 162, in parse_file
    ret = parser.parse_file(TMPFILE, config)
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/encoders/btor2.py", line 100, in parse_file
    return self.parse_string(f.read())
  File "/home/hongce/cosaEnv/lib/python3.6/site-packages/cosa/encoders/btor2.py", line 230, in parse_string
    output_symbol = Symbol(nids[1], original_symbol.get_type())
AttributeError: '_BVType' object has no attribute 'get_type'

I have CoSA installed in the virtual environment and the installed packages are:

bit-vector (0.39a0)
coreir (2.0.19)
CoSA (0.4)
Cython (0.29.2)
gmpy2 (2.0.8)
hwtypes (1.0.13)
Jinja2 (2.10)
MarkupSafe (1.0)
numpy (1.15.3)
pip (9.0.1)
pkg-resources (0.0.0)
pyparsing (2.4.0)
PySMT (0.8.0)
pyverilog (1.1.2)
setuptools (39.0.1)
six (1.12.0)
wheel (0.32.2)
z3-solver (4.8.5.0)

I have Python 3.6.8 on Ubuntu 18.04

Please don't hesitate to tell me if there is any additional information that I can provide.

[btor2] Initialize array with scalar constant

The btor2 format allows initializing arrays with scalar constants:

initializing a memory with a bit-vector constant zero, zero-initializes the whole memory
(src: https://link.springer.com/content/pdf/10.1007%2F978-3-319-96145-3_32.pdf)

CoSA fails to translate this simplified example (which works fine with btormc):

15 sort bitvec 2
26 sort bitvec 9
63 sort array 26 15
64 const 15 00
65 state 63 memory
66 init 63 65 64

The error message is:

pysmt.exceptions.PysmtTypeError: The formula '(memory = 0_2)' is not well-formed

A question about CoSa and Pono workflow

For the current workflow in CoSa and Pono - is it possible to load the BTOR2 file with the Verilog model with no assertions and add "assertions" trough Python API?

If it's possible and stable - will you advise Pono or CoSa for that?

The goal is to formally check the Verilog modules in a more flexible way than open-source Yosys supports currently (with Python probably).

Consider using -expose instead of -anyseq in Yosys setundef pass

Using the Yosys pass: setundef -undriven -anyseq can create unnecessary state elements in the generated btor. It might be better to use -expose which instead ties these undriven wires to inputs. This needs to be investigated further.

Brainstorm architecture for a new CoSA API

Suggestion: Raw String for Regular Expression

Hi Makai,

On my machine (Ubuntu 18.04 Python 3.6.7), using escape generates warning like these:

 /home/hongce/CoSA/cosa/encoders/verilog_hts.py:189: DeprecationWarning: invalid escape sequence \w
  orig_lineno = re.search("/\w.*\(\d+\)", line)

CoSA/cosa/encoders/verilog_hts.py

Line 189 in e280d00

orig_lineno = re.search("/\w.*\(\d+\)", line)

I have a suggestion to change it to raw string to get rid of these warnings.

  orig_lineno = re.search(r"/\w.*\(\d+\)", line)

Semi-colons in STS can't be next to bit-vector constants

Just a reminder for me to fix this. The issue is likely in the quote_names function here:

CoSA/cosa/utils/formula_mngm.py

Line 131 in 4272108

def quote_names(strformula, prefix=None, replace_ops=True):

It needs to recognize bit-vector constants even if there's a semicolon next to it.

Feature Idea: Synchronize clocks

It might be nice to have an option to automatically synchronize and abstract clocks.

For the yosys/btor frontend, this would just mean adding the async2sync pass. For other frontends (e.g. coreir) this would just call add-clock and abstract_clock.

We should support add-clock for btor input too, just need to search inputs for clock or clk.

Out of date with bit vector

Bit vector no longer has an unsigned_value member. It is being used here:

CoSA/cosa/encoders/coreir.py

Line 377 in bbab8a3

xval = xval.unsigned_value

The problem about installing CoSA.

Hi Mattarei,

When I try to install CoSA according to your instructions, some errors about collecting corei are appeared.

The error reports are shown as follows:

Collecting coreir
Downloading https://files.pythonhosted.org/packages/88/c5/299886ff6938f26cea7ffa64b7e2c9c607c4ca96018df3de2645531d4668/coreir-2.0.61.tar.gz
ERROR: Command errored out with exit status 1:
command: /System/Library/Frameworks/Python.framework/Versions/2.7/Resources/Python.app/Contents/MacOS/Python -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/private/tmp/pip-install-fV7cqe/coreir/setup.py'"'"'; file='"'"'/private/tmp/pip-install-fV7cqe/coreir/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(file);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, file, '"'"'exec'"'"'))' egg_info --egg-base /private/tmp/pip-install-fV7cqe/coreir/pip-egg-info
cwd: /private/tmp/pip-install-fV7cqe/coreir/
Complete output (9 lines):
[proxychains] DLL init: proxychains-ng 4.14
[proxychains] DLL init: proxychains-ng 4.14
[proxychains] DLL init: proxychains-ng 4.14
Traceback (most recent call last):
File "", line 1, in
File "/private/tmp/pip-install-fV7cqe/coreir/setup.py", line 92
subprocess.check_call(["make", "-C", build_dir, f"-j{njobs}",
^
SyntaxError: invalid syntax
----------------------------------------
ERROR: Command errored out with exit status 1: python setup.py egg_info Check the logs for full command output.

How can I solve the problem?
Thanks a lot.

Yosys Verilog Frontend Might Blast Memories to Registers

Sometimes the yosys frontend will elect to turn memories into a sequence of registers. Additionally, it might fail for latches.

Suggested fixes:

• always read the verilog with the -nolatches switch
• when no_arrays=False (the default), run with -nomem2reg and memory -nomap

It might be worth it to always use read instead of read_verilog or verific as well.

Signed arithmetic not handled in internal parser

This also causes a bug in for loops with the condition (i >= 0) because everything defaults to unsigned comparisons.

cosa distributed with older version of bit_vector

I was looking at https://pypi.org/project/CoSA/#files, and if I download CoSA-0.2.4.tar.gz and look in the archive, I see:

❯ ls
CoSA.egg-info PKG-INFO      README.rst    bit_vector    cosa          setup.cfg     setup.py

It looks like cosa is being distributed with an older version of the bit_vector package.

This breaks compatibility with repos like https://github.com/StanfordAHA/garnet, where we use both cosa and bit_vector, but are expecting a newer version of bit_vector. Any chance we could get cosa upgraded to a newer version?

Alternatively, can CoSA rename the older bit_vector it's packaged with to something else? E.g. cosa_bit_vector, this would at least avoid the name conflict. This is probably the quicker work around to unblock our issue.

CoSA2?

Is there any way to get hold of a copy of the award-winning CoSA2?

I am currently working on a tool that emits bounded model checking problems in BTOR2 and SMT2 format. There are some problems where yices (+SMT2 encoding) does a lot better than btormc on the BTOR2 encoding.
It would be great if I had another fast model checker to compare with.

Possible regression in latest CoSA release (0.2.1)

Here are the necessary files
conf_sub.ets.txt
pe.json.txt
problem_pe_sub.txt

Command

CoSA --problem problem_pe_sub.txt

Output

** Problem PE check sub configuration **
Description: "Check configuring to opcode=1 results in read_data=1"
Result: FALSE
Expected: TRUE
FALSE != TRUE <<<---------| ERROR
Counterexample:
---> INIT <---
  I: conf_done = 0_1
  I: self.I0 = 22_16
  I: self.I1 = 20_16
  I: self.O = 42_16
  I: self.clk = 0_1
  I: self.config_addr = 0_1
  I: self.config_data = 0_2
  I: self.config_en = 0_1
  I: self.read_data = 0_2
  I: self.reset = 0_1

---> STATE 1 <---
  S1: self.I0 = 18_16
  S1: self.I1 = 17_16
  S1: self.O = 35_16

---> STATE 2 <---
  S2: self.I0 = 15_16
  S2: self.I1 = 13_16
  S2: self.O = 28_16
  S2: self.reset = 1_1

---> STATE 3 <---
  S3: self.I0 = 11_16
  S3: self.I1 = 10_16
  S3: self.O = 21_16
  S3: self.reset = 0_1

---> STATE 4 <---
  S4: self.I0 = 8_16
  S4: self.I1 = 6_16
  S4: self.O = 14_16
  S4: self.clk = 1_1
  S4: self.config_data = 1_2
  S4: self.config_en = 1_1

---> STATE 5 <---
  S5: self.I0 = 4_16
  S5: self.I1 = 3_16
  S5: self.O = 7_16

---> STATE 6 <---
  S6: conf_done = 1_1
  S6: self.I0 = 1_16
  S6: self.I1 = 0_16
  S6: self.O = 1_16
  S6: self.clk = 0_1
  S6: self.config_data = 0_2
  S6: self.config_en = 0_1

This check used to pass on version 0.2.0. Let me know if this is actually an issue in the problem description rather than the checker.

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/[email protected]/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/[email protected]/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!

Enhancement Idea: Use Yosys through Python API

Yosys now has a Python API using boost_python. Enable it with:
sudo make install ENABLE_PYOSYS=1 ENABLE_LIBYOSYS=1

We can use this to encode the Verilog directly from RTLIL instead of going through the BTOR format. This would give us much better control over the design and even allow us to dynamically run passes based on the contents of the design.