General Flow
We assume that a digital design is complex enough to have the following
- Workload that can be simulated is significantly smaller than the workload that can be emulated. That is to say that Simulation « Emulation. They are equivalent logically though. We can call this realm Runtime
- It is very hard to constrain Formal to be the same as Runtime. It is also better to be under-constrained than be over-constrained. So we start of with no constrains. This naturally leads to invalid CEX.
These are our assumptions. We don’t really care about the specific miner, simulator or the FPGA environment used. A microprocessor is just an example of such complex design. But it is not specific to that.
Periscope suggests a workflow that uses the best parts from these three environments. More importantly it attempts to alleviate the gaps with a feedback mechanism.
The basic version of this feedback mechanism is the cardinality of the categories.
A high number of
- Cat 1 implies FV-RV are in sync
- Cat 2 implies Simulated Workload and Emulated Workload are out of sync
- Cat 3 implies FV-RV are out of sync
- Cat 4 implies hardware or setup issues
Just by seeing this, improvements can be made by adjusting the workloads.
Another mechanism is the Assumption grid. This allows to close the FV-RV gap by converting reasonable assertions into assumptions.
Section 4 could be general and can be seen as a way to improve Runtime workload
This also plays into why just having a miner is not enough