Averroes (avr) -- Abstract VERification of Reachability Of Electronic Systems
 	version 2.0
	Reads a Verilog file and performs property checking with data abstraction.
		supports SystemVerilog concurrent assertions

	Copyright (C) 2019  Aman Goel <amangoel@umich.edu> and Karem A. Sakallah <karem@umich.edu>, University of Michigan
	
	------------
	Dependencies
	------------
	1. Yosys    (Copyright (C) 2019 Clifford Wolf <clifford@clifford.at>)
	2. Yices 2  (Copyright (C) 2019 SRI International)
	3. Z3       (Copyright (c) 2019 Microsoft Corporation)
	4. MathSAT5 (Copyright (c) 2019 Fondazione Bruno Kessler, Italy)

	---------------------------------
	Limitiations (as of Feb 11, 2019)
	---------------------------------
	1. Can only handle safety properties that can be expressed without temporal operators.
	2. Handles asynchronous flops as synchronous.
	3. Handles memory using memory abstraction (experimental).
	4. avr uses yosys as its frontend and can handle most designs/formats that are supported by yosys.
		(customize the bin/avr for special preprocessing using Yosys)
	5. Support for .vmt frontend is limited.

	Please report bugs via email (amangoel@umich.edu) or on github (https://github.com/aman-goel/avr)

--> How to build
	avr requires yosys, yices2, z3, libgmp-dev
	a) Use build.sh to install yosys
	b) yices2, z3, MathSAT5 and libgmp-dev are statically linked to binaries in bin/ folder

--> How to run
	python avr.py <path>/<top-module-file>
		(use python avr.py -h for command-line options)
		
--> Examples
	“examples” directory contains several different test cases
		(use <test-name>/<test-name>.fconfig to identify top-module-file)

--> Output
	avr creates a directory <output-path>/work_<test-name> which contains detailed files relating to the run
		(<output-path> and <test-name> can be customized using command-line options in avr.py)

	work_<test-name> contains several files that provides details for the run:
	work_<test-name>
	├── inv.txt							// invariant file with axioms (when property is true)
	├── cex.txt							// counterexample file (when property is false)
	├── <test-name>.results				// detailed statistics report
	├── <test-name>.ilang				// .ilang file generated from yosys
	├── <test-name>_y.v					// verilog file (equivalent to .ilang)
	├── fconfig							// configuration file
	├── avr.err							// stderr report
	├── dot								// folder to visualize system
	├── data/reach.output				// detailed log of reachability analysis
	├── data/parse_original.results		// original system information
	├── data/parse.results				// system information (on which property checking is performed)
	├── data/design_original.txt		// original system given
	├── data/design.txt					// processed system
	├── data/refs.txt					// detailed log of refinement axioms learnt
	├── data/vwn.output					// output from stage 1 of frontend
	├── data/dpa.output					// output from stage 2 of frontend
	├── data/wn.dump					// internal system dump after stage 1 of frontend
	├── data/wn_orig.dump				// internal system dump after stage 2 of frontend
	└── yosys.log						// yosys log

	As a quick summary relating to the run, avr produces certain key information on stderr.
	For example, running python avr.py examples/cav14_example/cav14_example.v produces the following on stderr.

	3	: 0	: 0 s: 0                  
	3	: 1	: 0 1 s: 1                  
	3	: 1	: 0 0 1 s: 1                  
      Result        Time        Mem.       #Refs           
                     sec          MB                       
           h        0.01          13           3
    ":" separated numbers indicate the following:
		<# of refinements learnt> : <max frame> : <# of added clauses in each frame> s: <total # of clauses learnt>
	Result can be mapped as follows:
		h	-> Property holds				(inv.txt contains inductive invariant)
		v	-> Property violated 				(reach.output contains a set of counterexamples)
		f_*	-> Error / time or memory limit exceeded	(check reach.output for possible more information)

--> Notes
    a) avr is still in development phase and uses several parameters internally for efficient property checking.
       Many such parameters can be tuned/corrected, including frontend support via Yosys.
    b) "property" is a reserved keyword.
    c) Property description is expected to be present in the top module, and not in submodules.
    d) Multiple properties are allowed. One can select a single property by using option --property <prop-name> in the API.
       The option tries finding a signal named *<prop-name> in the design as property and discards all other assertions (if a match is found).
    e) There is also limited support for SystemVerilog concurrent assumptions using assume property ( .. ).
    f) Use the dot folder to explore visualizations for the transition system.
    g) Initial state conditions collected by avr are listed in parse.results file.
    h) Currently counterexample (for a violating property) is not presented in a standard format.
    i) After proving a property, avr performs a series of checks to ensure correctness of the result (for the interpreted system).
    j) If Averroes produces an output saying poor abstraction, this can be (sometimes) handled using a new technique (use option --abstract sa).
    k) avr performs best especially for control-centric properties and is almost independent of the bit-width of words in the system.
    l) Memory abstraction technique is still in development phase.
    m) Use option --effort_mininv to minimize inductive invariant (in the case property is true).
       0 (no minimization), 1 (abstract fast), 2 (abstract slow), 3 (concrete fast), 4 (concrete slow).
    n) Use --vmt to read in a .vmt file (instead of yosys frontend).
       supported theories: quantifier-free bit-vectors, linear integer arithmetic and arrays.
    o) Use --abstract to enable/disable data abstraction.
	   sa (no data abstraction, QF_BV), sa+uf (data abstraction, QF_UF)
    p) Use --granularity to configure abstract granularity level
       0 (lowest), 1 (also allow BV equaltity), 2 (also allow INT equaltity), 3 (also allow mixed), 4 (also allow input).


We would be glad to hear from you and help you in case you are having a difficulty in using Averroes.
Please contact Aman Goel (amangoel@umich.edu) for help/suggestions/modifications or just to share your comments on Averroes!