diff options
Diffstat (limited to 'scripts/smt2-bmc/README')
-rw-r--r-- | scripts/smt2-bmc/README | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/scripts/smt2-bmc/README b/scripts/smt2-bmc/README new file mode 100644 index 0000000..f947664 --- /dev/null +++ b/scripts/smt2-bmc/README @@ -0,0 +1,47 @@ + +Checking equivalence of different configurations of PicoRV32 using Yosys and +SMT solvers (Yices, Z3, CVC4, MathSAT). + +The PicoRV32 core provides configuration parameters that change the supported +ISA and/or the timing of the core. This set of scripts uses model checking +techniques to proof equivalence of cores in different configurations, thus +transfering the confidence in the cores gained by running test benches on a few +configurations to the rest of the configurations. + + +async +----- + +The async test compares two cores with different timings (number of clock +cycles per operation), but same ISA. The SMT problem models the following +scenario: + +The cores start out with identical memory and register file. In cycle 0 the +reset input is active, in all other cycles the reset input is inactive. The +trap output must by active in the last cycle for both cores. I.e. whatever +the program in memory does, it must terminate in a trap and it must do so +for both cores within the simulated number of clock cycles. + +The script searches for a trace that ends in different memory content and/or +different register file content in the last cycle, i.e. a trace that exposes +divergent behavior in the two cores. + + +sync +---- + +The sync test compares two cores same timings but different ISA. The ISA of the +2nd code (main_b) must be a superset of the ISA of the first core (main_a), and +catching illegal instructions and illegal memory transfers must be enabled in +the first core. The SMT problem models the following scenario: + +The cores start out with identical memory and register file. In cycle 0 the +reset input is active, in all other cycles the reset input is inactive. The +cores are run in parallel for a number of cycles with the first core not going +into the trap state. I.e. all traces are limited to the ISA supported by the +first core. + +The script searches for a trace that ends in different memory content and/or +different register file content in the last cycle, i.e. a trace that exposes +divergent behavior in the two cores. + |