GaloisInc/HARDENS issues and pull requests

#100 - trim down unused lando

Issue - State: closed - Opened by podhrmic over 2 years ago - 2 comments
Labels: documentation, ENHANCEMENT, specifications, Lando/Lobot

#99 - characterize what final document-centric deliverable will look like for the NRC and team

Issue - State: closed - Opened by kiniry over 2 years ago - 1 comment
Labels: documentation, ENHANCEMENT, On Deck

#98 - FPGA utilization

Issue - State: open - Opened by podhrmic over 2 years ago - 1 comment
Labels: hardware, software, WiP, Someday

#97 - add riscv-formal to docker image

Issue - State: closed - Opened by kiniry over 2 years ago - 1 comment
Labels: ENHANCEMENT, docker, On Deck, assurance, build system, Q/A

#96 - add RISC-V tools to docker image

Issue - State: closed - Opened by kiniry over 2 years ago - 1 comment
Labels: ENHANCEMENT, FEATURE, docker, On Deck, BLOCKED, build system, feature model

#95 - create new top-level Makefile that drives all system builds and V&V

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, On Deck, assurance, build system, feature model, Q/A, Someday

#94 - update docs to mention availability of artifactory docker image builds and their use

Issue - State: closed - Opened by kiniry over 2 years ago - 1 comment
Labels: documentation, ENHANCEMENT, docker, On Deck

#93 - Minor docker fixes

Pull Request - State: closed - Opened by podhrmic over 2 years ago - 1 comment

#92 - Significantly reduced docker image size, updated README

Pull Request - State: closed - Opened by podhrmic over 2 years ago

#91 - Merge develop into main for Task 2 release

Pull Request - State: closed - Opened by andrew-bivin over 2 years ago

#90 - Add Task 2 description to README

Pull Request - State: closed - Opened by andrew-bivin over 2 years ago

#89 - build and run our system in software simulation using non-Verilator hardware simulators

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, hardware, Q/A, Someday

#88 - measure code coverage of runtime verification

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, assurance, Q/A, Someday

#87 - Cryptol property to implementation property coverage

Issue - State: open - Opened by kiniry over 2 years ago
Labels: documentation, ENHANCEMENT, specifications, software, verification, On Deck, assurance, Q/A, source code, cryptol, ACSL, Someday

#86 - measure Cryptol model coverage

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, assurance, cryptol, Someday

#85 - Ongoing revisions of assurance write-up for the task 2 deliverable.

Pull Request - State: closed - Opened by kiniry over 2 years ago
Labels: documentation, ENHANCEMENT, WiP, assurance

#84 - single core NERV SoC self-test

Pull Request - State: closed - Opened by podhrmic over 2 years ago - 4 comments

#83 - add stub of i2c interface for the sensor reads

Pull Request - State: closed - Opened by podhrmic over 2 years ago

#82 - Update docker with saw, cryptol, cryptol-verilogc and crymp

Pull Request - State: closed - Opened by podhrmic over 2 years ago

#81 - Add versions/branches for Galois tools

Pull Request - State: closed - Opened by abakst over 2 years ago

#80 - Add Linux builds of cryptol-verilog and crymp

Pull Request - State: closed - Opened by abakst over 2 years ago - 7 comments

#79 - Implement end to end tests

Pull Request - State: closed - Opened by abakst over 2 years ago - 3 comments
Labels: assurance, Q/A

#78 - Add frettish requirement for self test

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: specifications

#77 - Add configurable sensor simulation bias

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: ENHANCEMENT, FEATURE, assurance, Q/A

#76 - Add ACSL specs

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: assurance

#75 - Add saturation table to SysMLv2 specification

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: specifications, architecture, SysML

#74 - Nerv2 with self test

Pull Request - State: closed - Opened by podhrmic over 2 years ago - 1 comment

#73 - Ensure SAW proofs work in Docker container

Issue - State: closed - Opened by abakst over 2 years ago - 3 comments

#72 - Simple SoC

Pull Request - State: closed - Opened by podhrmic over 2 years ago - 6 comments
Labels: ENHANCEMENT, hardware

#71 - Implement self test

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: FEATURE, source code

#70 - DRAFT: Snapshot of ongoing revisions of SysML specification.

Pull Request - State: closed - Opened by kiniry over 2 years ago - 1 comment
Labels: WiP

#69 - Cryptol Model: Replace magic constants with variables

Issue - State: open - Opened by abakst over 2 years ago - 1 comment
Labels: ENHANCEMENT, cryptol, Someday

#68 - Revise SysML/lando events/scenarios specifications

Pull Request - State: closed - Opened by abakst over 2 years ago - 1 comment

#67 - Fix dockerfile

Pull Request - State: closed - Opened by podhrmic over 2 years ago

#66 - Add disclaimers to top-level README

Pull Request - State: closed - Opened by andrew-bivin over 2 years ago - 1 comment

#65 - Use table-based Saturation Margin

Pull Request - State: closed - Opened by abakst over 2 years ago
Labels: ENHANCEMENT, source code

#64 - Document branches/versions of dependencies

Issue - State: closed - Opened by abakst over 2 years ago
Labels: documentation

#63 - Invoke the actuator from the "core" program (and do so only once).

Pull Request - State: closed - Opened by abakst over 2 years ago

#62 - Implement self test

Issue - State: closed - Opened by abakst over 2 years ago - 1 comment
Labels: source code

#61 - SAW proofs

Pull Request - State: closed - Opened by abakst over 2 years ago - 2 comments

#60 - write and check Bluecheck properties on SoC

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, specifications, hardware, verification, assurance, Someday

#59 - write-up of assurance case

Issue - State: closed - Opened by abakst over 2 years ago - 1 comment
Labels: documentation, assurance

#58 - write a "bottom" implementation of the system (as we did in previous systems where every function body is basically assert false) to ensure that the ACSL spec is sound

Issue - State: closed - Opened by kiniry over 2 years ago - 3 comments
Labels: ENHANCEMENT, specifications, verification, On Deck, assurance

#57 - ACSL models and Frama-C V&V

Issue - State: closed - Opened by kiniry over 2 years ago - 4 comments
Labels: ENHANCEMENT, specifications, verification, On Deck, Q/A

#56 - build a potentially executable (down the road) SysML model of these behavioral specs using Individuals and Snapshots.

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, verification, assurance, Q/A, SysML, Someday

#55 - get all NERV SoC smoketests (single core and three core) up and running reliably

Issue - State: open - Opened by kiniry over 2 years ago - 5 comments
Labels: BUG, hardware, WiP, BLOCKED, build system, feature model, Lando/Lobot, Someday

#54 - end-to-end test script

Issue - State: closed - Opened by abakst over 2 years ago - 1 comment
Labels: ENHANCEMENT, Q/A

#53 - add build feature to bias sensor data

Issue - State: closed - Opened by abakst over 2 years ago - 1 comment

#52 - add a mock model for actuator

Issue - State: closed - Opened by abakst over 2 years ago - 1 comment
Labels: ENHANCEMENT

#51 - setup build system to cross-compile application to the NERV build and ensure that the build rules align with the feature model's spec of product variants.

Issue - State: open - Opened by kiniry over 2 years ago
Labels: ENHANCEMENT, software, On Deck, build system, feature model, Someday

#50 - Handwritten implementations

Pull Request - State: closed - Opened by abakst over 2 years ago

#49 - hand-written implementations of actuation unit, instrumentation

Issue - State: closed - Opened by abakst over 2 years ago - 2 comments
Labels: ENHANCEMENT, hardware, software, On Deck, source code

#48 - add table-based saturation margin implementation

Issue - State: closed - Opened by abakst over 2 years ago - 4 comments
Labels: ENHANCEMENT, specifications, source code, cryptol

#47 - Simulate devices

Pull Request - State: closed - Opened by abakst over 2 years ago

#46 - update Docker image with additional tools

Issue - State: closed - Opened by podhrmic over 2 years ago - 2 comments
Labels: build system

#45 - revise scenario specifications to reflect final system under V&V

Issue - State: closed - Opened by kiniry over 2 years ago - 3 comments
Labels: ENHANCEMENT, specifications, architecture, On Deck, Lando/Lobot, SysML

#44 - revise events specifications to reflect final system under V&V

Issue - State: open - Opened by kiniry over 2 years ago - 3 comments
Labels: documentation, ENHANCEMENT, specifications, architecture, On Deck, Lando/Lobot, SysML, Someday

#43 - Task 1 deliverable release into main

Pull Request - State: closed - Opened by andrew-bivin over 2 years ago

#42 - Task 1 documentation for delivery.

Pull Request - State: closed - Opened by kiniry over 2 years ago
Labels: Ready for Review

#41 - 28 events and scenarios

Pull Request - State: closed - Opened by kiniry over 2 years ago
Labels: Ready for Review

#40 - handle all outstanding `@todo` annotations in Lando model

Issue - State: open - Opened by kiniry over 2 years ago - 3 comments
Labels: documentation, specifications, Lando/Lobot, Someday

#39 - Add directory structure

Pull Request - State: closed - Opened by abakst over 2 years ago

#38 - Update `README.md` for Dec 17 release

Issue - State: closed - Opened by abakst over 2 years ago

#37 - Cryptol model improvement + Specify test procedures

Pull Request - State: closed - Opened by abakst over 2 years ago

#36 - Update Requirements

Pull Request - State: closed - Opened by abakst almost 3 years ago - 1 comment

#35 - Implementation of C components (harnesses + generated code)

Pull Request - State: closed - Opened by abakst almost 3 years ago

#34 - Generate implementation of core logic from Cryptol Model

Issue - State: closed - Opened by abakst almost 3 years ago
Labels: hardware, software, source code

#33 - Executable Cryptol Model

Pull Request - State: closed - Opened by abakst almost 3 years ago

#32 - Sys ml spec

Pull Request - State: closed - Opened by podhrmic almost 3 years ago - 1 comment

#31 - SoC design questions

Issue - State: closed - Opened by podhrmic almost 3 years ago - 2 comments
Labels: architecture, hardware

#30 - revise and extend SysML specification

Issue - State: open - Opened by kiniry almost 3 years ago - 6 comments
Labels: documentation, ENHANCEMENT, specifications, FEATURE, architecture, verification, assurance, feature model, Lando/Lobot, cryptol, SysML, ACSL, Someday

#29 - Cryptol model of RTS

Issue - State: closed - Opened by abakst almost 3 years ago
Labels: cryptol

#28 - Specify demonstrator scenarios and events

Issue - State: closed - Opened by kiniry almost 3 years ago - 4 comments
Labels: documentation, specifications, FEATURE, architecture, WiP, Lando/Lobot

#27 - Initial SoC commits

Pull Request - State: closed - Opened by podhrmic almost 3 years ago - 2 comments

#26 - install and configure Eclipse SysMLv2

Issue - State: closed - Opened by kiniry almost 3 years ago - 4 comments
Labels: specifications, FEATURE, WiP, SysML

#25 - Requirements first draft

Pull Request - State: closed - Opened by abakst almost 3 years ago - 1 comment
Labels: architecture

#24 - Requirements: specify setpoint doesn't change

Issue - State: closed - Opened by abakst almost 3 years ago - 1 comment

#23 - Self Test Requirements

Issue - State: closed - Opened by abakst almost 3 years ago - 4 comments
Labels: specifications, assurance, Q/A

#22 - Requirements Issues

Issue - State: closed - Opened by abakst almost 3 years ago - 3 comments
Labels: specifications

#21 - Spin up Ubuntu VM

Issue - State: closed - Opened by abakst almost 3 years ago - 3 comments

#20 - ensure that all build configurations are supported by RTS build system.

Issue - State: closed - Opened by kiniry almost 3 years ago - 1 comment
Labels: ENHANCEMENT, FEATURE, On Deck, build system, feature model

#19 - Refine feature model constraints after RTS models are written.

Issue - State: closed - Opened by kiniry almost 3 years ago - 1 comment
Labels: ENHANCEMENT, specifications, FEATURE

#18 - Refine feature model to reflect system architecture.

Issue - State: closed - Opened by kiniry almost 3 years ago - 1 comment
Labels: ENHANCEMENT, specifications, feature model

#17 - Add proposal as a reference to the project documentation.

Pull Request - State: closed - Opened by kiniry almost 3 years ago
Labels: documentation, ENHANCEMENT

#16 - Snapshot of basic design files from Lattice.

Pull Request - State: closed - Opened by kiniry almost 3 years ago
Labels: documentation, hardware

#15 - Updated Lando highlighting mode for Emacs.

Pull Request - State: closed - Opened by kiniry almost 3 years ago
Labels: ENHANCEMENT, software

#14 - 5 lando lobot

Pull Request - State: closed - Opened by kiniry almost 3 years ago
Labels: documentation, specifications, architecture, hardware, software, Ready for Review

#13 - Lattice ECP 5 documentation

Pull Request - State: closed - Opened by kiniry almost 3 years ago
Labels: documentation, hardware

#12 - Decide on Requirements Specification Language

Issue - State: closed - Opened by abakst almost 3 years ago - 1 comment
Labels: specifications, architecture, software

#11 - Determine, source, and document implementation components (sensors/actuators)

Issue - State: closed - Opened by andrew-bivin almost 3 years ago - 3 comments
Labels: documentation, hardware

#10 - Create a SysML system architecture spec (refinement of high level LANDO spec)

Issue - State: closed - Opened by andrew-bivin almost 3 years ago - 1 comment
Labels: specifications, architecture

#9 - Setup a HARDENS Artifactory package for internal sharing of Docker containers

Issue - State: closed - Opened by kiniry almost 3 years ago - 2 comments
Labels: ENHANCEMENT, docker

#8 - Dockerfile with FPGA tools

Pull Request - State: closed - Opened by podhrmic almost 3 years ago - 1 comment
Labels: documentation

#7 - Create Docker container for dev use & enable remote access

Issue - State: closed - Opened by andrew-bivin almost 3 years ago
Labels: docker

#6 - Determine which RISC-V core to use based on system/proposal requirements

Issue - State: closed - Opened by andrew-bivin almost 3 years ago - 12 comments
Labels: hardware

#5 - Write high-level system spec in LANDO & product line spec in LOBOT

Issue - State: closed - Opened by andrew-bivin almost 3 years ago - 1 comment
Labels: specifications, architecture

#4 - add labels for project tasks

Issue - State: closed - Opened by kiniry almost 3 years ago - 2 comments
Labels: ENHANCEMENT

#3 - create milestones for project per our SoW

Issue - State: closed - Opened by kiniry almost 3 years ago - 1 comment
Labels: ENHANCEMENT

#2 - purchase and distribute initial FPGA dev boards

Issue - State: closed - Opened by kiniry almost 3 years ago - 6 comments
Labels: ENHANCEMENT

#1 - Update README.md

Pull Request - State: closed - Opened by kiniry almost 3 years ago - 1 comment
Labels: documentation, ENHANCEMENT

GitHub / GaloisInc/HARDENS issues and pull requests