georgerennie

General architecture for a hardware model checking tool

Key Principles

• Things should feel real time
  • Solvers should be able to communicate between threads rapidly for clause sharing, solver shutdown etc
  • Main thread should be only used for comms between/launching threads, UI/user scripts should run in their own thread so you don't get the case where e.g. you can't load a CEX while a script is running
• Users should have the power to control proof performance in sound and intuitive

georgerennie

#include <algorithm>
#include <array>
#include <atomic>
#include <cassert>
#include <chrono>
#include <cstdint>
#include <iostream>
#include <limits>
#include <mutex>
#include <optional>

georgerennie

.PHONY: install
install:
	mkdir -p /usr/bin
	cp csby.sh /usr/bin/csby
	sudo chmod +x /usr/bin/csby

georgerennie

package chisel3.util.experimental

import chisel3._
import chisel3.experimental.{annotate, ChiselAnnotation}
import firrtl.annotations._

object memoryArrayInitInline {
  def apply[T <: Data](memory: MemBase[T], data: Seq[BigInt]): Unit = {
    annotate(new ChiselAnnotation {
      override def toFirrtl = MemoryArrayInitAnnotation(memory.toTarget, data)

georgerennie

#! /bin/sh
set -x

# Clear old install
sudo rm -rf /usr/share/discord/

TEMP_DIR=$(mktemp -d)

cd $TEMP_DIR