diff options
| author | Kevin Laeufer | 2020-08-14 18:39:42 -0700 |
|---|---|---|
| committer | GitHub | 2020-08-15 01:39:42 +0000 |
| commit | 2e5f942d25d7afab79ee1263c5d6833cad9d743d (patch) | |
| tree | add86d0b4b090807b48bb2307d10f2b7b38e0bce /.install_z3.sh | |
| parent | 1b48fe5f5e94bdfdef700956e45d478b5706f25e (diff) | |
experimental SMTLib and btor2 emitter (#1826)
This adds an experimental new SMTLib and Btor2 emitter
that converts a firrtl module into a format
suitable for open source model checkers.
The format generally follows the behavior of yosys'
write_smt2 and write_btor commands.
To generate btor2 for the module in m.fir run
> ./utils/bin/firrtl -i m.fir -E experimental-btor2
for SMT:
> ./utils/bin/firrtl -i m.fir -E experimental-smt2
If you have a design with multiple clocks
or an asynchronous reset, try out the new StutteringClockTransform.
You can designate any input of type Clock to be your
global simulation clock using the new GlobalClockAnnotation.
If your toplevel module instantiates submodules,
you need to inline them if you want the submodule
logic to be included in the formal model.
Diffstat (limited to '.install_z3.sh')
| -rw-r--r-- | .install_z3.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/.install_z3.sh b/.install_z3.sh new file mode 100644 index 00000000..13ffb90e --- /dev/null +++ b/.install_z3.sh @@ -0,0 +1,9 @@ +set -e +# Install Z3 (https://github.com/Z3Prover/z3) +if [ ! -f $INSTALL_DIR/bin/z3 ]; then + mkdir -p $INSTALL_DIR + # download prebuilt binary + wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip + unzip z3-4.8.8-x64-ubuntu-16.04.zip + mv ./z3-4.8.8-x64-ubuntu-16.04/bin/z3 $INSTALL_DIR/bin/z3 +fi |