Skip to content

Commit

Permalink
Update boolector install (#13)
Browse files Browse the repository at this point in the history
  • Loading branch information
dopamane authored Oct 10, 2023
1 parent f6aae55 commit 105dffb
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 5 deletions.
10 changes: 6 additions & 4 deletions .github/workflows/haskell.yml
Original file line number Diff line number Diff line change
Expand Up @@ -29,13 +29,15 @@ jobs:

- name: Free up environment resources
run: |
df -h
sudo rm -rf /usr/share/dotnet
sudo rm -rf /opt/ghc
sudo rm -rf /usr/local/share/boost
sudo rm -rf "$AGENT_TOOLSDIRECTORY"
df -h
- name: Set up GHC ${{ matrix.ghc-version }}
uses: haskell/actions/setup@v2
uses: haskell-actions/setup@v2
id: setup
with:
ghc-version: ${{ matrix.ghc-version }}
Expand Down Expand Up @@ -63,7 +65,7 @@ jobs:
cabal configure --enable-tests --enable-benchmarks --disable-documentation
cabal build --dry-run
- name: Restore cached dependencies
- name: Restore Haskell cached dependencies
uses: actions/cache/restore@v3
id: cache
env:
Expand Down Expand Up @@ -175,12 +177,12 @@ jobs:
- name: Install boolector
working-directory: boolector
run: |
./contrib/setup-btor2tools.sh
./contrib/setup-lingeling.sh
./contrib/setup-btor2tools.sh
./configure.sh
make -C build -j$(nproc)
sudo cp build/bin/{boolector,btor*} /usr/local/bin
sudo cp deps/btor2tools/bin/btorsim /usr/local/bin
sudo cp deps/btor2tools/build/bin/btorsim /usr/local/bin
- name: Checkout riscv-gnu-toolchain
uses: actions/checkout@v3
Expand Down
7 changes: 6 additions & 1 deletion lion-formal/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,12 @@ At minimum to run Lion formal verification using [riscv-formal](https://github.c
> See [here](https://symbiyosys.readthedocs.io/en/latest/install.html)
> for intall instructions.
If you want to inspect counter example traces or disassemble the code in the counter example traces see the [ricsv-formal prerequisites](https://github.com/standardsemiconductor/riscv-formal/blob/lion/docs/quickstart.md#prerequisites).
The [nightly pipeline](https://github.com/standardsemiconductor/lion/blob/main/.github/workflows/haskell.yml)
also has up-to-date steps to install Yosys, SymbiYosys,
and Boolector.

If you want to inspect counter example traces or disassemble the code in the
counter example traces see the [ricsv-formal prerequisites](https://github.com/standardsemiconductor/riscv-formal/blob/lion/docs/quickstart.md#prerequisites).

## Usage
Build: `cabal build`
Expand Down

0 comments on commit 105dffb

Please sign in to comment.