Check out our latest paper. AutoCC: a methodology that leverages FPV to automatically discover covert channels in hardware that is time-shared between processes. AutoCC operates at RTL to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. The AutoCC github contains the artifacts of the papers and the flow generation methodology, based on AutoSVA, enjoy!
AutoSVA was build with the goal of making Formal Property Verification (FPV) more accesible for hardware designers. AutoSVA brings a simple language to make annotations in the signal declaration section of a module interface. This enables our to generate Formal Testbenches (FT) that check that transactions between hardware RTL modules follow their interface especifications. It does not check full correctness of the design but it automatically generate liveness properties (prevent duplicated responses, prevent requests being dropped) and some safety-relate properties of transactions, like data integrity, transaction invariants, uniqueness, stability... To understand this more fully you can read the paper. AutoSVA is publised at the 58th ACM/IEEE Design Automation Conference (DAC'21) December 2021.
This 3 minute video summarizes the AutoSVA approach
To cite our paper, please use:
@inproceedings{orenes2021autosva,
title={AutoSVA: Democratizing Formal Verification of RTL Module Interactions},
author={Orenes-Vera, Marcelo and Manocha, Aninda and Wentzlaff, David and Martonosi, Margaret},
booktitle={2021 58th ACM/IEEE Design Automation Conference (DAC)},
pages={535--540},
year={2021},
organization={IEEE}
}
The AutoSVA tool is based on a Python script, which takes the next arguments
Required argument
-f FILENAME, --filename FILENAME
Path to DUT RTL module file.
Optional arguments
-h, --help show this help message and exit
-src SOURCE [SOURCE ...], --source SOURCE [SOURCE ...]
Path to source code folder where submodules are.
-i INCLUDE, --include INCLUDE
Path to include folder that DUT and submodules use.
-as SUBMODULE_ASSERT [SUBMODULE_ASSERT ...], --submodule_assert SUBMODULE_ASSERT [SUBMODULE_ASSERT ...]
List of submodules for which ASSERT the behavior of
outgoing transactions.
-am SUBMODULE_ASSUME [SUBMODULE_ASSUME ...], --submodule_assume SUBMODULE_ASSUME [SUBMODULE_ASSUME ...]
List of submodules for which ASSUME the behavior of
outgoing transactions (ASSUME can constrain the DUT).
-x [XPROP_MACRO], --xprop_macro [XPROP_MACRO]
Generate X Propagation assertions, specify argument to
create property under <MACRO> (default none)
-tool [TOOL] Backend tool to use [jasper|sby] (default sby)
For example:
python autosva.py -f <DUT_PATH/DUT_NAME.v> -v -src <SRC_PATH> -i <INCLUDE_PATH>
You can set the flag -v to generate the verbose output and see the parsing process
Once the FT is generated, you can run the FT on SBY like this:
./run.sh <DUT_NAME>
SVA files at the Formal Testbench (FT) are auto-generated every time you execute autosva_py on a DUT_NAME, but manual commands can be added manually to ft_<DUT_NAME>/FPV.sby, for example, to solve the next cases:
A. When SBY is elaborating the project, if it complains about any RTL submodule or include not being found, add its path manually (more info at SymbiYosys ReadTheDocs)
B. Alternatively, you can add blackbox for those submodule if you want to blackbox them
C. If the RTL needs some defines to be set, do so also by appending "read -define =1" after "read -verific"
- Python version 2 or superior
- A formal tool backend (two tools options are currently supported, you only need one)
- SymbiYosys (SBY) with Verific, e.g. provided by Tabby CAD at www.yosyshq.com (to run with -tool sby)
- JasperGold version >= 2015.12 (to run with -tool jg)
# Clone the Ariane repository with the annotations to the modules
git clone https://github.com/morenes/cva6.git ariane
cd ariane
git checkout autosva
git submodule update --init --recursive --force src
cd ..
# Set DUT_ROOT and AUTOSVA_ROOT env variable
export DUT_ROOT=$PWD/ariane
export AUTOSVA_ROOT=$PWD
# Enter AutoSVA folder and run scripts to update relative Formal Testbenches (FT)
cd autosva
./setup_ariane.sh
./run.sh mmu # lsu_lookup_transid_was_a_request shows the ghost response bug
In the 14 minute Youtube tutorial we create a Formal Property Verification (FPV) testbench for a FIFO queue. We show step by step how to generate it by adding 3 lines of code of annotations and simply pressing the play button. Our transaction abstraction is applicable to many more modules, and out explicit annotations provide flexibility of names and interface styles, e.g. we support annotating when interfaces use structs, or when transactions do not seem obvious at first.
export DUT_ROOT=$PWD/quickstart
export AUTOSVA_ROOT=$PWD
Then we added the following annotations to the fifo.v inside the quickstart folder
/*AUTOSVA
fifo: in -IN> out
[INFLIGHT_IDX-1:0] in_transid = fifo.buffer_head_reg
[INFLIGHT_IDX-1:0] out_transid = fifo.buffer_tail_reg
*/
Then we run the autosva tool, what will generate the formal testbench called 'ft_fifo':
python autosva.py -f fifo.v -x XPROP -tool sby #For SymbiYosys
python autosva.py -f fifo.v -x XPROP -tool jasper #For JasperGold
(To target JasperGold, use -tool jasper instead of -tool sby)
Then we run the formal property verification tool. We use the run script to run the fifo FT
source run_sby.sh fifo #For SymbiYosys
source run_jg.sh fifo #For JasperGold
To watch the waveforms of a Counterexample (CEX) in SBY we use
gtkwave ft_fifo/FPV_prv/engine_0/trace.vcd &