kepler-formal/examples/xilinx at main · keplertech/kepler-formal · GitHub

//files/disambiguate" data-turbo-transient="true" />

Skip to content

Type / to search

Sign in<br>Sign upAppearance settings

You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

{{ message }}

Uh oh!

There was an error while loading. Please reload this page.

keplertech

kepler-formal

Public

Notifications<br>You must be signed in to change notification settings

Fork<br>13

Star<br>94

FilesExpand file tree

main

/xilinx<br>Copy path

Directory actions

More options<br>More options

Directory actions

More options<br>More options

Latest commit

History<br>History<br>History

main

/xilinx<br>Copy path

Top

Folders and files<br>NameNameLast commit message<br>Last commit date<br>parent directory<br>..<br>register_slice

register_slice

vexriscv

vexriscv

README.md

README.md

xilinx.py

xilinx.py

View all files

README.md

Xilinx Examples

The Xilinx examples use the shared xilinx.py formal primitive<br>models through the YAML py_tech_files option.

Directory<br>Contents

register_slice<br>Small mapped-versus-compact SEC equivalence example.

vexriscv<br>Large VexRiscv GenFull LEC self-check and intentional-difference examples.

xilinx.py models the combinational, parameterized LUT, sequential, carry,<br>DSP, distributed RAM, and block RAM primitives used by these netlists.

You can’t perform that action at this time.