Skip to content

example

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

example

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
tinyrocket_naja.if
tinyrocket_naja.if
 
 
tinyrocket_naja_edited.if
tinyrocket_naja_edited.if
 
 
BUILD.bazel
BUILD.bazel
 
 
NangateOpenCellLibrary_typical.lib
NangateOpenCellLibrary_typical.lib
 
 
README.md
README.md
 
 
edit.py
edit.py
 
 
extract_tinyrocket_csrfile_sec.py
extract_tinyrocket_csrfile_sec.py
 
 
fakeram45_1024x32.lib
fakeram45_1024x32.lib
 
 
fakeram45_64x15.lib
fakeram45_64x15.lib
 
 
fakeram45_64x32.lib
fakeram45_64x32.lib
 
 
test_config_naja_if.yaml
test_config_naja_if.yaml
 
 
test_config_verilog.yaml
test_config_verilog.yaml
 
 
test_config_verilog_tinyrocket_csrfile_sec.yaml
test_config_verilog_tinyrocket_csrfile_sec.yaml
 
 
test_config_verilog_tinyrocket_sec.yaml
test_config_verilog_tinyrocket_sec.yaml
 
 
tinyrocket.v
tinyrocket.v
 
 
tinyrocket_csrfile_wrapper.v
tinyrocket_csrfile_wrapper.v
 
 
tinyrocket_csrfile_wrapper_k3.v
tinyrocket_csrfile_wrapper_k3.v
 
 
tinyrocket_edited.v
tinyrocket_edited.v
 
 
to_naja_if.py
to_naja_if.py
 
 

README.md

Examples

Instructions

# Through binary flags

## Verilog example
../build/src/bin/kepler-formal -verilog tinyrocket.v tinyrocket_edited.v \
  NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib fakeram45_64x15.lib

## naja_if example
../build/src/bin/kepler-formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if \
  NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib fakeram45_64x15.lib

# Through config file

## LEC YAML example
../build/src/bin/kepler-formal --config test_config_verilog.yaml

## SEC YAML example
../build/src/bin/kepler-formal --config test_config_verilog_tinyrocket_sec.yaml