colin
/
Hazard3
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Hazard3/test/formal/bus_compliance_2port/Makefile

14 lines
176 B
Makefile
Raw Normal View History

Do not rely on environment variables for any intra-project paths It's no longer necessary to source `sourceme` before running any of the project Makefiles.
2024-05-27 23:52:54 +08:00
include ../project_paths.mk
Add simple formal bus properties check
2021-05-30 17:19:42 +08:00
DOTF=tb.f
TOP=tb
Add single-port bus compliance. Fix adapter not re-arbitrating following an ERROR response, causing a squashed younger load-store to remain presented to the bus.
2021-12-18 23:41:05 +08:00
YOSYS_SMT_SOLVER=z3
Fix bug where an IRQ can fire during load/store dphase, followed by dphase bus exception. Result was that the exception would sample the IRQ vector PC rather than the load/store instruction PC. Fix by fencing off on in-flight dphases before asserting the IRQ. This adds a cycle of jitter to IRQs, but is required for correct operation without adding a full exception-gathering pipeline.
2021-12-08 03:24:53 +08:00
DEPTH=25
Add separate define HAZARD3_ASSERTIONS for enabling internal assertions, and enable it only on the bus compliance model checks. Trying to make the solver's life easier in instruction_fetch_match.
2022-06-26 03:08:35 +08:00
# Also check internal properties
DEFINES=HAZARD3_ASSERTIONS
Fix bug where an IRQ can fire during load/store dphase, followed by dphase bus exception. Result was that the exception would sample the IRQ vector PC rather than the load/store instruction PC. Fix by fencing off on in-flight dphases before asserting the IRQ. This adds a cycle of jitter to IRQs, but is required for correct operation without adding a full exception-gathering pipeline.
2021-12-08 03:24:53 +08:00
all: bmc
Add simple formal bus properties check
2021-05-30 17:19:42 +08:00
include $(SCRIPTS)/formal.mk