mirror of
https://github.com/annoyatron255/yosys4gal.git
synced 2024-12-22 10:42:24 +00:00
26 lines
982 B
Markdown
26 lines
982 B
Markdown
Model-Based Verification Checking
|
|
=================================
|
|
|
|
To assist with verification checking, _yosys4gal_ includes Verilog models of
|
|
the supported GAL16V8 and GAL22V10 chips. These Verilog read in the
|
|
tool-generated fuse map and the behavior should match that of the original
|
|
Verilog. The provided script performs this check using yosys' SAT solver:
|
|
```
|
|
./prove_equiv.tcl -- <JEDEC FILE> <PCF CONSTRAINTS> <VERILOG FILES...>
|
|
```
|
|
|
|
Limitations
|
|
-----------
|
|
The models only support the functionality of the GAL chips which is supported
|
|
in _yosys4gal_. I.e. the GAL16V8 model only supports registered mode and the
|
|
GAL22V10 model doesn't support asynchronous set/reset. Also note that a failure
|
|
to prove equivalence does not imply inequivalence. In particular, yosys can
|
|
struggle to synthesize the GAL22V10 model correctly. The false positive rate,
|
|
however, should be zero.
|
|
|
|
Dependencies
|
|
------------
|
|
- `yosys` 0.38 or higher
|
|
- `jedutil` from MAME utilities
|
|
- `xxd` from Vim
|