[formal] Remove build infrastructure for data independent timing

This commit is contained in:
Marno van der Maas 2022-10-04 10:18:55 +01:00 committed by Marno van der Maas
parent fce41ff4d3
commit ab350c4604
3 changed files with 4 additions and 60 deletions

View file

@ -1,37 +0,0 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
# A simple wrapper around fusesoc to make it a bit easier to run the formal flow
core-name := lowrisc:fpv:ibex_data_ind_timing
vlnv := $(subst :,_,$(core-name))
build-root := $(abspath ../../build/$(vlnv))
# Since we have a hacky hook that runs sv2v in place on fusesoc's
# copied source files, we have to generate different build roots for
# the two flavours (otherwise bad things will happen if you run make
# -j2)
mk-build-root = $(abspath ../../build/$(vlnv)/$(1))
mk-fusesoc-cmd = \
fusesoc --cores-root=../.. \
run --build-root=$(call mk-build-root,$(1)) \
--target=$(1) \
$(core-name) $(fusesoc-params)
.PHONY: all slow fast single
all: slow fast single
operations := mull mulh div rem
slow_tgts := $(addprefix slow_, $(operations))
fast_tgts := $(addprefix fast_, $(operations))
single_tgts := $(addprefix single_, $(operations))
all_tgts := $(slow_tgts) $(fast_tgts) $(single_tgts)
slow: $(slow_tgts)
fast: $(fast_tgts)
single: $(single_tgts)
$(all_tgts):
$(call mk-fusesoc-cmd,$@)

View file

@ -0,0 +1,4 @@
# Data Independent Timing Assertions
We currently do not have a way to run these SystemVerilog assertions.
However, we keep these files because they will be useful for future work.

View file

@ -1,23 +0,0 @@
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
[tasks]
slow sl
fast fs
single si
[options]
mode bmc
depth 50
[engines]
smtbmc boolector
[script]
{{"-sv"|gen_reads}}
prep -top {{top_level}}
[files]
{{files}}